blob: 050b1995db1b99d401fa667df7eab5e68a88950a (
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
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# R3 := {[x] -> [y] : (y = x) | (y = 3x)};
#
#
# Rf := {[x] -> [y] : x <= y <= 3x};
#
#
# R3;
{[x] -> [x] } union
{[x] -> [3x] }
#
#
# Rf;
{[x] -> [y] : x <= y <= 3x}
#
#
# s12 := {[x] : 1 <= x <= 2};
#
# s12;
{[x]: 1 <= x <= 2}
#
#
# sd3 := R3(s12);
#
# sd3;
{[y]: 1 <= y <= 2} union
{[y]: Exists ( alpha : y = 3alpha && 3 <= y <= 6)}
#
#
# sc3 := Rf(s12);
#
# sc3;
{[y]: 1 <= y <= 6}
#
#
# sc3 intersection sd3;
{[y]: 1 <= y <= 2} union
{[y]: Exists ( alpha : y = 3alpha && 3 <= y <= 6)}
#
#
# # I think this is faulty
# sc3 - sd3;
{[y]: 4 <= y <= 5}
#
#
# # This is OK
# sd3 - sc3;
{[y] : FALSE }
#
#
# complement sc3;
{[y]: y <= 0} union
{[y]: 7 <= y}
#
# complement sd3;
{[y]: y <= 0} union
{[y]: 7 <= y} union
{[y]: 4 <= y <= 5}
#
#
# sc3;
{[y]: 1 <= y <= 6}
#
#
# sc3 intersection (complement sd3);
{[y]: 4 <= y <= 5}
#
#
# # alternative description of sd3;
# sd3' := {[y] : 1 <= y <= 3 | y = 6};
#
# sd3';
{[y]: 1 <= y <= 3} union
{[6]}
#
# sc3 - sd3';
{[y]: 4 <= y <= 5}
#
#
# # sd3 wrt sd3';
#
# sd3 - sd3';
{[y] : FALSE }
#
#
# sd3' - sd3;
{[y] : FALSE }
#
|
