blob: 614a9fb1a1871a122162ff465ca57770f08eb12e (
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
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# symbolic n(1);
#
# S := { [i] -> [j] : 1 <= i < j <= 100 && n(j) >= 0};
#
# R := domain S;
#
# S;
{[i] -> [j] : 1 <= i < j <= 100 && 0 <= n(j)}
#
# R;
{[i]: 1 <= i <= 99 && UNKNOWN}
#
# upper_bound R;
{[i]: 1 <= i <= 99}
#
# lower_bound R;
{[i] : FALSE }
#
#
# R - {[1:50]};
{[i]: 51 <= i <= 99 && UNKNOWN}
#
# {[1:50]} - R;
{[i]: 1 <= i <= 50 && UNKNOWN}
#
# {[1:50]} - upper_bound R;
{[i] : FALSE }
#
# {[1:50]} - lower_bound R;
{[i]: 1 <= i <= 50}
#
#
# R union {[10:30]} union {[25:100]} union {[1:10]};
{[i]: 1 <= i <= 99 && UNKNOWN} union
{[i]: 10 <= i <= 30} union
{[i]: 25 <= i <= 100} union
{[i]: 1 <= i <= 10}
#
# upper_bound (R union {[10:30]} union {[25:100]} union {[1:10]});
{[i]: 1 <= i <= 99} union
{[i]: 25 <= i <= 100}
#
# lower_bound (R union {[10:30]} union {[25:100]} union {[1:10]});
{[i]: 10 <= i <= 30} union
{[i]: 25 <= i <= 100} union
{[i]: 1 <= i <= 10}
#
#
# {[101:200]} - R;
{[i]: 101 <= i <= 200}
#
# {[1:200]} - R;
{[i]: 1 <= i <= 99 && UNKNOWN} union
{[i]: 100 <= i <= 200}
#
# {[1:200]} - R - {[10:30]} - {[25:100]};
{[i]: 1 <= i <= 9 && UNKNOWN} union
{[i]: 101 <= i <= 200}
#
# {[1:200]} - (R union {[10:30]} union {[25:100]} union {[1:10]});
{[i]: 101 <= i <= 200}
#
# {[1:200]} - R - {[10:30]} - {[25:100]} - {[1:10]};
{[i]: 101 <= i <= 200}
#
|
