Problem: +(0(),x) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) Proof: Commute Transformation Processor: +(0(),x) -> x +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Church Rosser Transformation Processor (dup): strict: weak: +(0(),x) -> x +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) critical peaks: 26 0() <-0|[]- +(0(),0()) -1|[]-> 0() +(y,z) <-0|0[]- +(+(0(),y),z) -2|[]-> +(0(),+(y,z)) +(y,z) <-0|[]- +(0(),+(y,z)) -3|[]-> +(+(0(),y),z) +(x,z) <-0|1[]- +(x,+(0(),z)) -3|[]-> +(+(x,0()),z) y <-0|[]- +(0(),y) -4|[]-> +(y,0()) 0() <-1|[]- +(0(),0()) -0|[]-> 0() +(x,y) <-1|[]- +(+(x,y),0()) -2|[]-> +(x,+(y,0())) +(x,z) <-1|0[]- +(+(x,0()),z) -2|[]-> +(x,+(0(),z)) +(x,y) <-1|1[]- +(x,+(y,0())) -3|[]-> +(+(x,y),0()) x <-1|[]- +(x,0()) -4|[]-> +(0(),x) +(x103,+(x104,0())) <-2|[]- +(+(x103,x104),0()) -1|[]-> +(x103,x104) +(+(x106,+(x107,y)),z) <-2|0[]- +(+(+(x106,x107),y),z) -2|[]-> +(+(x106,x107),+(y,z)) +(x109,+(x110,+(y,z))) <-2|[]- +(+(x109,x110),+(y,z)) -3|[]-> +(+(+(x109,x110),y),z) +(x,+(x112,+(x113,z))) <-2|1[]- +(x,+(+(x112,x113),z)) -3|[]-> +(+(x,+(x112,x113)),z) +(x115,+(x116,y)) <-2|[]- +(+(x115,x116),y) -4|[]-> +(y,+(x115,x116)) +(+(0(),x119),x120) <-3|[]- +(0(),+(x119,x120)) -0|[]-> +(x119,x120) +(+(+(x,y),x122),x123) <-3|[]- +(+(x,y),+(x122,x123)) -2|[]-> +(x,+(y,+(x122,x123))) +(+(+(x,x125),x126),z) <-3|0[]- +(+(x,+(x125,x126)),z) -2|[]-> +(x,+(+(x125,x126),z)) +(x,+(+(y,x128),x129)) <-3|1[]- +(x,+(y,+(x128,x129))) -3|[]-> +(+(x,y),+(x128,x129)) +(+(x,x131),x132) <-3|[]- +(x,+(x131,x132)) -4|[]-> +(+(x131,x132),x) +(x,0()) <-4|[]- +(0(),x) -0|[]-> x +(0(),x) <-4|[]- +(x,0()) -1|[]-> x +(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, x1) = x0 + x1, [0] = 2 orientation: +(0(),x) = x + 2 >= x = x +(x,0()) = x + 2 >= x = x +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(x,y) = x + y >= x + y = +(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: +(0(),0()) -> 0() +(0(),0()) -> 0() +(+(0(),y),z) -> +(y,z) +(+(0(),y),z) -> +(0(),+(y,z)) +(0(),+(y,z)) -> +(y,z) +(0(),+(y,z)) -> +(y,z) +(0(),+(y,z)) -> +(+(0(),y),z) +(+(0(),y),z) -> +(y,z) +(x,+(0(),z)) -> +(x,z) +(x,+(0(),z)) -> +(+(x,0()),z) +(+(x,0()),z) -> +(x,z) +(0(),y) -> y +(0(),y) -> +(y,0()) +(y,0()) -> y +(0(),0()) -> 0() +(0(),0()) -> 0() +(+(x,y),0()) -> +(x,y) +(+(x,y),0()) -> +(x,+(y,0())) +(x,+(y,0())) -> +(x,y) +(+(x,0()),z) -> +(x,z) +(+(x,0()),z) -> +(x,+(0(),z)) +(x,+(0(),z)) -> +(x,z) +(x,+(y,0())) -> +(x,y) +(x,+(y,0())) -> +(+(x,y),0()) +(+(x,y),0()) -> +(x,y) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x +(+(x103,x104),0()) -> +(x103,+(x104,0())) +(+(x103,x104),0()) -> +(x103,x104) +(x103,+(x104,0())) -> +(x103,x104) +(+(+(x106,x107),y),z) -> +(+(x106,+(x107,y)),z) +(+(+(x106,x107),y),z) -> +(+(x106,x107),+(y,z)) +(+(x106,+(x107,y)),z) -> +(+(+(x106,x107),y),z) +(+(x106,x107),+(y,z)) -> +(+(+(x106,x107),y),z) +(+(x109,x110),+(y,z)) -> +(x109,+(x110,+(y,z))) +(+(x109,x110),+(y,z)) -> +(+(+(x109,x110),y),z) +(x109,+(x110,+(y,z))) -> +(+(x109,x110),+(y,z)) +(+(+(x109,x110),y),z) -> +(+(x109,x110),+(y,z)) +(x,+(+(x112,x113),z)) -> +(x,+(x112,+(x113,z))) +(x,+(+(x112,x113),z)) -> +(+(x,+(x112,x113)),z) +(x,+(x112,+(x113,z))) -> +(x,+(+(x112,x113),z)) +(+(x,+(x112,x113)),z) -> +(x,+(+(x112,x113),z)) +(+(x115,x116),y) -> +(x115,+(x116,y)) +(+(x115,x116),y) -> +(y,+(x115,x116)) +(x115,+(x116,y)) -> +(+(x115,x116),y) +(y,+(x115,x116)) -> +(+(x115,x116),y) +(0(),+(x119,x120)) -> +(+(0(),x119),x120) +(0(),+(x119,x120)) -> +(x119,x120) +(+(0(),x119),x120) -> +(x119,x120) +(+(x,y),+(x122,x123)) -> +(+(+(x,y),x122),x123) +(+(x,y),+(x122,x123)) -> +(x,+(y,+(x122,x123))) +(+(+(x,y),x122),x123) -> +(+(x,y),+(x122,x123)) +(x,+(y,+(x122,x123))) -> +(+(x,y),+(x122,x123)) +(+(x,+(x125,x126)),z) -> +(+(+(x,x125),x126),z) +(+(x,+(x125,x126)),z) -> +(x,+(+(x125,x126),z)) +(+(+(x,x125),x126),z) -> +(+(x,+(x125,x126)),z) +(x,+(+(x125,x126),z)) -> +(+(x,+(x125,x126)),z) +(x,+(y,+(x128,x129))) -> +(x,+(+(y,x128),x129)) +(x,+(y,+(x128,x129))) -> +(+(x,y),+(x128,x129)) +(x,+(+(y,x128),x129)) -> +(x,+(y,+(x128,x129))) +(+(x,y),+(x128,x129)) -> +(x,+(y,+(x128,x129))) +(x,+(x131,x132)) -> +(+(x,x131),x132) +(x,+(x131,x132)) -> +(+(x131,x132),x) +(+(x,x131),x132) -> +(x,+(x131,x132)) +(+(x131,x132),x) -> +(x,+(x131,x132)) +(0(),x) -> +(x,0()) +(0(),x) -> x +(x,0()) -> x +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> 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: +(0(),x) -> x +(x,0()) -> x +(+(x,y),z) -> +(x,+(y,z)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [+](x0, x1) = x0 + x1, [0] = 2 orientation: +(0(),0()) = 4 >= 2 = 0() +(0(),0()) = 4 >= 2 = 0() +(+(0(),y),z) = y + z + 2 >= y + z = +(y,z) +(+(0(),y),z) = y + z + 2 >= y + z + 2 = +(0(),+(y,z)) +(0(),+(y,z)) = y + z + 2 >= y + z = +(y,z) +(0(),+(y,z)) = y + z + 2 >= y + z = +(y,z) +(0(),+(y,z)) = y + z + 2 >= y + z + 2 = +(+(0(),y),z) +(+(0(),y),z) = y + z + 2 >= y + z = +(y,z) +(x,+(0(),z)) = x + z + 2 >= x + z = +(x,z) +(x,+(0(),z)) = x + z + 2 >= x + z + 2 = +(+(x,0()),z) +(+(x,0()),z) = x + z + 2 >= x + z = +(x,z) +(0(),y) = y + 2 >= y = y +(0(),y) = y + 2 >= y + 2 = +(y,0()) +(y,0()) = y + 2 >= y = y +(0(),0()) = 4 >= 2 = 0() +(0(),0()) = 4 >= 2 = 0() +(+(x,y),0()) = x + y + 2 >= x + y = +(x,y) +(+(x,y),0()) = x + y + 2 >= x + y + 2 = +(x,+(y,0())) +(x,+(y,0())) = x + y + 2 >= x + y = +(x,y) +(+(x,0()),z) = x + z + 2 >= x + z = +(x,z) +(+(x,0()),z) = x + z + 2 >= x + z + 2 = +(x,+(0(),z)) +(x,+(0(),z)) = x + z + 2 >= x + z = +(x,z) +(x,+(y,0())) = x + y + 2 >= x + y = +(x,y) +(x,+(y,0())) = x + y + 2 >= x + y + 2 = +(+(x,y),0()) +(+(x,y),0()) = x + y + 2 >= x + y = +(x,y) +(x,0()) = x + 2 >= x = x +(x,0()) = x + 2 >= x + 2 = +(0(),x) +(0(),x) = x + 2 >= x = x +(+(x103,x104),0()) = x103 + x104 + 2 >= x103 + x104 + 2 = +(x103,+(x104,0())) +(+(x103,x104),0()) = x103 + x104 + 2 >= x103 + x104 = +(x103,x104) +(x103,+(x104,0())) = x103 + x104 + 2 >= x103 + x104 = +(x103,x104) +(+(+(x106,x107),y),z) = x106 + x107 + y + z >= x106 + x107 + y + z = +(+(x106,+(x107,y)),z) +(+(+(x106,x107),y),z) = x106 + x107 + y + z >= x106 + x107 + y + z = +(+(x106,x107),+(y,z)) +(+(x106,+(x107,y)),z) = x106 + x107 + y + z >= x106 + x107 + y + z = +(+(+(x106,x107),y),z) +(+(x106,x107),+(y,z)) = x106 + x107 + y + z >= x106 + x107 + y + z = +(+(+(x106,x107),y),z) +(+(x109,x110),+(y,z)) = x109 + x110 + y + z >= x109 + x110 + y + z = +(x109,+(x110,+(y,z))) +(+(x109,x110),+(y,z)) = x109 + x110 + y + z >= x109 + x110 + y + z = +(+(+(x109,x110),y),z) +(x109,+(x110,+(y,z))) = x109 + x110 + y + z >= x109 + x110 + y + z = +(+(x109,x110),+(y,z)) +(+(+(x109,x110),y),z) = x109 + x110 + y + z >= x109 + x110 + y + z = +(+(x109,x110),+(y,z)) +(x,+(+(x112,x113),z)) = x + x112 + x113 + z >= x + x112 + x113 + z = +(x,+(x112,+(x113,z))) +(x,+(+(x112,x113),z)) = x + x112 + x113 + z >= x + x112 + x113 + z = +(+(x,+(x112,x113)),z) +(x,+(x112,+(x113,z))) = x + x112 + x113 + z >= x + x112 + x113 + z = +(x,+(+(x112,x113),z)) +(+(x,+(x112,x113)),z) = x + x112 + x113 + z >= x + x112 + x113 + z = +(x,+(+(x112,x113),z)) +(+(x115,x116),y) = x115 + x116 + y >= x115 + x116 + y = +(x115,+(x116,y)) +(+(x115,x116),y) = x115 + x116 + y >= x115 + x116 + y = +(y,+(x115,x116)) +(x115,+(x116,y)) = x115 + x116 + y >= x115 + x116 + y = +(+(x115,x116),y) +(y,+(x115,x116)) = x115 + x116 + y >= x115 + x116 + y = +(+(x115,x116),y) +(0(),+(x119,x120)) = x119 + x120 + 2 >= x119 + x120 + 2 = +(+(0(),x119),x120) +(0(),+(x119,x120)) = x119 + x120 + 2 >= x119 + x120 = +(x119,x120) +(+(0(),x119),x120) = x119 + x120 + 2 >= x119 + x120 = +(x119,x120) +(+(x,y),+(x122,x123)) = x + x122 + x123 + y >= x + x122 + x123 + y = +(+(+(x,y),x122),x123) +(+(x,y),+(x122,x123)) = x + x122 + x123 + y >= x + x122 + x123 + y = +(x,+(y,+(x122,x123))) +(+(+(x,y),x122),x123) = x + x122 + x123 + y >= x + x122 + x123 + y = +(+(x,y),+(x122,x123)) +(x,+(y,+(x122,x123))) = x + x122 + x123 + y >= x + x122 + x123 + y = +(+(x,y),+(x122,x123)) +(+(x,+(x125,x126)),z) = x + x125 + x126 + z >= x + x125 + x126 + z = +(+(+(x,x125),x126),z) +(+(x,+(x125,x126)),z) = x + x125 + x126 + z >= x + x125 + x126 + z = +(x,+(+(x125,x126),z)) +(+(+(x,x125),x126),z) = x + x125 + x126 + z >= x + x125 + x126 + z = +(+(x,+(x125,x126)),z) +(x,+(+(x125,x126),z)) = x + x125 + x126 + z >= x + x125 + x126 + z = +(+(x,+(x125,x126)),z) +(x,+(y,+(x128,x129))) = x + x128 + x129 + y >= x + x128 + x129 + y = +(x,+(+(y,x128),x129)) +(x,+(y,+(x128,x129))) = x + x128 + x129 + y >= x + x128 + x129 + y = +(+(x,y),+(x128,x129)) +(x,+(+(y,x128),x129)) = x + x128 + x129 + y >= x + x128 + x129 + y = +(x,+(y,+(x128,x129))) +(+(x,y),+(x128,x129)) = x + x128 + x129 + y >= x + x128 + x129 + y = +(x,+(y,+(x128,x129))) +(x,+(x131,x132)) = x + x131 + x132 >= x + x131 + x132 = +(+(x,x131),x132) +(x,+(x131,x132)) = x + x131 + x132 >= x + x131 + x132 = +(+(x131,x132),x) +(+(x,x131),x132) = x + x131 + x132 >= x + x131 + x132 = +(x,+(x131,x132)) +(+(x131,x132),x) = x + x131 + x132 >= x + x131 + x132 = +(x,+(x131,x132)) +(0(),x) = x + 2 >= x + 2 = +(x,0()) +(0(),x) = x + 2 >= x = x +(x,0()) = x + 2 >= x = x +(x,0()) = x + 2 >= x + 2 = +(0(),x) +(x,0()) = x + 2 >= x = x +(0(),x) = x + 2 >= x = x +(+(x,y),z) = x + y + z >= x + y + z = +(z,+(x,y)) +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(z,+(x,y)) = x + y + z >= x + y + z = +(+(x,y),z) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(+(x,y),z) = x + y + z >= x + y + z = +(+(y,x),z) +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(+(y,x),z) = x + y + z >= x + y + z = +(+(x,y),z) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(y,z),x) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(+(y,z),x) = x + y + z >= x + y + z = +(x,+(y,z)) +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(x,+(y,z)) = x + y + z >= x + y + z = +(x,+(z,y)) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) +(x,+(z,y)) = x + y + z >= x + y + z = +(x,+(y,z)) +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z)) +(x,y) = x + y >= x + y = +(y,x) problem: strict: +(+(0(),y),z) -> +(0(),+(y,z)) +(0(),+(y,z)) -> +(+(0(),y),z) +(x,+(0(),z)) -> +(+(x,0()),z) +(0(),y) -> +(y,0()) +(+(x,y),0()) -> +(x,+(y,0())) +(+(x,0()),z) -> +(x,+(0(),z)) +(x,+(y,0())) -> +(+(x,y),0()) +(x,0()) -> +(0(),x) +(+(x103,x104),0()) -> +(x103,+(x104,0())) +(+(+(x106,x107),y),z) -> +(+(x106,+(x107,y)),z) +(+(+(x106,x107),y),z) -> +(+(x106,x107),+(y,z)) +(+(x106,+(x107,y)),z) -> +(+(+(x106,x107),y),z) +(+(x106,x107),+(y,z)) -> +(+(+(x106,x107),y),z) +(+(x109,x110),+(y,z)) -> +(x109,+(x110,+(y,z))) +(+(x109,x110),+(y,z)) -> +(+(+(x109,x110),y),z) +(x109,+(x110,+(y,z))) -> +(+(x109,x110),+(y,z)) +(+(+(x109,x110),y),z) -> +(+(x109,x110),+(y,z)) +(x,+(+(x112,x113),z)) -> +(x,+(x112,+(x113,z))) +(x,+(+(x112,x113),z)) -> +(+(x,+(x112,x113)),z) +(x,+(x112,+(x113,z))) -> +(x,+(+(x112,x113),z)) +(+(x,+(x112,x113)),z) -> +(x,+(+(x112,x113),z)) +(+(x115,x116),y) -> +(x115,+(x116,y)) +(+(x115,x116),y) -> +(y,+(x115,x116)) +(x115,+(x116,y)) -> +(+(x115,x116),y) +(y,+(x115,x116)) -> +(+(x115,x116),y) +(0(),+(x119,x120)) -> +(+(0(),x119),x120) +(+(x,y),+(x122,x123)) -> +(+(+(x,y),x122),x123) +(+(x,y),+(x122,x123)) -> +(x,+(y,+(x122,x123))) +(+(+(x,y),x122),x123) -> +(+(x,y),+(x122,x123)) +(x,+(y,+(x122,x123))) -> +(+(x,y),+(x122,x123)) +(+(x,+(x125,x126)),z) -> +(+(+(x,x125),x126),z) +(+(x,+(x125,x126)),z) -> +(x,+(+(x125,x126),z)) +(+(+(x,x125),x126),z) -> +(+(x,+(x125,x126)),z) +(x,+(+(x125,x126),z)) -> +(+(x,+(x125,x126)),z) +(x,+(y,+(x128,x129))) -> +(x,+(+(y,x128),x129)) +(x,+(y,+(x128,x129))) -> +(+(x,y),+(x128,x129)) +(x,+(+(y,x128),x129)) -> +(x,+(y,+(x128,x129))) +(+(x,y),+(x128,x129)) -> +(x,+(y,+(x128,x129))) +(x,+(x131,x132)) -> +(+(x,x131),x132) +(x,+(x131,x132)) -> +(+(x131,x132),x) +(+(x,x131),x132) -> +(x,+(x131,x132)) +(+(x131,x132),x) -> +(x,+(x131,x132)) +(0(),x) -> +(x,0()) +(x,0()) -> +(0(),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: 0() <-0|[1]- +(0(),0()) -1|[1]-> 0() joins: peak: +(y,z) <-0|0[1]- +(+(0(),y),z) -2|[1]-> +(0(),+(y,z)) joins: +(0(),+(y,z)) -0|[1]-> +(y,z) peak: +(y,z) <-0|[1]- +(0(),+(y,z)) -3|[1]-> +(+(0(),y),z) joins: +(+(0(),y),z) -0|0[1]-> +(y,z) peak: +(x,z) <-0|1[1]- +(x,+(0(),z)) -3|[1]-> +(+(x,0()),z) joins: +(+(x,0()),z) -1|0[1]-> +(x,z) peak: y <-0|[1]- +(0(),y) -4|[1]-> +(y,0()) joins: +(y,0()) -1|[1]-> y peak: 0() <-1|[1]- +(0(),0()) -0|[1]-> 0() joins: peak: +(x,y) <-1|[1]- +(+(x,y),0()) -2|[1]-> +(x,+(y,0())) joins: +(x,+(y,0())) -1|1[1]-> +(x,y) peak: +(x,z) <-1|0[1]- +(+(x,0()),z) -2|[1]-> +(x,+(0(),z)) joins: +(x,+(0(),z)) -0|1[1]-> +(x,z) peak: +(x,y) <-1|1[1]- +(x,+(y,0())) -3|[1]-> +(+(x,y),0()) joins: +(+(x,y),0()) -1|[1]-> +(x,y) peak: x <-1|[1]- +(x,0()) -4|[1]-> +(0(),x) joins: +(0(),x) -0|[1]-> x peak: +(x103,+(x104,0())) <-2|[1]- +(+(x103,x104),0()) -1|[1]-> +(x103,x104) joins: +(x103,+(x104,0())) -1|1[1]-> +(x103,x104) peak: +(+(x106,+(x107,y)),z) <-2|0[1]- +(+(+(x106,x107),y),z) -2|[1]-> +(+(x106,x107),+(y,z)) joins: +(+(x106,+(x107,y)),z) -3|0[1]-> +(+(+(x106,x107),y),z) +(+(x106,x107),+(y,z)) -3|[1]-> +(+(+(x106,x107),y),z) peak: +(x109,+(x110,+(y,z))) <-2|[1]- +(+(x109,x110),+(y,z)) -3|[1]-> +(+(+(x109,x110),y),z) joins: +(x109,+(x110,+(y,z))) -3|[1]-> +(+(x109,x110),+(y,z)) +(+(+(x109,x110),y),z) -2|[1]-> +(+(x109,x110),+(y,z)) peak: +(x,+(x112,+(x113,z))) <-2|1[1]- +(x,+(+(x112,x113),z)) -3|[1]-> +(+(x,+(x112,x113)),z) joins: +(x,+(x112,+(x113,z))) -3|1[1]-> +(x,+(+(x112,x113),z)) +(+(x,+(x112,x113)),z) -2|[1]-> +(x,+(+(x112,x113),z)) peak: +(x115,+(x116,y)) <-2|[1]- +(+(x115,x116),y) -4|[1]-> +(y,+(x115,x116)) joins: +(x115,+(x116,y)) -3|[1]-> +(+(x115,x116),y) +(y,+(x115,x116)) -4|[1]-> +(+(x115,x116),y) peak: +(+(0(),x119),x120) <-3|[1]- +(0(),+(x119,x120)) -0|[1]-> +(x119,x120) joins: +(+(0(),x119),x120) -0|0[1]-> +(x119,x120) peak: +(+(+(x,y),x122),x123) <-3|[1]- +(+(x,y),+(x122,x123)) -2|[1]-> +(x,+(y,+(x122,x123))) joins: +(+(+(x,y),x122),x123) -2|[1]-> +(+(x,y),+(x122,x123)) +(x,+(y,+(x122,x123))) -3|[1]-> +(+(x,y),+(x122,x123)) peak: +(+(+(x,x125),x126),z) <-3|0[1]- +(+(x,+(x125,x126)),z) -2|[1]-> +(x,+(+(x125,x126),z)) joins: +(+(+(x,x125),x126),z) -2|0[1]-> +(+(x,+(x125,x126)),z) +(x,+(+(x125,x126),z)) -3|[1]-> +(+(x,+(x125,x126)),z) peak: +(x,+(+(y,x128),x129)) <-3|1[1]- +(x,+(y,+(x128,x129))) -3|[1]-> +(+(x,y),+(x128,x129)) joins: +(x,+(+(y,x128),x129)) -2|1[1]-> +(x,+(y,+(x128,x129))) +(+(x,y),+(x128,x129)) -2|[1]-> +(x,+(y,+(x128,x129))) peak: +(+(x,x131),x132) <-3|[1]- +(x,+(x131,x132)) -4|[1]-> +(+(x131,x132),x) joins: +(+(x,x131),x132) -2|[1]-> +(x,+(x131,x132)) +(+(x131,x132),x) -4|[1]-> +(x,+(x131,x132)) peak: +(x,0()) <-4|[1]- +(0(),x) -0|[1]-> x joins: +(x,0()) -1|[1]-> x peak: +(0(),x) <-4|[1]- +(x,0()) -1|[1]-> x joins: +(0(),x) -0|[1]-> 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