YES(?,O(n^1)) 0.16/0.72 YES(?,O(n^1)) 0.16/0.72 0.16/0.72 Problem: 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 0.16/0.72 Proof: 0.16/0.72 Complexity Transformation Processor: 0.16/0.72 strict: 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 weak: 0.16/0.72 0.16/0.72 Matrix Interpretation Processor: dim=1 0.16/0.72 0.16/0.72 max_matrix: 0.16/0.72 1 0.16/0.72 interpretation: 0.16/0.72 [d](x0) = x0 + 4, 0.16/0.72 0.16/0.72 [c](x0) = x0, 0.16/0.72 0.16/0.72 [b](x0) = x0, 0.16/0.72 0.16/0.72 [a](x0) = x0 0.16/0.72 orientation: 0.16/0.72 a(a(a(a(x1)))) = x1 >= x1 = b(b(b(b(b(b(x1)))))) 0.16/0.72 0.16/0.72 b(b(b(b(x1)))) = x1 >= x1 = c(c(c(c(c(c(x1)))))) 0.16/0.72 0.16/0.72 c(c(c(c(x1)))) = x1 >= x1 + 24 = d(d(d(d(d(d(x1)))))) 0.16/0.72 0.16/0.72 b(b(x1)) = x1 >= x1 + 16 = d(d(d(d(x1)))) 0.16/0.72 0.16/0.72 c(c(d(d(d(d(x1)))))) = x1 + 16 >= x1 = a(a(x1)) 0.16/0.72 problem: 0.16/0.72 strict: 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 weak: 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 Matrix Interpretation Processor: dim=1 0.16/0.72 0.16/0.72 max_matrix: 0.16/0.72 1 0.16/0.72 interpretation: 0.16/0.72 [d](x0) = x0, 0.16/0.72 0.16/0.72 [c](x0) = x0 + 4, 0.16/0.72 0.16/0.72 [b](x0) = x0, 0.16/0.72 0.16/0.72 [a](x0) = x0 + 2 0.16/0.72 orientation: 0.16/0.72 a(a(a(a(x1)))) = x1 + 8 >= x1 = b(b(b(b(b(b(x1)))))) 0.16/0.72 0.16/0.72 b(b(b(b(x1)))) = x1 >= x1 + 24 = c(c(c(c(c(c(x1)))))) 0.16/0.72 0.16/0.72 c(c(c(c(x1)))) = x1 + 16 >= x1 = d(d(d(d(d(d(x1)))))) 0.16/0.72 0.16/0.72 b(b(x1)) = x1 >= x1 = d(d(d(d(x1)))) 0.16/0.72 0.16/0.72 c(c(d(d(d(d(x1)))))) = x1 + 8 >= x1 + 4 = a(a(x1)) 0.16/0.72 problem: 0.16/0.72 strict: 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 weak: 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 Matrix Interpretation Processor: dim=1 0.16/0.72 0.16/0.72 max_matrix: 0.16/0.72 1 0.16/0.72 interpretation: 0.16/0.72 [d](x0) = x0 + 1, 0.16/0.72 0.16/0.72 [c](x0) = x0 + 5, 0.16/0.72 0.16/0.72 [b](x0) = x0 + 3, 0.16/0.72 0.16/0.72 [a](x0) = x0 + 7 0.16/0.72 orientation: 0.16/0.72 b(b(b(b(x1)))) = x1 + 12 >= x1 + 30 = c(c(c(c(c(c(x1)))))) 0.16/0.72 0.16/0.72 b(b(x1)) = x1 + 6 >= x1 + 4 = d(d(d(d(x1)))) 0.16/0.72 0.16/0.72 a(a(a(a(x1)))) = x1 + 28 >= x1 + 18 = b(b(b(b(b(b(x1)))))) 0.16/0.72 0.16/0.72 c(c(c(c(x1)))) = x1 + 20 >= x1 + 6 = d(d(d(d(d(d(x1)))))) 0.16/0.72 0.16/0.72 c(c(d(d(d(d(x1)))))) = x1 + 14 >= x1 + 14 = a(a(x1)) 0.16/0.72 problem: 0.16/0.72 strict: 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 weak: 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 Matrix Interpretation Processor: dim=1 0.16/0.72 0.16/0.72 max_matrix: 0.16/0.72 1 0.16/0.72 interpretation: 0.16/0.72 [d](x0) = x0 + 11, 0.16/0.72 0.16/0.72 [c](x0) = x0 + 17, 0.16/0.72 0.16/0.72 [b](x0) = x0 + 26, 0.16/0.72 0.16/0.72 [a](x0) = x0 + 39 0.16/0.72 orientation: 0.16/0.72 b(b(b(b(x1)))) = x1 + 104 >= x1 + 102 = c(c(c(c(c(c(x1)))))) 0.16/0.72 0.16/0.72 b(b(x1)) = x1 + 52 >= x1 + 44 = d(d(d(d(x1)))) 0.16/0.72 0.16/0.72 a(a(a(a(x1)))) = x1 + 156 >= x1 + 156 = b(b(b(b(b(b(x1)))))) 0.16/0.72 0.16/0.72 c(c(c(c(x1)))) = x1 + 68 >= x1 + 66 = d(d(d(d(d(d(x1)))))) 0.16/0.72 0.16/0.72 c(c(d(d(d(d(x1)))))) = x1 + 78 >= x1 + 78 = a(a(x1)) 0.16/0.72 problem: 0.16/0.72 strict: 0.16/0.72 0.16/0.72 weak: 0.16/0.72 b(b(b(b(x1)))) -> c(c(c(c(c(c(x1)))))) 0.16/0.72 b(b(x1)) -> d(d(d(d(x1)))) 0.16/0.72 a(a(a(a(x1)))) -> b(b(b(b(b(b(x1)))))) 0.16/0.72 c(c(c(c(x1)))) -> d(d(d(d(d(d(x1)))))) 0.16/0.72 c(c(d(d(d(d(x1)))))) -> a(a(x1)) 0.16/0.72 Qed 0.16/0.73 EOF