YES(?,O(n^1)) 31.89/8.33 YES(?,O(n^1)) 31.89/8.33 31.89/8.33 Problem: 31.89/8.33 a(a(x1)) -> a(b(a(x1))) 31.89/8.33 b(b(x1)) -> a(a(x1)) 31.89/8.33 a(b(b(a(x1)))) -> x1 31.89/8.33 31.89/8.33 Proof: 31.89/8.33 Complexity Transformation Processor: 31.89/8.33 strict: 31.89/8.33 a(a(x1)) -> a(b(a(x1))) 31.89/8.33 b(b(x1)) -> a(a(x1)) 31.89/8.33 a(b(b(a(x1)))) -> x1 31.89/8.33 weak: 31.89/8.33 31.89/8.33 Root-Labeling Processor: 31.89/8.33 strict: 31.89/8.33 a(a)(a(a)(x1)) -> a(b)(b(a)(a(a)(x1))) 31.89/8.33 a(a)(a(b)(x1)) -> a(b)(b(a)(a(b)(x1))) 31.89/8.33 a(b)(b(b)(b(a)(x1))) -> a(a)(a(a)(a(a)(x1))) 31.89/8.33 a(b)(b(b)(b(b)(x1))) -> a(a)(a(a)(a(b)(x1))) 31.89/8.33 b(b)(b(b)(b(a)(x1))) -> b(a)(a(a)(a(a)(x1))) 31.89/8.33 b(b)(b(b)(b(b)(x1))) -> b(a)(a(a)(a(b)(x1))) 31.89/8.33 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> a(a)(x1) 31.89/8.33 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> a(b)(x1) 31.89/8.33 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> b(a)(x1) 31.89/8.33 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> b(b)(x1) 31.89/8.33 weak: 31.89/8.33 31.89/8.33 Arctic Interpretation Processor: 31.89/8.33 dimension: 1 31.89/8.33 interpretation: 31.89/8.33 [b(b)](x0) = 4x0, 31.89/8.33 31.89/8.33 [b(a)](x0) = x0, 31.89/8.33 31.89/8.33 [a(b)](x0) = x0, 31.89/8.33 31.89/8.33 [a(a)](x0) = x0 31.89/8.33 orientation: 31.89/8.33 a(a)(a(a)(x1)) = x1 >= x1 = a(b)(b(a)(a(a)(x1))) 31.89/8.33 31.89/8.33 a(a)(a(b)(x1)) = x1 >= x1 = a(b)(b(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(a)(x1))) = 4x1 >= x1 = a(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(b)(x1))) = 8x1 >= x1 = a(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(a)(x1))) = 8x1 >= x1 = b(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(b)(x1))) = 12x1 >= x1 = b(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 4x1 >= x1 = a(a)(x1) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 4x1 >= x1 = a(b)(x1) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 4x1 >= x1 = b(a)(x1) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 4x1 >= 4x1 = b(b)(x1) 31.89/8.34 problem: 31.89/8.34 strict: 31.89/8.34 a(a)(a(a)(x1)) -> a(b)(b(a)(a(a)(x1))) 31.89/8.34 a(a)(a(b)(x1)) -> a(b)(b(a)(a(b)(x1))) 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> b(b)(x1) 31.89/8.34 weak: 31.89/8.34 a(b)(b(b)(b(a)(x1))) -> a(a)(a(a)(a(a)(x1))) 31.89/8.34 a(b)(b(b)(b(b)(x1))) -> a(a)(a(a)(a(b)(x1))) 31.89/8.34 b(b)(b(b)(b(a)(x1))) -> b(a)(a(a)(a(a)(x1))) 31.89/8.34 b(b)(b(b)(b(b)(x1))) -> b(a)(a(a)(a(b)(x1))) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> a(a)(x1) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> a(b)(x1) 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> b(a)(x1) 31.89/8.34 Arctic Interpretation Processor: 31.89/8.34 dimension: 1 31.89/8.34 interpretation: 31.89/8.34 [b(b)](x0) = 9x0, 31.89/8.34 31.89/8.34 [b(a)](x0) = 4x0, 31.89/8.34 31.89/8.34 [a(b)](x0) = x0, 31.89/8.34 31.89/8.34 [a(a)](x0) = 4x0 31.89/8.34 orientation: 31.89/8.34 a(a)(a(a)(x1)) = 8x1 >= 8x1 = a(b)(b(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 a(a)(a(b)(x1)) = 4x1 >= 4x1 = a(b)(b(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 17x1 >= 9x1 = b(b)(x1) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(a)(x1))) = 13x1 >= 12x1 = a(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(b)(x1))) = 18x1 >= 8x1 = a(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(a)(x1))) = 22x1 >= 12x1 = b(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(b)(x1))) = 27x1 >= 8x1 = b(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 21x1 >= 4x1 = a(a)(x1) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 17x1 >= x1 = a(b)(x1) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 21x1 >= 4x1 = b(a)(x1) 31.89/8.34 problem: 31.89/8.34 strict: 31.89/8.34 a(a)(a(a)(x1)) -> a(b)(b(a)(a(a)(x1))) 31.89/8.34 a(a)(a(b)(x1)) -> a(b)(b(a)(a(b)(x1))) 31.89/8.34 weak: 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> b(b)(x1) 31.89/8.34 a(b)(b(b)(b(a)(x1))) -> a(a)(a(a)(a(a)(x1))) 31.89/8.34 a(b)(b(b)(b(b)(x1))) -> a(a)(a(a)(a(b)(x1))) 31.89/8.34 b(b)(b(b)(b(a)(x1))) -> b(a)(a(a)(a(a)(x1))) 31.89/8.34 b(b)(b(b)(b(b)(x1))) -> b(a)(a(a)(a(b)(x1))) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> a(a)(x1) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> a(b)(x1) 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> b(a)(x1) 31.89/8.34 Arctic Interpretation Processor: 31.89/8.34 dimension: 1 31.89/8.34 interpretation: 31.89/8.34 [b(b)](x0) = 10x0, 31.89/8.34 31.89/8.34 [b(a)](x0) = 2x0, 31.89/8.34 31.89/8.34 [a(b)](x0) = x0, 31.89/8.34 31.89/8.34 [a(a)](x0) = 4x0 31.89/8.34 orientation: 31.89/8.34 a(a)(a(a)(x1)) = 8x1 >= 6x1 = a(b)(b(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 a(a)(a(b)(x1)) = 4x1 >= 2x1 = a(b)(b(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 14x1 >= 10x1 = b(b)(x1) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(a)(x1))) = 12x1 >= 12x1 = a(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 a(b)(b(b)(b(b)(x1))) = 20x1 >= 8x1 = a(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(a)(x1))) = 22x1 >= 10x1 = b(a)(a(a)(a(a)(x1))) 31.89/8.34 31.89/8.34 b(b)(b(b)(b(b)(x1))) = 30x1 >= 6x1 = b(a)(a(a)(a(b)(x1))) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 20x1 >= 4x1 = a(a)(x1) 31.89/8.34 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) = 16x1 >= x1 = a(b)(x1) 31.89/8.34 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) = 18x1 >= 2x1 = b(a)(x1) 31.89/8.34 problem: 31.89/8.34 strict: 31.89/8.34 31.89/8.34 weak: 31.89/8.34 a(a)(a(a)(x1)) -> a(b)(b(a)(a(a)(x1))) 31.89/8.34 a(a)(a(b)(x1)) -> a(b)(b(a)(a(b)(x1))) 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> b(b)(x1) 31.89/8.34 a(b)(b(b)(b(a)(x1))) -> a(a)(a(a)(a(a)(x1))) 31.89/8.34 a(b)(b(b)(b(b)(x1))) -> a(a)(a(a)(a(b)(x1))) 31.89/8.34 b(b)(b(b)(b(a)(x1))) -> b(a)(a(a)(a(a)(x1))) 31.89/8.34 b(b)(b(b)(b(b)(x1))) -> b(a)(a(a)(a(b)(x1))) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> a(a)(x1) 31.89/8.34 a(a)(a(b)(b(b)(b(a)(a(b)(x1))))) -> a(b)(x1) 31.89/8.34 b(a)(a(b)(b(b)(b(a)(a(a)(x1))))) -> b(a)(x1) 31.89/8.34 Qed 31.89/8.34 EOF