# 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.