YES(?,O(n^2)) 1170.78/295.38 YES(?,O(n^2)) 1170.78/295.39 1170.78/295.39 Problem: 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 1170.78/295.39 Proof: 1170.78/295.39 Complexity Transformation Processor: 1170.78/295.39 strict: 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 weak: 1170.78/295.39 1170.78/295.39 Matrix Interpretation Processor: dim=1 1170.78/295.39 1170.78/295.39 max_matrix: 1170.78/295.39 1 1170.78/295.39 interpretation: 1170.78/295.39 [C](x0) = x0 + 116, 1170.78/295.39 1170.78/295.39 [B](x0) = x0 + 32, 1170.78/295.39 1170.78/295.39 [A](x0) = x0 + 112, 1170.78/295.39 1170.78/295.39 [a](x0) = x0 + 140, 1170.78/295.39 1170.78/295.39 [b](x0) = x0 + 8, 1170.78/295.39 1170.78/295.39 [c](x0) = x0 + 17 1170.78/295.39 orientation: 1170.78/295.39 a(b(c(x1))) = x1 + 165 >= x1 + 165 = c(b(a(x1))) 1170.78/295.39 1170.78/295.39 C(B(A(x1))) = x1 + 260 >= x1 + 260 = A(B(C(x1))) 1170.78/295.39 1170.78/295.39 b(a(C(x1))) = x1 + 264 >= x1 + 264 = C(a(b(x1))) 1170.78/295.39 1170.78/295.39 c(A(B(x1))) = x1 + 161 >= x1 + 161 = B(A(c(x1))) 1170.78/295.39 1170.78/295.39 A(c(b(x1))) = x1 + 137 >= x1 + 137 = b(c(A(x1))) 1170.78/295.39 1170.78/295.39 B(C(a(x1))) = x1 + 288 >= x1 + 288 = a(C(B(x1))) 1170.78/295.39 1170.78/295.39 a(A(x1)) = x1 + 252 >= x1 = x1 1170.78/295.39 1170.78/295.39 A(a(x1)) = x1 + 252 >= x1 = x1 1170.78/295.39 1170.78/295.39 b(B(x1)) = x1 + 40 >= x1 = x1 1170.78/295.39 1170.78/295.39 B(b(x1)) = x1 + 40 >= x1 = x1 1170.78/295.39 1170.78/295.39 c(C(x1)) = x1 + 133 >= x1 = x1 1170.78/295.39 1170.78/295.39 C(c(x1)) = x1 + 133 >= x1 = x1 1170.78/295.39 problem: 1170.78/295.39 strict: 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 weak: 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 Splitting Processor: 1170.78/295.39 strict: 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 weak: 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 Matrix Interpretation Processor: dim=2 1170.78/295.39 1170.78/295.39 max_matrix: 1170.78/295.39 [1 1] 1170.78/295.39 [0 1] 1170.78/295.39 interpretation: 1170.78/295.39 [2] 1170.78/295.39 [C](x0) = x0 + [0], 1170.78/295.39 1170.78/295.39 1170.78/295.39 [B](x0) = x0, 1170.78/295.39 1170.78/295.39 [1 1] 1170.78/295.39 [A](x0) = [0 1]x0, 1170.78/295.39 1170.78/295.39 1170.78/295.39 [a](x0) = x0, 1170.78/295.39 1170.78/295.39 [2] 1170.78/295.39 [b](x0) = x0 + [1], 1170.78/295.39 1170.78/295.39 [2] 1170.78/295.39 [c](x0) = x0 + [0] 1170.78/295.39 orientation: 1170.78/295.39 [1 1] [5] [1 1] [4] 1170.78/295.39 A(c(b(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = b(c(A(x1))) 1170.78/295.39 1170.78/295.39 [1 1] 1170.78/295.39 a(A(x1)) = [0 1]x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 [1 1] 1170.78/295.39 A(a(x1)) = [0 1]x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 [2] 1170.78/295.39 b(B(x1)) = x1 + [1] >= x1 = x1 1170.78/295.39 1170.78/295.39 [2] 1170.78/295.39 B(b(x1)) = x1 + [1] >= x1 = x1 1170.78/295.39 1170.78/295.39 [4] 1170.78/295.39 c(C(x1)) = x1 + [0] >= x1 = x1 1170.78/295.39 1170.78/295.39 [4] 1170.78/295.39 C(c(x1)) = x1 + [0] >= x1 = x1 1170.78/295.39 1170.78/295.39 [4] [4] 1170.78/295.39 a(b(c(x1))) = x1 + [1] >= x1 + [1] = c(b(a(x1))) 1170.78/295.39 1170.78/295.39 [1 1] [2] [1 1] [2] 1170.78/295.39 C(B(A(x1))) = [0 1]x1 + [0] >= [0 1]x1 + [0] = A(B(C(x1))) 1170.78/295.39 1170.78/295.39 [4] [4] 1170.78/295.39 b(a(C(x1))) = x1 + [1] >= x1 + [1] = C(a(b(x1))) 1170.78/295.39 1170.78/295.39 [1 1] [2] [1 1] [2] 1170.78/295.39 c(A(B(x1))) = [0 1]x1 + [0] >= [0 1]x1 + [0] = B(A(c(x1))) 1170.78/295.39 1170.78/295.39 [2] [2] 1170.78/295.39 B(C(a(x1))) = x1 + [0] >= x1 + [0] = a(C(B(x1))) 1170.78/295.39 problem: 1170.78/295.39 strict: 1170.78/295.39 1170.78/295.39 weak: 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 Qed 1170.78/295.39 1170.78/295.39 strict: 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 weak: 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 Splitting Processor: 1170.78/295.39 strict: 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 weak: 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 Splitting Processor: 1170.78/295.39 strict: 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 weak: 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 Matrix Interpretation Processor: dim=2 1170.78/295.39 1170.78/295.39 max_matrix: 1170.78/295.39 [1 2] 1170.78/295.39 [0 1] 1170.78/295.39 interpretation: 1170.78/295.39 [0] 1170.78/295.39 [C](x0) = x0 + [1], 1170.78/295.39 1170.78/295.39 1170.78/295.39 [B](x0) = x0, 1170.78/295.39 1170.78/295.39 1170.78/295.39 [A](x0) = x0, 1170.78/295.39 1170.78/295.39 1170.78/295.39 [a](x0) = x0, 1170.78/295.39 1170.78/295.39 [1 2] 1170.78/295.39 [b](x0) = [0 1]x0, 1170.78/295.39 1170.78/295.39 1170.78/295.39 [c](x0) = x0 1170.78/295.39 orientation: 1170.78/295.39 [1 2] [2] [1 2] [0] 1170.78/295.39 b(a(C(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = C(a(b(x1))) 1170.78/295.39 1170.78/295.39 [0] [0] 1170.78/295.39 B(C(a(x1))) = x1 + [1] >= x1 + [1] = a(C(B(x1))) 1170.78/295.39 1170.78/295.39 [1 2] [1 2] 1170.78/295.39 A(c(b(x1))) = [0 1]x1 >= [0 1]x1 = b(c(A(x1))) 1170.78/295.39 1170.78/295.39 1170.78/295.39 a(A(x1)) = x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 1170.78/295.39 A(a(x1)) = x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 [1 2] 1170.78/295.39 b(B(x1)) = [0 1]x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 [1 2] 1170.78/295.39 B(b(x1)) = [0 1]x1 >= x1 = x1 1170.78/295.39 1170.78/295.39 [0] 1170.78/295.39 c(C(x1)) = x1 + [1] >= x1 = x1 1170.78/295.39 1170.78/295.39 [0] 1170.78/295.39 C(c(x1)) = x1 + [1] >= x1 = x1 1170.78/295.39 1170.78/295.39 [1 2] [1 2] 1170.78/295.39 a(b(c(x1))) = [0 1]x1 >= [0 1]x1 = c(b(a(x1))) 1170.78/295.39 1170.78/295.39 [0] [0] 1170.78/295.39 C(B(A(x1))) = x1 + [1] >= x1 + [1] = A(B(C(x1))) 1170.78/295.39 1170.78/295.39 1170.78/295.39 c(A(B(x1))) = x1 >= x1 = B(A(c(x1))) 1170.78/295.39 problem: 1170.78/295.39 strict: 1170.78/295.39 1170.78/295.39 weak: 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 Qed 1170.78/295.39 1170.78/295.39 strict: 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.39 weak: 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 Splitting Processor: 1170.78/295.39 strict: 1170.78/295.39 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.39 weak: 1170.78/295.39 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.39 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.39 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.39 a(A(x1)) -> x1 1170.78/295.39 A(a(x1)) -> x1 1170.78/295.39 b(B(x1)) -> x1 1170.78/295.39 B(b(x1)) -> x1 1170.78/295.39 c(C(x1)) -> x1 1170.78/295.39 C(c(x1)) -> x1 1170.78/295.39 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.40 Splitting Processor: 1170.78/295.40 strict: 1170.78/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.78/295.40 weak: 1170.78/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.78/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.78/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.78/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.78/295.40 a(A(x1)) -> x1 1170.78/295.40 A(a(x1)) -> x1 1170.78/295.40 b(B(x1)) -> x1 1170.78/295.40 B(b(x1)) -> x1 1170.78/295.40 c(C(x1)) -> x1 1170.78/295.40 C(c(x1)) -> x1 1170.78/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.78/295.40 Matrix Interpretation Processor: dim=2 1170.78/295.40 1170.78/295.40 max_matrix: 1170.78/295.40 [1 1] 1170.78/295.40 [0 1] 1170.78/295.40 interpretation: 1170.78/295.40 1170.78/295.40 [C](x0) = x0, 1170.78/295.40 1170.78/295.40 [0] 1170.78/295.40 [B](x0) = x0 + [1], 1170.78/295.40 1170.78/295.40 1170.78/295.40 [A](x0) = x0, 1170.78/295.40 1170.78/295.40 1170.78/295.40 [a](x0) = x0, 1170.78/295.40 1170.78/295.40 [1] 1170.78/295.40 [b](x0) = x0 + [0], 1170.78/295.40 1170.78/295.40 [1 1] 1170.78/295.40 [c](x0) = [0 1]x0 1170.78/295.40 orientation: 1170.78/295.40 [1 1] [1] [1 1] [0] 1170.78/295.40 c(A(B(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = B(A(c(x1))) 1170.78/295.40 1170.78/295.40 [0] [0] 1170.78/295.40 C(B(A(x1))) = x1 + [1] >= x1 + [1] = A(B(C(x1))) 1170.78/295.40 1170.78/295.40 [1] [1] 1170.78/295.40 b(a(C(x1))) = x1 + [0] >= x1 + [0] = C(a(b(x1))) 1170.78/295.40 1170.78/295.40 [0] [0] 1170.78/295.40 B(C(a(x1))) = x1 + [1] >= x1 + [1] = a(C(B(x1))) 1170.78/295.40 1170.78/295.40 [1 1] [1] [1 1] [1] 1170.78/295.40 A(c(b(x1))) = [0 1]x1 + [0] >= [0 1]x1 + [0] = b(c(A(x1))) 1170.78/295.40 1170.78/295.40 1170.78/295.40 a(A(x1)) = x1 >= x1 = x1 1170.78/295.40 1170.78/295.40 1170.78/295.40 A(a(x1)) = x1 >= x1 = x1 1170.78/295.40 1170.78/295.40 [1] 1170.78/295.40 b(B(x1)) = x1 + [1] >= x1 = x1 1170.78/295.40 1170.78/295.40 [1] 1170.78/295.40 B(b(x1)) = x1 + [1] >= x1 = x1 1170.78/295.40 1170.78/295.40 [1 1] 1170.88/295.40 c(C(x1)) = [0 1]x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] 1170.88/295.40 C(c(x1)) = [0 1]x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] [1] [1 1] [1] 1170.88/295.40 a(b(c(x1))) = [0 1]x1 + [0] >= [0 1]x1 + [0] = c(b(a(x1))) 1170.88/295.40 problem: 1170.88/295.40 strict: 1170.88/295.40 1170.88/295.40 weak: 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 Qed 1170.88/295.40 1170.88/295.40 strict: 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 weak: 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 Matrix Interpretation Processor: dim=2 1170.88/295.40 1170.88/295.40 max_matrix: 1170.88/295.40 [1 2] 1170.88/295.40 [0 1] 1170.88/295.40 interpretation: 1170.88/295.40 1170.88/295.40 [C](x0) = x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [B](x0) = x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [A](x0) = x0, 1170.88/295.40 1170.88/295.40 [1 2] [0] 1170.88/295.40 [a](x0) = [0 1]x0 + [1], 1170.88/295.40 1170.88/295.40 1170.88/295.40 [b](x0) = x0, 1170.88/295.40 1170.88/295.40 [3] 1170.88/295.40 [c](x0) = x0 + [3] 1170.88/295.40 orientation: 1170.88/295.40 [1 2] [9] [1 2] [3] 1170.88/295.40 a(b(c(x1))) = [0 1]x1 + [4] >= [0 1]x1 + [4] = c(b(a(x1))) 1170.88/295.40 1170.88/295.40 [3] [3] 1170.88/295.40 c(A(B(x1))) = x1 + [3] >= x1 + [3] = B(A(c(x1))) 1170.88/295.40 1170.88/295.40 1170.88/295.40 C(B(A(x1))) = x1 >= x1 = A(B(C(x1))) 1170.88/295.40 1170.88/295.40 [1 2] [0] [1 2] [0] 1170.88/295.40 b(a(C(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = C(a(b(x1))) 1170.88/295.40 1170.88/295.40 [1 2] [0] [1 2] [0] 1170.88/295.40 B(C(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(C(B(x1))) 1170.88/295.40 1170.88/295.40 [3] [3] 1170.88/295.40 A(c(b(x1))) = x1 + [3] >= x1 + [3] = b(c(A(x1))) 1170.88/295.40 1170.88/295.40 [1 2] [0] 1170.88/295.40 a(A(x1)) = [0 1]x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 2] [0] 1170.88/295.40 A(a(x1)) = [0 1]x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 b(B(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 B(b(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [3] 1170.88/295.40 c(C(x1)) = x1 + [3] >= x1 = x1 1170.88/295.40 1170.88/295.40 [3] 1170.88/295.40 C(c(x1)) = x1 + [3] >= x1 = x1 1170.88/295.40 problem: 1170.88/295.40 strict: 1170.88/295.40 1170.88/295.40 weak: 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 Qed 1170.88/295.40 1170.88/295.40 strict: 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 weak: 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 Matrix Interpretation Processor: dim=2 1170.88/295.40 1170.88/295.40 max_matrix: 1170.88/295.40 [1 1] 1170.88/295.40 [0 1] 1170.88/295.40 interpretation: 1170.88/295.40 [1 1] 1170.88/295.40 [C](x0) = [0 1]x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [B](x0) = x0, 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 [A](x0) = x0 + [1], 1170.88/295.40 1170.88/295.40 1170.88/295.40 [a](x0) = x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [b](x0) = x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [c](x0) = x0 1170.88/295.40 orientation: 1170.88/295.40 [1 1] [1] [1 1] [0] 1170.88/295.40 C(B(A(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = A(B(C(x1))) 1170.88/295.40 1170.88/295.40 [1 1] [1 1] 1170.88/295.40 b(a(C(x1))) = [0 1]x1 >= [0 1]x1 = C(a(b(x1))) 1170.88/295.40 1170.88/295.40 [1 1] [1 1] 1170.88/295.40 B(C(a(x1))) = [0 1]x1 >= [0 1]x1 = a(C(B(x1))) 1170.88/295.40 1170.88/295.40 [0] [0] 1170.88/295.40 A(c(b(x1))) = x1 + [1] >= x1 + [1] = b(c(A(x1))) 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 a(A(x1)) = x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 A(a(x1)) = x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 b(B(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 B(b(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] 1170.88/295.40 c(C(x1)) = [0 1]x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] 1170.88/295.40 C(c(x1)) = [0 1]x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 a(b(c(x1))) = x1 >= x1 = c(b(a(x1))) 1170.88/295.40 1170.88/295.40 [0] [0] 1170.88/295.40 c(A(B(x1))) = x1 + [1] >= x1 + [1] = B(A(c(x1))) 1170.88/295.40 problem: 1170.88/295.40 strict: 1170.88/295.40 1170.88/295.40 weak: 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 Qed 1170.88/295.40 1170.88/295.40 strict: 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 weak: 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 Matrix Interpretation Processor: dim=2 1170.88/295.40 1170.88/295.40 max_matrix: 1170.88/295.40 [1 1] 1170.88/295.40 [0 1] 1170.88/295.40 interpretation: 1170.88/295.40 1170.88/295.40 [C](x0) = x0, 1170.88/295.40 1170.88/295.40 [1 1] 1170.88/295.40 [B](x0) = [0 1]x0, 1170.88/295.40 1170.88/295.40 1170.88/295.40 [A](x0) = x0, 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 [a](x0) = x0 + [1], 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 [b](x0) = x0 + [2], 1170.88/295.40 1170.88/295.40 1170.88/295.40 [c](x0) = x0 1170.88/295.40 orientation: 1170.88/295.40 [1 1] [1] [1 1] [0] 1170.88/295.40 B(C(a(x1))) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(C(B(x1))) 1170.88/295.40 1170.88/295.40 [0] [0] 1170.88/295.40 A(c(b(x1))) = x1 + [2] >= x1 + [2] = b(c(A(x1))) 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 a(A(x1)) = x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 [0] 1170.88/295.40 A(a(x1)) = x1 + [1] >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] [0] 1170.88/295.40 b(B(x1)) = [0 1]x1 + [2] >= x1 = x1 1170.88/295.40 1170.88/295.40 [1 1] [2] 1170.88/295.40 B(b(x1)) = [0 1]x1 + [2] >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 c(C(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 1170.88/295.40 C(c(x1)) = x1 >= x1 = x1 1170.88/295.40 1170.88/295.40 [0] [0] 1170.88/295.40 a(b(c(x1))) = x1 + [3] >= x1 + [3] = c(b(a(x1))) 1170.88/295.40 1170.88/295.40 [1 1] [1 1] 1170.88/295.40 C(B(A(x1))) = [0 1]x1 >= [0 1]x1 = A(B(C(x1))) 1170.88/295.40 1170.88/295.40 [0] [0] 1170.88/295.40 b(a(C(x1))) = x1 + [3] >= x1 + [3] = C(a(b(x1))) 1170.88/295.40 1170.88/295.40 [1 1] [1 1] 1170.88/295.40 c(A(B(x1))) = [0 1]x1 >= [0 1]x1 = B(A(c(x1))) 1170.88/295.40 problem: 1170.88/295.40 strict: 1170.88/295.40 1170.88/295.40 weak: 1170.88/295.40 B(C(a(x1))) -> a(C(B(x1))) 1170.88/295.40 A(c(b(x1))) -> b(c(A(x1))) 1170.88/295.40 a(A(x1)) -> x1 1170.88/295.40 A(a(x1)) -> x1 1170.88/295.40 b(B(x1)) -> x1 1170.88/295.40 B(b(x1)) -> x1 1170.88/295.40 c(C(x1)) -> x1 1170.88/295.40 C(c(x1)) -> x1 1170.88/295.40 a(b(c(x1))) -> c(b(a(x1))) 1170.88/295.40 C(B(A(x1))) -> A(B(C(x1))) 1170.88/295.40 b(a(C(x1))) -> C(a(b(x1))) 1170.88/295.40 c(A(B(x1))) -> B(A(c(x1))) 1170.88/295.40 Qed 1170.88/295.41 EOF