Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) *(x,0()) -> 0() *(x,s(y)) -> +(*(x,y),x) +(x,y) -> +(y,x) Proof: Commute Transformation Processor: +(x,0()) -> x +(0(),x) -> x +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) *(x,0()) -> 0() *(x,s(y)) -> +(*(x,y),x) +(x,y) -> +(y,x) Church Rosser Transformation Processor (star): strict: *(0)(x) -> +(0)(*(0)(x)) *(0)(x) -> +(1)(x) weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) *(1)(s(0)(y)) -> +(0)(*(1)(y)) +(0)(s(0)(y)) -> s(0)(+(1)(y)) +(1)(x) -> s(0)(+(0)(x)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) +(1)(x) -> x +(0)(x) -> x critical peaks: 16 0() <-0|[]- +(0(),0()) -1|[]-> 0() s(y) <-0|[]- +(s(y),0()) -3|[]-> s(+(0(),y)) x <-0|[]- +(x,0()) -6|[]-> +(0(),x) 0() <-1|[]- +(0(),0()) -0|[]-> 0() s(y) <-1|[]- +(0(),s(y)) -2|[]-> s(+(0(),y)) y <-1|[]- +(0(),y) -6|[]-> +(y,0()) s(+(0(),x152)) <-2|[]- +(0(),s(x152)) -1|[]-> s(x152) s(+(s(y),x154)) <-2|[]- +(s(y),s(x154)) -3|[]-> s(+(s(x154),y)) s(+(x,x156)) <-2|[]- +(x,s(x156)) -6|[]-> +(s(x156),x) s(+(0(),x157)) <-3|[]- +(s(x157),0()) -0|[]-> s(x157) s(+(s(y),x159)) <-3|[]- +(s(x159),s(y)) -2|[]-> s(+(s(x159),y)) s(+(y,x161)) <-3|[]- +(s(x161),y) -6|[]-> +(y,s(x161)) +(0(),x) <-6|[]- +(x,0()) -0|[]-> x +(x,0()) <-6|[]- +(0(),x) -1|[]-> x +(s(y),x) <-6|[]- +(x,s(y)) -2|[]-> s(+(x,y)) +(x,s(y)) <-6|[]- +(s(y),x) -3|[]-> s(+(x,y)) Matrix Interpretation Processor: dim=1, lab=right interpretation: [s(0)](x0) = x0, [*(1)](x0) = x0 + 2, [*(0)](x0) = 2x0 + 1, [+(1)](x0) = x0, [+(0)](x0) = x0 orientation: *(0)(x) = 2x + 1 >= 2x + 1 = +(0)(*(0)(x)) *(0)(x) = 2x + 1 >= x = +(1)(x) +(0)(x) = x >= x = +(1)(x) +(1)(y) = y >= y = +(0)(y) *(1)(s(0)(y)) = y + 2 >= y + 2 = +(0)(*(1)(y)) +(0)(s(0)(y)) = y >= y = s(0)(+(1)(y)) +(1)(x) = x >= x = s(0)(+(0)(x)) +(0)(x) = x >= x = s(0)(+(0)(x)) +(1)(s(0)(y)) = y >= y = s(0)(+(1)(y)) +(1)(x) = x >= x = x +(0)(x) = x >= x = x problem: strict: *(0)(x) -> +(0)(*(0)(x)) weak: +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) *(1)(s(0)(y)) -> +(0)(*(1)(y)) +(0)(s(0)(y)) -> s(0)(+(1)(y)) +(1)(x) -> s(0)(+(0)(x)) +(0)(x) -> s(0)(+(0)(x)) +(1)(s(0)(y)) -> s(0)(+(1)(y)) +(1)(x) -> x +(0)(x) -> x Shift Processor (**) lab=left: strict: weak: Shift Processor lab=left (dd): strict: +(0(),0()) -> 0() +(0(),0()) -> 0() +(s(y),0()) -> s(y) +(s(y),0()) -> s(+(0(),y)) s(+(0(),y)) -> s(y) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x +(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 +(0(),s(x152)) -> s(+(0(),x152)) +(0(),s(x152)) -> s(x152) s(+(0(),x152)) -> s(x152) +(s(y),s(x154)) -> s(+(s(y),x154)) +(s(y),s(x154)) -> s(+(s(x154),y)) s(+(s(y),x154)) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(+(x154,s(y))) s(+(x154,s(y))) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(+(y,s(x154))) s(+(y,s(x154))) -> s(s(+(y,x154))) +(x,s(x156)) -> s(+(x,x156)) +(x,s(x156)) -> +(s(x156),x) +(s(x156),x) -> s(+(x,x156)) +(s(x157),0()) -> s(+(0(),x157)) +(s(x157),0()) -> s(x157) s(+(0(),x157)) -> s(x157) +(s(x159),s(y)) -> s(+(s(y),x159)) +(s(x159),s(y)) -> s(+(s(x159),y)) s(+(s(y),x159)) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(+(x159,s(y))) s(+(x159,s(y))) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(+(y,s(x159))) s(+(y,s(x159))) -> s(s(+(y,x159))) +(s(x161),y) -> s(+(y,x161)) +(s(x161),y) -> +(y,s(x161)) +(y,s(x161)) -> s(+(y,x161)) +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> x +(0(),x) -> +(x,0()) +(0(),x) -> x +(x,0()) -> x +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) +(s(y),x) -> +(x,s(y)) +(s(y),x) -> s(+(x,y)) +(x,s(y)) -> s(+(x,y)) weak: +(x,0()) -> x +(0(),x) -> x +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) *(x,0()) -> 0() *(x,s(y)) -> +(*(x,y),x) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [*](x0, x1) = 2x0 + x1 + x1x0, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [0] = 0 orientation: +(0(),0()) = 1 >= 0 = 0() +(0(),0()) = 1 >= 0 = 0() +(s(y),0()) = y + 2 >= y + 1 = s(y) +(s(y),0()) = y + 2 >= y + 2 = s(+(0(),y)) s(+(0(),y)) = y + 2 >= y + 1 = s(y) +(x,0()) = x + 1 >= x = x +(x,0()) = x + 1 >= x + 1 = +(0(),x) +(0(),x) = x + 1 >= x = x +(0(),0()) = 1 >= 0 = 0() +(0(),0()) = 1 >= 0 = 0() +(0(),s(y)) = y + 2 >= y + 1 = s(y) +(0(),s(y)) = y + 2 >= y + 2 = s(+(0(),y)) s(+(0(),y)) = y + 2 >= y + 1 = s(y) +(0(),y) = y + 1 >= y = y +(0(),y) = y + 1 >= y + 1 = +(y,0()) +(y,0()) = y + 1 >= y = y +(0(),s(x152)) = x152 + 2 >= x152 + 2 = s(+(0(),x152)) +(0(),s(x152)) = x152 + 2 >= x152 + 1 = s(x152) s(+(0(),x152)) = x152 + 2 >= x152 + 1 = s(x152) +(s(y),s(x154)) = x154 + y + 3 >= x154 + y + 3 = s(+(s(y),x154)) +(s(y),s(x154)) = x154 + y + 3 >= x154 + y + 3 = s(+(s(x154),y)) s(+(s(y),x154)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(+(s(x154),y)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) s(s(+(y,x154))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(+(s(y),x154)) = x154 + y + 3 >= x154 + y + 3 = s(+(x154,s(y))) s(+(x154,s(y))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(+(s(x154),y)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) s(s(+(y,x154))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(+(s(y),x154)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(s(+(x154,y))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) s(+(s(x154),y)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) s(+(s(y),x154)) = x154 + y + 3 >= x154 + y + 3 = s(s(+(x154,y))) s(s(+(x154,y))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) s(+(s(x154),y)) = x154 + y + 3 >= x154 + y + 3 = s(+(y,s(x154))) s(+(y,s(x154))) = x154 + y + 3 >= x154 + y + 3 = s(s(+(y,x154))) +(x,s(x156)) = x + x156 + 2 >= x + x156 + 2 = s(+(x,x156)) +(x,s(x156)) = x + x156 + 2 >= x + x156 + 2 = +(s(x156),x) +(s(x156),x) = x + x156 + 2 >= x + x156 + 2 = s(+(x,x156)) +(s(x157),0()) = x157 + 2 >= x157 + 2 = s(+(0(),x157)) +(s(x157),0()) = x157 + 2 >= x157 + 1 = s(x157) s(+(0(),x157)) = x157 + 2 >= x157 + 1 = s(x157) +(s(x159),s(y)) = x159 + y + 3 >= x159 + y + 3 = s(+(s(y),x159)) +(s(x159),s(y)) = x159 + y + 3 >= x159 + y + 3 = s(+(s(x159),y)) s(+(s(y),x159)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(+(s(x159),y)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) s(s(+(y,x159))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(+(s(y),x159)) = x159 + y + 3 >= x159 + y + 3 = s(+(x159,s(y))) s(+(x159,s(y))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(+(s(x159),y)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) s(s(+(y,x159))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(+(s(y),x159)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(s(+(x159,y))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) s(+(s(x159),y)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) s(+(s(y),x159)) = x159 + y + 3 >= x159 + y + 3 = s(s(+(x159,y))) s(s(+(x159,y))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) s(+(s(x159),y)) = x159 + y + 3 >= x159 + y + 3 = s(+(y,s(x159))) s(+(y,s(x159))) = x159 + y + 3 >= x159 + y + 3 = s(s(+(y,x159))) +(s(x161),y) = x161 + y + 2 >= x161 + y + 2 = s(+(y,x161)) +(s(x161),y) = x161 + y + 2 >= x161 + y + 2 = +(y,s(x161)) +(y,s(x161)) = x161 + y + 2 >= x161 + y + 2 = s(+(y,x161)) +(x,0()) = x + 1 >= x + 1 = +(0(),x) +(x,0()) = x + 1 >= x = x +(0(),x) = x + 1 >= x = x +(0(),x) = x + 1 >= x + 1 = +(x,0()) +(0(),x) = x + 1 >= x = x +(x,0()) = x + 1 >= x = x +(x,s(y)) = x + y + 2 >= x + y + 2 = +(s(y),x) +(x,s(y)) = x + y + 2 >= x + y + 2 = s(+(x,y)) +(s(y),x) = x + y + 2 >= x + y + 2 = s(+(x,y)) +(s(y),x) = x + y + 2 >= x + y + 2 = +(x,s(y)) +(s(y),x) = x + y + 2 >= x + y + 2 = s(+(x,y)) +(x,s(y)) = x + y + 2 >= x + y + 2 = s(+(x,y)) *(x,0()) = 2x >= 0 = 0() *(x,s(y)) = 3x + x*y + y + 1 >= 3x + x*y + y + 1 = +(*(x,y),x) +(x,y) = x + y + 1 >= x + y + 1 = +(y,x) problem: strict: +(s(y),0()) -> s(+(0(),y)) +(x,0()) -> +(0(),x) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) +(0(),s(x152)) -> s(+(0(),x152)) +(s(y),s(x154)) -> s(+(s(y),x154)) +(s(y),s(x154)) -> s(+(s(x154),y)) s(+(s(y),x154)) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(+(x154,s(y))) s(+(x154,s(y))) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(+(y,s(x154))) s(+(y,s(x154))) -> s(s(+(y,x154))) +(x,s(x156)) -> s(+(x,x156)) +(x,s(x156)) -> +(s(x156),x) +(s(x156),x) -> s(+(x,x156)) +(s(x157),0()) -> s(+(0(),x157)) +(s(x159),s(y)) -> s(+(s(y),x159)) +(s(x159),s(y)) -> s(+(s(x159),y)) s(+(s(y),x159)) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(+(x159,s(y))) s(+(x159,s(y))) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(+(y,s(x159))) s(+(y,s(x159))) -> s(s(+(y,x159))) +(s(x161),y) -> s(+(y,x161)) +(s(x161),y) -> +(y,s(x161)) +(y,s(x161)) -> s(+(y,x161)) +(x,0()) -> +(0(),x) +(0(),x) -> +(x,0()) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) +(s(y),x) -> +(x,s(y)) +(s(y),x) -> s(+(x,y)) +(x,s(y)) -> s(+(x,y)) weak: +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) *(x,0()) -> 0() *(x,s(y)) -> +(*(x,y),x) +(x,y) -> +(y,x) Polynomial Interpretation Processor: dimension: 1 interpretation: [*](x0, x1) = 2x0 + 2x1 + 2x1x0 + 1, [s](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [0] = 0 orientation: +(s(y),0()) = y + 1 >= y + 1 = s(+(0(),y)) +(x,0()) = x >= x = +(0(),x) +(0(),s(y)) = y + 1 >= y + 1 = s(+(0(),y)) +(0(),y) = y >= y = +(y,0()) +(0(),s(x152)) = x152 + 1 >= x152 + 1 = s(+(0(),x152)) +(s(y),s(x154)) = x154 + y + 2 >= x154 + y + 2 = s(+(s(y),x154)) +(s(y),s(x154)) = x154 + y + 2 >= x154 + y + 2 = s(+(s(x154),y)) s(+(s(y),x154)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(+(s(x154),y)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) s(s(+(y,x154))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(+(s(y),x154)) = x154 + y + 2 >= x154 + y + 2 = s(+(x154,s(y))) s(+(x154,s(y))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(+(s(x154),y)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) s(s(+(y,x154))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(+(s(y),x154)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(s(+(x154,y))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) s(+(s(x154),y)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) s(+(s(y),x154)) = x154 + y + 2 >= x154 + y + 2 = s(s(+(x154,y))) s(s(+(x154,y))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) s(+(s(x154),y)) = x154 + y + 2 >= x154 + y + 2 = s(+(y,s(x154))) s(+(y,s(x154))) = x154 + y + 2 >= x154 + y + 2 = s(s(+(y,x154))) +(x,s(x156)) = x + x156 + 1 >= x + x156 + 1 = s(+(x,x156)) +(x,s(x156)) = x + x156 + 1 >= x + x156 + 1 = +(s(x156),x) +(s(x156),x) = x + x156 + 1 >= x + x156 + 1 = s(+(x,x156)) +(s(x157),0()) = x157 + 1 >= x157 + 1 = s(+(0(),x157)) +(s(x159),s(y)) = x159 + y + 2 >= x159 + y + 2 = s(+(s(y),x159)) +(s(x159),s(y)) = x159 + y + 2 >= x159 + y + 2 = s(+(s(x159),y)) s(+(s(y),x159)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(+(s(x159),y)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) s(s(+(y,x159))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(+(s(y),x159)) = x159 + y + 2 >= x159 + y + 2 = s(+(x159,s(y))) s(+(x159,s(y))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(+(s(x159),y)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) s(s(+(y,x159))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(+(s(y),x159)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(s(+(x159,y))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) s(+(s(x159),y)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) s(+(s(y),x159)) = x159 + y + 2 >= x159 + y + 2 = s(s(+(x159,y))) s(s(+(x159,y))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) s(+(s(x159),y)) = x159 + y + 2 >= x159 + y + 2 = s(+(y,s(x159))) s(+(y,s(x159))) = x159 + y + 2 >= x159 + y + 2 = s(s(+(y,x159))) +(s(x161),y) = x161 + y + 1 >= x161 + y + 1 = s(+(y,x161)) +(s(x161),y) = x161 + y + 1 >= x161 + y + 1 = +(y,s(x161)) +(y,s(x161)) = x161 + y + 1 >= x161 + y + 1 = s(+(y,x161)) +(x,0()) = x >= x = +(0(),x) +(0(),x) = x >= x = +(x,0()) +(x,s(y)) = x + y + 1 >= x + y + 1 = +(s(y),x) +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(s(y),x) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(s(y),x) = x + y + 1 >= x + y + 1 = +(x,s(y)) +(s(y),x) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y)) *(x,0()) = 2x + 1 >= 0 = 0() *(x,s(y)) = 4x + 2x*y + 2y + 3 >= 3x + 2x*y + 2y + 1 = +(*(x,y),x) +(x,y) = x + y >= x + y = +(y,x) problem: strict: +(s(y),0()) -> s(+(0(),y)) +(x,0()) -> +(0(),x) +(0(),s(y)) -> s(+(0(),y)) +(0(),y) -> +(y,0()) +(0(),s(x152)) -> s(+(0(),x152)) +(s(y),s(x154)) -> s(+(s(y),x154)) +(s(y),s(x154)) -> s(+(s(x154),y)) s(+(s(y),x154)) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(+(x154,s(y))) s(+(x154,s(y))) -> s(s(+(x154,y))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(s(+(y,x154))) s(+(s(y),x154)) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(+(y,s(x154))) s(+(y,s(x154))) -> s(s(+(y,x154))) +(x,s(x156)) -> s(+(x,x156)) +(x,s(x156)) -> +(s(x156),x) +(s(x156),x) -> s(+(x,x156)) +(s(x157),0()) -> s(+(0(),x157)) +(s(x159),s(y)) -> s(+(s(y),x159)) +(s(x159),s(y)) -> s(+(s(x159),y)) s(+(s(y),x159)) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(+(x159,s(y))) s(+(x159,s(y))) -> s(s(+(x159,y))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(s(+(y,x159))) s(+(s(y),x159)) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(+(y,s(x159))) s(+(y,s(x159))) -> s(s(+(y,x159))) +(s(x161),y) -> s(+(y,x161)) +(s(x161),y) -> +(y,s(x161)) +(y,s(x161)) -> s(+(y,x161)) +(x,0()) -> +(0(),x) +(0(),x) -> +(x,0()) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) +(s(y),x) -> +(x,s(y)) +(s(y),x) -> s(+(x,y)) +(x,s(y)) -> s(+(x,y)) weak: +(x,s(y)) -> s(+(x,y)) +(s(y),x) -> s(+(x,y)) +(x,y) -> +(y,x) Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0 + 1, [+](x0, x1) = 3x0 + 3x1 + 1, [0] = 2 orientation: +(s(y),0()) = 3y + 10 >= 3y + 8 = s(+(0(),y)) +(x,0()) = 3x + 7 >= 3x + 7 = +(0(),x) +(0(),s(y)) = 3y + 10 >= 3y + 8 = s(+(0(),y)) +(0(),y) = 3y + 7 >= 3y + 7 = +(y,0()) +(0(),s(x152)) = 3x152 + 10 >= 3x152 + 8 = s(+(0(),x152)) +(s(y),s(x154)) = 3x154 + 3y + 7 >= 3x154 + 3y + 5 = s(+(s(y),x154)) +(s(y),s(x154)) = 3x154 + 3y + 7 >= 3x154 + 3y + 5 = s(+(s(x154),y)) s(+(s(y),x154)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(+(s(x154),y)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(y,x154))) s(s(+(y,x154))) = 3x154 + 3y + 3 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(+(s(y),x154)) = 3x154 + 3y + 5 >= 3x154 + 3y + 5 = s(+(x154,s(y))) s(+(x154,s(y))) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(+(s(x154),y)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(y,x154))) s(s(+(y,x154))) = 3x154 + 3y + 3 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(+(s(y),x154)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(s(+(x154,y))) = 3x154 + 3y + 3 >= 3x154 + 3y + 3 = s(s(+(y,x154))) s(+(s(x154),y)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(y,x154))) s(+(s(y),x154)) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(x154,y))) s(s(+(x154,y))) = 3x154 + 3y + 3 >= 3x154 + 3y + 3 = s(s(+(y,x154))) s(+(s(x154),y)) = 3x154 + 3y + 5 >= 3x154 + 3y + 5 = s(+(y,s(x154))) s(+(y,s(x154))) = 3x154 + 3y + 5 >= 3x154 + 3y + 3 = s(s(+(y,x154))) +(x,s(x156)) = 3x + 3x156 + 4 >= 3x + 3x156 + 2 = s(+(x,x156)) +(x,s(x156)) = 3x + 3x156 + 4 >= 3x + 3x156 + 4 = +(s(x156),x) +(s(x156),x) = 3x + 3x156 + 4 >= 3x + 3x156 + 2 = s(+(x,x156)) +(s(x157),0()) = 3x157 + 10 >= 3x157 + 8 = s(+(0(),x157)) +(s(x159),s(y)) = 3x159 + 3y + 7 >= 3x159 + 3y + 5 = s(+(s(y),x159)) +(s(x159),s(y)) = 3x159 + 3y + 7 >= 3x159 + 3y + 5 = s(+(s(x159),y)) s(+(s(y),x159)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(+(s(x159),y)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(y,x159))) s(s(+(y,x159))) = 3x159 + 3y + 3 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(+(s(y),x159)) = 3x159 + 3y + 5 >= 3x159 + 3y + 5 = s(+(x159,s(y))) s(+(x159,s(y))) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(+(s(x159),y)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(y,x159))) s(s(+(y,x159))) = 3x159 + 3y + 3 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(+(s(y),x159)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(s(+(x159,y))) = 3x159 + 3y + 3 >= 3x159 + 3y + 3 = s(s(+(y,x159))) s(+(s(x159),y)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(y,x159))) s(+(s(y),x159)) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(x159,y))) s(s(+(x159,y))) = 3x159 + 3y + 3 >= 3x159 + 3y + 3 = s(s(+(y,x159))) s(+(s(x159),y)) = 3x159 + 3y + 5 >= 3x159 + 3y + 5 = s(+(y,s(x159))) s(+(y,s(x159))) = 3x159 + 3y + 5 >= 3x159 + 3y + 3 = s(s(+(y,x159))) +(s(x161),y) = 3x161 + 3y + 4 >= 3x161 + 3y + 2 = s(+(y,x161)) +(s(x161),y) = 3x161 + 3y + 4 >= 3x161 + 3y + 4 = +(y,s(x161)) +(y,s(x161)) = 3x161 + 3y + 4 >= 3x161 + 3y + 2 = s(+(y,x161)) +(x,0()) = 3x + 7 >= 3x + 7 = +(0(),x) +(0(),x) = 3x + 7 >= 3x + 7 = +(x,0()) +(x,s(y)) = 3x + 3y + 4 >= 3x + 3y + 4 = +(s(y),x) +(x,s(y)) = 3x + 3y + 4 >= 3x + 3y + 2 = s(+(x,y)) +(s(y),x) = 3x + 3y + 4 >= 3x + 3y + 2 = s(+(x,y)) +(s(y),x) = 3x + 3y + 4 >= 3x + 3y + 4 = +(x,s(y)) +(s(y),x) = 3x + 3y + 4 >= 3x + 3y + 2 = s(+(x,y)) +(x,s(y)) = 3x + 3y + 4 >= 3x + 3y + 2 = s(+(x,y)) +(x,y) = 3x + 3y + 1 >= 3x + 3y + 1 = +(y,x) problem: strict: +(x,0()) -> +(0(),x) +(0(),y) -> +(y,0()) s(s(+(y,x154))) -> s(s(+(x154,y))) s(+(s(y),x154)) -> s(+(x154,s(y))) s(s(+(y,x154))) -> s(s(+(x154,y))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(s(+(x154,y))) -> s(s(+(y,x154))) s(+(s(x154),y)) -> s(+(y,s(x154))) +(x,s(x156)) -> +(s(x156),x) s(s(+(y,x159))) -> s(s(+(x159,y))) s(+(s(y),x159)) -> s(+(x159,s(y))) s(s(+(y,x159))) -> s(s(+(x159,y))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(s(+(x159,y))) -> s(s(+(y,x159))) s(+(s(x159),y)) -> s(+(y,s(x159))) +(s(x161),y) -> +(y,s(x161)) +(x,0()) -> +(0(),x) +(0(),x) -> +(x,0()) +(x,s(y)) -> +(s(y),x) +(s(y),x) -> +(x,s(y)) weak: +(x,y) -> +(y,x) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: 0() <-0|[1,0]- +(0(),0()) -1|[1,0]-> 0() joins: peak: s(y) <-0|[1,0]- +(s(y),0()) -3|[1,0]-> s(+(0(),y)) joins: s(+(0(),y)) -1|0[0,0]-> s(y) peak: x <-0|[1,0]- +(x,0()) -6|[1,0]-> +(0(),x) joins: +(0(),x) -1|[1,0]-> x peak: 0() <-1|[1,0]- +(0(),0()) -0|[1,0]-> 0() joins: peak: s(y) <-1|[1,0]- +(0(),s(y)) -2|[1,0]-> s(+(0(),y)) joins: s(+(0(),y)) -1|0[0,0]-> s(y) peak: y <-1|[1,0]- +(0(),y) -6|[1,0]-> +(y,0()) joins: +(y,0()) -0|[1,0]-> y peak: s(+(0(),x152)) <-2|[1,0]- +(0(),s(x152)) -1|[1,0]-> s(x152) joins: s(+(0(),x152)) -1|0[0,0]-> s(x152) peak: s(+(s(y),x154)) <-2|[1,0]- +(s(y),s(x154)) -3|[1,0]-> s(+(s(x154),y)) joins: s(+(s(y),x154)) -3|0[0,0]-> s(s(+(x154,y))) s(+(s(x154),y)) -3|0[0,0]-> s(s(+(y,x154))) -6|0,0[0,0]-> s(s(+(x154,y))) peak: s(+(x,x156)) <-2|[1,0]- +(x,s(x156)) -6|[1,0]-> +(s(x156),x) joins: +(s(x156),x) -3|[1,0]-> s(+(x,x156)) peak: s(+(0(),x157)) <-3|[1,0]- +(s(x157),0()) -0|[1,0]-> s(x157) joins: s(+(0(),x157)) -1|0[0,0]-> s(x157) peak: s(+(s(y),x159)) <-3|[1,0]- +(s(x159),s(y)) -2|[1,0]-> s(+(s(x159),y)) joins: s(+(s(y),x159)) -3|0[0,0]-> s(s(+(x159,y))) s(+(s(x159),y)) -3|0[0,0]-> s(s(+(y,x159))) -6|0,0[0,0]-> s(s(+(x159,y))) peak: s(+(y,x161)) <-3|[1,0]- +(s(x161),y) -6|[1,0]-> +(y,s(x161)) joins: +(y,s(x161)) -2|[1,0]-> s(+(y,x161)) peak: +(0(),x) <-6|[1,0]- +(x,0()) -0|[1,0]-> x joins: +(0(),x) -1|[1,0]-> x peak: +(x,0()) <-6|[1,0]- +(0(),x) -1|[1,0]-> x joins: +(x,0()) -0|[1,0]-> x peak: +(s(y),x) <-6|[1,0]- +(x,s(y)) -2|[1,0]-> s(+(x,y)) joins: +(s(y),x) -3|[1,0]-> s(+(x,y)) peak: +(x,s(y)) <-6|[1,0]- +(s(y),x) -3|[1,0]-> s(+(x,y)) joins: +(x,s(y)) -2|[1,0]-> s(+(x,y)) Qed