YES(?,O(n^2)) 32.00/12.07 YES(?,O(n^2)) 32.00/12.08 32.00/12.08 Problem: 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 32.00/12.08 Proof: 32.00/12.08 Complexity Transformation Processor: 32.00/12.08 strict: 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 weak: 32.00/12.08 32.00/12.08 Matrix Interpretation Processor: dim=1 32.00/12.08 32.00/12.08 max_matrix: 32.00/12.08 1 32.00/12.08 interpretation: 32.00/12.08 [g](x0, x1) = x0 + x1 + 11, 32.00/12.08 32.00/12.08 [f](x0, x1) = x0 + x1, 32.00/12.08 32.00/12.08 [s](x0) = x0 + 2, 32.00/12.08 32.00/12.08 [a] = 8 32.00/12.08 orientation: 32.00/12.08 s(a()) = 10 >= 8 = a() 32.00/12.08 32.00/12.08 s(s(x)) = x + 4 >= x = x 32.00/12.08 32.00/12.08 s(f(x,y)) = x + y + 2 >= x + y + 4 = f(s(y),s(x)) 32.00/12.08 32.00/12.08 s(g(x,y)) = x + y + 13 >= x + y + 15 = g(s(x),s(y)) 32.00/12.08 32.00/12.08 f(x,a()) = x + 8 >= x = x 32.00/12.08 32.00/12.08 f(a(),y) = y + 8 >= y = y 32.00/12.08 32.00/12.08 f(g(x,y),g(u,v)) = u + v + x + y + 22 >= u + v + x + y + 11 = g(f(x,u),f(y,v)) 32.00/12.08 32.00/12.08 g(a(),a()) = 27 >= 8 = a() 32.00/12.08 problem: 32.00/12.08 strict: 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 weak: 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 Splitting Processor: 32.00/12.08 strict: 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 weak: 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 Matrix Interpretation Processor: dim=2 32.00/12.08 32.00/12.08 max_matrix: 32.00/12.08 [1 3] 32.00/12.08 [0 1] 32.00/12.08 interpretation: 32.00/12.08 [1 3] [0] 32.00/12.08 [g](x0, x1) = [0 1]x0 + x1 + [2], 32.00/12.08 32.00/12.08 [1 1] [1 1] [1] 32.00/12.08 [f](x0, x1) = [0 1]x0 + [0 1]x1 + [1], 32.00/12.08 32.00/12.08 [1 2] 32.00/12.08 [s](x0) = [0 1]x0, 32.00/12.08 32.00/12.08 [0] 32.00/12.08 [a] = [2] 32.00/12.08 orientation: 32.00/12.08 [1 3] [1 3] [3] [1 3] [1 3] [1] 32.00/12.08 s(f(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(s(y),s(x)) 32.00/12.08 32.00/12.08 [1 5] [1 2] [4] [1 5] [1 2] [0] 32.00/12.08 s(g(x,y)) = [0 1]x + [0 1]y + [2] >= [0 1]x + [0 1]y + [2] = g(s(x),s(y)) 32.00/12.08 32.00/12.08 [4] [0] 32.00/12.08 s(a()) = [2] >= [2] = a() 32.00/12.08 32.00/12.08 [1 4] 32.00/12.08 s(s(x)) = [0 1]x >= x = x 32.00/12.08 32.00/12.08 [1 1] [3] 32.00/12.08 f(x,a()) = [0 1]x + [3] >= x = x 32.00/12.08 32.00/12.08 [1 1] [3] 32.00/12.08 f(a(),y) = [0 1]y + [3] >= y = y 32.00/12.08 32.00/12.08 [1 4] [1 1] [1 4] [1 1] [5] [1 4] [1 1] [1 4] [1 1] [5] 32.00/12.08 f(g(x,y),g(u,v)) = [0 1]u + [0 1]v + [0 1]x + [0 1]y + [5] >= [0 1]u + [0 1]v + [0 1]x + [0 1]y + [4] = g(f(x,u),f(y,v)) 32.00/12.08 32.00/12.08 [6] [0] 32.00/12.08 g(a(),a()) = [6] >= [2] = a() 32.00/12.08 problem: 32.00/12.08 strict: 32.00/12.08 32.00/12.08 weak: 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 Qed 32.00/12.08 32.00/12.08 strict: 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 weak: 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 Matrix Interpretation Processor: dim=2 32.00/12.08 32.00/12.08 max_matrix: 32.00/12.08 [1 1] 32.00/12.08 [0 1] 32.00/12.08 interpretation: 32.00/12.08 [1 1] [0] 32.00/12.08 [g](x0, x1) = x0 + [0 1]x1 + [1], 32.00/12.08 32.00/12.08 [1 1] [1 1] [0] 32.00/12.08 [f](x0, x1) = [0 1]x0 + [0 1]x1 + [1], 32.00/12.08 32.00/12.08 [1 1] 32.00/12.08 [s](x0) = [0 1]x0, 32.00/12.08 32.00/12.08 [3] 32.00/12.08 [a] = [2] 32.00/12.08 orientation: 32.00/12.08 [1 1] [1 2] [1] [1 1] [1 2] [0] 32.00/12.08 s(g(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(s(x),s(y)) 32.00/12.08 32.00/12.08 [5] [3] 32.00/12.08 s(a()) = [2] >= [2] = a() 32.00/12.08 32.00/12.08 [1 2] 32.00/12.08 s(s(x)) = [0 1]x >= x = x 32.00/12.08 32.00/12.08 [1 1] [5] 32.00/12.08 f(x,a()) = [0 1]x + [3] >= x = x 32.00/12.08 32.00/12.08 [1 1] [5] 32.00/12.08 f(a(),y) = [0 1]y + [3] >= y = y 32.00/12.08 32.00/12.08 [1 1] [1 2] [1 1] [1 2] [2] [1 1] [1 2] [1 1] [1 2] [1] 32.00/12.08 f(g(x,y),g(u,v)) = [0 1]u + [0 1]v + [0 1]x + [0 1]y + [3] >= [0 1]u + [0 1]v + [0 1]x + [0 1]y + [3] = g(f(x,u),f(y,v)) 32.00/12.08 32.00/12.08 [8] [3] 32.00/12.08 g(a(),a()) = [5] >= [2] = a() 32.00/12.08 32.00/12.08 [1 2] [1 2] [1] [1 2] [1 2] [0] 32.00/12.08 s(f(x,y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(s(y),s(x)) 32.00/12.08 problem: 32.00/12.08 strict: 32.00/12.08 32.00/12.08 weak: 32.00/12.08 s(g(x,y)) -> g(s(x),s(y)) 32.00/12.08 s(a()) -> a() 32.00/12.08 s(s(x)) -> x 32.00/12.08 f(x,a()) -> x 32.00/12.08 f(a(),y) -> y 32.00/12.08 f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) 32.00/12.08 g(a(),a()) -> a() 32.00/12.08 s(f(x,y)) -> f(s(y),s(x)) 32.00/12.08 Qed 32.00/12.08 EOF