YES(?,O(n^1)) 14.18/4.37 YES(?,O(n^1)) 14.18/4.38 14.18/4.38 Problem: 14.18/4.38 a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x)))) 14.18/4.38 a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x)))) 14.18/4.38 14.18/4.38 Proof: 14.18/4.38 Uncurry Processor: 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.38 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.38 a(f(),x1) -> f1(x1) 14.18/4.38 a(g(),x1) -> g1(x1) 14.18/4.38 Complexity Transformation Processor: 14.18/4.38 strict: 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.38 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.38 a(f(),x1) -> f1(x1) 14.18/4.38 a(g(),x1) -> g1(x1) 14.18/4.38 weak: 14.18/4.38 14.18/4.38 Matrix Interpretation Processor: dim=1 14.18/4.38 14.18/4.38 max_matrix: 14.18/4.38 1 14.18/4.38 interpretation: 14.18/4.38 [g1](x0) = x0, 14.18/4.38 14.18/4.38 [f1](x0) = x0 + 128, 14.18/4.38 14.18/4.38 [a](x0, x1) = x0 + x1 + 249, 14.18/4.38 14.18/4.38 [g] = 0, 14.18/4.38 14.18/4.38 [f] = 10 14.18/4.38 orientation: 14.18/4.38 f1(g1(f1(x))) = x + 256 >= x + 256 = f1(g1(g1(f1(x)))) 14.18/4.38 14.18/4.38 g1(f1(g1(x))) = x + 128 >= x + 256 = g1(f1(f1(g1(x)))) 14.18/4.38 14.18/4.38 a(f(),x1) = x1 + 259 >= x1 + 128 = f1(x1) 14.18/4.38 14.18/4.38 a(g(),x1) = x1 + 249 >= x1 = g1(x1) 14.18/4.38 problem: 14.18/4.38 strict: 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.38 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.38 weak: 14.18/4.38 a(f(),x1) -> f1(x1) 14.18/4.38 a(g(),x1) -> g1(x1) 14.18/4.38 Splitting Processor: 14.18/4.38 strict: 14.18/4.38 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.38 weak: 14.18/4.38 a(f(),x1) -> f1(x1) 14.18/4.38 a(g(),x1) -> g1(x1) 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.38 Matrix Interpretation Processor: dim=5 14.18/4.38 14.18/4.38 max_matrix: 14.18/4.38 [1 1 1 1 1] 14.18/4.38 [0 0 1 1 1] 14.18/4.38 [0 0 0 1 1] 14.18/4.38 [0 0 0 0 1] 14.18/4.38 [0 0 0 0 0] 14.18/4.38 interpretation: 14.18/4.38 [1 1 0 0 0] [0] 14.18/4.38 [0 0 0 0 0] [0] 14.18/4.38 [g1](x0) = [0 0 0 0 1]x0 + [0] 14.18/4.38 [0 0 0 0 0] [1] 14.18/4.38 [0 0 0 0 0] [1], 14.18/4.38 14.18/4.38 [1 0 0 0 1] 14.18/4.38 [0 0 0 1 1] 14.18/4.38 [f1](x0) = [0 0 0 0 0]x0 14.18/4.38 [0 0 0 0 0] 14.18/4.38 [0 0 0 0 0] , 14.18/4.38 14.18/4.38 [1 1 1 0 0] [1 1 1 1 1] [0] 14.18/4.38 [0 0 0 1 0] [0 0 1 1 1] [0] 14.18/4.38 [a](x0, x1) = [0 0 0 0 0]x0 + [0 0 0 1 1]x1 + [0] 14.18/4.38 [0 0 0 0 1] [0 0 0 0 0] [1] 14.18/4.38 [0 0 0 0 0] [0 0 0 0 0] [1], 14.18/4.38 14.18/4.38 [0] 14.18/4.38 [1] 14.18/4.38 [g] = [1] 14.18/4.38 [0] 14.18/4.38 [0], 14.18/4.38 14.18/4.38 [0] 14.18/4.38 [0] 14.18/4.38 [f] = [0] 14.18/4.38 [0] 14.18/4.38 [0] 14.18/4.38 orientation: 14.18/4.38 [1 1 0 0 0] [3] [1 1 0 0 0] [1] 14.18/4.38 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 14.18/4.38 g1(f1(g1(x))) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = g1(f1(f1(g1(x)))) 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 14.18/4.38 14.18/4.38 [1 1 1 1 1] [0] [1 0 0 0 1] 14.18/4.38 [0 0 1 1 1] [0] [0 0 0 1 1] 14.18/4.38 a(f(),x1) = [0 0 0 1 1]x1 + [0] >= [0 0 0 0 0]x1 = f1(x1) 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] 14.18/4.38 14.18/4.38 [1 1 1 1 1] [2] [1 1 0 0 0] [0] 14.18/4.38 [0 0 1 1 1] [0] [0 0 0 0 0] [0] 14.18/4.38 a(g(),x1) = [0 0 0 1 1]x1 + [0] >= [0 0 0 0 1]x1 + [0] = g1(x1) 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 14.18/4.38 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 14.18/4.38 14.18/4.38 [1 0 0 1 2] [1] [1 0 0 1 2] [1] 14.18/4.38 [0 0 0 0 0] [2] [0 0 0 0 0] [2] 14.18/4.38 f1(g1(f1(x))) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x + [0] = f1(g1(g1(f1(x)))) 14.18/4.38 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 14.18/4.38 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 14.18/4.38 problem: 14.18/4.38 strict: 14.18/4.38 14.18/4.38 weak: 14.18/4.38 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.38 a(f(),x1) -> f1(x1) 14.18/4.38 a(g(),x1) -> g1(x1) 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.38 Qed 14.18/4.38 14.18/4.38 strict: 14.18/4.38 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.39 weak: 14.18/4.39 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.39 a(f(),x1) -> f1(x1) 14.18/4.39 a(g(),x1) -> g1(x1) 14.18/4.39 Matrix Interpretation Processor: dim=4 14.18/4.39 14.18/4.39 max_matrix: 14.18/4.39 [1 1 1 1] 14.18/4.39 [0 0 1 1] 14.18/4.39 [0 0 0 1] 14.18/4.39 [0 0 0 0] 14.18/4.39 interpretation: 14.18/4.39 [1 0 1 1] 14.18/4.39 [0 0 0 1] 14.18/4.39 [g1](x0) = [0 0 0 0]x0 14.18/4.39 [0 0 0 0] , 14.18/4.39 14.18/4.39 [1 1 0 0] [0] 14.18/4.39 [0 0 1 0] [0] 14.18/4.39 [f1](x0) = [0 0 0 0]x0 + [1] 14.18/4.39 [0 0 0 0] [1], 14.18/4.39 14.18/4.39 [1 0 0 0] [1 1 1 1] [0] 14.18/4.39 [0 0 1 1] [0 0 1 1] [1] 14.18/4.39 [a](x0, x1) = [0 0 0 1]x0 + [0 0 0 0]x1 + [1] 14.18/4.39 [0 0 0 0] [0 0 0 0] [1], 14.18/4.39 14.18/4.39 [0] 14.18/4.39 [0] 14.18/4.39 [g] = [0] 14.18/4.39 [0], 14.18/4.39 14.18/4.39 [0] 14.18/4.39 [0] 14.18/4.39 [f] = [1] 14.18/4.39 [1] 14.18/4.39 orientation: 14.18/4.39 [1 1 0 0] [3] [1 1 0 0] [2] 14.18/4.39 [0 0 0 0] [0] [0 0 0 0] [0] 14.18/4.39 f1(g1(f1(x))) = [0 0 0 0]x + [1] >= [0 0 0 0]x + [1] = f1(g1(g1(f1(x)))) 14.18/4.39 [0 0 0 0] [1] [0 0 0 0] [1] 14.18/4.39 14.18/4.39 [1 0 1 2] [2] [1 0 1 2] [2] 14.18/4.39 [0 0 0 0] [1] [0 0 0 0] [1] 14.18/4.39 g1(f1(g1(x))) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = g1(f1(f1(g1(x)))) 14.18/4.39 [0 0 0 0] [0] [0 0 0 0] [0] 14.18/4.39 14.18/4.39 [1 1 1 1] [0] [1 1 0 0] [0] 14.18/4.39 [0 0 1 1] [3] [0 0 1 0] [0] 14.18/4.39 a(f(),x1) = [0 0 0 0]x1 + [2] >= [0 0 0 0]x1 + [1] = f1(x1) 14.18/4.39 [0 0 0 0] [1] [0 0 0 0] [1] 14.18/4.39 14.18/4.39 [1 1 1 1] [0] [1 0 1 1] 14.18/4.39 [0 0 1 1] [1] [0 0 0 1] 14.18/4.39 a(g(),x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 = g1(x1) 14.18/4.39 [0 0 0 0] [1] [0 0 0 0] 14.18/4.39 problem: 14.18/4.39 strict: 14.18/4.39 14.18/4.39 weak: 14.18/4.39 f1(g1(f1(x))) -> f1(g1(g1(f1(x)))) 14.18/4.39 g1(f1(g1(x))) -> g1(f1(f1(g1(x)))) 14.18/4.39 a(f(),x1) -> f1(x1) 14.18/4.39 a(g(),x1) -> g1(x1) 14.18/4.39 Qed 14.18/4.39 EOF