YES(?,O(n^1)) 82.93/22.01 YES(?,O(n^1)) 82.93/22.01 82.93/22.01 Problem: 82.93/22.01 2(7(x1)) -> 1(8(x1)) 82.93/22.01 2(8(1(x1))) -> 8(x1) 82.93/22.01 2(8(x1)) -> 4(x1) 82.93/22.01 5(9(x1)) -> 0(x1) 82.93/22.01 4(x1) -> 5(2(3(x1))) 82.93/22.01 5(3(x1)) -> 6(0(x1)) 82.93/22.01 2(8(x1)) -> 7(x1) 82.93/22.01 4(7(x1)) -> 1(3(x1)) 82.93/22.01 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.01 9(7(x1)) -> 7(5(x1)) 82.93/22.01 7(2(x1)) -> 4(x1) 82.93/22.01 7(0(x1)) -> 9(3(x1)) 82.93/22.01 6(9(x1)) -> 9(x1) 82.93/22.01 9(5(9(x1))) -> 5(7(x1)) 82.93/22.01 4(x1) -> 9(6(6(x1))) 82.93/22.01 9(x1) -> 6(7(x1)) 82.93/22.01 6(2(x1)) -> 7(7(x1)) 82.93/22.01 2(4(x1)) -> 0(7(x1)) 82.93/22.01 6(6(x1)) -> 3(x1) 82.93/22.01 0(3(x1)) -> 5(3(x1)) 82.93/22.01 82.93/22.01 Proof: 82.93/22.01 Complexity Transformation Processor: 82.93/22.01 strict: 82.93/22.01 2(7(x1)) -> 1(8(x1)) 82.93/22.01 2(8(1(x1))) -> 8(x1) 82.93/22.01 2(8(x1)) -> 4(x1) 82.93/22.01 5(9(x1)) -> 0(x1) 82.93/22.01 4(x1) -> 5(2(3(x1))) 82.93/22.01 5(3(x1)) -> 6(0(x1)) 82.93/22.01 2(8(x1)) -> 7(x1) 82.93/22.01 4(7(x1)) -> 1(3(x1)) 82.93/22.01 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.01 9(7(x1)) -> 7(5(x1)) 82.93/22.01 7(2(x1)) -> 4(x1) 82.93/22.01 7(0(x1)) -> 9(3(x1)) 82.93/22.01 6(9(x1)) -> 9(x1) 82.93/22.01 9(5(9(x1))) -> 5(7(x1)) 82.93/22.01 4(x1) -> 9(6(6(x1))) 82.93/22.01 9(x1) -> 6(7(x1)) 82.93/22.01 6(2(x1)) -> 7(7(x1)) 82.93/22.01 2(4(x1)) -> 0(7(x1)) 82.93/22.01 6(6(x1)) -> 3(x1) 82.93/22.01 0(3(x1)) -> 5(3(x1)) 82.93/22.01 weak: 82.93/22.01 82.93/22.01 Matrix Interpretation Processor: dim=1 82.93/22.01 82.93/22.01 max_matrix: 82.93/22.01 1 82.93/22.01 interpretation: 82.93/22.01 [6](x0) = x0 + 2, 82.93/22.01 82.93/22.01 [3](x0) = x0 + 9, 82.93/22.01 82.93/22.01 [0](x0) = x0 + 10, 82.93/22.01 82.93/22.01 [5](x0) = x0 + 9, 82.93/22.01 82.93/22.01 [9](x0) = x0 + 3, 82.93/22.01 82.93/22.01 [4](x0) = x0 + 1, 82.93/22.01 82.93/22.01 [1](x0) = x0 + 9, 82.93/22.01 82.93/22.01 [8](x0) = x0 + 4, 82.93/22.01 82.93/22.01 [2](x0) = x0 + 3, 82.93/22.01 82.93/22.01 [7](x0) = x0 + 1 82.93/22.01 orientation: 82.93/22.01 2(7(x1)) = x1 + 4 >= x1 + 13 = 1(8(x1)) 82.93/22.01 82.93/22.01 2(8(1(x1))) = x1 + 16 >= x1 + 4 = 8(x1) 82.93/22.01 82.93/22.01 2(8(x1)) = x1 + 7 >= x1 + 1 = 4(x1) 82.93/22.01 82.93/22.01 5(9(x1)) = x1 + 12 >= x1 + 10 = 0(x1) 82.93/22.01 82.93/22.01 4(x1) = x1 + 1 >= x1 + 21 = 5(2(3(x1))) 82.93/22.01 82.93/22.01 5(3(x1)) = x1 + 18 >= x1 + 12 = 6(0(x1)) 82.93/22.01 82.93/22.01 2(8(x1)) = x1 + 7 >= x1 + 1 = 7(x1) 82.93/22.01 82.93/22.01 4(7(x1)) = x1 + 2 >= x1 + 18 = 1(3(x1)) 82.93/22.01 82.93/22.01 5(2(6(x1))) = x1 + 14 >= x1 + 6 = 6(2(4(x1))) 82.93/22.01 82.93/22.01 9(7(x1)) = x1 + 4 >= x1 + 10 = 7(5(x1)) 82.93/22.01 82.93/22.01 7(2(x1)) = x1 + 4 >= x1 + 1 = 4(x1) 82.93/22.01 82.93/22.01 7(0(x1)) = x1 + 11 >= x1 + 12 = 9(3(x1)) 82.93/22.01 82.93/22.01 6(9(x1)) = x1 + 5 >= x1 + 3 = 9(x1) 82.93/22.01 82.93/22.01 9(5(9(x1))) = x1 + 15 >= x1 + 10 = 5(7(x1)) 82.93/22.01 82.93/22.01 4(x1) = x1 + 1 >= x1 + 7 = 9(6(6(x1))) 82.93/22.01 82.93/22.01 9(x1) = x1 + 3 >= x1 + 3 = 6(7(x1)) 82.93/22.01 82.93/22.01 6(2(x1)) = x1 + 5 >= x1 + 2 = 7(7(x1)) 82.93/22.01 82.93/22.01 2(4(x1)) = x1 + 4 >= x1 + 11 = 0(7(x1)) 82.93/22.01 82.93/22.01 6(6(x1)) = x1 + 4 >= x1 + 9 = 3(x1) 82.93/22.01 82.93/22.01 0(3(x1)) = x1 + 19 >= x1 + 18 = 5(3(x1)) 82.93/22.01 problem: 82.93/22.01 strict: 82.93/22.01 2(7(x1)) -> 1(8(x1)) 82.93/22.01 4(x1) -> 5(2(3(x1))) 82.93/22.01 4(7(x1)) -> 1(3(x1)) 82.93/22.01 9(7(x1)) -> 7(5(x1)) 82.93/22.01 7(0(x1)) -> 9(3(x1)) 82.93/22.01 4(x1) -> 9(6(6(x1))) 82.93/22.01 9(x1) -> 6(7(x1)) 82.93/22.01 2(4(x1)) -> 0(7(x1)) 82.93/22.01 6(6(x1)) -> 3(x1) 82.93/22.01 weak: 82.93/22.01 2(8(1(x1))) -> 8(x1) 82.93/22.01 2(8(x1)) -> 4(x1) 82.93/22.01 5(9(x1)) -> 0(x1) 82.93/22.01 5(3(x1)) -> 6(0(x1)) 82.93/22.01 2(8(x1)) -> 7(x1) 82.93/22.01 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.01 7(2(x1)) -> 4(x1) 82.93/22.01 6(9(x1)) -> 9(x1) 82.93/22.01 9(5(9(x1))) -> 5(7(x1)) 82.93/22.01 6(2(x1)) -> 7(7(x1)) 82.93/22.01 0(3(x1)) -> 5(3(x1)) 82.93/22.01 Matrix Interpretation Processor: dim=1 82.93/22.01 82.93/22.01 max_matrix: 82.93/22.01 1 82.93/22.01 interpretation: 82.93/22.01 [6](x0) = x0 + 1, 82.93/22.01 82.93/22.01 [3](x0) = x0 + 1, 82.93/22.01 82.93/22.01 [0](x0) = x0 + 10, 82.93/22.01 82.93/22.01 [5](x0) = x0 + 10, 82.93/22.01 82.93/22.01 [9](x0) = x0 + 4, 82.93/22.01 82.93/22.01 [4](x0) = x0 + 4, 82.93/22.01 82.93/22.01 [1](x0) = x0 + 5, 82.93/22.01 82.93/22.01 [8](x0) = x0, 82.93/22.01 82.93/22.01 [2](x0) = x0 + 13, 82.93/22.01 82.93/22.01 [7](x0) = x0 82.93/22.01 orientation: 82.93/22.01 2(7(x1)) = x1 + 13 >= x1 + 5 = 1(8(x1)) 82.93/22.01 82.93/22.01 4(x1) = x1 + 4 >= x1 + 24 = 5(2(3(x1))) 82.93/22.01 82.93/22.01 4(7(x1)) = x1 + 4 >= x1 + 6 = 1(3(x1)) 82.93/22.01 82.93/22.01 9(7(x1)) = x1 + 4 >= x1 + 10 = 7(5(x1)) 82.93/22.01 82.93/22.01 7(0(x1)) = x1 + 10 >= x1 + 5 = 9(3(x1)) 82.93/22.01 82.93/22.01 4(x1) = x1 + 4 >= x1 + 6 = 9(6(6(x1))) 82.93/22.01 82.93/22.01 9(x1) = x1 + 4 >= x1 + 1 = 6(7(x1)) 82.93/22.01 82.93/22.01 2(4(x1)) = x1 + 17 >= x1 + 10 = 0(7(x1)) 82.93/22.01 82.93/22.01 6(6(x1)) = x1 + 2 >= x1 + 1 = 3(x1) 82.93/22.01 82.93/22.01 2(8(1(x1))) = x1 + 18 >= x1 = 8(x1) 82.93/22.01 82.93/22.01 2(8(x1)) = x1 + 13 >= x1 + 4 = 4(x1) 82.93/22.01 82.93/22.01 5(9(x1)) = x1 + 14 >= x1 + 10 = 0(x1) 82.93/22.01 82.93/22.01 5(3(x1)) = x1 + 11 >= x1 + 11 = 6(0(x1)) 82.93/22.01 82.93/22.01 2(8(x1)) = x1 + 13 >= x1 = 7(x1) 82.93/22.01 82.93/22.01 5(2(6(x1))) = x1 + 24 >= x1 + 18 = 6(2(4(x1))) 82.93/22.01 82.93/22.01 7(2(x1)) = x1 + 13 >= x1 + 4 = 4(x1) 82.93/22.01 82.93/22.01 6(9(x1)) = x1 + 5 >= x1 + 4 = 9(x1) 82.93/22.01 82.93/22.01 9(5(9(x1))) = x1 + 18 >= x1 + 10 = 5(7(x1)) 82.93/22.02 82.93/22.02 6(2(x1)) = x1 + 14 >= x1 = 7(7(x1)) 82.93/22.02 82.93/22.02 0(3(x1)) = x1 + 11 >= x1 + 11 = 5(3(x1)) 82.93/22.02 problem: 82.93/22.02 strict: 82.93/22.02 4(x1) -> 5(2(3(x1))) 82.93/22.02 4(7(x1)) -> 1(3(x1)) 82.93/22.02 9(7(x1)) -> 7(5(x1)) 82.93/22.02 4(x1) -> 9(6(6(x1))) 82.93/22.02 weak: 82.93/22.02 2(7(x1)) -> 1(8(x1)) 82.93/22.02 7(0(x1)) -> 9(3(x1)) 82.93/22.02 9(x1) -> 6(7(x1)) 82.93/22.02 2(4(x1)) -> 0(7(x1)) 82.93/22.02 6(6(x1)) -> 3(x1) 82.93/22.02 2(8(1(x1))) -> 8(x1) 82.93/22.02 2(8(x1)) -> 4(x1) 82.93/22.02 5(9(x1)) -> 0(x1) 82.93/22.02 5(3(x1)) -> 6(0(x1)) 82.93/22.02 2(8(x1)) -> 7(x1) 82.93/22.02 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.02 7(2(x1)) -> 4(x1) 82.93/22.02 6(9(x1)) -> 9(x1) 82.93/22.02 9(5(9(x1))) -> 5(7(x1)) 82.93/22.02 6(2(x1)) -> 7(7(x1)) 82.93/22.02 0(3(x1)) -> 5(3(x1)) 82.93/22.02 Matrix Interpretation Processor: dim=1 82.93/22.02 82.93/22.02 max_matrix: 82.93/22.02 1 82.93/22.02 interpretation: 82.93/22.02 [6](x0) = x0, 82.93/22.02 82.93/22.02 [3](x0) = x0, 82.93/22.02 82.93/22.02 [0](x0) = x0, 82.93/22.02 82.93/22.02 [5](x0) = x0, 82.93/22.02 82.93/22.02 [9](x0) = x0 + 1, 82.93/22.02 82.93/22.02 [4](x0) = x0, 82.93/22.02 82.93/22.02 [1](x0) = x0, 82.93/22.02 82.93/22.02 [8](x0) = x0, 82.93/22.02 82.93/22.02 [2](x0) = x0 + 2, 82.93/22.02 82.93/22.02 [7](x0) = x0 + 1 82.93/22.02 orientation: 82.93/22.02 4(x1) = x1 >= x1 + 2 = 5(2(3(x1))) 82.93/22.02 82.93/22.02 4(7(x1)) = x1 + 1 >= x1 = 1(3(x1)) 82.93/22.02 82.93/22.02 9(7(x1)) = x1 + 2 >= x1 + 1 = 7(5(x1)) 82.93/22.02 82.93/22.02 4(x1) = x1 >= x1 + 1 = 9(6(6(x1))) 82.93/22.02 82.93/22.02 2(7(x1)) = x1 + 3 >= x1 = 1(8(x1)) 82.93/22.02 82.93/22.02 7(0(x1)) = x1 + 1 >= x1 + 1 = 9(3(x1)) 82.93/22.02 82.93/22.02 9(x1) = x1 + 1 >= x1 + 1 = 6(7(x1)) 82.93/22.02 82.93/22.02 2(4(x1)) = x1 + 2 >= x1 + 1 = 0(7(x1)) 82.93/22.02 82.93/22.02 6(6(x1)) = x1 >= x1 = 3(x1) 82.93/22.02 82.93/22.02 2(8(1(x1))) = x1 + 2 >= x1 = 8(x1) 82.93/22.02 82.93/22.02 2(8(x1)) = x1 + 2 >= x1 = 4(x1) 82.93/22.02 82.93/22.02 5(9(x1)) = x1 + 1 >= x1 = 0(x1) 82.93/22.02 82.93/22.02 5(3(x1)) = x1 >= x1 = 6(0(x1)) 82.93/22.02 82.93/22.02 2(8(x1)) = x1 + 2 >= x1 + 1 = 7(x1) 82.93/22.02 82.93/22.02 5(2(6(x1))) = x1 + 2 >= x1 + 2 = 6(2(4(x1))) 82.93/22.02 82.93/22.02 7(2(x1)) = x1 + 3 >= x1 = 4(x1) 82.93/22.02 82.93/22.02 6(9(x1)) = x1 + 1 >= x1 + 1 = 9(x1) 82.93/22.02 82.93/22.02 9(5(9(x1))) = x1 + 2 >= x1 + 1 = 5(7(x1)) 82.93/22.02 82.93/22.02 6(2(x1)) = x1 + 2 >= x1 + 2 = 7(7(x1)) 82.93/22.02 82.93/22.02 0(3(x1)) = x1 >= x1 = 5(3(x1)) 82.93/22.02 problem: 82.93/22.02 strict: 82.93/22.02 4(x1) -> 5(2(3(x1))) 82.93/22.02 4(x1) -> 9(6(6(x1))) 82.93/22.02 weak: 82.93/22.02 4(7(x1)) -> 1(3(x1)) 82.93/22.02 9(7(x1)) -> 7(5(x1)) 82.93/22.02 2(7(x1)) -> 1(8(x1)) 82.93/22.02 7(0(x1)) -> 9(3(x1)) 82.93/22.02 9(x1) -> 6(7(x1)) 82.93/22.02 2(4(x1)) -> 0(7(x1)) 82.93/22.02 6(6(x1)) -> 3(x1) 82.93/22.02 2(8(1(x1))) -> 8(x1) 82.93/22.02 2(8(x1)) -> 4(x1) 82.93/22.02 5(9(x1)) -> 0(x1) 82.93/22.02 5(3(x1)) -> 6(0(x1)) 82.93/22.02 2(8(x1)) -> 7(x1) 82.93/22.02 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.02 7(2(x1)) -> 4(x1) 82.93/22.02 6(9(x1)) -> 9(x1) 82.93/22.02 9(5(9(x1))) -> 5(7(x1)) 82.93/22.02 6(2(x1)) -> 7(7(x1)) 82.93/22.02 0(3(x1)) -> 5(3(x1)) 82.93/22.02 Splitting Processor: 82.93/22.02 strict: 82.93/22.02 4(x1) -> 9(6(6(x1))) 82.93/22.02 weak: 82.93/22.02 4(7(x1)) -> 1(3(x1)) 82.93/22.02 9(7(x1)) -> 7(5(x1)) 82.93/22.02 2(7(x1)) -> 1(8(x1)) 82.93/22.02 7(0(x1)) -> 9(3(x1)) 82.93/22.02 9(x1) -> 6(7(x1)) 82.93/22.02 2(4(x1)) -> 0(7(x1)) 82.93/22.02 6(6(x1)) -> 3(x1) 82.93/22.02 2(8(1(x1))) -> 8(x1) 82.93/22.02 2(8(x1)) -> 4(x1) 82.93/22.02 5(9(x1)) -> 0(x1) 82.93/22.02 5(3(x1)) -> 6(0(x1)) 82.93/22.02 2(8(x1)) -> 7(x1) 82.93/22.02 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.02 7(2(x1)) -> 4(x1) 82.93/22.02 6(9(x1)) -> 9(x1) 82.93/22.02 9(5(9(x1))) -> 5(7(x1)) 82.93/22.02 6(2(x1)) -> 7(7(x1)) 82.93/22.02 0(3(x1)) -> 5(3(x1)) 82.93/22.02 4(x1) -> 5(2(3(x1))) 82.93/22.02 Matrix Interpretation Processor: dim=5 82.93/22.02 82.93/22.02 max_matrix: 82.93/22.02 [1 1 0 1 0] 82.93/22.02 [0 0 1 1 1] 82.93/22.02 [0 0 0 0 1] 82.93/22.02 [0 0 0 0 0] 82.93/22.02 [0 0 0 0 0] 82.93/22.02 interpretation: 82.93/22.02 [1 0 0 0 0] [0] 82.93/22.02 [0 0 0 1 0] [0] 82.93/22.02 [6](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.02 [0 0 0 0 0] [0] 82.93/22.02 [0 0 0 0 0] [1], 82.93/22.02 82.93/22.02 [1 0 0 0 0] 82.93/22.02 [0 0 0 0 0] 82.93/22.02 [3](x0) = [0 0 0 0 0]x0 82.93/22.02 [0 0 0 0 0] 82.93/22.02 [0 0 0 0 0] , 82.93/22.02 82.93/22.02 [1 0 0 0 0] [0] 82.93/22.02 [0 0 0 0 0] [0] 82.93/22.02 [0](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.02 [0 0 0 0 0] [0] 82.93/22.02 [0 0 0 0 0] [1], 82.93/22.02 82.93/22.02 [1 0 0 1 0] [0] 82.93/22.02 [0 0 1 0 0] [0] 82.93/22.02 [5](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1], 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [9](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1], 82.93/22.03 82.93/22.03 [1 0 0 1 0] [1] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [4](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1], 82.93/22.03 82.93/22.03 [1 0 0 1 0] 82.93/22.03 [0 0 1 1 0] 82.93/22.03 [1](x0) = [0 0 0 0 0]x0 82.93/22.03 [0 0 0 0 0] 82.93/22.03 [0 0 0 0 0] , 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [1] 82.93/22.03 [8](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1], 82.93/22.03 82.93/22.03 [1 1 0 1 0] [0] 82.93/22.03 [0 0 0 1 1] [0] 82.93/22.03 [2](x0) = [0 0 0 0 1]x0 + [0] 82.93/22.03 [0 0 0 0 0] [1] 82.93/22.03 [0 0 0 0 0] [1], 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [7](x0) = [0 0 0 0 0]x0 + [0] 82.93/22.03 [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] 82.93/22.03 orientation: 82.93/22.03 [1 0 0 1 0] [1] [1 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 4(x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 9(6(6(x1))) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.03 82.93/22.03 [1 0 0 1 0] [1] [1 0 0 0 0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] 82.93/22.03 4(7(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 1(3(x1)) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 9(7(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 7(5(x1)) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] [1 0 0 1 0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] 82.93/22.03 2(7(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 1(8(x1)) 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] 82.93/22.03 82.93/22.03 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 7(0(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 9(3(x1)) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.03 82.93/22.03 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 9(x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 6(7(x1)) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.03 82.93/22.03 [1 0 0 1 0] [1] [1 0 0 1 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.03 2(4(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(7(x1)) 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.03 82.93/22.03 [1 0 0 0 0] [0] [1 0 0 0 0] 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] 82.93/22.03 6(6(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = 3(x1) 82.93/22.03 [0 0 0 0 0] [0] [0 0 0 0 0] 82.93/22.03 [0 0 0 0 0] [1] [0 0 0 0 0] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [1] [1 0 0 1 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 2(8(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 8(x1) 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [1] [1 0 0 1 0] [1] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 2(8(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 4(x1) 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [0] [1 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 5(9(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 0(x1) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 5(3(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 6(0(x1)) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [1] [1 0 0 1 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 2(8(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 7(x1) 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [1] [1 0 0 1 0] [1] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 5(2(6(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 6(2(4(x1))) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 1 0 1 0] [1] [1 0 0 1 0] [1] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 7(2(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 4(x1) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 6(9(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 9(x1) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 1 0] [0] [1 0 0 1 0] [0] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 9(5(9(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(7(x1)) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 1 0 1 0] [0] [1 0 0 1 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 82.93/22.04 6(2(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 7(7(x1)) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.04 82.93/22.04 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 0(3(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(3(x1)) 82.93/22.04 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.04 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.05 82.93/22.05 [1 0 0 1 0] [1] [1 0 0 0 0] [1] 82.93/22.05 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.05 4(x1) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = 5(2(3(x1))) 82.93/22.05 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 82.93/22.05 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 82.93/22.05 problem: 82.93/22.05 strict: 82.93/22.05 82.93/22.05 weak: 82.93/22.05 4(x1) -> 9(6(6(x1))) 82.93/22.05 4(7(x1)) -> 1(3(x1)) 82.93/22.05 9(7(x1)) -> 7(5(x1)) 82.93/22.05 2(7(x1)) -> 1(8(x1)) 82.93/22.05 7(0(x1)) -> 9(3(x1)) 82.93/22.05 9(x1) -> 6(7(x1)) 82.93/22.05 2(4(x1)) -> 0(7(x1)) 82.93/22.05 6(6(x1)) -> 3(x1) 82.93/22.05 2(8(1(x1))) -> 8(x1) 82.93/22.05 2(8(x1)) -> 4(x1) 82.93/22.05 5(9(x1)) -> 0(x1) 82.93/22.05 5(3(x1)) -> 6(0(x1)) 82.93/22.05 2(8(x1)) -> 7(x1) 82.93/22.05 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.05 7(2(x1)) -> 4(x1) 82.93/22.05 6(9(x1)) -> 9(x1) 82.93/22.05 9(5(9(x1))) -> 5(7(x1)) 82.93/22.05 6(2(x1)) -> 7(7(x1)) 82.93/22.05 0(3(x1)) -> 5(3(x1)) 82.93/22.05 4(x1) -> 5(2(3(x1))) 82.93/22.05 Qed 82.93/22.05 82.93/22.05 strict: 82.93/22.05 4(x1) -> 5(2(3(x1))) 82.93/22.05 weak: 82.93/22.05 4(x1) -> 9(6(6(x1))) 82.93/22.05 4(7(x1)) -> 1(3(x1)) 82.93/22.05 9(7(x1)) -> 7(5(x1)) 82.93/22.05 2(7(x1)) -> 1(8(x1)) 82.93/22.05 7(0(x1)) -> 9(3(x1)) 82.93/22.05 9(x1) -> 6(7(x1)) 82.93/22.05 2(4(x1)) -> 0(7(x1)) 82.93/22.05 6(6(x1)) -> 3(x1) 82.93/22.05 2(8(1(x1))) -> 8(x1) 82.93/22.05 2(8(x1)) -> 4(x1) 82.93/22.05 5(9(x1)) -> 0(x1) 82.93/22.05 5(3(x1)) -> 6(0(x1)) 82.93/22.05 2(8(x1)) -> 7(x1) 82.93/22.05 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.05 7(2(x1)) -> 4(x1) 82.93/22.05 6(9(x1)) -> 9(x1) 82.93/22.05 9(5(9(x1))) -> 5(7(x1)) 82.93/22.05 6(2(x1)) -> 7(7(x1)) 82.93/22.05 0(3(x1)) -> 5(3(x1)) 82.93/22.05 Matrix Interpretation Processor: dim=4 82.93/22.05 82.93/22.05 max_matrix: 82.93/22.05 [1 2 3 0] 82.93/22.05 [0 0 2 0] 82.93/22.05 [0 0 0 1] 82.93/22.05 [0 0 0 0] 82.93/22.05 interpretation: 82.93/22.05 [1 1 0 0] [0] 82.93/22.05 [0 0 1 0] [0] 82.93/22.05 [6](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 0 0 0] 82.93/22.05 [0 0 0 0] 82.93/22.05 [3](x0) = [0 0 0 0]x0 82.93/22.05 [0 0 0 0] , 82.93/22.05 82.93/22.05 [1 0 0 0] [0] 82.93/22.05 [0 0 0 0] [0] 82.93/22.05 [0](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 0 1 0] [0] 82.93/22.05 [0 0 1 0] [0] 82.93/22.05 [5](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 1 3 0] [0] 82.93/22.05 [0 0 0 0] [0] 82.93/22.05 [9](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 1 2 0] [1] 82.93/22.05 [0 0 0 0] [0] 82.93/22.05 [4](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 1 0 0] 82.93/22.05 [0 0 2 0] 82.93/22.05 [1](x0) = [0 0 0 1]x0 82.93/22.05 [0 0 0 0] , 82.93/22.05 82.93/22.05 [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [0] 82.93/22.05 [8](x0) = [0 0 0 0]x0 + [1] 82.93/22.05 [0 0 0 0] [2], 82.93/22.05 82.93/22.05 [1 2 1 0] [0] 82.93/22.05 [0 0 1 0] [2] 82.93/22.05 [2](x0) = [0 0 0 1]x0 + [0] 82.93/22.05 [0 0 0 0] [3], 82.93/22.05 82.93/22.05 [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [0] 82.93/22.05 [7](x0) = [0 0 0 0]x0 + [0] 82.93/22.05 [0 0 0 0] [3] 82.93/22.05 orientation: 82.93/22.05 [1 1 2 0] [1] [1 0 0 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 4(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(2(3(x1))) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [1] [1 1 1 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 4(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 9(6(6(x1))) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [1] [1 0 0 0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] 82.93/22.05 4(7(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 1(3(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] 82.93/22.05 82.93/22.05 [1 1 2 0] [0] [1 0 2 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 9(7(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 7(5(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [0] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [2] [0 0 0 0] [2] 82.93/22.05 2(7(x1)) = [0 0 0 0]x1 + [3] >= [0 0 0 0]x1 + [2] = 1(8(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [0] 82.93/22.05 82.93/22.05 [1 0 0 0] [0] [1 0 0 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 7(0(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 9(3(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 3 0] [0] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 9(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 6(7(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [1] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [2] [0 0 0 0] [0] 82.93/22.05 2(4(x1)) = [0 0 0 0]x1 + [3] >= [0 0 0 0]x1 + [0] = 0(7(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 1 0] [0] [1 0 0 0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] 82.93/22.05 6(6(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = 3(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] 82.93/22.05 82.93/22.05 [1 1 2 2] [1] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [0] 82.93/22.05 2(8(1(x1))) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [1] = 8(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [2] 82.93/22.05 82.93/22.05 [1 1 2 0] [1] [1 1 2 0] [1] 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [0] 82.93/22.05 2(8(x1)) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [0] = 4(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 3 0] [0] [1 0 0 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 5(9(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 0(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 0 0 0] [0] [1 0 0 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 5(3(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 6(0(x1)) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [1] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [0] 82.93/22.05 2(8(x1)) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [0] = 7(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 2 0] [3] [1 1 2 0] [3] 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 5(2(6(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 6(2(4(x1))) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 2 2 2] [2] [1 1 2 0] [1] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 7(2(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 4(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 3 0] [0] [1 1 3 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 6(9(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 9(x1) 82.93/22.05 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.05 82.93/22.05 [1 1 3 0] [0] [1 1 2 0] [0] 82.93/22.05 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.05 9(5(9(x1))) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(7(x1)) 82.93/22.06 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.06 82.93/22.06 [1 2 2 0] [2] [1 1 2 0] [0] 82.93/22.06 [0 0 0 1] [0] [0 0 0 0] [0] 82.93/22.06 6(2(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 7(7(x1)) 82.93/22.06 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.06 82.93/22.06 [1 0 0 0] [0] [1 0 0 0] [0] 82.93/22.06 [0 0 0 0] [0] [0 0 0 0] [0] 82.93/22.06 0(3(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = 5(3(x1)) 82.93/22.06 [0 0 0 0] [3] [0 0 0 0] [3] 82.93/22.06 problem: 82.93/22.06 strict: 82.93/22.06 82.93/22.06 weak: 82.93/22.06 4(x1) -> 5(2(3(x1))) 82.93/22.06 4(x1) -> 9(6(6(x1))) 82.93/22.06 4(7(x1)) -> 1(3(x1)) 82.93/22.06 9(7(x1)) -> 7(5(x1)) 82.93/22.06 2(7(x1)) -> 1(8(x1)) 82.93/22.06 7(0(x1)) -> 9(3(x1)) 82.93/22.06 9(x1) -> 6(7(x1)) 82.93/22.06 2(4(x1)) -> 0(7(x1)) 82.93/22.06 6(6(x1)) -> 3(x1) 82.93/22.06 2(8(1(x1))) -> 8(x1) 82.93/22.06 2(8(x1)) -> 4(x1) 82.93/22.06 5(9(x1)) -> 0(x1) 82.93/22.06 5(3(x1)) -> 6(0(x1)) 82.93/22.06 2(8(x1)) -> 7(x1) 82.93/22.06 5(2(6(x1))) -> 6(2(4(x1))) 82.93/22.06 7(2(x1)) -> 4(x1) 82.93/22.06 6(9(x1)) -> 9(x1) 82.93/22.06 9(5(9(x1))) -> 5(7(x1)) 82.93/22.06 6(2(x1)) -> 7(7(x1)) 82.93/22.06 0(3(x1)) -> 5(3(x1)) 82.93/22.06 Qed 82.93/22.06 EOF