blob: 109e02926ae9a08d0a74ce4d31dcdf441b6fe7fc (
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# R := { [i] -> [i'] : 1 <= i,i' <= 10 && i' = i+1 };
#
# R;
{[i] -> [i+1] : 1 <= i <= 9}
#
# inverse R;
{[i] -> [i-1] : 2 <= i <= 10}
#
# domain R;
{[i]: 1 <= i <= 9}
#
# range R;
{[i]: 2 <= i <= 10}
#
# R compose R;
{[i] -> [i+2] : 1 <= i <= 8}
#
# R+;
{[i] -> [i'] : 1 <= i < i' <= 10}
# # closure of R = R union (R compose R) union (R compose R ...
# complement R;
{[i] -> [i'] : i <= 0} union
{[i] -> [i'] : 10 <= i} union
{[i] -> [i'] : 1 <= i <= 9, i'-2} union
{[i] -> [i'] : 1, i' <= i <= 9}
#
# S := {[i] : 5 <= i <= 25};
#
# S;
{[i]: 5 <= i <= 25}
#
# R(S);
{[i]: 6 <= i <= 10}
# # apply R to S
# R \ S;
{[i] -> [i+1] : 5 <= i <= 9}
# # restrict domain of R to S
# R / S;
{[i] -> [i+1] : 4 <= i <= 9}
# # restrict range of R to S
# (R\S) union (R/S);
{[i] -> [i+1] : 4 <= i <= 9}
#
# (R\S) intersection (R/S);
{[i] -> [i+1] : 5 <= i <= 9}
#
# (R/S) - (R\S);
{[4] -> [5] }
#
# S*S;
{[i] -> [i'] : 5 <= i <= 25 && 5 <= i' <= 25}
# # cross product
# D := S - {[9:16:2]} - {[17:19]};
#
# D;
{[i]: 5 <= i <= 8} union
{[i]: Exists ( alpha : 2alpha = i && 10 <= i <= 16)} union
{[i]: 20 <= i <= 25}
#
# T := { [i] : 1 <= i <= 11 & exists (a : i = 2a) };
#
# T;
{[i]: Exists ( alpha : 2alpha = i && 2 <= i <= 10)}
#
# Hull T;
{[i]: 2 <= i <= 10}
#
# Hull D;
{[i]: 5 <= i <= 25}
#
# codegen D;
for(t1 = 5; t1 <= 8; t1++) {
s1(t1);
}
for(t1 = 10; t1 <= 16; t1 += 2) {
s1(t1);
}
for(t1 = 20; t1 <= 25; t1++) {
s1(t1);
}
#
# codegen {[i,j] : 1 <= i+j,j <= 10};
for(t1 = -9; t1 <= 9; t1++) {
for(t2 = max(-t1+1,1); t2 <= min(-t1+10,10); t2++) {
s1(t1,t2);
}
}
#
|
