Problem: -(x,x) -> 0() +(x,y) -> +(y,x) +(0(),x) -> x +(x,0()) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) +(p(x),y) -> p(+(x,y)) +(x,p(y)) -> p(+(y,x)) s(p(x)) -> x p(s(x)) -> x Proof: sorted: (order) 0:-(x,x) -> 0() 1:+(x,y) -> +(y,x) +(0(),x) -> x +(x,0()) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) +(p(x),y) -> p(+(x,y)) +(x,p(y)) -> p(+(y,x)) s(p(x)) -> x p(s(x)) -> x ----- sorts [1>2, 1>4, 3>4] sort attachment (non-strict) - : 2 x 2 -> 1 0 : 4 + : 3 x 3 -> 3 s : 3 -> 3 p : 3 -> 3 ----- 0:-(x,x) -> 0() Church Rosser Transformation Processor (kb): -(x,x) -> 0() critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [0] = [0] [0], [1 0 0] [1 0 0] [1] [-](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0] [0 0 0] [0 0 0] [0] orientation: [2 0 0] [1] [0] -(x,x) = [0 0 0]x + [0] >= [0] = 0() [0 0 0] [0] [0] problem: Qed 1:+(x,y) -> +(y,x) +(0(),x) -> x +(x,0()) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) +(p(x),y) -> p(+(x,y)) +(x,p(y)) -> p(+(y,x)) s(p(x)) -> x p(s(x)) -> x Church Rosser Transformation Processor (star): strict: weak: p(0)(s(0)(x)) -> x s(0)(p(0)(x)) -> x +(0)(x) -> p(0)(+(1)(x)) +(1)(p(0)(y)) -> p(0)(+(0)(y)) +(0)(p(0)(x)) -> p(0)(+(0)(x)) +(1)(y) -> p(0)(+(1)(y)) +(0)(x) -> s(0)(+(1)(x)) +(1)(s(0)(y)) -> s(0)(+(0)(y)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> x +(1)(x) -> x +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) critical peaks: 36 +(x,0()) <-0|[]- +(0(),x) -1|[]-> x +(0(),x) <-0|[]- +(x,0()) -2|[]-> x +(y,s(x)) <-0|[]- +(s(x),y) -3|[]-> s(+(x,y)) +(s(y),x) <-0|[]- +(x,s(y)) -4|[]-> s(+(y,x)) +(y,p(x)) <-0|[]- +(p(x),y) -5|[]-> p(+(x,y)) +(p(y),x) <-0|[]- +(x,p(y)) -6|[]-> p(+(y,x)) y <-1|[]- +(0(),y) -0|[]-> +(y,0()) 0() <-1|[]- +(0(),0()) -2|[]-> 0() s(y) <-1|[]- +(0(),s(y)) -4|[]-> s(+(y,0())) p(y) <-1|[]- +(0(),p(y)) -6|[]-> p(+(y,0())) x <-2|[]- +(x,0()) -0|[]-> +(0(),x) 0() <-2|[]- +(0(),0()) -1|[]-> 0() s(x) <-2|[]- +(s(x),0()) -3|[]-> s(+(x,0())) p(x) <-2|[]- +(p(x),0()) -5|[]-> p(+(x,0())) s(+(x261,y)) <-3|[]- +(s(x261),y) -0|[]-> +(y,s(x261)) s(+(x263,0())) <-3|[]- +(s(x263),0()) -2|[]-> s(x263) s(+(x265,s(y))) <-3|[]- +(s(x265),s(y)) -4|[]-> s(+(y,s(x265))) s(+(x267,p(y))) <-3|[]- +(s(x267),p(y)) -6|[]-> p(+(y,s(x267))) s(+(x270,x)) <-4|[]- +(x,s(x270)) -0|[]-> +(s(x270),x) s(+(x272,0())) <-4|[]- +(0(),s(x272)) -1|[]-> s(x272) s(+(x274,s(x))) <-4|[]- +(s(x),s(x274)) -3|[]-> s(+(x,s(x274))) s(+(x276,p(x))) <-4|[]- +(p(x),s(x276)) -5|[]-> p(+(x,s(x276))) p(+(x277,y)) <-5|[]- +(p(x277),y) -0|[]-> +(y,p(x277)) p(+(x279,0())) <-5|[]- +(p(x279),0()) -2|[]-> p(x279) p(+(x281,s(y))) <-5|[]- +(p(x281),s(y)) -4|[]-> s(+(y,p(x281))) p(+(x283,p(y))) <-5|[]- +(p(x283),p(y)) -6|[]-> p(+(y,p(x283))) p(+(x286,x)) <-6|[]- +(x,p(x286)) -0|[]-> +(p(x286),x) p(+(x288,0())) <-6|[]- +(0(),p(x288)) -1|[]-> p(x288) p(+(x290,s(x))) <-6|[]- +(s(x),p(x290)) -3|[]-> s(+(x,p(x290))) p(+(x292,p(x))) <-6|[]- +(p(x),p(x292)) -5|[]-> p(+(x,p(x292))) +(x293,y) <-7|0[]- +(s(p(x293)),y) -3|[]-> s(+(p(x293),y)) +(x,x294) <-7|1[]- +(x,s(p(x294))) -4|[]-> s(+(p(x294),x)) p(x295) <-7|0[]- p(s(p(x295))) -8|[]-> p(x295) +(x296,y) <-8|0[]- +(p(s(x296)),y) -5|[]-> p(+(s(x296),y)) +(x,x297) <-8|1[]- +(x,p(s(x297))) -6|[]-> p(+(s(x297),x)) s(x298) <-8|0[]- s(p(s(x298))) -7|[]-> s(x298) Matrix Interpretation Processor: dim=1, lab=right interpretation: [+(1)](x0) = 2x0 + 2, [+(0)](x0) = 2x0 + 2, [s(0)](x0) = x0, [p(0)](x0) = x0 orientation: p(0)(s(0)(x)) = x >= x = x s(0)(p(0)(x)) = x >= x = x +(0)(x) = 2x + 2 >= 2x + 2 = p(0)(+(1)(x)) +(1)(p(0)(y)) = 2y + 2 >= 2y + 2 = p(0)(+(0)(y)) +(0)(p(0)(x)) = 2x + 2 >= 2x + 2 = p(0)(+(0)(x)) +(1)(y) = 2y + 2 >= 2y + 2 = p(0)(+(1)(y)) +(0)(x) = 2x + 2 >= 2x + 2 = s(0)(+(1)(x)) +(1)(s(0)(y)) = 2y + 2 >= 2y + 2 = s(0)(+(0)(y)) +(0)(s(0)(x)) = 2x + 2 >= 2x + 2 = s(0)(+(0)(x)) +(1)(y) = 2y + 2 >= 2y + 2 = s(0)(+(1)(y)) +(0)(x) = 2x + 2 >= x = x +(1)(x) = 2x + 2 >= x = x +(0)(x) = 2x + 2 >= 2x + 2 = +(1)(x) +(1)(y) = 2y + 2 >= 2y + 2 = +(0)(y) problem: strict: weak: p(0)(s(0)(x)) -> x s(0)(p(0)(x)) -> x +(0)(x) -> p(0)(+(1)(x)) +(1)(p(0)(y)) -> p(0)(+(0)(y)) +(0)(p(0)(x)) -> p(0)(+(0)(x)) +(1)(y) -> p(0)(+(1)(y)) +(0)(x) -> s(0)(+(1)(x)) +(1)(s(0)(y)) -> s(0)(+(0)(y)) +(0)(s(0)(x)) -> s(0)(+(0)(x)) +(1)(y) -> s(0)(+(1)(y)) +(0)(x) -> +(1)(x) +(1)(y) -> +(0)(y) Shift Processor lab=left (dd): strict: +(0(),x) -> +(x,0()) +(0(),x) -> x +(x,0()) -> x +(x,0()) -> +(0(),x) +(x,0()) -> x +(0(),x) -> x +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(y,x)) +(s(y),x) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(x,y)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(y,x)) +(p(y),x) -> p(+(y,x)) +(0(),y) -> y +(0(),y) -> +(y,0()) +(y,0()) -> y +(0(),0()) -> 0() +(0(),0()) -> 0() +(0(),s(y)) -> s(y) +(0(),s(y)) -> s(+(y,0())) s(+(y,0())) -> s(y) +(0(),p(y)) -> p(y) +(0(),p(y)) -> p(+(y,0())) p(+(y,0())) -> p(y) +(x,0()) -> x +(x,0()) -> +(0(),x) +(0(),x) -> x +(0(),0()) -> 0() +(0(),0()) -> 0() +(s(x),0()) -> s(x) +(s(x),0()) -> s(+(x,0())) s(+(x,0())) -> s(x) +(p(x),0()) -> p(x) +(p(x),0()) -> p(+(x,0())) p(+(x,0())) -> p(x) +(s(x261),y) -> s(+(x261,y)) +(s(x261),y) -> +(y,s(x261)) +(y,s(x261)) -> s(+(x261,y)) +(s(x263),0()) -> s(+(x263,0())) +(s(x263),0()) -> s(x263) s(+(x263,0())) -> s(x263) +(s(x265),s(y)) -> s(+(x265,s(y))) +(s(x265),s(y)) -> s(+(y,s(x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(+(s(y),x265)) s(+(s(y),x265)) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(+(s(x265),y)) s(+(s(x265),y)) -> s(s(+(x265,y))) +(s(x267),p(y)) -> s(+(x267,p(y))) +(s(x267),p(y)) -> p(+(y,s(x267))) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) p(s(+(y,x267))) -> +(y,x267) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) s(+(p(y),x267)) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) p(s(+(y,x267))) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) s(+(p(y),x267)) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> s(p(+(x267,y))) s(p(+(x267,y))) -> +(x267,y) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> s(p(+(x267,y))) s(p(+(x267,y))) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x,s(x270)) -> s(+(x270,x)) +(x,s(x270)) -> +(s(x270),x) +(s(x270),x) -> s(+(x270,x)) +(0(),s(x272)) -> s(+(x272,0())) +(0(),s(x272)) -> s(x272) s(+(x272,0())) -> s(x272) +(s(x),s(x274)) -> s(+(x274,s(x))) +(s(x),s(x274)) -> s(+(x,s(x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(+(s(x),x274)) s(+(s(x),x274)) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(+(s(x274),x)) s(+(s(x274),x)) -> s(s(+(x274,x))) +(p(x),s(x276)) -> s(+(x276,p(x))) +(p(x),s(x276)) -> p(+(x,s(x276))) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) p(s(+(x,x276))) -> +(x,x276) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) s(+(p(x),x276)) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) p(s(+(x,x276))) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) s(+(p(x),x276)) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> s(p(+(x276,x))) s(p(+(x276,x))) -> +(x276,x) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> s(p(+(x276,x))) s(p(+(x276,x))) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(p(x277),y) -> p(+(x277,y)) +(p(x277),y) -> +(y,p(x277)) +(y,p(x277)) -> p(+(x277,y)) +(p(x279),0()) -> p(+(x279,0())) +(p(x279),0()) -> p(x279) p(+(x279,0())) -> p(x279) +(p(x281),s(y)) -> p(+(x281,s(y))) +(p(x281),s(y)) -> s(+(y,p(x281))) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> s(p(+(y,x281))) s(p(+(y,x281))) -> +(y,x281) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> s(p(+(y,x281))) s(p(+(y,x281))) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) p(s(+(x281,y))) -> +(x281,y) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) p(s(+(x281,y))) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) s(+(p(x281),y)) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) s(+(p(x281),y)) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(p(x283),p(y)) -> p(+(x283,p(y))) +(p(x283),p(y)) -> p(+(y,p(x283))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(+(p(y),x283)) p(+(p(y),x283)) -> p(p(+(y,x283))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(+(p(x283),y)) p(+(p(x283),y)) -> p(p(+(x283,y))) +(x,p(x286)) -> p(+(x286,x)) +(x,p(x286)) -> +(p(x286),x) +(p(x286),x) -> p(+(x286,x)) +(0(),p(x288)) -> p(+(x288,0())) +(0(),p(x288)) -> p(x288) p(+(x288,0())) -> p(x288) +(s(x),p(x290)) -> p(+(x290,s(x))) +(s(x),p(x290)) -> s(+(x,p(x290))) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> s(p(+(x,x290))) s(p(+(x,x290))) -> +(x,x290) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> s(p(+(x,x290))) s(p(+(x,x290))) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) p(s(+(x290,x))) -> +(x290,x) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) p(s(+(x290,x))) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) s(+(p(x290),x)) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) s(+(p(x290),x)) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(p(x),p(x292)) -> p(+(x292,p(x))) +(p(x),p(x292)) -> p(+(x,p(x292))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(+(p(x),x292)) p(+(p(x),x292)) -> p(p(+(x,x292))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(+(p(x292),x)) p(+(p(x292),x)) -> p(p(+(x292,x))) +(s(p(x293)),y) -> +(x293,y) +(s(p(x293)),y) -> s(+(p(x293),y)) s(+(p(x293),y)) -> s(p(+(x293,y))) s(p(+(x293,y))) -> +(x293,y) +(x,s(p(x294))) -> +(x,x294) +(x,s(p(x294))) -> s(+(p(x294),x)) +(x,x294) -> +(x294,x) s(+(p(x294),x)) -> s(p(+(x294,x))) s(p(+(x294,x))) -> +(x294,x) p(s(p(x295))) -> p(x295) p(s(p(x295))) -> p(x295) +(p(s(x296)),y) -> +(x296,y) +(p(s(x296)),y) -> p(+(s(x296),y)) p(+(s(x296),y)) -> p(s(+(x296,y))) p(s(+(x296,y))) -> +(x296,y) +(x,p(s(x297))) -> +(x,x297) +(x,p(s(x297))) -> p(+(s(x297),x)) +(x,x297) -> +(x297,x) p(+(s(x297),x)) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(p(s(x298))) -> s(x298) s(p(s(x298))) -> s(x298) weak: +(x,y) -> +(y,x) +(0(),x) -> x +(x,0()) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) +(p(x),y) -> p(+(x,y)) +(x,p(y)) -> p(+(y,x)) s(p(x)) -> x p(s(x)) -> x Matrix Interpretation Processor: dim=1 interpretation: [p](x0) = x0, [s](x0) = x0, [+](x0, x1) = x0 + x1, [0] = 5 orientation: +(0(),x) = x + 5 >= x + 5 = +(x,0()) +(0(),x) = x + 5 >= x = x +(x,0()) = x + 5 >= x = x +(x,0()) = x + 5 >= x + 5 = +(0(),x) +(x,0()) = x + 5 >= x = x +(0(),x) = x + 5 >= x = x +(s(x),y) = x + y >= x + y = +(y,s(x)) +(s(x),y) = x + y >= x + y = s(+(x,y)) +(y,s(x)) = x + y >= x + y = s(+(x,y)) +(x,s(y)) = x + y >= x + y = +(s(y),x) +(x,s(y)) = x + y >= x + y = s(+(y,x)) +(s(y),x) = x + y >= x + y = s(+(y,x)) +(p(x),y) = x + y >= x + y = +(y,p(x)) +(p(x),y) = x + y >= x + y = p(+(x,y)) +(y,p(x)) = x + y >= x + y = p(+(x,y)) +(x,p(y)) = x + y >= x + y = +(p(y),x) +(x,p(y)) = x + y >= x + y = p(+(y,x)) +(p(y),x) = x + y >= x + y = p(+(y,x)) +(0(),y) = y + 5 >= y = y +(0(),y) = y + 5 >= y + 5 = +(y,0()) +(y,0()) = y + 5 >= y = y +(0(),0()) = 10 >= 5 = 0() +(0(),0()) = 10 >= 5 = 0() +(0(),s(y)) = y + 5 >= y = s(y) +(0(),s(y)) = y + 5 >= y + 5 = s(+(y,0())) s(+(y,0())) = y + 5 >= y = s(y) +(0(),p(y)) = y + 5 >= y = p(y) +(0(),p(y)) = y + 5 >= y + 5 = p(+(y,0())) p(+(y,0())) = y + 5 >= y = p(y) +(x,0()) = x + 5 >= x = x +(x,0()) = x + 5 >= x + 5 = +(0(),x) +(0(),x) = x + 5 >= x = x +(0(),0()) = 10 >= 5 = 0() +(0(),0()) = 10 >= 5 = 0() +(s(x),0()) = x + 5 >= x = s(x) +(s(x),0()) = x + 5 >= x + 5 = s(+(x,0())) s(+(x,0())) = x + 5 >= x = s(x) +(p(x),0()) = x + 5 >= x = p(x) +(p(x),0()) = x + 5 >= x + 5 = p(+(x,0())) p(+(x,0())) = x + 5 >= x = p(x) +(s(x261),y) = x261 + y >= x261 + y = s(+(x261,y)) +(s(x261),y) = x261 + y >= x261 + y = +(y,s(x261)) +(y,s(x261)) = x261 + y >= x261 + y = s(+(x261,y)) +(s(x263),0()) = x263 + 5 >= x263 + 5 = s(+(x263,0())) +(s(x263),0()) = x263 + 5 >= x263 = s(x263) s(+(x263,0())) = x263 + 5 >= x263 = s(x263) +(s(x265),s(y)) = x265 + y >= x265 + y = s(+(x265,s(y))) +(s(x265),s(y)) = x265 + y >= x265 + y = s(+(y,s(x265))) s(+(x265,s(y))) = x265 + y >= x265 + y = s(s(+(y,x265))) s(+(y,s(x265))) = x265 + y >= x265 + y = s(s(+(x265,y))) s(s(+(x265,y))) = x265 + y >= x265 + y = s(s(+(y,x265))) s(+(x265,s(y))) = x265 + y >= x265 + y = s(+(s(y),x265)) s(+(s(y),x265)) = x265 + y >= x265 + y = s(s(+(y,x265))) s(+(y,s(x265))) = x265 + y >= x265 + y = s(s(+(x265,y))) s(s(+(x265,y))) = x265 + y >= x265 + y = s(s(+(y,x265))) s(+(x265,s(y))) = x265 + y >= x265 + y = s(s(+(y,x265))) s(s(+(y,x265))) = x265 + y >= x265 + y = s(s(+(x265,y))) s(+(y,s(x265))) = x265 + y >= x265 + y = s(s(+(x265,y))) s(+(x265,s(y))) = x265 + y >= x265 + y = s(s(+(y,x265))) s(s(+(y,x265))) = x265 + y >= x265 + y = s(s(+(x265,y))) s(+(y,s(x265))) = x265 + y >= x265 + y = s(+(s(x265),y)) s(+(s(x265),y)) = x265 + y >= x265 + y = s(s(+(x265,y))) +(s(x267),p(y)) = x267 + y >= x267 + y = s(+(x267,p(y))) +(s(x267),p(y)) = x267 + y >= x267 + y = p(+(y,s(x267))) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = p(s(+(y,x267))) p(s(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) +(x267,y) = x267 + y >= x267 + y = +(y,x267) s(+(x267,p(y))) = x267 + y >= x267 + y = s(+(p(y),x267)) s(+(p(y),x267)) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = p(s(+(y,x267))) p(s(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) s(+(x267,p(y))) = x267 + y >= x267 + y = s(+(p(y),x267)) s(+(p(y),x267)) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) +(x267,y) = x267 + y >= x267 + y = +(y,x267) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = s(p(+(x267,y))) s(p(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = s(p(+(x267,y))) s(p(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) p(+(y,s(x267))) = x267 + y >= x267 + y = p(+(s(x267),y)) p(+(s(x267),y)) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) +(y,x267) = x267 + y >= x267 + y = +(x267,y) p(+(y,s(x267))) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) s(+(x267,p(y))) = x267 + y >= x267 + y = s(p(+(y,x267))) s(p(+(y,x267))) = x267 + y >= x267 + y = +(y,x267) +(y,x267) = x267 + y >= x267 + y = +(x267,y) p(+(y,s(x267))) = x267 + y >= x267 + y = p(+(s(x267),y)) p(+(s(x267),y)) = x267 + y >= x267 + y = p(s(+(x267,y))) p(s(+(x267,y))) = x267 + y >= x267 + y = +(x267,y) +(x,s(x270)) = x + x270 >= x + x270 = s(+(x270,x)) +(x,s(x270)) = x + x270 >= x + x270 = +(s(x270),x) +(s(x270),x) = x + x270 >= x + x270 = s(+(x270,x)) +(0(),s(x272)) = x272 + 5 >= x272 + 5 = s(+(x272,0())) +(0(),s(x272)) = x272 + 5 >= x272 = s(x272) s(+(x272,0())) = x272 + 5 >= x272 = s(x272) +(s(x),s(x274)) = x + x274 >= x + x274 = s(+(x274,s(x))) +(s(x),s(x274)) = x + x274 >= x + x274 = s(+(x,s(x274))) s(+(x274,s(x))) = x + x274 >= x + x274 = s(s(+(x,x274))) s(+(x,s(x274))) = x + x274 >= x + x274 = s(s(+(x274,x))) s(s(+(x274,x))) = x + x274 >= x + x274 = s(s(+(x,x274))) s(+(x274,s(x))) = x + x274 >= x + x274 = s(+(s(x),x274)) s(+(s(x),x274)) = x + x274 >= x + x274 = s(s(+(x,x274))) s(+(x,s(x274))) = x + x274 >= x + x274 = s(s(+(x274,x))) s(s(+(x274,x))) = x + x274 >= x + x274 = s(s(+(x,x274))) s(+(x274,s(x))) = x + x274 >= x + x274 = s(s(+(x,x274))) s(s(+(x,x274))) = x + x274 >= x + x274 = s(s(+(x274,x))) s(+(x,s(x274))) = x + x274 >= x + x274 = s(s(+(x274,x))) s(+(x274,s(x))) = x + x274 >= x + x274 = s(s(+(x,x274))) s(s(+(x,x274))) = x + x274 >= x + x274 = s(s(+(x274,x))) s(+(x,s(x274))) = x + x274 >= x + x274 = s(+(s(x274),x)) s(+(s(x274),x)) = x + x274 >= x + x274 = s(s(+(x274,x))) +(p(x),s(x276)) = x + x276 >= x + x276 = s(+(x276,p(x))) +(p(x),s(x276)) = x + x276 >= x + x276 = p(+(x,s(x276))) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = p(s(+(x,x276))) p(s(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) +(x276,x) = x + x276 >= x + x276 = +(x,x276) s(+(x276,p(x))) = x + x276 >= x + x276 = s(+(p(x),x276)) s(+(p(x),x276)) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = p(s(+(x,x276))) p(s(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) s(+(x276,p(x))) = x + x276 >= x + x276 = s(+(p(x),x276)) s(+(p(x),x276)) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) +(x276,x) = x + x276 >= x + x276 = +(x,x276) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = s(p(+(x276,x))) s(p(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = s(p(+(x276,x))) s(p(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) p(+(x,s(x276))) = x + x276 >= x + x276 = p(+(s(x276),x)) p(+(s(x276),x)) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) +(x,x276) = x + x276 >= x + x276 = +(x276,x) p(+(x,s(x276))) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) s(+(x276,p(x))) = x + x276 >= x + x276 = s(p(+(x,x276))) s(p(+(x,x276))) = x + x276 >= x + x276 = +(x,x276) +(x,x276) = x + x276 >= x + x276 = +(x276,x) p(+(x,s(x276))) = x + x276 >= x + x276 = p(+(s(x276),x)) p(+(s(x276),x)) = x + x276 >= x + x276 = p(s(+(x276,x))) p(s(+(x276,x))) = x + x276 >= x + x276 = +(x276,x) +(p(x277),y) = x277 + y >= x277 + y = p(+(x277,y)) +(p(x277),y) = x277 + y >= x277 + y = +(y,p(x277)) +(y,p(x277)) = x277 + y >= x277 + y = p(+(x277,y)) +(p(x279),0()) = x279 + 5 >= x279 + 5 = p(+(x279,0())) +(p(x279),0()) = x279 + 5 >= x279 = p(x279) p(+(x279,0())) = x279 + 5 >= x279 = p(x279) +(p(x281),s(y)) = x281 + y >= x281 + y = p(+(x281,s(y))) +(p(x281),s(y)) = x281 + y >= x281 + y = s(+(y,p(x281))) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = s(p(+(y,x281))) s(p(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) +(x281,y) = x281 + y >= x281 + y = +(y,x281) p(+(x281,s(y))) = x281 + y >= x281 + y = p(+(s(y),x281)) p(+(s(y),x281)) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = s(p(+(y,x281))) s(p(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) p(+(x281,s(y))) = x281 + y >= x281 + y = p(+(s(y),x281)) p(+(s(y),x281)) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) +(x281,y) = x281 + y >= x281 + y = +(y,x281) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = p(s(+(x281,y))) p(s(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = p(s(+(x281,y))) p(s(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) s(+(y,p(x281))) = x281 + y >= x281 + y = s(+(p(x281),y)) s(+(p(x281),y)) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) +(y,x281) = x281 + y >= x281 + y = +(x281,y) s(+(y,p(x281))) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) p(+(x281,s(y))) = x281 + y >= x281 + y = p(s(+(y,x281))) p(s(+(y,x281))) = x281 + y >= x281 + y = +(y,x281) +(y,x281) = x281 + y >= x281 + y = +(x281,y) s(+(y,p(x281))) = x281 + y >= x281 + y = s(+(p(x281),y)) s(+(p(x281),y)) = x281 + y >= x281 + y = s(p(+(x281,y))) s(p(+(x281,y))) = x281 + y >= x281 + y = +(x281,y) +(p(x283),p(y)) = x283 + y >= x283 + y = p(+(x283,p(y))) +(p(x283),p(y)) = x283 + y >= x283 + y = p(+(y,p(x283))) p(+(x283,p(y))) = x283 + y >= x283 + y = p(p(+(y,x283))) p(+(y,p(x283))) = x283 + y >= x283 + y = p(p(+(x283,y))) p(p(+(x283,y))) = x283 + y >= x283 + y = p(p(+(y,x283))) p(+(x283,p(y))) = x283 + y >= x283 + y = p(+(p(y),x283)) p(+(p(y),x283)) = x283 + y >= x283 + y = p(p(+(y,x283))) p(+(y,p(x283))) = x283 + y >= x283 + y = p(p(+(x283,y))) p(p(+(x283,y))) = x283 + y >= x283 + y = p(p(+(y,x283))) p(+(x283,p(y))) = x283 + y >= x283 + y = p(p(+(y,x283))) p(p(+(y,x283))) = x283 + y >= x283 + y = p(p(+(x283,y))) p(+(y,p(x283))) = x283 + y >= x283 + y = p(p(+(x283,y))) p(+(x283,p(y))) = x283 + y >= x283 + y = p(p(+(y,x283))) p(p(+(y,x283))) = x283 + y >= x283 + y = p(p(+(x283,y))) p(+(y,p(x283))) = x283 + y >= x283 + y = p(+(p(x283),y)) p(+(p(x283),y)) = x283 + y >= x283 + y = p(p(+(x283,y))) +(x,p(x286)) = x + x286 >= x + x286 = p(+(x286,x)) +(x,p(x286)) = x + x286 >= x + x286 = +(p(x286),x) +(p(x286),x) = x + x286 >= x + x286 = p(+(x286,x)) +(0(),p(x288)) = x288 + 5 >= x288 + 5 = p(+(x288,0())) +(0(),p(x288)) = x288 + 5 >= x288 = p(x288) p(+(x288,0())) = x288 + 5 >= x288 = p(x288) +(s(x),p(x290)) = x + x290 >= x + x290 = p(+(x290,s(x))) +(s(x),p(x290)) = x + x290 >= x + x290 = s(+(x,p(x290))) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = s(p(+(x,x290))) s(p(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) +(x290,x) = x + x290 >= x + x290 = +(x,x290) p(+(x290,s(x))) = x + x290 >= x + x290 = p(+(s(x),x290)) p(+(s(x),x290)) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = s(p(+(x,x290))) s(p(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) p(+(x290,s(x))) = x + x290 >= x + x290 = p(+(s(x),x290)) p(+(s(x),x290)) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) +(x290,x) = x + x290 >= x + x290 = +(x,x290) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = p(s(+(x290,x))) p(s(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = p(s(+(x290,x))) p(s(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) s(+(x,p(x290))) = x + x290 >= x + x290 = s(+(p(x290),x)) s(+(p(x290),x)) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) +(x,x290) = x + x290 >= x + x290 = +(x290,x) s(+(x,p(x290))) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) p(+(x290,s(x))) = x + x290 >= x + x290 = p(s(+(x,x290))) p(s(+(x,x290))) = x + x290 >= x + x290 = +(x,x290) +(x,x290) = x + x290 >= x + x290 = +(x290,x) s(+(x,p(x290))) = x + x290 >= x + x290 = s(+(p(x290),x)) s(+(p(x290),x)) = x + x290 >= x + x290 = s(p(+(x290,x))) s(p(+(x290,x))) = x + x290 >= x + x290 = +(x290,x) +(p(x),p(x292)) = x + x292 >= x + x292 = p(+(x292,p(x))) +(p(x),p(x292)) = x + x292 >= x + x292 = p(+(x,p(x292))) p(+(x292,p(x))) = x + x292 >= x + x292 = p(p(+(x,x292))) p(+(x,p(x292))) = x + x292 >= x + x292 = p(p(+(x292,x))) p(p(+(x292,x))) = x + x292 >= x + x292 = p(p(+(x,x292))) p(+(x292,p(x))) = x + x292 >= x + x292 = p(+(p(x),x292)) p(+(p(x),x292)) = x + x292 >= x + x292 = p(p(+(x,x292))) p(+(x,p(x292))) = x + x292 >= x + x292 = p(p(+(x292,x))) p(p(+(x292,x))) = x + x292 >= x + x292 = p(p(+(x,x292))) p(+(x292,p(x))) = x + x292 >= x + x292 = p(p(+(x,x292))) p(p(+(x,x292))) = x + x292 >= x + x292 = p(p(+(x292,x))) p(+(x,p(x292))) = x + x292 >= x + x292 = p(p(+(x292,x))) p(+(x292,p(x))) = x + x292 >= x + x292 = p(p(+(x,x292))) p(p(+(x,x292))) = x + x292 >= x + x292 = p(p(+(x292,x))) p(+(x,p(x292))) = x + x292 >= x + x292 = p(+(p(x292),x)) p(+(p(x292),x)) = x + x292 >= x + x292 = p(p(+(x292,x))) +(s(p(x293)),y) = x293 + y >= x293 + y = +(x293,y) +(s(p(x293)),y) = x293 + y >= x293 + y = s(+(p(x293),y)) s(+(p(x293),y)) = x293 + y >= x293 + y = s(p(+(x293,y))) s(p(+(x293,y))) = x293 + y >= x293 + y = +(x293,y) +(x,s(p(x294))) = x + x294 >= x + x294 = +(x,x294) +(x,s(p(x294))) = x + x294 >= x + x294 = s(+(p(x294),x)) +(x,x294) = x + x294 >= x + x294 = +(x294,x) s(+(p(x294),x)) = x + x294 >= x + x294 = s(p(+(x294,x))) s(p(+(x294,x))) = x + x294 >= x + x294 = +(x294,x) p(s(p(x295))) = x295 >= x295 = p(x295) p(s(p(x295))) = x295 >= x295 = p(x295) +(p(s(x296)),y) = x296 + y >= x296 + y = +(x296,y) +(p(s(x296)),y) = x296 + y >= x296 + y = p(+(s(x296),y)) p(+(s(x296),y)) = x296 + y >= x296 + y = p(s(+(x296,y))) p(s(+(x296,y))) = x296 + y >= x296 + y = +(x296,y) +(x,p(s(x297))) = x + x297 >= x + x297 = +(x,x297) +(x,p(s(x297))) = x + x297 >= x + x297 = p(+(s(x297),x)) +(x,x297) = x + x297 >= x + x297 = +(x297,x) p(+(s(x297),x)) = x + x297 >= x + x297 = p(s(+(x297,x))) p(s(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) s(p(s(x298))) = x298 >= x298 = s(x298) s(p(s(x298))) = x298 >= x298 = s(x298) +(x,y) = x + y >= x + y = +(y,x) s(p(x)) = x >= x = x p(s(x)) = x >= x = x problem: strict: +(0(),x) -> +(x,0()) +(x,0()) -> +(0(),x) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(y,x)) +(s(y),x) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(p(x),y) -> p(+(x,y)) +(y,p(x)) -> p(+(x,y)) +(x,p(y)) -> +(p(y),x) +(x,p(y)) -> p(+(y,x)) +(p(y),x) -> p(+(y,x)) +(0(),y) -> +(y,0()) +(0(),s(y)) -> s(+(y,0())) +(0(),p(y)) -> p(+(y,0())) +(x,0()) -> +(0(),x) +(s(x),0()) -> s(+(x,0())) +(p(x),0()) -> p(+(x,0())) +(s(x261),y) -> s(+(x261,y)) +(s(x261),y) -> +(y,s(x261)) +(y,s(x261)) -> s(+(x261,y)) +(s(x263),0()) -> s(+(x263,0())) +(s(x265),s(y)) -> s(+(x265,s(y))) +(s(x265),s(y)) -> s(+(y,s(x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(+(s(y),x265)) s(+(s(y),x265)) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(+(s(x265),y)) s(+(s(x265),y)) -> s(s(+(x265,y))) +(s(x267),p(y)) -> s(+(x267,p(y))) +(s(x267),p(y)) -> p(+(y,s(x267))) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) p(s(+(y,x267))) -> +(y,x267) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) s(+(p(y),x267)) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) p(s(+(y,x267))) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) s(+(p(y),x267)) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> s(p(+(x267,y))) s(p(+(x267,y))) -> +(x267,y) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> s(p(+(x267,y))) s(p(+(x267,y))) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) s(+(x267,p(y))) -> s(p(+(y,x267))) s(p(+(y,x267))) -> +(y,x267) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) p(s(+(x267,y))) -> +(x267,y) +(x,s(x270)) -> s(+(x270,x)) +(x,s(x270)) -> +(s(x270),x) +(s(x270),x) -> s(+(x270,x)) +(0(),s(x272)) -> s(+(x272,0())) +(s(x),s(x274)) -> s(+(x274,s(x))) +(s(x),s(x274)) -> s(+(x,s(x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(+(s(x),x274)) s(+(s(x),x274)) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(+(s(x274),x)) s(+(s(x274),x)) -> s(s(+(x274,x))) +(p(x),s(x276)) -> s(+(x276,p(x))) +(p(x),s(x276)) -> p(+(x,s(x276))) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) p(s(+(x,x276))) -> +(x,x276) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) s(+(p(x),x276)) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) p(s(+(x,x276))) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) s(+(p(x),x276)) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> s(p(+(x276,x))) s(p(+(x276,x))) -> +(x276,x) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> s(p(+(x276,x))) s(p(+(x276,x))) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) s(+(x276,p(x))) -> s(p(+(x,x276))) s(p(+(x,x276))) -> +(x,x276) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) p(s(+(x276,x))) -> +(x276,x) +(p(x277),y) -> p(+(x277,y)) +(p(x277),y) -> +(y,p(x277)) +(y,p(x277)) -> p(+(x277,y)) +(p(x279),0()) -> p(+(x279,0())) +(p(x281),s(y)) -> p(+(x281,s(y))) +(p(x281),s(y)) -> s(+(y,p(x281))) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> s(p(+(y,x281))) s(p(+(y,x281))) -> +(y,x281) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> s(p(+(y,x281))) s(p(+(y,x281))) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) p(s(+(x281,y))) -> +(x281,y) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) p(s(+(x281,y))) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) s(+(p(x281),y)) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> +(y,x281) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) s(+(p(x281),y)) -> s(p(+(x281,y))) s(p(+(x281,y))) -> +(x281,y) +(p(x283),p(y)) -> p(+(x283,p(y))) +(p(x283),p(y)) -> p(+(y,p(x283))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(+(p(y),x283)) p(+(p(y),x283)) -> p(p(+(y,x283))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(p(+(x283,y))) p(+(x283,p(y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(+(p(x283),y)) p(+(p(x283),y)) -> p(p(+(x283,y))) +(x,p(x286)) -> p(+(x286,x)) +(x,p(x286)) -> +(p(x286),x) +(p(x286),x) -> p(+(x286,x)) +(0(),p(x288)) -> p(+(x288,0())) +(s(x),p(x290)) -> p(+(x290,s(x))) +(s(x),p(x290)) -> s(+(x,p(x290))) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> s(p(+(x,x290))) s(p(+(x,x290))) -> +(x,x290) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> s(p(+(x,x290))) s(p(+(x,x290))) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) p(s(+(x290,x))) -> +(x290,x) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) p(s(+(x290,x))) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) s(+(p(x290),x)) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> +(x,x290) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) s(+(p(x290),x)) -> s(p(+(x290,x))) s(p(+(x290,x))) -> +(x290,x) +(p(x),p(x292)) -> p(+(x292,p(x))) +(p(x),p(x292)) -> p(+(x,p(x292))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(+(p(x),x292)) p(+(p(x),x292)) -> p(p(+(x,x292))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(p(+(x292,x))) p(+(x292,p(x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(+(p(x292),x)) p(+(p(x292),x)) -> p(p(+(x292,x))) +(s(p(x293)),y) -> +(x293,y) +(s(p(x293)),y) -> s(+(p(x293),y)) s(+(p(x293),y)) -> s(p(+(x293,y))) s(p(+(x293,y))) -> +(x293,y) +(x,s(p(x294))) -> +(x,x294) +(x,s(p(x294))) -> s(+(p(x294),x)) +(x,x294) -> +(x294,x) s(+(p(x294),x)) -> s(p(+(x294,x))) s(p(+(x294,x))) -> +(x294,x) p(s(p(x295))) -> p(x295) p(s(p(x295))) -> p(x295) +(p(s(x296)),y) -> +(x296,y) +(p(s(x296)),y) -> p(+(s(x296),y)) p(+(s(x296),y)) -> p(s(+(x296,y))) p(s(+(x296,y))) -> +(x296,y) +(x,p(s(x297))) -> +(x,x297) +(x,p(s(x297))) -> p(+(s(x297),x)) +(x,x297) -> +(x297,x) p(+(s(x297),x)) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(p(s(x298))) -> s(x298) s(p(s(x298))) -> s(x298) weak: +(x,y) -> +(y,x) +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) +(p(x),y) -> p(+(x,y)) +(x,p(y)) -> p(+(y,x)) s(p(x)) -> x p(s(x)) -> x Matrix Interpretation Processor: dim=1 interpretation: [p](x0) = x0 + 1, [s](x0) = x0, [+](x0, x1) = 4x0 + 4x1 + 7, [0] = 1 orientation: +(0(),x) = 4x + 11 >= 4x + 11 = +(x,0()) +(x,0()) = 4x + 11 >= 4x + 11 = +(0(),x) +(s(x),y) = 4x + 4y + 7 >= 4x + 4y + 7 = +(y,s(x)) +(s(x),y) = 4x + 4y + 7 >= 4x + 4y + 7 = s(+(x,y)) +(y,s(x)) = 4x + 4y + 7 >= 4x + 4y + 7 = s(+(x,y)) +(x,s(y)) = 4x + 4y + 7 >= 4x + 4y + 7 = +(s(y),x) +(x,s(y)) = 4x + 4y + 7 >= 4x + 4y + 7 = s(+(y,x)) +(s(y),x) = 4x + 4y + 7 >= 4x + 4y + 7 = s(+(y,x)) +(p(x),y) = 4x + 4y + 11 >= 4x + 4y + 11 = +(y,p(x)) +(p(x),y) = 4x + 4y + 11 >= 4x + 4y + 8 = p(+(x,y)) +(y,p(x)) = 4x + 4y + 11 >= 4x + 4y + 8 = p(+(x,y)) +(x,p(y)) = 4x + 4y + 11 >= 4x + 4y + 11 = +(p(y),x) +(x,p(y)) = 4x + 4y + 11 >= 4x + 4y + 8 = p(+(y,x)) +(p(y),x) = 4x + 4y + 11 >= 4x + 4y + 8 = p(+(y,x)) +(0(),y) = 4y + 11 >= 4y + 11 = +(y,0()) +(0(),s(y)) = 4y + 11 >= 4y + 11 = s(+(y,0())) +(0(),p(y)) = 4y + 15 >= 4y + 12 = p(+(y,0())) +(x,0()) = 4x + 11 >= 4x + 11 = +(0(),x) +(s(x),0()) = 4x + 11 >= 4x + 11 = s(+(x,0())) +(p(x),0()) = 4x + 15 >= 4x + 12 = p(+(x,0())) +(s(x261),y) = 4x261 + 4y + 7 >= 4x261 + 4y + 7 = s(+(x261,y)) +(s(x261),y) = 4x261 + 4y + 7 >= 4x261 + 4y + 7 = +(y,s(x261)) +(y,s(x261)) = 4x261 + 4y + 7 >= 4x261 + 4y + 7 = s(+(x261,y)) +(s(x263),0()) = 4x263 + 11 >= 4x263 + 11 = s(+(x263,0())) +(s(x265),s(y)) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(+(x265,s(y))) +(s(x265),s(y)) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(+(y,s(x265))) s(+(x265,s(y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(+(y,s(x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) s(s(+(x265,y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(+(x265,s(y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(+(s(y),x265)) s(+(s(y),x265)) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(+(y,s(x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) s(s(+(x265,y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(+(x265,s(y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(s(+(y,x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) s(+(y,s(x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) s(+(x265,s(y))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(y,x265))) s(s(+(y,x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) s(+(y,s(x265))) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(+(s(x265),y)) s(+(s(x265),y)) = 4x265 + 4y + 7 >= 4x265 + 4y + 7 = s(s(+(x265,y))) +(s(x267),p(y)) = 4x267 + 4y + 11 >= 4x267 + 4y + 11 = s(+(x267,p(y))) +(s(x267),p(y)) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = p(+(y,s(x267))) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(y,x267))) p(s(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) +(x267,y) = 4x267 + 4y + 7 >= 4x267 + 4y + 7 = +(y,x267) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 11 = s(+(p(y),x267)) s(+(p(y),x267)) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(y,x267))) p(s(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 11 = s(+(p(y),x267)) s(+(p(y),x267)) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) +(x267,y) = 4x267 + 4y + 7 >= 4x267 + 4y + 7 = +(y,x267) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = s(p(+(x267,y))) s(p(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = s(p(+(x267,y))) s(p(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(+(s(x267),y)) p(+(s(x267),y)) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) +(y,x267) = 4x267 + 4y + 7 >= 4x267 + 4y + 7 = +(x267,y) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) s(+(x267,p(y))) = 4x267 + 4y + 11 >= 4x267 + 4y + 8 = s(p(+(y,x267))) s(p(+(y,x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(y,x267) +(y,x267) = 4x267 + 4y + 7 >= 4x267 + 4y + 7 = +(x267,y) p(+(y,s(x267))) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(+(s(x267),y)) p(+(s(x267),y)) = 4x267 + 4y + 8 >= 4x267 + 4y + 8 = p(s(+(x267,y))) p(s(+(x267,y))) = 4x267 + 4y + 8 >= 4x267 + 4y + 7 = +(x267,y) +(x,s(x270)) = 4x + 4x270 + 7 >= 4x + 4x270 + 7 = s(+(x270,x)) +(x,s(x270)) = 4x + 4x270 + 7 >= 4x + 4x270 + 7 = +(s(x270),x) +(s(x270),x) = 4x + 4x270 + 7 >= 4x + 4x270 + 7 = s(+(x270,x)) +(0(),s(x272)) = 4x272 + 11 >= 4x272 + 11 = s(+(x272,0())) +(s(x),s(x274)) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(+(x274,s(x))) +(s(x),s(x274)) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(+(x,s(x274))) s(+(x274,s(x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(+(x,s(x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) s(s(+(x274,x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(+(x274,s(x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(+(s(x),x274)) s(+(s(x),x274)) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(+(x,s(x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) s(s(+(x274,x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(+(x274,s(x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(s(+(x,x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) s(+(x,s(x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) s(+(x274,s(x))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x,x274))) s(s(+(x,x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) s(+(x,s(x274))) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(+(s(x274),x)) s(+(s(x274),x)) = 4x + 4x274 + 7 >= 4x + 4x274 + 7 = s(s(+(x274,x))) +(p(x),s(x276)) = 4x + 4x276 + 11 >= 4x + 4x276 + 11 = s(+(x276,p(x))) +(p(x),s(x276)) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = p(+(x,s(x276))) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x,x276))) p(s(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) +(x276,x) = 4x + 4x276 + 7 >= 4x + 4x276 + 7 = +(x,x276) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 11 = s(+(p(x),x276)) s(+(p(x),x276)) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x,x276))) p(s(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 11 = s(+(p(x),x276)) s(+(p(x),x276)) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) +(x276,x) = 4x + 4x276 + 7 >= 4x + 4x276 + 7 = +(x,x276) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = s(p(+(x276,x))) s(p(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = s(p(+(x276,x))) s(p(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(+(s(x276),x)) p(+(s(x276),x)) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) +(x,x276) = 4x + 4x276 + 7 >= 4x + 4x276 + 7 = +(x276,x) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) s(+(x276,p(x))) = 4x + 4x276 + 11 >= 4x + 4x276 + 8 = s(p(+(x,x276))) s(p(+(x,x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x,x276) +(x,x276) = 4x + 4x276 + 7 >= 4x + 4x276 + 7 = +(x276,x) p(+(x,s(x276))) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(+(s(x276),x)) p(+(s(x276),x)) = 4x + 4x276 + 8 >= 4x + 4x276 + 8 = p(s(+(x276,x))) p(s(+(x276,x))) = 4x + 4x276 + 8 >= 4x + 4x276 + 7 = +(x276,x) +(p(x277),y) = 4x277 + 4y + 11 >= 4x277 + 4y + 8 = p(+(x277,y)) +(p(x277),y) = 4x277 + 4y + 11 >= 4x277 + 4y + 11 = +(y,p(x277)) +(y,p(x277)) = 4x277 + 4y + 11 >= 4x277 + 4y + 8 = p(+(x277,y)) +(p(x279),0()) = 4x279 + 15 >= 4x279 + 12 = p(+(x279,0())) +(p(x281),s(y)) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = p(+(x281,s(y))) +(p(x281),s(y)) = 4x281 + 4y + 11 >= 4x281 + 4y + 11 = s(+(y,p(x281))) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = s(p(+(y,x281))) s(p(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) +(x281,y) = 4x281 + 4y + 7 >= 4x281 + 4y + 7 = +(y,x281) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(+(s(y),x281)) p(+(s(y),x281)) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = s(p(+(y,x281))) s(p(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(+(s(y),x281)) p(+(s(y),x281)) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) +(x281,y) = 4x281 + 4y + 7 >= 4x281 + 4y + 7 = +(y,x281) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(x281,y))) p(s(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(x281,y))) p(s(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 11 = s(+(p(x281),y)) s(+(p(x281),y)) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) +(y,x281) = 4x281 + 4y + 7 >= 4x281 + 4y + 7 = +(x281,y) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) p(+(x281,s(y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 8 = p(s(+(y,x281))) p(s(+(y,x281))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(y,x281) +(y,x281) = 4x281 + 4y + 7 >= 4x281 + 4y + 7 = +(x281,y) s(+(y,p(x281))) = 4x281 + 4y + 11 >= 4x281 + 4y + 11 = s(+(p(x281),y)) s(+(p(x281),y)) = 4x281 + 4y + 11 >= 4x281 + 4y + 8 = s(p(+(x281,y))) s(p(+(x281,y))) = 4x281 + 4y + 8 >= 4x281 + 4y + 7 = +(x281,y) +(p(x283),p(y)) = 4x283 + 4y + 15 >= 4x283 + 4y + 12 = p(+(x283,p(y))) +(p(x283),p(y)) = 4x283 + 4y + 15 >= 4x283 + 4y + 12 = p(+(y,p(x283))) p(+(x283,p(y))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(+(y,p(x283))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(x283,y))) p(p(+(x283,y))) = 4x283 + 4y + 9 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(+(x283,p(y))) = 4x283 + 4y + 12 >= 4x283 + 4y + 12 = p(+(p(y),x283)) p(+(p(y),x283)) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(+(y,p(x283))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(x283,y))) p(p(+(x283,y))) = 4x283 + 4y + 9 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(+(x283,p(y))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(p(+(y,x283))) = 4x283 + 4y + 9 >= 4x283 + 4y + 9 = p(p(+(x283,y))) p(+(y,p(x283))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(x283,y))) p(+(x283,p(y))) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(y,x283))) p(p(+(y,x283))) = 4x283 + 4y + 9 >= 4x283 + 4y + 9 = p(p(+(x283,y))) p(+(y,p(x283))) = 4x283 + 4y + 12 >= 4x283 + 4y + 12 = p(+(p(x283),y)) p(+(p(x283),y)) = 4x283 + 4y + 12 >= 4x283 + 4y + 9 = p(p(+(x283,y))) +(x,p(x286)) = 4x + 4x286 + 11 >= 4x + 4x286 + 8 = p(+(x286,x)) +(x,p(x286)) = 4x + 4x286 + 11 >= 4x + 4x286 + 11 = +(p(x286),x) +(p(x286),x) = 4x + 4x286 + 11 >= 4x + 4x286 + 8 = p(+(x286,x)) +(0(),p(x288)) = 4x288 + 15 >= 4x288 + 12 = p(+(x288,0())) +(s(x),p(x290)) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = p(+(x290,s(x))) +(s(x),p(x290)) = 4x + 4x290 + 11 >= 4x + 4x290 + 11 = s(+(x,p(x290))) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = s(p(+(x,x290))) s(p(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) +(x290,x) = 4x + 4x290 + 7 >= 4x + 4x290 + 7 = +(x,x290) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(+(s(x),x290)) p(+(s(x),x290)) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = s(p(+(x,x290))) s(p(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(+(s(x),x290)) p(+(s(x),x290)) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) +(x290,x) = 4x + 4x290 + 7 >= 4x + 4x290 + 7 = +(x,x290) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x290,x))) p(s(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x290,x))) p(s(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 11 = s(+(p(x290),x)) s(+(p(x290),x)) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) +(x,x290) = 4x + 4x290 + 7 >= 4x + 4x290 + 7 = +(x290,x) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) p(+(x290,s(x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 8 = p(s(+(x,x290))) p(s(+(x,x290))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x,x290) +(x,x290) = 4x + 4x290 + 7 >= 4x + 4x290 + 7 = +(x290,x) s(+(x,p(x290))) = 4x + 4x290 + 11 >= 4x + 4x290 + 11 = s(+(p(x290),x)) s(+(p(x290),x)) = 4x + 4x290 + 11 >= 4x + 4x290 + 8 = s(p(+(x290,x))) s(p(+(x290,x))) = 4x + 4x290 + 8 >= 4x + 4x290 + 7 = +(x290,x) +(p(x),p(x292)) = 4x + 4x292 + 15 >= 4x + 4x292 + 12 = p(+(x292,p(x))) +(p(x),p(x292)) = 4x + 4x292 + 15 >= 4x + 4x292 + 12 = p(+(x,p(x292))) p(+(x292,p(x))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(+(x,p(x292))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x292,x))) p(p(+(x292,x))) = 4x + 4x292 + 9 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(+(x292,p(x))) = 4x + 4x292 + 12 >= 4x + 4x292 + 12 = p(+(p(x),x292)) p(+(p(x),x292)) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(+(x,p(x292))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x292,x))) p(p(+(x292,x))) = 4x + 4x292 + 9 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(+(x292,p(x))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(p(+(x,x292))) = 4x + 4x292 + 9 >= 4x + 4x292 + 9 = p(p(+(x292,x))) p(+(x,p(x292))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x292,x))) p(+(x292,p(x))) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x,x292))) p(p(+(x,x292))) = 4x + 4x292 + 9 >= 4x + 4x292 + 9 = p(p(+(x292,x))) p(+(x,p(x292))) = 4x + 4x292 + 12 >= 4x + 4x292 + 12 = p(+(p(x292),x)) p(+(p(x292),x)) = 4x + 4x292 + 12 >= 4x + 4x292 + 9 = p(p(+(x292,x))) +(s(p(x293)),y) = 4x293 + 4y + 11 >= 4x293 + 4y + 7 = +(x293,y) +(s(p(x293)),y) = 4x293 + 4y + 11 >= 4x293 + 4y + 11 = s(+(p(x293),y)) s(+(p(x293),y)) = 4x293 + 4y + 11 >= 4x293 + 4y + 8 = s(p(+(x293,y))) s(p(+(x293,y))) = 4x293 + 4y + 8 >= 4x293 + 4y + 7 = +(x293,y) +(x,s(p(x294))) = 4x + 4x294 + 11 >= 4x + 4x294 + 7 = +(x,x294) +(x,s(p(x294))) = 4x + 4x294 + 11 >= 4x + 4x294 + 11 = s(+(p(x294),x)) +(x,x294) = 4x + 4x294 + 7 >= 4x + 4x294 + 7 = +(x294,x) s(+(p(x294),x)) = 4x + 4x294 + 11 >= 4x + 4x294 + 8 = s(p(+(x294,x))) s(p(+(x294,x))) = 4x + 4x294 + 8 >= 4x + 4x294 + 7 = +(x294,x) p(s(p(x295))) = x295 + 2 >= x295 + 1 = p(x295) p(s(p(x295))) = x295 + 2 >= x295 + 1 = p(x295) +(p(s(x296)),y) = 4x296 + 4y + 11 >= 4x296 + 4y + 7 = +(x296,y) +(p(s(x296)),y) = 4x296 + 4y + 11 >= 4x296 + 4y + 8 = p(+(s(x296),y)) p(+(s(x296),y)) = 4x296 + 4y + 8 >= 4x296 + 4y + 8 = p(s(+(x296,y))) p(s(+(x296,y))) = 4x296 + 4y + 8 >= 4x296 + 4y + 7 = +(x296,y) +(x,p(s(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 7 = +(x,x297) +(x,p(s(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = p(+(s(x297),x)) +(x,x297) = 4x + 4x297 + 7 >= 4x + 4x297 + 7 = +(x297,x) p(+(s(x297),x)) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x297,x))) p(s(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) s(p(s(x298))) = x298 + 1 >= x298 = s(x298) s(p(s(x298))) = x298 + 1 >= x298 = s(x298) +(x,y) = 4x + 4y + 7 >= 4x + 4y + 7 = +(y,x) s(p(x)) = x + 1 >= x = x p(s(x)) = x + 1 >= x = x problem: strict: +(0(),x) -> +(x,0()) +(x,0()) -> +(0(),x) +(s(x),y) -> +(y,s(x)) +(s(x),y) -> s(+(x,y)) +(y,s(x)) -> s(+(x,y)) +(x,s(y)) -> +(s(y),x) +(x,s(y)) -> s(+(y,x)) +(s(y),x) -> s(+(y,x)) +(p(x),y) -> +(y,p(x)) +(x,p(y)) -> +(p(y),x) +(0(),y) -> +(y,0()) +(0(),s(y)) -> s(+(y,0())) +(x,0()) -> +(0(),x) +(s(x),0()) -> s(+(x,0())) +(s(x261),y) -> s(+(x261,y)) +(s(x261),y) -> +(y,s(x261)) +(y,s(x261)) -> s(+(x261,y)) +(s(x263),0()) -> s(+(x263,0())) +(s(x265),s(y)) -> s(+(x265,s(y))) +(s(x265),s(y)) -> s(+(y,s(x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(+(s(y),x265)) s(+(s(y),x265)) -> s(s(+(y,x265))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(s(+(x265,y))) s(+(x265,s(y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(+(s(x265),y)) s(+(s(x265),y)) -> s(s(+(x265,y))) +(s(x267),p(y)) -> s(+(x267,p(y))) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) p(+(y,s(x267))) -> p(s(+(x267,y))) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) p(+(y,s(x267))) -> p(s(+(x267,y))) p(s(+(x267,y))) -> p(s(+(y,x267))) s(+(x267,p(y))) -> s(+(p(y),x267)) p(+(y,s(x267))) -> p(s(+(x267,y))) +(x267,y) -> +(y,x267) s(p(+(y,x267))) -> s(p(+(x267,y))) p(+(y,s(x267))) -> p(s(+(x267,y))) s(p(+(y,x267))) -> s(p(+(x267,y))) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(s(+(x267,y))) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) p(+(s(x267),y)) -> p(s(+(x267,y))) +(x,s(x270)) -> s(+(x270,x)) +(x,s(x270)) -> +(s(x270),x) +(s(x270),x) -> s(+(x270,x)) +(0(),s(x272)) -> s(+(x272,0())) +(s(x),s(x274)) -> s(+(x274,s(x))) +(s(x),s(x274)) -> s(+(x,s(x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(+(s(x),x274)) s(+(s(x),x274)) -> s(s(+(x,x274))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(s(+(x274,x))) s(+(x274,s(x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(+(s(x274),x)) s(+(s(x274),x)) -> s(s(+(x274,x))) +(p(x),s(x276)) -> s(+(x276,p(x))) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) p(+(x,s(x276))) -> p(s(+(x276,x))) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) p(+(x,s(x276))) -> p(s(+(x276,x))) p(s(+(x276,x))) -> p(s(+(x,x276))) s(+(x276,p(x))) -> s(+(p(x),x276)) p(+(x,s(x276))) -> p(s(+(x276,x))) +(x276,x) -> +(x,x276) s(p(+(x,x276))) -> s(p(+(x276,x))) p(+(x,s(x276))) -> p(s(+(x276,x))) s(p(+(x,x276))) -> s(p(+(x276,x))) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(s(+(x276,x))) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) p(+(s(x276),x)) -> p(s(+(x276,x))) +(p(x277),y) -> +(y,p(x277)) +(p(x281),s(y)) -> s(+(y,p(x281))) p(+(x281,s(y))) -> p(s(+(y,x281))) s(p(+(x281,y))) -> s(p(+(y,x281))) p(+(x281,s(y))) -> p(s(+(y,x281))) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) s(p(+(x281,y))) -> s(p(+(y,x281))) p(+(x281,s(y))) -> p(+(s(y),x281)) p(+(s(y),x281)) -> p(s(+(y,x281))) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) p(+(x281,s(y))) -> p(s(+(y,x281))) p(s(+(y,x281))) -> p(s(+(x281,y))) s(+(y,p(x281))) -> s(+(p(x281),y)) p(+(x281,s(y))) -> p(s(+(y,x281))) +(y,x281) -> +(x281,y) p(+(x281,s(y))) -> p(s(+(y,x281))) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(+(p(y),x283)) p(p(+(x283,y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(+(p(x283),y)) +(x,p(x286)) -> +(p(x286),x) +(s(x),p(x290)) -> s(+(x,p(x290))) p(+(x290,s(x))) -> p(s(+(x,x290))) s(p(+(x290,x))) -> s(p(+(x,x290))) p(+(x290,s(x))) -> p(s(+(x,x290))) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) s(p(+(x290,x))) -> s(p(+(x,x290))) p(+(x290,s(x))) -> p(+(s(x),x290)) p(+(s(x),x290)) -> p(s(+(x,x290))) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) p(+(x290,s(x))) -> p(s(+(x,x290))) p(s(+(x,x290))) -> p(s(+(x290,x))) s(+(x,p(x290))) -> s(+(p(x290),x)) p(+(x290,s(x))) -> p(s(+(x,x290))) +(x,x290) -> +(x290,x) p(+(x290,s(x))) -> p(s(+(x,x290))) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(+(p(x),x292)) p(p(+(x292,x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(+(p(x292),x)) +(s(p(x293)),y) -> s(+(p(x293),y)) +(x,s(p(x294))) -> s(+(p(x294),x)) +(x,x294) -> +(x294,x) p(+(s(x296),y)) -> p(s(+(x296,y))) +(x,x297) -> +(x297,x) p(+(s(x297),x)) -> p(s(+(x297,x))) weak: +(x,y) -> +(y,x) +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(y,x)) Matrix Interpretation Processor: dim=1 interpretation: [p](x0) = x0, [s](x0) = x0 + 1, [+](x0, x1) = 2x0 + 2x1, [0] = 0 orientation: +(0(),x) = 2x >= 2x = +(x,0()) +(x,0()) = 2x >= 2x = +(0(),x) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,s(x)) +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 1 = s(+(x,y)) +(y,s(x)) = 2x + 2y + 2 >= 2x + 2y + 1 = s(+(x,y)) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(s(y),x) +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 1 = s(+(y,x)) +(s(y),x) = 2x + 2y + 2 >= 2x + 2y + 1 = s(+(y,x)) +(p(x),y) = 2x + 2y >= 2x + 2y = +(y,p(x)) +(x,p(y)) = 2x + 2y >= 2x + 2y = +(p(y),x) +(0(),y) = 2y >= 2y = +(y,0()) +(0(),s(y)) = 2y + 2 >= 2y + 1 = s(+(y,0())) +(x,0()) = 2x >= 2x = +(0(),x) +(s(x),0()) = 2x + 2 >= 2x + 1 = s(+(x,0())) +(s(x261),y) = 2x261 + 2y + 2 >= 2x261 + 2y + 1 = s(+(x261,y)) +(s(x261),y) = 2x261 + 2y + 2 >= 2x261 + 2y + 2 = +(y,s(x261)) +(y,s(x261)) = 2x261 + 2y + 2 >= 2x261 + 2y + 1 = s(+(x261,y)) +(s(x263),0()) = 2x263 + 2 >= 2x263 + 1 = s(+(x263,0())) +(s(x265),s(y)) = 2x265 + 2y + 4 >= 2x265 + 2y + 3 = s(+(x265,s(y))) +(s(x265),s(y)) = 2x265 + 2y + 4 >= 2x265 + 2y + 3 = s(+(y,s(x265))) s(+(x265,s(y))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(+(y,s(x265))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(x265,y))) s(s(+(x265,y))) = 2x265 + 2y + 2 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(+(x265,s(y))) = 2x265 + 2y + 3 >= 2x265 + 2y + 3 = s(+(s(y),x265)) s(+(s(y),x265)) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(+(y,s(x265))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(x265,y))) s(s(+(x265,y))) = 2x265 + 2y + 2 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(+(x265,s(y))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(s(+(y,x265))) = 2x265 + 2y + 2 >= 2x265 + 2y + 2 = s(s(+(x265,y))) s(+(y,s(x265))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(x265,y))) s(+(x265,s(y))) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(y,x265))) s(s(+(y,x265))) = 2x265 + 2y + 2 >= 2x265 + 2y + 2 = s(s(+(x265,y))) s(+(y,s(x265))) = 2x265 + 2y + 3 >= 2x265 + 2y + 3 = s(+(s(x265),y)) s(+(s(x265),y)) = 2x265 + 2y + 3 >= 2x265 + 2y + 2 = s(s(+(x265,y))) +(s(x267),p(y)) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = s(+(x267,p(y))) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) p(s(+(x267,y))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = p(s(+(y,x267))) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) +(x267,y) = 2x267 + 2y >= 2x267 + 2y = +(y,x267) s(+(x267,p(y))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = s(+(p(y),x267)) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) p(s(+(x267,y))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = p(s(+(y,x267))) s(+(x267,p(y))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = s(+(p(y),x267)) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) +(x267,y) = 2x267 + 2y >= 2x267 + 2y = +(y,x267) s(p(+(y,x267))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = s(p(+(x267,y))) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) s(p(+(y,x267))) = 2x267 + 2y + 1 >= 2x267 + 2y + 1 = s(p(+(x267,y))) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 2 = p(+(s(x267),y)) p(+(s(x267),y)) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) +(y,x267) = 2x267 + 2y >= 2x267 + 2y = +(x267,y) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) +(y,x267) = 2x267 + 2y >= 2x267 + 2y = +(x267,y) p(+(y,s(x267))) = 2x267 + 2y + 2 >= 2x267 + 2y + 2 = p(+(s(x267),y)) p(+(s(x267),y)) = 2x267 + 2y + 2 >= 2x267 + 2y + 1 = p(s(+(x267,y))) +(x,s(x270)) = 2x + 2x270 + 2 >= 2x + 2x270 + 1 = s(+(x270,x)) +(x,s(x270)) = 2x + 2x270 + 2 >= 2x + 2x270 + 2 = +(s(x270),x) +(s(x270),x) = 2x + 2x270 + 2 >= 2x + 2x270 + 1 = s(+(x270,x)) +(0(),s(x272)) = 2x272 + 2 >= 2x272 + 1 = s(+(x272,0())) +(s(x),s(x274)) = 2x + 2x274 + 4 >= 2x + 2x274 + 3 = s(+(x274,s(x))) +(s(x),s(x274)) = 2x + 2x274 + 4 >= 2x + 2x274 + 3 = s(+(x,s(x274))) s(+(x274,s(x))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(+(x,s(x274))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x274,x))) s(s(+(x274,x))) = 2x + 2x274 + 2 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(+(x274,s(x))) = 2x + 2x274 + 3 >= 2x + 2x274 + 3 = s(+(s(x),x274)) s(+(s(x),x274)) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(+(x,s(x274))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x274,x))) s(s(+(x274,x))) = 2x + 2x274 + 2 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(+(x274,s(x))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(s(+(x,x274))) = 2x + 2x274 + 2 >= 2x + 2x274 + 2 = s(s(+(x274,x))) s(+(x,s(x274))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x274,x))) s(+(x274,s(x))) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x,x274))) s(s(+(x,x274))) = 2x + 2x274 + 2 >= 2x + 2x274 + 2 = s(s(+(x274,x))) s(+(x,s(x274))) = 2x + 2x274 + 3 >= 2x + 2x274 + 3 = s(+(s(x274),x)) s(+(s(x274),x)) = 2x + 2x274 + 3 >= 2x + 2x274 + 2 = s(s(+(x274,x))) +(p(x),s(x276)) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = s(+(x276,p(x))) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) p(s(+(x276,x))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = p(s(+(x,x276))) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) +(x276,x) = 2x + 2x276 >= 2x + 2x276 = +(x,x276) s(+(x276,p(x))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = s(+(p(x),x276)) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) p(s(+(x276,x))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = p(s(+(x,x276))) s(+(x276,p(x))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = s(+(p(x),x276)) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) +(x276,x) = 2x + 2x276 >= 2x + 2x276 = +(x,x276) s(p(+(x,x276))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = s(p(+(x276,x))) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) s(p(+(x,x276))) = 2x + 2x276 + 1 >= 2x + 2x276 + 1 = s(p(+(x276,x))) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 2 = p(+(s(x276),x)) p(+(s(x276),x)) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) +(x,x276) = 2x + 2x276 >= 2x + 2x276 = +(x276,x) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) +(x,x276) = 2x + 2x276 >= 2x + 2x276 = +(x276,x) p(+(x,s(x276))) = 2x + 2x276 + 2 >= 2x + 2x276 + 2 = p(+(s(x276),x)) p(+(s(x276),x)) = 2x + 2x276 + 2 >= 2x + 2x276 + 1 = p(s(+(x276,x))) +(p(x277),y) = 2x277 + 2y >= 2x277 + 2y = +(y,p(x277)) +(p(x281),s(y)) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = s(+(y,p(x281))) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) s(p(+(x281,y))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = s(p(+(y,x281))) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) +(x281,y) = 2x281 + 2y >= 2x281 + 2y = +(y,x281) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 2 = p(+(s(y),x281)) p(+(s(y),x281)) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) s(p(+(x281,y))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = s(p(+(y,x281))) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 2 = p(+(s(y),x281)) p(+(s(y),x281)) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) +(x281,y) = 2x281 + 2y >= 2x281 + 2y = +(y,x281) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) p(s(+(y,x281))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = p(s(+(x281,y))) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) p(s(+(y,x281))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = p(s(+(x281,y))) s(+(y,p(x281))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = s(+(p(x281),y)) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) +(y,x281) = 2x281 + 2y >= 2x281 + 2y = +(x281,y) p(+(x281,s(y))) = 2x281 + 2y + 2 >= 2x281 + 2y + 1 = p(s(+(y,x281))) +(y,x281) = 2x281 + 2y >= 2x281 + 2y = +(x281,y) s(+(y,p(x281))) = 2x281 + 2y + 1 >= 2x281 + 2y + 1 = s(+(p(x281),y)) p(p(+(x283,y))) = 2x283 + 2y >= 2x283 + 2y = p(p(+(y,x283))) p(+(x283,p(y))) = 2x283 + 2y >= 2x283 + 2y = p(+(p(y),x283)) p(p(+(x283,y))) = 2x283 + 2y >= 2x283 + 2y = p(p(+(y,x283))) p(p(+(y,x283))) = 2x283 + 2y >= 2x283 + 2y = p(p(+(x283,y))) p(p(+(y,x283))) = 2x283 + 2y >= 2x283 + 2y = p(p(+(x283,y))) p(+(y,p(x283))) = 2x283 + 2y >= 2x283 + 2y = p(+(p(x283),y)) +(x,p(x286)) = 2x + 2x286 >= 2x + 2x286 = +(p(x286),x) +(s(x),p(x290)) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = s(+(x,p(x290))) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) s(p(+(x290,x))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = s(p(+(x,x290))) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) +(x290,x) = 2x + 2x290 >= 2x + 2x290 = +(x,x290) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 2 = p(+(s(x),x290)) p(+(s(x),x290)) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) s(p(+(x290,x))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = s(p(+(x,x290))) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 2 = p(+(s(x),x290)) p(+(s(x),x290)) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) +(x290,x) = 2x + 2x290 >= 2x + 2x290 = +(x,x290) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) p(s(+(x,x290))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = p(s(+(x290,x))) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) p(s(+(x,x290))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = p(s(+(x290,x))) s(+(x,p(x290))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = s(+(p(x290),x)) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) +(x,x290) = 2x + 2x290 >= 2x + 2x290 = +(x290,x) p(+(x290,s(x))) = 2x + 2x290 + 2 >= 2x + 2x290 + 1 = p(s(+(x,x290))) +(x,x290) = 2x + 2x290 >= 2x + 2x290 = +(x290,x) s(+(x,p(x290))) = 2x + 2x290 + 1 >= 2x + 2x290 + 1 = s(+(p(x290),x)) p(p(+(x292,x))) = 2x + 2x292 >= 2x + 2x292 = p(p(+(x,x292))) p(+(x292,p(x))) = 2x + 2x292 >= 2x + 2x292 = p(+(p(x),x292)) p(p(+(x292,x))) = 2x + 2x292 >= 2x + 2x292 = p(p(+(x,x292))) p(p(+(x,x292))) = 2x + 2x292 >= 2x + 2x292 = p(p(+(x292,x))) p(p(+(x,x292))) = 2x + 2x292 >= 2x + 2x292 = p(p(+(x292,x))) p(+(x,p(x292))) = 2x + 2x292 >= 2x + 2x292 = p(+(p(x292),x)) +(s(p(x293)),y) = 2x293 + 2y + 2 >= 2x293 + 2y + 1 = s(+(p(x293),y)) +(x,s(p(x294))) = 2x + 2x294 + 2 >= 2x + 2x294 + 1 = s(+(p(x294),x)) +(x,x294) = 2x + 2x294 >= 2x + 2x294 = +(x294,x) p(+(s(x296),y)) = 2x296 + 2y + 2 >= 2x296 + 2y + 1 = p(s(+(x296,y))) +(x,x297) = 2x + 2x297 >= 2x + 2x297 = +(x297,x) p(+(s(x297),x)) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x297,x))) +(x,y) = 2x + 2y >= 2x + 2y = +(y,x) problem: strict: +(0(),x) -> +(x,0()) +(x,0()) -> +(0(),x) +(s(x),y) -> +(y,s(x)) +(x,s(y)) -> +(s(y),x) +(p(x),y) -> +(y,p(x)) +(x,p(y)) -> +(p(y),x) +(0(),y) -> +(y,0()) +(x,0()) -> +(0(),x) +(s(x261),y) -> +(y,s(x261)) s(s(+(x265,y))) -> s(s(+(y,x265))) s(+(x265,s(y))) -> s(+(s(y),x265)) s(s(+(x265,y))) -> s(s(+(y,x265))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(s(+(y,x265))) -> s(s(+(x265,y))) s(+(y,s(x265))) -> s(+(s(x265),y)) p(s(+(x267,y))) -> p(s(+(y,x267))) +(x267,y) -> +(y,x267) s(+(x267,p(y))) -> s(+(p(y),x267)) p(s(+(x267,y))) -> p(s(+(y,x267))) s(+(x267,p(y))) -> s(+(p(y),x267)) +(x267,y) -> +(y,x267) s(p(+(y,x267))) -> s(p(+(x267,y))) s(p(+(y,x267))) -> s(p(+(x267,y))) p(+(y,s(x267))) -> p(+(s(x267),y)) +(y,x267) -> +(x267,y) +(y,x267) -> +(x267,y) p(+(y,s(x267))) -> p(+(s(x267),y)) +(x,s(x270)) -> +(s(x270),x) s(s(+(x274,x))) -> s(s(+(x,x274))) s(+(x274,s(x))) -> s(+(s(x),x274)) s(s(+(x274,x))) -> s(s(+(x,x274))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(s(+(x,x274))) -> s(s(+(x274,x))) s(+(x,s(x274))) -> s(+(s(x274),x)) p(s(+(x276,x))) -> p(s(+(x,x276))) +(x276,x) -> +(x,x276) s(+(x276,p(x))) -> s(+(p(x),x276)) p(s(+(x276,x))) -> p(s(+(x,x276))) s(+(x276,p(x))) -> s(+(p(x),x276)) +(x276,x) -> +(x,x276) s(p(+(x,x276))) -> s(p(+(x276,x))) s(p(+(x,x276))) -> s(p(+(x276,x))) p(+(x,s(x276))) -> p(+(s(x276),x)) +(x,x276) -> +(x276,x) +(x,x276) -> +(x276,x) p(+(x,s(x276))) -> p(+(s(x276),x)) +(p(x277),y) -> +(y,p(x277)) s(p(+(x281,y))) -> s(p(+(y,x281))) +(x281,y) -> +(y,x281) p(+(x281,s(y))) -> p(+(s(y),x281)) s(p(+(x281,y))) -> s(p(+(y,x281))) p(+(x281,s(y))) -> p(+(s(y),x281)) +(x281,y) -> +(y,x281) p(s(+(y,x281))) -> p(s(+(x281,y))) p(s(+(y,x281))) -> p(s(+(x281,y))) s(+(y,p(x281))) -> s(+(p(x281),y)) +(y,x281) -> +(x281,y) +(y,x281) -> +(x281,y) s(+(y,p(x281))) -> s(+(p(x281),y)) p(p(+(x283,y))) -> p(p(+(y,x283))) p(+(x283,p(y))) -> p(+(p(y),x283)) p(p(+(x283,y))) -> p(p(+(y,x283))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(p(+(y,x283))) -> p(p(+(x283,y))) p(+(y,p(x283))) -> p(+(p(x283),y)) +(x,p(x286)) -> +(p(x286),x) s(p(+(x290,x))) -> s(p(+(x,x290))) +(x290,x) -> +(x,x290) p(+(x290,s(x))) -> p(+(s(x),x290)) s(p(+(x290,x))) -> s(p(+(x,x290))) p(+(x290,s(x))) -> p(+(s(x),x290)) +(x290,x) -> +(x,x290) p(s(+(x,x290))) -> p(s(+(x290,x))) p(s(+(x,x290))) -> p(s(+(x290,x))) s(+(x,p(x290))) -> s(+(p(x290),x)) +(x,x290) -> +(x290,x) +(x,x290) -> +(x290,x) s(+(x,p(x290))) -> s(+(p(x290),x)) p(p(+(x292,x))) -> p(p(+(x,x292))) p(+(x292,p(x))) -> p(+(p(x),x292)) p(p(+(x292,x))) -> p(p(+(x,x292))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(p(+(x,x292))) -> p(p(+(x292,x))) p(+(x,p(x292))) -> p(+(p(x292),x)) +(x,x294) -> +(x294,x) +(x,x297) -> +(x297,x) weak: +(x,y) -> +(y,x) Shift Processor (ldh) lab=left (force): strict: weak: Decreasing Processor: The following diagrams are decreasing: peak: +(x,0()) <-0|[1,0]- +(0(),x) -1|[1,0]-> x joins: +(x,0()) -2|[1,0]-> x peak: +(0(),x) <-0|[1,0]- +(x,0()) -2|[1,0]-> x joins: +(0(),x) -1|[1,0]-> x peak: +(y,s(x)) <-0|[1,0]- +(s(x),y) -3|[1,0]-> s(+(x,y)) joins: +(y,s(x)) -4|[1,0]-> s(+(x,y)) peak: +(s(y),x) <-0|[1,0]- +(x,s(y)) -4|[1,0]-> s(+(y,x)) joins: +(s(y),x) -3|[1,0]-> s(+(y,x)) peak: +(y,p(x)) <-0|[1,0]- +(p(x),y) -5|[1,0]-> p(+(x,y)) joins: +(y,p(x)) -6|[1,0]-> p(+(x,y)) peak: +(p(y),x) <-0|[1,0]- +(x,p(y)) -6|[1,0]-> p(+(y,x)) joins: +(p(y),x) -5|[1,0]-> p(+(y,x)) peak: y <-1|[1,0]- +(0(),y) -0|[1,0]-> +(y,0()) joins: +(y,0()) -2|[1,0]-> y peak: 0() <-1|[1,0]- +(0(),0()) -2|[1,0]-> 0() joins: peak: s(y) <-1|[1,0]- +(0(),s(y)) -4|[1,0]-> s(+(y,0())) joins: s(+(y,0())) -2|0[0,0]-> s(y) peak: p(y) <-1|[1,0]- +(0(),p(y)) -6|[1,0]-> p(+(y,0())) joins: p(+(y,0())) -2|0[0,0]-> p(y) peak: x <-2|[1,0]- +(x,0()) -0|[1,0]-> +(0(),x) joins: +(0(),x) -1|[1,0]-> x peak: 0() <-2|[1,0]- +(0(),0()) -1|[1,0]-> 0() joins: peak: s(x) <-2|[1,0]- +(s(x),0()) -3|[1,0]-> s(+(x,0())) joins: s(+(x,0())) -2|0[0,0]-> s(x) peak: p(x) <-2|[1,0]- +(p(x),0()) -5|[1,0]-> p(+(x,0())) joins: p(+(x,0())) -2|0[0,0]-> p(x) peak: s(+(x261,y)) <-3|[1,0]- +(s(x261),y) -0|[1,0]-> +(y,s(x261)) joins: +(y,s(x261)) -4|[1,0]-> s(+(x261,y)) peak: s(+(x263,0())) <-3|[1,0]- +(s(x263),0()) -2|[1,0]-> s(x263) joins: s(+(x263,0())) -2|0[0,0]-> s(x263) peak: s(+(x265,s(y))) <-3|[1,0]- +(s(x265),s(y)) -4|[1,0]-> s(+(y,s(x265))) joins: s(+(x265,s(y))) -4|0[0,0]-> s(s(+(y,x265))) s(+(y,s(x265))) -4|0[0,0]-> s(s(+(x265,y))) -0|0,0[0,0]-> s(s(+(y,x265))) peak: s(+(x267,p(y))) <-3|[1,0]- +(s(x267),p(y)) -6|[1,0]-> p(+(y,s(x267))) joins: s(+(x267,p(y))) -6|0[0,0]-> s(p(+(y,x267))) -7|[0,0]-> +(y,x267) p(+(y,s(x267))) -4|0[0,0]-> p(s(+(x267,y))) -0|0,0[0,0]-> p(s(+(y,x267))) -8|[0,0]-> +(y,x267) peak: s(+(x270,x)) <-4|[1,0]- +(x,s(x270)) -0|[1,0]-> +(s(x270),x) joins: +(s(x270),x) -3|[1,0]-> s(+(x270,x)) peak: s(+(x272,0())) <-4|[1,0]- +(0(),s(x272)) -1|[1,0]-> s(x272) joins: s(+(x272,0())) -2|0[0,0]-> s(x272) peak: s(+(x274,s(x))) <-4|[1,0]- +(s(x),s(x274)) -3|[1,0]-> s(+(x,s(x274))) joins: s(+(x274,s(x))) -4|0[0,0]-> s(s(+(x,x274))) s(+(x,s(x274))) -4|0[0,0]-> s(s(+(x274,x))) -0|0,0[0,0]-> s(s(+(x,x274))) peak: s(+(x276,p(x))) <-4|[1,0]- +(p(x),s(x276)) -5|[1,0]-> p(+(x,s(x276))) joins: s(+(x276,p(x))) -6|0[0,0]-> s(p(+(x,x276))) -7|[0,0]-> +(x,x276) p(+(x,s(x276))) -4|0[0,0]-> p(s(+(x276,x))) -0|0,0[0,0]-> p(s(+(x,x276))) -8|[0,0]-> +(x,x276) peak: p(+(x277,y)) <-5|[1,0]- +(p(x277),y) -0|[1,0]-> +(y,p(x277)) joins: +(y,p(x277)) -6|[1,0]-> p(+(x277,y)) peak: p(+(x279,0())) <-5|[1,0]- +(p(x279),0()) -2|[1,0]-> p(x279) joins: p(+(x279,0())) -2|0[0,0]-> p(x279) peak: p(+(x281,s(y))) <-5|[1,0]- +(p(x281),s(y)) -4|[1,0]-> s(+(y,p(x281))) joins: p(+(x281,s(y))) -4|0[0,0]-> p(s(+(y,x281))) -8|[0,0]-> +(y,x281) s(+(y,p(x281))) -6|0[0,0]-> s(p(+(x281,y))) -0|0,0[0,0]-> s(p(+(y,x281))) -7|[0,0]-> +(y,x281) peak: p(+(x283,p(y))) <-5|[1,0]- +(p(x283),p(y)) -6|[1,0]-> p(+(y,p(x283))) joins: p(+(x283,p(y))) -6|0[0,0]-> p(p(+(y,x283))) p(+(y,p(x283))) -6|0[0,0]-> p(p(+(x283,y))) -0|0,0[0,0]-> p(p(+(y,x283))) peak: p(+(x286,x)) <-6|[1,0]- +(x,p(x286)) -0|[1,0]-> +(p(x286),x) joins: +(p(x286),x) -5|[1,0]-> p(+(x286,x)) peak: p(+(x288,0())) <-6|[1,0]- +(0(),p(x288)) -1|[1,0]-> p(x288) joins: p(+(x288,0())) -2|0[0,0]-> p(x288) peak: p(+(x290,s(x))) <-6|[1,0]- +(s(x),p(x290)) -3|[1,0]-> s(+(x,p(x290))) joins: p(+(x290,s(x))) -4|0[0,0]-> p(s(+(x,x290))) -8|[0,0]-> +(x,x290) s(+(x,p(x290))) -6|0[0,0]-> s(p(+(x290,x))) -0|0,0[0,0]-> s(p(+(x,x290))) -7|[0,0]-> +(x,x290) peak: p(+(x292,p(x))) <-6|[1,0]- +(p(x),p(x292)) -5|[1,0]-> p(+(x,p(x292))) joins: p(+(x292,p(x))) -6|0[0,0]-> p(p(+(x,x292))) p(+(x,p(x292))) -6|0[0,0]-> p(p(+(x292,x))) -0|0,0[0,0]-> p(p(+(x,x292))) peak: +(x293,y) <-7|0[1,2]- +(s(p(x293)),y) -3|[1,0]-> s(+(p(x293),y)) joins: s(+(p(x293),y)) -5|0[0,0]-> s(p(+(x293,y))) -7|[0,0]-> +(x293,y) peak: +(x,x294) <-7|1[1,2]- +(x,s(p(x294))) -4|[1,0]-> s(+(p(x294),x)) joins: +(x,x294) -0|[0,0]-> +(x294,x) s(+(p(x294),x)) -5|0[0,0]-> s(p(+(x294,x))) -7|[0,0]-> +(x294,x) peak: p(x295) <-7|0[1,0]- p(s(p(x295))) -8|[1,0]-> p(x295) joins: peak: +(x296,y) <-8|0[1,2]- +(p(s(x296)),y) -5|[1,0]-> p(+(s(x296),y)) joins: p(+(s(x296),y)) -3|0[0,0]-> p(s(+(x296,y))) -8|[0,0]-> +(x296,y) peak: +(x,x297) <-8|1[1,2]- +(x,p(s(x297))) -6|[1,0]-> p(+(s(x297),x)) joins: +(x,x297) -0|[0,0]-> +(x297,x) p(+(s(x297),x)) -3|0[0,0]-> p(s(+(x297,x))) -8|[0,0]-> +(x297,x) peak: s(x298) <-8|0[1,0]- s(p(s(x298))) -7|[1,0]-> s(x298) joins: Qed