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