YES(?,O(n^2)) Problem: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x Proof: Complexity Transformation Processor: strict: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) f(x) -> x weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [d](x0) = x0 + 1, [f](x0) = x0 + 1, [g](x0) = x0, [c](x0, x1) = x0 + x1, [s](x0) = x0 orientation: g(c(x,s(y))) = x + y >= x + y = g(c(s(x),y)) f(c(s(x),y)) = x + y + 1 >= x + y + 1 = f(c(x,s(y))) f(f(x)) = x + 2 >= x + 3 = f(d(f(x))) f(x) = x + 1 >= x = x problem: strict: g(c(x,s(y))) -> g(c(s(x),y)) f(c(s(x),y)) -> f(c(x,s(y))) f(f(x)) -> f(d(f(x))) weak: f(x) -> x Bounds Processor: bound: 1 enrichment: match automaton: final states: {6} transitions: g1(42) -> 6* c1(13,13) -> 42* c1(13,6) -> 42* c1(6,13) -> 14* s1(6) -> 13* s1(13) -> 13* f1(14) -> 6* f1(6) -> 6* d1(6) -> 14* g0(6) -> 6* c0(6,6) -> 6* s0(6) -> 6* f0(6) -> 6* d0(6) -> 6* 14 -> 6* problem: strict: g(c(x,s(y))) -> g(c(s(x),y)) f(f(x)) -> f(d(f(x))) weak: f(c(s(x),y)) -> f(c(x,s(y))) f(x) -> x Bounds Processor: bound: 2 enrichment: match automaton: final states: {6} transitions: c1(6,35) -> 15* s1(35) -> 35* s1(6) -> 35* f1(15) -> 16* f1(17) -> 18* d1(19) -> 20* d1(16) -> 17* f2(27) -> 28* f2(29) -> 30* g0(6) -> 6* d2(28) -> 29* c0(6,6) -> 6* s0(6) -> 6* f0(6) -> 6* d0(6) -> 6* 6 -> 15* 15 -> 16* 17 -> 18,27 18 -> 16,19,6 20 -> 17* 27 -> 28* 29 -> 30* 30 -> 16* problem: strict: g(c(x,s(y))) -> g(c(s(x),y)) weak: f(f(x)) -> f(d(f(x))) f(c(s(x),y)) -> f(c(x,s(y))) f(x) -> x Matrix Interpretation Processor: dimension: 2 max_matrix: [1 1] [0 1] interpretation: [d](x0) = x0, [1 1] [f](x0) = [0 1]x0, [1 0] [g](x0) = [0 0]x0, [1 1] [0] [c](x0, x1) = x0 + [0 0]x1 + [1], [0] [s](x0) = x0 + [1] orientation: [1 0] [1 1] [1] [1 0] [1 1] g(c(x,s(y))) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y = g(c(s(x),y)) [1 2] [1 2] f(f(x)) = [0 1]x >= [0 1]x = f(d(f(x))) [1 1] [1 1] [2] [1 1] [1 1] [2] f(c(s(x),y)) = [0 1]x + [0 0]y + [2] >= [0 1]x + [0 0]y + [1] = f(c(x,s(y))) [1 1] f(x) = [0 1]x >= x = x problem: strict: weak: g(c(x,s(y))) -> g(c(s(x),y)) f(f(x)) -> f(d(f(x))) f(c(s(x),y)) -> f(c(x,s(y))) f(x) -> x Qed