MAYBE
Problem:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
Proof:
RT Transformation Processor:
strict:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
+(0(),y) -> y
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(g(h(x,y))) -> f(h(s(x),y))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
weak:
Matrix Interpretation Processor:
dimension: 1
interpretation:
[h](x0, x1) = x0 + x1 + 10,
[g](x0) = x0 + 23,
[f](x0) = x0 + 1,
[s](x0) = x0 + 9,
[+](x0, x1) = x0 + x1 + 21,
[0] = 13
orientation:
+(x,0()) = x + 34 >= x = x
+(x,s(y)) = x + y + 30 >= x + y + 30 = s(+(x,y))
+(0(),y) = y + 34 >= y = y
+(s(x),y) = x + y + 30 >= x + y + 30 = s(+(x,y))
+(x,+(y,z)) = x + y + z + 42 >= x + y + z + 42 = +(+(x,y),z)
f(g(f(x))) = x + 25 >= x + 33 = f(h(s(0()),x))
f(g(h(x,y))) = x + y + 34 >= x + y + 20 = f(h(s(x),y))
f(h(x,h(y,z))) = x + y + z + 21 >= x + y + z + 32 = f(h(+(x,y),z))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
weak:
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
Matrix Interpretation Processor:
dimension: 1
interpretation:
[h](x0, x1) = x0 + x1 + 19,
[g](x0) = x0 + 1,
[f](x0) = x0 + 17,
[s](x0) = x0 + 1,
[+](x0, x1) = x0 + x1 + 16,
[0] = 13
orientation:
+(x,s(y)) = x + y + 17 >= x + y + 17 = s(+(x,y))
+(s(x),y) = x + y + 17 >= x + y + 17 = s(+(x,y))
+(x,+(y,z)) = x + y + z + 32 >= x + y + z + 32 = +(+(x,y),z)
f(g(f(x))) = x + 35 >= x + 50 = f(h(s(0()),x))
f(h(x,h(y,z))) = x + y + z + 55 >= x + y + z + 52 = f(h(+(x,y),z))
+(x,0()) = x + 29 >= x = x
+(0(),y) = y + 29 >= y = y
f(g(h(x,y))) = x + y + 37 >= x + y + 37 = f(h(s(x),y))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
weak:
f(h(x,h(y,z))) -> f(h(+(x,y),z))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
Matrix Interpretation Processor:
dimension: 1
interpretation:
[h](x0, x1) = x0 + x1 + 9,
[g](x0) = x0 + 26,
[f](x0) = x0 + 18,
[s](x0) = x0 + 4,
[+](x0, x1) = x0 + x1,
[0] = 30
orientation:
+(x,s(y)) = x + y + 4 >= x + y + 4 = s(+(x,y))
+(s(x),y) = x + y + 4 >= x + y + 4 = s(+(x,y))
+(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z)
f(g(f(x))) = x + 62 >= x + 61 = f(h(s(0()),x))
f(h(x,h(y,z))) = x + y + z + 36 >= x + y + z + 27 = f(h(+(x,y),z))
+(x,0()) = x + 30 >= x = x
+(0(),y) = y + 30 >= y = y
f(g(h(x,y))) = x + y + 53 >= x + y + 31 = f(h(s(x),y))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
weak:
f(g(f(x))) -> f(h(s(0()),x))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 2] [0]
[h](x0, x1) = x0 + [0 1]x1 + [7],
[1 2] [9]
[g](x0) = [0 1]x0 + [9],
[0]
[f](x0) = x0 + [8],
[2]
[s](x0) = x0 + [0],
[1 1] [0]
[+](x0, x1) = x0 + [0 1]x1 + [2],
[0]
[0] = [5]
orientation:
[1 1] [2] [1 1] [2]
+(x,s(y)) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))
[1 1] [2] [1 1] [2]
+(s(x),y) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(x,y))
[1 1] [1 2] [2] [1 1] [1 1] [0]
+(x,+(y,z)) = x + [0 1]y + [0 1]z + [4] >= x + [0 1]y + [0 1]z + [4] = +(+(x,y),z)
[1 2] [25] [1 2] [2 ]
f(g(f(x))) = [0 1]x + [25] >= [0 1]x + [20] = f(h(s(0()),x))
[1 2] [1 4] [14] [1 1] [1 2] [0 ]
f(h(x,h(y,z))) = x + [0 1]y + [0 1]z + [22] >= x + [0 1]y + [0 1]z + [17] = f(h(+(x,y),z))
[5]
+(x,0()) = x + [7] >= x = x
[1 1] [0]
+(0(),y) = [0 1]y + [7] >= y = y
[1 2] [1 4] [23] [1 2] [2 ]
f(g(h(x,y))) = [0 1]x + [0 1]y + [24] >= x + [0 1]y + [15] = f(h(s(x),y))
problem:
strict:
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
weak:
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 4] [3]
[h](x0, x1) = x0 + [0 1]x1 + [0],
[1 1] [12]
[g](x0) = [0 1]x0 + [4 ],
[1 4]
[f](x0) = [0 1]x0,
[0]
[s](x0) = x0 + [1],
[1 4] [1]
[+](x0, x1) = x0 + [0 1]x1 + [0],
[13]
[0] = [2 ]
orientation:
[1 4] [5] [1 4] [1]
+(x,s(y)) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
[1 4] [1] [1 4] [1]
+(s(x),y) = x + [0 1]y + [1] >= x + [0 1]y + [1] = s(+(x,y))
[1 4] [1 8] [2] [1 4] [1 4] [2]
+(x,+(y,z)) = x + [0 1]y + [0 1]z + [0] >= x + [0 1]y + [0 1]z + [0] = +(+(x,y),z)
[1 9] [28] [1 8] [28]
f(g(f(x))) = [0 1]x + [4 ] >= [0 1]x + [3 ] = f(h(s(0()),x))
[1 4] [1 8] [1 12] [6] [1 4] [1 8] [1 8] [4]
f(h(x,h(y,z))) = [0 1]x + [0 1]y + [0 1 ]z + [0] >= [0 1]x + [0 1]y + [0 1]z + [0] = f(h(+(x,y),z))
[22]
+(x,0()) = x + [2 ] >= x = x
[1 4] [14]
+(0(),y) = [0 1]y + [2 ] >= y = y
[1 5] [1 9] [31] [1 4] [1 8] [7]
f(g(h(x,y))) = [0 1]x + [0 1]y + [4 ] >= [0 1]x + [0 1]y + [1] = f(h(s(x),y))
problem:
strict:
+(s(x),y) -> s(+(x,y))
weak:
+(x,s(y)) -> s(+(x,y))
+(x,+(y,z)) -> +(+(x,y),z)
f(g(f(x))) -> f(h(s(0()),x))
f(h(x,h(y,z))) -> f(h(+(x,y),z))
+(x,0()) -> x
+(0(),y) -> y
f(g(h(x,y))) -> f(h(s(x),y))
Open