YES(?,O(n^1)) 0.16/0.32 YES(?,O(n^1)) 0.16/0.32 0.16/0.32 Problem: 0.16/0.32 a(a(x1)) -> b(b(b(x1))) 0.16/0.32 b(b(x1)) -> c(c(c(x1))) 0.16/0.32 c(c(c(c(x1)))) -> a(b(x1)) 0.16/0.32 0.16/0.32 Proof: 0.16/0.32 Complexity Transformation Processor: 0.16/0.32 strict: 0.16/0.32 a(a(x1)) -> b(b(b(x1))) 0.16/0.32 b(b(x1)) -> c(c(c(x1))) 0.16/0.32 c(c(c(c(x1)))) -> a(b(x1)) 0.16/0.32 weak: 0.16/0.32 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [c](x0) = x0 + 32, 0.16/0.32 0.16/0.32 [b](x0) = x0 + 4, 0.16/0.32 0.16/0.32 [a](x0) = x0 + 128 0.16/0.32 orientation: 0.16/0.32 a(a(x1)) = x1 + 256 >= x1 + 12 = b(b(b(x1))) 0.16/0.32 0.16/0.32 b(b(x1)) = x1 + 8 >= x1 + 96 = c(c(c(x1))) 0.16/0.32 0.16/0.32 c(c(c(c(x1)))) = x1 + 128 >= x1 + 132 = a(b(x1)) 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 b(b(x1)) -> c(c(c(x1))) 0.16/0.32 c(c(c(c(x1)))) -> a(b(x1)) 0.16/0.32 weak: 0.16/0.32 a(a(x1)) -> b(b(b(x1))) 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [c](x0) = x0 + 5, 0.16/0.32 0.16/0.32 [b](x0) = x0 + 8, 0.16/0.32 0.16/0.32 [a](x0) = x0 + 12 0.16/0.32 orientation: 0.16/0.32 b(b(x1)) = x1 + 16 >= x1 + 15 = c(c(c(x1))) 0.16/0.32 0.16/0.32 c(c(c(c(x1)))) = x1 + 20 >= x1 + 20 = a(b(x1)) 0.16/0.32 0.16/0.32 a(a(x1)) = x1 + 24 >= x1 + 24 = b(b(b(x1))) 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 c(c(c(c(x1)))) -> a(b(x1)) 0.16/0.32 weak: 0.16/0.32 b(b(x1)) -> c(c(c(x1))) 0.16/0.32 a(a(x1)) -> b(b(b(x1))) 0.16/0.32 Matrix Interpretation Processor: dim=1 0.16/0.32 0.16/0.32 max_matrix: 0.16/0.32 1 0.16/0.32 interpretation: 0.16/0.32 [c](x0) = x0 + 12, 0.16/0.32 0.16/0.32 [b](x0) = x0 + 18, 0.16/0.32 0.16/0.32 [a](x0) = x0 + 27 0.16/0.32 orientation: 0.16/0.32 c(c(c(c(x1)))) = x1 + 48 >= x1 + 45 = a(b(x1)) 0.16/0.32 0.16/0.32 b(b(x1)) = x1 + 36 >= x1 + 36 = c(c(c(x1))) 0.16/0.32 0.16/0.32 a(a(x1)) = x1 + 54 >= x1 + 54 = b(b(b(x1))) 0.16/0.32 problem: 0.16/0.32 strict: 0.16/0.32 0.16/0.32 weak: 0.16/0.32 c(c(c(c(x1)))) -> a(b(x1)) 0.16/0.32 b(b(x1)) -> c(c(c(x1))) 0.16/0.32 a(a(x1)) -> b(b(b(x1))) 0.16/0.32 Qed 0.16/0.33 EOF