YES(?,O(n^2)) Problem: a12(a12(x1)) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a34(a34(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a45(a45(x1)) -> x1 a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a24(x1) -> a23(a34(a23(x1))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a46(x1) -> a45(a56(a45(x1))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) Proof: RT Transformation Processor: strict: a12(a12(x1)) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a34(a34(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a45(a45(x1)) -> x1 a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a24(x1) -> a23(a34(a23(x1))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a46(x1) -> a45(a56(a45(x1))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [a56](x0) = x0, [a46](x0) = x0, [a45](x0) = x0, [a36](x0) = x0 + 20, [a35](x0) = x0 + 4, [a34](x0) = x0, [a26](x0) = x0 + 4, [a25](x0) = x0 + 16, [a24](x0) = x0 + 6, [a23](x0) = x0 + 3, [a16](x0) = x0 + 24, [a15](x0) = x0 + 9, [a14](x0) = x0 + 8, [a13](x0) = x0 + 10, [a12](x0) = x0 orientation: a12(a12(x1)) = x1 >= x1 = x1 a13(a13(x1)) = x1 + 20 >= x1 = x1 a14(a14(x1)) = x1 + 16 >= x1 = x1 a15(a15(x1)) = x1 + 18 >= x1 = x1 a16(a16(x1)) = x1 + 48 >= x1 = x1 a23(a23(x1)) = x1 + 6 >= x1 = x1 a24(a24(x1)) = x1 + 12 >= x1 = x1 a25(a25(x1)) = x1 + 32 >= x1 = x1 a26(a26(x1)) = x1 + 8 >= x1 = x1 a34(a34(x1)) = x1 >= x1 = x1 a35(a35(x1)) = x1 + 8 >= x1 = x1 a36(a36(x1)) = x1 + 40 >= x1 = x1 a45(a45(x1)) = x1 >= x1 = x1 a46(a46(x1)) = x1 >= x1 = x1 a56(a56(x1)) = x1 >= x1 = x1 a13(x1) = x1 + 10 >= x1 + 3 = a12(a23(a12(x1))) a14(x1) = x1 + 8 >= x1 + 6 = a12(a23(a34(a23(a12(x1))))) a15(x1) = x1 + 9 >= x1 + 6 = a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) = x1 + 24 >= x1 + 6 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a24(x1) = x1 + 6 >= x1 + 6 = a23(a34(a23(x1))) a25(x1) = x1 + 16 >= x1 + 6 = a23(a34(a45(a34(a23(x1))))) a26(x1) = x1 + 4 >= x1 + 6 = a23(a34(a45(a56(a45(a34(a23(x1))))))) a35(x1) = x1 + 4 >= x1 = a34(a45(a34(x1))) a36(x1) = x1 + 20 >= x1 = a34(a45(a56(a45(a34(x1))))) a46(x1) = x1 >= x1 = a45(a56(a45(x1))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 9 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 9 >= x1 = x1 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) a12(a56(x1)) = x1 >= x1 = a56(a12(x1)) a23(a45(x1)) = x1 + 3 >= x1 + 3 = a45(a23(x1)) a23(a56(x1)) = x1 + 3 >= x1 + 3 = a56(a23(x1)) a34(a56(x1)) = x1 >= x1 = a56(a34(x1)) problem: strict: a12(a12(x1)) -> x1 a34(a34(x1)) -> x1 a45(a45(x1)) -> x1 a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a46(x1) -> a45(a56(a45(x1))) a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 1 interpretation: [a56](x0) = x0, [a46](x0) = x0, [a45](x0) = x0, [a36](x0) = x0 + 10, [a35](x0) = x0 + 10, [a34](x0) = x0 + 5, [a26](x0) = x0, [a25](x0) = x0 + 26, [a24](x0) = x0, [a23](x0) = x0 + 8, [a16](x0) = x0 + 28, [a15](x0) = x0 + 28, [a14](x0) = x0 + 21, [a13](x0) = x0 + 8, [a12](x0) = x0 orientation: a12(a12(x1)) = x1 >= x1 = x1 a34(a34(x1)) = x1 + 10 >= x1 = x1 a45(a45(x1)) = x1 >= x1 = x1 a46(a46(x1)) = x1 >= x1 = x1 a56(a56(x1)) = x1 >= x1 = x1 a24(x1) = x1 >= x1 + 21 = a23(a34(a23(x1))) a26(x1) = x1 >= x1 + 26 = a23(a34(a45(a56(a45(a34(a23(x1))))))) a46(x1) = x1 >= x1 = a45(a56(a45(x1))) a34(a45(a34(a45(a34(a45(x1)))))) = x1 + 15 >= x1 = x1 a45(a56(a45(a56(a45(a56(x1)))))) = x1 >= x1 = x1 a12(a34(x1)) = x1 + 5 >= x1 + 5 = a34(a12(x1)) a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) a12(a56(x1)) = x1 >= x1 = a56(a12(x1)) a23(a45(x1)) = x1 + 8 >= x1 + 8 = a45(a23(x1)) a23(a56(x1)) = x1 + 8 >= x1 + 8 = a56(a23(x1)) a34(a56(x1)) = x1 + 5 >= x1 + 5 = a56(a34(x1)) a13(a13(x1)) = x1 + 16 >= x1 = x1 a14(a14(x1)) = x1 + 42 >= x1 = x1 a15(a15(x1)) = x1 + 56 >= x1 = x1 a16(a16(x1)) = x1 + 56 >= x1 = x1 a23(a23(x1)) = x1 + 16 >= x1 = x1 a24(a24(x1)) = x1 >= x1 = x1 a25(a25(x1)) = x1 + 52 >= x1 = x1 a26(a26(x1)) = x1 >= x1 = x1 a35(a35(x1)) = x1 + 20 >= x1 = x1 a36(a36(x1)) = x1 + 20 >= x1 = x1 a13(x1) = x1 + 8 >= x1 + 8 = a12(a23(a12(x1))) a14(x1) = x1 + 21 >= x1 + 21 = a12(a23(a34(a23(a12(x1))))) a15(x1) = x1 + 28 >= x1 + 26 = a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) = x1 + 28 >= x1 + 26 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) = x1 + 26 >= x1 + 26 = a23(a34(a45(a34(a23(x1))))) a35(x1) = x1 + 10 >= x1 + 10 = a34(a45(a34(x1))) a36(x1) = x1 + 10 >= x1 + 10 = a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 24 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 39 >= x1 = x1 problem: strict: a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 1 interpretation: [a56](x0) = x0 + 2, [a46](x0) = x0 + 8, [a45](x0) = x0, [a36](x0) = x0 + 2, [a35](x0) = x0, [a34](x0) = x0, [a26](x0) = x0, [a25](x0) = x0 + 2, [a24](x0) = x0, [a23](x0) = x0 + 1, [a16](x0) = x0 + 4, [a15](x0) = x0 + 2, [a14](x0) = x0 + 3, [a13](x0) = x0 + 16, [a12](x0) = x0 orientation: a12(a12(x1)) = x1 >= x1 = x1 a45(a45(x1)) = x1 >= x1 = x1 a46(a46(x1)) = x1 + 16 >= x1 = x1 a56(a56(x1)) = x1 + 4 >= x1 = x1 a24(x1) = x1 >= x1 + 2 = a23(a34(a23(x1))) a26(x1) = x1 >= x1 + 4 = a23(a34(a45(a56(a45(a34(a23(x1))))))) a46(x1) = x1 + 8 >= x1 + 2 = a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 6 >= x1 = x1 a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) a12(a56(x1)) = x1 + 2 >= x1 + 2 = a56(a12(x1)) a23(a45(x1)) = x1 + 1 >= x1 + 1 = a45(a23(x1)) a23(a56(x1)) = x1 + 3 >= x1 + 3 = a56(a23(x1)) a34(a56(x1)) = x1 + 2 >= x1 + 2 = a56(a34(x1)) a34(a34(x1)) = x1 >= x1 = x1 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 a13(a13(x1)) = x1 + 32 >= x1 = x1 a14(a14(x1)) = x1 + 6 >= x1 = x1 a15(a15(x1)) = x1 + 4 >= x1 = x1 a16(a16(x1)) = x1 + 8 >= x1 = x1 a23(a23(x1)) = x1 + 2 >= x1 = x1 a24(a24(x1)) = x1 >= x1 = x1 a25(a25(x1)) = x1 + 4 >= x1 = x1 a26(a26(x1)) = x1 >= x1 = x1 a35(a35(x1)) = x1 >= x1 = x1 a36(a36(x1)) = x1 + 4 >= x1 = x1 a13(x1) = x1 + 16 >= x1 + 1 = a12(a23(a12(x1))) a14(x1) = x1 + 3 >= x1 + 2 = a12(a23(a34(a23(a12(x1))))) a15(x1) = x1 + 2 >= x1 + 2 = a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) = x1 + 4 >= x1 + 4 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) = x1 + 2 >= x1 + 2 = a23(a34(a45(a34(a23(x1))))) a35(x1) = x1 >= x1 = a34(a45(a34(x1))) a36(x1) = x1 + 2 >= x1 + 2 = a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 3 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 3 >= x1 = x1 problem: strict: a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 1 interpretation: [a56](x0) = x0, [a46](x0) = x0 + 12, [a45](x0) = x0 + 6, [a36](x0) = x0 + 16, [a35](x0) = x0 + 16, [a34](x0) = x0, [a26](x0) = x0, [a25](x0) = x0 + 8, [a24](x0) = x0 + 16, [a23](x0) = x0 + 1, [a16](x0) = x0 + 16, [a15](x0) = x0 + 16, [a14](x0) = x0 + 4, [a13](x0) = x0 + 3, [a12](x0) = x0 + 1 orientation: a12(a12(x1)) = x1 + 2 >= x1 = x1 a45(a45(x1)) = x1 + 12 >= x1 = x1 a24(x1) = x1 + 16 >= x1 + 2 = a23(a34(a23(x1))) a26(x1) = x1 >= x1 + 14 = a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a34(x1)) = x1 + 1 >= x1 + 1 = a34(a12(x1)) a12(a45(x1)) = x1 + 7 >= x1 + 7 = a45(a12(x1)) a12(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a12(x1)) a23(a45(x1)) = x1 + 7 >= x1 + 7 = a45(a23(x1)) a23(a56(x1)) = x1 + 1 >= x1 + 1 = a56(a23(x1)) a34(a56(x1)) = x1 >= x1 = a56(a34(x1)) a46(a46(x1)) = x1 + 24 >= x1 = x1 a56(a56(x1)) = x1 >= x1 = x1 a46(x1) = x1 + 12 >= x1 + 12 = a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 18 >= x1 = x1 a34(a34(x1)) = x1 >= x1 = x1 a34(a45(a34(a45(a34(a45(x1)))))) = x1 + 18 >= x1 = x1 a13(a13(x1)) = x1 + 6 >= x1 = x1 a14(a14(x1)) = x1 + 8 >= x1 = x1 a15(a15(x1)) = x1 + 32 >= x1 = x1 a16(a16(x1)) = x1 + 32 >= x1 = x1 a23(a23(x1)) = x1 + 2 >= x1 = x1 a24(a24(x1)) = x1 + 32 >= x1 = x1 a25(a25(x1)) = x1 + 16 >= x1 = x1 a26(a26(x1)) = x1 >= x1 = x1 a35(a35(x1)) = x1 + 32 >= x1 = x1 a36(a36(x1)) = x1 + 32 >= x1 = x1 a13(x1) = x1 + 3 >= x1 + 3 = a12(a23(a12(x1))) a14(x1) = x1 + 4 >= x1 + 4 = a12(a23(a34(a23(a12(x1))))) a15(x1) = x1 + 16 >= x1 + 10 = a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) = x1 + 16 >= x1 + 16 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) = x1 + 8 >= x1 + 8 = a23(a34(a45(a34(a23(x1))))) a35(x1) = x1 + 16 >= x1 + 6 = a34(a45(a34(x1))) a36(x1) = x1 + 16 >= x1 + 12 = a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 6 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 3 >= x1 = x1 problem: strict: a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 1 interpretation: [a56](x0) = x0 + 26, [a46](x0) = x0 + 26, [a45](x0) = x0, [a36](x0) = x0 + 26, [a35](x0) = x0, [a34](x0) = x0, [a26](x0) = x0 + 31, [a25](x0) = x0 + 4, [a24](x0) = x0 + 8, [a23](x0) = x0 + 2, [a16](x0) = x0 + 31, [a15](x0) = x0 + 4, [a14](x0) = x0 + 16, [a13](x0) = x0 + 3, [a12](x0) = x0 orientation: a26(x1) = x1 + 31 >= x1 + 30 = a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) a12(a45(x1)) = x1 >= x1 = a45(a12(x1)) a12(a56(x1)) = x1 + 26 >= x1 + 26 = a56(a12(x1)) a23(a45(x1)) = x1 + 2 >= x1 + 2 = a45(a23(x1)) a23(a56(x1)) = x1 + 28 >= x1 + 28 = a56(a23(x1)) a34(a56(x1)) = x1 + 26 >= x1 + 26 = a56(a34(x1)) a12(a12(x1)) = x1 >= x1 = x1 a45(a45(x1)) = x1 >= x1 = x1 a24(x1) = x1 + 8 >= x1 + 4 = a23(a34(a23(x1))) a46(a46(x1)) = x1 + 52 >= x1 = x1 a56(a56(x1)) = x1 + 52 >= x1 = x1 a46(x1) = x1 + 26 >= x1 + 26 = a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) = x1 + 78 >= x1 = x1 a34(a34(x1)) = x1 >= x1 = x1 a34(a45(a34(a45(a34(a45(x1)))))) = x1 >= x1 = x1 a13(a13(x1)) = x1 + 6 >= x1 = x1 a14(a14(x1)) = x1 + 32 >= x1 = x1 a15(a15(x1)) = x1 + 8 >= x1 = x1 a16(a16(x1)) = x1 + 62 >= x1 = x1 a23(a23(x1)) = x1 + 4 >= x1 = x1 a24(a24(x1)) = x1 + 16 >= x1 = x1 a25(a25(x1)) = x1 + 8 >= x1 = x1 a26(a26(x1)) = x1 + 62 >= x1 = x1 a35(a35(x1)) = x1 >= x1 = x1 a36(a36(x1)) = x1 + 52 >= x1 = x1 a13(x1) = x1 + 3 >= x1 + 2 = a12(a23(a12(x1))) a14(x1) = x1 + 16 >= x1 + 4 = a12(a23(a34(a23(a12(x1))))) a15(x1) = x1 + 4 >= x1 + 4 = a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) = x1 + 31 >= x1 + 30 = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) = x1 + 4 >= x1 + 4 = a23(a34(a45(a34(a23(x1))))) a35(x1) = x1 >= x1 = a34(a45(a34(x1))) a36(x1) = x1 + 26 >= x1 + 26 = a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 + 6 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 + 6 >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [1 2] [1] [a56](x0) = [0 1]x0 + [0], [1 2] [11] [a46](x0) = [0 1]x0 + [3 ], [4] [a45](x0) = x0 + [1], [1 2] [13] [a36](x0) = [0 1]x0 + [2 ], [1 2] [6] [a35](x0) = [0 1]x0 + [8], [1] [a34](x0) = x0 + [0], [1 4] [15] [a26](x0) = [0 1]x0 + [2 ], [1 2] [8] [a25](x0) = [0 1]x0 + [1], [1 3] [1] [a24](x0) = [0 1]x0 + [0], [1 1] [a23](x0) = [0 1]x0, [1 4] [15] [a16](x0) = [0 1]x0 + [2 ], [1 2] [7] [a15](x0) = [0 1]x0 + [2], [1 4] [1] [a14](x0) = [0 1]x0 + [1], [1 1] [a13](x0) = [0 1]x0, [a12](x0) = x0 orientation: [1] [1] a12(a34(x1)) = x1 + [0] >= x1 + [0] = a34(a12(x1)) [4] [4] a12(a45(x1)) = x1 + [1] >= x1 + [1] = a45(a12(x1)) [1 2] [1] [1 2] [1] a12(a56(x1)) = [0 1]x1 + [0] >= [0 1]x1 + [0] = a56(a12(x1)) [1 1] [5] [1 1] [4] a23(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a23(x1)) [1 3] [1] [1 3] [1] a23(a56(x1)) = [0 1]x1 + [0] >= [0 1]x1 + [0] = a56(a23(x1)) [1 2] [2] [1 2] [2] a34(a56(x1)) = [0 1]x1 + [0] >= [0 1]x1 + [0] = a56(a34(x1)) [1 4] [15] [1 4] [15] a26(x1) = [0 1]x1 + [2 ] >= [0 1]x1 + [2 ] = a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) = x1 >= x1 = x1 [8] a45(a45(x1)) = x1 + [2] >= x1 = x1 [1 3] [1] [1 2] [1] a24(x1) = [0 1]x1 + [0] >= [0 1]x1 + [0] = a23(a34(a23(x1))) [1 4] [28] a46(a46(x1)) = [0 1]x1 + [6 ] >= x1 = x1 [1 4] [2] a56(a56(x1)) = [0 1]x1 + [0] >= x1 = x1 [1 2] [11] [1 2] [11] a46(x1) = [0 1]x1 + [3 ] >= [0 1]x1 + [2 ] = a45(a56(a45(x1))) [1 6] [21] a45(a56(a45(a56(a45(a56(x1)))))) = [0 1]x1 + [3 ] >= x1 = x1 [2] a34(a34(x1)) = x1 + [0] >= x1 = x1 [15] a34(a45(a34(a45(a34(a45(x1)))))) = x1 + [3 ] >= x1 = x1 [1 2] a13(a13(x1)) = [0 1]x1 >= x1 = x1 [1 8] [6] a14(a14(x1)) = [0 1]x1 + [2] >= x1 = x1 [1 4] [18] a15(a15(x1)) = [0 1]x1 + [4 ] >= x1 = x1 [1 8] [38] a16(a16(x1)) = [0 1]x1 + [4 ] >= x1 = x1 [1 2] a23(a23(x1)) = [0 1]x1 >= x1 = x1 [1 6] [2] a24(a24(x1)) = [0 1]x1 + [0] >= x1 = x1 [1 4] [18] a25(a25(x1)) = [0 1]x1 + [2 ] >= x1 = x1 [1 8] [38] a26(a26(x1)) = [0 1]x1 + [4 ] >= x1 = x1 [1 4] [28] a35(a35(x1)) = [0 1]x1 + [16] >= x1 = x1 [1 4] [30] a36(a36(x1)) = [0 1]x1 + [4 ] >= x1 = x1 [1 1] [1 1] a13(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a12(x1))) [1 4] [1] [1 2] [1] a14(x1) = [0 1]x1 + [1] >= [0 1]x1 + [0] = a12(a23(a34(a23(a12(x1))))) [1 2] [7] [1 2] [7] a15(x1) = [0 1]x1 + [2] >= [0 1]x1 + [1] = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 4] [15] [1 4] [15] a16(x1) = [0 1]x1 + [2 ] >= [0 1]x1 + [2 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 2] [8] [1 2] [7] a25(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a23(a34(a45(a34(a23(x1))))) [1 2] [6] [6] a35(x1) = [0 1]x1 + [8] >= x1 + [1] = a34(a45(a34(x1))) [1 2] [13] [1 2] [13] a36(x1) = [0 1]x1 + [2 ] >= [0 1]x1 + [2 ] = a34(a45(a56(a45(a34(x1))))) [1 3] a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 [1 3] [3] a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 + [0] >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [0] [a56](x0) = x0 + [4], [1 2] [5] [a46](x0) = [0 1]x0 + [4], [1 1] [a45](x0) = [0 1]x0, [1 5] [8] [a36](x0) = [0 1]x0 + [5], [1 1] [a35](x0) = [0 1]x0, [a34](x0) = x0, [1 8] [8] [a26](x0) = [0 1]x0 + [4], [1 1] [2] [a25](x0) = [0 1]x0 + [8], [1 3] [a24](x0) = [0 1]x0, [a23](x0) = x0, [1 9] [12] [a16](x0) = [0 1]x0 + [4 ], [1 8] [8] [a15](x0) = [0 1]x0 + [8], [1 6] [0] [a14](x0) = [0 1]x0 + [2], [1 4] [0] [a13](x0) = [0 1]x0 + [2], [1 2] [a12](x0) = [0 1]x0 orientation: [1 2] [1 2] a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) [1 3] [1 3] a12(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a12(x1)) [1 2] [8] [1 2] [0] a12(a56(x1)) = [0 1]x1 + [4] >= [0 1]x1 + [4] = a56(a12(x1)) [0] [0] a23(a56(x1)) = x1 + [4] >= x1 + [4] = a56(a23(x1)) [0] [0] a34(a56(x1)) = x1 + [4] >= x1 + [4] = a56(a34(x1)) [1 1] [1 1] a23(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a23(x1)) [1 8] [8] [1 2] [4] a26(x1) = [0 1]x1 + [4] >= [0 1]x1 + [4] = a23(a34(a45(a56(a45(a34(a23(x1))))))) [1 4] a12(a12(x1)) = [0 1]x1 >= x1 = x1 [1 2] a45(a45(x1)) = [0 1]x1 >= x1 = x1 [1 3] a24(x1) = [0 1]x1 >= x1 = a23(a34(a23(x1))) [1 4] [18] a46(a46(x1)) = [0 1]x1 + [8 ] >= x1 = x1 [0] a56(a56(x1)) = x1 + [8] >= x1 = x1 [1 2] [5] [1 2] [4] a46(x1) = [0 1]x1 + [4] >= [0 1]x1 + [4] = a45(a56(a45(x1))) [1 3] [24] a45(a56(a45(a56(a45(a56(x1)))))) = [0 1]x1 + [12] >= x1 = x1 a34(a34(x1)) = x1 >= x1 = x1 [1 3] a34(a45(a34(a45(a34(a45(x1)))))) = [0 1]x1 >= x1 = x1 [1 8] [8] a13(a13(x1)) = [0 1]x1 + [4] >= x1 = x1 [1 12] [12] a14(a14(x1)) = [0 1 ]x1 + [4 ] >= x1 = x1 [1 16] [80] a15(a15(x1)) = [0 1 ]x1 + [16] >= x1 = x1 [1 18] [60] a16(a16(x1)) = [0 1 ]x1 + [8 ] >= x1 = x1 a23(a23(x1)) = x1 >= x1 = x1 [1 6] a24(a24(x1)) = [0 1]x1 >= x1 = x1 [1 2] [12] a25(a25(x1)) = [0 1]x1 + [16] >= x1 = x1 [1 16] [48] a26(a26(x1)) = [0 1 ]x1 + [8 ] >= x1 = x1 [1 2] a35(a35(x1)) = [0 1]x1 >= x1 = x1 [1 10] [41] a36(a36(x1)) = [0 1 ]x1 + [10] >= x1 = x1 [1 4] [0] [1 4] a13(x1) = [0 1]x1 + [2] >= [0 1]x1 = a12(a23(a12(x1))) [1 6] [0] [1 4] a14(x1) = [0 1]x1 + [2] >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) [1 8] [8] [1 5] a15(x1) = [0 1]x1 + [8] >= [0 1]x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 9] [12] [1 6] [12] a16(x1) = [0 1]x1 + [4 ] >= [0 1]x1 + [4 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 1] [2] [1 1] a25(x1) = [0 1]x1 + [8] >= [0 1]x1 = a23(a34(a45(a34(a23(x1))))) [1 1] [1 1] a35(x1) = [0 1]x1 >= [0 1]x1 = a34(a45(a34(x1))) [1 5] [8] [1 2] [4] a36(x1) = [0 1]x1 + [5] >= [0 1]x1 + [4] = a34(a45(a56(a45(a34(x1))))) [1 6] a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 a23(a34(a23(a34(a23(a34(x1)))))) = x1 >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) a12(a45(x1)) -> a45(a12(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [1 8] [a56](x0) = [0 1]x0, [1 8] [8] [a46](x0) = [0 1]x0 + [2], [0] [a45](x0) = x0 + [1], [1 12] [12] [a36](x0) = [0 1 ]x0 + [2 ], [1 12] [2] [a35](x0) = [0 1 ]x0 + [1], [1 2] [a34](x0) = [0 1]x0, [1 12] [13] [a26](x0) = [0 1 ]x0 + [4 ], [1 4] [2] [a25](x0) = [0 1]x0 + [1], [1 12] [2] [a24](x0) = [0 1 ]x0 + [0], [a23](x0) = x0, [1 14] [14] [a16](x0) = [0 1 ]x0 + [2 ], [1 8] [3] [a15](x0) = [0 1]x0 + [1], [1 8] [4] [a14](x0) = [0 1]x0 + [0], [1 2] [0] [a13](x0) = [0 1]x0 + [8], [1 1] [a12](x0) = [0 1]x0 orientation: [1 3] [1 3] a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) [1 1] [1] [1 1] [0] a12(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a12(x1)) [1 8] [1 8] a23(a56(x1)) = [0 1]x1 >= [0 1]x1 = a56(a23(x1)) [1 10] [1 10] a34(a56(x1)) = [0 1 ]x1 >= [0 1 ]x1 = a56(a34(x1)) [1 9] [1 9] a12(a56(x1)) = [0 1]x1 >= [0 1]x1 = a56(a12(x1)) [0] [0] a23(a45(x1)) = x1 + [1] >= x1 + [1] = a45(a23(x1)) [1 12] [13] [1 12] [12] a26(x1) = [0 1 ]x1 + [4 ] >= [0 1 ]x1 + [2 ] = a23(a34(a45(a56(a45(a34(a23(x1))))))) [1 2] a12(a12(x1)) = [0 1]x1 >= x1 = x1 [0] a45(a45(x1)) = x1 + [2] >= x1 = x1 [1 12] [2] [1 2] a24(x1) = [0 1 ]x1 + [0] >= [0 1]x1 = a23(a34(a23(x1))) [1 16] [32] a46(a46(x1)) = [0 1 ]x1 + [4 ] >= x1 = x1 [1 16] a56(a56(x1)) = [0 1 ]x1 >= x1 = x1 [1 8] [8] [1 8] [8] a46(x1) = [0 1]x1 + [2] >= [0 1]x1 + [2] = a45(a56(a45(x1))) [1 24] [24] a45(a56(a45(a56(a45(a56(x1)))))) = [0 1 ]x1 + [3 ] >= x1 = x1 [1 4] a34(a34(x1)) = [0 1]x1 >= x1 = x1 [1 6] [12] a34(a45(a34(a45(a34(a45(x1)))))) = [0 1]x1 + [3 ] >= x1 = x1 [1 4] [16] a13(a13(x1)) = [0 1]x1 + [16] >= x1 = x1 [1 16] [8] a14(a14(x1)) = [0 1 ]x1 + [0] >= x1 = x1 [1 16] [14] a15(a15(x1)) = [0 1 ]x1 + [2 ] >= x1 = x1 [1 28] [56] a16(a16(x1)) = [0 1 ]x1 + [4 ] >= x1 = x1 a23(a23(x1)) = x1 >= x1 = x1 [1 24] [4] a24(a24(x1)) = [0 1 ]x1 + [0] >= x1 = x1 [1 8] [8] a25(a25(x1)) = [0 1]x1 + [2] >= x1 = x1 [1 24] [74] a26(a26(x1)) = [0 1 ]x1 + [8 ] >= x1 = x1 [1 24] [16] a35(a35(x1)) = [0 1 ]x1 + [2 ] >= x1 = x1 [1 24] [48] a36(a36(x1)) = [0 1 ]x1 + [4 ] >= x1 = x1 [1 2] [0] [1 2] a13(x1) = [0 1]x1 + [8] >= [0 1]x1 = a12(a23(a12(x1))) [1 8] [4] [1 4] a14(x1) = [0 1]x1 + [0] >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) [1 8] [3] [1 6] [3] a15(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 14] [14] [1 14] [14] a16(x1) = [0 1 ]x1 + [2 ] >= [0 1 ]x1 + [2 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 4] [2] [1 4] [2] a25(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a23(a34(a45(a34(a23(x1))))) [1 12] [2] [1 4] [2] a35(x1) = [0 1 ]x1 + [1] >= [0 1]x1 + [1] = a34(a45(a34(x1))) [1 12] [12] [1 12] [12] a36(x1) = [0 1 ]x1 + [2 ] >= [0 1 ]x1 + [2 ] = a34(a45(a56(a45(a34(x1))))) [1 3] a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 [1 6] a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) weak: a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [1 8] [0] [a56](x0) = [0 1]x0 + [1], [1 12] [13] [a46](x0) = [0 1 ]x0 + [3 ], [1 2] [0] [a45](x0) = [0 1]x0 + [1], [1 14] [15] [a36](x0) = [0 1 ]x0 + [3 ], [1 8] [1] [a35](x0) = [0 1]x0 + [4], [1 1] [a34](x0) = [0 1]x0, [1 14] [15] [a26](x0) = [0 1 ]x0 + [3 ], [1 6] [1] [a25](x0) = [0 1]x0 + [8], [1 1] [8] [a24](x0) = [0 1]x0 + [2], [a23](x0) = x0, [1 14] [15] [a16](x0) = [0 1 ]x0 + [3 ], [1 4] [1] [a15](x0) = [0 1]x0 + [1], [1 11] [1] [a14](x0) = [0 1 ]x0 + [0], [1 9] [a13](x0) = [0 1]x0, [a12](x0) = x0 orientation: [1 1] [1 1] a12(a34(x1)) = [0 1]x1 >= [0 1]x1 = a34(a12(x1)) [1 8] [0] [1 8] [0] a23(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a23(x1)) [1 9] [1] [1 9] [0] a34(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a34(x1)) [1 2] [0] [1 2] [0] a12(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a12(x1)) [1 8] [0] [1 8] [0] a12(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a12(x1)) [1 2] [0] [1 2] [0] a23(a45(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a45(a23(x1)) [1 14] [15] [1 14] [15] a26(x1) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [3 ] = a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) = x1 >= x1 = x1 [1 4] [2] a45(a45(x1)) = [0 1]x1 + [2] >= x1 = x1 [1 1] [8] [1 1] a24(x1) = [0 1]x1 + [2] >= [0 1]x1 = a23(a34(a23(x1))) [1 24] [62] a46(a46(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 16] [8] a56(a56(x1)) = [0 1 ]x1 + [2] >= x1 = x1 [1 12] [13] [1 12] [12] a46(x1) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [3 ] = a45(a56(a45(x1))) [1 30] [66] a45(a56(a45(a56(a45(a56(x1)))))) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 2] a34(a34(x1)) = [0 1]x1 >= x1 = x1 [1 9] [12] a34(a45(a34(a45(a34(a45(x1)))))) = [0 1]x1 + [3 ] >= x1 = x1 [1 18] a13(a13(x1)) = [0 1 ]x1 >= x1 = x1 [1 22] [2] a14(a14(x1)) = [0 1 ]x1 + [0] >= x1 = x1 [1 8] [6] a15(a15(x1)) = [0 1]x1 + [2] >= x1 = x1 [1 28] [72] a16(a16(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 a23(a23(x1)) = x1 >= x1 = x1 [1 2] [18] a24(a24(x1)) = [0 1]x1 + [4 ] >= x1 = x1 [1 12] [50] a25(a25(x1)) = [0 1 ]x1 + [16] >= x1 = x1 [1 28] [72] a26(a26(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 16] [34] a35(a35(x1)) = [0 1 ]x1 + [8 ] >= x1 = x1 [1 28] [72] a36(a36(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 9] a13(x1) = [0 1]x1 >= x1 = a12(a23(a12(x1))) [1 11] [1] [1 1] a14(x1) = [0 1 ]x1 + [0] >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) [1 4] [1] [1 4] [1] a15(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 14] [15] [1 14] [15] a16(x1) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [3 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 6] [1] [1 4] [1] a25(x1) = [0 1]x1 + [8] >= [0 1]x1 + [1] = a23(a34(a45(a34(a23(x1))))) [1 8] [1] [1 4] [1] a35(x1) = [0 1]x1 + [4] >= [0 1]x1 + [1] = a34(a45(a34(x1))) [1 14] [15] [1 14] [15] a36(x1) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [3 ] = a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) = x1 >= x1 = x1 [1 3] a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) a23(a56(x1)) -> a56(a23(x1)) weak: a34(a56(x1)) -> a56(a34(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [1 5] [3] [a56](x0) = [0 1]x0 + [3], [1 9] [10] [a46](x0) = [0 1]x0 + [8 ], [1 2] [a45](x0) = [0 1]x0, [1 12] [9] [a36](x0) = [0 1 ]x0 + [3], [1 2] [0] [a35](x0) = [0 1]x0 + [1], [a34](x0) = x0, [1 13] [15] [a26](x0) = [0 1 ]x0 + [4 ], [1 6] [8] [a25](x0) = [0 1]x0 + [0], [1 7] [a24](x0) = [0 1]x0, [1 2] [a23](x0) = [0 1]x0, [1 14] [15] [a16](x0) = [0 1 ]x0 + [3 ], [1 6] [a15](x0) = [0 1]x0, [1 4] [a14](x0) = [0 1]x0, [1 8] [a13](x0) = [0 1]x0, [a12](x0) = x0 orientation: a12(a34(x1)) = x1 >= x1 = a34(a12(x1)) [1 7] [9] [1 7] [3] a23(a56(x1)) = [0 1]x1 + [3] >= [0 1]x1 + [3] = a56(a23(x1)) [1 5] [3] [1 5] [3] a34(a56(x1)) = [0 1]x1 + [3] >= [0 1]x1 + [3] = a56(a34(x1)) [1 2] [1 2] a12(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a12(x1)) [1 5] [3] [1 5] [3] a12(a56(x1)) = [0 1]x1 + [3] >= [0 1]x1 + [3] = a56(a12(x1)) [1 4] [1 4] a23(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a23(x1)) [1 13] [15] [1 13] [15] a26(x1) = [0 1 ]x1 + [4 ] >= [0 1 ]x1 + [3 ] = a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) = x1 >= x1 = x1 [1 4] a45(a45(x1)) = [0 1]x1 >= x1 = x1 [1 7] [1 4] a24(x1) = [0 1]x1 >= [0 1]x1 = a23(a34(a23(x1))) [1 18] [92] a46(a46(x1)) = [0 1 ]x1 + [16] >= x1 = x1 [1 10] [21] a56(a56(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 9] [10] [1 9] [9] a46(x1) = [0 1]x1 + [8 ] >= [0 1]x1 + [3] = a45(a56(a45(x1))) [1 21] [90] a45(a56(a45(a56(a45(a56(x1)))))) = [0 1 ]x1 + [9 ] >= x1 = x1 a34(a34(x1)) = x1 >= x1 = x1 [1 6] a34(a45(a34(a45(a34(a45(x1)))))) = [0 1]x1 >= x1 = x1 [1 16] a13(a13(x1)) = [0 1 ]x1 >= x1 = x1 [1 8] a14(a14(x1)) = [0 1]x1 >= x1 = x1 [1 12] a15(a15(x1)) = [0 1 ]x1 >= x1 = x1 [1 28] [72] a16(a16(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 4] a23(a23(x1)) = [0 1]x1 >= x1 = x1 [1 14] a24(a24(x1)) = [0 1 ]x1 >= x1 = x1 [1 12] [16] a25(a25(x1)) = [0 1 ]x1 + [0 ] >= x1 = x1 [1 26] [82] a26(a26(x1)) = [0 1 ]x1 + [8 ] >= x1 = x1 [1 4] [2] a35(a35(x1)) = [0 1]x1 + [2] >= x1 = x1 [1 24] [54] a36(a36(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 8] [1 2] a13(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a12(x1))) [1 4] [1 4] a14(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a23(a12(x1))))) [1 6] [1 6] a15(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 14] [15] [1 13] [15] a16(x1) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [3 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 6] [8] [1 6] a25(x1) = [0 1]x1 + [0] >= [0 1]x1 = a23(a34(a45(a34(a23(x1))))) [1 2] [0] [1 2] a35(x1) = [0 1]x1 + [1] >= [0 1]x1 = a34(a45(a34(x1))) [1 12] [9] [1 9] [9] a36(x1) = [0 1 ]x1 + [3] >= [0 1]x1 + [3] = a34(a45(a56(a45(a34(x1))))) [1 6] a12(a23(a12(a23(a12(a23(x1)))))) = [0 1]x1 >= x1 = x1 [1 6] a23(a34(a23(a34(a23(a34(x1)))))) = [0 1]x1 >= x1 = x1 problem: strict: a12(a34(x1)) -> a34(a12(x1)) weak: a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Matrix Interpretation Processor: dimension: 2 interpretation: [0] [a56](x0) = x0 + [1], [4] [a46](x0) = x0 + [8], [a45](x0) = x0, [1 1] [0] [a36](x0) = [0 1]x0 + [3], [0] [a35](x0) = x0 + [3], [0] [a34](x0) = x0 + [1], [8] [a26](x0) = x0 + [3], [1 6] [0] [a25](x0) = [0 1]x0 + [2], [0] [a24](x0) = x0 + [2], [a23](x0) = x0, [1 8] [14] [a16](x0) = [0 1]x0 + [3 ], [1 8] [8] [a15](x0) = [0 1]x0 + [3], [1 9] [4] [a14](x0) = [0 1]x0 + [1], [1 9] [a13](x0) = [0 1]x0, [1 4] [a12](x0) = [0 1]x0 orientation: [1 4] [4] [1 4] [0] a12(a34(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a34(a12(x1)) [0] [0] a23(a56(x1)) = x1 + [1] >= x1 + [1] = a56(a23(x1)) [0] [0] a34(a56(x1)) = x1 + [2] >= x1 + [2] = a56(a34(x1)) [1 4] [1 4] a12(a45(x1)) = [0 1]x1 >= [0 1]x1 = a45(a12(x1)) [1 4] [4] [1 4] [0] a12(a56(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a56(a12(x1)) a23(a45(x1)) = x1 >= x1 = a45(a23(x1)) [8] [0] a26(x1) = x1 + [3] >= x1 + [3] = a23(a34(a45(a56(a45(a34(a23(x1))))))) [1 8] a12(a12(x1)) = [0 1]x1 >= x1 = x1 a45(a45(x1)) = x1 >= x1 = x1 [0] [0] a24(x1) = x1 + [2] >= x1 + [1] = a23(a34(a23(x1))) [8 ] a46(a46(x1)) = x1 + [16] >= x1 = x1 [0] a56(a56(x1)) = x1 + [2] >= x1 = x1 [4] [0] a46(x1) = x1 + [8] >= x1 + [1] = a45(a56(a45(x1))) [0] a45(a56(a45(a56(a45(a56(x1)))))) = x1 + [3] >= x1 = x1 [0] a34(a34(x1)) = x1 + [2] >= x1 = x1 [0] a34(a45(a34(a45(a34(a45(x1)))))) = x1 + [3] >= x1 = x1 [1 18] a13(a13(x1)) = [0 1 ]x1 >= x1 = x1 [1 18] [17] a14(a14(x1)) = [0 1 ]x1 + [2 ] >= x1 = x1 [1 16] [40] a15(a15(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 [1 16] [52] a16(a16(x1)) = [0 1 ]x1 + [6 ] >= x1 = x1 a23(a23(x1)) = x1 >= x1 = x1 [0] a24(a24(x1)) = x1 + [4] >= x1 = x1 [1 12] [12] a25(a25(x1)) = [0 1 ]x1 + [4 ] >= x1 = x1 [16] a26(a26(x1)) = x1 + [6 ] >= x1 = x1 [0] a35(a35(x1)) = x1 + [6] >= x1 = x1 [1 2] [3] a36(a36(x1)) = [0 1]x1 + [6] >= x1 = x1 [1 9] [1 8] a13(x1) = [0 1]x1 >= [0 1]x1 = a12(a23(a12(x1))) [1 9] [4] [1 8] [4] a14(x1) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a12(a23(a34(a23(a12(x1))))) [1 8] [8] [1 8] [8] a15(x1) = [0 1]x1 + [3] >= [0 1]x1 + [2] = a12(a23(a34(a45(a34(a23(a12(x1))))))) [1 8] [14] [1 8] [12] a16(x1) = [0 1]x1 + [3 ] >= [0 1]x1 + [3 ] = a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) [1 6] [0] [0] a25(x1) = [0 1]x1 + [2] >= x1 + [2] = a23(a34(a45(a34(a23(x1))))) [0] [0] a35(x1) = x1 + [3] >= x1 + [2] = a34(a45(a34(x1))) [1 1] [0] [0] a36(x1) = [0 1]x1 + [3] >= x1 + [3] = a34(a45(a56(a45(a34(x1))))) [1 12] a12(a23(a12(a23(a12(a23(x1)))))) = [0 1 ]x1 >= x1 = x1 [0] a23(a34(a23(a34(a23(a34(x1)))))) = x1 + [3] >= x1 = x1 problem: strict: weak: a12(a34(x1)) -> a34(a12(x1)) a23(a56(x1)) -> a56(a23(x1)) a34(a56(x1)) -> a56(a34(x1)) a12(a45(x1)) -> a45(a12(x1)) a12(a56(x1)) -> a56(a12(x1)) a23(a45(x1)) -> a45(a23(x1)) a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1))))))) a12(a12(x1)) -> x1 a45(a45(x1)) -> x1 a24(x1) -> a23(a34(a23(x1))) a46(a46(x1)) -> x1 a56(a56(x1)) -> x1 a46(x1) -> a45(a56(a45(x1))) a45(a56(a45(a56(a45(a56(x1)))))) -> x1 a34(a34(x1)) -> x1 a34(a45(a34(a45(a34(a45(x1)))))) -> x1 a13(a13(x1)) -> x1 a14(a14(x1)) -> x1 a15(a15(x1)) -> x1 a16(a16(x1)) -> x1 a23(a23(x1)) -> x1 a24(a24(x1)) -> x1 a25(a25(x1)) -> x1 a26(a26(x1)) -> x1 a35(a35(x1)) -> x1 a36(a36(x1)) -> x1 a13(x1) -> a12(a23(a12(x1))) a14(x1) -> a12(a23(a34(a23(a12(x1))))) a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1))))))) a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1))))))))) a25(x1) -> a23(a34(a45(a34(a23(x1))))) a35(x1) -> a34(a45(a34(x1))) a36(x1) -> a34(a45(a56(a45(a34(x1))))) a12(a23(a12(a23(a12(a23(x1)))))) -> x1 a23(a34(a23(a34(a23(a34(x1)))))) -> x1 Qed