summaryrefslogtreecommitdiff
path: root/omega/examples/old_test/tex1
diff options
context:
space:
mode:
Diffstat (limited to 'omega/examples/old_test/tex1')
-rw-r--r--omega/examples/old_test/tex149
1 files changed, 49 insertions, 0 deletions
diff --git a/omega/examples/old_test/tex1 b/omega/examples/old_test/tex1
new file mode 100644
index 0000000..ca84924
--- /dev/null
+++ b/omega/examples/old_test/tex1
@@ -0,0 +1,49 @@
+#
+# Extract from omega4
+# removed "eqnarray" commands, associated &'s, and overbrace commands
+# added declaration of n
+# added semicolon
+#
+# It would be nice not to have to do the following:
+# removed \ in front of variable names
+#
+
+$$
+symbolic n;
+R := \{\ [ii] \rightarrow [ki] \mid
+1 \leq ii \leq 2n
+ \ \land \ 1 \leq ki \leq 2n
+\land ii = ki
+\land ii = ki\\
+\t \land
+ \ \neg (\ \exists [ji, jj] \st
+(1 \leq ji \leq 2n \land 1 \leq jj \leq n\!-\!1)
+\land (ii \leq ji \land ji \leq ki) \land (2jj = ki)\ )\\
+\t
+\land \
+\neg (\ \exists [ji, jj] \st
+(1 \leq ji \leq 2n \land 1 \leq jj \leq n\!-\!1)
+\land (ii \leq ji \land ji \leq ki) \land (2jj\!+\!1 = ki)\ )
+\ \}
+;
+
+R;
+$$
+# S := \{\ [\ii] \rightarrow [\ki] \mid
+# 1 \leq \ii \leq 2\n
+# \ \land \ 1 \leq \ki \leq 2\n
+# \land \ii = \ki
+# \land \ii = \ki\\
+# \t \land
+# \ \neg (\ \exists [\ji, \jj] \st
+# (1 \leq \ji \leq 2\n \land 1 \leq \jj \leq \n\!-\!1)
+# \land (\ii \leq \ji \land \ji \leq \ki) \land (2\jj = \ki)\ )\\
+# \t
+# \land \
+# \neg (\ \exists [\ji, \jj] \st
+# (1 \leq \ji \leq 2\n \land 1 \leq \jj \leq \n\!-\!1)
+# \land (\ii \leq \ji \land \ji \leq \ki) \land (2\jj\!+\!1 = \ki)\ )
+# \ \}
+# ;
+#
+# S;