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
|
# Omega Calculator v1.2 (based on Omega Library 1.2, August, 2000):
# T1 := {[k,i,j] -> [k',i,j] : 1 <= k < k' < i <= 1024 && k'+1 <= j <= 1024};
#
# T2 := {[k,i,j] -> [j,i,j'] : 1 <= k < j < i <= 1024 && j < j' <= 1024};
#
# T3 := {[k,k+1,k+1] -> [k+1,i',j'] : 1 <= k <= i'-2, j'-2 && j' <= 1024 && i' <= 1024};
#
#
# # The following expression evaluates to FALSE, which I believe is incorrect:
#
# T3+;
{[k,k+1,k+1] -> [Out_1,i,j] : 1 <= k < Out_1 < i <= 1024 && Out_1+1 <= j <= 1024}
#
#
# # And the following cause assertion failures:
#
# (T2 union T3)+;
{[k,k+1,k+1] -> [j',i',j''] : 1 <= k < j' < i' <= 1024 && j'+1 <= j'' <= 1024} union
{[k,i,i-1] -> [j',i',j''] : k+2 <= i <= j' < j'' <= 1024 && j' < i' <= 1024 && 1 <= k} union
{[k,i,j] -> [j',i',j''] : j+2 <= i <= j' < i' <= 1024 && 1 <= k < j && j' < j'' <= 1024} union
{[k,i,j] -> [j',i,j''] : 1 <= k < j < j' < i <= 1024 && j' < j'' <= 1024} union
{[k,i,j] -> [j,i,j''] : 1 <= k < j < i <= 1024 && j < j'' <= 1024}
#
# (T1 union T2)+;
{[k,i,j] -> [Out_1,i,j] : 1 <= k < Out_1 < i <= 1024 && Out_1+1 <= j <= 1024} union
{[k,i,j] -> [Out_1,i,j'] : 1 <= k < j < Out_1 < i <= 1024 && Out_1 < j' <= 1024} union
{[k,i,j] -> [j,i,j'] : 1 <= k < j < i <= 1024 && j < j' <= 1024}
#
#
# # This comes from Guassian Elimination.
|
