omega/examples/old_test/verlind1


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

   without_simplify;
   
   R3 := {[x] -> [y] : (y = x) | (y = 3x)};

   Rf := {[x] -> [y] : x <= y <= 3x};

   R3;

   Rf;

   s12 := {[x] : 1 <= x <= 2};
   s12;

   sd3 := R3(s12);
   sd3;

   sc3 := Rf(s12);
   sc3;

   sc3 intersection sd3;

   # I think this is faulty
   sc3 - sd3;

   # This is OK
   sd3 - sc3;

   complement sc3;
   complement sd3;

   sc3;

   sc3 intersection (complement sd3);

   # alternative description of sd3;
   sd3' := {[y] : 1 <= y <= 3 | y = 6};
   sd3';
   sc3 - sd3';

   # sd3 wrt sd3';

   sd3 - sd3';

   sd3' - sd3;