Problem: +(0(),y) -> y +(s(x),y) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) inc(+(x,y)) -> +(inc(x),y) Proof: Commute Transformation Processor: +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) inc(+(x,y)) -> +(inc(x),y) Church Rosser Transformation Processor (star): strict: weak: inc(0)(+(0)(x)) -> +(0)(inc(0)(x)) inc(0)(+(1)(y)) -> +(1)(y) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) inc(0)(x) -> s(0)(x) +(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: 23 0() <-0|[]- +(0(),0()) -1|[]-> 0() s(x) <-0|[]- +(0(),s(x)) -3|[]-> s(+(x,0())) y <-0|[]- +(0(),y) -5|[]-> +(y,0()) inc(y) <-0|0[]- inc(+(0(),y)) -6|[]-> +(inc(0()),y) 0() <-1|[]- +(0(),0()) -0|[]-> 0() s(x) <-1|[]- +(s(x),0()) -2|[]-> s(+(x,0())) x <-1|[]- +(x,0()) -5|[]-> +(0(),x) inc(x) <-1|0[]- inc(+(x,0())) -6|[]-> +(inc(x),0()) s(+(x142,0())) <-2|[]- +(s(x142),0()) -1|[]-> s(x142) s(+(x144,s(x))) <-2|[]- +(s(x144),s(x)) -3|[]-> s(+(x,s(x144))) s(+(x146,y)) <-2|[]- +(s(x146),y) -5|[]-> +(y,s(x146)) inc(s(+(x148,y))) <-2|0[]- inc(+(s(x148),y)) -6|[]-> +(inc(s(x148)),y) s(+(x151,0())) <-3|[]- +(0(),s(x151)) -0|[]-> s(x151) s(+(x153,s(x))) <-3|[]- +(s(x),s(x153)) -2|[]-> s(+(x,s(x153))) s(+(x155,x)) <-3|[]- +(x,s(x155)) -5|[]-> +(s(x155),x) inc(s(+(x157,x))) <-3|0[]- inc(+(x,s(x157))) -6|[]-> +(inc(x),s(x157)) s(+(x,y)) <-4|[]- inc(+(x,y)) -6|[]-> +(inc(x),y) +(y,0()) <-5|[]- +(0(),y) -0|[]-> y +(0(),y) <-5|[]- +(y,0()) -1|[]-> y +(y,s(x)) <-5|[]- +(s(x),y) -2|[]-> s(+(x,y)) +(s(x),y) <-5|[]- +(y,s(x)) -3|[]-> s(+(x,y)) inc(+(y,x)) <-5|0[]- inc(+(x,y)) -6|[]-> +(inc(x),y) +(inc(x169),x170) <-6|[]- inc(+(x169,x170)) -4|[]-> s(+(x169,x170)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [+(1)](x0) = 2x0 + 2, [+(0)](x0) = 2x0 + 2, [inc(0)](x0) = x0 orientation: inc(0)(+(0)(x)) = 2x + 2 >= 2x + 2 = +(0)(inc(0)(x)) inc(0)(+(1)(y)) = 2y + 2 >= 2y + 2 = +(1)(y) +(0)(x) = 2x + 2 >= 2x + 2 = +(1)(x) +(1)(y) = 2y + 2 >= 2y + 2 = +(0)(y) inc(0)(x) = x >= x = s(0)(x) +(0)(y) = 2y + 2 >= 2y + 2 = s(0)(+(1)(y)) +(1)(s(0)(x)) = 2x + 2 >= 2x + 2 = s(0)(+(0)(x)) +(0)(s(0)(x)) = 2x + 2 >= 2x + 2 = s(0)(+(0)(x)) +(1)(y) = 2y + 2 >= 2y + 2 = s(0)(+(1)(y)) +(0)(y) = 2y + 2 >= y = y +(1)(y) = 2y + 2 >= y = y problem: strict: weak: inc(0)(+(0)(x)) -> +(0)(inc(0)(x)) inc(0)(+(1)(y)) -> +(1)(y) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) inc(0)(x) -> s(0)(x) +(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)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [+(1)](x0) = x0, [+(0)](x0) = x0, [inc(0)](x0) = 2x0 + 1 orientation: inc(0)(+(0)(x)) = 2x + 1 >= 2x + 1 = +(0)(inc(0)(x)) inc(0)(+(1)(y)) = 2y + 1 >= y = +(1)(y) +(0)(x) = x >= x = +(1)(x) +(1)(y) = y >= y = +(0)(y) inc(0)(x) = 2x + 1 >= x = s(0)(x) +(0)(y) = y >= y = s(0)(+(1)(y)) +(1)(s(0)(x)) = x >= x = s(0)(+(0)(x)) +(0)(s(0)(x)) = x >= x = s(0)(+(0)(x)) +(1)(y) = y >= y = s(0)(+(1)(y)) problem: strict: weak: inc(0)(+(0)(x)) -> +(0)(inc(0)(x)) +(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)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [+(1)](x0) = x0 + 1, [+(0)](x0) = x0 + 1, [inc(0)](x0) = 2x0 orientation: inc(0)(+(0)(x)) = 2x + 2 >= 2x + 1 = +(0)(inc(0)(x)) +(0)(x) = x + 1 >= x + 1 = +(1)(x) +(1)(y) = y + 1 >= y + 1 = +(0)(y) +(0)(y) = y + 1 >= y + 1 = s(0)(+(1)(y)) +(1)(s(0)(x)) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(0)(s(0)(x)) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(1)(y) = y + 1 >= y + 1 = s(0)(+(1)(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 inc(+(0(),y)) -> inc(y) inc(+(0(),y)) -> +(inc(0()),y) inc(y) -> s(y) +(inc(0()),y) -> +(s(0()),y) +(s(0()),y) -> s(+(0(),y)) s(+(0(),y)) -> s(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 inc(+(x,0())) -> inc(x) inc(+(x,0())) -> +(inc(x),0()) +(inc(x),0()) -> inc(x) +(s(x142),0()) -> s(+(x142,0())) +(s(x142),0()) -> s(x142) s(+(x142,0())) -> s(x142) +(s(x144),s(x)) -> s(+(x144,s(x))) +(s(x144),s(x)) -> s(+(x,s(x144))) s(+(x144,s(x))) -> s(s(+(x,x144))) s(+(x,s(x144))) -> s(s(+(x144,x))) s(s(+(x144,x))) -> s(s(+(x,x144))) s(+(x144,s(x))) -> s(+(s(x),x144)) s(+(s(x),x144)) -> s(s(+(x,x144))) s(+(x,s(x144))) -> s(s(+(x144,x))) s(s(+(x144,x))) -> s(s(+(x,x144))) s(+(x144,s(x))) -> s(s(+(x,x144))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(+(x,s(x144))) -> s(s(+(x144,x))) s(+(x144,s(x))) -> s(s(+(x,x144))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(+(x,s(x144))) -> s(+(s(x144),x)) s(+(s(x144),x)) -> s(s(+(x144,x))) +(s(x146),y) -> s(+(x146,y)) +(s(x146),y) -> +(y,s(x146)) +(y,s(x146)) -> s(+(x146,y)) inc(+(s(x148),y)) -> inc(s(+(x148,y))) inc(+(s(x148),y)) -> +(inc(s(x148)),y) inc(s(+(x148,y))) -> s(s(+(x148,y))) +(inc(s(x148)),y) -> +(s(s(x148)),y) +(s(s(x148)),y) -> s(+(s(x148),y)) s(+(s(x148),y)) -> s(s(+(x148,y))) inc(s(+(x148,y))) -> s(s(+(x148,y))) s(s(+(x148,y))) -> s(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) +(inc(s(x148)),y) -> +(s(s(x148)),y) +(s(s(x148)),y) -> s(+(s(x148),y)) s(+(s(x148),y)) -> s(s(+(x148,y))) inc(s(+(x148,y))) -> inc(s(+(y,x148))) inc(s(+(y,x148))) -> s(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) +(inc(s(x148)),y) -> +(s(s(x148)),y) +(s(s(x148)),y) -> s(+(s(x148),y)) s(+(s(x148),y)) -> s(s(+(x148,y))) +(0(),s(x151)) -> s(+(x151,0())) +(0(),s(x151)) -> s(x151) s(+(x151,0())) -> s(x151) +(s(x),s(x153)) -> s(+(x153,s(x))) +(s(x),s(x153)) -> s(+(x,s(x153))) s(+(x153,s(x))) -> s(s(+(x,x153))) s(+(x,s(x153))) -> s(s(+(x153,x))) s(s(+(x153,x))) -> s(s(+(x,x153))) s(+(x153,s(x))) -> s(+(s(x),x153)) s(+(s(x),x153)) -> s(s(+(x,x153))) s(+(x,s(x153))) -> s(s(+(x153,x))) s(s(+(x153,x))) -> s(s(+(x,x153))) s(+(x153,s(x))) -> s(s(+(x,x153))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(+(x,s(x153))) -> s(s(+(x153,x))) s(+(x153,s(x))) -> s(s(+(x,x153))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(+(x,s(x153))) -> s(+(s(x153),x)) s(+(s(x153),x)) -> s(s(+(x153,x))) +(x,s(x155)) -> s(+(x155,x)) +(x,s(x155)) -> +(s(x155),x) +(s(x155),x) -> s(+(x155,x)) inc(+(x,s(x157))) -> inc(s(+(x157,x))) inc(+(x,s(x157))) -> +(inc(x),s(x157)) inc(s(+(x157,x))) -> s(s(+(x157,x))) +(inc(x),s(x157)) -> +(s(x),s(x157)) +(s(x),s(x157)) -> s(+(x,s(x157))) s(+(x,s(x157))) -> s(s(+(x157,x))) inc(s(+(x157,x))) -> s(s(+(x157,x))) s(s(+(x157,x))) -> s(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) +(inc(x),s(x157)) -> +(s(x),s(x157)) +(s(x),s(x157)) -> s(+(x,s(x157))) s(+(x,s(x157))) -> s(s(+(x157,x))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) inc(s(+(x,x157))) -> s(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) +(inc(x),s(x157)) -> +(s(x),s(x157)) +(s(x),s(x157)) -> s(+(x,s(x157))) s(+(x,s(x157))) -> s(s(+(x157,x))) inc(s(+(x157,x))) -> s(s(+(x157,x))) s(s(+(x157,x))) -> s(s(+(x,x157))) +(inc(x),s(x157)) -> s(+(x157,inc(x))) s(+(x157,inc(x))) -> s(+(x157,s(x))) s(+(x157,s(x))) -> s(s(+(x,x157))) inc(s(+(x157,x))) -> s(s(+(x157,x))) s(s(+(x157,x))) -> s(s(+(x,x157))) +(inc(x),s(x157)) -> +(s(x),s(x157)) +(s(x),s(x157)) -> s(+(x157,s(x))) s(+(x157,s(x))) -> s(s(+(x,x157))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) inc(s(+(x,x157))) -> s(s(+(x,x157))) +(inc(x),s(x157)) -> s(+(x157,inc(x))) s(+(x157,inc(x))) -> s(+(x157,s(x))) s(+(x157,s(x))) -> s(s(+(x,x157))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) inc(s(+(x,x157))) -> s(s(+(x,x157))) +(inc(x),s(x157)) -> +(s(x),s(x157)) +(s(x),s(x157)) -> s(+(x157,s(x))) s(+(x157,s(x))) -> s(s(+(x,x157))) inc(+(x,y)) -> s(+(x,y)) inc(+(x,y)) -> +(inc(x),y) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) +(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)) inc(+(x,y)) -> inc(+(y,x)) inc(+(x,y)) -> +(inc(x),y) inc(+(y,x)) -> s(+(y,x)) s(+(y,x)) -> s(+(x,y)) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) inc(+(x,y)) -> s(+(x,y)) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) inc(+(x,y)) -> +(inc(x),y) inc(+(x169,x170)) -> +(inc(x169),x170) inc(+(x169,x170)) -> s(+(x169,x170)) +(inc(x169),x170) -> +(s(x169),x170) +(s(x169),x170) -> s(+(x169,x170)) weak: +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) inc(+(x,y)) -> +(inc(x),y) Matrix Interpretation Processor: dim=1 interpretation: [inc](x0) = 2x0 + 2, [s](x0) = x0 + 2, [+](x0, x1) = 2x0 + 2x1 + 2, [0] = 1 orientation: +(0(),0()) = 6 >= 1 = 0() +(0(),0()) = 6 >= 1 = 0() +(0(),s(x)) = 2x + 8 >= x + 2 = s(x) +(0(),s(x)) = 2x + 8 >= 2x + 6 = s(+(x,0())) s(+(x,0())) = 2x + 6 >= x + 2 = s(x) +(0(),y) = 2y + 4 >= y = y +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(y,0()) = 2y + 4 >= y = y inc(+(0(),y)) = 4y + 10 >= 2y + 2 = inc(y) inc(+(0(),y)) = 4y + 10 >= 2y + 10 = +(inc(0()),y) inc(y) = 2y + 2 >= y + 2 = s(y) +(inc(0()),y) = 2y + 10 >= 2y + 8 = +(s(0()),y) +(s(0()),y) = 2y + 8 >= 2y + 6 = s(+(0(),y)) s(+(0(),y)) = 2y + 6 >= y + 2 = s(y) +(0(),0()) = 6 >= 1 = 0() +(0(),0()) = 6 >= 1 = 0() +(s(x),0()) = 2x + 8 >= x + 2 = s(x) +(s(x),0()) = 2x + 8 >= 2x + 6 = s(+(x,0())) s(+(x,0())) = 2x + 6 >= x + 2 = s(x) +(x,0()) = 2x + 4 >= x = x +(x,0()) = 2x + 4 >= 2x + 4 = +(0(),x) +(0(),x) = 2x + 4 >= x = x inc(+(x,0())) = 4x + 10 >= 2x + 2 = inc(x) inc(+(x,0())) = 4x + 10 >= 4x + 8 = +(inc(x),0()) +(inc(x),0()) = 4x + 8 >= 2x + 2 = inc(x) +(s(x142),0()) = 2x142 + 8 >= 2x142 + 6 = s(+(x142,0())) +(s(x142),0()) = 2x142 + 8 >= x142 + 2 = s(x142) s(+(x142,0())) = 2x142 + 6 >= x142 + 2 = s(x142) +(s(x144),s(x)) = 2x + 2x144 + 10 >= 2x + 2x144 + 8 = s(+(x144,s(x))) +(s(x144),s(x)) = 2x + 2x144 + 10 >= 2x + 2x144 + 8 = s(+(x,s(x144))) s(+(x144,s(x))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(+(x,s(x144))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x144,x))) s(s(+(x144,x))) = 2x + 2x144 + 6 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(+(x144,s(x))) = 2x + 2x144 + 8 >= 2x + 2x144 + 8 = s(+(s(x),x144)) s(+(s(x),x144)) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(+(x,s(x144))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x144,x))) s(s(+(x144,x))) = 2x + 2x144 + 6 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(+(x144,s(x))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(s(+(x,x144))) = 2x + 2x144 + 6 >= 2x + 2x144 + 6 = s(s(+(x144,x))) s(+(x,s(x144))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x144,x))) s(+(x144,s(x))) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x,x144))) s(s(+(x,x144))) = 2x + 2x144 + 6 >= 2x + 2x144 + 6 = s(s(+(x144,x))) s(+(x,s(x144))) = 2x + 2x144 + 8 >= 2x + 2x144 + 8 = s(+(s(x144),x)) s(+(s(x144),x)) = 2x + 2x144 + 8 >= 2x + 2x144 + 6 = s(s(+(x144,x))) +(s(x146),y) = 2x146 + 2y + 6 >= 2x146 + 2y + 4 = s(+(x146,y)) +(s(x146),y) = 2x146 + 2y + 6 >= 2x146 + 2y + 6 = +(y,s(x146)) +(y,s(x146)) = 2x146 + 2y + 6 >= 2x146 + 2y + 4 = s(+(x146,y)) inc(+(s(x148),y)) = 4x148 + 4y + 14 >= 4x148 + 4y + 10 = inc(s(+(x148,y))) inc(+(s(x148),y)) = 4x148 + 4y + 14 >= 4x148 + 2y + 14 = +(inc(s(x148)),y) inc(s(+(x148,y))) = 4x148 + 4y + 10 >= 2x148 + 2y + 6 = s(s(+(x148,y))) +(inc(s(x148)),y) = 4x148 + 2y + 14 >= 2x148 + 2y + 10 = +(s(s(x148)),y) +(s(s(x148)),y) = 2x148 + 2y + 10 >= 2x148 + 2y + 8 = s(+(s(x148),y)) s(+(s(x148),y)) = 2x148 + 2y + 8 >= 2x148 + 2y + 6 = s(s(+(x148,y))) inc(s(+(x148,y))) = 4x148 + 4y + 10 >= 2x148 + 2y + 6 = s(s(+(x148,y))) s(s(+(x148,y))) = 2x148 + 2y + 6 >= 2x148 + 2y + 6 = s(s(+(y,x148))) s(s(+(y,x148))) = 2x148 + 2y + 6 >= 2x148 + 2y + 6 = s(s(+(x148,y))) +(inc(s(x148)),y) = 4x148 + 2y + 14 >= 2x148 + 2y + 10 = +(s(s(x148)),y) +(s(s(x148)),y) = 2x148 + 2y + 10 >= 2x148 + 2y + 8 = s(+(s(x148),y)) s(+(s(x148),y)) = 2x148 + 2y + 8 >= 2x148 + 2y + 6 = s(s(+(x148,y))) inc(s(+(x148,y))) = 4x148 + 4y + 10 >= 4x148 + 4y + 10 = inc(s(+(y,x148))) inc(s(+(y,x148))) = 4x148 + 4y + 10 >= 2x148 + 2y + 6 = s(s(+(y,x148))) s(s(+(y,x148))) = 2x148 + 2y + 6 >= 2x148 + 2y + 6 = s(s(+(x148,y))) +(inc(s(x148)),y) = 4x148 + 2y + 14 >= 2x148 + 2y + 10 = +(s(s(x148)),y) +(s(s(x148)),y) = 2x148 + 2y + 10 >= 2x148 + 2y + 8 = s(+(s(x148),y)) s(+(s(x148),y)) = 2x148 + 2y + 8 >= 2x148 + 2y + 6 = s(s(+(x148,y))) +(0(),s(x151)) = 2x151 + 8 >= 2x151 + 6 = s(+(x151,0())) +(0(),s(x151)) = 2x151 + 8 >= x151 + 2 = s(x151) s(+(x151,0())) = 2x151 + 6 >= x151 + 2 = s(x151) +(s(x),s(x153)) = 2x + 2x153 + 10 >= 2x + 2x153 + 8 = s(+(x153,s(x))) +(s(x),s(x153)) = 2x + 2x153 + 10 >= 2x + 2x153 + 8 = s(+(x,s(x153))) s(+(x153,s(x))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(+(x,s(x153))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x153,x))) s(s(+(x153,x))) = 2x + 2x153 + 6 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(+(x153,s(x))) = 2x + 2x153 + 8 >= 2x + 2x153 + 8 = s(+(s(x),x153)) s(+(s(x),x153)) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(+(x,s(x153))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x153,x))) s(s(+(x153,x))) = 2x + 2x153 + 6 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(+(x153,s(x))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(s(+(x,x153))) = 2x + 2x153 + 6 >= 2x + 2x153 + 6 = s(s(+(x153,x))) s(+(x,s(x153))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x153,x))) s(+(x153,s(x))) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x,x153))) s(s(+(x,x153))) = 2x + 2x153 + 6 >= 2x + 2x153 + 6 = s(s(+(x153,x))) s(+(x,s(x153))) = 2x + 2x153 + 8 >= 2x + 2x153 + 8 = s(+(s(x153),x)) s(+(s(x153),x)) = 2x + 2x153 + 8 >= 2x + 2x153 + 6 = s(s(+(x153,x))) +(x,s(x155)) = 2x + 2x155 + 6 >= 2x + 2x155 + 4 = s(+(x155,x)) +(x,s(x155)) = 2x + 2x155 + 6 >= 2x + 2x155 + 6 = +(s(x155),x) +(s(x155),x) = 2x + 2x155 + 6 >= 2x + 2x155 + 4 = s(+(x155,x)) inc(+(x,s(x157))) = 4x + 4x157 + 14 >= 4x + 4x157 + 10 = inc(s(+(x157,x))) inc(+(x,s(x157))) = 4x + 4x157 + 14 >= 4x + 2x157 + 10 = +(inc(x),s(x157)) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x157,x))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 2x + 2x157 + 10 = +(s(x),s(x157)) +(s(x),s(x157)) = 2x + 2x157 + 10 >= 2x + 2x157 + 8 = s(+(x,s(x157))) s(+(x,s(x157))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x157,x))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x157,x))) s(s(+(x157,x))) = 2x + 2x157 + 6 >= 2x + 2x157 + 6 = s(s(+(x,x157))) s(s(+(x,x157))) = 2x + 2x157 + 6 >= 2x + 2x157 + 6 = s(s(+(x157,x))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 2x + 2x157 + 10 = +(s(x),s(x157)) +(s(x),s(x157)) = 2x + 2x157 + 10 >= 2x + 2x157 + 8 = s(+(x,s(x157))) s(+(x,s(x157))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x157,x))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 4x + 4x157 + 10 = inc(s(+(x,x157))) inc(s(+(x,x157))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x,x157))) s(s(+(x,x157))) = 2x + 2x157 + 6 >= 2x + 2x157 + 6 = s(s(+(x157,x))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 2x + 2x157 + 10 = +(s(x),s(x157)) +(s(x),s(x157)) = 2x + 2x157 + 10 >= 2x + 2x157 + 8 = s(+(x,s(x157))) s(+(x,s(x157))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x157,x))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x157,x))) s(s(+(x157,x))) = 2x + 2x157 + 6 >= 2x + 2x157 + 6 = s(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 4x + 2x157 + 8 = s(+(x157,inc(x))) s(+(x157,inc(x))) = 4x + 2x157 + 8 >= 2x + 2x157 + 8 = s(+(x157,s(x))) s(+(x157,s(x))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x,x157))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x157,x))) s(s(+(x157,x))) = 2x + 2x157 + 6 >= 2x + 2x157 + 6 = s(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 2x + 2x157 + 10 = +(s(x),s(x157)) +(s(x),s(x157)) = 2x + 2x157 + 10 >= 2x + 2x157 + 8 = s(+(x157,s(x))) s(+(x157,s(x))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x,x157))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 4x + 4x157 + 10 = inc(s(+(x,x157))) inc(s(+(x,x157))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 4x + 2x157 + 8 = s(+(x157,inc(x))) s(+(x157,inc(x))) = 4x + 2x157 + 8 >= 2x + 2x157 + 8 = s(+(x157,s(x))) s(+(x157,s(x))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x,x157))) inc(s(+(x157,x))) = 4x + 4x157 + 10 >= 4x + 4x157 + 10 = inc(s(+(x,x157))) inc(s(+(x,x157))) = 4x + 4x157 + 10 >= 2x + 2x157 + 6 = s(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 10 >= 2x + 2x157 + 10 = +(s(x),s(x157)) +(s(x),s(x157)) = 2x + 2x157 + 10 >= 2x + 2x157 + 8 = s(+(x157,s(x))) s(+(x157,s(x))) = 2x + 2x157 + 8 >= 2x + 2x157 + 6 = s(s(+(x,x157))) inc(+(x,y)) = 4x + 4y + 6 >= 2x + 2y + 4 = s(+(x,y)) inc(+(x,y)) = 4x + 4y + 6 >= 4x + 2y + 6 = +(inc(x),y) +(inc(x),y) = 4x + 2y + 6 >= 2x + 2y + 6 = +(s(x),y) +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) +(0(),y) = 2y + 4 >= 2y + 4 = +(y,0()) +(0(),y) = 2y + 4 >= y = y +(y,0()) = 2y + 4 >= y = y +(y,0()) = 2y + 4 >= 2y + 4 = +(0(),y) +(y,0()) = 2y + 4 >= y = y +(0(),y) = 2y + 4 >= y = y +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 6 = +(y,s(x)) +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 6 >= 2x + 2y + 6 = +(s(x),y) +(y,s(x)) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) inc(+(x,y)) = 4x + 4y + 6 >= 4x + 4y + 6 = inc(+(y,x)) inc(+(x,y)) = 4x + 4y + 6 >= 4x + 2y + 6 = +(inc(x),y) inc(+(y,x)) = 4x + 4y + 6 >= 2x + 2y + 4 = s(+(y,x)) s(+(y,x)) = 2x + 2y + 4 >= 2x + 2y + 4 = s(+(x,y)) +(inc(x),y) = 4x + 2y + 6 >= 2x + 2y + 6 = +(s(x),y) +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) inc(+(y,x)) = 4x + 4y + 6 >= 4x + 4y + 6 = inc(+(x,y)) inc(+(x,y)) = 4x + 4y + 6 >= 2x + 2y + 4 = s(+(x,y)) +(inc(x),y) = 4x + 2y + 6 >= 2x + 2y + 6 = +(s(x),y) +(s(x),y) = 2x + 2y + 6 >= 2x + 2y + 4 = s(+(x,y)) inc(+(y,x)) = 4x + 4y + 6 >= 4x + 4y + 6 = inc(+(x,y)) inc(+(x,y)) = 4x + 4y + 6 >= 4x + 2y + 6 = +(inc(x),y) inc(+(x169,x170)) = 4x169 + 4x170 + 6 >= 4x169 + 2x170 + 6 = +(inc(x169),x170) inc(+(x169,x170)) = 4x169 + 4x170 + 6 >= 2x169 + 2x170 + 4 = s(+(x169,x170)) +(inc(x169),x170) = 4x169 + 2x170 + 6 >= 2x169 + 2x170 + 6 = +(s(x169),x170) +(s(x169),x170) = 2x169 + 2x170 + 6 >= 2x169 + 2x170 + 4 = s(+(x169,x170)) inc(x) = 2x + 2 >= x + 2 = s(x) +(x,y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,x) problem: strict: +(0(),y) -> +(y,0()) inc(+(0(),y)) -> +(inc(0()),y) inc(y) -> s(y) +(x,0()) -> +(0(),x) s(s(+(x144,x))) -> s(s(+(x,x144))) s(+(x144,s(x))) -> s(+(s(x),x144)) s(s(+(x144,x))) -> s(s(+(x,x144))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(+(x,s(x144))) -> s(+(s(x144),x)) +(s(x146),y) -> +(y,s(x146)) inc(+(s(x148),y)) -> +(inc(s(x148)),y) s(s(+(x148,y))) -> s(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) inc(s(+(x148,y))) -> inc(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) s(s(+(x153,x))) -> s(s(+(x,x153))) s(+(x153,s(x))) -> s(+(s(x),x153)) s(s(+(x153,x))) -> s(s(+(x,x153))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(+(x,s(x153))) -> s(+(s(x153),x)) +(x,s(x155)) -> +(s(x155),x) +(inc(x),s(x157)) -> +(s(x),s(x157)) s(s(+(x157,x))) -> s(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) +(inc(x),s(x157)) -> +(s(x),s(x157)) inc(s(+(x157,x))) -> inc(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) +(inc(x),s(x157)) -> +(s(x),s(x157)) s(s(+(x157,x))) -> s(s(+(x,x157))) s(+(x157,inc(x))) -> s(+(x157,s(x))) s(s(+(x157,x))) -> s(s(+(x,x157))) +(inc(x),s(x157)) -> +(s(x),s(x157)) inc(s(+(x157,x))) -> inc(s(+(x,x157))) s(+(x157,inc(x))) -> s(+(x157,s(x))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) +(inc(x),s(x157)) -> +(s(x),s(x157)) inc(+(x,y)) -> +(inc(x),y) +(inc(x),y) -> +(s(x),y) +(0(),y) -> +(y,0()) +(y,0()) -> +(0(),y) +(s(x),y) -> +(y,s(x)) +(y,s(x)) -> +(s(x),y) inc(+(x,y)) -> inc(+(y,x)) inc(+(x,y)) -> +(inc(x),y) s(+(y,x)) -> s(+(x,y)) +(inc(x),y) -> +(s(x),y) inc(+(y,x)) -> inc(+(x,y)) +(inc(x),y) -> +(s(x),y) inc(+(y,x)) -> inc(+(x,y)) inc(+(x,y)) -> +(inc(x),y) inc(+(x169,x170)) -> +(inc(x169),x170) +(inc(x169),x170) -> +(s(x169),x170) weak: inc(x) -> s(x) +(x,y) -> +(y,x) inc(+(x,y)) -> +(inc(x),y) Matrix Interpretation Processor: dim=1 interpretation: [inc](x0) = 4x0 + 3, [s](x0) = 2x0, [+](x0, x1) = x0 + x1 + 2, [0] = 1 orientation: +(0(),y) = y + 3 >= y + 3 = +(y,0()) inc(+(0(),y)) = 4y + 15 >= y + 9 = +(inc(0()),y) inc(y) = 4y + 3 >= 2y = s(y) +(x,0()) = x + 3 >= x + 3 = +(0(),x) s(s(+(x144,x))) = 4x + 4x144 + 8 >= 4x + 4x144 + 8 = s(s(+(x,x144))) s(+(x144,s(x))) = 4x + 2x144 + 4 >= 4x + 2x144 + 4 = s(+(s(x),x144)) s(s(+(x144,x))) = 4x + 4x144 + 8 >= 4x + 4x144 + 8 = s(s(+(x,x144))) s(s(+(x,x144))) = 4x + 4x144 + 8 >= 4x + 4x144 + 8 = s(s(+(x144,x))) s(s(+(x,x144))) = 4x + 4x144 + 8 >= 4x + 4x144 + 8 = s(s(+(x144,x))) s(+(x,s(x144))) = 2x + 4x144 + 4 >= 2x + 4x144 + 4 = s(+(s(x144),x)) +(s(x146),y) = 2x146 + y + 2 >= 2x146 + y + 2 = +(y,s(x146)) inc(+(s(x148),y)) = 8x148 + 4y + 11 >= 8x148 + y + 5 = +(inc(s(x148)),y) s(s(+(x148,y))) = 4x148 + 4y + 8 >= 4x148 + 4y + 8 = s(s(+(y,x148))) s(s(+(y,x148))) = 4x148 + 4y + 8 >= 4x148 + 4y + 8 = s(s(+(x148,y))) inc(s(+(x148,y))) = 8x148 + 8y + 19 >= 8x148 + 8y + 19 = inc(s(+(y,x148))) s(s(+(y,x148))) = 4x148 + 4y + 8 >= 4x148 + 4y + 8 = s(s(+(x148,y))) s(s(+(x153,x))) = 4x + 4x153 + 8 >= 4x + 4x153 + 8 = s(s(+(x,x153))) s(+(x153,s(x))) = 4x + 2x153 + 4 >= 4x + 2x153 + 4 = s(+(s(x),x153)) s(s(+(x153,x))) = 4x + 4x153 + 8 >= 4x + 4x153 + 8 = s(s(+(x,x153))) s(s(+(x,x153))) = 4x + 4x153 + 8 >= 4x + 4x153 + 8 = s(s(+(x153,x))) s(s(+(x,x153))) = 4x + 4x153 + 8 >= 4x + 4x153 + 8 = s(s(+(x153,x))) s(+(x,s(x153))) = 2x + 4x153 + 4 >= 2x + 4x153 + 4 = s(+(s(x153),x)) +(x,s(x155)) = x + 2x155 + 2 >= x + 2x155 + 2 = +(s(x155),x) +(inc(x),s(x157)) = 4x + 2x157 + 5 >= 2x + 2x157 + 2 = +(s(x),s(x157)) s(s(+(x157,x))) = 4x + 4x157 + 8 >= 4x + 4x157 + 8 = s(s(+(x,x157))) s(s(+(x,x157))) = 4x + 4x157 + 8 >= 4x + 4x157 + 8 = s(s(+(x157,x))) +(inc(x),s(x157)) = 4x + 2x157 + 5 >= 2x + 2x157 + 2 = +(s(x),s(x157)) inc(s(+(x157,x))) = 8x + 8x157 + 19 >= 8x + 8x157 + 19 = inc(s(+(x,x157))) s(s(+(x,x157))) = 4x + 4x157 + 8 >= 4x + 4x157 + 8 = s(s(+(x157,x))) +(inc(x),s(x157)) = 4x + 2x157 + 5 >= 2x + 2x157 + 2 = +(s(x),s(x157)) s(s(+(x157,x))) = 4x + 4x157 + 8 >= 4x + 4x157 + 8 = s(s(+(x,x157))) s(+(x157,inc(x))) = 8x + 2x157 + 10 >= 4x + 2x157 + 4 = s(+(x157,s(x))) s(s(+(x157,x))) = 4x + 4x157 + 8 >= 4x + 4x157 + 8 = s(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 5 >= 2x + 2x157 + 2 = +(s(x),s(x157)) inc(s(+(x157,x))) = 8x + 8x157 + 19 >= 8x + 8x157 + 19 = inc(s(+(x,x157))) s(+(x157,inc(x))) = 8x + 2x157 + 10 >= 4x + 2x157 + 4 = s(+(x157,s(x))) inc(s(+(x157,x))) = 8x + 8x157 + 19 >= 8x + 8x157 + 19 = inc(s(+(x,x157))) +(inc(x),s(x157)) = 4x + 2x157 + 5 >= 2x + 2x157 + 2 = +(s(x),s(x157)) inc(+(x,y)) = 4x + 4y + 11 >= 4x + y + 5 = +(inc(x),y) +(inc(x),y) = 4x + y + 5 >= 2x + y + 2 = +(s(x),y) +(0(),y) = y + 3 >= y + 3 = +(y,0()) +(y,0()) = y + 3 >= y + 3 = +(0(),y) +(s(x),y) = 2x + y + 2 >= 2x + y + 2 = +(y,s(x)) +(y,s(x)) = 2x + y + 2 >= 2x + y + 2 = +(s(x),y) inc(+(x,y)) = 4x + 4y + 11 >= 4x + 4y + 11 = inc(+(y,x)) inc(+(x,y)) = 4x + 4y + 11 >= 4x + y + 5 = +(inc(x),y) s(+(y,x)) = 2x + 2y + 4 >= 2x + 2y + 4 = s(+(x,y)) +(inc(x),y) = 4x + y + 5 >= 2x + y + 2 = +(s(x),y) inc(+(y,x)) = 4x + 4y + 11 >= 4x + 4y + 11 = inc(+(x,y)) +(inc(x),y) = 4x + y + 5 >= 2x + y + 2 = +(s(x),y) inc(+(y,x)) = 4x + 4y + 11 >= 4x + 4y + 11 = inc(+(x,y)) inc(+(x,y)) = 4x + 4y + 11 >= 4x + y + 5 = +(inc(x),y) inc(+(x169,x170)) = 4x169 + 4x170 + 11 >= 4x169 + x170 + 5 = +(inc(x169),x170) +(inc(x169),x170) = 4x169 + x170 + 5 >= 2x169 + x170 + 2 = +(s(x169),x170) inc(x) = 4x + 3 >= 2x = s(x) +(x,y) = x + y + 2 >= x + y + 2 = +(y,x) problem: strict: +(0(),y) -> +(y,0()) +(x,0()) -> +(0(),x) s(s(+(x144,x))) -> s(s(+(x,x144))) s(+(x144,s(x))) -> s(+(s(x),x144)) s(s(+(x144,x))) -> s(s(+(x,x144))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(s(+(x,x144))) -> s(s(+(x144,x))) s(+(x,s(x144))) -> s(+(s(x144),x)) +(s(x146),y) -> +(y,s(x146)) s(s(+(x148,y))) -> s(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) inc(s(+(x148,y))) -> inc(s(+(y,x148))) s(s(+(y,x148))) -> s(s(+(x148,y))) s(s(+(x153,x))) -> s(s(+(x,x153))) s(+(x153,s(x))) -> s(+(s(x),x153)) s(s(+(x153,x))) -> s(s(+(x,x153))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(s(+(x,x153))) -> s(s(+(x153,x))) s(+(x,s(x153))) -> s(+(s(x153),x)) +(x,s(x155)) -> +(s(x155),x) s(s(+(x157,x))) -> s(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) s(s(+(x,x157))) -> s(s(+(x157,x))) s(s(+(x157,x))) -> s(s(+(x,x157))) s(s(+(x157,x))) -> s(s(+(x,x157))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) inc(s(+(x157,x))) -> inc(s(+(x,x157))) +(0(),y) -> +(y,0()) +(y,0()) -> +(0(),y) +(s(x),y) -> +(y,s(x)) +(y,s(x)) -> +(s(x),y) inc(+(x,y)) -> inc(+(y,x)) s(+(y,x)) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) inc(+(y,x)) -> inc(+(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]- +(0(),0()) -1|[1,0,0,0]-> 0() joins: peak: s(x) <-0|[1,0,0,0]- +(0(),s(x)) -3|[1,0,0,0]-> s(+(x,0())) joins: s(+(x,0())) -1|0[0,0,0,0]-> s(x) peak: y <-0|[1,0,0,0]- +(0(),y) -5|[1,0,0,0]-> +(y,0()) joins: +(y,0()) -1|[1,0,0,0]-> y peak: inc(y) <-0|0[1,0,1,0]- inc(+(0(),y)) -6|[1,0,0,0]-> +(inc(0()),y) joins: inc(y) -4|[0,0,0,0]-> s(y) +(inc(0()),y) -4|0[0,2,0,1]-> +(s(0()),y) -2|[0,0,0,0]-> s(+(0(),y)) -0|0[0,0,0,0]-> s(y) peak: 0() <-1|[1,0,0,0]- +(0(),0()) -0|[1,0,0,0]-> 0() joins: peak: s(x) <-1|[1,0,0,0]- +(s(x),0()) -2|[1,0,0,0]-> s(+(x,0())) joins: s(+(x,0())) -1|0[0,0,0,0]-> s(x) peak: x <-1|[1,0,0,0]- +(x,0()) -5|[1,0,0,0]-> +(0(),x) joins: +(0(),x) -0|[1,0,0,0]-> x peak: inc(x) <-1|0[1,0,1,0]- inc(+(x,0())) -6|[1,0,0,0]-> +(inc(x),0()) joins: +(inc(x),0()) -1|[0,0,0,0]-> inc(x) peak: s(+(x142,0())) <-2|[1,0,0,0]- +(s(x142),0()) -1|[1,0,0,0]-> s(x142) joins: s(+(x142,0())) -1|0[0,0,0,0]-> s(x142) peak: s(+(x144,s(x))) <-2|[1,0,0,0]- +(s(x144),s(x)) -3|[1,0,0,0]-> s(+(x,s(x144))) joins: s(+(x144,s(x))) -3|0[0,0,0,0]-> s(s(+(x,x144))) s(+(x,s(x144))) -3|0[0,0,0,0]-> s(s(+(x144,x))) -5|0,0[0,0,0,0]-> s(s(+(x,x144))) peak: s(+(x146,y)) <-2|[1,0,0,0]- +(s(x146),y) -5|[1,0,0,0]-> +(y,s(x146)) joins: +(y,s(x146)) -3|[1,0,0,0]-> s(+(x146,y)) peak: inc(s(+(x148,y))) <-2|0[1,0,1,0]- inc(+(s(x148),y)) -6|[1,0,0,0]-> +(inc(s(x148)),y) joins: inc(s(+(x148,y))) -4|[0,0,0,0]-> s(s(+(x148,y))) +(inc(s(x148)),y) -4|0[0,2,0,1]-> +(s(s(x148)),y) -2|[0,0,0,0]-> s(+(s(x148),y)) -2|0[0,0,0,0]-> s(s(+(x148,y))) peak: s(+(x151,0())) <-3|[1,0,0,0]- +(0(),s(x151)) -0|[1,0,0,0]-> s(x151) joins: s(+(x151,0())) -1|0[0,0,0,0]-> s(x151) peak: s(+(x153,s(x))) <-3|[1,0,0,0]- +(s(x),s(x153)) -2|[1,0,0,0]-> s(+(x,s(x153))) joins: s(+(x153,s(x))) -3|0[0,0,0,0]-> s(s(+(x,x153))) s(+(x,s(x153))) -3|0[0,0,0,0]-> s(s(+(x153,x))) -5|0,0[0,0,0,0]-> s(s(+(x,x153))) peak: s(+(x155,x)) <-3|[1,0,0,0]- +(x,s(x155)) -5|[1,0,0,0]-> +(s(x155),x) joins: +(s(x155),x) -2|[1,0,0,0]-> s(+(x155,x)) peak: inc(s(+(x157,x))) <-3|0[1,0,1,0]- inc(+(x,s(x157))) -6|[1,0,0,0]-> +(inc(x),s(x157)) joins: inc(s(+(x157,x))) -4|[0,0,0,0]-> s(s(+(x157,x))) +(inc(x),s(x157)) -4|0[0,2,0,1]-> +(s(x),s(x157)) -2|[0,0,0,0]-> s(+(x,s(x157))) -3|0[0,0,0,0]-> s(s(+(x157,x))) peak: s(+(x,y)) <-4|[1,0,0,0]- inc(+(x,y)) -6|[1,0,0,0]-> +(inc(x),y) joins: +(inc(x),y) -4|0[0,2,0,1]-> +(s(x),y) -2|[0,0,0,0]-> s(+(x,y)) peak: +(y,0()) <-5|[1,0,0,0]- +(0(),y) -0|[1,0,0,0]-> y joins: +(y,0()) -1|[1,0,0,0]-> y peak: +(0(),y) <-5|[1,0,0,0]- +(y,0()) -1|[1,0,0,0]-> y joins: +(0(),y) -0|[1,0,0,0]-> y peak: +(y,s(x)) <-5|[1,0,0,0]- +(s(x),y) -2|[1,0,0,0]-> s(+(x,y)) joins: +(y,s(x)) -3|[1,0,0,0]-> s(+(x,y)) peak: +(s(x),y) <-5|[1,0,0,0]- +(y,s(x)) -3|[1,0,0,0]-> s(+(x,y)) joins: +(s(x),y) -2|[1,0,0,0]-> s(+(x,y)) peak: inc(+(y,x)) <-5|0[1,0,1,0]- inc(+(x,y)) -6|[1,0,0,0]-> +(inc(x),y) joins: inc(+(y,x)) -4|[1,0,0,0]-> s(+(y,x)) -5|0[0,0,0,0]-> s(+(x,y)) +(inc(x),y) -4|0[0,2,0,1]-> +(s(x),y) -2|[0,0,0,0]-> s(+(x,y)) peak: +(inc(x169),x170) <-6|[1,0,0,0]- inc(+(x169,x170)) -4|[1,0,0,0]-> s(+(x169,x170)) joins: +(inc(x169),x170) -4|0[0,2,0,1]-> +(s(x169),x170) -2|[0,0,0,0]-> s(+(x169,x170)) Qed