YES(?,O(n^2)) 53.81/26.35 YES(?,O(n^2)) 53.81/26.35 53.81/26.35 Problem: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 53.81/26.35 Proof: 53.81/26.35 Complexity Transformation Processor: 53.81/26.35 strict: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 weak: 53.81/26.35 53.81/26.35 Matrix Interpretation Processor: dim=1 53.81/26.35 53.81/26.35 max_matrix: 53.81/26.35 1 53.81/26.35 interpretation: 53.81/26.35 [mark](x0) = x0 + 200, 53.81/26.35 53.81/26.35 [g](x0) = x0 + 84, 53.81/26.35 53.81/26.35 [a__f](x0) = x0 + 127, 53.81/26.35 53.81/26.35 [f](x0) = x0 + 56, 53.81/26.35 53.81/26.35 [a] = 121 53.81/26.35 orientation: 53.81/26.35 a__f(f(a())) = 304 >= 388 = a__f(g(f(a()))) 53.81/26.35 53.81/26.35 mark(f(X)) = X + 256 >= X + 127 = a__f(X) 53.81/26.35 53.81/26.35 mark(a()) = 321 >= 121 = a() 53.81/26.35 53.81/26.35 mark(g(X)) = X + 284 >= X + 284 = g(mark(X)) 53.81/26.35 53.81/26.35 a__f(X) = X + 127 >= X + 56 = f(X) 53.81/26.35 problem: 53.81/26.35 strict: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 weak: 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 Splitting Processor: 53.81/26.35 strict: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 weak: 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 Matrix Interpretation Processor: dim=5 53.81/26.35 53.81/26.35 max_matrix: 53.81/26.35 [1 0 0 0 1] 53.81/26.35 [0 0 0 0 0] 53.81/26.35 [0 0 0 0 0] 53.81/26.35 [0 0 0 0 0] 53.81/26.35 [0 0 0 0 0] 53.81/26.35 interpretation: 53.81/26.35 [1 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1] 53.81/26.35 [mark](x0) = [0 0 0 0 0]x0 + [1] 53.81/26.35 [0 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1], 53.81/26.35 53.81/26.35 [1 0 0 0 0] 53.81/26.35 [0 0 0 0 0] 53.81/26.35 [g](x0) = [0 0 0 0 0]x0 53.81/26.35 [0 0 0 0 0] 53.81/26.35 [0 0 0 0 0] , 53.81/26.35 53.81/26.35 [1 0 0 0 1] [0] 53.81/26.35 [0 0 0 0 0] [0] 53.81/26.35 [a__f](x0) = [0 0 0 0 0]x0 + [1] 53.81/26.35 [0 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1], 53.81/26.35 53.81/26.35 [1 0 0 0 1] [0] 53.81/26.35 [0 0 0 0 0] [0] 53.81/26.35 [f](x0) = [0 0 0 0 0]x0 + [0] 53.81/26.35 [0 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1], 53.81/26.35 53.81/26.35 [0] 53.81/26.35 [0] 53.81/26.35 [a] = [0] 53.81/26.35 [0] 53.81/26.35 [0] 53.81/26.35 orientation: 53.81/26.35 [1] [0] 53.81/26.35 [0] [0] 53.81/26.35 a__f(f(a())) = [1] >= [1] = a__f(g(f(a()))) 53.81/26.35 [0] [0] 53.81/26.35 [1] [1] 53.81/26.35 53.81/26.35 [1 0 0 0 1] [0] [1 0 0 0 1] [0] 53.81/26.35 [0 0 0 0 0] [1] [0 0 0 0 0] [0] 53.81/26.35 mark(f(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [1] = a__f(X) 53.81/26.35 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 53.81/26.35 53.81/26.35 [0] [0] 53.81/26.35 [1] [0] 53.81/26.35 mark(a()) = [1] >= [0] = a() 53.81/26.35 [0] [0] 53.81/26.35 [1] [0] 53.81/26.35 53.81/26.35 [1 0 0 0 1] [0] [1 0 0 0 1] [0] 53.81/26.35 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 53.81/26.35 a__f(X) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X + [0] = f(X) 53.81/26.35 [0 0 0 0 0] [0] [0 0 0 0 0] [0] 53.81/26.35 [0 0 0 0 0] [1] [0 0 0 0 0] [1] 53.81/26.35 53.81/26.35 [1 0 0 0 0] [0] [1 0 0 0 0] 53.81/26.35 [0 0 0 0 0] [1] [0 0 0 0 0] 53.81/26.35 mark(g(X)) = [0 0 0 0 0]X + [1] >= [0 0 0 0 0]X = g(mark(X)) 53.81/26.35 [0 0 0 0 0] [0] [0 0 0 0 0] 53.81/26.35 [0 0 0 0 0] [1] [0 0 0 0 0] 53.81/26.35 problem: 53.81/26.35 strict: 53.81/26.35 53.81/26.35 weak: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 Qed 53.81/26.35 53.81/26.35 strict: 53.81/26.35 mark(g(X)) -> g(mark(X)) 53.81/26.35 weak: 53.81/26.35 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.35 mark(f(X)) -> a__f(X) 53.81/26.35 mark(a()) -> a() 53.81/26.35 a__f(X) -> f(X) 53.81/26.35 Matrix Interpretation Processor: dim=2 53.81/26.35 53.81/26.35 max_matrix: 53.81/26.35 [1 4] 53.81/26.35 [0 1] 53.81/26.35 interpretation: 53.81/26.36 [1 4] [0] 53.81/26.36 [mark](x0) = [0 1]x0 + [4], 53.81/26.36 53.81/26.36 [0] 53.81/26.36 [g](x0) = x0 + [1], 53.81/26.36 53.81/26.36 [1 0] 53.81/26.36 [a__f](x0) = [0 0]x0, 53.81/26.36 53.81/26.36 [1 0] 53.81/26.36 [f](x0) = [0 0]x0, 53.81/26.36 53.81/26.36 [1] 53.81/26.36 [a] = [1] 53.81/26.36 orientation: 53.81/26.36 [1 4] [4] [1 4] [0] 53.81/26.36 mark(g(X)) = [0 1]X + [5] >= [0 1]X + [5] = g(mark(X)) 53.81/26.36 53.81/26.36 [1] [1] 53.81/26.36 a__f(f(a())) = [0] >= [0] = a__f(g(f(a()))) 53.81/26.36 53.81/26.36 [1 0] [0] [1 0] 53.81/26.36 mark(f(X)) = [0 0]X + [4] >= [0 0]X = a__f(X) 53.81/26.36 53.81/26.36 [5] [1] 53.81/26.36 mark(a()) = [5] >= [1] = a() 53.81/26.36 53.81/26.36 [1 0] [1 0] 53.81/26.36 a__f(X) = [0 0]X >= [0 0]X = f(X) 53.81/26.36 problem: 53.81/26.36 strict: 53.81/26.36 53.81/26.36 weak: 53.81/26.36 mark(g(X)) -> g(mark(X)) 53.81/26.36 a__f(f(a())) -> a__f(g(f(a()))) 53.81/26.36 mark(f(X)) -> a__f(X) 53.81/26.36 mark(a()) -> a() 53.81/26.36 a__f(X) -> f(X) 53.81/26.36 Qed 53.81/26.36 EOF