YES(?,O(n^2)) 233.22/67.04 YES(?,O(n^2)) 233.22/67.04 233.22/67.04 Problem: 233.22/67.04 3(1(x1)) -> 4(1(x1)) 233.22/67.04 5(9(x1)) -> 2(6(5(x1))) 233.22/67.04 3(5(x1)) -> 8(9(7(x1))) 233.22/67.04 9(x1) -> 3(2(3(x1))) 233.22/67.04 8(4(x1)) -> 6(x1) 233.22/67.04 2(6(x1)) -> 4(3(x1)) 233.22/67.04 3(8(x1)) -> 3(2(7(x1))) 233.22/67.04 9(x1) -> 5(0(2(x1))) 233.22/67.04 8(8(4(x1))) -> 1(9(x1)) 233.22/67.04 7(1(x1)) -> 6(9(x1)) 233.22/67.04 3(9(x1)) -> 9(3(x1)) 233.22/67.04 7(5(x1)) -> 1(0(x1)) 233.22/67.04 233.22/67.04 Proof: 233.22/67.04 Complexity Transformation Processor: 233.22/67.04 strict: 233.22/67.04 3(1(x1)) -> 4(1(x1)) 233.22/67.04 5(9(x1)) -> 2(6(5(x1))) 233.22/67.04 3(5(x1)) -> 8(9(7(x1))) 233.22/67.04 9(x1) -> 3(2(3(x1))) 233.22/67.04 8(4(x1)) -> 6(x1) 233.22/67.04 2(6(x1)) -> 4(3(x1)) 233.22/67.04 3(8(x1)) -> 3(2(7(x1))) 233.22/67.04 9(x1) -> 5(0(2(x1))) 233.22/67.04 8(8(4(x1))) -> 1(9(x1)) 233.22/67.04 7(1(x1)) -> 6(9(x1)) 233.22/67.04 3(9(x1)) -> 9(3(x1)) 233.22/67.04 7(5(x1)) -> 1(0(x1)) 233.22/67.04 weak: 233.22/67.04 233.22/67.04 Matrix Interpretation Processor: dim=1 233.22/67.04 233.22/67.04 max_matrix: 233.22/67.04 1 233.22/67.04 interpretation: 233.22/67.04 [0](x0) = x0 + 2, 233.22/67.04 233.22/67.04 [8](x0) = x0 + 3, 233.22/67.04 233.22/67.04 [7](x0) = x0 + 12, 233.22/67.04 233.22/67.04 [2](x0) = x0 + 6, 233.22/67.04 233.22/67.04 [6](x0) = x0 + 5, 233.22/67.04 233.22/67.04 [5](x0) = x0 + 3, 233.22/67.04 233.22/67.04 [9](x0) = x0 + 8, 233.22/67.04 233.22/67.04 [4](x0) = x0 + 13, 233.22/67.04 233.22/67.04 [3](x0) = x0 + 12, 233.22/67.04 233.22/67.04 [1](x0) = x0 + 4 233.22/67.04 orientation: 233.22/67.04 3(1(x1)) = x1 + 16 >= x1 + 17 = 4(1(x1)) 233.22/67.04 233.22/67.04 5(9(x1)) = x1 + 11 >= x1 + 14 = 2(6(5(x1))) 233.22/67.04 233.22/67.04 3(5(x1)) = x1 + 15 >= x1 + 23 = 8(9(7(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 + 8 >= x1 + 30 = 3(2(3(x1))) 233.22/67.04 233.22/67.04 8(4(x1)) = x1 + 16 >= x1 + 5 = 6(x1) 233.22/67.04 233.22/67.04 2(6(x1)) = x1 + 11 >= x1 + 25 = 4(3(x1)) 233.22/67.04 233.22/67.04 3(8(x1)) = x1 + 15 >= x1 + 30 = 3(2(7(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 + 8 >= x1 + 11 = 5(0(2(x1))) 233.22/67.04 233.22/67.04 8(8(4(x1))) = x1 + 19 >= x1 + 12 = 1(9(x1)) 233.22/67.04 233.22/67.04 7(1(x1)) = x1 + 16 >= x1 + 13 = 6(9(x1)) 233.22/67.04 233.22/67.04 3(9(x1)) = x1 + 20 >= x1 + 20 = 9(3(x1)) 233.22/67.04 233.22/67.04 7(5(x1)) = x1 + 15 >= x1 + 6 = 1(0(x1)) 233.22/67.04 problem: 233.22/67.04 strict: 233.22/67.04 3(1(x1)) -> 4(1(x1)) 233.22/67.04 5(9(x1)) -> 2(6(5(x1))) 233.22/67.04 3(5(x1)) -> 8(9(7(x1))) 233.22/67.04 9(x1) -> 3(2(3(x1))) 233.22/67.04 2(6(x1)) -> 4(3(x1)) 233.22/67.04 3(8(x1)) -> 3(2(7(x1))) 233.22/67.04 9(x1) -> 5(0(2(x1))) 233.22/67.04 3(9(x1)) -> 9(3(x1)) 233.22/67.04 weak: 233.22/67.04 8(4(x1)) -> 6(x1) 233.22/67.04 8(8(4(x1))) -> 1(9(x1)) 233.22/67.04 7(1(x1)) -> 6(9(x1)) 233.22/67.04 7(5(x1)) -> 1(0(x1)) 233.22/67.04 Matrix Interpretation Processor: dim=1 233.22/67.04 233.22/67.04 max_matrix: 233.22/67.04 1 233.22/67.04 interpretation: 233.22/67.04 [0](x0) = x0, 233.22/67.04 233.22/67.04 [8](x0) = x0 + 11, 233.22/67.04 233.22/67.04 [7](x0) = x0 + 9, 233.22/67.04 233.22/67.04 [2](x0) = x0, 233.22/67.04 233.22/67.04 [6](x0) = x0 + 4, 233.22/67.04 233.22/67.04 [5](x0) = x0, 233.22/67.04 233.22/67.04 [9](x0) = x0, 233.22/67.04 233.22/67.04 [4](x0) = x0 + 1, 233.22/67.04 233.22/67.04 [3](x0) = x0, 233.22/67.04 233.22/67.04 [1](x0) = x0 233.22/67.04 orientation: 233.22/67.04 3(1(x1)) = x1 >= x1 + 1 = 4(1(x1)) 233.22/67.04 233.22/67.04 5(9(x1)) = x1 >= x1 + 4 = 2(6(5(x1))) 233.22/67.04 233.22/67.04 3(5(x1)) = x1 >= x1 + 20 = 8(9(7(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 >= x1 = 3(2(3(x1))) 233.22/67.04 233.22/67.04 2(6(x1)) = x1 + 4 >= x1 + 1 = 4(3(x1)) 233.22/67.04 233.22/67.04 3(8(x1)) = x1 + 11 >= x1 + 9 = 3(2(7(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 >= x1 = 5(0(2(x1))) 233.22/67.04 233.22/67.04 3(9(x1)) = x1 >= x1 = 9(3(x1)) 233.22/67.04 233.22/67.04 8(4(x1)) = x1 + 12 >= x1 + 4 = 6(x1) 233.22/67.04 233.22/67.04 8(8(4(x1))) = x1 + 23 >= x1 = 1(9(x1)) 233.22/67.04 233.22/67.04 7(1(x1)) = x1 + 9 >= x1 + 4 = 6(9(x1)) 233.22/67.04 233.22/67.04 7(5(x1)) = x1 + 9 >= x1 = 1(0(x1)) 233.22/67.04 problem: 233.22/67.04 strict: 233.22/67.04 3(1(x1)) -> 4(1(x1)) 233.22/67.04 5(9(x1)) -> 2(6(5(x1))) 233.22/67.04 3(5(x1)) -> 8(9(7(x1))) 233.22/67.04 9(x1) -> 3(2(3(x1))) 233.22/67.04 9(x1) -> 5(0(2(x1))) 233.22/67.04 3(9(x1)) -> 9(3(x1)) 233.22/67.04 weak: 233.22/67.04 2(6(x1)) -> 4(3(x1)) 233.22/67.04 3(8(x1)) -> 3(2(7(x1))) 233.22/67.04 8(4(x1)) -> 6(x1) 233.22/67.04 8(8(4(x1))) -> 1(9(x1)) 233.22/67.04 7(1(x1)) -> 6(9(x1)) 233.22/67.04 7(5(x1)) -> 1(0(x1)) 233.22/67.04 Matrix Interpretation Processor: dim=1 233.22/67.04 233.22/67.04 max_matrix: 233.22/67.04 1 233.22/67.04 interpretation: 233.22/67.04 [0](x0) = x0, 233.22/67.04 233.22/67.04 [8](x0) = x0 + 8, 233.22/67.04 233.22/67.04 [7](x0) = x0 + 2, 233.22/67.04 233.22/67.04 [2](x0) = x0 + 6, 233.22/67.04 233.22/67.04 [6](x0) = x0 + 10, 233.22/67.04 233.22/67.04 [5](x0) = x0 + 7, 233.22/67.04 233.22/67.04 [9](x0) = x0, 233.22/67.04 233.22/67.04 [4](x0) = x0 + 8, 233.22/67.04 233.22/67.04 [3](x0) = x0 + 8, 233.22/67.04 233.22/67.04 [1](x0) = x0 + 9 233.22/67.04 orientation: 233.22/67.04 3(1(x1)) = x1 + 17 >= x1 + 17 = 4(1(x1)) 233.22/67.04 233.22/67.04 5(9(x1)) = x1 + 7 >= x1 + 23 = 2(6(5(x1))) 233.22/67.04 233.22/67.04 3(5(x1)) = x1 + 15 >= x1 + 10 = 8(9(7(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 >= x1 + 22 = 3(2(3(x1))) 233.22/67.04 233.22/67.04 9(x1) = x1 >= x1 + 13 = 5(0(2(x1))) 233.22/67.04 233.22/67.04 3(9(x1)) = x1 + 8 >= x1 + 8 = 9(3(x1)) 233.22/67.04 233.22/67.04 2(6(x1)) = x1 + 16 >= x1 + 16 = 4(3(x1)) 233.22/67.04 233.22/67.04 3(8(x1)) = x1 + 16 >= x1 + 16 = 3(2(7(x1))) 233.22/67.05 233.22/67.05 8(4(x1)) = x1 + 16 >= x1 + 10 = 6(x1) 233.22/67.05 233.22/67.05 8(8(4(x1))) = x1 + 24 >= x1 + 9 = 1(9(x1)) 233.22/67.05 233.22/67.05 7(1(x1)) = x1 + 11 >= x1 + 10 = 6(9(x1)) 233.22/67.05 233.22/67.05 7(5(x1)) = x1 + 9 >= x1 + 9 = 1(0(x1)) 233.22/67.05 problem: 233.22/67.05 strict: 233.22/67.05 3(1(x1)) -> 4(1(x1)) 233.22/67.05 5(9(x1)) -> 2(6(5(x1))) 233.22/67.05 9(x1) -> 3(2(3(x1))) 233.22/67.05 9(x1) -> 5(0(2(x1))) 233.22/67.05 3(9(x1)) -> 9(3(x1)) 233.22/67.05 weak: 233.22/67.05 3(5(x1)) -> 8(9(7(x1))) 233.22/67.05 2(6(x1)) -> 4(3(x1)) 233.22/67.05 3(8(x1)) -> 3(2(7(x1))) 233.22/67.05 8(4(x1)) -> 6(x1) 233.22/67.05 8(8(4(x1))) -> 1(9(x1)) 233.22/67.05 7(1(x1)) -> 6(9(x1)) 233.22/67.05 7(5(x1)) -> 1(0(x1)) 233.22/67.05 Matrix Interpretation Processor: dim=1 233.22/67.05 233.22/67.05 max_matrix: 233.22/67.05 1 233.22/67.05 interpretation: 233.22/67.05 [0](x0) = x0 + 26, 233.22/67.05 233.22/67.05 [8](x0) = x0 + 32, 233.22/67.05 233.22/67.05 [7](x0) = x0 + 28, 233.22/67.05 233.22/67.05 [2](x0) = x0 + 1, 233.22/67.05 233.22/67.05 [6](x0) = x0 + 32, 233.22/67.05 233.22/67.05 [5](x0) = x0 + 64, 233.22/67.05 233.22/67.05 [9](x0) = x0 + 4, 233.22/67.05 233.22/67.05 [4](x0) = x0, 233.22/67.05 233.22/67.05 [3](x0) = x0, 233.22/67.05 233.22/67.05 [1](x0) = x0 + 8 233.22/67.05 orientation: 233.22/67.05 3(1(x1)) = x1 + 8 >= x1 + 8 = 4(1(x1)) 233.22/67.05 233.22/67.05 5(9(x1)) = x1 + 68 >= x1 + 97 = 2(6(5(x1))) 233.22/67.05 233.22/67.05 9(x1) = x1 + 4 >= x1 + 1 = 3(2(3(x1))) 233.22/67.05 233.22/67.05 9(x1) = x1 + 4 >= x1 + 91 = 5(0(2(x1))) 233.22/67.05 233.22/67.05 3(9(x1)) = x1 + 4 >= x1 + 4 = 9(3(x1)) 233.22/67.05 233.22/67.05 3(5(x1)) = x1 + 64 >= x1 + 64 = 8(9(7(x1))) 233.22/67.05 233.22/67.05 2(6(x1)) = x1 + 33 >= x1 = 4(3(x1)) 233.22/67.05 233.22/67.05 3(8(x1)) = x1 + 32 >= x1 + 29 = 3(2(7(x1))) 233.22/67.05 233.22/67.05 8(4(x1)) = x1 + 32 >= x1 + 32 = 6(x1) 233.22/67.05 233.22/67.05 8(8(4(x1))) = x1 + 64 >= x1 + 12 = 1(9(x1)) 233.22/67.05 233.22/67.05 7(1(x1)) = x1 + 36 >= x1 + 36 = 6(9(x1)) 233.22/67.05 233.22/67.05 7(5(x1)) = x1 + 92 >= x1 + 34 = 1(0(x1)) 233.22/67.05 problem: 233.22/67.05 strict: 233.22/67.05 3(1(x1)) -> 4(1(x1)) 233.22/67.05 5(9(x1)) -> 2(6(5(x1))) 233.22/67.05 9(x1) -> 5(0(2(x1))) 233.22/67.05 3(9(x1)) -> 9(3(x1)) 233.22/67.05 weak: 233.22/67.05 9(x1) -> 3(2(3(x1))) 233.22/67.05 3(5(x1)) -> 8(9(7(x1))) 233.22/67.05 2(6(x1)) -> 4(3(x1)) 233.22/67.05 3(8(x1)) -> 3(2(7(x1))) 233.22/67.05 8(4(x1)) -> 6(x1) 233.22/67.05 8(8(4(x1))) -> 1(9(x1)) 233.22/67.05 7(1(x1)) -> 6(9(x1)) 233.22/67.05 7(5(x1)) -> 1(0(x1)) 233.22/67.05 Matrix Interpretation Processor: dim=1 233.22/67.05 233.22/67.05 max_matrix: 233.22/67.05 1 233.22/67.05 interpretation: 233.22/67.05 [0](x0) = x0 + 1, 233.22/67.05 233.22/67.05 [8](x0) = x0 + 1, 233.22/67.05 233.22/67.05 [7](x0) = x0, 233.22/67.05 233.22/67.05 [2](x0) = x0, 233.22/67.05 233.22/67.05 [6](x0) = x0, 233.22/67.05 233.22/67.05 [5](x0) = x0 + 2, 233.22/67.05 233.22/67.05 [9](x0) = x0 + 1, 233.22/67.05 233.22/67.05 [4](x0) = x0, 233.22/67.05 233.22/67.05 [3](x0) = x0, 233.22/67.05 233.22/67.05 [1](x0) = x0 + 1 233.22/67.05 orientation: 233.22/67.05 3(1(x1)) = x1 + 1 >= x1 + 1 = 4(1(x1)) 233.22/67.05 233.22/67.05 5(9(x1)) = x1 + 3 >= x1 + 2 = 2(6(5(x1))) 233.22/67.05 233.22/67.05 9(x1) = x1 + 1 >= x1 + 3 = 5(0(2(x1))) 233.22/67.05 233.22/67.05 3(9(x1)) = x1 + 1 >= x1 + 1 = 9(3(x1)) 233.22/67.05 233.22/67.05 9(x1) = x1 + 1 >= x1 = 3(2(3(x1))) 233.22/67.05 233.22/67.05 3(5(x1)) = x1 + 2 >= x1 + 2 = 8(9(7(x1))) 233.22/67.05 233.22/67.05 2(6(x1)) = x1 >= x1 = 4(3(x1)) 233.22/67.05 233.22/67.05 3(8(x1)) = x1 + 1 >= x1 = 3(2(7(x1))) 233.22/67.05 233.22/67.05 8(4(x1)) = x1 + 1 >= x1 = 6(x1) 233.22/67.05 233.22/67.05 8(8(4(x1))) = x1 + 2 >= x1 + 2 = 1(9(x1)) 233.22/67.05 233.22/67.05 7(1(x1)) = x1 + 1 >= x1 + 1 = 6(9(x1)) 233.22/67.05 233.22/67.05 7(5(x1)) = x1 + 2 >= x1 + 2 = 1(0(x1)) 233.22/67.05 problem: 233.22/67.05 strict: 233.22/67.05 3(1(x1)) -> 4(1(x1)) 233.22/67.05 9(x1) -> 5(0(2(x1))) 233.22/67.05 3(9(x1)) -> 9(3(x1)) 233.22/67.05 weak: 233.22/67.05 5(9(x1)) -> 2(6(5(x1))) 233.22/67.05 9(x1) -> 3(2(3(x1))) 233.22/67.05 3(5(x1)) -> 8(9(7(x1))) 233.22/67.05 2(6(x1)) -> 4(3(x1)) 233.22/67.05 3(8(x1)) -> 3(2(7(x1))) 233.22/67.05 8(4(x1)) -> 6(x1) 233.22/67.05 8(8(4(x1))) -> 1(9(x1)) 233.22/67.05 7(1(x1)) -> 6(9(x1)) 233.22/67.05 7(5(x1)) -> 1(0(x1)) 233.22/67.05 Matrix Interpretation Processor: dim=1 233.22/67.05 233.22/67.05 max_matrix: 233.22/67.05 1 233.22/67.05 interpretation: 233.22/67.05 [0](x0) = x0 + 2, 233.22/67.05 233.22/67.05 [8](x0) = x0 + 8, 233.22/67.05 233.22/67.05 [7](x0) = x0, 233.22/67.05 233.22/67.05 [2](x0) = x0, 233.22/67.05 233.22/67.05 [6](x0) = x0 + 3, 233.22/67.05 233.22/67.05 [5](x0) = x0 + 10, 233.22/67.05 233.22/67.05 [9](x0) = x0 + 4, 233.22/67.05 233.22/67.05 [4](x0) = x0, 233.22/67.05 233.22/67.05 [3](x0) = x0 + 2, 233.22/67.05 233.22/67.05 [1](x0) = x0 + 8 233.22/67.05 orientation: 233.22/67.05 3(1(x1)) = x1 + 10 >= x1 + 8 = 4(1(x1)) 233.22/67.06 233.22/67.06 9(x1) = x1 + 4 >= x1 + 12 = 5(0(2(x1))) 233.22/67.06 233.22/67.06 3(9(x1)) = x1 + 6 >= x1 + 6 = 9(3(x1)) 233.22/67.06 233.22/67.06 5(9(x1)) = x1 + 14 >= x1 + 13 = 2(6(5(x1))) 233.22/67.06 233.22/67.06 9(x1) = x1 + 4 >= x1 + 4 = 3(2(3(x1))) 233.22/67.06 233.22/67.06 3(5(x1)) = x1 + 12 >= x1 + 12 = 8(9(7(x1))) 233.22/67.06 233.22/67.06 2(6(x1)) = x1 + 3 >= x1 + 2 = 4(3(x1)) 233.22/67.06 233.22/67.06 3(8(x1)) = x1 + 10 >= x1 + 2 = 3(2(7(x1))) 233.22/67.06 233.22/67.06 8(4(x1)) = x1 + 8 >= x1 + 3 = 6(x1) 233.22/67.06 233.22/67.06 8(8(4(x1))) = x1 + 16 >= x1 + 12 = 1(9(x1)) 233.22/67.06 233.22/67.06 7(1(x1)) = x1 + 8 >= x1 + 7 = 6(9(x1)) 233.22/67.06 233.22/67.06 7(5(x1)) = x1 + 10 >= x1 + 10 = 1(0(x1)) 233.22/67.06 problem: 233.22/67.06 strict: 233.22/67.06 9(x1) -> 5(0(2(x1))) 233.22/67.06 3(9(x1)) -> 9(3(x1)) 233.22/67.06 weak: 233.22/67.06 3(1(x1)) -> 4(1(x1)) 233.22/67.06 5(9(x1)) -> 2(6(5(x1))) 233.22/67.06 9(x1) -> 3(2(3(x1))) 233.22/67.06 3(5(x1)) -> 8(9(7(x1))) 233.22/67.06 2(6(x1)) -> 4(3(x1)) 233.22/67.06 3(8(x1)) -> 3(2(7(x1))) 233.22/67.06 8(4(x1)) -> 6(x1) 233.22/67.06 8(8(4(x1))) -> 1(9(x1)) 233.22/67.06 7(1(x1)) -> 6(9(x1)) 233.22/67.06 7(5(x1)) -> 1(0(x1)) 233.22/67.06 Splitting Processor: 233.22/67.06 strict: 233.22/67.06 3(9(x1)) -> 9(3(x1)) 233.22/67.06 weak: 233.22/67.06 3(1(x1)) -> 4(1(x1)) 233.22/67.06 5(9(x1)) -> 2(6(5(x1))) 233.22/67.06 9(x1) -> 3(2(3(x1))) 233.22/67.06 3(5(x1)) -> 8(9(7(x1))) 233.22/67.06 2(6(x1)) -> 4(3(x1)) 233.22/67.06 3(8(x1)) -> 3(2(7(x1))) 233.22/67.06 8(4(x1)) -> 6(x1) 233.22/67.06 8(8(4(x1))) -> 1(9(x1)) 233.22/67.06 7(1(x1)) -> 6(9(x1)) 233.22/67.06 7(5(x1)) -> 1(0(x1)) 233.22/67.06 9(x1) -> 5(0(2(x1))) 233.22/67.06 Matrix Interpretation Processor: dim=3 233.22/67.06 233.22/67.06 max_matrix: 233.22/67.06 [1 3 3] 233.22/67.06 [0 0 2] 233.22/67.06 [0 0 0] 233.22/67.06 interpretation: 233.22/67.06 [1 0 0] [0] 233.22/67.06 [0](x0) = [0 0 0]x0 + [1] 233.22/67.06 [0 0 0] [0], 233.22/67.06 233.22/67.06 [1 3 0] [0] 233.22/67.06 [8](x0) = [0 0 0]x0 + [2] 233.22/67.06 [0 0 0] [1], 233.22/67.06 233.22/67.06 [1 0 0] [2] 233.22/67.06 [7](x0) = [0 0 0]x0 + [2] 233.22/67.06 [0 0 0] [0], 233.22/67.06 233.22/67.06 [1 0 0] [0] 233.22/67.06 [2](x0) = [0 0 0]x0 + [1] 233.22/67.06 [0 0 0] [0], 233.22/67.06 233.22/67.06 [1 0 3] [0] 233.22/67.06 [6](x0) = [0 0 0]x0 + [2] 233.22/67.06 [0 0 0] [0], 233.22/67.06 233.22/67.06 [1 0 2] [0] 233.22/67.06 [5](x0) = [0 0 1]x0 + [0] 233.22/67.06 [0 0 0] [1], 233.22/67.06 233.22/67.06 [1 0 3] [1] 233.22/67.06 [9](x0) = [0 0 0]x0 + [0] 233.22/67.06 [0 0 0] [1], 233.22/67.06 233.22/67.06 [1 0 0] 233.22/67.06 [4](x0) = [0 0 1]x0 233.22/67.06 [0 0 0] , 233.22/67.06 233.22/67.06 [1 0 3] [0] 233.22/67.06 [3](x0) = [0 0 2]x0 + [0] 233.22/67.06 [0 0 0] [1], 233.22/67.06 233.22/67.06 [1 0 3] [2] 233.22/67.06 [1](x0) = [0 0 2]x0 + [0] 233.22/67.06 [0 0 0] [0] 233.22/67.06 orientation: 233.22/67.06 [1 0 3] [1] [1 0 0] [0] 233.22/67.06 9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 5(0(2(x1))) 233.22/67.06 [0 0 0] [1] [0 0 0] [1] 233.22/67.06 233.22/67.06 [1 0 3] [4] [1 0 3] [4] 233.22/67.06 3(9(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 9(3(x1)) 233.22/67.06 [0 0 0] [1] [0 0 0] [1] 233.22/67.06 233.22/67.06 [1 0 3] [2] [1 0 3] [2] 233.22/67.06 3(1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 4(1(x1)) 233.22/67.06 [0 0 0] [1] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 0 3] [3] [1 0 2] [3] 233.22/67.06 5(9(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 2(6(5(x1))) 233.22/67.06 [0 0 0] [1] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 0 3] [1] [1 0 3] [0] 233.22/67.06 9(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 3(2(3(x1))) 233.22/67.06 [0 0 0] [1] [0 0 0] [1] 233.22/67.06 233.22/67.06 [1 0 2] [3] [1 0 0] [3] 233.22/67.06 3(5(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 8(9(7(x1))) 233.22/67.06 [0 0 0] [1] [0 0 0] [1] 233.22/67.06 233.22/67.06 [1 0 3] [0] [1 0 3] [0] 233.22/67.06 2(6(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 4(3(x1)) 233.22/67.06 [0 0 0] [0] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 3 0] [3] [1 0 0] [2] 233.22/67.06 3(8(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 3(2(7(x1))) 233.22/67.06 [0 0 0] [1] [0 0 0] [1] 233.22/67.06 233.22/67.06 [1 0 3] [0] [1 0 3] [0] 233.22/67.06 8(4(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 6(x1) 233.22/67.06 [0 0 0] [1] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 0 3] [6] [1 0 3] [6] 233.22/67.06 8(8(4(x1))) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 1(9(x1)) 233.22/67.06 [0 0 0] [1] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 0 3] [4] [1 0 3] [4] 233.22/67.06 7(1(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [2] = 6(9(x1)) 233.22/67.06 [0 0 0] [0] [0 0 0] [0] 233.22/67.06 233.22/67.06 [1 0 2] [2] [1 0 0] [2] 233.22/67.06 7(5(x1)) = [0 0 0]x1 + [2] >= [0 0 0]x1 + [0] = 1(0(x1)) 233.22/67.06 [0 0 0] [0] [0 0 0] [0] 233.22/67.06 problem: 233.22/67.06 strict: 233.22/67.06 233.22/67.06 weak: 233.22/67.06 9(x1) -> 5(0(2(x1))) 233.22/67.06 3(9(x1)) -> 9(3(x1)) 233.22/67.06 3(1(x1)) -> 4(1(x1)) 233.22/67.06 5(9(x1)) -> 2(6(5(x1))) 233.22/67.06 9(x1) -> 3(2(3(x1))) 233.22/67.06 3(5(x1)) -> 8(9(7(x1))) 233.22/67.06 2(6(x1)) -> 4(3(x1)) 233.22/67.06 3(8(x1)) -> 3(2(7(x1))) 233.22/67.06 8(4(x1)) -> 6(x1) 233.22/67.06 8(8(4(x1))) -> 1(9(x1)) 233.22/67.06 7(1(x1)) -> 6(9(x1)) 233.22/67.06 7(5(x1)) -> 1(0(x1)) 233.22/67.06 Qed 233.22/67.06 233.22/67.06 strict: 233.22/67.06 9(x1) -> 5(0(2(x1))) 233.22/67.06 weak: 233.22/67.06 3(9(x1)) -> 9(3(x1)) 233.22/67.06 3(1(x1)) -> 4(1(x1)) 233.22/67.06 5(9(x1)) -> 2(6(5(x1))) 233.22/67.06 9(x1) -> 3(2(3(x1))) 233.22/67.06 3(5(x1)) -> 8(9(7(x1))) 233.22/67.06 2(6(x1)) -> 4(3(x1)) 233.22/67.06 3(8(x1)) -> 3(2(7(x1))) 233.22/67.06 8(4(x1)) -> 6(x1) 233.22/67.06 8(8(4(x1))) -> 1(9(x1)) 233.22/67.06 7(1(x1)) -> 6(9(x1)) 233.22/67.06 7(5(x1)) -> 1(0(x1)) 233.22/67.06 Matrix Interpretation Processor: dim=5 233.22/67.06 233.22/67.06 max_matrix: 233.22/67.06 [1 1 2 0 0] 233.22/67.06 [0 0 1 0 0] 233.22/67.06 [0 0 1 3 0] 233.22/67.06 [0 0 0 0 1] 233.22/67.06 [0 0 0 0 0] 233.22/67.06 interpretation: 233.22/67.06 [1 0 0 0 0] [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [0](x0) = [0 0 0 0 0]x0 + [0] 233.22/67.06 [0 0 0 0 1] [1] 233.22/67.06 [0 0 0 0 0] [0], 233.22/67.06 233.22/67.06 [1 0 1 0 0] [0] 233.22/67.06 [0 0 0 0 0] [1] 233.22/67.06 [8](x0) = [0 0 1 3 0]x0 + [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [0 0 0 0 0] [2], 233.22/67.06 233.22/67.06 [1 0 1 0 0] [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [7](x0) = [0 0 1 0 0]x0 + [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [0 0 0 0 0] [3], 233.22/67.06 233.22/67.06 [1 0 0 0 0] 233.22/67.06 [0 0 0 0 0] 233.22/67.06 [2](x0) = [0 0 1 0 0]x0 233.22/67.06 [0 0 0 0 1] 233.22/67.06 [0 0 0 0 0] , 233.22/67.06 233.22/67.06 [1 1 1 0 0] [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [6](x0) = [0 0 1 0 0]x0 + [0] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [0 0 0 0 0] [2], 233.22/67.06 233.22/67.06 [1 1 2 0 0] [0] 233.22/67.06 [0 0 0 0 0] [1] 233.22/67.06 [5](x0) = [0 0 1 0 0]x0 + [1] 233.22/67.06 [0 0 0 0 1] [0] 233.22/67.06 [0 0 0 0 0] [0], 233.22/67.06 233.22/67.06 [1 1 0 0 0] [0] 233.22/67.06 [0 0 1 0 0] [1] 233.22/67.06 [9](x0) = [0 0 1 0 0]x0 + [1] 233.22/67.06 [0 0 0 0 0] [0] 233.22/67.06 [0 0 0 0 0] [2], 233.22/67.07 233.22/67.07 [1 1 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [0] 233.22/67.07 [4](x0) = [0 0 1 0 0]x0 + [0] 233.22/67.07 [0 0 0 0 0] [1] 233.22/67.07 [0 0 0 0 0] [0], 233.22/67.07 233.22/67.07 [1 1 0 0 0] [0] 233.22/67.07 [0 0 1 0 0] [0] 233.22/67.07 [3](x0) = [0 0 1 0 0]x0 + [0] 233.22/67.07 [0 0 0 0 1] [0] 233.22/67.07 [0 0 0 0 0] [2], 233.22/67.07 233.22/67.07 [1 1 1 0 0] [1] 233.22/67.07 [0 0 0 0 0] [0] 233.22/67.07 [1](x0) = [0 0 1 0 0]x0 + [1] 233.22/67.07 [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [1] 233.22/67.07 orientation: 233.22/67.07 [1 1 1 0 0] [1] [1 1 1 0 0] [0] 233.22/67.07 [0 0 1 0 0] [1] [0 0 1 0 0] [1] 233.22/67.07 3(9(x1)) = [0 0 1 0 0]x1 + [1] >= [0 0 1 0 0]x1 + [1] = 9(3(x1)) 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 233.22/67.07 [1 1 1 0 0] [1] [1 1 1 0 0] [1] 233.22/67.07 [0 0 1 0 0] [1] [0 0 0 0 0] [0] 233.22/67.07 3(1(x1)) = [0 0 1 0 0]x1 + [1] >= [0 0 1 0 0]x1 + [1] = 4(1(x1)) 233.22/67.07 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [0] 233.22/67.07 233.22/67.07 [1 1 3 0 0] [3] [1 1 3 0 0] [2] 233.22/67.07 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 233.22/67.07 5(9(x1)) = [0 0 1 0 0]x1 + [2] >= [0 0 1 0 0]x1 + [1] = 2(6(5(x1))) 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 233.22/67.07 [1 1 0 0 0] [0] [1 1 0 0 0] [0] 233.22/67.07 [0 0 1 0 0] [1] [0 0 1 0 0] [0] 233.22/67.07 9(x1) = [0 0 1 0 0]x1 + [1] >= [0 0 1 0 0]x1 + [0] = 3(2(3(x1))) 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 233.22/67.07 [1 1 2 0 0] [1] [1 0 2 0 0] [1] 233.22/67.07 [0 0 1 0 0] [1] [0 0 0 0 0] [1] 233.22/67.07 3(5(x1)) = [0 0 1 0 0]x1 + [1] >= [0 0 1 0 0]x1 + [1] = 8(9(7(x1))) 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 233.22/67.07 [1 1 1 0 0] [0] [1 1 1 0 0] [0] 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 2(6(x1)) = [0 0 1 0 0]x1 + [0] >= [0 0 1 0 0]x1 + [0] = 4(3(x1)) 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [1] 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 233.22/67.07 [1 0 1 0 0] [1] [1 0 1 0 0] [0] 233.22/67.07 [0 0 1 3 0] [0] [0 0 1 0 0] [0] 233.22/67.07 3(8(x1)) = [0 0 1 3 0]x1 + [0] >= [0 0 1 0 0]x1 + [0] = 3(2(7(x1))) 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 233.22/67.07 [1 1 1 0 0] [0] [1 1 1 0 0] [0] 233.22/67.07 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 233.22/67.07 8(4(x1)) = [0 0 1 0 0]x1 + [3] >= [0 0 1 0 0]x1 + [0] = 6(x1) 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.07 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 233.22/67.07 233.22/67.07 [1 1 2 0 0] [3] [1 1 2 0 0] [3] 233.22/67.07 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 233.22/67.07 8(8(4(x1))) = [0 0 1 0 0]x1 + [3] >= [0 0 1 0 0]x1 + [2] = 1(9(x1)) 233.22/67.07 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 [0 0 0 0 0] [2] [0 0 0 0 0] [1] 233.22/67.08 233.22/67.08 [1 1 2 0 0] [2] [1 1 2 0 0] [2] 233.22/67.08 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 7(1(x1)) = [0 0 1 0 0]x1 + [1] >= [0 0 1 0 0]x1 + [1] = 6(9(x1)) 233.22/67.08 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 [0 0 0 0 0] [3] [0 0 0 0 0] [2] 233.22/67.08 233.22/67.08 [1 1 3 0 0] [1] [1 0 0 0 0] [1] 233.22/67.08 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 7(5(x1)) = [0 0 1 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1(0(x1)) 233.22/67.08 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 [0 0 0 0 0] [3] [0 0 0 0 0] [1] 233.22/67.08 233.22/67.08 [1 1 0 0 0] [0] [1 0 0 0 0] [0] 233.22/67.08 [0 0 1 0 0] [1] [0 0 0 0 0] [1] 233.22/67.08 9(x1) = [0 0 1 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 5(0(2(x1))) 233.22/67.08 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 233.22/67.08 [0 0 0 0 0] [2] [0 0 0 0 0] [0] 233.22/67.08 problem: 233.22/67.08 strict: 233.22/67.08 233.22/67.08 weak: 233.22/67.08 3(9(x1)) -> 9(3(x1)) 233.22/67.08 3(1(x1)) -> 4(1(x1)) 233.22/67.08 5(9(x1)) -> 2(6(5(x1))) 233.22/67.08 9(x1) -> 3(2(3(x1))) 233.22/67.08 3(5(x1)) -> 8(9(7(x1))) 233.22/67.08 2(6(x1)) -> 4(3(x1)) 233.22/67.08 3(8(x1)) -> 3(2(7(x1))) 233.22/67.08 8(4(x1)) -> 6(x1) 233.22/67.08 8(8(4(x1))) -> 1(9(x1)) 233.22/67.08 7(1(x1)) -> 6(9(x1)) 233.22/67.08 7(5(x1)) -> 1(0(x1)) 233.22/67.08 9(x1) -> 5(0(2(x1))) 233.22/67.08 Qed 233.22/67.08 EOF