blob: fd138d05e5e03be1a4719e39484f62c9ccbffcc6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# #
# # 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;
{[ii] -> [ii] : n = 1 && 1 <= ii <= 2} union
{[2n] -> [2n] : 2 <= n} union
{[1] -> [1] : 2 <= n}
#
# $$
# # 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;
|
