YES(?,O(n^2)) 328.06/95.98 YES(?,O(n^2)) 328.06/95.99 328.06/95.99 Problem: 328.06/95.99 q0(0(x1)) -> 0'(q1(x1)) 328.06/95.99 q1(0(x1)) -> 0(q1(x1)) 328.06/95.99 q1(1'(x1)) -> 1'(q1(x1)) 328.06/95.99 0(q1(1(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.06/95.99 0(q2(0(x1))) -> q2(0(0(x1))) 328.06/95.99 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.06/95.99 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.06/95.99 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.06/95.99 q2(0'(x1)) -> 0'(q0(x1)) 328.06/95.99 q0(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 q3(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 q3(b(x1)) -> b(q4(x1)) 328.06/95.99 328.06/95.99 Proof: 328.06/95.99 Complexity Transformation Processor: 328.06/95.99 strict: 328.06/95.99 q0(0(x1)) -> 0'(q1(x1)) 328.06/95.99 q1(0(x1)) -> 0(q1(x1)) 328.06/95.99 q1(1'(x1)) -> 1'(q1(x1)) 328.06/95.99 0(q1(1(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.06/95.99 0(q2(0(x1))) -> q2(0(0(x1))) 328.06/95.99 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.06/95.99 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.06/95.99 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.06/95.99 q2(0'(x1)) -> 0'(q0(x1)) 328.06/95.99 q0(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 q3(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 q3(b(x1)) -> b(q4(x1)) 328.06/95.99 weak: 328.06/95.99 328.06/95.99 Matrix Interpretation Processor: dim=1 328.06/95.99 328.06/95.99 max_matrix: 328.06/95.99 1 328.06/95.99 interpretation: 328.06/95.99 [q4](x0) = x0 + 1, 328.06/95.99 328.06/95.99 [b](x0) = x0 + 3, 328.06/95.99 328.06/95.99 [q3](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [q2](x0) = x0 + 6, 328.06/95.99 328.06/95.99 [1](x0) = x0 + 1, 328.06/95.99 328.06/95.99 [1'](x0) = x0 + 10, 328.06/95.99 328.06/95.99 [0'](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [q1](x0) = x0 + 7, 328.06/95.99 328.06/95.99 [q0](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [0](x0) = x0 328.06/95.99 orientation: 328.06/95.99 q0(0(x1)) = x1 + 4 >= x1 + 11 = 0'(q1(x1)) 328.06/95.99 328.06/95.99 q1(0(x1)) = x1 + 7 >= x1 + 7 = 0(q1(x1)) 328.06/95.99 328.06/95.99 q1(1'(x1)) = x1 + 17 >= x1 + 17 = 1'(q1(x1)) 328.06/95.99 328.06/95.99 0(q1(1(x1))) = x1 + 8 >= x1 + 16 = q2(0(1'(x1))) 328.06/95.99 328.06/95.99 0'(q1(1(x1))) = x1 + 12 >= x1 + 20 = q2(0'(1'(x1))) 328.06/95.99 328.06/95.99 1'(q1(1(x1))) = x1 + 18 >= x1 + 26 = q2(1'(1'(x1))) 328.06/95.99 328.06/95.99 0(q2(0(x1))) = x1 + 6 >= x1 + 6 = q2(0(0(x1))) 328.06/95.99 328.06/95.99 0'(q2(0(x1))) = x1 + 10 >= x1 + 10 = q2(0'(0(x1))) 328.06/95.99 328.06/95.99 1'(q2(0(x1))) = x1 + 16 >= x1 + 16 = q2(1'(0(x1))) 328.06/95.99 328.06/95.99 0(q2(1'(x1))) = x1 + 16 >= x1 + 16 = q2(0(1'(x1))) 328.06/95.99 328.06/95.99 0'(q2(1'(x1))) = x1 + 20 >= x1 + 20 = q2(0'(1'(x1))) 328.06/95.99 328.06/95.99 1'(q2(1'(x1))) = x1 + 26 >= x1 + 26 = q2(1'(1'(x1))) 328.06/95.99 328.06/95.99 q2(0'(x1)) = x1 + 10 >= x1 + 8 = 0'(q0(x1)) 328.06/95.99 328.06/95.99 q0(1'(x1)) = x1 + 14 >= x1 + 14 = 1'(q3(x1)) 328.06/95.99 328.06/95.99 q3(1'(x1)) = x1 + 14 >= x1 + 14 = 1'(q3(x1)) 328.06/95.99 328.06/95.99 q3(b(x1)) = x1 + 7 >= x1 + 4 = b(q4(x1)) 328.06/95.99 problem: 328.06/95.99 strict: 328.06/95.99 q0(0(x1)) -> 0'(q1(x1)) 328.06/95.99 q1(0(x1)) -> 0(q1(x1)) 328.06/95.99 q1(1'(x1)) -> 1'(q1(x1)) 328.06/95.99 0(q1(1(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.06/95.99 0(q2(0(x1))) -> q2(0(0(x1))) 328.06/95.99 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.06/95.99 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.06/95.99 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.06/95.99 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.06/95.99 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.06/95.99 q0(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 q3(1'(x1)) -> 1'(q3(x1)) 328.06/95.99 weak: 328.06/95.99 q2(0'(x1)) -> 0'(q0(x1)) 328.06/95.99 q3(b(x1)) -> b(q4(x1)) 328.06/95.99 Matrix Interpretation Processor: dim=1 328.06/95.99 328.06/95.99 max_matrix: 328.06/95.99 1 328.06/95.99 interpretation: 328.06/95.99 [q4](x0) = x0 + 2, 328.06/95.99 328.06/95.99 [b](x0) = x0 + 6, 328.06/95.99 328.06/95.99 [q3](x0) = x0 + 2, 328.06/95.99 328.06/95.99 [q2](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [1](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [1'](x0) = x0, 328.06/95.99 328.06/95.99 [0'](x0) = x0 + 12, 328.06/95.99 328.06/95.99 [q1](x0) = x0, 328.06/95.99 328.06/95.99 [q0](x0) = x0 + 4, 328.06/95.99 328.06/95.99 [0](x0) = x0 + 9 328.06/95.99 orientation: 328.06/95.99 q0(0(x1)) = x1 + 13 >= x1 + 12 = 0'(q1(x1)) 328.06/95.99 328.06/95.99 q1(0(x1)) = x1 + 9 >= x1 + 9 = 0(q1(x1)) 328.06/95.99 328.06/95.99 q1(1'(x1)) = x1 >= x1 = 1'(q1(x1)) 328.06/95.99 328.06/95.99 0(q1(1(x1))) = x1 + 13 >= x1 + 13 = q2(0(1'(x1))) 328.06/95.99 328.06/95.99 0'(q1(1(x1))) = x1 + 16 >= x1 + 16 = q2(0'(1'(x1))) 328.06/95.99 328.06/95.99 1'(q1(1(x1))) = x1 + 4 >= x1 + 4 = q2(1'(1'(x1))) 328.06/95.99 328.06/95.99 0(q2(0(x1))) = x1 + 22 >= x1 + 22 = q2(0(0(x1))) 328.06/95.99 328.06/95.99 0'(q2(0(x1))) = x1 + 25 >= x1 + 25 = q2(0'(0(x1))) 328.06/95.99 328.06/95.99 1'(q2(0(x1))) = x1 + 13 >= x1 + 13 = q2(1'(0(x1))) 328.06/95.99 328.06/95.99 0(q2(1'(x1))) = x1 + 13 >= x1 + 13 = q2(0(1'(x1))) 328.06/95.99 328.06/95.99 0'(q2(1'(x1))) = x1 + 16 >= x1 + 16 = q2(0'(1'(x1))) 328.06/95.99 328.06/95.99 1'(q2(1'(x1))) = x1 + 4 >= x1 + 4 = q2(1'(1'(x1))) 328.06/95.99 328.06/95.99 q0(1'(x1)) = x1 + 4 >= x1 + 2 = 1'(q3(x1)) 328.06/95.99 328.06/95.99 q3(1'(x1)) = x1 + 2 >= x1 + 2 = 1'(q3(x1)) 328.06/95.99 328.06/95.99 q2(0'(x1)) = x1 + 16 >= x1 + 16 = 0'(q0(x1)) 328.15/96.00 328.15/96.00 q3(b(x1)) = x1 + 8 >= x1 + 8 = b(q4(x1)) 328.15/96.00 problem: 328.15/96.00 strict: 328.15/96.00 q1(0(x1)) -> 0(q1(x1)) 328.15/96.00 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.00 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.00 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.00 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.00 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.00 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.00 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.00 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.00 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.00 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.00 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 weak: 328.15/96.00 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.00 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.00 q3(b(x1)) -> b(q4(x1)) 328.15/96.00 Matrix Interpretation Processor: dim=1 328.15/96.00 328.15/96.00 max_matrix: 328.15/96.00 1 328.15/96.00 interpretation: 328.15/96.00 [q4](x0) = x0 + 49, 328.15/96.00 328.15/96.00 [b](x0) = x0 + 82, 328.15/96.00 328.15/96.00 [q3](x0) = x0 + 49, 328.15/96.00 328.15/96.00 [q2](x0) = x0 + 96, 328.15/96.00 328.15/96.00 [1](x0) = x0 + 124, 328.15/96.00 328.15/96.00 [1'](x0) = x0 + 2, 328.15/96.00 328.15/96.00 [0'](x0) = x0 + 18, 328.15/96.00 328.15/96.00 [q1](x0) = x0 + 4, 328.15/96.00 328.15/96.00 [q0](x0) = x0 + 82, 328.15/96.00 328.15/96.00 [0](x0) = x0 + 3 328.15/96.00 orientation: 328.15/96.00 q1(0(x1)) = x1 + 7 >= x1 + 7 = 0(q1(x1)) 328.15/96.00 328.15/96.00 q1(1'(x1)) = x1 + 6 >= x1 + 6 = 1'(q1(x1)) 328.15/96.00 328.15/96.00 0(q1(1(x1))) = x1 + 131 >= x1 + 101 = q2(0(1'(x1))) 328.15/96.00 328.15/96.00 0'(q1(1(x1))) = x1 + 146 >= x1 + 116 = q2(0'(1'(x1))) 328.15/96.00 328.15/96.00 1'(q1(1(x1))) = x1 + 130 >= x1 + 100 = q2(1'(1'(x1))) 328.15/96.00 328.15/96.00 0(q2(0(x1))) = x1 + 102 >= x1 + 102 = q2(0(0(x1))) 328.15/96.00 328.15/96.00 0'(q2(0(x1))) = x1 + 117 >= x1 + 117 = q2(0'(0(x1))) 328.15/96.00 328.15/96.00 1'(q2(0(x1))) = x1 + 101 >= x1 + 101 = q2(1'(0(x1))) 328.15/96.00 328.15/96.00 0(q2(1'(x1))) = x1 + 101 >= x1 + 101 = q2(0(1'(x1))) 328.15/96.00 328.15/96.00 0'(q2(1'(x1))) = x1 + 116 >= x1 + 116 = q2(0'(1'(x1))) 328.15/96.00 328.15/96.00 1'(q2(1'(x1))) = x1 + 100 >= x1 + 100 = q2(1'(1'(x1))) 328.15/96.00 328.15/96.00 q3(1'(x1)) = x1 + 51 >= x1 + 51 = 1'(q3(x1)) 328.15/96.00 328.15/96.00 q0(0(x1)) = x1 + 85 >= x1 + 22 = 0'(q1(x1)) 328.15/96.00 328.15/96.00 q0(1'(x1)) = x1 + 84 >= x1 + 51 = 1'(q3(x1)) 328.15/96.00 328.15/96.00 q2(0'(x1)) = x1 + 114 >= x1 + 100 = 0'(q0(x1)) 328.15/96.00 328.15/96.00 q3(b(x1)) = x1 + 131 >= x1 + 131 = b(q4(x1)) 328.15/96.00 problem: 328.15/96.00 strict: 328.15/96.00 q1(0(x1)) -> 0(q1(x1)) 328.15/96.00 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.00 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.00 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.00 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.00 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.00 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.00 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.00 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 weak: 328.15/96.00 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.00 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.00 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.00 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.00 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.00 q3(b(x1)) -> b(q4(x1)) 328.15/96.00 Splitting Processor: 328.15/96.00 strict: 328.15/96.00 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.00 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.00 weak: 328.15/96.00 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.00 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.00 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.00 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.00 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.00 q3(b(x1)) -> b(q4(x1)) 328.15/96.00 q1(0(x1)) -> 0(q1(x1)) 328.15/96.00 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.00 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.00 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.00 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.00 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.00 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.00 Matrix Interpretation Processor: dim=5 328.15/96.00 328.15/96.00 max_matrix: 328.15/96.00 [1 0 1 1 1] 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [0 0 0 0 1] 328.15/96.00 [0 0 0 0 0] 328.15/96.00 interpretation: 328.15/96.00 [1 0 0 0 0] 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [q4](x0) = [0 0 0 0 0]x0 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [0 0 0 0 0] , 328.15/96.00 328.15/96.00 [1 0 0 0 0] 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [b](x0) = [0 0 0 0 0]x0 328.15/96.00 [0 0 0 0 0] 328.15/96.00 [0 0 0 0 0] , 328.15/96.00 328.15/96.00 [1 0 0 0 0] [0] 328.15/96.00 [0 0 0 0 0] [0] 328.15/96.00 [q3](x0) = [0 0 0 0 0]x0 + [1] 328.15/96.00 [0 0 0 0 1] [0] 328.15/96.00 [0 0 0 0 0] [0], 328.15/96.00 328.15/96.00 [1 0 1 0 1] 328.15/96.01 [0 0 0 0 0] 328.15/96.01 [q2](x0) = [0 0 0 0 0]x0 328.15/96.01 [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] , 328.15/96.01 328.15/96.01 [1 0 0 0 1] [1] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [1](x0) = [0 0 0 0 0]x0 + [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0], 328.15/96.01 328.15/96.01 [1 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [1'](x0) = [0 0 0 0 0]x0 + [1] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0], 328.15/96.01 328.15/96.01 [1 0 0 1 0] 328.15/96.01 [0 0 0 0 0] 328.15/96.01 [0'](x0) = [0 0 0 0 0]x0 328.15/96.01 [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] , 328.15/96.01 328.15/96.01 [1 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [q1](x0) = [0 0 0 0 0]x0 + [1] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [1], 328.15/96.01 328.15/96.01 [1 0 0 1 0] [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [q0](x0) = [0 0 0 0 0]x0 + [1] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0], 328.15/96.01 328.15/96.01 [1 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0](x0) = [0 0 0 0 0]x0 + [0] 328.15/96.01 [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [1] 328.15/96.01 orientation: 328.15/96.01 [1 0 0 0 0] [1] [1 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 0'(q2(0(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = q2(0'(0(x1))) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 328.15/96.01 [1 0 0 0 0] [1] [1 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 0'(q2(1'(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = q2(0'(1'(x1))) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 328.15/96.01 [1 0 0 0 1] [1] [1 0 0 0 0] [1] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 0(q1(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = q2(0(1'(x1))) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 328.15/96.01 328.15/96.01 [1 0 0 0 1] [1] [1 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 0'(q1(1(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 = q2(0'(1'(x1))) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 328.15/96.01 [1 0 0 0 1] [1] [1 0 0 0 0] [1] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 1'(q1(1(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = q2(1'(1'(x1))) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 328.15/96.01 [1 0 0 0 0] [0] [1 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 q0(0(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = 0'(q1(x1)) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.01 328.15/96.01 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 q0(1'(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1'(q3(x1)) 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.01 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 1 0] [1 0 0 1 0] 328.15/96.02 [0 0 0 0 0] [0 0 0 0 0] 328.15/96.02 q2(0'(x1)) = [0 0 0 0 0]x1 >= [0 0 0 0 0]x1 = 0'(q0(x1)) 328.15/96.02 [0 0 0 0 0] [0 0 0 0 0] 328.15/96.02 [0 0 0 0 0] [0 0 0 0 0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [0] [1 0 0 0 0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.02 q3(b(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 = b(q4(x1)) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 q1(0(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = 0(q1(x1)) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 q1(1'(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1'(q1(x1)) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 0(q2(0(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = q2(0(0(x1))) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 1'(q2(0(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = q2(1'(0(x1))) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 0(q2(1'(x1))) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = q2(0(1'(x1))) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [1] [1 0 0 0 0] [1] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 1'(q2(1'(x1))) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [0] = q2(1'(1'(x1))) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 328.15/96.02 [1 0 0 0 0] [0] [1 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 q3(1'(x1)) = [0 0 0 0 0]x1 + [1] >= [0 0 0 0 0]x1 + [1] = 1'(q3(x1)) 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 328.15/96.02 problem: 328.15/96.02 strict: 328.15/96.02 328.15/96.02 weak: 328.15/96.02 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.02 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.02 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.02 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.02 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.02 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.02 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.02 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.02 q3(b(x1)) -> b(q4(x1)) 328.15/96.02 q1(0(x1)) -> 0(q1(x1)) 328.15/96.02 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.02 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.02 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.03 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.03 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 Qed 328.15/96.03 328.15/96.03 strict: 328.15/96.03 q1(0(x1)) -> 0(q1(x1)) 328.15/96.03 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.03 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.03 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.03 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.03 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 weak: 328.15/96.03 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.03 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.03 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.03 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.03 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.03 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.03 q3(b(x1)) -> b(q4(x1)) 328.15/96.03 Splitting Processor: 328.15/96.03 strict: 328.15/96.03 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 weak: 328.15/96.03 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.03 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.03 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.03 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.03 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.03 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.03 q3(b(x1)) -> b(q4(x1)) 328.15/96.03 q1(0(x1)) -> 0(q1(x1)) 328.15/96.03 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.03 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.03 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.03 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.03 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.03 Matrix Interpretation Processor: dim=3 328.15/96.03 328.15/96.03 max_matrix: 328.15/96.03 [1 1 0] 328.15/96.03 [0 1 1] 328.15/96.03 [0 0 0] 328.15/96.03 interpretation: 328.15/96.03 [1 0 0] 328.15/96.03 [q4](x0) = [0 0 0]x0 328.15/96.03 [0 0 0] , 328.15/96.03 328.15/96.03 [1 0 0] [0] 328.15/96.03 [b](x0) = [0 1 1]x0 + [1] 328.15/96.03 [0 0 0] [0], 328.15/96.03 328.15/96.03 [1 0 0] [0] 328.15/96.03 [q3](x0) = [0 1 0]x0 + [1] 328.15/96.03 [0 0 0] [0], 328.15/96.03 328.15/96.03 [1 0 0] [0] 328.15/96.03 [q2](x0) = [0 1 0]x0 + [1] 328.15/96.03 [0 0 0] [0], 328.15/96.03 328.15/96.03 [1 0 0] [0] 328.15/96.03 [1](x0) = [0 1 1]x0 + [1] 328.15/96.03 [0 0 0] [0], 328.15/96.03 328.15/96.03 [1 0 0] 328.15/96.03 [1'](x0) = [0 1 0]x0 328.15/96.03 [0 0 0] , 328.15/96.03 328.15/96.03 [1 0 0] 328.15/96.03 [0'](x0) = [0 1 0]x0 328.15/96.03 [0 0 0] , 328.15/96.03 328.15/96.03 [1 1 0] [0] 328.15/96.03 [q1](x0) = [0 1 0]x0 + [1] 328.15/96.03 [0 0 0] [1], 328.15/96.03 328.15/96.03 [1 0 0] [0] 328.15/96.03 [q0](x0) = [0 1 0]x0 + [1] 328.15/96.03 [0 0 0] [0], 328.15/96.03 328.15/96.03 [1 1 0] [0] 328.15/96.03 [0](x0) = [0 1 0]x0 + [1] 328.15/96.03 [0 0 0] [0] 328.15/96.03 orientation: 328.15/96.03 [1 2 0] [1] [1 2 0] [1] 328.15/96.03 q1(0(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 0(q1(x1)) 328.15/96.03 [0 0 0] [1] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 0] [0] [1 1 0] [0] 328.15/96.03 q1(1'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1'(q1(x1)) 328.15/96.03 [0 0 0] [1] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 2 0] [2] [1 2 0] [1] 328.15/96.03 0(q2(0(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(0(0(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 0] [0] [1 1 0] [0] 328.15/96.03 1'(q2(0(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(1'(0(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 0] [1] [1 1 0] [0] 328.15/96.03 0(q2(1'(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 1'(q2(1'(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = q2(1'(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 q3(1'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1'(q3(x1)) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 0] [0] [1 1 0] [0] 328.15/96.03 0'(q2(0(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0'(0(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 0'(q2(1'(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = q2(0'(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 2 2] [3] [1 1 0] [0] 328.15/96.03 0(q1(1(x1))) = [0 1 1]x1 + [3] >= [0 1 0]x1 + [2] = q2(0(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 1] [1] [1 0 0] [0] 328.15/96.03 0'(q1(1(x1))) = [0 1 1]x1 + [2] >= [0 1 0]x1 + [1] = q2(0'(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 1] [1] [1 0 0] [0] 328.15/96.03 1'(q1(1(x1))) = [0 1 1]x1 + [2] >= [0 1 0]x1 + [1] = q2(1'(1'(x1))) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 1 0] [0] [1 1 0] [0] 328.15/96.03 q0(0(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [1] = 0'(q1(x1)) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 q0(1'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1'(q3(x1)) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 q2(0'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 0'(q0(x1)) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 328.15/96.03 [1 0 0] [0] [1 0 0] [0] 328.15/96.03 q3(b(x1)) = [0 1 1]x1 + [2] >= [0 0 0]x1 + [1] = b(q4(x1)) 328.15/96.03 [0 0 0] [0] [0 0 0] [0] 328.15/96.03 problem: 328.15/96.03 strict: 328.15/96.03 q1(0(x1)) -> 0(q1(x1)) 328.15/96.03 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.03 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.03 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.03 weak: 328.15/96.03 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.03 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.03 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.03 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.03 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.03 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.03 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.03 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.03 q3(b(x1)) -> b(q4(x1)) 328.15/96.03 Splitting Processor: 328.15/96.03 strict: 328.15/96.03 q1(0(x1)) -> 0(q1(x1)) 328.15/96.03 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.03 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.03 weak: 328.15/96.03 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.03 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.03 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.03 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.03 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.03 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.03 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.03 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.03 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.03 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.03 q3(b(x1)) -> b(q4(x1)) 328.15/96.03 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.03 Matrix Interpretation Processor: dim=2 328.15/96.03 328.15/96.03 max_matrix: 328.15/96.03 [1 1] 328.15/96.03 [0 1] 328.15/96.03 interpretation: 328.15/96.03 [1 0] 328.15/96.03 [q4](x0) = [0 0]x0, 328.15/96.03 328.15/96.03 [1 0] 328.15/96.03 [b](x0) = [0 0]x0, 328.15/96.03 328.15/96.03 328.15/96.03 [q3](x0) = x0, 328.15/96.03 328.15/96.03 [0] 328.15/96.03 [q2](x0) = x0 + [1], 328.15/96.03 328.15/96.03 [1 1] [1] 328.15/96.03 [1](x0) = [0 1]x0 + [2], 328.15/96.03 328.15/96.03 [1 1] 328.15/96.04 [1'](x0) = [0 1]x0, 328.15/96.04 328.15/96.04 328.15/96.04 [0'](x0) = x0, 328.15/96.04 328.15/96.04 328.15/96.04 [q1](x0) = x0, 328.15/96.04 328.15/96.04 328.15/96.04 [q0](x0) = x0, 328.15/96.04 328.15/96.04 328.15/96.04 [0](x0) = x0 328.15/96.04 orientation: 328.15/96.04 328.15/96.04 q1(0(x1)) = x1 >= x1 = 0(q1(x1)) 328.15/96.04 328.15/96.04 [1 1] [1] [1 1] [0] 328.15/96.04 1'(q2(0(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(0(x1))) 328.15/96.04 328.15/96.04 [1 2] [1] [1 2] [0] 328.15/96.04 1'(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(1'(1'(x1))) 328.15/96.04 328.15/96.04 [0] [0] 328.15/96.04 0(q2(0(x1))) = x1 + [1] >= x1 + [1] = q2(0(0(x1))) 328.15/96.04 328.15/96.04 [1 1] [0] [1 1] [0] 328.15/96.04 0(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0(1'(x1))) 328.15/96.04 328.15/96.04 [1 1] [1 1] 328.15/96.04 q3(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q3(x1)) 328.15/96.04 328.15/96.04 [0] [0] 328.15/96.04 0'(q2(0(x1))) = x1 + [1] >= x1 + [1] = q2(0'(0(x1))) 328.15/96.04 328.15/96.04 [1 1] [0] [1 1] [0] 328.15/96.04 0'(q2(1'(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = q2(0'(1'(x1))) 328.15/96.04 328.15/96.04 [1 1] [1] [1 1] [0] 328.15/96.04 0(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [1] = q2(0(1'(x1))) 328.15/96.04 328.15/96.04 [1 1] [1] [1 1] [0] 328.15/96.04 0'(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [1] = q2(0'(1'(x1))) 328.15/96.04 328.15/96.04 [1 2] [3] [1 2] [0] 328.15/96.04 1'(q1(1(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [1] = q2(1'(1'(x1))) 328.15/96.04 328.15/96.04 328.15/96.04 q0(0(x1)) = x1 >= x1 = 0'(q1(x1)) 328.15/96.04 328.15/96.04 [1 1] [1 1] 328.15/96.04 q0(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q3(x1)) 328.15/96.04 328.15/96.04 [0] 328.15/96.04 q2(0'(x1)) = x1 + [1] >= x1 = 0'(q0(x1)) 328.15/96.04 328.15/96.04 [1 0] [1 0] 328.15/96.04 q3(b(x1)) = [0 0]x1 >= [0 0]x1 = b(q4(x1)) 328.15/96.04 328.15/96.04 [1 1] [1 1] 328.15/96.04 q1(1'(x1)) = [0 1]x1 >= [0 1]x1 = 1'(q1(x1)) 328.15/96.04 problem: 328.15/96.04 strict: 328.15/96.04 q1(0(x1)) -> 0(q1(x1)) 328.15/96.04 weak: 328.15/96.04 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.04 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.04 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.04 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.04 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.04 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.04 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.04 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.04 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.04 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.04 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.04 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.04 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.04 q3(b(x1)) -> b(q4(x1)) 328.15/96.04 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.04 Matrix Interpretation Processor: dim=3 328.15/96.04 328.15/96.04 max_matrix: 328.15/96.04 [1 1 1] 328.15/96.04 [0 1 1] 328.15/96.04 [0 0 0] 328.15/96.04 interpretation: 328.15/96.04 [1 0 0] 328.15/96.04 [q4](x0) = [0 0 1]x0 328.15/96.04 [0 0 0] , 328.15/96.04 328.15/96.04 [1 0 0] [1] 328.15/96.04 [b](x0) = [0 0 0]x0 + [0] 328.15/96.04 [0 0 0] [0], 328.15/96.04 328.15/96.04 [1 1 0] 328.15/96.04 [q3](x0) = [0 0 0]x0 328.15/96.04 [0 0 0] , 328.15/96.04 328.15/96.04 [1 0 0] [0] 328.15/96.04 [q2](x0) = [0 1 0]x0 + [1] 328.15/96.04 [0 0 0] [0], 328.15/96.04 328.15/96.04 [1 0 1] [0] 328.15/96.04 [1](x0) = [0 1 1]x0 + [1] 328.15/96.04 [0 0 0] [0], 328.15/96.04 328.15/96.04 [1 1 0] [1] 328.15/96.04 [1'](x0) = [0 1 1]x0 + [0] 328.15/96.04 [0 0 0] [0], 328.15/96.04 328.15/96.04 [1 0 0] 328.15/96.04 [0'](x0) = [0 1 0]x0 328.15/96.04 [0 0 0] , 328.15/96.04 328.15/96.04 [1 1 0] 328.15/96.04 [q1](x0) = [0 1 0]x0 328.15/96.04 [0 0 0] , 328.15/96.04 328.15/96.04 [1 0 0] [0] 328.15/96.04 [q0](x0) = [0 1 0]x0 + [0] 328.15/96.04 [0 0 0] [1], 328.15/96.04 328.15/96.04 [1 1 0] [0] 328.15/96.04 [0](x0) = [0 1 1]x0 + [1] 328.15/96.04 [0 0 0] [0] 328.15/96.04 orientation: 328.15/96.04 [1 2 1] [1] [1 2 0] [0] 328.15/96.04 q1(0(x1)) = [0 1 1]x1 + [1] >= [0 1 0]x1 + [1] = 0(q1(x1)) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 1] [3] [1 2 1] [2] 328.15/96.04 1'(q2(0(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = q2(1'(0(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 1] [3] [1 2 1] [2] 328.15/96.04 1'(q2(1'(x1))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = q2(1'(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 1] [2] [1 2 1] [1] 328.15/96.04 0(q2(0(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(0(0(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 1] [2] [1 2 1] [1] 328.15/96.04 0(q2(1'(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = q2(0(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 1] [1] [1 1 0] [1] 328.15/96.04 q3(1'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1'(q3(x1)) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 1 0] [0] [1 1 0] [0] 328.15/96.04 0'(q2(0(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = q2(0'(0(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 1 0] [1] [1 1 0] [1] 328.15/96.04 0'(q2(1'(x1))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = q2(0'(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 3] [2] [1 2 1] [1] 328.15/96.04 0(q1(1(x1))) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [2] = q2(0(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 1 2] [1] [1 1 0] [1] 328.15/96.04 0'(q1(1(x1))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = q2(0'(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 2 3] [3] [1 2 1] [2] 328.15/96.04 1'(q1(1(x1))) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = q2(1'(1'(x1))) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 1 0] [0] [1 1 0] 328.15/96.04 q0(0(x1)) = [0 1 1]x1 + [1] >= [0 1 0]x1 = 0'(q1(x1)) 328.15/96.04 [0 0 0] [1] [0 0 0] 328.15/96.04 328.15/96.04 [1 1 0] [1] [1 1 0] [1] 328.15/96.04 q0(1'(x1)) = [0 1 1]x1 + [0] >= [0 0 0]x1 + [0] = 1'(q3(x1)) 328.15/96.04 [0 0 0] [1] [0 0 0] [0] 328.15/96.04 328.15/96.04 [1 0 0] [0] [1 0 0] 328.15/96.04 q2(0'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 = 0'(q0(x1)) 328.15/96.04 [0 0 0] [0] [0 0 0] 328.15/96.04 328.15/96.04 [1 0 0] [1] [1 0 0] [1] 328.15/96.04 q3(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(q4(x1)) 328.15/96.04 [0 0 0] [0] [0 0 0] [0] 328.15/96.05 328.15/96.05 [1 2 1] [1] [1 2 0] [1] 328.15/96.05 q1(1'(x1)) = [0 1 1]x1 + [0] >= [0 1 0]x1 + [0] = 1'(q1(x1)) 328.15/96.05 [0 0 0] [0] [0 0 0] [0] 328.15/96.05 problem: 328.15/96.05 strict: 328.15/96.05 328.15/96.05 weak: 328.15/96.05 q1(0(x1)) -> 0(q1(x1)) 328.15/96.05 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.05 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.05 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.05 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.05 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.05 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.05 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.05 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.05 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.05 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.05 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.05 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.05 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.05 q3(b(x1)) -> b(q4(x1)) 328.15/96.05 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.05 Qed 328.15/96.05 328.15/96.05 strict: 328.15/96.05 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.05 weak: 328.15/96.05 q1(0(x1)) -> 0(q1(x1)) 328.15/96.05 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.05 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.05 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.05 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.05 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.05 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.05 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.05 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.05 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.05 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.05 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.05 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.05 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.05 q3(b(x1)) -> b(q4(x1)) 328.15/96.05 Matrix Interpretation Processor: dim=3 328.15/96.05 328.15/96.05 max_matrix: 328.15/96.05 [1 0 1] 328.15/96.05 [0 0 1] 328.15/96.05 [0 0 1] 328.15/96.05 interpretation: 328.15/96.05 [1 0 1] 328.15/96.05 [q4](x0) = [0 0 1]x0 328.15/96.05 [0 0 0] , 328.15/96.05 328.15/96.05 [1 0 1] [0] 328.15/96.05 [b](x0) = [0 0 0]x0 + [1] 328.15/96.05 [0 0 1] [1], 328.15/96.05 328.15/96.05 [1 0 0] [1] 328.15/96.05 [q3](x0) = [0 0 0]x0 + [1] 328.15/96.05 [0 0 1] [1], 328.15/96.05 328.15/96.05 [1 0 0] [1] 328.15/96.05 [q2](x0) = [0 0 0]x0 + [0] 328.15/96.05 [0 0 1] [0], 328.15/96.05 328.15/96.05 [1 0 1] [1] 328.15/96.05 [1](x0) = [0 0 0]x0 + [0] 328.15/96.05 [0 0 1] [1], 328.15/96.05 328.15/96.05 [1 0 0] [0] 328.15/96.05 [1'](x0) = [0 0 0]x0 + [0] 328.15/96.05 [0 0 1] [1], 328.15/96.05 328.15/96.05 [1 0 0] [1] 328.15/96.05 [0'](x0) = [0 0 0]x0 + [0] 328.15/96.05 [0 0 0] [0], 328.15/96.05 328.15/96.05 [1 0 1] [0] 328.15/96.05 [q1](x0) = [0 0 0]x0 + [1] 328.15/96.05 [0 0 1] [0], 328.15/96.05 328.15/96.05 [1 0 0] [1] 328.15/96.05 [q0](x0) = [0 0 0]x0 + [0] 328.15/96.05 [0 0 1] [1], 328.15/96.05 328.15/96.05 [1 0 1] 328.15/96.05 [0](x0) = [0 0 0]x0 328.15/96.05 [0 0 1] 328.15/96.05 orientation: 328.15/96.05 [1 0 1] [1] [1 0 1] [0] 328.15/96.05 q1(1'(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1'(q1(x1)) 328.15/96.05 [0 0 1] [1] [0 0 1] [1] 328.15/96.05 328.15/96.05 [1 0 2] [0] [1 0 2] 328.15/96.05 q1(0(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = 0(q1(x1)) 328.15/96.05 [0 0 1] [0] [0 0 1] 328.15/96.05 328.15/96.05 [1 0 1] [1] [1 0 1] [1] 328.15/96.05 1'(q2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(1'(0(x1))) 328.15/96.05 [0 0 1] [1] [0 0 1] [1] 328.15/96.05 328.15/96.05 [1 0 0] [1] [1 0 0] [1] 328.15/96.05 1'(q2(1'(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(1'(1'(x1))) 328.15/96.05 [0 0 1] [2] [0 0 1] [2] 328.15/96.05 328.15/96.05 [1 0 2] [1] [1 0 2] [1] 328.15/96.05 0(q2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0(0(x1))) 328.15/96.06 [0 0 1] [0] [0 0 1] [0] 328.15/96.06 328.15/96.06 [1 0 1] [2] [1 0 1] [2] 328.15/96.06 0(q2(1'(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0(1'(x1))) 328.15/96.06 [0 0 1] [1] [0 0 1] [1] 328.15/96.06 328.15/96.06 [1 0 0] [1] [1 0 0] [1] 328.15/96.06 q3(1'(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = 1'(q3(x1)) 328.15/96.06 [0 0 1] [2] [0 0 1] [2] 328.15/96.06 328.15/96.06 [1 0 1] [2] [1 0 1] [2] 328.15/96.06 0'(q2(0(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(0(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 0] [2] [1 0 0] [2] 328.15/96.06 0'(q2(1'(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 3] [3] [1 0 1] [2] 328.15/96.06 0(q1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0(1'(x1))) 328.15/96.06 [0 0 1] [1] [0 0 1] [1] 328.15/96.06 328.15/96.06 [1 0 2] [3] [1 0 0] [2] 328.15/96.06 0'(q1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(0'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 2] [2] [1 0 0] [1] 328.15/96.06 1'(q1(1(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(1'(1'(x1))) 328.15/96.06 [0 0 1] [2] [0 0 1] [2] 328.15/96.06 328.15/96.06 [1 0 1] [1] [1 0 1] [1] 328.15/96.06 q0(0(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0'(q1(x1)) 328.15/96.06 [0 0 1] [1] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 0] [1] [1 0 0] [1] 328.15/96.06 q0(1'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1'(q3(x1)) 328.15/96.06 [0 0 1] [2] [0 0 1] [2] 328.15/96.06 328.15/96.06 [1 0 0] [2] [1 0 0] [2] 328.15/96.06 q2(0'(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 0'(q0(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 1] [1] [1 0 1] [0] 328.15/96.06 q3(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(q4(x1)) 328.15/96.06 [0 0 1] [2] [0 0 0] [1] 328.15/96.06 problem: 328.15/96.06 strict: 328.15/96.06 328.15/96.06 weak: 328.15/96.06 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.06 q1(0(x1)) -> 0(q1(x1)) 328.15/96.06 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.06 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.06 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.06 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.06 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.06 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.06 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.06 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.06 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.06 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.06 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.06 q3(b(x1)) -> b(q4(x1)) 328.15/96.06 Qed 328.15/96.06 328.15/96.06 strict: 328.15/96.06 q1(0(x1)) -> 0(q1(x1)) 328.15/96.06 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.06 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.06 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.06 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.06 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.06 weak: 328.15/96.06 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.06 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.06 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.06 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.06 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.06 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.06 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.06 q3(b(x1)) -> b(q4(x1)) 328.15/96.06 Matrix Interpretation Processor: dim=3 328.15/96.06 328.15/96.06 max_matrix: 328.15/96.06 [1 1 1] 328.15/96.06 [0 1 0] 328.15/96.06 [0 0 0] 328.15/96.06 interpretation: 328.15/96.06 [1 0 0] 328.15/96.06 [q4](x0) = [0 0 0]x0 328.15/96.06 [0 0 0] , 328.15/96.06 328.15/96.06 [1 0 0] [0] 328.15/96.06 [b](x0) = [0 0 0]x0 + [1] 328.15/96.06 [0 0 0] [0], 328.15/96.06 328.15/96.06 [1 1 1] 328.15/96.06 [q3](x0) = [0 1 0]x0 328.15/96.06 [0 0 0] , 328.15/96.06 328.15/96.06 [1 1 0] [0] 328.15/96.06 [q2](x0) = [0 1 0]x0 + [1] 328.15/96.06 [0 0 0] [0], 328.15/96.06 328.15/96.06 [1 1 1] [0] 328.15/96.06 [1](x0) = [0 1 0]x0 + [1] 328.15/96.06 [0 0 0] [0], 328.15/96.06 328.15/96.06 [1 1 1] [0] 328.15/96.06 [1'](x0) = [0 1 0]x0 + [1] 328.15/96.06 [0 0 0] [0], 328.15/96.06 328.15/96.06 [1 0 0] 328.15/96.06 [0'](x0) = [0 1 0]x0 328.15/96.06 [0 0 0] , 328.15/96.06 328.15/96.06 [1 1 0] [0] 328.15/96.06 [q1](x0) = [0 1 0]x0 + [1] 328.15/96.06 [0 0 0] [0], 328.15/96.06 328.15/96.06 [1 1 0] [0] 328.15/96.06 [q0](x0) = [0 1 0]x0 + [1] 328.15/96.06 [0 0 0] [1], 328.15/96.06 328.15/96.06 [1 0 1] 328.15/96.06 [0](x0) = [0 1 0]x0 328.15/96.06 [0 0 0] 328.15/96.06 orientation: 328.15/96.06 [1 2 1] [1] [1 2 1] [0] 328.15/96.06 q3(1'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 1'(q3(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 1 1] [0] [1 1 1] [0] 328.15/96.06 0'(q2(0(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = q2(0'(0(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [1] 328.15/96.06 0'(q2(1'(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [1] 328.15/96.06 0(q1(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [1] 328.15/96.06 0'(q1(1(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 3 1] [3] [1 3 1] [3] 328.15/96.06 1'(q1(1(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(1'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 1 1] [0] [1 1 0] [0] 328.15/96.06 q0(0(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 0'(q1(x1)) 328.15/96.06 [0 0 0] [1] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [0] 328.15/96.06 q0(1'(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [1] = 1'(q3(x1)) 328.15/96.06 [0 0 0] [1] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 1 0] [0] [1 1 0] [0] 328.15/96.06 q2(0'(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 0'(q0(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 0 0] [1] [1 0 0] [0] 328.15/96.06 q3(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = b(q4(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 1 1] [0] [1 1 0] [0] 328.15/96.06 q1(0(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = 0(q1(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 0] [1] 328.15/96.06 q1(1'(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = 1'(q1(x1)) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 1 1] [0] [1 1 1] [0] 328.15/96.06 0(q2(0(x1))) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = q2(0(0(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [1] 328.15/96.06 1'(q2(0(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(1'(0(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 2 1] [1] [1 2 1] [1] 328.15/96.06 0(q2(1'(x1))) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = q2(0(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 328.15/96.06 [1 3 1] [3] [1 3 1] [3] 328.15/96.06 1'(q2(1'(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(1'(1'(x1))) 328.15/96.06 [0 0 0] [0] [0 0 0] [0] 328.15/96.06 problem: 328.15/96.06 strict: 328.15/96.06 328.15/96.06 weak: 328.15/96.06 q3(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 0'(q2(0(x1))) -> q2(0'(0(x1))) 328.15/96.06 0'(q2(1'(x1))) -> q2(0'(1'(x1))) 328.15/96.06 0(q1(1(x1))) -> q2(0(1'(x1))) 328.15/96.06 0'(q1(1(x1))) -> q2(0'(1'(x1))) 328.15/96.06 1'(q1(1(x1))) -> q2(1'(1'(x1))) 328.15/96.06 q0(0(x1)) -> 0'(q1(x1)) 328.15/96.06 q0(1'(x1)) -> 1'(q3(x1)) 328.15/96.06 q2(0'(x1)) -> 0'(q0(x1)) 328.15/96.06 q3(b(x1)) -> b(q4(x1)) 328.15/96.06 q1(0(x1)) -> 0(q1(x1)) 328.15/96.06 q1(1'(x1)) -> 1'(q1(x1)) 328.15/96.06 0(q2(0(x1))) -> q2(0(0(x1))) 328.15/96.06 1'(q2(0(x1))) -> q2(1'(0(x1))) 328.15/96.06 0(q2(1'(x1))) -> q2(0(1'(x1))) 328.15/96.06 1'(q2(1'(x1))) -> q2(1'(1'(x1))) 328.15/96.06 Qed 328.15/96.07 EOF