MAYBE Problem: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) Proof: RT Transformation Processor: strict: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(s(f(x))) -> h(f(x)) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [c] = 8, [h](x0) = x0, [s](x0) = x0 + 8, [f](x0) = x0, [g](x0, x1) = x0 + x1, [b] = 0, [a] = 0, [i](x0, x1) = x0 + x1 orientation: i(x,x) = 2x >= 0 = i(a(),b()) g(x,x) = 2x >= 0 = g(a(),b()) h(s(f(x))) = x + 8 >= x = h(f(x)) f(s(x)) = x + 8 >= x + 24 = s(s(f(h(s(x))))) f(g(s(x),y)) = x + y + 8 >= x + y + 8 = f(g(x,s(y))) h(g(x,s(y))) = x + y + 8 >= x + y + 8 = h(g(s(x),y)) h(i(x,y)) = x + y >= x + y + 8 = i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) = 2x + y >= x + y = g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) problem: strict: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) f(s(x)) -> s(s(f(h(s(x))))) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) weak: h(s(f(x))) -> h(f(x)) Matrix Interpretation Processor: dimension: 2 interpretation: [0] [c] = [0], [1 0] [h](x0) = [0 0]x0, [1 0] [0] [s](x0) = [0 0]x0 + [6], [1 3] [8] [f](x0) = [0 1]x0 + [0], [1 0] [1 0] [g](x0, x1) = [0 0]x0 + [0 0]x1, [0] [b] = [0], [0] [a] = [0], [1 12] [1 0] [i](x0, x1) = [0 0 ]x0 + [0 0]x1 orientation: [2 12] [0] i(x,x) = [0 0 ]x >= [0] = i(a(),b()) [2 0] [0] g(x,x) = [0 0]x >= [0] = g(a(),b()) [1 0] [26] [1 0] [8] f(s(x)) = [0 0]x + [6 ] >= [0 0]x + [6] = s(s(f(h(s(x))))) [1 0] [1 0] [8] [1 0] [1 0] [8] f(g(s(x),y)) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = f(g(x,s(y))) [1 0] [1 0] [1 0] [1 0] h(g(x,s(y))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = h(g(s(x),y)) [1 12] [1 0] [1 0] [1 0] h(i(x,y)) = [0 0 ]x + [0 0]y >= [0 0]x + [0 0]y = i(i(c(),h(h(y))),x) [2 0] [1 0] [1 0] [1 0] g(a(),g(x,g(b(),g(a(),g(x,y))))) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) [1 3] [8] [1 3] [8] h(s(f(x))) = [0 0]x + [0] >= [0 0]x + [0] = h(f(x)) problem: strict: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) f(g(s(x),y)) -> f(g(x,s(y))) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) weak: f(s(x)) -> s(s(f(h(s(x))))) h(s(f(x))) -> h(f(x)) Matrix Interpretation Processor: dimension: 3 interpretation: [0] [c] = [1] [0], [1 0 0] [0] [h](x0) = [0 0 0]x0 + [1] [0 0 0] [0], [1 0 0] [0] [s](x0) = [0 1 2]x0 + [0] [0 0 0] [2], [1 4 4] [0] [f](x0) = [0 0 4]x0 + [0] [0 0 0] [2], [1 0 0] [1 0 0] [g](x0, x1) = [0 1 1]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [b] = [0] [0], [0] [a] = [0] [0], [1 0 0] [1 0 0] [i](x0, x1) = [0 1 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] orientation: [2 0 0] [0] i(x,x) = [0 1 0]x >= [0] = i(a(),b()) [0 0 0] [0] [2 0 0] [0] g(x,x) = [0 1 1]x >= [0] = g(a(),b()) [0 0 0] [0] [1 4 8] [1 0 0] [8] [1 4 4] [1 0 0] [0] f(g(s(x),y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = f(g(x,s(y))) [0 0 0] [0 0 0] [2] [0 0 0] [0 0 0] [2] [1 0 0] [1 0 0] [0] [1 0 0] [1 0 0] [0] h(g(x,s(y))) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [1] = h(g(s(x),y)) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 0 0] [1 0 0] [0] [1 0 0] [1 0 0] [0] h(i(x,y)) = [0 0 0]x + [0 0 0]y + [1] >= [0 0 0]x + [0 0 0]y + [1] = i(i(c(),h(h(y))),x) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [2 0 0] [1 0 0] [1 0 0] [1 0 0] g(a(),g(x,g(b(),g(a(),g(x,y))))) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 4 8] [8] [1 0 0] [4] f(s(x)) = [0 0 0]x + [8] >= [0 0 0]x + [8] = s(s(f(h(s(x))))) [0 0 0] [2] [0 0 0] [2] [1 4 4] [0] [1 4 4] [0] h(s(f(x))) = [0 0 0]x + [1] >= [0 0 0]x + [1] = h(f(x)) [0 0 0] [0] [0 0 0] [0] problem: strict: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(g(x,s(y))) -> h(g(s(x),y)) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) weak: f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) h(s(f(x))) -> h(f(x)) Matrix Interpretation Processor: dimension: 3 interpretation: [0] [c] = [0] [4], [1 0 0] [h](x0) = [0 0 0]x0 [0 0 0] , [1 0 0] [0] [s](x0) = [0 1 0]x0 + [1] [0 0 0] [4], [1 2 1] [4] [f](x0) = [0 0 2]x0 + [7] [0 0 1] [0], [1 0 0] [1 1 0] [g](x0, x1) = [0 1 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [b] = [0] [0], [0] [a] = [0] [0], [1 0 0] [1 0 0] [i](x0, x1) = [0 0 2]x0 + [0 0 0]x1 [0 0 0] [0 0 0] orientation: [2 0 0] [0] i(x,x) = [0 0 2]x >= [0] = i(a(),b()) [0 0 0] [0] [2 1 0] [0] g(x,x) = [0 1 0]x >= [0] = g(a(),b()) [0 0 0] [0] [1 0 0] [1 1 0] [1] [1 0 0] [1 1 0] h(g(x,s(y))) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y = h(g(s(x),y)) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] h(i(x,y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = i(i(c(),h(h(y))),x) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [2 2 0] [1 1 0] [1 1 0] [1 1 0] g(a(),g(x,g(b(),g(a(),g(x,y))))) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 2 0] [1 1 0] [6] [1 2 0] [1 1 0] [5] f(g(s(x),y)) = [0 0 0]x + [0 0 0]y + [7] >= [0 0 0]x + [0 0 0]y + [7] = f(g(x,s(y))) [0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0] [1 2 0] [10] [1 0 0] [4] f(s(x)) = [0 0 0]x + [15] >= [0 0 0]x + [9] = s(s(f(h(s(x))))) [0 0 0] [4 ] [0 0 0] [4] [1 2 1] [4] [1 2 1] [4] h(s(f(x))) = [0 0 0]x + [0] >= [0 0 0]x + [0] = h(f(x)) [0 0 0] [0] [0 0 0] [0] problem: strict: i(x,x) -> i(a(),b()) g(x,x) -> g(a(),b()) h(i(x,y)) -> i(i(c(),h(h(y))),x) g(a(),g(x,g(b(),g(a(),g(x,y))))) -> g(a(),g(a(),g(a(),g(x,g(b(),g(b(),y)))))) weak: h(g(x,s(y))) -> h(g(s(x),y)) f(g(s(x),y)) -> f(g(x,s(y))) f(s(x)) -> s(s(f(h(s(x))))) h(s(f(x))) -> h(f(x)) Open