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