Problem: -(+(x,y)) -> +(-(x),-(y)) -(-(x)) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) Proof: Commute Transformation Processor: -(+(x,y)) -> +(-(x),-(y)) -(-(x)) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Church Rosser Transformation Processor (dup): strict: weak: -(+(x,y)) -> +(-(x),-(y)) -(-(x)) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) critical peaks: 17 -(+(-(x102),-(x103))) <-0|0[]- -(-(+(x102,x103))) -1|[]-> +(x102,x103) -(x104) <-1|0[]- -(-(-(x104))) -1|[]-> -(x104) -(+(x105,+(x106,y))) <-2|0[]- -(+(+(x105,x106),y)) -0|[]-> +(-(+(x105,x106)),-(y)) +(+(x108,+(x109,y)),z) <-2|0[]- +(+(+(x108,x109),y),z) -2|[]-> +(+(x108,x109),+(y,z)) +(x111,+(x112,+(y,z))) <-2|[]- +(+(x111,x112),+(y,z)) -3|[]-> +(+(+(x111,x112),y),z) +(x,+(x114,+(x115,z))) <-2|1[]- +(x,+(+(x114,x115),z)) -3|[]-> +(+(x,+(x114,x115)),z) +(x117,+(x118,y)) <-2|[]- +(+(x117,x118),y) -4|[]-> +(y,+(x117,x118)) -(+(+(x,x121),x122)) <-3|0[]- -(+(x,+(x121,x122))) -0|[]-> +(-(x),-(+(x121,x122))) +(+(+(x,y),x124),x125) <-3|[]- +(+(x,y),+(x124,x125)) -2|[]-> +(x,+(y,+(x124,x125))) +(+(+(x,x127),x128),z) <-3|0[]- +(+(x,+(x127,x128)),z) -2|[]-> +(x,+(+(x127,x128),z)) +(x,+(+(y,x130),x131)) <-3|1[]- +(x,+(y,+(x130,x131))) -3|[]-> +(+(x,y),+(x130,x131)) +(+(x,x133),x134) <-3|[]- +(x,+(x133,x134)) -4|[]-> +(+(x133,x134),x) -(+(y,x)) <-4|0[]- -(+(x,y)) -0|[]-> +(-(x),-(y)) +(z,+(x,y)) <-4|[]- +(+(x,y),z) -2|[]-> +(x,+(y,z)) +(+(y,x),z) <-4|0[]- +(+(x,y),z) -2|[]-> +(x,+(y,z)) +(+(y,z),x) <-4|[]- +(x,+(y,z)) -3|[]-> +(+(x,y),z) +(x,+(z,y)) <-4|1[]- +(x,+(y,z)) -3|[]-> +(+(x,y),z) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 2x0 + 1, [+](x0, x1) = x0 + x1 + 1 orientation: -(+(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = +(-(x),-(y)) -(-(x)) = 4x + 3 >= x = x +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: weak: -(+(x,y)) -> +(-(x),-(y)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 2x0, [+](x0, x1) = x0 + x1 + 1 orientation: -(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 1 = +(-(x),-(y)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: weak: +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Shift Processor (no label): strict: weak: Shift Processor lab=left (dd): strict: -(-(+(x102,x103))) -> -(+(-(x102),-(x103))) -(-(+(x102,x103))) -> +(x102,x103) -(+(-(x102),-(x103))) -> +(-(-(x102)),-(-(x103))) +(-(-(x102)),-(-(x103))) -> +(-(-(x102)),x103) +(-(-(x102)),x103) -> +(x102,x103) -(+(-(x102),-(x103))) -> +(-(-(x102)),-(-(x103))) +(-(-(x102)),-(-(x103))) -> +(x102,-(-(x103))) +(x102,-(-(x103))) -> +(x102,x103) -(-(-(x104))) -> -(x104) -(-(-(x104))) -> -(x104) -(+(+(x105,x106),y)) -> -(+(x105,+(x106,y))) -(+(+(x105,x106),y)) -> +(-(+(x105,x106)),-(y)) -(+(x105,+(x106,y))) -> +(-(x105),-(+(x106,y))) +(-(x105),-(+(x106,y))) -> +(-(x105),+(-(x106),-(y))) +(-(+(x105,x106)),-(y)) -> +(+(-(x105),-(x106)),-(y)) +(+(-(x105),-(x106)),-(y)) -> +(-(x105),+(-(x106),-(y))) -(+(x105,+(x106,y))) -> -(+(+(x105,x106),y)) -(+(+(x105,x106),y)) -> +(-(+(x105,x106)),-(y)) +(+(+(x108,x109),y),z) -> +(+(x108,+(x109,y)),z) +(+(+(x108,x109),y),z) -> +(+(x108,x109),+(y,z)) +(+(x108,+(x109,y)),z) -> +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) -> +(+(+(x108,x109),y),z) +(+(x111,x112),+(y,z)) -> +(x111,+(x112,+(y,z))) +(+(x111,x112),+(y,z)) -> +(+(+(x111,x112),y),z) +(x111,+(x112,+(y,z))) -> +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) -> +(+(x111,x112),+(y,z)) +(x,+(+(x114,x115),z)) -> +(x,+(x114,+(x115,z))) +(x,+(+(x114,x115),z)) -> +(+(x,+(x114,x115)),z) +(x,+(x114,+(x115,z))) -> +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) -> +(x,+(+(x114,x115),z)) +(+(x117,x118),y) -> +(x117,+(x118,y)) +(+(x117,x118),y) -> +(y,+(x117,x118)) +(x117,+(x118,y)) -> +(+(x117,x118),y) +(y,+(x117,x118)) -> +(+(x117,x118),y) -(+(x,+(x121,x122))) -> -(+(+(x,x121),x122)) -(+(x,+(x121,x122))) -> +(-(x),-(+(x121,x122))) -(+(+(x,x121),x122)) -> +(-(+(x,x121)),-(x122)) +(-(+(x,x121)),-(x122)) -> +(+(-(x),-(x121)),-(x122)) +(-(x),-(+(x121,x122))) -> +(-(x),+(-(x121),-(x122))) +(-(x),+(-(x121),-(x122))) -> +(+(-(x),-(x121)),-(x122)) -(+(+(x,x121),x122)) -> -(+(x,+(x121,x122))) -(+(x,+(x121,x122))) -> +(-(x),-(+(x121,x122))) +(+(x,y),+(x124,x125)) -> +(+(+(x,y),x124),x125) +(+(x,y),+(x124,x125)) -> +(x,+(y,+(x124,x125))) +(+(+(x,y),x124),x125) -> +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) -> +(+(x,y),+(x124,x125)) +(+(x,+(x127,x128)),z) -> +(+(+(x,x127),x128),z) +(+(x,+(x127,x128)),z) -> +(x,+(+(x127,x128),z)) +(+(+(x,x127),x128),z) -> +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) -> +(+(x,+(x127,x128)),z) +(x,+(y,+(x130,x131))) -> +(x,+(+(y,x130),x131)) +(x,+(y,+(x130,x131))) -> +(+(x,y),+(x130,x131)) +(x,+(+(y,x130),x131)) -> +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) -> +(x,+(y,+(x130,x131))) +(x,+(x133,x134)) -> +(+(x,x133),x134) +(x,+(x133,x134)) -> +(+(x133,x134),x) +(+(x,x133),x134) -> +(x,+(x133,x134)) +(+(x133,x134),x) -> +(x,+(x133,x134)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) weak: -(+(x,y)) -> +(-(x),-(y)) -(-(x)) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 2x0 + 1, [+](x0, x1) = x0 + x1 + 1 orientation: -(-(+(x102,x103))) = 4x102 + 4x103 + 7 >= 4x102 + 4x103 + 7 = -(+(-(x102),-(x103))) -(-(+(x102,x103))) = 4x102 + 4x103 + 7 >= x102 + x103 + 1 = +(x102,x103) -(+(-(x102),-(x103))) = 4x102 + 4x103 + 7 >= 4x102 + 4x103 + 7 = +(-(-(x102)),-(-(x103))) +(-(-(x102)),-(-(x103))) = 4x102 + 4x103 + 7 >= 4x102 + x103 + 4 = +(-(-(x102)),x103) +(-(-(x102)),x103) = 4x102 + x103 + 4 >= x102 + x103 + 1 = +(x102,x103) -(+(-(x102),-(x103))) = 4x102 + 4x103 + 7 >= 4x102 + 4x103 + 7 = +(-(-(x102)),-(-(x103))) +(-(-(x102)),-(-(x103))) = 4x102 + 4x103 + 7 >= x102 + 4x103 + 4 = +(x102,-(-(x103))) +(x102,-(-(x103))) = x102 + 4x103 + 4 >= x102 + x103 + 1 = +(x102,x103) -(-(-(x104))) = 8x104 + 7 >= 2x104 + 1 = -(x104) -(-(-(x104))) = 8x104 + 7 >= 2x104 + 1 = -(x104) -(+(+(x105,x106),y)) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = -(+(x105,+(x106,y))) -(+(+(x105,x106),y)) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(-(+(x105,x106)),-(y)) -(+(x105,+(x106,y))) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(-(x105),-(+(x106,y))) +(-(x105),-(+(x106,y))) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(-(x105),+(-(x106),-(y))) +(-(+(x105,x106)),-(y)) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(+(-(x105),-(x106)),-(y)) +(+(-(x105),-(x106)),-(y)) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(-(x105),+(-(x106),-(y))) -(+(x105,+(x106,y))) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = -(+(+(x105,x106),y)) -(+(+(x105,x106),y)) = 2x105 + 2x106 + 2y + 5 >= 2x105 + 2x106 + 2y + 5 = +(-(+(x105,x106)),-(y)) +(+(+(x108,x109),y),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(x108,+(x109,y)),z) +(+(+(x108,x109),y),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(x108,x109),+(y,z)) +(+(x108,+(x109,y)),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(+(x108,x109),y),z) +(+(x111,x112),+(y,z)) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(x111,+(x112,+(y,z))) +(+(x111,x112),+(y,z)) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(+(x111,x112),y),z) +(x111,+(x112,+(y,z))) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(x111,x112),+(y,z)) +(x,+(+(x114,x115),z)) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(x114,+(x115,z))) +(x,+(+(x114,x115),z)) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(+(x,+(x114,x115)),z) +(x,+(x114,+(x115,z))) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(+(x114,x115),z)) +(+(x117,x118),y) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(x117,+(x118,y)) +(+(x117,x118),y) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(y,+(x117,x118)) +(x117,+(x118,y)) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(+(x117,x118),y) +(y,+(x117,x118)) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(+(x117,x118),y) -(+(x,+(x121,x122))) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = -(+(+(x,x121),x122)) -(+(x,+(x121,x122))) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(-(x),-(+(x121,x122))) -(+(+(x,x121),x122)) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(-(+(x,x121)),-(x122)) +(-(+(x,x121)),-(x122)) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(+(-(x),-(x121)),-(x122)) +(-(x),-(+(x121,x122))) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(-(x),+(-(x121),-(x122))) +(-(x),+(-(x121),-(x122))) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(+(-(x),-(x121)),-(x122)) -(+(+(x,x121),x122)) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = -(+(x,+(x121,x122))) -(+(x,+(x121,x122))) = 2x + 2x121 + 2x122 + 5 >= 2x + 2x121 + 2x122 + 5 = +(-(x),-(+(x121,x122))) +(+(x,y),+(x124,x125)) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(+(x,y),x124),x125) +(+(x,y),+(x124,x125)) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(x,+(y,+(x124,x125))) +(+(+(x,y),x124),x125) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(x,y),+(x124,x125)) +(+(x,+(x127,x128)),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(+(x,x127),x128),z) +(+(x,+(x127,x128)),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(x,+(+(x127,x128),z)) +(+(+(x,x127),x128),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(x,+(x127,x128)),z) +(x,+(y,+(x130,x131))) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(+(y,x130),x131)) +(x,+(y,+(x130,x131))) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(+(x,y),+(x130,x131)) +(x,+(+(y,x130),x131)) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(y,+(x130,x131))) +(x,+(x133,x134)) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(+(x,x133),x134) +(x,+(x133,x134)) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(+(x133,x134),x) +(+(x,x133),x134) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(x,+(x133,x134)) +(+(x133,x134),x) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(x,+(x133,x134)) -(+(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = -(+(y,x)) -(+(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = +(-(x),-(y)) -(+(y,x)) = 2x + 2y + 3 >= 2x + 2y + 3 = +(-(y),-(x)) +(-(x),-(y)) = 2x + 2y + 3 >= 2x + 2y + 3 = +(-(y),-(x)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(z,+(x,y)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(z,+(x,y)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(+(y,x),z) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(y,x),z) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(y,z),x) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(+(y,z),x) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(x,+(z,y)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(z,y)) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) -(-(x)) = 4x + 3 >= x = x +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: -(-(+(x102,x103))) -> -(+(-(x102),-(x103))) -(+(-(x102),-(x103))) -> +(-(-(x102)),-(-(x103))) -(+(-(x102),-(x103))) -> +(-(-(x102)),-(-(x103))) -(+(+(x105,x106),y)) -> -(+(x105,+(x106,y))) -(+(+(x105,x106),y)) -> +(-(+(x105,x106)),-(y)) -(+(x105,+(x106,y))) -> +(-(x105),-(+(x106,y))) +(-(x105),-(+(x106,y))) -> +(-(x105),+(-(x106),-(y))) +(-(+(x105,x106)),-(y)) -> +(+(-(x105),-(x106)),-(y)) +(+(-(x105),-(x106)),-(y)) -> +(-(x105),+(-(x106),-(y))) -(+(x105,+(x106,y))) -> -(+(+(x105,x106),y)) -(+(+(x105,x106),y)) -> +(-(+(x105,x106)),-(y)) +(+(+(x108,x109),y),z) -> +(+(x108,+(x109,y)),z) +(+(+(x108,x109),y),z) -> +(+(x108,x109),+(y,z)) +(+(x108,+(x109,y)),z) -> +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) -> +(+(+(x108,x109),y),z) +(+(x111,x112),+(y,z)) -> +(x111,+(x112,+(y,z))) +(+(x111,x112),+(y,z)) -> +(+(+(x111,x112),y),z) +(x111,+(x112,+(y,z))) -> +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) -> +(+(x111,x112),+(y,z)) +(x,+(+(x114,x115),z)) -> +(x,+(x114,+(x115,z))) +(x,+(+(x114,x115),z)) -> +(+(x,+(x114,x115)),z) +(x,+(x114,+(x115,z))) -> +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) -> +(x,+(+(x114,x115),z)) +(+(x117,x118),y) -> +(x117,+(x118,y)) +(+(x117,x118),y) -> +(y,+(x117,x118)) +(x117,+(x118,y)) -> +(+(x117,x118),y) +(y,+(x117,x118)) -> +(+(x117,x118),y) -(+(x,+(x121,x122))) -> -(+(+(x,x121),x122)) -(+(x,+(x121,x122))) -> +(-(x),-(+(x121,x122))) -(+(+(x,x121),x122)) -> +(-(+(x,x121)),-(x122)) +(-(+(x,x121)),-(x122)) -> +(+(-(x),-(x121)),-(x122)) +(-(x),-(+(x121,x122))) -> +(-(x),+(-(x121),-(x122))) +(-(x),+(-(x121),-(x122))) -> +(+(-(x),-(x121)),-(x122)) -(+(+(x,x121),x122)) -> -(+(x,+(x121,x122))) -(+(x,+(x121,x122))) -> +(-(x),-(+(x121,x122))) +(+(x,y),+(x124,x125)) -> +(+(+(x,y),x124),x125) +(+(x,y),+(x124,x125)) -> +(x,+(y,+(x124,x125))) +(+(+(x,y),x124),x125) -> +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) -> +(+(x,y),+(x124,x125)) +(+(x,+(x127,x128)),z) -> +(+(+(x,x127),x128),z) +(+(x,+(x127,x128)),z) -> +(x,+(+(x127,x128),z)) +(+(+(x,x127),x128),z) -> +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) -> +(+(x,+(x127,x128)),z) +(x,+(y,+(x130,x131))) -> +(x,+(+(y,x130),x131)) +(x,+(y,+(x130,x131))) -> +(+(x,y),+(x130,x131)) +(x,+(+(y,x130),x131)) -> +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) -> +(x,+(y,+(x130,x131))) +(x,+(x133,x134)) -> +(+(x,x133),x134) +(x,+(x133,x134)) -> +(+(x133,x134),x) +(+(x,x133),x134) -> +(x,+(x133,x134)) +(+(x133,x134),x) -> +(x,+(x133,x134)) -(+(x,y)) -> -(+(y,x)) -(+(x,y)) -> +(-(x),-(y)) -(+(y,x)) -> +(-(y),-(x)) +(-(x),-(y)) -> +(-(y),-(x)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) weak: -(+(x,y)) -> +(-(x),-(y)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [-](x0) = 3x0, [+](x0, x1) = x0 + x1 + 1 orientation: -(-(+(x102,x103))) = 9x102 + 9x103 + 9 >= 9x102 + 9x103 + 3 = -(+(-(x102),-(x103))) -(+(-(x102),-(x103))) = 9x102 + 9x103 + 3 >= 9x102 + 9x103 + 1 = +(-(-(x102)),-(-(x103))) -(+(-(x102),-(x103))) = 9x102 + 9x103 + 3 >= 9x102 + 9x103 + 1 = +(-(-(x102)),-(-(x103))) -(+(+(x105,x106),y)) = 3x105 + 3x106 + 3y + 6 >= 3x105 + 3x106 + 3y + 6 = -(+(x105,+(x106,y))) -(+(+(x105,x106),y)) = 3x105 + 3x106 + 3y + 6 >= 3x105 + 3x106 + 3y + 4 = +(-(+(x105,x106)),-(y)) -(+(x105,+(x106,y))) = 3x105 + 3x106 + 3y + 6 >= 3x105 + 3x106 + 3y + 4 = +(-(x105),-(+(x106,y))) +(-(x105),-(+(x106,y))) = 3x105 + 3x106 + 3y + 4 >= 3x105 + 3x106 + 3y + 2 = +(-(x105),+(-(x106),-(y))) +(-(+(x105,x106)),-(y)) = 3x105 + 3x106 + 3y + 4 >= 3x105 + 3x106 + 3y + 2 = +(+(-(x105),-(x106)),-(y)) +(+(-(x105),-(x106)),-(y)) = 3x105 + 3x106 + 3y + 2 >= 3x105 + 3x106 + 3y + 2 = +(-(x105),+(-(x106),-(y))) -(+(x105,+(x106,y))) = 3x105 + 3x106 + 3y + 6 >= 3x105 + 3x106 + 3y + 6 = -(+(+(x105,x106),y)) -(+(+(x105,x106),y)) = 3x105 + 3x106 + 3y + 6 >= 3x105 + 3x106 + 3y + 4 = +(-(+(x105,x106)),-(y)) +(+(+(x108,x109),y),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(x108,+(x109,y)),z) +(+(+(x108,x109),y),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(x108,x109),+(y,z)) +(+(x108,+(x109,y)),z) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) = x108 + x109 + y + z + 3 >= x108 + x109 + y + z + 3 = +(+(+(x108,x109),y),z) +(+(x111,x112),+(y,z)) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(x111,+(x112,+(y,z))) +(+(x111,x112),+(y,z)) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(+(x111,x112),y),z) +(x111,+(x112,+(y,z))) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) = x111 + x112 + y + z + 3 >= x111 + x112 + y + z + 3 = +(+(x111,x112),+(y,z)) +(x,+(+(x114,x115),z)) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(x114,+(x115,z))) +(x,+(+(x114,x115),z)) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(+(x,+(x114,x115)),z) +(x,+(x114,+(x115,z))) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) = x + x114 + x115 + z + 3 >= x + x114 + x115 + z + 3 = +(x,+(+(x114,x115),z)) +(+(x117,x118),y) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(x117,+(x118,y)) +(+(x117,x118),y) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(y,+(x117,x118)) +(x117,+(x118,y)) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(+(x117,x118),y) +(y,+(x117,x118)) = x117 + x118 + y + 2 >= x117 + x118 + y + 2 = +(+(x117,x118),y) -(+(x,+(x121,x122))) = 3x + 3x121 + 3x122 + 6 >= 3x + 3x121 + 3x122 + 6 = -(+(+(x,x121),x122)) -(+(x,+(x121,x122))) = 3x + 3x121 + 3x122 + 6 >= 3x + 3x121 + 3x122 + 4 = +(-(x),-(+(x121,x122))) -(+(+(x,x121),x122)) = 3x + 3x121 + 3x122 + 6 >= 3x + 3x121 + 3x122 + 4 = +(-(+(x,x121)),-(x122)) +(-(+(x,x121)),-(x122)) = 3x + 3x121 + 3x122 + 4 >= 3x + 3x121 + 3x122 + 2 = +(+(-(x),-(x121)),-(x122)) +(-(x),-(+(x121,x122))) = 3x + 3x121 + 3x122 + 4 >= 3x + 3x121 + 3x122 + 2 = +(-(x),+(-(x121),-(x122))) +(-(x),+(-(x121),-(x122))) = 3x + 3x121 + 3x122 + 2 >= 3x + 3x121 + 3x122 + 2 = +(+(-(x),-(x121)),-(x122)) -(+(+(x,x121),x122)) = 3x + 3x121 + 3x122 + 6 >= 3x + 3x121 + 3x122 + 6 = -(+(x,+(x121,x122))) -(+(x,+(x121,x122))) = 3x + 3x121 + 3x122 + 6 >= 3x + 3x121 + 3x122 + 4 = +(-(x),-(+(x121,x122))) +(+(x,y),+(x124,x125)) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(+(x,y),x124),x125) +(+(x,y),+(x124,x125)) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(x,+(y,+(x124,x125))) +(+(+(x,y),x124),x125) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) = x + x124 + x125 + y + 3 >= x + x124 + x125 + y + 3 = +(+(x,y),+(x124,x125)) +(+(x,+(x127,x128)),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(+(x,x127),x128),z) +(+(x,+(x127,x128)),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(x,+(+(x127,x128),z)) +(+(+(x,x127),x128),z) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) = x + x127 + x128 + z + 3 >= x + x127 + x128 + z + 3 = +(+(x,+(x127,x128)),z) +(x,+(y,+(x130,x131))) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(+(y,x130),x131)) +(x,+(y,+(x130,x131))) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(+(x,y),+(x130,x131)) +(x,+(+(y,x130),x131)) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) = x + x130 + x131 + y + 3 >= x + x130 + x131 + y + 3 = +(x,+(y,+(x130,x131))) +(x,+(x133,x134)) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(+(x,x133),x134) +(x,+(x133,x134)) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(+(x133,x134),x) +(+(x,x133),x134) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(x,+(x133,x134)) +(+(x133,x134),x) = x + x133 + x134 + 2 >= x + x133 + x134 + 2 = +(x,+(x133,x134)) -(+(x,y)) = 3x + 3y + 3 >= 3x + 3y + 3 = -(+(y,x)) -(+(x,y)) = 3x + 3y + 3 >= 3x + 3y + 1 = +(-(x),-(y)) -(+(y,x)) = 3x + 3y + 3 >= 3x + 3y + 1 = +(-(y),-(x)) +(-(x),-(y)) = 3x + 3y + 1 >= 3x + 3y + 1 = +(-(y),-(x)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(z,+(x,y)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(z,+(x,y)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(+(y,x),z) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(y,x),z) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(y,z),x) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(+(y,z),x) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(x,+(z,y)) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) +(x,+(z,y)) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: -(+(+(x105,x106),y)) -> -(+(x105,+(x106,y))) +(+(-(x105),-(x106)),-(y)) -> +(-(x105),+(-(x106),-(y))) -(+(x105,+(x106,y))) -> -(+(+(x105,x106),y)) +(+(+(x108,x109),y),z) -> +(+(x108,+(x109,y)),z) +(+(+(x108,x109),y),z) -> +(+(x108,x109),+(y,z)) +(+(x108,+(x109,y)),z) -> +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) -> +(+(+(x108,x109),y),z) +(+(x111,x112),+(y,z)) -> +(x111,+(x112,+(y,z))) +(+(x111,x112),+(y,z)) -> +(+(+(x111,x112),y),z) +(x111,+(x112,+(y,z))) -> +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) -> +(+(x111,x112),+(y,z)) +(x,+(+(x114,x115),z)) -> +(x,+(x114,+(x115,z))) +(x,+(+(x114,x115),z)) -> +(+(x,+(x114,x115)),z) +(x,+(x114,+(x115,z))) -> +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) -> +(x,+(+(x114,x115),z)) +(+(x117,x118),y) -> +(x117,+(x118,y)) +(+(x117,x118),y) -> +(y,+(x117,x118)) +(x117,+(x118,y)) -> +(+(x117,x118),y) +(y,+(x117,x118)) -> +(+(x117,x118),y) -(+(x,+(x121,x122))) -> -(+(+(x,x121),x122)) +(-(x),+(-(x121),-(x122))) -> +(+(-(x),-(x121)),-(x122)) -(+(+(x,x121),x122)) -> -(+(x,+(x121,x122))) +(+(x,y),+(x124,x125)) -> +(+(+(x,y),x124),x125) +(+(x,y),+(x124,x125)) -> +(x,+(y,+(x124,x125))) +(+(+(x,y),x124),x125) -> +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) -> +(+(x,y),+(x124,x125)) +(+(x,+(x127,x128)),z) -> +(+(+(x,x127),x128),z) +(+(x,+(x127,x128)),z) -> +(x,+(+(x127,x128),z)) +(+(+(x,x127),x128),z) -> +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) -> +(+(x,+(x127,x128)),z) +(x,+(y,+(x130,x131))) -> +(x,+(+(y,x130),x131)) +(x,+(y,+(x130,x131))) -> +(+(x,y),+(x130,x131)) +(x,+(+(y,x130),x131)) -> +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) -> +(x,+(y,+(x130,x131))) +(x,+(x133,x134)) -> +(+(x,x133),x134) +(x,+(x133,x134)) -> +(+(x133,x134),x) +(+(x,x133),x134) -> +(x,+(x133,x134)) +(+(x133,x134),x) -> +(x,+(x133,x134)) -(+(x,y)) -> -(+(y,x)) +(-(x),-(y)) -> +(-(y),-(x)) +(+(x,y),z) -> +(z,+(x,y)) +(+(x,y),z) -> +(x,+(y,z)) +(z,+(x,y)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(+(y,x),z) +(+(x,y),z) -> +(x,+(y,z)) +(+(y,x),z) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(y,z)) -> +(+(y,z),x) +(x,+(y,z)) -> +(+(x,y),z) +(+(y,z),x) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(x,+(z,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,+(z,y)) -> +(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) weak: +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: -(+(-(x102),-(x103))) <-0|0[1]- -(-(+(x102,x103))) -1|[1]-> +(x102,x103) joins: -(+(-(x102),-(x103))) -0|[0]-> +(-(-(x102)),-(-(x103))) -1|1[0]-> +(-(-(x102)),x103) -1|0[0]-> +(x102,x103) peak: -(x104) <-1|0[1]- -(-(-(x104))) -1|[1]-> -(x104) joins: peak: -(+(x105,+(x106,y))) <-2|0[1]- -(+(+(x105,x106),y)) -0|[1]-> +(-(+(x105,x106)),-(y)) joins: -(+(x105,+(x106,y))) -0|[1]-> +(-(x105),-(+(x106,y))) -0| 1[0]-> +(-(x105),+(-(x106),-(y))) +(-(+(x105,x106)),-(y)) -0|0[0]-> +(+(-(x105),-(x106)),-(y)) -2| [0]-> +(-(x105),+(-(x106),-(y))) peak: +(+(x108,+(x109,y)),z) <-2|0[1]- +(+(+(x108,x109),y),z) -2|[1]-> +(+(x108,x109),+(y,z)) joins: +(+(x108,+(x109,y)),z) -3|0[1]-> +(+(+(x108,x109),y),z) +(+(x108,x109),+(y,z)) -3|[1]-> +(+(+(x108,x109),y),z) peak: +(x111,+(x112,+(y,z))) <-2|[1]- +(+(x111,x112),+(y,z)) -3|[1]-> +(+(+(x111,x112),y),z) joins: +(x111,+(x112,+(y,z))) -3|[1]-> +(+(x111,x112),+(y,z)) +(+(+(x111,x112),y),z) -2|[1]-> +(+(x111,x112),+(y,z)) peak: +(x,+(x114,+(x115,z))) <-2|1[1]- +(x,+(+(x114,x115),z)) -3|[1]-> +(+(x,+(x114,x115)),z) joins: +(x,+(x114,+(x115,z))) -3|1[1]-> +(x,+(+(x114,x115),z)) +(+(x,+(x114,x115)),z) -2|[1]-> +(x,+(+(x114,x115),z)) peak: +(x117,+(x118,y)) <-2|[1]- +(+(x117,x118),y) -4|[1]-> +(y,+(x117,x118)) joins: +(x117,+(x118,y)) -3|[1]-> +(+(x117,x118),y) +(y,+(x117,x118)) -4|[1]-> +(+(x117,x118),y) peak: -(+(+(x,x121),x122)) <-3|0[1]- -(+(x,+(x121,x122))) -0|[1]-> +(-(x),-(+(x121,x122))) joins: -(+(+(x,x121),x122)) -0|[1]-> +(-(+(x,x121)),-(x122)) -0| 0[0]-> +(+(-(x),-(x121)),-(x122)) +(-(x),-(+(x121,x122))) -0|1[0]-> +(-(x),+(-(x121),-(x122))) -3| [0]-> +(+(-(x),-(x121)),-(x122)) peak: +(+(+(x,y),x124),x125) <-3|[1]- +(+(x,y),+(x124,x125)) -2|[1]-> +(x,+(y,+(x124,x125))) joins: +(+(+(x,y),x124),x125) -2|[1]-> +(+(x,y),+(x124,x125)) +(x,+(y,+(x124,x125))) -3|[1]-> +(+(x,y),+(x124,x125)) peak: +(+(+(x,x127),x128),z) <-3|0[1]- +(+(x,+(x127,x128)),z) -2|[1]-> +(x,+(+(x127,x128),z)) joins: +(+(+(x,x127),x128),z) -2|0[1]-> +(+(x,+(x127,x128)),z) +(x,+(+(x127,x128),z)) -3|[1]-> +(+(x,+(x127,x128)),z) peak: +(x,+(+(y,x130),x131)) <-3|1[1]- +(x,+(y,+(x130,x131))) -3|[1]-> +(+(x,y),+(x130,x131)) joins: +(x,+(+(y,x130),x131)) -2|1[1]-> +(x,+(y,+(x130,x131))) +(+(x,y),+(x130,x131)) -2|[1]-> +(x,+(y,+(x130,x131))) peak: +(+(x,x133),x134) <-3|[1]- +(x,+(x133,x134)) -4|[1]-> +(+(x133,x134),x) joins: +(+(x,x133),x134) -2|[1]-> +(x,+(x133,x134)) +(+(x133,x134),x) -4|[1]-> +(x,+(x133,x134)) peak: -(+(y,x)) <-4|0[1]- -(+(x,y)) -0|[1]-> +(-(x),-(y)) joins: -(+(y,x)) -0|[1]-> +(-(y),-(x)) +(-(x),-(y)) -4|[0]-> +(-(y),-(x)) peak: +(z,+(x,y)) <-4|[1]- +(+(x,y),z) -2|[1]-> +(x,+(y,z)) joins: +(z,+(x,y)) -4|[1]-> +(+(x,y),z) +(x,+(y,z)) -3|[1]-> +(+(x,y),z) peak: +(+(y,x),z) <-4|0[1]- +(+(x,y),z) -2|[1]-> +(x,+(y,z)) joins: +(+(y,x),z) -4|0[1]-> +(+(x,y),z) +(x,+(y,z)) -3|[1]-> +(+(x,y),z) peak: +(+(y,z),x) <-4|[1]- +(x,+(y,z)) -3|[1]-> +(+(x,y),z) joins: +(+(y,z),x) -4|[1]-> +(x,+(y,z)) +(+(x,y),z) -2|[1]-> +(x,+(y,z)) peak: +(x,+(z,y)) <-4|1[1]- +(x,+(y,z)) -3|[1]-> +(+(x,y),z) joins: +(x,+(z,y)) -4|1[1]-> +(x,+(y,z)) +(+(x,y),z) -2|[1]-> +(x,+(y,z)) Qed