Problem: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(x,y) -> +(y,x) Proof: Commute Transformation Processor: +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,y) -> +(y,x) Church Rosser Transformation Processor (star): strict: weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(y) -> s(0)(+(1)(y)) +(1)(s(0)(x)) -> s(0)(+(0)(x)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(y) -> y +(1)(y) -> y critical peaks: 16 0() <-0|[]- +(0(),0()) -1|[]-> 0() s(x) <-0|[]- +(0(),s(x)) -3|[]-> s(+(x,0())) y <-0|[]- +(0(),y) -4|[]-> +(y,0()) 0() <-1|[]- +(0(),0()) -0|[]-> 0() s(x) <-1|[]- +(s(x),0()) -2|[]-> s(+(x,0())) x <-1|[]- +(x,0()) -4|[]-> +(0(),x) s(+(x80,0())) <-2|[]- +(s(x80),0()) -1|[]-> s(x80) s(+(x82,s(x))) <-2|[]- +(s(x82),s(x)) -3|[]-> s(+(x,s(x82))) s(+(x84,y)) <-2|[]- +(s(x84),y) -4|[]-> +(y,s(x84)) s(+(x87,0())) <-3|[]- +(0(),s(x87)) -0|[]-> s(x87) s(+(x89,s(x))) <-3|[]- +(s(x),s(x89)) -2|[]-> s(+(x,s(x89))) s(+(x91,x)) <-3|[]- +(x,s(x91)) -4|[]-> +(s(x91),x) +(y,0()) <-4|[]- +(0(),y) -0|[]-> y +(0(),y) <-4|[]- +(y,0()) -1|[]-> y +(y,s(x)) <-4|[]- +(s(x),y) -2|[]-> s(+(x,y)) +(s(x),y) <-4|[]- +(y,s(x)) -3|[]-> s(+(x,y)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [+(1)](x0) = 2x0 + 1, [+(0)](x0) = 2x0 + 1 orientation: +(0)(x) = 2x + 1 >= 2x + 1 = +(1)(x) +(1)(y) = 2y + 1 >= 2y + 1 = +(0)(y) +(0)(y) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y)) +(1)(s(0)(x)) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x)) +(0)(s(0)(x)) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x)) +(1)(y) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y)) +(0)(y) = 2y + 1 >= y = y +(1)(y) = 2y + 1 >= y = y problem: strict: weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(y) -> s(0)(+(1)(y)) +(1)(s(0)(x)) -> s(0)(+(0)(x)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) Shift Processor lab=left (dd): strict: +(0(),0()) -> 0() +(0(),0()) -> 0() +(0(),s(x)) -> s(x) +(0(),s(x)) -> s(+(x,0())) s(+(x,0())) -> s(x) +(0(),y) -> y +(0(),y) -> +(y,0()) +(y,0()) -> y +(0(),0()) -> 0() +(0(),0()) -> 0() +(s(x),0()) -> s(x) +(s(x),0()) -> s(+(x,0())) s(+(x,0())) -> s(x) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x +(s(x80),0()) -> s(+(x80,0())) +(s(x80),0()) -> s(x80) s(+(x80,0())) -> s(x80) +(s(x82),s(x)) -> s(+(x82,s(x))) +(s(x82),s(x)) -> s(+(x,s(x82))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(s(+(x82,x))) -> s(s(+(x,x82))) s(+(x82,s(x))) -> s(+(s(x),x82)) s(+(s(x),x82)) -> s(s(+(x,x82))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(s(+(x82,x))) -> s(s(+(x,x82))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(+(x,s(x82))) -> s(+(s(x82),x)) s(+(s(x82),x)) -> s(s(+(x82,x))) +(s(x84),y) -> s(+(x84,y)) +(s(x84),y) -> +(y,s(x84)) +(y,s(x84)) -> s(+(x84,y)) +(0(),s(x87)) -> s(+(x87,0())) +(0(),s(x87)) -> s(x87) s(+(x87,0())) -> s(x87) +(s(x),s(x89)) -> s(+(x89,s(x))) +(s(x),s(x89)) -> s(+(x,s(x89))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(s(+(x89,x))) -> s(s(+(x,x89))) s(+(x89,s(x))) -> s(+(s(x),x89)) s(+(s(x),x89)) -> s(s(+(x,x89))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(s(+(x89,x))) -> s(s(+(x,x89))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(+(x,s(x89))) -> s(+(s(x89),x)) s(+(s(x89),x)) -> s(s(+(x89,x))) +(x,s(x91)) -> s(+(x91,x)) +(x,s(x91)) -> +(s(x91),x) +(s(x91),x) -> s(+(x91,x)) +(0(),y) -> +(y,0()) +(0(),y) -> y +(y,0()) -> y +(y,0()) -> +(0(),y) +(y,0()) -> y +(0(),y) -> y +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(y,s(x)) -> +(s(x),y) +(y,s(x)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) weak: +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0, [+](x0, x1) = x0 + x1 + 1, [0] = 1 orientation: +(0(),0()) = 3 >= 1 = 0() +(0(),0()) = 3 >= 1 = 0() +(0(),s(x)) = x + 2 >= x = s(x) +(0(),s(x)) = x + 2 >= x + 2 = s(+(x,0())) s(+(x,0())) = x + 2 >= x = s(x) +(0(),y) = y + 2 >= y = y +(0(),y) = y + 2 >= y + 2 = +(y,0()) +(y,0()) = y + 2 >= y = y +(0(),0()) = 3 >= 1 = 0() +(0(),0()) = 3 >= 1 = 0() +(s(x),0()) = x + 2 >= x = s(x) +(s(x),0()) = x + 2 >= x + 2 = s(+(x,0())) s(+(x,0())) = x + 2 >= x = s(x) +(x,0()) = x + 2 >= x = x +(x,0()) = x + 2 >= x + 2 = +(0(),x) +(0(),x) = x + 2 >= x = x +(s(x80),0()) = x80 + 2 >= x80 + 2 = s(+(x80,0())) +(s(x80),0()) = x80 + 2 >= x80 = s(x80) s(+(x80,0())) = x80 + 2 >= x80 = s(x80) +(s(x82),s(x)) = x + x82 + 1 >= x + x82 + 1 = s(+(x82,s(x))) +(s(x82),s(x)) = x + x82 + 1 >= x + x82 + 1 = s(+(x,s(x82))) s(+(x82,s(x))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(+(x,s(x82))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) s(s(+(x82,x))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(+(x82,s(x))) = x + x82 + 1 >= x + x82 + 1 = s(+(s(x),x82)) s(+(s(x),x82)) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(+(x,s(x82))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) s(s(+(x82,x))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(+(x82,s(x))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(s(+(x,x82))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) s(+(x,s(x82))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) s(+(x82,s(x))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x,x82))) s(s(+(x,x82))) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) s(+(x,s(x82))) = x + x82 + 1 >= x + x82 + 1 = s(+(s(x82),x)) s(+(s(x82),x)) = x + x82 + 1 >= x + x82 + 1 = s(s(+(x82,x))) +(s(x84),y) = x84 + y + 1 >= x84 + y + 1 = s(+(x84,y)) +(s(x84),y) = x84 + y + 1 >= x84 + y + 1 = +(y,s(x84)) +(y,s(x84)) = x84 + y + 1 >= x84 + y + 1 = s(+(x84,y)) +(0(),s(x87)) = x87 + 2 >= x87 + 2 = s(+(x87,0())) +(0(),s(x87)) = x87 + 2 >= x87 = s(x87) s(+(x87,0())) = x87 + 2 >= x87 = s(x87) +(s(x),s(x89)) = x + x89 + 1 >= x + x89 + 1 = s(+(x89,s(x))) +(s(x),s(x89)) = x + x89 + 1 >= x + x89 + 1 = s(+(x,s(x89))) s(+(x89,s(x))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(+(x,s(x89))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) s(s(+(x89,x))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(+(x89,s(x))) = x + x89 + 1 >= x + x89 + 1 = s(+(s(x),x89)) s(+(s(x),x89)) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(+(x,s(x89))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) s(s(+(x89,x))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(+(x89,s(x))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(s(+(x,x89))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) s(+(x,s(x89))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) s(+(x89,s(x))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x,x89))) s(s(+(x,x89))) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) s(+(x,s(x89))) = x + x89 + 1 >= x + x89 + 1 = s(+(s(x89),x)) s(+(s(x89),x)) = x + x89 + 1 >= x + x89 + 1 = s(s(+(x89,x))) +(x,s(x91)) = x + x91 + 1 >= x + x91 + 1 = s(+(x91,x)) +(x,s(x91)) = x + x91 + 1 >= x + x91 + 1 = +(s(x91),x) +(s(x91),x) = x + x91 + 1 >= x + x91 + 1 = s(+(x91,x)) +(0(),y) = y + 2 >= y + 2 = +(y,0()) +(0(),y) = y + 2 >= y = y +(y,0()) = y + 2 >= y = y +(y,0()) = y + 2 >= y + 2 = +(0(),y) +(y,0()) = y + 2 >= y = y +(0(),y) = y + 2 >= y = y +(s(x),y) = x + y + 1 >= x + y + 1 = +(y,s(x)) +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(y,s(x)) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(y,s(x)) = x + y + 1 >= x + y + 1 = +(s(x),y) +(y,s(x)) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: +(0(),s(x)) -> s(+(x,0())) +(0(),y) -> +(y,0()) +(s(x),0()) -> s(+(x,0())) +(x,0()) -> +(0(),x) +(s(x80),0()) -> s(+(x80,0())) +(s(x82),s(x)) -> s(+(x82,s(x))) +(s(x82),s(x)) -> s(+(x,s(x82))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(s(+(x82,x))) -> s(s(+(x,x82))) s(+(x82,s(x))) -> s(+(s(x),x82)) s(+(s(x),x82)) -> s(s(+(x,x82))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(s(+(x82,x))) -> s(s(+(x,x82))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(+(x,s(x82))) -> s(s(+(x82,x))) s(+(x82,s(x))) -> s(s(+(x,x82))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(+(x,s(x82))) -> s(+(s(x82),x)) s(+(s(x82),x)) -> s(s(+(x82,x))) +(s(x84),y) -> s(+(x84,y)) +(s(x84),y) -> +(y,s(x84)) +(y,s(x84)) -> s(+(x84,y)) +(0(),s(x87)) -> s(+(x87,0())) +(s(x),s(x89)) -> s(+(x89,s(x))) +(s(x),s(x89)) -> s(+(x,s(x89))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(s(+(x89,x))) -> s(s(+(x,x89))) s(+(x89,s(x))) -> s(+(s(x),x89)) s(+(s(x),x89)) -> s(s(+(x,x89))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(s(+(x89,x))) -> s(s(+(x,x89))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(+(x,s(x89))) -> s(s(+(x89,x))) s(+(x89,s(x))) -> s(s(+(x,x89))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(+(x,s(x89))) -> s(+(s(x89),x)) s(+(s(x89),x)) -> s(s(+(x89,x))) +(x,s(x91)) -> s(+(x91,x)) +(x,s(x91)) -> +(s(x91),x) +(s(x91),x) -> s(+(x91,x)) +(0(),y) -> +(y,0()) +(y,0()) -> +(0(),y) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(y,s(x)) -> +(s(x),y) +(y,s(x)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) weak: +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0 + 2, [+](x0, x1) = 2x0 + 2x1, [0] = 0 orientation: +(0(),s(x)) = 2x + 4 >= 2x + 2 = s(+(x,0())) +(0(),y) = 2y >= 2y = +(y,0()) +(s(x),0()) = 2x + 4 >= 2x + 2 = s(+(x,0())) +(x,0()) = 2x >= 2x = +(0(),x) +(s(x80),0()) = 2x80 + 4 >= 2x80 + 2 = s(+(x80,0())) +(s(x82),s(x)) = 2x + 2x82 + 8 >= 2x + 2x82 + 6 = s(+(x82,s(x))) +(s(x82),s(x)) = 2x + 2x82 + 8 >= 2x + 2x82 + 6 = s(+(x,s(x82))) s(+(x82,s(x))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(+(x,s(x82))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x82,x))) s(s(+(x82,x))) = 2x + 2x82 + 4 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(+(x82,s(x))) = 2x + 2x82 + 6 >= 2x + 2x82 + 6 = s(+(s(x),x82)) s(+(s(x),x82)) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(+(x,s(x82))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x82,x))) s(s(+(x82,x))) = 2x + 2x82 + 4 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(+(x82,s(x))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(s(+(x,x82))) = 2x + 2x82 + 4 >= 2x + 2x82 + 4 = s(s(+(x82,x))) s(+(x,s(x82))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x82,x))) s(+(x82,s(x))) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x,x82))) s(s(+(x,x82))) = 2x + 2x82 + 4 >= 2x + 2x82 + 4 = s(s(+(x82,x))) s(+(x,s(x82))) = 2x + 2x82 + 6 >= 2x + 2x82 + 6 = s(+(s(x82),x)) s(+(s(x82),x)) = 2x + 2x82 + 6 >= 2x + 2x82 + 4 = s(s(+(x82,x))) +(s(x84),y) = 2x84 + 2y + 4 >= 2x84 + 2y + 2 = s(+(x84,y)) +(s(x84),y) = 2x84 + 2y + 4 >= 2x84 + 2y + 4 = +(y,s(x84)) +(y,s(x84)) = 2x84 + 2y + 4 >= 2x84 + 2y + 2 = s(+(x84,y)) +(0(),s(x87)) = 2x87 + 4 >= 2x87 + 2 = s(+(x87,0())) +(s(x),s(x89)) = 2x + 2x89 + 8 >= 2x + 2x89 + 6 = s(+(x89,s(x))) +(s(x),s(x89)) = 2x + 2x89 + 8 >= 2x + 2x89 + 6 = s(+(x,s(x89))) s(+(x89,s(x))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(+(x,s(x89))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x89,x))) s(s(+(x89,x))) = 2x + 2x89 + 4 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(+(x89,s(x))) = 2x + 2x89 + 6 >= 2x + 2x89 + 6 = s(+(s(x),x89)) s(+(s(x),x89)) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(+(x,s(x89))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x89,x))) s(s(+(x89,x))) = 2x + 2x89 + 4 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(+(x89,s(x))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(s(+(x,x89))) = 2x + 2x89 + 4 >= 2x + 2x89 + 4 = s(s(+(x89,x))) s(+(x,s(x89))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x89,x))) s(+(x89,s(x))) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x,x89))) s(s(+(x,x89))) = 2x + 2x89 + 4 >= 2x + 2x89 + 4 = s(s(+(x89,x))) s(+(x,s(x89))) = 2x + 2x89 + 6 >= 2x + 2x89 + 6 = s(+(s(x89),x)) s(+(s(x89),x)) = 2x + 2x89 + 6 >= 2x + 2x89 + 4 = s(s(+(x89,x))) +(x,s(x91)) = 2x + 2x91 + 4 >= 2x + 2x91 + 2 = s(+(x91,x)) +(x,s(x91)) = 2x + 2x91 + 4 >= 2x + 2x91 + 4 = +(s(x91),x) +(s(x91),x) = 2x + 2x91 + 4 >= 2x + 2x91 + 2 = s(+(x91,x)) +(0(),y) = 2y >= 2y = +(y,0()) +(y,0()) = 2y >= 2y = +(0(),y) +(s(x),y) = 2x + 2y + 4 >= 2x + 2y + 4 = +(y,s(x)) +(s(x),y) = 2x + 2y + 4 >= 2x + 2y + 2 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 4 >= 2x + 2y + 2 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 4 >= 2x + 2y + 4 = +(s(x),y) +(y,s(x)) = 2x + 2y + 4 >= 2x + 2y + 2 = s(+(x,y)) +(s(x),y) = 2x + 2y + 4 >= 2x + 2y + 2 = s(+(x,y)) +(x,y) = 2x + 2y >= 2x + 2y = +(y,x) problem: strict: +(0(),y) -> +(y,0()) +(x,0()) -> +(0(),x) s(s(+(x82,x))) -> s(s(+(x,x82))) s(+(x82,s(x))) -> s(+(s(x),x82)) s(s(+(x82,x))) -> s(s(+(x,x82))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(s(+(x,x82))) -> s(s(+(x82,x))) s(+(x,s(x82))) -> s(+(s(x82),x)) +(s(x84),y) -> +(y,s(x84)) s(s(+(x89,x))) -> s(s(+(x,x89))) s(+(x89,s(x))) -> s(+(s(x),x89)) s(s(+(x89,x))) -> s(s(+(x,x89))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(s(+(x,x89))) -> s(s(+(x89,x))) s(+(x,s(x89))) -> s(+(s(x89),x)) +(x,s(x91)) -> +(s(x91),x) +(0(),y) -> +(y,0()) +(y,0()) -> +(0(),y) +(s(x),y) -> +(y,s(x)) +(y,s(x)) -> +(s(x),y) weak: +(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(),0()) -1|[1,0]-> 0() joins: peak: s(x) <-0|[1,0]- +(0(),s(x)) -3|[1,0]-> s(+(x,0())) joins: s(+(x,0())) -1|0[0,0]-> s(x) peak: y <-0|[1,0]- +(0(),y) -4|[1,0]-> +(y,0()) joins: +(y,0()) -1|[1,0]-> y peak: 0() <-1|[1,0]- +(0(),0()) -0|[1,0]-> 0() joins: peak: s(x) <-1|[1,0]- +(s(x),0()) -2|[1,0]-> s(+(x,0())) joins: s(+(x,0())) -1|0[0,0]-> s(x) peak: x <-1|[1,0]- +(x,0()) -4|[1,0]-> +(0(),x) joins: +(0(),x) -0|[1,0]-> x peak: s(+(x80,0())) <-2|[1,0]- +(s(x80),0()) -1|[1,0]-> s(x80) joins: s(+(x80,0())) -1|0[0,0]-> s(x80) peak: s(+(x82,s(x))) <-2|[1,0]- +(s(x82),s(x)) -3|[1,0]-> s(+(x,s(x82))) joins: s(+(x82,s(x))) -3|0[0,0]-> s(s(+(x,x82))) s(+(x,s(x82))) -3|0[0,0]-> s(s(+(x82,x))) -4|0,0[0,0]-> s(s(+(x,x82))) peak: s(+(x84,y)) <-2|[1,0]- +(s(x84),y) -4|[1,0]-> +(y,s(x84)) joins: +(y,s(x84)) -3|[1,0]-> s(+(x84,y)) peak: s(+(x87,0())) <-3|[1,0]- +(0(),s(x87)) -0|[1,0]-> s(x87) joins: s(+(x87,0())) -1|0[0,0]-> s(x87) peak: s(+(x89,s(x))) <-3|[1,0]- +(s(x),s(x89)) -2|[1,0]-> s(+(x,s(x89))) joins: s(+(x89,s(x))) -3|0[0,0]-> s(s(+(x,x89))) s(+(x,s(x89))) -3|0[0,0]-> s(s(+(x89,x))) -4|0,0[0,0]-> s(s(+(x,x89))) peak: s(+(x91,x)) <-3|[1,0]- +(x,s(x91)) -4|[1,0]-> +(s(x91),x) joins: +(s(x91),x) -2|[1,0]-> s(+(x91,x)) peak: +(y,0()) <-4|[1,0]- +(0(),y) -0|[1,0]-> y joins: +(y,0()) -1|[1,0]-> y peak: +(0(),y) <-4|[1,0]- +(y,0()) -1|[1,0]-> y joins: +(0(),y) -0|[1,0]-> y peak: +(y,s(x)) <-4|[1,0]- +(s(x),y) -2|[1,0]-> s(+(x,y)) joins: +(y,s(x)) -3|[1,0]-> s(+(x,y)) peak: +(s(x),y) <-4|[1,0]- +(y,s(x)) -3|[1,0]-> s(+(x,y)) joins: +(s(x),y) -2|[1,0]-> s(+(x,y)) Qed