Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) inc(+(x,y)) -> +(inc(x),y) Proof: 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)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(1)(y) -> y +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) +(0)(x) -> x critical peaks: 23 0() <-0|[]- +(0(),0()) -2|[]-> 0() s(x) <-0|[]- +(s(x),0()) -3|[]-> s(+(x,0())) x <-0|[]- +(x,0()) -5|[]-> +(0(),x) inc(x) <-0|0[]- inc(+(x,0())) -6|[]-> +(inc(x),0()) s(+(0(),x139)) <-1|[]- +(0(),s(x139)) -2|[]-> s(x139) s(+(s(x),x141)) <-1|[]- +(s(x),s(x141)) -3|[]-> s(+(x,s(x141))) s(+(x,x143)) <-1|[]- +(x,s(x143)) -5|[]-> +(s(x143),x) inc(s(+(x,x145))) <-1|0[]- inc(+(x,s(x145))) -6|[]-> +(inc(x),s(x145)) 0() <-2|[]- +(0(),0()) -0|[]-> 0() s(y) <-2|[]- +(0(),s(y)) -1|[]-> s(+(0(),y)) y <-2|[]- +(0(),y) -5|[]-> +(y,0()) inc(y) <-2|0[]- inc(+(0(),y)) -6|[]-> +(inc(0()),y) s(+(x150,0())) <-3|[]- +(s(x150),0()) -0|[]-> s(x150) s(+(x152,s(y))) <-3|[]- +(s(x152),s(y)) -1|[]-> s(+(s(x152),y)) s(+(x154,y)) <-3|[]- +(s(x154),y) -5|[]-> +(y,s(x154)) inc(s(+(x156,y))) <-3|0[]- inc(+(s(x156),y)) -6|[]-> +(inc(s(x156)),y) s(+(x,y)) <-4|[]- inc(+(x,y)) -6|[]-> +(inc(x),y) +(0(),x) <-5|[]- +(x,0()) -0|[]-> x +(s(y),x) <-5|[]- +(x,s(y)) -1|[]-> s(+(x,y)) +(y,0()) <-5|[]- +(0(),y) -2|[]-> y +(y,s(x)) <-5|[]- +(s(x),y) -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 + 1, [+(0)](x0) = 2x0 + 1, [inc(0)](x0) = x0 orientation: inc(0)(+(0)(x)) = 2x + 1 >= 2x + 1 = +(0)(inc(0)(x)) inc(0)(+(1)(y)) = 2y + 1 >= 2y + 1 = +(1)(y) +(0)(x) = 2x + 1 >= 2x + 1 = +(1)(x) +(1)(y) = 2y + 1 >= 2y + 1 = +(0)(y) inc(0)(x) = x >= x = s(0)(x) +(0)(s(0)(x)) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x)) +(1)(y) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y)) +(1)(y) = 2y + 1 >= y = y +(0)(x) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x)) +(1)(s(0)(y)) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y)) +(0)(x) = 2x + 1 >= x = x 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)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(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 + 1 orientation: inc(0)(+(0)(x)) = 2x + 3 >= 2x + 2 = +(0)(inc(0)(x)) inc(0)(+(1)(y)) = 2y + 3 >= y + 1 = +(1)(y) +(0)(x) = x + 1 >= x + 1 = +(1)(x) +(1)(y) = y + 1 >= y + 1 = +(0)(y) inc(0)(x) = 2x + 1 >= x = s(0)(x) +(0)(s(0)(x)) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(1)(y) = y + 1 >= y + 1 = s(0)(+(1)(y)) +(0)(x) = x + 1 >= x + 1 = s(0)(+(0)(x)) +(1)(s(0)(y)) = y + 1 >= y + 1 = s(0)(+(1)(y)) problem: strict: weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) Shift Processor lab=left (dd): strict: +(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) +(0(),s(x139)) -> s(+(0(),x139)) +(0(),s(x139)) -> s(x139) s(+(0(),x139)) -> s(x139) +(s(x),s(x141)) -> s(+(s(x),x141)) +(s(x),s(x141)) -> s(+(x,s(x141))) s(+(s(x),x141)) -> s(s(+(x,x141))) s(+(x,s(x141))) -> s(s(+(x,x141))) +(x,s(x143)) -> s(+(x,x143)) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) +(s(x143),x) -> s(+(x143,x)) inc(+(x,s(x145))) -> inc(s(+(x,x145))) inc(+(x,s(x145))) -> +(inc(x),s(x145)) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) +(0(),0()) -> 0() +(0(),0()) -> 0() +(0(),s(y)) -> s(y) +(0(),s(y)) -> s(+(0(),y)) s(+(0(),y)) -> s(y) +(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) +(s(x150),0()) -> s(+(x150,0())) +(s(x150),0()) -> s(x150) s(+(x150,0())) -> s(x150) +(s(x152),s(y)) -> s(+(x152,s(y))) +(s(x152),s(y)) -> s(+(s(x152),y)) s(+(x152,s(y))) -> s(s(+(x152,y))) s(+(s(x152),y)) -> s(s(+(x152,y))) +(s(x154),y) -> s(+(x154,y)) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) +(y,s(x154)) -> s(+(y,x154)) inc(+(s(x156),y)) -> inc(s(+(x156,y))) inc(+(s(x156),y)) -> +(inc(s(x156)),y) inc(s(+(x156,y))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> s(s(+(x156,y))) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) inc(s(+(y,x156))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(+(x,y)) -> s(+(x,y)) inc(+(x,y)) -> +(inc(x),y) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> x +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(0(),y) -> y +(y,0()) -> y +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) 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: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(0(),y) -> y +(s(x),y) -> 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) = 4x0, [s](x0) = x0, [+](x0, x1) = 2x0 + 2x1, [0] = 1 orientation: +(0(),0()) = 4 >= 1 = 0() +(0(),0()) = 4 >= 1 = 0() +(s(x),0()) = 2x + 2 >= x = s(x) +(s(x),0()) = 2x + 2 >= 2x + 2 = s(+(x,0())) s(+(x,0())) = 2x + 2 >= x = s(x) +(x,0()) = 2x + 2 >= x = x +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(0(),x) = 2x + 2 >= x = x inc(+(x,0())) = 8x + 8 >= 4x = inc(x) inc(+(x,0())) = 8x + 8 >= 8x + 2 = +(inc(x),0()) +(inc(x),0()) = 8x + 2 >= 4x = inc(x) +(0(),s(x139)) = 2x139 + 2 >= 2x139 + 2 = s(+(0(),x139)) +(0(),s(x139)) = 2x139 + 2 >= x139 = s(x139) s(+(0(),x139)) = 2x139 + 2 >= x139 = s(x139) +(s(x),s(x141)) = 2x + 2x141 >= 2x + 2x141 = s(+(s(x),x141)) +(s(x),s(x141)) = 2x + 2x141 >= 2x + 2x141 = s(+(x,s(x141))) s(+(s(x),x141)) = 2x + 2x141 >= 2x + 2x141 = s(s(+(x,x141))) s(+(x,s(x141))) = 2x + 2x141 >= 2x + 2x141 = s(s(+(x,x141))) +(x,s(x143)) = 2x + 2x143 >= 2x + 2x143 = s(+(x,x143)) +(x,s(x143)) = 2x + 2x143 >= 2x + 2x143 = +(s(x143),x) s(+(x,x143)) = 2x + 2x143 >= 2x + 2x143 = s(+(x143,x)) +(s(x143),x) = 2x + 2x143 >= 2x + 2x143 = s(+(x143,x)) inc(+(x,s(x145))) = 8x + 8x145 >= 8x + 8x145 = inc(s(+(x,x145))) inc(+(x,s(x145))) = 8x + 8x145 >= 8x + 2x145 = +(inc(x),s(x145)) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 8x + 2x145 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 8x + 2x145 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 8x + 8x145 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 8x + 2x145 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 8x + 8x145 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 >= 8x + 8x145 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 >= 2x + 2x145 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 >= 2x + 2x145 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 >= 2x + 2x145 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 >= 2x + 2x145 = s(s(+(x,x145))) +(0(),0()) = 4 >= 1 = 0() +(0(),0()) = 4 >= 1 = 0() +(0(),s(y)) = 2y + 2 >= y = s(y) +(0(),s(y)) = 2y + 2 >= 2y + 2 = s(+(0(),y)) s(+(0(),y)) = 2y + 2 >= y = s(y) +(0(),y) = 2y + 2 >= y = y +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) +(y,0()) = 2y + 2 >= y = y inc(+(0(),y)) = 8y + 8 >= 4y = inc(y) inc(+(0(),y)) = 8y + 8 >= 2y + 8 = +(inc(0()),y) inc(y) = 4y >= y = s(y) +(inc(0()),y) = 2y + 8 >= 2y + 2 = +(s(0()),y) +(s(0()),y) = 2y + 2 >= 2y + 2 = s(+(0(),y)) s(+(0(),y)) = 2y + 2 >= y = s(y) +(s(x150),0()) = 2x150 + 2 >= 2x150 + 2 = s(+(x150,0())) +(s(x150),0()) = 2x150 + 2 >= x150 = s(x150) s(+(x150,0())) = 2x150 + 2 >= x150 = s(x150) +(s(x152),s(y)) = 2x152 + 2y >= 2x152 + 2y = s(+(x152,s(y))) +(s(x152),s(y)) = 2x152 + 2y >= 2x152 + 2y = s(+(s(x152),y)) s(+(x152,s(y))) = 2x152 + 2y >= 2x152 + 2y = s(s(+(x152,y))) s(+(s(x152),y)) = 2x152 + 2y >= 2x152 + 2y = s(s(+(x152,y))) +(s(x154),y) = 2x154 + 2y >= 2x154 + 2y = s(+(x154,y)) +(s(x154),y) = 2x154 + 2y >= 2x154 + 2y = +(y,s(x154)) s(+(x154,y)) = 2x154 + 2y >= 2x154 + 2y = s(+(y,x154)) +(y,s(x154)) = 2x154 + 2y >= 2x154 + 2y = s(+(y,x154)) inc(+(s(x156),y)) = 8x156 + 8y >= 8x156 + 8y = inc(s(+(x156,y))) inc(+(s(x156),y)) = 8x156 + 8y >= 8x156 + 2y = +(inc(s(x156)),y) inc(s(+(x156,y))) = 8x156 + 8y >= 2x156 + 2y = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y >= 2x156 + 2y = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y >= 2x156 + 2y = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y >= 2x156 + 2y = s(s(+(x156,y))) inc(s(+(x156,y))) = 8x156 + 8y >= 2x156 + 2y = s(s(+(x156,y))) s(s(+(x156,y))) = 2x156 + 2y >= 2x156 + 2y = s(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y >= 2x156 + 2y = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y >= 2x156 + 2y = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y >= 2x156 + 2y = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y >= 2x156 + 2y = s(s(+(x156,y))) inc(s(+(x156,y))) = 8x156 + 8y >= 8x156 + 8y = inc(s(+(y,x156))) inc(s(+(y,x156))) = 8x156 + 8y >= 2x156 + 2y = s(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y >= 2x156 + 2y = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y >= 2x156 + 2y = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y >= 2x156 + 2y = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y >= 2x156 + 2y = s(s(+(x156,y))) inc(+(x,y)) = 8x + 8y >= 2x + 2y = s(+(x,y)) inc(+(x,y)) = 8x + 8y >= 8x + 2y = +(inc(x),y) +(inc(x),y) = 8x + 2y >= 2x + 2y = +(s(x),y) +(s(x),y) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(x,0()) = 2x + 2 >= x = x +(0(),x) = 2x + 2 >= x = x +(x,s(y)) = 2x + 2y >= 2x + 2y = +(s(y),x) +(x,s(y)) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(s(y),x) = 2x + 2y >= 2x + 2y = s(+(y,x)) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) +(0(),y) = 2y + 2 >= y = y +(y,0()) = 2y + 2 >= y = y +(s(x),y) = 2x + 2y >= 2x + 2y = +(y,s(x)) +(s(x),y) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(y,s(x)) = 2x + 2y >= 2x + 2y = s(+(y,x)) s(+(x,y)) = 2x + 2y >= 2x + 2y = s(+(y,x)) inc(+(x,y)) = 8x + 8y >= 8x + 8y = inc(+(y,x)) inc(+(x,y)) = 8x + 8y >= 8x + 2y = +(inc(x),y) inc(+(y,x)) = 8x + 8y >= 2x + 2y = s(+(y,x)) s(+(y,x)) = 2x + 2y >= 2x + 2y = s(+(x,y)) +(inc(x),y) = 8x + 2y >= 2x + 2y = +(s(x),y) +(s(x),y) = 2x + 2y >= 2x + 2y = s(+(x,y)) inc(+(y,x)) = 8x + 8y >= 8x + 8y = inc(+(x,y)) inc(+(x,y)) = 8x + 8y >= 2x + 2y = s(+(x,y)) +(inc(x),y) = 8x + 2y >= 2x + 2y = +(s(x),y) +(s(x),y) = 2x + 2y >= 2x + 2y = s(+(x,y)) inc(+(y,x)) = 8x + 8y >= 8x + 8y = inc(+(x,y)) inc(+(x,y)) = 8x + 8y >= 8x + 2y = +(inc(x),y) inc(+(x169,x170)) = 8x169 + 8x170 >= 8x169 + 2x170 = +(inc(x169),x170) inc(+(x169,x170)) = 8x169 + 8x170 >= 2x169 + 2x170 = s(+(x169,x170)) +(inc(x169),x170) = 8x169 + 2x170 >= 2x169 + 2x170 = +(s(x169),x170) +(s(x169),x170) = 2x169 + 2x170 >= 2x169 + 2x170 = s(+(x169,x170)) inc(x) = 4x >= x = s(x) +(x,y) = 2x + 2y >= 2x + 2y = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(x,0()) -> +(0(),x) +(0(),s(x139)) -> s(+(0(),x139)) +(s(x),s(x141)) -> s(+(s(x),x141)) +(s(x),s(x141)) -> s(+(x,s(x141))) s(+(s(x),x141)) -> s(s(+(x,x141))) s(+(x,s(x141))) -> s(s(+(x,x141))) +(x,s(x143)) -> s(+(x,x143)) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) +(s(x143),x) -> s(+(x143,x)) inc(+(x,s(x145))) -> inc(s(+(x,x145))) inc(+(x,s(x145))) -> +(inc(x),s(x145)) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) inc(s(+(x145,x))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) inc(+(0(),y)) -> +(inc(0()),y) inc(y) -> s(y) +(s(0()),y) -> s(+(0(),y)) +(s(x150),0()) -> s(+(x150,0())) +(s(x152),s(y)) -> s(+(x152,s(y))) +(s(x152),s(y)) -> s(+(s(x152),y)) s(+(x152,s(y))) -> s(s(+(x152,y))) s(+(s(x152),y)) -> s(s(+(x152,y))) +(s(x154),y) -> s(+(x154,y)) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) +(y,s(x154)) -> s(+(y,x154)) inc(+(s(x156),y)) -> inc(s(+(x156,y))) inc(+(s(x156),y)) -> +(inc(s(x156)),y) inc(s(+(x156,y))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> s(s(+(x156,y))) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) inc(s(+(y,x156))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(+(x,y)) -> s(+(x,y)) inc(+(x,y)) -> +(inc(x),y) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) 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: +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> 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) = 4x0, [s](x0) = x0, [+](x0, x1) = 2x0 + 2x1 + 2, [0] = 0 orientation: +(s(x),0()) = 2x + 2 >= 2x + 2 = s(+(x,0())) +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(0(),s(x139)) = 2x139 + 2 >= 2x139 + 2 = s(+(0(),x139)) +(s(x),s(x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(+(s(x),x141)) +(s(x),s(x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(+(x,s(x141))) s(+(s(x),x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(s(+(x,x141))) s(+(x,s(x141))) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(s(+(x,x141))) +(x,s(x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x,x143)) +(x,s(x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = +(s(x143),x) s(+(x,x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x143,x)) +(s(x143),x) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x143,x)) inc(+(x,s(x145))) = 8x + 8x145 + 8 >= 8x + 8x145 + 8 = inc(s(+(x,x145))) inc(+(x,s(x145))) = 8x + 8x145 + 8 >= 8x + 2x145 + 2 = +(inc(x),s(x145)) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 8x + 2x145 + 2 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 8x + 2x145 + 2 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 8x + 8x145 + 8 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 8x + 2x145 + 2 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 8x + 8x145 + 8 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 8x + 8x145 + 8 >= 8x + 8x145 + 8 = inc(s(+(x145,x))) inc(s(+(x145,x))) = 8x + 8x145 + 8 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 8x + 2x145 + 2 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(0(),s(y)) = 2y + 2 >= 2y + 2 = s(+(0(),y)) +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) inc(+(0(),y)) = 8y + 8 >= 2y + 2 = +(inc(0()),y) inc(y) = 4y >= y = s(y) +(s(0()),y) = 2y + 2 >= 2y + 2 = s(+(0(),y)) +(s(x150),0()) = 2x150 + 2 >= 2x150 + 2 = s(+(x150,0())) +(s(x152),s(y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(+(x152,s(y))) +(s(x152),s(y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(+(s(x152),y)) s(+(x152,s(y))) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(s(+(x152,y))) s(+(s(x152),y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(s(+(x152,y))) +(s(x154),y) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(x154,y)) +(s(x154),y) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = +(y,s(x154)) s(+(x154,y)) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(y,x154)) +(y,s(x154)) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(y,x154)) inc(+(s(x156),y)) = 8x156 + 8y + 8 >= 8x156 + 8y + 8 = inc(s(+(x156,y))) inc(+(s(x156),y)) = 8x156 + 8y + 8 >= 8x156 + 2y + 2 = +(inc(s(x156)),y) inc(s(+(x156,y))) = 8x156 + 8y + 8 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y + 2 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) inc(s(+(x156,y))) = 8x156 + 8y + 8 >= 2x156 + 2y + 2 = s(s(+(x156,y))) s(s(+(x156,y))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y + 2 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) inc(s(+(x156,y))) = 8x156 + 8y + 8 >= 8x156 + 8y + 8 = inc(s(+(y,x156))) inc(s(+(y,x156))) = 8x156 + 8y + 8 >= 2x156 + 2y + 2 = s(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(s(x156)),y) = 8x156 + 2y + 2 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) inc(+(x,y)) = 8x + 8y + 8 >= 2x + 2y + 2 = s(+(x,y)) inc(+(x,y)) = 8x + 8y + 8 >= 8x + 2y + 2 = +(inc(x),y) +(inc(x),y) = 8x + 2y + 2 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(s(y),x) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(s(y),x) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,s(x)) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) inc(+(x,y)) = 8x + 8y + 8 >= 8x + 8y + 8 = inc(+(y,x)) inc(+(x,y)) = 8x + 8y + 8 >= 8x + 2y + 2 = +(inc(x),y) inc(+(y,x)) = 8x + 8y + 8 >= 2x + 2y + 2 = s(+(y,x)) s(+(y,x)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(inc(x),y) = 8x + 2y + 2 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) inc(+(y,x)) = 8x + 8y + 8 >= 8x + 8y + 8 = inc(+(x,y)) inc(+(x,y)) = 8x + 8y + 8 >= 2x + 2y + 2 = s(+(x,y)) +(inc(x),y) = 8x + 2y + 2 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) inc(+(y,x)) = 8x + 8y + 8 >= 8x + 8y + 8 = inc(+(x,y)) inc(+(x,y)) = 8x + 8y + 8 >= 8x + 2y + 2 = +(inc(x),y) inc(+(x169,x170)) = 8x169 + 8x170 + 8 >= 8x169 + 2x170 + 2 = +(inc(x169),x170) inc(+(x169,x170)) = 8x169 + 8x170 + 8 >= 2x169 + 2x170 + 2 = s(+(x169,x170)) +(inc(x169),x170) = 8x169 + 2x170 + 2 >= 2x169 + 2x170 + 2 = +(s(x169),x170) +(s(x169),x170) = 2x169 + 2x170 + 2 >= 2x169 + 2x170 + 2 = s(+(x169,x170)) inc(x) = 4x >= x = s(x) +(x,y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(x,0()) -> +(0(),x) +(0(),s(x139)) -> s(+(0(),x139)) +(s(x),s(x141)) -> s(+(s(x),x141)) +(s(x),s(x141)) -> s(+(x,s(x141))) s(+(s(x),x141)) -> s(s(+(x,x141))) s(+(x,s(x141))) -> s(s(+(x,x141))) +(x,s(x143)) -> s(+(x,x143)) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) +(s(x143),x) -> s(+(x143,x)) inc(+(x,s(x145))) -> inc(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) inc(y) -> s(y) +(s(0()),y) -> s(+(0(),y)) +(s(x150),0()) -> s(+(x150,0())) +(s(x152),s(y)) -> s(+(x152,s(y))) +(s(x152),s(y)) -> s(+(s(x152),y)) s(+(x152,s(y))) -> s(s(+(x152,y))) s(+(s(x152),y)) -> s(s(+(x152,y))) +(s(x154),y) -> s(+(x154,y)) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) +(y,s(x154)) -> s(+(y,x154)) inc(+(s(x156),y)) -> inc(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) inc(+(x,y)) -> inc(+(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) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) +(inc(x169),x170) -> +(s(x169),x170) +(s(x169),x170) -> s(+(x169,x170)) weak: +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=2 interpretation: [1 1] [0] [inc](x0) = [0 1]x0 + [1], [1 0] [s](x0) = [0 0]x0, [2 0] [2 0] [1] [+](x0, x1) = [0 2]x0 + [0 2]x1 + [1], [0] [0] = [1] orientation: [2 0] [1] [2 0] [1] +(s(x),0()) = [0 0]x + [3] >= [0 0]x + [0] = s(+(x,0())) [2 0] [1] [2 0] [1] +(x,0()) = [0 2]x + [3] >= [0 2]x + [3] = +(0(),x) [2 0] [1] [2 0] [1] +(0(),s(x139)) = [0 0]x139 + [3] >= [0 0]x139 + [0] = s(+(0(),x139)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x141)) = [0 0]x + [0 0]x141 + [1] >= [0 0]x + [0 0]x141 + [0] = s(+(s(x),x141)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x141)) = [0 0]x + [0 0]x141 + [1] >= [0 0]x + [0 0]x141 + [0] = s(+(x,s(x141))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x141)) = [0 0]x + [0 0]x141 + [0] >= [0 0]x + [0 0]x141 + [0] = s(s(+(x,x141))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,s(x141))) = [0 0]x + [0 0]x141 + [0] >= [0 0]x + [0 0]x141 + [0] = s(s(+(x,x141))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(x,s(x143)) = [0 2]x + [0 0]x143 + [1] >= [0 0]x + [0 0]x143 + [0] = s(+(x,x143)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(x,s(x143)) = [0 2]x + [0 0]x143 + [1] >= [0 2]x + [0 0]x143 + [1] = +(s(x143),x) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,x143)) = [0 0]x + [0 0]x143 + [0] >= [0 0]x + [0 0]x143 + [0] = s(+(x143,x)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x143),x) = [0 2]x + [0 0]x143 + [1] >= [0 0]x + [0 0]x143 + [0] = s(+(x143,x)) [2 2] [2 0] [2] [2 0] [2 0] [1] inc(+(x,s(x145))) = [0 2]x + [0 0]x145 + [2] >= [0 0]x + [0 0]x145 + [1] = inc(s(+(x,x145))) [2 2] [2 0] [1] [2 2] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [0] = s(+(inc(x),x145)) [2 2] [2 0] [1] [2 0] [2 0] [1] s(+(inc(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(x,s(x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,s(x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x,x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 2] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [0] = s(+(inc(x),x145)) [2 2] [2 0] [1] [2 0] [2 0] [1] s(+(inc(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x,x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x,x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(x,s(x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,s(x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] inc(s(+(x,x145))) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [1] = inc(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 2] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [0] = s(+(inc(x),x145)) [2 2] [2 0] [1] [2 0] [2 0] [1] s(+(inc(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] inc(s(+(x,x145))) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [1] = inc(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(s(x),x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x),x145)) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] inc(s(+(x,x145))) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [1] = inc(s(+(x145,x))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x145,x))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),s(x145)) = [0 2]x + [0 0]x145 + [3] >= [0 0]x + [0 0]x145 + [1] = +(s(x),s(x145)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),s(x145)) = [0 0]x + [0 0]x145 + [1] >= [0 0]x + [0 0]x145 + [0] = s(+(x,s(x145))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,s(x145))) = [0 0]x + [0 0]x145 + [0] >= [0 0]x + [0 0]x145 + [0] = s(s(+(x,x145))) [2 0] [1] [2 0] [1] +(0(),s(y)) = [0 0]y + [3] >= [0 0]y + [0] = s(+(0(),y)) [2 0] [1] [2 0] [1] +(0(),y) = [0 2]y + [3] >= [0 2]y + [3] = +(y,0()) [1 1] [0] [1 0] inc(y) = [0 1]y + [1] >= [0 0]y = s(y) [2 0] [1] [2 0] [1] +(s(0()),y) = [0 2]y + [1] >= [0 0]y + [0] = s(+(0(),y)) [2 0] [1] [2 0] [1] +(s(x150),0()) = [0 0]x150 + [3] >= [0 0]x150 + [0] = s(+(x150,0())) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x152),s(y)) = [0 0]x152 + [0 0]y + [1] >= [0 0]x152 + [0 0]y + [0] = s(+(x152,s(y))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x152),s(y)) = [0 0]x152 + [0 0]y + [1] >= [0 0]x152 + [0 0]y + [0] = s(+(s(x152),y)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x152,s(y))) = [0 0]x152 + [0 0]y + [0] >= [0 0]x152 + [0 0]y + [0] = s(s(+(x152,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x152),y)) = [0 0]x152 + [0 0]y + [0] >= [0 0]x152 + [0 0]y + [0] = s(s(+(x152,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x154),y) = [0 0]x154 + [0 2]y + [1] >= [0 0]x154 + [0 0]y + [0] = s(+(x154,y)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x154),y) = [0 0]x154 + [0 2]y + [1] >= [0 0]x154 + [0 2]y + [1] = +(y,s(x154)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x154,y)) = [0 0]x154 + [0 0]y + [0] >= [0 0]x154 + [0 0]y + [0] = s(+(y,x154)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(y,s(x154)) = [0 0]x154 + [0 2]y + [1] >= [0 0]x154 + [0 0]y + [0] = s(+(y,x154)) [2 0] [2 2] [2] [2 0] [2 0] [1] inc(+(s(x156),y)) = [0 0]x156 + [0 2]y + [2] >= [0 0]x156 + [0 0]y + [1] = inc(s(+(x156,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(inc(s(x156)),y) = [0 0]x156 + [0 2]y + [3] >= [0 0]x156 + [0 2]y + [1] = +(s(s(x156)),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(s(x156)),y) = [0 0]x156 + [0 2]y + [1] >= [0 0]x156 + [0 0]y + [0] = s(+(s(x156),y)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x156),y)) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(x156,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(x156,y))) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(y,x156))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(y,x156))) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(x156,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(inc(s(x156)),y) = [0 0]x156 + [0 2]y + [3] >= [0 0]x156 + [0 2]y + [1] = +(s(s(x156)),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(s(x156)),y) = [0 0]x156 + [0 2]y + [1] >= [0 0]x156 + [0 0]y + [0] = s(+(s(x156),y)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x156),y)) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(x156,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] inc(s(+(x156,y))) = [0 0]x156 + [0 0]y + [1] >= [0 0]x156 + [0 0]y + [1] = inc(s(+(y,x156))) [2 0] [2 0] [1] [2 0] [2 0] [1] s(s(+(y,x156))) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(x156,y))) [2 0] [2 0] [1] [2 0] [2 0] [1] +(inc(s(x156)),y) = [0 0]x156 + [0 2]y + [3] >= [0 0]x156 + [0 2]y + [1] = +(s(s(x156)),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(s(x156)),y) = [0 0]x156 + [0 2]y + [1] >= [0 0]x156 + [0 0]y + [0] = s(+(s(x156),y)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(s(x156),y)) = [0 0]x156 + [0 0]y + [0] >= [0 0]x156 + [0 0]y + [0] = s(s(+(x156,y))) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),y) = [0 2]x + [0 2]y + [3] >= [0 0]x + [0 2]y + [1] = +(s(x),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),y) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 0] [1] [2 0] [1] +(x,0()) = [0 2]x + [3] >= [0 2]x + [3] = +(0(),x) [2 0] [2 0] [1] [2 0] [2 0] [1] +(x,s(y)) = [0 2]x + [0 0]y + [1] >= [0 2]x + [0 0]y + [1] = +(s(y),x) [2 0] [2 0] [1] [2 0] [2 0] [1] +(x,s(y)) = [0 2]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(y),x) = [0 2]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(y,x)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,y)) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = s(+(y,x)) [2 0] [1] [2 0] [1] +(0(),y) = [0 2]y + [3] >= [0 2]y + [3] = +(y,0()) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),y) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 2]y + [1] = +(y,s(x)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),y) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 0] [2 0] [1] [2 0] [2 0] [1] +(y,s(x)) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(y,x)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(x,y)) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = s(+(y,x)) [2 2] [2 2] [2] [2 2] [2 2] [2] inc(+(x,y)) = [0 2]x + [0 2]y + [2] >= [0 2]x + [0 2]y + [2] = inc(+(y,x)) [2 0] [2 0] [1] [2 0] [2 0] [1] s(+(y,x)) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),y) = [0 2]x + [0 2]y + [3] >= [0 0]x + [0 2]y + [1] = +(s(x),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),y) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 2] [2 2] [2] [2 2] [2 2] [2] inc(+(y,x)) = [0 2]x + [0 2]y + [2] >= [0 2]x + [0 2]y + [2] = inc(+(x,y)) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x),y) = [0 2]x + [0 2]y + [3] >= [0 0]x + [0 2]y + [1] = +(s(x),y) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x),y) = [0 0]x + [0 2]y + [1] >= [0 0]x + [0 0]y + [0] = s(+(x,y)) [2 2] [2 2] [2] [2 2] [2 2] [2] inc(+(y,x)) = [0 2]x + [0 2]y + [2] >= [0 2]x + [0 2]y + [2] = inc(+(x,y)) [2 2] [2 0] [1] [2 0] [2 0] [1] +(inc(x169),x170) = [0 2]x169 + [0 2]x170 + [3] >= [0 0]x169 + [0 2]x170 + [1] = +(s(x169),x170) [2 0] [2 0] [1] [2 0] [2 0] [1] +(s(x169),x170) = [0 0]x169 + [0 2]x170 + [1] >= [0 0]x169 + [0 0]x170 + [0] = s(+(x169,x170)) [1 1] [0] [1 0] inc(x) = [0 1]x + [1] >= [0 0]x = s(x) [2 0] [2 0] [1] [2 0] [2 0] [1] +(x,y) = [0 2]x + [0 2]y + [1] >= [0 2]x + [0 2]y + [1] = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(x,0()) -> +(0(),x) +(0(),s(x139)) -> s(+(0(),x139)) +(s(x),s(x141)) -> s(+(s(x),x141)) +(s(x),s(x141)) -> s(+(x,s(x141))) s(+(s(x),x141)) -> s(s(+(x,x141))) s(+(x,s(x141))) -> s(s(+(x,x141))) +(x,s(x143)) -> s(+(x,x143)) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) +(s(x143),x) -> s(+(x143,x)) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(inc(x),x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> +(s(x),s(x145)) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) inc(y) -> s(y) +(s(0()),y) -> s(+(0(),y)) +(s(x150),0()) -> s(+(x150,0())) +(s(x152),s(y)) -> s(+(x152,s(y))) +(s(x152),s(y)) -> s(+(s(x152),y)) s(+(x152,s(y))) -> s(s(+(x152,y))) s(+(s(x152),y)) -> s(s(+(x152,y))) +(s(x154),y) -> s(+(x154,y)) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) +(y,s(x154)) -> s(+(y,x154)) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(inc(s(x156)),y) -> +(s(s(x156)),y) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) +(inc(x),y) -> +(s(x),y) +(s(x),y) -> s(+(x,y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) inc(+(x,y)) -> inc(+(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) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) +(inc(x169),x170) -> +(s(x169),x170) +(s(x169),x170) -> s(+(x169,x170)) weak: +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) inc(x) -> s(x) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [inc](x0) = x0 + 6, [s](x0) = x0, [+](x0, x1) = 2x0 + 2x1 + 2, [0] = 0 orientation: +(s(x),0()) = 2x + 2 >= 2x + 2 = s(+(x,0())) +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(0(),s(x139)) = 2x139 + 2 >= 2x139 + 2 = s(+(0(),x139)) +(s(x),s(x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(+(s(x),x141)) +(s(x),s(x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(+(x,s(x141))) s(+(s(x),x141)) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(s(+(x,x141))) s(+(x,s(x141))) = 2x + 2x141 + 2 >= 2x + 2x141 + 2 = s(s(+(x,x141))) +(x,s(x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x,x143)) +(x,s(x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = +(s(x143),x) s(+(x,x143)) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x143,x)) +(s(x143),x) = 2x + 2x143 + 2 >= 2x + 2x143 + 2 = s(+(x143,x)) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 14 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 14 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 2x + 2x145 + 8 >= 2x + 2x145 + 8 = inc(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 14 = s(+(inc(x),x145)) s(+(inc(x),x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 2x + 2x145 + 8 >= 2x + 2x145 + 8 = inc(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(s(x),x145)) s(+(s(x),x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 2x + 2x145 + 8 >= 2x + 2x145 + 8 = inc(s(+(x145,x))) s(s(+(x145,x))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 2x + 2x145 + 14 >= 2x + 2x145 + 2 = +(s(x),s(x145)) +(s(x),s(x145)) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(+(x,s(x145))) s(+(x,s(x145))) = 2x + 2x145 + 2 >= 2x + 2x145 + 2 = s(s(+(x,x145))) +(0(),s(y)) = 2y + 2 >= 2y + 2 = s(+(0(),y)) +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) inc(y) = y + 6 >= y = s(y) +(s(0()),y) = 2y + 2 >= 2y + 2 = s(+(0(),y)) +(s(x150),0()) = 2x150 + 2 >= 2x150 + 2 = s(+(x150,0())) +(s(x152),s(y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(+(x152,s(y))) +(s(x152),s(y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(+(s(x152),y)) s(+(x152,s(y))) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(s(+(x152,y))) s(+(s(x152),y)) = 2x152 + 2y + 2 >= 2x152 + 2y + 2 = s(s(+(x152,y))) +(s(x154),y) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(x154,y)) +(s(x154),y) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = +(y,s(x154)) s(+(x154,y)) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(y,x154)) +(y,s(x154)) = 2x154 + 2y + 2 >= 2x154 + 2y + 2 = s(+(y,x154)) +(inc(s(x156)),y) = 2x156 + 2y + 14 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) s(s(+(x156,y))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(s(x156)),y) = 2x156 + 2y + 14 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) inc(s(+(x156,y))) = 2x156 + 2y + 8 >= 2x156 + 2y + 8 = inc(s(+(y,x156))) s(s(+(y,x156))) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(s(x156)),y) = 2x156 + 2y + 14 >= 2x156 + 2y + 2 = +(s(s(x156)),y) +(s(s(x156)),y) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(+(s(x156),y)) s(+(s(x156),y)) = 2x156 + 2y + 2 >= 2x156 + 2y + 2 = s(s(+(x156,y))) +(inc(x),y) = 2x + 2y + 14 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(x,0()) = 2x + 2 >= 2x + 2 = +(0(),x) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(s(y),x) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(s(y),x) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) +(0(),y) = 2y + 2 >= 2y + 2 = +(y,0()) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,s(x)) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x)) inc(+(x,y)) = 2x + 2y + 8 >= 2x + 2y + 8 = inc(+(y,x)) s(+(y,x)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) +(inc(x),y) = 2x + 2y + 14 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) inc(+(y,x)) = 2x + 2y + 8 >= 2x + 2y + 8 = inc(+(x,y)) +(inc(x),y) = 2x + 2y + 14 >= 2x + 2y + 2 = +(s(x),y) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(x,y)) inc(+(y,x)) = 2x + 2y + 8 >= 2x + 2y + 8 = inc(+(x,y)) +(inc(x169),x170) = 2x169 + 2x170 + 14 >= 2x169 + 2x170 + 2 = +(s(x169),x170) +(s(x169),x170) = 2x169 + 2x170 + 2 >= 2x169 + 2x170 + 2 = s(+(x169,x170)) inc(x) = x + 6 >= x = s(x) +(x,y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,x) problem: strict: +(s(x),0()) -> s(+(x,0())) +(x,0()) -> +(0(),x) +(0(),s(x139)) -> s(+(0(),x139)) +(s(x),s(x141)) -> s(+(s(x),x141)) +(s(x),s(x141)) -> s(+(x,s(x141))) s(+(s(x),x141)) -> s(s(+(x,x141))) s(+(x,s(x141))) -> s(s(+(x,x141))) +(x,s(x143)) -> s(+(x,x143)) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) +(s(x143),x) -> s(+(x143,x)) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(inc(x),s(x145)) -> s(+(inc(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(s(x),x145)) s(+(s(x),x145)) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(s(x),s(x145)) -> s(+(x,s(x145))) s(+(x,s(x145))) -> s(s(+(x,x145))) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) +(s(0()),y) -> s(+(0(),y)) +(s(x150),0()) -> s(+(x150,0())) +(s(x152),s(y)) -> s(+(x152,s(y))) +(s(x152),s(y)) -> s(+(s(x152),y)) s(+(x152,s(y))) -> s(s(+(x152,y))) s(+(s(x152),y)) -> s(s(+(x152,y))) +(s(x154),y) -> s(+(x154,y)) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) +(y,s(x154)) -> s(+(y,x154)) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(s(s(x156)),y) -> s(+(s(x156),y)) s(+(s(x156),y)) -> s(s(+(x156,y))) +(s(x),y) -> s(+(x,y)) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(y,x)) s(+(x,y)) -> s(+(y,x)) inc(+(x,y)) -> inc(+(y,x)) s(+(y,x)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) +(s(x),y) -> s(+(x,y)) inc(+(y,x)) -> inc(+(x,y)) +(s(x169),x170) -> s(+(x169,x170)) weak: +(x,s(y)) -> s(+(x,y)) +(s(x),y) -> s(+(x,y)) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [inc](x0) = x0, [s](x0) = x0 + 1, [+](x0, x1) = 4x0 + 4x1, [0] = 0 orientation: +(s(x),0()) = 4x + 4 >= 4x + 1 = s(+(x,0())) +(x,0()) = 4x >= 4x = +(0(),x) +(0(),s(x139)) = 4x139 + 4 >= 4x139 + 1 = s(+(0(),x139)) +(s(x),s(x141)) = 4x + 4x141 + 8 >= 4x + 4x141 + 5 = s(+(s(x),x141)) +(s(x),s(x141)) = 4x + 4x141 + 8 >= 4x + 4x141 + 5 = s(+(x,s(x141))) s(+(s(x),x141)) = 4x + 4x141 + 5 >= 4x + 4x141 + 2 = s(s(+(x,x141))) s(+(x,s(x141))) = 4x + 4x141 + 5 >= 4x + 4x141 + 2 = s(s(+(x,x141))) +(x,s(x143)) = 4x + 4x143 + 4 >= 4x + 4x143 + 1 = s(+(x,x143)) +(x,s(x143)) = 4x + 4x143 + 4 >= 4x + 4x143 + 4 = +(s(x143),x) s(+(x,x143)) = 4x + 4x143 + 1 >= 4x + 4x143 + 1 = s(+(x143,x)) +(s(x143),x) = 4x + 4x143 + 4 >= 4x + 4x143 + 1 = s(+(x143,x)) +(inc(x),s(x145)) = 4x + 4x145 + 4 >= 4x + 4x145 + 1 = s(+(inc(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(s(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(x,s(x145))) s(+(x,s(x145))) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 4x + 4x145 + 4 >= 4x + 4x145 + 1 = s(+(inc(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(s(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) s(s(+(x,x145))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(x,s(x145))) s(+(x,s(x145))) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 4x + 4x145 + 1 >= 4x + 4x145 + 1 = inc(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(inc(x),s(x145)) = 4x + 4x145 + 4 >= 4x + 4x145 + 1 = s(+(inc(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 4x + 4x145 + 1 >= 4x + 4x145 + 1 = inc(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(s(x),x145)) s(+(s(x),x145)) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) inc(s(+(x,x145))) = 4x + 4x145 + 1 >= 4x + 4x145 + 1 = inc(s(+(x145,x))) s(s(+(x145,x))) = 4x + 4x145 + 2 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(s(x),s(x145)) = 4x + 4x145 + 8 >= 4x + 4x145 + 5 = s(+(x,s(x145))) s(+(x,s(x145))) = 4x + 4x145 + 5 >= 4x + 4x145 + 2 = s(s(+(x,x145))) +(0(),s(y)) = 4y + 4 >= 4y + 1 = s(+(0(),y)) +(0(),y) = 4y >= 4y = +(y,0()) +(s(0()),y) = 4y + 4 >= 4y + 1 = s(+(0(),y)) +(s(x150),0()) = 4x150 + 4 >= 4x150 + 1 = s(+(x150,0())) +(s(x152),s(y)) = 4x152 + 4y + 8 >= 4x152 + 4y + 5 = s(+(x152,s(y))) +(s(x152),s(y)) = 4x152 + 4y + 8 >= 4x152 + 4y + 5 = s(+(s(x152),y)) s(+(x152,s(y))) = 4x152 + 4y + 5 >= 4x152 + 4y + 2 = s(s(+(x152,y))) s(+(s(x152),y)) = 4x152 + 4y + 5 >= 4x152 + 4y + 2 = s(s(+(x152,y))) +(s(x154),y) = 4x154 + 4y + 4 >= 4x154 + 4y + 1 = s(+(x154,y)) +(s(x154),y) = 4x154 + 4y + 4 >= 4x154 + 4y + 4 = +(y,s(x154)) s(+(x154,y)) = 4x154 + 4y + 1 >= 4x154 + 4y + 1 = s(+(y,x154)) +(y,s(x154)) = 4x154 + 4y + 4 >= 4x154 + 4y + 1 = s(+(y,x154)) +(s(s(x156)),y) = 4x156 + 4y + 8 >= 4x156 + 4y + 5 = s(+(s(x156),y)) s(+(s(x156),y)) = 4x156 + 4y + 5 >= 4x156 + 4y + 2 = s(s(+(x156,y))) s(s(+(x156,y))) = 4x156 + 4y + 2 >= 4x156 + 4y + 2 = s(s(+(y,x156))) s(s(+(y,x156))) = 4x156 + 4y + 2 >= 4x156 + 4y + 2 = s(s(+(x156,y))) +(s(s(x156)),y) = 4x156 + 4y + 8 >= 4x156 + 4y + 5 = s(+(s(x156),y)) s(+(s(x156),y)) = 4x156 + 4y + 5 >= 4x156 + 4y + 2 = s(s(+(x156,y))) inc(s(+(x156,y))) = 4x156 + 4y + 1 >= 4x156 + 4y + 1 = inc(s(+(y,x156))) s(s(+(y,x156))) = 4x156 + 4y + 2 >= 4x156 + 4y + 2 = s(s(+(x156,y))) +(s(s(x156)),y) = 4x156 + 4y + 8 >= 4x156 + 4y + 5 = s(+(s(x156),y)) s(+(s(x156),y)) = 4x156 + 4y + 5 >= 4x156 + 4y + 2 = s(s(+(x156,y))) +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y)) +(x,0()) = 4x >= 4x = +(0(),x) +(x,s(y)) = 4x + 4y + 4 >= 4x + 4y + 4 = +(s(y),x) +(x,s(y)) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y)) +(s(y),x) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(y,x)) s(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = s(+(y,x)) +(0(),y) = 4y >= 4y = +(y,0()) +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 4 = +(y,s(x)) +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y)) +(y,s(x)) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(y,x)) s(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = s(+(y,x)) inc(+(x,y)) = 4x + 4y >= 4x + 4y = inc(+(y,x)) s(+(y,x)) = 4x + 4y + 1 >= 4x + 4y + 1 = s(+(x,y)) +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y)) inc(+(y,x)) = 4x + 4y >= 4x + 4y = inc(+(x,y)) +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y)) inc(+(y,x)) = 4x + 4y >= 4x + 4y = inc(+(x,y)) +(s(x169),x170) = 4x169 + 4x170 + 4 >= 4x169 + 4x170 + 1 = s(+(x169,x170)) +(x,y) = 4x + 4y >= 4x + 4y = +(y,x) problem: strict: +(x,0()) -> +(0(),x) +(x,s(x143)) -> +(s(x143),x) s(+(x,x143)) -> s(+(x143,x)) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) s(s(+(x,x145))) -> s(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) inc(s(+(x,x145))) -> inc(s(+(x145,x))) s(s(+(x145,x))) -> s(s(+(x,x145))) +(0(),y) -> +(y,0()) +(s(x154),y) -> +(y,s(x154)) s(+(x154,y)) -> s(+(y,x154)) s(s(+(x156,y))) -> s(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) inc(s(+(x156,y))) -> inc(s(+(y,x156))) s(s(+(y,x156))) -> s(s(+(x156,y))) +(x,0()) -> +(0(),x) +(x,s(y)) -> +(s(y),x) s(+(x,y)) -> s(+(y,x)) +(0(),y) -> +(y,0()) +(s(x),y) -> +(y,s(x)) s(+(x,y)) -> s(+(y,x)) 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()) -2|[1,0,0]-> 0() joins: peak: s(x) <-0|[1,0,0]- +(s(x),0()) -3|[1,0,0]-> s(+(x,0())) joins: s(+(x,0())) -0|0[0,0,0]-> s(x) peak: x <-0|[1,0,0]- +(x,0()) -5|[1,0,0]-> +(0(),x) joins: +(0(),x) -2|[1,0,0]-> x peak: inc(x) <-0|0[1,0,0]- inc(+(x,0())) -6|[1,0,0]-> +(inc(x),0()) joins: +(inc(x),0()) -0|[0,0,0]-> inc(x) peak: s(+(0(),x139)) <-1|[1,0,0]- +(0(),s(x139)) -2|[1,0,0]-> s(x139) joins: s(+(0(),x139)) -2|0[0,0,0]-> s(x139) peak: s(+(s(x),x141)) <-1|[1,0,0]- +(s(x),s(x141)) -3|[1,0,0]-> s(+(x,s(x141))) joins: s(+(s(x),x141)) -3|0[0,0,0]-> s(s(+(x,x141))) s(+(x,s(x141))) -1|0[0,0,0]-> s(s(+(x,x141))) peak: s(+(x,x143)) <-1|[1,0,0]- +(x,s(x143)) -5|[1,0,0]-> +(s(x143),x) joins: s(+(x,x143)) -5|0[0,0,0]-> s(+(x143,x)) +(s(x143),x) -3|[1,0,0]-> s(+(x143,x)) peak: inc(s(+(x,x145))) <-1|0[1,0,0]- inc(+(x,s(x145))) -6|[1,0,0]-> +(inc(x),s(x145)) joins: inc(s(+(x,x145))) -4|[0,0,0]-> s(s(+(x,x145))) +(inc(x),s(x145)) -1|[0,0,0]-> s(+(inc(x),x145)) -4|0,0[0,1,1]-> s(+(s(x),x145)) -3|0[0,0,0]-> s(s(+(x,x145))) peak: 0() <-2|[1,0,0]- +(0(),0()) -0|[1,0,0]-> 0() joins: peak: s(y) <-2|[1,0,0]- +(0(),s(y)) -1|[1,0,0]-> s(+(0(),y)) joins: s(+(0(),y)) -2|0[0,0,0]-> s(y) peak: y <-2|[1,0,0]- +(0(),y) -5|[1,0,0]-> +(y,0()) joins: +(y,0()) -0|[1,0,0]-> y peak: inc(y) <-2|0[1,0,0]- inc(+(0(),y)) -6|[1,0,0]-> +(inc(0()),y) joins: inc(y) -4|[0,0,0]-> s(y) +(inc(0()),y) -4|0[0,1,1]-> +(s(0()),y) -3|[0,0,0]-> s(+(0(),y)) -2|0[0,0,0]-> s(y) peak: s(+(x150,0())) <-3|[1,0,0]- +(s(x150),0()) -0|[1,0,0]-> s(x150) joins: s(+(x150,0())) -0|0[0,0,0]-> s(x150) peak: s(+(x152,s(y))) <-3|[1,0,0]- +(s(x152),s(y)) -1|[1,0,0]-> s(+(s(x152),y)) joins: s(+(x152,s(y))) -1|0[0,0,0]-> s(s(+(x152,y))) s(+(s(x152),y)) -3|0[0,0,0]-> s(s(+(x152,y))) peak: s(+(x154,y)) <-3|[1,0,0]- +(s(x154),y) -5|[1,0,0]-> +(y,s(x154)) joins: s(+(x154,y)) -5|0[0,0,0]-> s(+(y,x154)) +(y,s(x154)) -1|[1,0,0]-> s(+(y,x154)) peak: inc(s(+(x156,y))) <-3|0[1,0,0]- inc(+(s(x156),y)) -6|[1,0,0]-> +(inc(s(x156)),y) joins: inc(s(+(x156,y))) -4|[0,0,0]-> s(s(+(x156,y))) +(inc(s(x156)),y) -4|0[0,1,1]-> +(s(s(x156)),y) -3|[0,0,0]-> s(+(s(x156),y)) -3|0[0,0,0]-> s(s(+(x156,y))) peak: s(+(x,y)) <-4|[1,0,0]- inc(+(x,y)) -6|[1,0,0]-> +(inc(x),y) joins: +(inc(x),y) -4|0[0,1,1]-> +(s(x),y) -3|[0,0,0]-> s(+(x,y)) peak: +(0(),x) <-5|[1,0,0]- +(x,0()) -0|[1,0,0]-> x joins: +(0(),x) -2|[1,0,0]-> x peak: +(s(y),x) <-5|[1,0,0]- +(x,s(y)) -1|[1,0,0]-> s(+(x,y)) joins: +(s(y),x) -3|[1,0,0]-> s(+(y,x)) s(+(x,y)) -5|0[0,0,0]-> s(+(y,x)) peak: +(y,0()) <-5|[1,0,0]- +(0(),y) -2|[1,0,0]-> y joins: +(y,0()) -0|[1,0,0]-> y peak: +(y,s(x)) <-5|[1,0,0]- +(s(x),y) -3|[1,0,0]-> s(+(x,y)) joins: +(y,s(x)) -1|[1,0,0]-> s(+(y,x)) s(+(x,y)) -5|0[0,0,0]-> s(+(y,x)) peak: inc(+(y,x)) <-5|0[1,0,0]- inc(+(x,y)) -6|[1,0,0]-> +(inc(x),y) joins: inc(+(y,x)) -4|[1,0,0]-> s(+(y,x)) -5|0[0,0,0]-> s(+(x,y)) +(inc(x),y) -4|0[0,1,1]-> +(s(x),y) -3|[0,0,0]-> s(+(x,y)) peak: +(inc(x169),x170) <-6|[1,0,0]- inc(+(x169,x170)) -4|[1,0,0]-> s(+(x169,x170)) joins: +(inc(x169),x170) -4|0[0,1,1]-> +(s(x169),x170) -3|[0,0,0]-> s(+(x169,x170)) Qed