YES(?,O(n^2)) 1169.13/295.71 YES(?,O(n^2)) 1169.13/295.72 1169.13/295.72 Problem: 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 1169.13/295.72 Proof: 1169.13/295.72 Complexity Transformation Processor: 1169.13/295.72 strict: 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 weak: 1169.13/295.72 1169.13/295.72 Matrix Interpretation Processor: dim=1 1169.13/295.72 1169.13/295.72 max_matrix: 1169.13/295.72 1 1169.13/295.72 interpretation: 1169.13/295.72 [q4](x0) = x0 + 9, 1169.13/295.72 1169.13/295.72 [bl](x0) = x0 + 5, 1169.13/295.72 1169.13/295.72 [q3](x0) = x0 + 10, 1169.13/295.72 1169.13/295.72 [q2](x0) = x0, 1169.13/295.72 1169.13/295.72 [b](x0) = x0, 1169.13/295.72 1169.13/295.72 [y](x0) = x0 + 4, 1169.13/295.72 1169.13/295.72 [x](x0) = x0 + 14, 1169.13/295.72 1169.13/295.72 [q1](x0) = x0, 1169.13/295.72 1169.13/295.72 [q0](x0) = x0 + 2, 1169.13/295.72 1169.13/295.72 [a](x0) = x0 + 8 1169.13/295.72 orientation: 1169.13/295.72 q0(a(x1)) = x1 + 10 >= x1 + 14 = x(q1(x1)) 1169.13/295.72 1169.13/295.72 q1(a(x1)) = x1 + 8 >= x1 + 8 = a(q1(x1)) 1169.13/295.72 1169.13/295.72 q1(y(x1)) = x1 + 4 >= x1 + 4 = y(q1(x1)) 1169.13/295.72 1169.13/295.72 a(q1(b(x1))) = x1 + 8 >= x1 + 12 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 a(q2(a(x1))) = x1 + 16 >= x1 + 16 = q2(a(a(x1))) 1169.13/295.72 1169.13/295.72 a(q2(y(x1))) = x1 + 12 >= x1 + 12 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 y(q1(b(x1))) = x1 + 4 >= x1 + 8 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 y(q2(a(x1))) = x1 + 12 >= x1 + 12 = q2(y(a(x1))) 1169.13/295.72 1169.13/295.72 y(q2(y(x1))) = x1 + 8 >= x1 + 8 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 q2(x(x1)) = x1 + 14 >= x1 + 16 = x(q0(x1)) 1169.13/295.72 1169.13/295.72 q0(y(x1)) = x1 + 6 >= x1 + 14 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q3(y(x1)) = x1 + 14 >= x1 + 14 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q3(bl(x1)) = x1 + 15 >= x1 + 14 = bl(q4(x1)) 1169.13/295.72 problem: 1169.13/295.72 strict: 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 weak: 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 Matrix Interpretation Processor: dim=1 1169.13/295.72 1169.13/295.72 max_matrix: 1169.13/295.72 1 1169.13/295.72 interpretation: 1169.13/295.72 [q4](x0) = x0 + 65, 1169.13/295.72 1169.13/295.72 [bl](x0) = x0 + 12, 1169.13/295.72 1169.13/295.72 [q3](x0) = x0 + 128, 1169.13/295.72 1169.13/295.72 [q2](x0) = x0 + 2, 1169.13/295.72 1169.13/295.72 [b](x0) = x0 + 64, 1169.13/295.72 1169.13/295.72 [y](x0) = x0 + 5, 1169.13/295.72 1169.13/295.72 [x](x0) = x0 + 24, 1169.13/295.72 1169.13/295.72 [q1](x0) = x0 + 48, 1169.13/295.72 1169.13/295.72 [q0](x0) = x0 + 194, 1169.13/295.72 1169.13/295.72 [a](x0) = x0 + 81 1169.13/295.72 orientation: 1169.13/295.72 q0(a(x1)) = x1 + 275 >= x1 + 72 = x(q1(x1)) 1169.13/295.72 1169.13/295.72 q1(a(x1)) = x1 + 129 >= x1 + 129 = a(q1(x1)) 1169.13/295.72 1169.13/295.72 q1(y(x1)) = x1 + 53 >= x1 + 53 = y(q1(x1)) 1169.13/295.72 1169.13/295.72 a(q1(b(x1))) = x1 + 193 >= x1 + 88 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 a(q2(a(x1))) = x1 + 164 >= x1 + 164 = q2(a(a(x1))) 1169.13/295.72 1169.13/295.72 a(q2(y(x1))) = x1 + 88 >= x1 + 88 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 y(q1(b(x1))) = x1 + 117 >= x1 + 12 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 y(q2(a(x1))) = x1 + 88 >= x1 + 88 = q2(y(a(x1))) 1169.13/295.72 1169.13/295.72 y(q2(y(x1))) = x1 + 12 >= x1 + 12 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 q2(x(x1)) = x1 + 26 >= x1 + 218 = x(q0(x1)) 1169.13/295.72 1169.13/295.72 q0(y(x1)) = x1 + 199 >= x1 + 133 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q3(y(x1)) = x1 + 133 >= x1 + 133 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q3(bl(x1)) = x1 + 140 >= x1 + 77 = bl(q4(x1)) 1169.13/295.72 problem: 1169.13/295.72 strict: 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 weak: 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 Matrix Interpretation Processor: dim=1 1169.13/295.72 1169.13/295.72 max_matrix: 1169.13/295.72 1 1169.13/295.72 interpretation: 1169.13/295.72 [q4](x0) = x0, 1169.13/295.72 1169.13/295.72 [bl](x0) = x0, 1169.13/295.72 1169.13/295.72 [q3](x0) = x0 + 8, 1169.13/295.72 1169.13/295.72 [q2](x0) = x0 + 9, 1169.13/295.72 1169.13/295.72 [b](x0) = x0 + 8, 1169.13/295.72 1169.13/295.72 [y](x0) = x0 + 1, 1169.13/295.72 1169.13/295.72 [x](x0) = x0, 1169.13/295.72 1169.13/295.72 [q1](x0) = x0 + 9, 1169.13/295.72 1169.13/295.72 [q0](x0) = x0 + 8, 1169.13/295.72 1169.13/295.72 [a](x0) = x0 + 3 1169.13/295.72 orientation: 1169.13/295.72 q1(a(x1)) = x1 + 12 >= x1 + 12 = a(q1(x1)) 1169.13/295.72 1169.13/295.72 q1(y(x1)) = x1 + 10 >= x1 + 10 = y(q1(x1)) 1169.13/295.72 1169.13/295.72 a(q2(a(x1))) = x1 + 15 >= x1 + 15 = q2(a(a(x1))) 1169.13/295.72 1169.13/295.72 a(q2(y(x1))) = x1 + 13 >= x1 + 13 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 y(q2(a(x1))) = x1 + 13 >= x1 + 13 = q2(y(a(x1))) 1169.13/295.72 1169.13/295.72 y(q2(y(x1))) = x1 + 11 >= x1 + 11 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 q2(x(x1)) = x1 + 9 >= x1 + 8 = x(q0(x1)) 1169.13/295.72 1169.13/295.72 q3(y(x1)) = x1 + 9 >= x1 + 9 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q0(a(x1)) = x1 + 11 >= x1 + 9 = x(q1(x1)) 1169.13/295.72 1169.13/295.72 a(q1(b(x1))) = x1 + 20 >= x1 + 13 = q2(a(y(x1))) 1169.13/295.72 1169.13/295.72 y(q1(b(x1))) = x1 + 18 >= x1 + 11 = q2(y(y(x1))) 1169.13/295.72 1169.13/295.72 q0(y(x1)) = x1 + 9 >= x1 + 9 = y(q3(x1)) 1169.13/295.72 1169.13/295.72 q3(bl(x1)) = x1 + 8 >= x1 = bl(q4(x1)) 1169.13/295.72 problem: 1169.13/295.72 strict: 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 weak: 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 Splitting Processor: 1169.13/295.72 strict: 1169.13/295.72 q1(a(x1)) -> a(q1(x1)) 1169.13/295.72 weak: 1169.13/295.72 q2(x(x1)) -> x(q0(x1)) 1169.13/295.72 q0(a(x1)) -> x(q1(x1)) 1169.13/295.72 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.72 q0(y(x1)) -> y(q3(x1)) 1169.13/295.72 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.72 q1(y(x1)) -> y(q1(x1)) 1169.13/295.72 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.72 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.72 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.72 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.72 q3(y(x1)) -> y(q3(x1)) 1169.13/295.72 Matrix Interpretation Processor: dim=3 1169.13/295.72 1169.13/295.72 max_matrix: 1169.13/295.72 [1 1 1] 1169.13/295.72 [0 0 1] 1169.13/295.72 [0 0 1] 1169.13/295.72 interpretation: 1169.13/295.72 [1 1 1] 1169.13/295.72 [q4](x0) = [0 0 0]x0 1169.13/295.72 [0 0 0] , 1169.13/295.72 1169.13/295.72 [1 1 1] 1169.13/295.72 [bl](x0) = [0 0 1]x0 1169.13/295.72 [0 0 1] , 1169.13/295.72 1169.13/295.72 [1 0 0] 1169.13/295.72 [q3](x0) = [0 0 0]x0 1169.13/295.72 [0 0 0] , 1169.13/295.72 1169.13/295.72 [1 1 0] 1169.13/295.72 [q2](x0) = [0 0 0]x0 1169.13/295.72 [0 0 0] , 1169.13/295.72 1169.13/295.72 [1 1 1] [0] 1169.13/295.72 [b](x0) = [0 0 1]x0 + [0] 1169.13/295.72 [0 0 0] [1], 1169.13/295.72 1169.13/295.72 [1 0 0] 1169.13/295.72 [y](x0) = [0 0 0]x0 1169.13/295.72 [0 0 1] , 1169.13/295.72 1169.13/295.72 [1 0 0] 1169.13/295.72 [x](x0) = [0 0 1]x0 1169.13/295.72 [0 0 0] , 1169.13/295.72 1169.13/295.72 [1 0 1] 1169.13/295.72 [q1](x0) = [0 0 1]x0 1169.13/295.72 [0 0 1] , 1169.13/295.72 1169.13/295.72 [1 0 1] 1169.13/295.72 [q0](x0) = [0 0 1]x0 1169.13/295.72 [0 0 0] , 1169.13/295.72 1169.13/295.72 [1 0 0] [0] 1169.13/295.72 [a](x0) = [0 0 0]x0 + [0] 1169.13/295.72 [0 0 1] [1] 1169.13/295.72 orientation: 1169.13/295.72 [1 0 1] [1] [1 0 1] [0] 1169.13/295.72 q1(a(x1)) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = a(q1(x1)) 1169.13/295.72 [0 0 1] [1] [0 0 1] [1] 1169.13/295.72 1169.13/295.72 [1 0 1] [1 0 1] 1169.13/295.72 q2(x(x1)) = [0 0 0]x1 >= [0 0 0]x1 = x(q0(x1)) 1169.13/295.72 [0 0 0] [0 0 0] 1169.13/295.72 1169.13/295.72 [1 0 1] [1] [1 0 1] 1169.13/295.72 q0(a(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 = x(q1(x1)) 1169.13/295.72 [0 0 0] [0] [0 0 0] 1169.13/295.72 1169.13/295.72 [1 1 1] [1] [1 0 0] 1169.13/295.72 a(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = q2(a(y(x1))) 1169.13/295.72 [0 0 0] [2] [0 0 0] 1169.13/295.72 1169.13/295.72 [1 1 1] [1] [1 0 0] 1169.13/295.72 y(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = q2(y(y(x1))) 1169.13/295.72 [0 0 0] [1] [0 0 0] 1169.13/295.72 1169.13/295.72 [1 0 1] [1 0 0] 1169.13/295.73 q0(y(x1)) = [0 0 1]x1 >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.73 [0 0 0] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 1 1] [1 1 1] 1169.13/295.73 q3(bl(x1)) = [0 0 0]x1 >= [0 0 0]x1 = bl(q4(x1)) 1169.13/295.73 [0 0 0] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 0 1] [1 0 1] 1169.13/295.73 q1(y(x1)) = [0 0 1]x1 >= [0 0 0]x1 = y(q1(x1)) 1169.13/295.73 [0 0 1] [0 0 1] 1169.13/295.73 1169.13/295.73 [1 0 0] [0] [1 0 0] 1169.13/295.73 a(q2(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = q2(a(a(x1))) 1169.13/295.73 [0 0 0] [1] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 0 0] [0] [1 0 0] 1169.13/295.73 a(q2(y(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 = q2(a(y(x1))) 1169.13/295.73 [0 0 0] [1] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 0 0] [1 0 0] 1169.13/295.73 y(q2(a(x1))) = [0 0 0]x1 >= [0 0 0]x1 = q2(y(a(x1))) 1169.13/295.73 [0 0 0] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 0 0] [1 0 0] 1169.13/295.73 y(q2(y(x1))) = [0 0 0]x1 >= [0 0 0]x1 = q2(y(y(x1))) 1169.13/295.73 [0 0 0] [0 0 0] 1169.13/295.73 1169.13/295.73 [1 0 0] [1 0 0] 1169.13/295.73 q3(y(x1)) = [0 0 0]x1 >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.73 [0 0 0] [0 0 0] 1169.13/295.73 problem: 1169.13/295.73 strict: 1169.13/295.73 1169.13/295.73 weak: 1169.13/295.73 q1(a(x1)) -> a(q1(x1)) 1169.13/295.73 q2(x(x1)) -> x(q0(x1)) 1169.13/295.73 q0(a(x1)) -> x(q1(x1)) 1169.13/295.73 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.73 q0(y(x1)) -> y(q3(x1)) 1169.13/295.73 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.73 q1(y(x1)) -> y(q1(x1)) 1169.13/295.73 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.73 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.73 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.73 q3(y(x1)) -> y(q3(x1)) 1169.13/295.73 Qed 1169.13/295.73 1169.13/295.73 strict: 1169.13/295.73 q1(y(x1)) -> y(q1(x1)) 1169.13/295.73 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.73 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.73 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.73 q3(y(x1)) -> y(q3(x1)) 1169.13/295.73 weak: 1169.13/295.73 q1(a(x1)) -> a(q1(x1)) 1169.13/295.73 q2(x(x1)) -> x(q0(x1)) 1169.13/295.73 q0(a(x1)) -> x(q1(x1)) 1169.13/295.73 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.73 q0(y(x1)) -> y(q3(x1)) 1169.13/295.73 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.73 Splitting Processor: 1169.13/295.73 strict: 1169.13/295.73 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.73 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.73 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.73 weak: 1169.13/295.73 q1(a(x1)) -> a(q1(x1)) 1169.13/295.73 q2(x(x1)) -> x(q0(x1)) 1169.13/295.73 q0(a(x1)) -> x(q1(x1)) 1169.13/295.73 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.73 q0(y(x1)) -> y(q3(x1)) 1169.13/295.73 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.73 q1(y(x1)) -> y(q1(x1)) 1169.13/295.73 q3(y(x1)) -> y(q3(x1)) 1169.13/295.73 Splitting Processor: 1169.13/295.73 strict: 1169.13/295.73 q1(y(x1)) -> y(q1(x1)) 1169.13/295.73 weak: 1169.13/295.73 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.73 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.73 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.73 q1(a(x1)) -> a(q1(x1)) 1169.13/295.73 q2(x(x1)) -> x(q0(x1)) 1169.13/295.73 q0(a(x1)) -> x(q1(x1)) 1169.13/295.73 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.73 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.73 q0(y(x1)) -> y(q3(x1)) 1169.13/295.73 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.73 q3(y(x1)) -> y(q3(x1)) 1169.13/295.73 Matrix Interpretation Processor: dim=3 1169.13/295.73 1169.13/295.73 max_matrix: 1169.13/295.73 [1 1 1] 1169.13/295.73 [0 0 1] 1169.13/295.73 [0 0 1] 1169.13/295.73 interpretation: 1169.13/295.73 [1 0 0] 1169.13/295.73 [q4](x0) = [0 0 0]x0 1169.13/295.73 [0 0 0] , 1169.13/295.73 1169.13/295.73 [1 0 0] 1169.13/295.73 [bl](x0) = [0 0 0]x0 1169.13/295.73 [0 0 0] , 1169.13/295.73 1169.13/295.73 [1 0 0] [1] 1169.13/295.73 [q3](x0) = [0 0 1]x0 + [0] 1169.13/295.73 [0 0 1] [0], 1169.13/295.73 1169.13/295.73 [1 0 0] [1] 1169.13/295.73 [q2](x0) = [0 0 0]x0 + [0] 1169.13/295.73 [0 0 1] [0], 1169.13/295.73 1169.13/295.73 [1 0 1] [0] 1169.13/295.73 [b](x0) = [0 0 0]x0 + [0] 1169.13/295.74 [0 0 1] [1], 1169.13/295.74 1169.13/295.74 [1 0 0] [0] 1169.13/295.74 [y](x0) = [0 0 0]x0 + [0] 1169.13/295.74 [0 0 1] [1], 1169.13/295.74 1169.13/295.74 [1 0 0] 1169.13/295.74 [x](x0) = [0 0 0]x0 1169.13/295.74 [0 0 0] , 1169.13/295.74 1169.13/295.74 [1 0 1] 1169.13/295.74 [q1](x0) = [0 0 0]x0 1169.13/295.74 [0 0 1] , 1169.13/295.74 1169.13/295.74 [1 0 0] [1] 1169.13/295.74 [q0](x0) = [0 0 0]x0 + [0] 1169.13/295.74 [0 0 1] [0], 1169.13/295.74 1169.13/295.74 [1 1 1] [1] 1169.13/295.74 [a](x0) = [0 0 0]x0 + [0] 1169.13/295.74 [0 0 1] [0] 1169.13/295.74 orientation: 1169.13/295.74 [1 0 1] [1] [1 0 1] [0] 1169.13/295.74 q1(y(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = y(q1(x1)) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 1169.13/295.74 [1 1 2] [3] [1 1 2] [3] 1169.13/295.74 a(q2(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(a(a(x1))) 1169.13/295.74 [0 0 1] [0] [0 0 1] [0] 1169.13/295.74 1169.13/295.74 [1 0 1] [3] [1 0 1] [3] 1169.13/295.74 a(q2(y(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 1169.13/295.74 [1 1 1] [2] [1 1 1] [2] 1169.13/295.74 y(q2(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(a(x1))) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 1169.13/295.74 [1 0 0] [1] [1 0 0] [1] 1169.13/295.74 y(q2(y(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.74 [0 0 1] [2] [0 0 1] [2] 1169.13/295.74 1169.13/295.74 [1 1 2] [1] [1 0 2] [1] 1169.13/295.74 q1(a(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(q1(x1)) 1169.13/295.74 [0 0 1] [0] [0 0 1] [0] 1169.13/295.74 1169.13/295.74 [1 0 0] [1] [1 0 0] [1] 1169.13/295.74 q2(x(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = x(q0(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 1 1] [2] [1 0 1] 1169.13/295.74 q0(a(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = x(q1(x1)) 1169.13/295.74 [0 0 1] [0] [0 0 0] 1169.13/295.74 1169.13/295.74 [1 0 3] [3] [1 0 1] [3] 1169.13/295.74 a(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 1169.13/295.74 [1 0 2] [1] [1 0 0] [1] 1169.13/295.74 y(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.74 [0 0 1] [2] [0 0 1] [2] 1169.13/295.74 1169.13/295.74 [1 0 0] [1] [1 0 0] [1] 1169.13/295.74 q0(y(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = y(q3(x1)) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 1169.13/295.74 [1 0 0] [1] [1 0 0] 1169.13/295.74 q3(bl(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = bl(q4(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] 1169.13/295.74 1169.13/295.74 [1 0 0] [1] [1 0 0] [1] 1169.13/295.74 q3(y(x1)) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = y(q3(x1)) 1169.13/295.74 [0 0 1] [1] [0 0 1] [1] 1169.13/295.74 problem: 1169.13/295.74 strict: 1169.13/295.74 1169.13/295.74 weak: 1169.13/295.74 q1(y(x1)) -> y(q1(x1)) 1169.13/295.74 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.74 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.74 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.74 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.74 q1(a(x1)) -> a(q1(x1)) 1169.13/295.74 q2(x(x1)) -> x(q0(x1)) 1169.13/295.74 q0(a(x1)) -> x(q1(x1)) 1169.13/295.74 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.74 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.74 q0(y(x1)) -> y(q3(x1)) 1169.13/295.74 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.74 q3(y(x1)) -> y(q3(x1)) 1169.13/295.74 Qed 1169.13/295.74 1169.13/295.74 strict: 1169.13/295.74 q3(y(x1)) -> y(q3(x1)) 1169.13/295.74 weak: 1169.13/295.74 q1(y(x1)) -> y(q1(x1)) 1169.13/295.74 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.74 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.74 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.74 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.74 q1(a(x1)) -> a(q1(x1)) 1169.13/295.74 q2(x(x1)) -> x(q0(x1)) 1169.13/295.74 q0(a(x1)) -> x(q1(x1)) 1169.13/295.74 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.74 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.74 q0(y(x1)) -> y(q3(x1)) 1169.13/295.74 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.74 Matrix Interpretation Processor: dim=3 1169.13/295.74 1169.13/295.74 max_matrix: 1169.13/295.74 [1 1 1] 1169.13/295.74 [0 1 1] 1169.13/295.74 [0 0 0] 1169.13/295.74 interpretation: 1169.13/295.74 [1 0 0] 1169.13/295.74 [q4](x0) = [0 0 0]x0 1169.13/295.74 [0 0 0] , 1169.13/295.74 1169.13/295.74 [1 0 0] [0] 1169.13/295.74 [bl](x0) = [0 0 0]x0 + [1] 1169.13/295.74 [0 0 0] [0], 1169.13/295.74 1169.13/295.74 [1 1 0] 1169.13/295.74 [q3](x0) = [0 1 0]x0 1169.13/295.74 [0 0 0] , 1169.13/295.74 1169.13/295.74 [1 1 0] [0] 1169.13/295.74 [q2](x0) = [0 1 0]x0 + [1] 1169.13/295.74 [0 0 0] [0], 1169.13/295.74 1169.13/295.74 [1 1 0] [0] 1169.13/295.74 [b](x0) = [0 1 1]x0 + [1] 1169.13/295.74 [0 0 0] [1], 1169.13/295.74 1169.13/295.74 [1 1 0] [0] 1169.13/295.74 [y](x0) = [0 1 1]x0 + [1] 1169.13/295.74 [0 0 0] [0], 1169.13/295.74 1169.13/295.74 [1 0 0] [1] 1169.13/295.74 [x](x0) = [0 1 0]x0 + [1] 1169.13/295.74 [0 0 0] [0], 1169.13/295.74 1169.13/295.74 [1 1 0] 1169.13/295.74 [q1](x0) = [0 1 1]x0 1169.13/295.74 [0 0 0] , 1169.13/295.74 1169.13/295.74 [1 1 0] [0] 1169.13/295.74 [q0](x0) = [0 1 0]x0 + [1] 1169.13/295.74 [0 0 0] [1], 1169.13/295.74 1169.13/295.74 [1 1 1] [0] 1169.13/295.74 [a](x0) = [0 1 1]x0 + [1] 1169.13/295.74 [0 0 0] [0] 1169.13/295.74 orientation: 1169.13/295.74 [1 2 1] [1] [1 2 0] [0] 1169.13/295.74 q3(y(x1)) = [0 1 1]x1 + [1] >= [0 1 0]x1 + [1] = y(q3(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 2 1] [1] [1 2 1] [0] 1169.13/295.74 q1(y(x1)) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = y(q1(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 3 3] [3] [1 3 3] [3] 1169.13/295.74 a(q2(a(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(a(a(x1))) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 3 2] [3] [1 3 2] [3] 1169.13/295.74 a(q2(y(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(a(y(x1))) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 3 3] [3] [1 3 3] [3] 1169.13/295.74 y(q2(a(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(y(a(x1))) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 3 2] [3] [1 3 2] [3] 1169.13/295.74 y(q2(y(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(y(y(x1))) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 2 2] [1] [1 2 1] [0] 1169.13/295.74 q1(a(x1)) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = a(q1(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 1 0] [2] [1 1 0] [1] 1169.13/295.74 q2(x(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = x(q0(x1)) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 2 2] [1] [1 1 0] [1] 1169.13/295.74 q0(a(x1)) = [0 1 1]x1 + [2] >= [0 1 1]x1 + [1] = x(q1(x1)) 1169.13/295.74 [0 0 0] [1] [0 0 0] [0] 1169.13/295.74 1169.13/295.74 [1 3 2] [3] [1 3 2] [3] 1169.13/295.74 a(q1(b(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(a(y(x1))) 1169.13/295.74 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 3 2] [3] [1 3 2] [3] 1169.13/295.75 y(q1(b(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = q2(y(y(x1))) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 2 1] [1] [1 2 0] [0] 1169.13/295.75 q0(y(x1)) = [0 1 1]x1 + [2] >= [0 1 0]x1 + [1] = y(q3(x1)) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 0 0] [1] [1 0 0] [0] 1169.13/295.75 q3(bl(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = bl(q4(x1)) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 problem: 1169.13/295.75 strict: 1169.13/295.75 1169.13/295.75 weak: 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 Qed 1169.13/295.75 1169.13/295.75 strict: 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.75 weak: 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 Splitting Processor: 1169.13/295.75 strict: 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 weak: 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 Splitting Processor: 1169.13/295.75 strict: 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 weak: 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 Matrix Interpretation Processor: dim=3 1169.13/295.75 1169.13/295.75 max_matrix: 1169.13/295.75 [1 1 1] 1169.13/295.75 [0 1 1] 1169.13/295.75 [0 0 0] 1169.13/295.75 interpretation: 1169.13/295.75 [1 0 0] 1169.13/295.75 [q4](x0) = [0 0 1]x0 1169.13/295.75 [0 0 0] , 1169.13/295.75 1169.13/295.75 [1 0 1] 1169.13/295.75 [bl](x0) = [0 0 0]x0 1169.13/295.75 [0 0 0] , 1169.13/295.75 1169.13/295.75 [1 0 0] [0] 1169.13/295.75 [q3](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [0], 1169.13/295.75 1169.13/295.75 [1 0 1] [0] 1169.13/295.75 [q2](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [0], 1169.13/295.75 1169.13/295.75 [1 0 0] [0] 1169.13/295.75 [b](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [0], 1169.13/295.75 1169.13/295.75 [1 0 0] [0] 1169.13/295.75 [y](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [0], 1169.13/295.75 1169.13/295.75 [1 0 0] 1169.13/295.75 [x](x0) = [0 1 0]x0 1169.13/295.75 [0 0 0] , 1169.13/295.75 1169.13/295.75 [1 1 0] [0] 1169.13/295.75 [q1](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [1], 1169.13/295.75 1169.13/295.75 [1 0 0] [0] 1169.13/295.75 [q0](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [1], 1169.13/295.75 1169.13/295.75 [1 1 0] [0] 1169.13/295.75 [a](x0) = [0 1 0]x0 + [1] 1169.13/295.75 [0 0 0] [1] 1169.13/295.75 orientation: 1169.13/295.75 [1 1 0] [1] [1 1 0] [0] 1169.13/295.75 y(q2(a(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(y(a(x1))) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 2 0] [3] [1 2 0] [2] 1169.13/295.75 a(q2(a(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(a(a(x1))) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 1 0] [2] [1 1 0] [2] 1169.13/295.75 a(q2(y(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(a(y(x1))) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 2 0] [1] [1 2 0] [1] 1169.13/295.75 q1(a(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = a(q1(x1)) 1169.13/295.75 [0 0 0] [1] [0 0 0] [1] 1169.13/295.75 1169.13/295.75 [1 0 0] [0] [1 0 0] [0] 1169.13/295.75 q2(x(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = x(q0(x1)) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 1 0] [0] [1 1 0] [0] 1169.13/295.75 q0(a(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [1] = x(q1(x1)) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 2 0] [3] [1 1 0] [2] 1169.13/295.75 a(q1(b(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(a(y(x1))) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 1 0] [1] [1 0 0] [0] 1169.13/295.75 y(q1(b(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(y(y(x1))) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 0 0] [0] [1 0 0] [0] 1169.13/295.75 q0(y(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = y(q3(x1)) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 0 1] [0] [1 0 0] 1169.13/295.75 q3(bl(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = bl(q4(x1)) 1169.13/295.75 [0 0 0] [0] [0 0 0] 1169.13/295.75 1169.13/295.75 [1 1 0] [1] [1 1 0] [0] 1169.13/295.75 q1(y(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = y(q1(x1)) 1169.13/295.75 [0 0 0] [1] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 0 0] [0] [1 0 0] [0] 1169.13/295.75 q3(y(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = y(q3(x1)) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 1169.13/295.75 [1 0 0] [0] [1 0 0] [0] 1169.13/295.75 y(q2(y(x1))) = [0 1 0]x1 + [3] >= [0 1 0]x1 + [3] = q2(y(y(x1))) 1169.13/295.75 [0 0 0] [0] [0 0 0] [0] 1169.13/295.75 problem: 1169.13/295.75 strict: 1169.13/295.75 1169.13/295.75 weak: 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 Qed 1169.13/295.75 1169.13/295.75 strict: 1169.13/295.75 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.75 weak: 1169.13/295.75 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.75 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.75 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.75 q1(a(x1)) -> a(q1(x1)) 1169.13/295.75 q2(x(x1)) -> x(q0(x1)) 1169.13/295.75 q0(a(x1)) -> x(q1(x1)) 1169.13/295.75 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.75 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.75 q0(y(x1)) -> y(q3(x1)) 1169.13/295.75 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.75 q1(y(x1)) -> y(q1(x1)) 1169.13/295.75 q3(y(x1)) -> y(q3(x1)) 1169.13/295.76 Matrix Interpretation Processor: dim=3 1169.13/295.76 1169.13/295.76 max_matrix: 1169.13/295.76 [1 1 1] 1169.13/295.76 [0 0 1] 1169.13/295.76 [0 0 1] 1169.13/295.76 interpretation: 1169.13/295.76 [1 0 0] 1169.13/295.76 [q4](x0) = [0 0 0]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 1 0] [0] 1169.13/295.76 [bl](x0) = [0 0 0]x0 + [0] 1169.13/295.76 [0 0 0] [1], 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [q3](x0) = [0 0 0]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 0 1] [0] 1169.13/295.76 [q2](x0) = [0 0 0]x0 + [0] 1169.13/295.76 [0 0 1] [1], 1169.13/295.76 1169.13/295.76 [1 0 1] [1] 1169.13/295.76 [b](x0) = [0 0 1]x0 + [0] 1169.13/295.76 [0 0 1] [1], 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [y](x0) = [0 0 0]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 0 0] 1169.13/295.76 [x](x0) = [0 0 0]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 0 1] [0] 1169.13/295.76 [q1](x0) = [0 0 0]x0 + [1] 1169.13/295.76 [0 0 1] [0], 1169.13/295.76 1169.13/295.76 [1 0 1] [0] 1169.13/295.76 [q0](x0) = [0 0 1]x0 + [0] 1169.13/295.76 [0 0 1] [1], 1169.13/295.76 1169.13/295.76 [1 0 0] [0] 1169.13/295.76 [a](x0) = [0 0 0]x0 + [1] 1169.13/295.76 [0 0 1] [0] 1169.13/295.76 orientation: 1169.13/295.76 [1 0 3] [1] [1 0 3] [0] 1169.13/295.76 y(q2(y(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [1] [1 0 2] [0] 1169.13/295.76 y(q2(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(a(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 1] [0] [1 0 1] [0] 1169.13/295.76 a(q2(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(a(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [0] [1 0 2] [0] 1169.13/295.76 a(q2(y(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 1] [0] [1 0 1] [0] 1169.13/295.76 q1(a(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(q1(x1)) 1169.13/295.76 [0 0 1] [0] [0 0 1] [0] 1169.13/295.76 1169.13/295.76 [1 0 1] [0] [1 0 1] [0] 1169.13/295.76 q2(x(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = x(q0(x1)) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 1] [0] [1 0 1] 1169.13/295.76 q0(a(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 = x(q1(x1)) 1169.13/295.76 [0 0 1] [1] [0 0 1] 1169.13/295.76 1169.13/295.76 [1 0 2] [2] [1 0 2] [0] 1169.13/295.76 a(q1(b(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 3] [3] [1 0 3] [0] 1169.13/295.76 y(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [0] [1 0 2] 1169.13/295.76 q0(y(x1)) = [0 0 1]x1 + [0] >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.76 [0 0 1] [1] [0 0 1] 1169.13/295.76 1169.13/295.76 [1 1 0] [1] [1 0 0] [0] 1169.13/295.76 q3(bl(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = bl(q4(x1)) 1169.13/295.76 [0 0 0] [1] [0 0 0] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [0] [1 0 2] 1169.13/295.76 q1(y(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = y(q1(x1)) 1169.13/295.76 [0 0 1] [0] [0 0 1] 1169.13/295.76 1169.13/295.76 [1 0 2] [1 0 2] 1169.13/295.76 q3(y(x1)) = [0 0 0]x1 >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.76 [0 0 1] [0 0 1] 1169.13/295.76 problem: 1169.13/295.76 strict: 1169.13/295.76 1169.13/295.76 weak: 1169.13/295.76 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.76 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.76 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.76 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.76 q1(a(x1)) -> a(q1(x1)) 1169.13/295.76 q2(x(x1)) -> x(q0(x1)) 1169.13/295.76 q0(a(x1)) -> x(q1(x1)) 1169.13/295.76 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.76 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.76 q0(y(x1)) -> y(q3(x1)) 1169.13/295.76 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.76 q1(y(x1)) -> y(q1(x1)) 1169.13/295.76 q3(y(x1)) -> y(q3(x1)) 1169.13/295.76 Qed 1169.13/295.76 1169.13/295.76 strict: 1169.13/295.76 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.76 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.76 weak: 1169.13/295.76 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.76 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.76 q1(a(x1)) -> a(q1(x1)) 1169.13/295.76 q2(x(x1)) -> x(q0(x1)) 1169.13/295.76 q0(a(x1)) -> x(q1(x1)) 1169.13/295.76 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.76 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.76 q0(y(x1)) -> y(q3(x1)) 1169.13/295.76 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.76 q1(y(x1)) -> y(q1(x1)) 1169.13/295.76 q3(y(x1)) -> y(q3(x1)) 1169.13/295.76 Matrix Interpretation Processor: dim=3 1169.13/295.76 1169.13/295.76 max_matrix: 1169.13/295.76 [1 0 1] 1169.13/295.76 [0 0 1] 1169.13/295.76 [0 0 1] 1169.13/295.76 interpretation: 1169.13/295.76 [1 0 0] 1169.13/295.76 [q4](x0) = [0 0 0]x0 1169.13/295.76 [0 0 0] , 1169.13/295.76 1169.13/295.76 [1 0 1] [0] 1169.13/295.76 [bl](x0) = [0 0 0]x0 + [1] 1169.13/295.76 [0 0 0] [0], 1169.13/295.76 1169.13/295.76 [1 0 0] [0] 1169.13/295.76 [q3](x0) = [0 0 0]x0 + [1] 1169.13/295.76 [0 0 0] [0], 1169.13/295.76 1169.13/295.76 [1 0 0] [0] 1169.13/295.76 [q2](x0) = [0 0 0]x0 + [0] 1169.13/295.76 [0 0 1] [1], 1169.13/295.76 1169.13/295.76 [1 0 0] [0] 1169.13/295.76 [b](x0) = [0 0 0]x0 + [0] 1169.13/295.76 [0 0 1] [1], 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [y](x0) = [0 0 0]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [x](x0) = [0 0 0]x0 1169.13/295.76 [0 0 0] , 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [q1](x0) = [0 0 1]x0 1169.13/295.76 [0 0 1] , 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [q0](x0) = [0 0 0]x0 1169.13/295.76 [0 0 0] , 1169.13/295.76 1169.13/295.76 [1 0 1] 1169.13/295.76 [a](x0) = [0 0 1]x0 1169.13/295.76 [0 0 1] 1169.13/295.76 orientation: 1169.13/295.76 [1 0 2] [1] [1 0 2] [0] 1169.13/295.76 a(q2(a(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(a(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [1] [1 0 2] [0] 1169.13/295.76 a(q2(y(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [1 0 2] 1169.13/295.76 q1(a(x1)) = [0 0 1]x1 >= [0 0 1]x1 = a(q1(x1)) 1169.13/295.76 [0 0 1] [0 0 1] 1169.13/295.76 1169.13/295.76 [1 0 1] [0] [1 0 1] 1169.13/295.76 q2(x(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 = x(q0(x1)) 1169.13/295.76 [0 0 0] [1] [0 0 0] 1169.13/295.76 1169.13/295.76 [1 0 2] [1 0 2] 1169.13/295.76 q0(a(x1)) = [0 0 0]x1 >= [0 0 0]x1 = x(q1(x1)) 1169.13/295.76 [0 0 0] [0 0 0] 1169.13/295.76 1169.13/295.76 [1 0 2] [2] [1 0 2] [0] 1169.13/295.76 a(q1(b(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 + [0] = q2(a(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [2] [1 0 2] [0] 1169.13/295.76 y(q1(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.76 [0 0 1] [1] [0 0 1] [1] 1169.13/295.76 1169.13/295.76 [1 0 2] [1 0 0] 1169.13/295.76 q0(y(x1)) = [0 0 0]x1 >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.77 [0 0 0] [0 0 0] 1169.13/295.77 1169.13/295.77 [1 0 1] [0] [1 0 0] [0] 1169.13/295.77 q3(bl(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = bl(q4(x1)) 1169.13/295.77 [0 0 0] [0] [0 0 0] [0] 1169.13/295.77 1169.13/295.77 [1 0 2] [1 0 2] 1169.13/295.77 q1(y(x1)) = [0 0 1]x1 >= [0 0 0]x1 = y(q1(x1)) 1169.13/295.77 [0 0 1] [0 0 1] 1169.13/295.77 1169.13/295.77 [1 0 1] [0] [1 0 0] 1169.13/295.77 q3(y(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 = y(q3(x1)) 1169.13/295.77 [0 0 0] [0] [0 0 0] 1169.13/295.77 1169.13/295.77 [1 0 2] [1] [1 0 2] [0] 1169.13/295.77 y(q2(a(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(a(x1))) 1169.13/295.77 [0 0 1] [1] [0 0 1] [1] 1169.13/295.77 1169.13/295.77 [1 0 2] [1] [1 0 2] [0] 1169.13/295.77 y(q2(y(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = q2(y(y(x1))) 1169.13/295.77 [0 0 1] [1] [0 0 1] [1] 1169.13/295.77 problem: 1169.13/295.77 strict: 1169.13/295.77 1169.13/295.77 weak: 1169.13/295.77 a(q2(a(x1))) -> q2(a(a(x1))) 1169.13/295.77 a(q2(y(x1))) -> q2(a(y(x1))) 1169.13/295.77 q1(a(x1)) -> a(q1(x1)) 1169.13/295.77 q2(x(x1)) -> x(q0(x1)) 1169.13/295.77 q0(a(x1)) -> x(q1(x1)) 1169.13/295.77 a(q1(b(x1))) -> q2(a(y(x1))) 1169.13/295.77 y(q1(b(x1))) -> q2(y(y(x1))) 1169.13/295.77 q0(y(x1)) -> y(q3(x1)) 1169.13/295.77 q3(bl(x1)) -> bl(q4(x1)) 1169.13/295.77 q1(y(x1)) -> y(q1(x1)) 1169.13/295.77 q3(y(x1)) -> y(q3(x1)) 1169.13/295.77 y(q2(a(x1))) -> q2(y(a(x1))) 1169.13/295.77 y(q2(y(x1))) -> q2(y(y(x1))) 1169.13/295.77 Qed 1169.13/295.77 EOF