MAYBE Problem: +(p1(),p1()) -> p2() +(p1(),+(p2(),p2())) -> p5() +(p5(),p5()) -> p10() +(+(x,y),z) -> +(x,+(y,z)) +(p1(),+(p1(),x)) -> +(p2(),x) +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),p1()) -> +(p1(),p2()) +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p5(),p1()) -> +(p1(),p5()) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p5(),+(p5(),x)) -> +(p10(),x) +(p10(),p1()) -> +(p1(),p10()) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) Proof: RT Transformation Processor: strict: +(p1(),p1()) -> p2() +(p1(),+(p2(),p2())) -> p5() +(p5(),p5()) -> p10() +(+(x,y),z) -> +(x,+(y,z)) +(p1(),+(p1(),x)) -> +(p2(),x) +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),p1()) -> +(p1(),p2()) +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p5(),p1()) -> +(p1(),p5()) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p5(),+(p5(),x)) -> +(p10(),x) +(p10(),p1()) -> +(p1(),p10()) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: Matrix Interpretation Processor: dimension: 1 interpretation: [p10] = 7, [p5] = 18, [p2] = 0, [+](x0, x1) = x0 + x1 + 3, [p1] = 2 orientation: +(p1(),p1()) = 7 >= 0 = p2() +(p1(),+(p2(),p2())) = 8 >= 18 = p5() +(p5(),p5()) = 39 >= 7 = p10() +(+(x,y),z) = x + y + z + 6 >= x + y + z + 6 = +(x,+(y,z)) +(p1(),+(p1(),x)) = x + 10 >= x + 3 = +(p2(),x) +(p1(),+(p2(),+(p2(),x))) = x + 11 >= x + 21 = +(p5(),x) +(p2(),p1()) = 5 >= 5 = +(p1(),p2()) +(p2(),+(p1(),x)) = x + 8 >= x + 8 = +(p1(),+(p2(),x)) +(p2(),+(p2(),p2())) = 6 >= 23 = +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) = x + 9 >= x + 26 = +(p1(),+(p5(),x)) +(p5(),p1()) = 23 >= 23 = +(p1(),p5()) +(p5(),+(p1(),x)) = x + 26 >= x + 26 = +(p1(),+(p5(),x)) +(p5(),p2()) = 21 >= 21 = +(p2(),p5()) +(p5(),+(p2(),x)) = x + 24 >= x + 24 = +(p2(),+(p5(),x)) +(p5(),+(p5(),x)) = x + 42 >= x + 10 = +(p10(),x) +(p10(),p1()) = 12 >= 12 = +(p1(),p10()) +(p10(),+(p1(),x)) = x + 15 >= x + 15 = +(p1(),+(p10(),x)) +(p10(),p2()) = 10 >= 10 = +(p2(),p10()) +(p10(),+(p2(),x)) = x + 13 >= x + 13 = +(p2(),+(p10(),x)) +(p10(),p5()) = 28 >= 28 = +(p5(),p10()) +(p10(),+(p5(),x)) = x + 31 >= x + 31 = +(p5(),+(p10(),x)) problem: strict: +(p1(),+(p2(),p2())) -> p5() +(+(x,y),z) -> +(x,+(y,z)) +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),p1()) -> +(p1(),p2()) +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p5(),p1()) -> +(p1(),p5()) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p10(),p1()) -> +(p1(),p10()) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: +(p1(),p1()) -> p2() +(p5(),p5()) -> p10() +(p1(),+(p1(),x)) -> +(p2(),x) +(p5(),+(p5(),x)) -> +(p10(),x) Matrix Interpretation Processor: dimension: 1 interpretation: [p10] = 0, [p5] = 0, [p2] = 6, [+](x0, x1) = x0 + x1 + 1, [p1] = 8 orientation: +(p1(),+(p2(),p2())) = 22 >= 0 = p5() +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(p1(),+(p2(),+(p2(),x))) = x + 23 >= x + 1 = +(p5(),x) +(p2(),p1()) = 15 >= 15 = +(p1(),p2()) +(p2(),+(p1(),x)) = x + 16 >= x + 16 = +(p1(),+(p2(),x)) +(p2(),+(p2(),p2())) = 20 >= 9 = +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) = x + 21 >= x + 10 = +(p1(),+(p5(),x)) +(p5(),p1()) = 9 >= 9 = +(p1(),p5()) +(p5(),+(p1(),x)) = x + 10 >= x + 10 = +(p1(),+(p5(),x)) +(p5(),p2()) = 7 >= 7 = +(p2(),p5()) +(p5(),+(p2(),x)) = x + 8 >= x + 8 = +(p2(),+(p5(),x)) +(p10(),p1()) = 9 >= 9 = +(p1(),p10()) +(p10(),+(p1(),x)) = x + 10 >= x + 10 = +(p1(),+(p10(),x)) +(p10(),p2()) = 7 >= 7 = +(p2(),p10()) +(p10(),+(p2(),x)) = x + 8 >= x + 8 = +(p2(),+(p10(),x)) +(p10(),p5()) = 1 >= 1 = +(p5(),p10()) +(p10(),+(p5(),x)) = x + 2 >= x + 2 = +(p5(),+(p10(),x)) +(p1(),p1()) = 17 >= 6 = p2() +(p5(),p5()) = 1 >= 0 = p10() +(p1(),+(p1(),x)) = x + 18 >= x + 7 = +(p2(),x) +(p5(),+(p5(),x)) = x + 2 >= x + 1 = +(p10(),x) problem: strict: +(+(x,y),z) -> +(x,+(y,z)) +(p2(),p1()) -> +(p1(),p2()) +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p5(),p1()) -> +(p1(),p5()) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p10(),p1()) -> +(p1(),p10()) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: +(p1(),+(p2(),p2())) -> p5() +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p1(),p1()) -> p2() +(p5(),p5()) -> p10() +(p1(),+(p1(),x)) -> +(p2(),x) +(p5(),+(p5(),x)) -> +(p10(),x) Matrix Interpretation Processor: dimension: 2 interpretation: [0] [p10] = [0], [0] [p5] = [0], [0] [p2] = [0], [1 0] [1 8] [+](x0, x1) = [0 0]x0 + [0 0]x1, [0] [p1] = [1] orientation: [1 0] [1 8] [1 8] [1 0] [1 0] [1 8] +(+(x,y),z) = [0 0]x + [0 0]y + [0 0]z >= [0 0]x + [0 0]y + [0 0]z = +(x,+(y,z)) [8] [0] +(p2(),p1()) = [0] >= [0] = +(p1(),p2()) [1 8] [1 8] +(p2(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p2(),x)) [8] [0] +(p5(),p1()) = [0] >= [0] = +(p1(),p5()) [1 8] [1 8] +(p5(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x)) [0] [0] +(p5(),p2()) = [0] >= [0] = +(p2(),p5()) [1 8] [1 8] +(p5(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p5(),x)) [8] [0] +(p10(),p1()) = [0] >= [0] = +(p1(),p10()) [1 8] [1 8] +(p10(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p1(),+(p10(),x)) [0] [0] +(p10(),p2()) = [0] >= [0] = +(p2(),p10()) [1 8] [1 8] +(p10(),+(p2(),x)) = [0 0]x >= [0 0]x = +(p2(),+(p10(),x)) [0] [0] +(p10(),p5()) = [0] >= [0] = +(p5(),p10()) [1 8] [1 8] +(p10(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p5(),+(p10(),x)) [0] [0] +(p1(),+(p2(),p2())) = [0] >= [0] = p5() [1 8] [1 8] +(p1(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p5(),x) [0] [0] +(p2(),+(p2(),p2())) = [0] >= [0] = +(p1(),p5()) [1 8] [1 8] +(p2(),+(p2(),+(p2(),x))) = [0 0]x >= [0 0]x = +(p1(),+(p5(),x)) [8] [0] +(p1(),p1()) = [0] >= [0] = p2() [0] [0] +(p5(),p5()) = [0] >= [0] = p10() [1 8] [1 8] +(p1(),+(p1(),x)) = [0 0]x >= [0 0]x = +(p2(),x) [1 8] [1 8] +(p5(),+(p5(),x)) = [0 0]x >= [0 0]x = +(p10(),x) problem: strict: +(+(x,y),z) -> +(x,+(y,z)) +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: +(p2(),p1()) -> +(p1(),p2()) +(p5(),p1()) -> +(p1(),p5()) +(p10(),p1()) -> +(p1(),p10()) +(p1(),+(p2(),p2())) -> p5() +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p1(),p1()) -> p2() +(p5(),p5()) -> p10() +(p1(),+(p1(),x)) -> +(p2(),x) +(p5(),+(p5(),x)) -> +(p10(),x) Matrix Interpretation Processor: dimension: 2 interpretation: [0] [p10] = [0], [0] [p5] = [0], [0] [p2] = [0], [1 12] [0] [+](x0, x1) = [0 1 ]x0 + x1 + [1], [0] [p1] = [0] orientation: [1 24] [1 12] [12] [1 12] [1 12] [0] +(+(x,y),z) = [0 1 ]x + [0 1 ]y + z + [2 ] >= [0 1 ]x + [0 1 ]y + z + [2] = +(x,+(y,z)) [0] [0] +(p2(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p2(),x)) [0] [0] +(p5(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p5(),x)) [0] [0] +(p5(),p2()) = [1] >= [1] = +(p2(),p5()) [0] [0] +(p5(),+(p2(),x)) = x + [2] >= x + [2] = +(p2(),+(p5(),x)) [0] [0] +(p10(),+(p1(),x)) = x + [2] >= x + [2] = +(p1(),+(p10(),x)) [0] [0] +(p10(),p2()) = [1] >= [1] = +(p2(),p10()) [0] [0] +(p10(),+(p2(),x)) = x + [2] >= x + [2] = +(p2(),+(p10(),x)) [0] [0] +(p10(),p5()) = [1] >= [1] = +(p5(),p10()) [0] [0] +(p10(),+(p5(),x)) = x + [2] >= x + [2] = +(p5(),+(p10(),x)) [0] [0] +(p2(),p1()) = [1] >= [1] = +(p1(),p2()) [0] [0] +(p5(),p1()) = [1] >= [1] = +(p1(),p5()) [0] [0] +(p10(),p1()) = [1] >= [1] = +(p1(),p10()) [0] [0] +(p1(),+(p2(),p2())) = [2] >= [0] = p5() [0] [0] +(p1(),+(p2(),+(p2(),x))) = x + [3] >= x + [1] = +(p5(),x) [0] [0] +(p2(),+(p2(),p2())) = [2] >= [1] = +(p1(),p5()) [0] [0] +(p2(),+(p2(),+(p2(),x))) = x + [3] >= x + [2] = +(p1(),+(p5(),x)) [0] [0] +(p1(),p1()) = [1] >= [0] = p2() [0] [0] +(p5(),p5()) = [1] >= [0] = p10() [0] [0] +(p1(),+(p1(),x)) = x + [2] >= x + [1] = +(p2(),x) [0] [0] +(p5(),+(p5(),x)) = x + [2] >= x + [1] = +(p10(),x) problem: strict: +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),p2()) -> +(p2(),p5()) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),p2()) -> +(p2(),p10()) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),p5()) -> +(p5(),p10()) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: +(+(x,y),z) -> +(x,+(y,z)) +(p2(),p1()) -> +(p1(),p2()) +(p5(),p1()) -> +(p1(),p5()) +(p10(),p1()) -> +(p1(),p10()) +(p1(),+(p2(),p2())) -> p5() +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p1(),p1()) -> p2() +(p5(),p5()) -> p10() +(p1(),+(p1(),x)) -> +(p2(),x) +(p5(),+(p5(),x)) -> +(p10(),x) Matrix Interpretation Processor: dimension: 2 interpretation: [0] [p10] = [2], [0] [p5] = [1], [1] [p2] = [0], [1 1] [0] [+](x0, x1) = [0 1]x0 + x1 + [8], [1] [p1] = [0] orientation: [2 ] [2 ] +(p2(),+(p1(),x)) = x + [16] >= x + [16] = +(p1(),+(p2(),x)) [2 ] [2 ] +(p5(),+(p1(),x)) = x + [17] >= x + [17] = +(p1(),+(p5(),x)) [2] [1] +(p5(),p2()) = [9] >= [9] = +(p2(),p5()) [2 ] [2 ] +(p5(),+(p2(),x)) = x + [17] >= x + [17] = +(p2(),+(p5(),x)) [3 ] [3 ] +(p10(),+(p1(),x)) = x + [18] >= x + [18] = +(p1(),+(p10(),x)) [3 ] [1 ] +(p10(),p2()) = [10] >= [10] = +(p2(),p10()) [3 ] [3 ] +(p10(),+(p2(),x)) = x + [18] >= x + [18] = +(p2(),+(p10(),x)) [2 ] [1 ] +(p10(),p5()) = [11] >= [11] = +(p5(),p10()) [3 ] [3 ] +(p10(),+(p5(),x)) = x + [19] >= x + [19] = +(p5(),+(p10(),x)) [1 2] [1 1] [8 ] [1 1] [1 1] [0 ] +(+(x,y),z) = [0 1]x + [0 1]y + z + [16] >= [0 1]x + [0 1]y + z + [16] = +(x,+(y,z)) [2] [2] +(p2(),p1()) = [8] >= [8] = +(p1(),p2()) [2] [1] +(p5(),p1()) = [9] >= [9] = +(p1(),p5()) [3 ] [1 ] +(p10(),p1()) = [10] >= [10] = +(p1(),p10()) [3 ] [0] +(p1(),+(p2(),p2())) = [16] >= [1] = p5() [3 ] [1] +(p1(),+(p2(),+(p2(),x))) = x + [24] >= x + [9] = +(p5(),x) [3 ] [1] +(p2(),+(p2(),p2())) = [16] >= [9] = +(p1(),p5()) [3 ] [2 ] +(p2(),+(p2(),+(p2(),x))) = x + [24] >= x + [17] = +(p1(),+(p5(),x)) [2] [1] +(p1(),p1()) = [8] >= [0] = p2() [1 ] [0] +(p5(),p5()) = [10] >= [2] = p10() [2 ] [1] +(p1(),+(p1(),x)) = x + [16] >= x + [8] = +(p2(),x) [2 ] [2 ] +(p5(),+(p5(),x)) = x + [18] >= x + [10] = +(p10(),x) problem: strict: +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x)) +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x)) +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x)) +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x)) +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x)) +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x)) weak: +(p5(),p2()) -> +(p2(),p5()) +(p10(),p2()) -> +(p2(),p10()) +(p10(),p5()) -> +(p5(),p10()) +(+(x,y),z) -> +(x,+(y,z)) +(p2(),p1()) -> +(p1(),p2()) +(p5(),p1()) -> +(p1(),p5()) +(p10(),p1()) -> +(p1(),p10()) +(p1(),+(p2(),p2())) -> p5() +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x) +(p2(),+(p2(),p2())) -> +(p1(),p5()) +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x)) +(p1(),p1()) -> p2() +(p5(),p5()) -> p10() +(p1(),+(p1(),x)) -> +(p2(),x) +(p5(),+(p5(),x)) -> +(p10(),x) Open