Problem: -(x,x) -> 0() -(x,0()) -> x +(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() -(x,0()) -> x 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, 2>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() -(x,0()) -> x Church Rosser Transformation Processor (kb): -(x,x) -> 0() -(x,0()) -> x critical peaks: joinable Matrix Interpretation Processor: dim=3 interpretation: [0] [0] = [1] [0], [1 1 1] [1 0 0] [1] [-](x0, x1) = [1 1 1]x0 + [0 0 0]x1 + [1] [1 1 1] [0 1 0] [0] orientation: [2 1 1] [1] [0] -(x,x) = [1 1 1]x + [1] >= [1] = 0() [1 2 1] [0] [0] [1 1 1] [1] -(x,0()) = [1 1 1]x + [1] >= x = x [1 1 1] [1] 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(+(x268,y)) <-3|[]- +(s(x268),y) -0|[]-> +(y,s(x268)) s(+(x270,0())) <-3|[]- +(s(x270),0()) -2|[]-> s(x270) s(+(x272,s(y))) <-3|[]- +(s(x272),s(y)) -4|[]-> s(+(y,s(x272))) s(+(x274,p(y))) <-3|[]- +(s(x274),p(y)) -6|[]-> p(+(y,s(x274))) s(+(x277,x)) <-4|[]- +(x,s(x277)) -0|[]-> +(s(x277),x) s(+(x279,0())) <-4|[]- +(0(),s(x279)) -1|[]-> s(x279) s(+(x281,s(x))) <-4|[]- +(s(x),s(x281)) -3|[]-> s(+(x,s(x281))) s(+(x283,p(x))) <-4|[]- +(p(x),s(x283)) -5|[]-> p(+(x,s(x283))) p(+(x284,y)) <-5|[]- +(p(x284),y) -0|[]-> +(y,p(x284)) p(+(x286,0())) <-5|[]- +(p(x286),0()) -2|[]-> p(x286) p(+(x288,s(y))) <-5|[]- +(p(x288),s(y)) -4|[]-> s(+(y,p(x288))) p(+(x290,p(y))) <-5|[]- +(p(x290),p(y)) -6|[]-> p(+(y,p(x290))) p(+(x293,x)) <-6|[]- +(x,p(x293)) -0|[]-> +(p(x293),x) p(+(x295,0())) <-6|[]- +(0(),p(x295)) -1|[]-> p(x295) p(+(x297,s(x))) <-6|[]- +(s(x),p(x297)) -3|[]-> s(+(x,p(x297))) p(+(x299,p(x))) <-6|[]- +(p(x),p(x299)) -5|[]-> p(+(x,p(x299))) +(x300,y) <-7|0[]- +(s(p(x300)),y) -3|[]-> s(+(p(x300),y)) +(x,x301) <-7|1[]- +(x,s(p(x301))) -4|[]-> s(+(p(x301),x)) p(x302) <-7|0[]- p(s(p(x302))) -8|[]-> p(x302) +(x303,y) <-8|0[]- +(p(s(x303)),y) -5|[]-> p(+(s(x303),y)) +(x,x304) <-8|1[]- +(x,p(s(x304))) -6|[]-> p(+(s(x304),x)) s(x305) <-8|0[]- s(p(s(x305))) -7|[]-> s(x305) 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(x268),y) -> s(+(x268,y)) +(s(x268),y) -> +(y,s(x268)) +(y,s(x268)) -> s(+(x268,y)) +(s(x270),0()) -> s(+(x270,0())) +(s(x270),0()) -> s(x270) s(+(x270,0())) -> s(x270) +(s(x272),s(y)) -> s(+(x272,s(y))) +(s(x272),s(y)) -> s(+(y,s(x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(+(s(y),x272)) s(+(s(y),x272)) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(+(s(x272),y)) s(+(s(x272),y)) -> s(s(+(x272,y))) +(s(x274),p(y)) -> s(+(x274,p(y))) +(s(x274),p(y)) -> p(+(y,s(x274))) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) p(s(+(y,x274))) -> +(y,x274) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) s(+(p(y),x274)) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) p(s(+(y,x274))) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) s(+(p(y),x274)) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> s(p(+(x274,y))) s(p(+(x274,y))) -> +(x274,y) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> s(p(+(x274,y))) s(p(+(x274,y))) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x,s(x277)) -> s(+(x277,x)) +(x,s(x277)) -> +(s(x277),x) +(s(x277),x) -> s(+(x277,x)) +(0(),s(x279)) -> s(+(x279,0())) +(0(),s(x279)) -> s(x279) s(+(x279,0())) -> s(x279) +(s(x),s(x281)) -> s(+(x281,s(x))) +(s(x),s(x281)) -> s(+(x,s(x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(+(s(x),x281)) s(+(s(x),x281)) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(+(s(x281),x)) s(+(s(x281),x)) -> s(s(+(x281,x))) +(p(x),s(x283)) -> s(+(x283,p(x))) +(p(x),s(x283)) -> p(+(x,s(x283))) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) p(s(+(x,x283))) -> +(x,x283) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) s(+(p(x),x283)) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) p(s(+(x,x283))) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) s(+(p(x),x283)) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> s(p(+(x283,x))) s(p(+(x283,x))) -> +(x283,x) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> s(p(+(x283,x))) s(p(+(x283,x))) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(p(x284),y) -> p(+(x284,y)) +(p(x284),y) -> +(y,p(x284)) +(y,p(x284)) -> p(+(x284,y)) +(p(x286),0()) -> p(+(x286,0())) +(p(x286),0()) -> p(x286) p(+(x286,0())) -> p(x286) +(p(x288),s(y)) -> p(+(x288,s(y))) +(p(x288),s(y)) -> s(+(y,p(x288))) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> s(p(+(y,x288))) s(p(+(y,x288))) -> +(y,x288) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> s(p(+(y,x288))) s(p(+(y,x288))) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) p(s(+(x288,y))) -> +(x288,y) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) p(s(+(x288,y))) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) s(+(p(x288),y)) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) s(+(p(x288),y)) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(p(x290),p(y)) -> p(+(x290,p(y))) +(p(x290),p(y)) -> p(+(y,p(x290))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(+(p(y),x290)) p(+(p(y),x290)) -> p(p(+(y,x290))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(+(p(x290),y)) p(+(p(x290),y)) -> p(p(+(x290,y))) +(x,p(x293)) -> p(+(x293,x)) +(x,p(x293)) -> +(p(x293),x) +(p(x293),x) -> p(+(x293,x)) +(0(),p(x295)) -> p(+(x295,0())) +(0(),p(x295)) -> p(x295) p(+(x295,0())) -> p(x295) +(s(x),p(x297)) -> p(+(x297,s(x))) +(s(x),p(x297)) -> s(+(x,p(x297))) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> s(p(+(x,x297))) s(p(+(x,x297))) -> +(x,x297) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> s(p(+(x,x297))) s(p(+(x,x297))) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) s(+(p(x297),x)) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) s(+(p(x297),x)) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(p(x),p(x299)) -> p(+(x299,p(x))) +(p(x),p(x299)) -> p(+(x,p(x299))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(+(p(x),x299)) p(+(p(x),x299)) -> p(p(+(x,x299))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(+(p(x299),x)) p(+(p(x299),x)) -> p(p(+(x299,x))) +(s(p(x300)),y) -> +(x300,y) +(s(p(x300)),y) -> s(+(p(x300),y)) s(+(p(x300),y)) -> s(p(+(x300,y))) s(p(+(x300,y))) -> +(x300,y) +(x,s(p(x301))) -> +(x,x301) +(x,s(p(x301))) -> s(+(p(x301),x)) +(x,x301) -> +(x301,x) s(+(p(x301),x)) -> s(p(+(x301,x))) s(p(+(x301,x))) -> +(x301,x) p(s(p(x302))) -> p(x302) p(s(p(x302))) -> p(x302) +(p(s(x303)),y) -> +(x303,y) +(p(s(x303)),y) -> p(+(s(x303),y)) p(+(s(x303),y)) -> p(s(+(x303,y))) p(s(+(x303,y))) -> +(x303,y) +(x,p(s(x304))) -> +(x,x304) +(x,p(s(x304))) -> p(+(s(x304),x)) +(x,x304) -> +(x304,x) p(+(s(x304),x)) -> p(s(+(x304,x))) p(s(+(x304,x))) -> +(x304,x) s(p(s(x305))) -> s(x305) s(p(s(x305))) -> s(x305) 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(x268),y) = x268 + y >= x268 + y = s(+(x268,y)) +(s(x268),y) = x268 + y >= x268 + y = +(y,s(x268)) +(y,s(x268)) = x268 + y >= x268 + y = s(+(x268,y)) +(s(x270),0()) = x270 + 5 >= x270 + 5 = s(+(x270,0())) +(s(x270),0()) = x270 + 5 >= x270 = s(x270) s(+(x270,0())) = x270 + 5 >= x270 = s(x270) +(s(x272),s(y)) = x272 + y >= x272 + y = s(+(x272,s(y))) +(s(x272),s(y)) = x272 + y >= x272 + y = s(+(y,s(x272))) s(+(x272,s(y))) = x272 + y >= x272 + y = s(s(+(y,x272))) s(+(y,s(x272))) = x272 + y >= x272 + y = s(s(+(x272,y))) s(s(+(x272,y))) = x272 + y >= x272 + y = s(s(+(y,x272))) s(+(x272,s(y))) = x272 + y >= x272 + y = s(+(s(y),x272)) s(+(s(y),x272)) = x272 + y >= x272 + y = s(s(+(y,x272))) s(+(y,s(x272))) = x272 + y >= x272 + y = s(s(+(x272,y))) s(s(+(x272,y))) = x272 + y >= x272 + y = s(s(+(y,x272))) s(+(x272,s(y))) = x272 + y >= x272 + y = s(s(+(y,x272))) s(s(+(y,x272))) = x272 + y >= x272 + y = s(s(+(x272,y))) s(+(y,s(x272))) = x272 + y >= x272 + y = s(s(+(x272,y))) s(+(x272,s(y))) = x272 + y >= x272 + y = s(s(+(y,x272))) s(s(+(y,x272))) = x272 + y >= x272 + y = s(s(+(x272,y))) s(+(y,s(x272))) = x272 + y >= x272 + y = s(+(s(x272),y)) s(+(s(x272),y)) = x272 + y >= x272 + y = s(s(+(x272,y))) +(s(x274),p(y)) = x274 + y >= x274 + y = s(+(x274,p(y))) +(s(x274),p(y)) = x274 + y >= x274 + y = p(+(y,s(x274))) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = p(s(+(y,x274))) p(s(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) +(x274,y) = x274 + y >= x274 + y = +(y,x274) s(+(x274,p(y))) = x274 + y >= x274 + y = s(+(p(y),x274)) s(+(p(y),x274)) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = p(s(+(y,x274))) p(s(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) s(+(x274,p(y))) = x274 + y >= x274 + y = s(+(p(y),x274)) s(+(p(y),x274)) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) +(x274,y) = x274 + y >= x274 + y = +(y,x274) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = s(p(+(x274,y))) s(p(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = s(p(+(x274,y))) s(p(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) p(+(y,s(x274))) = x274 + y >= x274 + y = p(+(s(x274),y)) p(+(s(x274),y)) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) +(y,x274) = x274 + y >= x274 + y = +(x274,y) p(+(y,s(x274))) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) s(+(x274,p(y))) = x274 + y >= x274 + y = s(p(+(y,x274))) s(p(+(y,x274))) = x274 + y >= x274 + y = +(y,x274) +(y,x274) = x274 + y >= x274 + y = +(x274,y) p(+(y,s(x274))) = x274 + y >= x274 + y = p(+(s(x274),y)) p(+(s(x274),y)) = x274 + y >= x274 + y = p(s(+(x274,y))) p(s(+(x274,y))) = x274 + y >= x274 + y = +(x274,y) +(x,s(x277)) = x + x277 >= x + x277 = s(+(x277,x)) +(x,s(x277)) = x + x277 >= x + x277 = +(s(x277),x) +(s(x277),x) = x + x277 >= x + x277 = s(+(x277,x)) +(0(),s(x279)) = x279 + 5 >= x279 + 5 = s(+(x279,0())) +(0(),s(x279)) = x279 + 5 >= x279 = s(x279) s(+(x279,0())) = x279 + 5 >= x279 = s(x279) +(s(x),s(x281)) = x + x281 >= x + x281 = s(+(x281,s(x))) +(s(x),s(x281)) = x + x281 >= x + x281 = s(+(x,s(x281))) s(+(x281,s(x))) = x + x281 >= x + x281 = s(s(+(x,x281))) s(+(x,s(x281))) = x + x281 >= x + x281 = s(s(+(x281,x))) s(s(+(x281,x))) = x + x281 >= x + x281 = s(s(+(x,x281))) s(+(x281,s(x))) = x + x281 >= x + x281 = s(+(s(x),x281)) s(+(s(x),x281)) = x + x281 >= x + x281 = s(s(+(x,x281))) s(+(x,s(x281))) = x + x281 >= x + x281 = s(s(+(x281,x))) s(s(+(x281,x))) = x + x281 >= x + x281 = s(s(+(x,x281))) s(+(x281,s(x))) = x + x281 >= x + x281 = s(s(+(x,x281))) s(s(+(x,x281))) = x + x281 >= x + x281 = s(s(+(x281,x))) s(+(x,s(x281))) = x + x281 >= x + x281 = s(s(+(x281,x))) s(+(x281,s(x))) = x + x281 >= x + x281 = s(s(+(x,x281))) s(s(+(x,x281))) = x + x281 >= x + x281 = s(s(+(x281,x))) s(+(x,s(x281))) = x + x281 >= x + x281 = s(+(s(x281),x)) s(+(s(x281),x)) = x + x281 >= x + x281 = s(s(+(x281,x))) +(p(x),s(x283)) = x + x283 >= x + x283 = s(+(x283,p(x))) +(p(x),s(x283)) = x + x283 >= x + x283 = p(+(x,s(x283))) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = p(s(+(x,x283))) p(s(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) +(x283,x) = x + x283 >= x + x283 = +(x,x283) s(+(x283,p(x))) = x + x283 >= x + x283 = s(+(p(x),x283)) s(+(p(x),x283)) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = p(s(+(x,x283))) p(s(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) s(+(x283,p(x))) = x + x283 >= x + x283 = s(+(p(x),x283)) s(+(p(x),x283)) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) +(x283,x) = x + x283 >= x + x283 = +(x,x283) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = s(p(+(x283,x))) s(p(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = s(p(+(x283,x))) s(p(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) p(+(x,s(x283))) = x + x283 >= x + x283 = p(+(s(x283),x)) p(+(s(x283),x)) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) +(x,x283) = x + x283 >= x + x283 = +(x283,x) p(+(x,s(x283))) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) s(+(x283,p(x))) = x + x283 >= x + x283 = s(p(+(x,x283))) s(p(+(x,x283))) = x + x283 >= x + x283 = +(x,x283) +(x,x283) = x + x283 >= x + x283 = +(x283,x) p(+(x,s(x283))) = x + x283 >= x + x283 = p(+(s(x283),x)) p(+(s(x283),x)) = x + x283 >= x + x283 = p(s(+(x283,x))) p(s(+(x283,x))) = x + x283 >= x + x283 = +(x283,x) +(p(x284),y) = x284 + y >= x284 + y = p(+(x284,y)) +(p(x284),y) = x284 + y >= x284 + y = +(y,p(x284)) +(y,p(x284)) = x284 + y >= x284 + y = p(+(x284,y)) +(p(x286),0()) = x286 + 5 >= x286 + 5 = p(+(x286,0())) +(p(x286),0()) = x286 + 5 >= x286 = p(x286) p(+(x286,0())) = x286 + 5 >= x286 = p(x286) +(p(x288),s(y)) = x288 + y >= x288 + y = p(+(x288,s(y))) +(p(x288),s(y)) = x288 + y >= x288 + y = s(+(y,p(x288))) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = s(p(+(y,x288))) s(p(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) +(x288,y) = x288 + y >= x288 + y = +(y,x288) p(+(x288,s(y))) = x288 + y >= x288 + y = p(+(s(y),x288)) p(+(s(y),x288)) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = s(p(+(y,x288))) s(p(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) p(+(x288,s(y))) = x288 + y >= x288 + y = p(+(s(y),x288)) p(+(s(y),x288)) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) +(x288,y) = x288 + y >= x288 + y = +(y,x288) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = p(s(+(x288,y))) p(s(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = p(s(+(x288,y))) p(s(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) s(+(y,p(x288))) = x288 + y >= x288 + y = s(+(p(x288),y)) s(+(p(x288),y)) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) +(y,x288) = x288 + y >= x288 + y = +(x288,y) s(+(y,p(x288))) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) p(+(x288,s(y))) = x288 + y >= x288 + y = p(s(+(y,x288))) p(s(+(y,x288))) = x288 + y >= x288 + y = +(y,x288) +(y,x288) = x288 + y >= x288 + y = +(x288,y) s(+(y,p(x288))) = x288 + y >= x288 + y = s(+(p(x288),y)) s(+(p(x288),y)) = x288 + y >= x288 + y = s(p(+(x288,y))) s(p(+(x288,y))) = x288 + y >= x288 + y = +(x288,y) +(p(x290),p(y)) = x290 + y >= x290 + y = p(+(x290,p(y))) +(p(x290),p(y)) = x290 + y >= x290 + y = p(+(y,p(x290))) p(+(x290,p(y))) = x290 + y >= x290 + y = p(p(+(y,x290))) p(+(y,p(x290))) = x290 + y >= x290 + y = p(p(+(x290,y))) p(p(+(x290,y))) = x290 + y >= x290 + y = p(p(+(y,x290))) p(+(x290,p(y))) = x290 + y >= x290 + y = p(+(p(y),x290)) p(+(p(y),x290)) = x290 + y >= x290 + y = p(p(+(y,x290))) p(+(y,p(x290))) = x290 + y >= x290 + y = p(p(+(x290,y))) p(p(+(x290,y))) = x290 + y >= x290 + y = p(p(+(y,x290))) p(+(x290,p(y))) = x290 + y >= x290 + y = p(p(+(y,x290))) p(p(+(y,x290))) = x290 + y >= x290 + y = p(p(+(x290,y))) p(+(y,p(x290))) = x290 + y >= x290 + y = p(p(+(x290,y))) p(+(x290,p(y))) = x290 + y >= x290 + y = p(p(+(y,x290))) p(p(+(y,x290))) = x290 + y >= x290 + y = p(p(+(x290,y))) p(+(y,p(x290))) = x290 + y >= x290 + y = p(+(p(x290),y)) p(+(p(x290),y)) = x290 + y >= x290 + y = p(p(+(x290,y))) +(x,p(x293)) = x + x293 >= x + x293 = p(+(x293,x)) +(x,p(x293)) = x + x293 >= x + x293 = +(p(x293),x) +(p(x293),x) = x + x293 >= x + x293 = p(+(x293,x)) +(0(),p(x295)) = x295 + 5 >= x295 + 5 = p(+(x295,0())) +(0(),p(x295)) = x295 + 5 >= x295 = p(x295) p(+(x295,0())) = x295 + 5 >= x295 = p(x295) +(s(x),p(x297)) = x + x297 >= x + x297 = p(+(x297,s(x))) +(s(x),p(x297)) = x + x297 >= x + x297 = s(+(x,p(x297))) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = s(p(+(x,x297))) s(p(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) +(x297,x) = x + x297 >= x + x297 = +(x,x297) p(+(x297,s(x))) = x + x297 >= x + x297 = p(+(s(x),x297)) p(+(s(x),x297)) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = s(p(+(x,x297))) s(p(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) p(+(x297,s(x))) = x + x297 >= x + x297 = p(+(s(x),x297)) p(+(s(x),x297)) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) +(x297,x) = x + x297 >= x + x297 = +(x,x297) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = p(s(+(x297,x))) p(s(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = p(s(+(x297,x))) p(s(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) s(+(x,p(x297))) = x + x297 >= x + x297 = s(+(p(x297),x)) s(+(p(x297),x)) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) +(x,x297) = x + x297 >= x + x297 = +(x297,x) s(+(x,p(x297))) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) p(+(x297,s(x))) = x + x297 >= x + x297 = p(s(+(x,x297))) p(s(+(x,x297))) = x + x297 >= x + x297 = +(x,x297) +(x,x297) = x + x297 >= x + x297 = +(x297,x) s(+(x,p(x297))) = x + x297 >= x + x297 = s(+(p(x297),x)) s(+(p(x297),x)) = x + x297 >= x + x297 = s(p(+(x297,x))) s(p(+(x297,x))) = x + x297 >= x + x297 = +(x297,x) +(p(x),p(x299)) = x + x299 >= x + x299 = p(+(x299,p(x))) +(p(x),p(x299)) = x + x299 >= x + x299 = p(+(x,p(x299))) p(+(x299,p(x))) = x + x299 >= x + x299 = p(p(+(x,x299))) p(+(x,p(x299))) = x + x299 >= x + x299 = p(p(+(x299,x))) p(p(+(x299,x))) = x + x299 >= x + x299 = p(p(+(x,x299))) p(+(x299,p(x))) = x + x299 >= x + x299 = p(+(p(x),x299)) p(+(p(x),x299)) = x + x299 >= x + x299 = p(p(+(x,x299))) p(+(x,p(x299))) = x + x299 >= x + x299 = p(p(+(x299,x))) p(p(+(x299,x))) = x + x299 >= x + x299 = p(p(+(x,x299))) p(+(x299,p(x))) = x + x299 >= x + x299 = p(p(+(x,x299))) p(p(+(x,x299))) = x + x299 >= x + x299 = p(p(+(x299,x))) p(+(x,p(x299))) = x + x299 >= x + x299 = p(p(+(x299,x))) p(+(x299,p(x))) = x + x299 >= x + x299 = p(p(+(x,x299))) p(p(+(x,x299))) = x + x299 >= x + x299 = p(p(+(x299,x))) p(+(x,p(x299))) = x + x299 >= x + x299 = p(+(p(x299),x)) p(+(p(x299),x)) = x + x299 >= x + x299 = p(p(+(x299,x))) +(s(p(x300)),y) = x300 + y >= x300 + y = +(x300,y) +(s(p(x300)),y) = x300 + y >= x300 + y = s(+(p(x300),y)) s(+(p(x300),y)) = x300 + y >= x300 + y = s(p(+(x300,y))) s(p(+(x300,y))) = x300 + y >= x300 + y = +(x300,y) +(x,s(p(x301))) = x + x301 >= x + x301 = +(x,x301) +(x,s(p(x301))) = x + x301 >= x + x301 = s(+(p(x301),x)) +(x,x301) = x + x301 >= x + x301 = +(x301,x) s(+(p(x301),x)) = x + x301 >= x + x301 = s(p(+(x301,x))) s(p(+(x301,x))) = x + x301 >= x + x301 = +(x301,x) p(s(p(x302))) = x302 >= x302 = p(x302) p(s(p(x302))) = x302 >= x302 = p(x302) +(p(s(x303)),y) = x303 + y >= x303 + y = +(x303,y) +(p(s(x303)),y) = x303 + y >= x303 + y = p(+(s(x303),y)) p(+(s(x303),y)) = x303 + y >= x303 + y = p(s(+(x303,y))) p(s(+(x303,y))) = x303 + y >= x303 + y = +(x303,y) +(x,p(s(x304))) = x + x304 >= x + x304 = +(x,x304) +(x,p(s(x304))) = x + x304 >= x + x304 = p(+(s(x304),x)) +(x,x304) = x + x304 >= x + x304 = +(x304,x) p(+(s(x304),x)) = x + x304 >= x + x304 = p(s(+(x304,x))) p(s(+(x304,x))) = x + x304 >= x + x304 = +(x304,x) s(p(s(x305))) = x305 >= x305 = s(x305) s(p(s(x305))) = x305 >= x305 = s(x305) +(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(x268),y) -> s(+(x268,y)) +(s(x268),y) -> +(y,s(x268)) +(y,s(x268)) -> s(+(x268,y)) +(s(x270),0()) -> s(+(x270,0())) +(s(x272),s(y)) -> s(+(x272,s(y))) +(s(x272),s(y)) -> s(+(y,s(x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(+(s(y),x272)) s(+(s(y),x272)) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(+(s(x272),y)) s(+(s(x272),y)) -> s(s(+(x272,y))) +(s(x274),p(y)) -> s(+(x274,p(y))) +(s(x274),p(y)) -> p(+(y,s(x274))) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) p(s(+(y,x274))) -> +(y,x274) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) s(+(p(y),x274)) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) p(s(+(y,x274))) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) s(+(p(y),x274)) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> s(p(+(x274,y))) s(p(+(x274,y))) -> +(x274,y) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> s(p(+(x274,y))) s(p(+(x274,y))) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) s(+(x274,p(y))) -> s(p(+(y,x274))) s(p(+(y,x274))) -> +(y,x274) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) p(s(+(x274,y))) -> +(x274,y) +(x,s(x277)) -> s(+(x277,x)) +(x,s(x277)) -> +(s(x277),x) +(s(x277),x) -> s(+(x277,x)) +(0(),s(x279)) -> s(+(x279,0())) +(s(x),s(x281)) -> s(+(x281,s(x))) +(s(x),s(x281)) -> s(+(x,s(x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(+(s(x),x281)) s(+(s(x),x281)) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(+(s(x281),x)) s(+(s(x281),x)) -> s(s(+(x281,x))) +(p(x),s(x283)) -> s(+(x283,p(x))) +(p(x),s(x283)) -> p(+(x,s(x283))) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) p(s(+(x,x283))) -> +(x,x283) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) s(+(p(x),x283)) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) p(s(+(x,x283))) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) s(+(p(x),x283)) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> s(p(+(x283,x))) s(p(+(x283,x))) -> +(x283,x) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> s(p(+(x283,x))) s(p(+(x283,x))) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) s(+(x283,p(x))) -> s(p(+(x,x283))) s(p(+(x,x283))) -> +(x,x283) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) p(s(+(x283,x))) -> +(x283,x) +(p(x284),y) -> p(+(x284,y)) +(p(x284),y) -> +(y,p(x284)) +(y,p(x284)) -> p(+(x284,y)) +(p(x286),0()) -> p(+(x286,0())) +(p(x288),s(y)) -> p(+(x288,s(y))) +(p(x288),s(y)) -> s(+(y,p(x288))) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> s(p(+(y,x288))) s(p(+(y,x288))) -> +(y,x288) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> s(p(+(y,x288))) s(p(+(y,x288))) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) p(s(+(x288,y))) -> +(x288,y) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) p(s(+(x288,y))) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) s(+(p(x288),y)) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> +(y,x288) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) s(+(p(x288),y)) -> s(p(+(x288,y))) s(p(+(x288,y))) -> +(x288,y) +(p(x290),p(y)) -> p(+(x290,p(y))) +(p(x290),p(y)) -> p(+(y,p(x290))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(+(p(y),x290)) p(+(p(y),x290)) -> p(p(+(y,x290))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(p(+(x290,y))) p(+(x290,p(y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(+(p(x290),y)) p(+(p(x290),y)) -> p(p(+(x290,y))) +(x,p(x293)) -> p(+(x293,x)) +(x,p(x293)) -> +(p(x293),x) +(p(x293),x) -> p(+(x293,x)) +(0(),p(x295)) -> p(+(x295,0())) +(s(x),p(x297)) -> p(+(x297,s(x))) +(s(x),p(x297)) -> s(+(x,p(x297))) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> s(p(+(x,x297))) s(p(+(x,x297))) -> +(x,x297) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> s(p(+(x,x297))) s(p(+(x,x297))) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) p(s(+(x297,x))) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) s(+(p(x297),x)) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> +(x,x297) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) s(+(p(x297),x)) -> s(p(+(x297,x))) s(p(+(x297,x))) -> +(x297,x) +(p(x),p(x299)) -> p(+(x299,p(x))) +(p(x),p(x299)) -> p(+(x,p(x299))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(+(p(x),x299)) p(+(p(x),x299)) -> p(p(+(x,x299))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(p(+(x299,x))) p(+(x299,p(x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(+(p(x299),x)) p(+(p(x299),x)) -> p(p(+(x299,x))) +(s(p(x300)),y) -> +(x300,y) +(s(p(x300)),y) -> s(+(p(x300),y)) s(+(p(x300),y)) -> s(p(+(x300,y))) s(p(+(x300,y))) -> +(x300,y) +(x,s(p(x301))) -> +(x,x301) +(x,s(p(x301))) -> s(+(p(x301),x)) +(x,x301) -> +(x301,x) s(+(p(x301),x)) -> s(p(+(x301,x))) s(p(+(x301,x))) -> +(x301,x) p(s(p(x302))) -> p(x302) p(s(p(x302))) -> p(x302) +(p(s(x303)),y) -> +(x303,y) +(p(s(x303)),y) -> p(+(s(x303),y)) p(+(s(x303),y)) -> p(s(+(x303,y))) p(s(+(x303,y))) -> +(x303,y) +(x,p(s(x304))) -> +(x,x304) +(x,p(s(x304))) -> p(+(s(x304),x)) +(x,x304) -> +(x304,x) p(+(s(x304),x)) -> p(s(+(x304,x))) p(s(+(x304,x))) -> +(x304,x) s(p(s(x305))) -> s(x305) s(p(s(x305))) -> s(x305) 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(x268),y) = 4x268 + 4y + 7 >= 4x268 + 4y + 7 = s(+(x268,y)) +(s(x268),y) = 4x268 + 4y + 7 >= 4x268 + 4y + 7 = +(y,s(x268)) +(y,s(x268)) = 4x268 + 4y + 7 >= 4x268 + 4y + 7 = s(+(x268,y)) +(s(x270),0()) = 4x270 + 11 >= 4x270 + 11 = s(+(x270,0())) +(s(x272),s(y)) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(+(x272,s(y))) +(s(x272),s(y)) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(+(y,s(x272))) s(+(x272,s(y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(+(y,s(x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) s(s(+(x272,y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(+(x272,s(y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(+(s(y),x272)) s(+(s(y),x272)) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(+(y,s(x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) s(s(+(x272,y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(+(x272,s(y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(s(+(y,x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) s(+(y,s(x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) s(+(x272,s(y))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(y,x272))) s(s(+(y,x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) s(+(y,s(x272))) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(+(s(x272),y)) s(+(s(x272),y)) = 4x272 + 4y + 7 >= 4x272 + 4y + 7 = s(s(+(x272,y))) +(s(x274),p(y)) = 4x274 + 4y + 11 >= 4x274 + 4y + 11 = s(+(x274,p(y))) +(s(x274),p(y)) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = p(+(y,s(x274))) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(y,x274))) p(s(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) +(x274,y) = 4x274 + 4y + 7 >= 4x274 + 4y + 7 = +(y,x274) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 11 = s(+(p(y),x274)) s(+(p(y),x274)) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(y,x274))) p(s(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 11 = s(+(p(y),x274)) s(+(p(y),x274)) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) +(x274,y) = 4x274 + 4y + 7 >= 4x274 + 4y + 7 = +(y,x274) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = s(p(+(x274,y))) s(p(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = s(p(+(x274,y))) s(p(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(+(s(x274),y)) p(+(s(x274),y)) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) +(y,x274) = 4x274 + 4y + 7 >= 4x274 + 4y + 7 = +(x274,y) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) s(+(x274,p(y))) = 4x274 + 4y + 11 >= 4x274 + 4y + 8 = s(p(+(y,x274))) s(p(+(y,x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(y,x274) +(y,x274) = 4x274 + 4y + 7 >= 4x274 + 4y + 7 = +(x274,y) p(+(y,s(x274))) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(+(s(x274),y)) p(+(s(x274),y)) = 4x274 + 4y + 8 >= 4x274 + 4y + 8 = p(s(+(x274,y))) p(s(+(x274,y))) = 4x274 + 4y + 8 >= 4x274 + 4y + 7 = +(x274,y) +(x,s(x277)) = 4x + 4x277 + 7 >= 4x + 4x277 + 7 = s(+(x277,x)) +(x,s(x277)) = 4x + 4x277 + 7 >= 4x + 4x277 + 7 = +(s(x277),x) +(s(x277),x) = 4x + 4x277 + 7 >= 4x + 4x277 + 7 = s(+(x277,x)) +(0(),s(x279)) = 4x279 + 11 >= 4x279 + 11 = s(+(x279,0())) +(s(x),s(x281)) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(+(x281,s(x))) +(s(x),s(x281)) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(+(x,s(x281))) s(+(x281,s(x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(+(x,s(x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) s(s(+(x281,x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(+(x281,s(x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(+(s(x),x281)) s(+(s(x),x281)) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(+(x,s(x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) s(s(+(x281,x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(+(x281,s(x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(s(+(x,x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) s(+(x,s(x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) s(+(x281,s(x))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x,x281))) s(s(+(x,x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) s(+(x,s(x281))) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(+(s(x281),x)) s(+(s(x281),x)) = 4x + 4x281 + 7 >= 4x + 4x281 + 7 = s(s(+(x281,x))) +(p(x),s(x283)) = 4x + 4x283 + 11 >= 4x + 4x283 + 11 = s(+(x283,p(x))) +(p(x),s(x283)) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = p(+(x,s(x283))) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x,x283))) p(s(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) +(x283,x) = 4x + 4x283 + 7 >= 4x + 4x283 + 7 = +(x,x283) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 11 = s(+(p(x),x283)) s(+(p(x),x283)) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x,x283))) p(s(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 11 = s(+(p(x),x283)) s(+(p(x),x283)) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) +(x283,x) = 4x + 4x283 + 7 >= 4x + 4x283 + 7 = +(x,x283) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = s(p(+(x283,x))) s(p(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = s(p(+(x283,x))) s(p(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(+(s(x283),x)) p(+(s(x283),x)) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) +(x,x283) = 4x + 4x283 + 7 >= 4x + 4x283 + 7 = +(x283,x) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) s(+(x283,p(x))) = 4x + 4x283 + 11 >= 4x + 4x283 + 8 = s(p(+(x,x283))) s(p(+(x,x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x,x283) +(x,x283) = 4x + 4x283 + 7 >= 4x + 4x283 + 7 = +(x283,x) p(+(x,s(x283))) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(+(s(x283),x)) p(+(s(x283),x)) = 4x + 4x283 + 8 >= 4x + 4x283 + 8 = p(s(+(x283,x))) p(s(+(x283,x))) = 4x + 4x283 + 8 >= 4x + 4x283 + 7 = +(x283,x) +(p(x284),y) = 4x284 + 4y + 11 >= 4x284 + 4y + 8 = p(+(x284,y)) +(p(x284),y) = 4x284 + 4y + 11 >= 4x284 + 4y + 11 = +(y,p(x284)) +(y,p(x284)) = 4x284 + 4y + 11 >= 4x284 + 4y + 8 = p(+(x284,y)) +(p(x286),0()) = 4x286 + 15 >= 4x286 + 12 = p(+(x286,0())) +(p(x288),s(y)) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = p(+(x288,s(y))) +(p(x288),s(y)) = 4x288 + 4y + 11 >= 4x288 + 4y + 11 = s(+(y,p(x288))) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = s(p(+(y,x288))) s(p(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) +(x288,y) = 4x288 + 4y + 7 >= 4x288 + 4y + 7 = +(y,x288) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(+(s(y),x288)) p(+(s(y),x288)) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = s(p(+(y,x288))) s(p(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(+(s(y),x288)) p(+(s(y),x288)) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) +(x288,y) = 4x288 + 4y + 7 >= 4x288 + 4y + 7 = +(y,x288) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(x288,y))) p(s(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(x288,y))) p(s(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 11 = s(+(p(x288),y)) s(+(p(x288),y)) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) +(y,x288) = 4x288 + 4y + 7 >= 4x288 + 4y + 7 = +(x288,y) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) p(+(x288,s(y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 8 = p(s(+(y,x288))) p(s(+(y,x288))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(y,x288) +(y,x288) = 4x288 + 4y + 7 >= 4x288 + 4y + 7 = +(x288,y) s(+(y,p(x288))) = 4x288 + 4y + 11 >= 4x288 + 4y + 11 = s(+(p(x288),y)) s(+(p(x288),y)) = 4x288 + 4y + 11 >= 4x288 + 4y + 8 = s(p(+(x288,y))) s(p(+(x288,y))) = 4x288 + 4y + 8 >= 4x288 + 4y + 7 = +(x288,y) +(p(x290),p(y)) = 4x290 + 4y + 15 >= 4x290 + 4y + 12 = p(+(x290,p(y))) +(p(x290),p(y)) = 4x290 + 4y + 15 >= 4x290 + 4y + 12 = p(+(y,p(x290))) p(+(x290,p(y))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(+(y,p(x290))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(x290,y))) p(p(+(x290,y))) = 4x290 + 4y + 9 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(+(x290,p(y))) = 4x290 + 4y + 12 >= 4x290 + 4y + 12 = p(+(p(y),x290)) p(+(p(y),x290)) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(+(y,p(x290))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(x290,y))) p(p(+(x290,y))) = 4x290 + 4y + 9 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(+(x290,p(y))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(p(+(y,x290))) = 4x290 + 4y + 9 >= 4x290 + 4y + 9 = p(p(+(x290,y))) p(+(y,p(x290))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(x290,y))) p(+(x290,p(y))) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(y,x290))) p(p(+(y,x290))) = 4x290 + 4y + 9 >= 4x290 + 4y + 9 = p(p(+(x290,y))) p(+(y,p(x290))) = 4x290 + 4y + 12 >= 4x290 + 4y + 12 = p(+(p(x290),y)) p(+(p(x290),y)) = 4x290 + 4y + 12 >= 4x290 + 4y + 9 = p(p(+(x290,y))) +(x,p(x293)) = 4x + 4x293 + 11 >= 4x + 4x293 + 8 = p(+(x293,x)) +(x,p(x293)) = 4x + 4x293 + 11 >= 4x + 4x293 + 11 = +(p(x293),x) +(p(x293),x) = 4x + 4x293 + 11 >= 4x + 4x293 + 8 = p(+(x293,x)) +(0(),p(x295)) = 4x295 + 15 >= 4x295 + 12 = p(+(x295,0())) +(s(x),p(x297)) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = p(+(x297,s(x))) +(s(x),p(x297)) = 4x + 4x297 + 11 >= 4x + 4x297 + 11 = s(+(x,p(x297))) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = s(p(+(x,x297))) s(p(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) +(x297,x) = 4x + 4x297 + 7 >= 4x + 4x297 + 7 = +(x,x297) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(+(s(x),x297)) p(+(s(x),x297)) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = s(p(+(x,x297))) s(p(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(+(s(x),x297)) p(+(s(x),x297)) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) +(x297,x) = 4x + 4x297 + 7 >= 4x + 4x297 + 7 = +(x,x297) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x297,x))) p(s(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x297,x))) p(s(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 11 = s(+(p(x297),x)) s(+(p(x297),x)) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) +(x,x297) = 4x + 4x297 + 7 >= 4x + 4x297 + 7 = +(x297,x) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) p(+(x297,s(x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 8 = p(s(+(x,x297))) p(s(+(x,x297))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x,x297) +(x,x297) = 4x + 4x297 + 7 >= 4x + 4x297 + 7 = +(x297,x) s(+(x,p(x297))) = 4x + 4x297 + 11 >= 4x + 4x297 + 11 = s(+(p(x297),x)) s(+(p(x297),x)) = 4x + 4x297 + 11 >= 4x + 4x297 + 8 = s(p(+(x297,x))) s(p(+(x297,x))) = 4x + 4x297 + 8 >= 4x + 4x297 + 7 = +(x297,x) +(p(x),p(x299)) = 4x + 4x299 + 15 >= 4x + 4x299 + 12 = p(+(x299,p(x))) +(p(x),p(x299)) = 4x + 4x299 + 15 >= 4x + 4x299 + 12 = p(+(x,p(x299))) p(+(x299,p(x))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(+(x,p(x299))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x299,x))) p(p(+(x299,x))) = 4x + 4x299 + 9 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(+(x299,p(x))) = 4x + 4x299 + 12 >= 4x + 4x299 + 12 = p(+(p(x),x299)) p(+(p(x),x299)) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(+(x,p(x299))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x299,x))) p(p(+(x299,x))) = 4x + 4x299 + 9 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(+(x299,p(x))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(p(+(x,x299))) = 4x + 4x299 + 9 >= 4x + 4x299 + 9 = p(p(+(x299,x))) p(+(x,p(x299))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x299,x))) p(+(x299,p(x))) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x,x299))) p(p(+(x,x299))) = 4x + 4x299 + 9 >= 4x + 4x299 + 9 = p(p(+(x299,x))) p(+(x,p(x299))) = 4x + 4x299 + 12 >= 4x + 4x299 + 12 = p(+(p(x299),x)) p(+(p(x299),x)) = 4x + 4x299 + 12 >= 4x + 4x299 + 9 = p(p(+(x299,x))) +(s(p(x300)),y) = 4x300 + 4y + 11 >= 4x300 + 4y + 7 = +(x300,y) +(s(p(x300)),y) = 4x300 + 4y + 11 >= 4x300 + 4y + 11 = s(+(p(x300),y)) s(+(p(x300),y)) = 4x300 + 4y + 11 >= 4x300 + 4y + 8 = s(p(+(x300,y))) s(p(+(x300,y))) = 4x300 + 4y + 8 >= 4x300 + 4y + 7 = +(x300,y) +(x,s(p(x301))) = 4x + 4x301 + 11 >= 4x + 4x301 + 7 = +(x,x301) +(x,s(p(x301))) = 4x + 4x301 + 11 >= 4x + 4x301 + 11 = s(+(p(x301),x)) +(x,x301) = 4x + 4x301 + 7 >= 4x + 4x301 + 7 = +(x301,x) s(+(p(x301),x)) = 4x + 4x301 + 11 >= 4x + 4x301 + 8 = s(p(+(x301,x))) s(p(+(x301,x))) = 4x + 4x301 + 8 >= 4x + 4x301 + 7 = +(x301,x) p(s(p(x302))) = x302 + 2 >= x302 + 1 = p(x302) p(s(p(x302))) = x302 + 2 >= x302 + 1 = p(x302) +(p(s(x303)),y) = 4x303 + 4y + 11 >= 4x303 + 4y + 7 = +(x303,y) +(p(s(x303)),y) = 4x303 + 4y + 11 >= 4x303 + 4y + 8 = p(+(s(x303),y)) p(+(s(x303),y)) = 4x303 + 4y + 8 >= 4x303 + 4y + 8 = p(s(+(x303,y))) p(s(+(x303,y))) = 4x303 + 4y + 8 >= 4x303 + 4y + 7 = +(x303,y) +(x,p(s(x304))) = 4x + 4x304 + 11 >= 4x + 4x304 + 7 = +(x,x304) +(x,p(s(x304))) = 4x + 4x304 + 11 >= 4x + 4x304 + 8 = p(+(s(x304),x)) +(x,x304) = 4x + 4x304 + 7 >= 4x + 4x304 + 7 = +(x304,x) p(+(s(x304),x)) = 4x + 4x304 + 8 >= 4x + 4x304 + 8 = p(s(+(x304,x))) p(s(+(x304,x))) = 4x + 4x304 + 8 >= 4x + 4x304 + 7 = +(x304,x) s(p(s(x305))) = x305 + 1 >= x305 = s(x305) s(p(s(x305))) = x305 + 1 >= x305 = s(x305) +(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(x268),y) -> s(+(x268,y)) +(s(x268),y) -> +(y,s(x268)) +(y,s(x268)) -> s(+(x268,y)) +(s(x270),0()) -> s(+(x270,0())) +(s(x272),s(y)) -> s(+(x272,s(y))) +(s(x272),s(y)) -> s(+(y,s(x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(+(s(y),x272)) s(+(s(y),x272)) -> s(s(+(y,x272))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(s(+(x272,y))) s(+(x272,s(y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(+(s(x272),y)) s(+(s(x272),y)) -> s(s(+(x272,y))) +(s(x274),p(y)) -> s(+(x274,p(y))) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) p(+(y,s(x274))) -> p(s(+(x274,y))) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) p(+(y,s(x274))) -> p(s(+(x274,y))) p(s(+(x274,y))) -> p(s(+(y,x274))) s(+(x274,p(y))) -> s(+(p(y),x274)) p(+(y,s(x274))) -> p(s(+(x274,y))) +(x274,y) -> +(y,x274) s(p(+(y,x274))) -> s(p(+(x274,y))) p(+(y,s(x274))) -> p(s(+(x274,y))) s(p(+(y,x274))) -> s(p(+(x274,y))) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(s(+(x274,y))) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) p(+(s(x274),y)) -> p(s(+(x274,y))) +(x,s(x277)) -> s(+(x277,x)) +(x,s(x277)) -> +(s(x277),x) +(s(x277),x) -> s(+(x277,x)) +(0(),s(x279)) -> s(+(x279,0())) +(s(x),s(x281)) -> s(+(x281,s(x))) +(s(x),s(x281)) -> s(+(x,s(x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(+(s(x),x281)) s(+(s(x),x281)) -> s(s(+(x,x281))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(s(+(x281,x))) s(+(x281,s(x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(+(s(x281),x)) s(+(s(x281),x)) -> s(s(+(x281,x))) +(p(x),s(x283)) -> s(+(x283,p(x))) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) p(+(x,s(x283))) -> p(s(+(x283,x))) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) p(+(x,s(x283))) -> p(s(+(x283,x))) p(s(+(x283,x))) -> p(s(+(x,x283))) s(+(x283,p(x))) -> s(+(p(x),x283)) p(+(x,s(x283))) -> p(s(+(x283,x))) +(x283,x) -> +(x,x283) s(p(+(x,x283))) -> s(p(+(x283,x))) p(+(x,s(x283))) -> p(s(+(x283,x))) s(p(+(x,x283))) -> s(p(+(x283,x))) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(s(+(x283,x))) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) p(+(s(x283),x)) -> p(s(+(x283,x))) +(p(x284),y) -> +(y,p(x284)) +(p(x288),s(y)) -> s(+(y,p(x288))) p(+(x288,s(y))) -> p(s(+(y,x288))) s(p(+(x288,y))) -> s(p(+(y,x288))) p(+(x288,s(y))) -> p(s(+(y,x288))) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) s(p(+(x288,y))) -> s(p(+(y,x288))) p(+(x288,s(y))) -> p(+(s(y),x288)) p(+(s(y),x288)) -> p(s(+(y,x288))) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) p(+(x288,s(y))) -> p(s(+(y,x288))) p(s(+(y,x288))) -> p(s(+(x288,y))) s(+(y,p(x288))) -> s(+(p(x288),y)) p(+(x288,s(y))) -> p(s(+(y,x288))) +(y,x288) -> +(x288,y) p(+(x288,s(y))) -> p(s(+(y,x288))) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(+(p(y),x290)) p(p(+(x290,y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(+(p(x290),y)) +(x,p(x293)) -> +(p(x293),x) +(s(x),p(x297)) -> s(+(x,p(x297))) p(+(x297,s(x))) -> p(s(+(x,x297))) s(p(+(x297,x))) -> s(p(+(x,x297))) p(+(x297,s(x))) -> p(s(+(x,x297))) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) s(p(+(x297,x))) -> s(p(+(x,x297))) p(+(x297,s(x))) -> p(+(s(x),x297)) p(+(s(x),x297)) -> p(s(+(x,x297))) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) p(+(x297,s(x))) -> p(s(+(x,x297))) p(s(+(x,x297))) -> p(s(+(x297,x))) s(+(x,p(x297))) -> s(+(p(x297),x)) p(+(x297,s(x))) -> p(s(+(x,x297))) +(x,x297) -> +(x297,x) p(+(x297,s(x))) -> p(s(+(x,x297))) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(+(p(x),x299)) p(p(+(x299,x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(+(p(x299),x)) +(s(p(x300)),y) -> s(+(p(x300),y)) +(x,s(p(x301))) -> s(+(p(x301),x)) +(x,x301) -> +(x301,x) p(+(s(x303),y)) -> p(s(+(x303,y))) +(x,x304) -> +(x304,x) p(+(s(x304),x)) -> p(s(+(x304,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(x268),y) = 2x268 + 2y + 2 >= 2x268 + 2y + 1 = s(+(x268,y)) +(s(x268),y) = 2x268 + 2y + 2 >= 2x268 + 2y + 2 = +(y,s(x268)) +(y,s(x268)) = 2x268 + 2y + 2 >= 2x268 + 2y + 1 = s(+(x268,y)) +(s(x270),0()) = 2x270 + 2 >= 2x270 + 1 = s(+(x270,0())) +(s(x272),s(y)) = 2x272 + 2y + 4 >= 2x272 + 2y + 3 = s(+(x272,s(y))) +(s(x272),s(y)) = 2x272 + 2y + 4 >= 2x272 + 2y + 3 = s(+(y,s(x272))) s(+(x272,s(y))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(+(y,s(x272))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(x272,y))) s(s(+(x272,y))) = 2x272 + 2y + 2 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(+(x272,s(y))) = 2x272 + 2y + 3 >= 2x272 + 2y + 3 = s(+(s(y),x272)) s(+(s(y),x272)) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(+(y,s(x272))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(x272,y))) s(s(+(x272,y))) = 2x272 + 2y + 2 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(+(x272,s(y))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(s(+(y,x272))) = 2x272 + 2y + 2 >= 2x272 + 2y + 2 = s(s(+(x272,y))) s(+(y,s(x272))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(x272,y))) s(+(x272,s(y))) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(y,x272))) s(s(+(y,x272))) = 2x272 + 2y + 2 >= 2x272 + 2y + 2 = s(s(+(x272,y))) s(+(y,s(x272))) = 2x272 + 2y + 3 >= 2x272 + 2y + 3 = s(+(s(x272),y)) s(+(s(x272),y)) = 2x272 + 2y + 3 >= 2x272 + 2y + 2 = s(s(+(x272,y))) +(s(x274),p(y)) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = s(+(x274,p(y))) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) p(s(+(x274,y))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = p(s(+(y,x274))) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) +(x274,y) = 2x274 + 2y >= 2x274 + 2y = +(y,x274) s(+(x274,p(y))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = s(+(p(y),x274)) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) p(s(+(x274,y))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = p(s(+(y,x274))) s(+(x274,p(y))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = s(+(p(y),x274)) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) +(x274,y) = 2x274 + 2y >= 2x274 + 2y = +(y,x274) s(p(+(y,x274))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = s(p(+(x274,y))) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) s(p(+(y,x274))) = 2x274 + 2y + 1 >= 2x274 + 2y + 1 = s(p(+(x274,y))) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 2 = p(+(s(x274),y)) p(+(s(x274),y)) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) +(y,x274) = 2x274 + 2y >= 2x274 + 2y = +(x274,y) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) +(y,x274) = 2x274 + 2y >= 2x274 + 2y = +(x274,y) p(+(y,s(x274))) = 2x274 + 2y + 2 >= 2x274 + 2y + 2 = p(+(s(x274),y)) p(+(s(x274),y)) = 2x274 + 2y + 2 >= 2x274 + 2y + 1 = p(s(+(x274,y))) +(x,s(x277)) = 2x + 2x277 + 2 >= 2x + 2x277 + 1 = s(+(x277,x)) +(x,s(x277)) = 2x + 2x277 + 2 >= 2x + 2x277 + 2 = +(s(x277),x) +(s(x277),x) = 2x + 2x277 + 2 >= 2x + 2x277 + 1 = s(+(x277,x)) +(0(),s(x279)) = 2x279 + 2 >= 2x279 + 1 = s(+(x279,0())) +(s(x),s(x281)) = 2x + 2x281 + 4 >= 2x + 2x281 + 3 = s(+(x281,s(x))) +(s(x),s(x281)) = 2x + 2x281 + 4 >= 2x + 2x281 + 3 = s(+(x,s(x281))) s(+(x281,s(x))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(+(x,s(x281))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x281,x))) s(s(+(x281,x))) = 2x + 2x281 + 2 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(+(x281,s(x))) = 2x + 2x281 + 3 >= 2x + 2x281 + 3 = s(+(s(x),x281)) s(+(s(x),x281)) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(+(x,s(x281))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x281,x))) s(s(+(x281,x))) = 2x + 2x281 + 2 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(+(x281,s(x))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(s(+(x,x281))) = 2x + 2x281 + 2 >= 2x + 2x281 + 2 = s(s(+(x281,x))) s(+(x,s(x281))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x281,x))) s(+(x281,s(x))) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x,x281))) s(s(+(x,x281))) = 2x + 2x281 + 2 >= 2x + 2x281 + 2 = s(s(+(x281,x))) s(+(x,s(x281))) = 2x + 2x281 + 3 >= 2x + 2x281 + 3 = s(+(s(x281),x)) s(+(s(x281),x)) = 2x + 2x281 + 3 >= 2x + 2x281 + 2 = s(s(+(x281,x))) +(p(x),s(x283)) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = s(+(x283,p(x))) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) p(s(+(x283,x))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = p(s(+(x,x283))) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) +(x283,x) = 2x + 2x283 >= 2x + 2x283 = +(x,x283) s(+(x283,p(x))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = s(+(p(x),x283)) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) p(s(+(x283,x))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = p(s(+(x,x283))) s(+(x283,p(x))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = s(+(p(x),x283)) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) +(x283,x) = 2x + 2x283 >= 2x + 2x283 = +(x,x283) s(p(+(x,x283))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = s(p(+(x283,x))) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) s(p(+(x,x283))) = 2x + 2x283 + 1 >= 2x + 2x283 + 1 = s(p(+(x283,x))) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 2 = p(+(s(x283),x)) p(+(s(x283),x)) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) +(x,x283) = 2x + 2x283 >= 2x + 2x283 = +(x283,x) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) +(x,x283) = 2x + 2x283 >= 2x + 2x283 = +(x283,x) p(+(x,s(x283))) = 2x + 2x283 + 2 >= 2x + 2x283 + 2 = p(+(s(x283),x)) p(+(s(x283),x)) = 2x + 2x283 + 2 >= 2x + 2x283 + 1 = p(s(+(x283,x))) +(p(x284),y) = 2x284 + 2y >= 2x284 + 2y = +(y,p(x284)) +(p(x288),s(y)) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = s(+(y,p(x288))) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) s(p(+(x288,y))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = s(p(+(y,x288))) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) +(x288,y) = 2x288 + 2y >= 2x288 + 2y = +(y,x288) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 2 = p(+(s(y),x288)) p(+(s(y),x288)) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) s(p(+(x288,y))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = s(p(+(y,x288))) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 2 = p(+(s(y),x288)) p(+(s(y),x288)) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) +(x288,y) = 2x288 + 2y >= 2x288 + 2y = +(y,x288) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) p(s(+(y,x288))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = p(s(+(x288,y))) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) p(s(+(y,x288))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = p(s(+(x288,y))) s(+(y,p(x288))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = s(+(p(x288),y)) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) +(y,x288) = 2x288 + 2y >= 2x288 + 2y = +(x288,y) p(+(x288,s(y))) = 2x288 + 2y + 2 >= 2x288 + 2y + 1 = p(s(+(y,x288))) +(y,x288) = 2x288 + 2y >= 2x288 + 2y = +(x288,y) s(+(y,p(x288))) = 2x288 + 2y + 1 >= 2x288 + 2y + 1 = s(+(p(x288),y)) p(p(+(x290,y))) = 2x290 + 2y >= 2x290 + 2y = p(p(+(y,x290))) p(+(x290,p(y))) = 2x290 + 2y >= 2x290 + 2y = p(+(p(y),x290)) p(p(+(x290,y))) = 2x290 + 2y >= 2x290 + 2y = p(p(+(y,x290))) p(p(+(y,x290))) = 2x290 + 2y >= 2x290 + 2y = p(p(+(x290,y))) p(p(+(y,x290))) = 2x290 + 2y >= 2x290 + 2y = p(p(+(x290,y))) p(+(y,p(x290))) = 2x290 + 2y >= 2x290 + 2y = p(+(p(x290),y)) +(x,p(x293)) = 2x + 2x293 >= 2x + 2x293 = +(p(x293),x) +(s(x),p(x297)) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = s(+(x,p(x297))) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) s(p(+(x297,x))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = s(p(+(x,x297))) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) +(x297,x) = 2x + 2x297 >= 2x + 2x297 = +(x,x297) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 2 = p(+(s(x),x297)) p(+(s(x),x297)) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) s(p(+(x297,x))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = s(p(+(x,x297))) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 2 = p(+(s(x),x297)) p(+(s(x),x297)) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) +(x297,x) = 2x + 2x297 >= 2x + 2x297 = +(x,x297) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) p(s(+(x,x297))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = p(s(+(x297,x))) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) p(s(+(x,x297))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = p(s(+(x297,x))) s(+(x,p(x297))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = s(+(p(x297),x)) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) +(x,x297) = 2x + 2x297 >= 2x + 2x297 = +(x297,x) p(+(x297,s(x))) = 2x + 2x297 + 2 >= 2x + 2x297 + 1 = p(s(+(x,x297))) +(x,x297) = 2x + 2x297 >= 2x + 2x297 = +(x297,x) s(+(x,p(x297))) = 2x + 2x297 + 1 >= 2x + 2x297 + 1 = s(+(p(x297),x)) p(p(+(x299,x))) = 2x + 2x299 >= 2x + 2x299 = p(p(+(x,x299))) p(+(x299,p(x))) = 2x + 2x299 >= 2x + 2x299 = p(+(p(x),x299)) p(p(+(x299,x))) = 2x + 2x299 >= 2x + 2x299 = p(p(+(x,x299))) p(p(+(x,x299))) = 2x + 2x299 >= 2x + 2x299 = p(p(+(x299,x))) p(p(+(x,x299))) = 2x + 2x299 >= 2x + 2x299 = p(p(+(x299,x))) p(+(x,p(x299))) = 2x + 2x299 >= 2x + 2x299 = p(+(p(x299),x)) +(s(p(x300)),y) = 2x300 + 2y + 2 >= 2x300 + 2y + 1 = s(+(p(x300),y)) +(x,s(p(x301))) = 2x + 2x301 + 2 >= 2x + 2x301 + 1 = s(+(p(x301),x)) +(x,x301) = 2x + 2x301 >= 2x + 2x301 = +(x301,x) p(+(s(x303),y)) = 2x303 + 2y + 2 >= 2x303 + 2y + 1 = p(s(+(x303,y))) +(x,x304) = 2x + 2x304 >= 2x + 2x304 = +(x304,x) p(+(s(x304),x)) = 2x + 2x304 + 2 >= 2x + 2x304 + 1 = p(s(+(x304,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(x268),y) -> +(y,s(x268)) s(s(+(x272,y))) -> s(s(+(y,x272))) s(+(x272,s(y))) -> s(+(s(y),x272)) s(s(+(x272,y))) -> s(s(+(y,x272))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(s(+(y,x272))) -> s(s(+(x272,y))) s(+(y,s(x272))) -> s(+(s(x272),y)) p(s(+(x274,y))) -> p(s(+(y,x274))) +(x274,y) -> +(y,x274) s(+(x274,p(y))) -> s(+(p(y),x274)) p(s(+(x274,y))) -> p(s(+(y,x274))) s(+(x274,p(y))) -> s(+(p(y),x274)) +(x274,y) -> +(y,x274) s(p(+(y,x274))) -> s(p(+(x274,y))) s(p(+(y,x274))) -> s(p(+(x274,y))) p(+(y,s(x274))) -> p(+(s(x274),y)) +(y,x274) -> +(x274,y) +(y,x274) -> +(x274,y) p(+(y,s(x274))) -> p(+(s(x274),y)) +(x,s(x277)) -> +(s(x277),x) s(s(+(x281,x))) -> s(s(+(x,x281))) s(+(x281,s(x))) -> s(+(s(x),x281)) s(s(+(x281,x))) -> s(s(+(x,x281))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(s(+(x,x281))) -> s(s(+(x281,x))) s(+(x,s(x281))) -> s(+(s(x281),x)) p(s(+(x283,x))) -> p(s(+(x,x283))) +(x283,x) -> +(x,x283) s(+(x283,p(x))) -> s(+(p(x),x283)) p(s(+(x283,x))) -> p(s(+(x,x283))) s(+(x283,p(x))) -> s(+(p(x),x283)) +(x283,x) -> +(x,x283) s(p(+(x,x283))) -> s(p(+(x283,x))) s(p(+(x,x283))) -> s(p(+(x283,x))) p(+(x,s(x283))) -> p(+(s(x283),x)) +(x,x283) -> +(x283,x) +(x,x283) -> +(x283,x) p(+(x,s(x283))) -> p(+(s(x283),x)) +(p(x284),y) -> +(y,p(x284)) s(p(+(x288,y))) -> s(p(+(y,x288))) +(x288,y) -> +(y,x288) p(+(x288,s(y))) -> p(+(s(y),x288)) s(p(+(x288,y))) -> s(p(+(y,x288))) p(+(x288,s(y))) -> p(+(s(y),x288)) +(x288,y) -> +(y,x288) p(s(+(y,x288))) -> p(s(+(x288,y))) p(s(+(y,x288))) -> p(s(+(x288,y))) s(+(y,p(x288))) -> s(+(p(x288),y)) +(y,x288) -> +(x288,y) +(y,x288) -> +(x288,y) s(+(y,p(x288))) -> s(+(p(x288),y)) p(p(+(x290,y))) -> p(p(+(y,x290))) p(+(x290,p(y))) -> p(+(p(y),x290)) p(p(+(x290,y))) -> p(p(+(y,x290))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(p(+(y,x290))) -> p(p(+(x290,y))) p(+(y,p(x290))) -> p(+(p(x290),y)) +(x,p(x293)) -> +(p(x293),x) s(p(+(x297,x))) -> s(p(+(x,x297))) +(x297,x) -> +(x,x297) p(+(x297,s(x))) -> p(+(s(x),x297)) s(p(+(x297,x))) -> s(p(+(x,x297))) p(+(x297,s(x))) -> p(+(s(x),x297)) +(x297,x) -> +(x,x297) p(s(+(x,x297))) -> p(s(+(x297,x))) p(s(+(x,x297))) -> p(s(+(x297,x))) s(+(x,p(x297))) -> s(+(p(x297),x)) +(x,x297) -> +(x297,x) +(x,x297) -> +(x297,x) s(+(x,p(x297))) -> s(+(p(x297),x)) p(p(+(x299,x))) -> p(p(+(x,x299))) p(+(x299,p(x))) -> p(+(p(x),x299)) p(p(+(x299,x))) -> p(p(+(x,x299))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(p(+(x,x299))) -> p(p(+(x299,x))) p(+(x,p(x299))) -> p(+(p(x299),x)) +(x,x301) -> +(x301,x) +(x,x304) -> +(x304,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(+(x268,y)) <-3|[1,0]- +(s(x268),y) -0|[1,0]-> +(y,s(x268)) joins: +(y,s(x268)) -4|[1,0]-> s(+(x268,y)) peak: s(+(x270,0())) <-3|[1,0]- +(s(x270),0()) -2|[1,0]-> s(x270) joins: s(+(x270,0())) -2|0[0,0]-> s(x270) peak: s(+(x272,s(y))) <-3|[1,0]- +(s(x272),s(y)) -4|[1,0]-> s(+(y,s(x272))) joins: s(+(x272,s(y))) -4|0[0,0]-> s(s(+(y,x272))) s(+(y,s(x272))) -4|0[0,0]-> s(s(+(x272,y))) -0|0,0[0,0]-> s(s(+(y,x272))) peak: s(+(x274,p(y))) <-3|[1,0]- +(s(x274),p(y)) -6|[1,0]-> p(+(y,s(x274))) joins: s(+(x274,p(y))) -6|0[0,0]-> s(p(+(y,x274))) -7|[0,0]-> +(y,x274) p(+(y,s(x274))) -4|0[0,0]-> p(s(+(x274,y))) -0|0,0[0,0]-> p(s(+(y,x274))) -8|[0,0]-> +(y,x274) peak: s(+(x277,x)) <-4|[1,0]- +(x,s(x277)) -0|[1,0]-> +(s(x277),x) joins: +(s(x277),x) -3|[1,0]-> s(+(x277,x)) peak: s(+(x279,0())) <-4|[1,0]- +(0(),s(x279)) -1|[1,0]-> s(x279) joins: s(+(x279,0())) -2|0[0,0]-> s(x279) peak: s(+(x281,s(x))) <-4|[1,0]- +(s(x),s(x281)) -3|[1,0]-> s(+(x,s(x281))) joins: s(+(x281,s(x))) -4|0[0,0]-> s(s(+(x,x281))) s(+(x,s(x281))) -4|0[0,0]-> s(s(+(x281,x))) -0|0,0[0,0]-> s(s(+(x,x281))) peak: s(+(x283,p(x))) <-4|[1,0]- +(p(x),s(x283)) -5|[1,0]-> p(+(x,s(x283))) joins: s(+(x283,p(x))) -6|0[0,0]-> s(p(+(x,x283))) -7|[0,0]-> +(x,x283) p(+(x,s(x283))) -4|0[0,0]-> p(s(+(x283,x))) -0|0,0[0,0]-> p(s(+(x,x283))) -8|[0,0]-> +(x,x283) peak: p(+(x284,y)) <-5|[1,0]- +(p(x284),y) -0|[1,0]-> +(y,p(x284)) joins: +(y,p(x284)) -6|[1,0]-> p(+(x284,y)) peak: p(+(x286,0())) <-5|[1,0]- +(p(x286),0()) -2|[1,0]-> p(x286) joins: p(+(x286,0())) -2|0[0,0]-> p(x286) peak: p(+(x288,s(y))) <-5|[1,0]- +(p(x288),s(y)) -4|[1,0]-> s(+(y,p(x288))) joins: p(+(x288,s(y))) -4|0[0,0]-> p(s(+(y,x288))) -8|[0,0]-> +(y,x288) s(+(y,p(x288))) -6|0[0,0]-> s(p(+(x288,y))) -0|0,0[0,0]-> s(p(+(y,x288))) -7|[0,0]-> +(y,x288) peak: p(+(x290,p(y))) <-5|[1,0]- +(p(x290),p(y)) -6|[1,0]-> p(+(y,p(x290))) joins: p(+(x290,p(y))) -6|0[0,0]-> p(p(+(y,x290))) p(+(y,p(x290))) -6|0[0,0]-> p(p(+(x290,y))) -0|0,0[0,0]-> p(p(+(y,x290))) peak: p(+(x293,x)) <-6|[1,0]- +(x,p(x293)) -0|[1,0]-> +(p(x293),x) joins: +(p(x293),x) -5|[1,0]-> p(+(x293,x)) peak: p(+(x295,0())) <-6|[1,0]- +(0(),p(x295)) -1|[1,0]-> p(x295) joins: p(+(x295,0())) -2|0[0,0]-> p(x295) peak: p(+(x297,s(x))) <-6|[1,0]- +(s(x),p(x297)) -3|[1,0]-> s(+(x,p(x297))) joins: p(+(x297,s(x))) -4|0[0,0]-> p(s(+(x,x297))) -8|[0,0]-> +(x,x297) s(+(x,p(x297))) -6|0[0,0]-> s(p(+(x297,x))) -0|0,0[0,0]-> s(p(+(x,x297))) -7|[0,0]-> +(x,x297) peak: p(+(x299,p(x))) <-6|[1,0]- +(p(x),p(x299)) -5|[1,0]-> p(+(x,p(x299))) joins: p(+(x299,p(x))) -6|0[0,0]-> p(p(+(x,x299))) p(+(x,p(x299))) -6|0[0,0]-> p(p(+(x299,x))) -0|0,0[0,0]-> p(p(+(x,x299))) peak: +(x300,y) <-7|0[1,2]- +(s(p(x300)),y) -3|[1,0]-> s(+(p(x300),y)) joins: s(+(p(x300),y)) -5|0[0,0]-> s(p(+(x300,y))) -7|[0,0]-> +(x300,y) peak: +(x,x301) <-7|1[1,2]- +(x,s(p(x301))) -4|[1,0]-> s(+(p(x301),x)) joins: +(x,x301) -0|[0,0]-> +(x301,x) s(+(p(x301),x)) -5|0[0,0]-> s(p(+(x301,x))) -7|[0,0]-> +(x301,x) peak: p(x302) <-7|0[1,0]- p(s(p(x302))) -8|[1,0]-> p(x302) joins: peak: +(x303,y) <-8|0[1,2]- +(p(s(x303)),y) -5|[1,0]-> p(+(s(x303),y)) joins: p(+(s(x303),y)) -3|0[0,0]-> p(s(+(x303,y))) -8|[0,0]-> +(x303,y) peak: +(x,x304) <-8|1[1,2]- +(x,p(s(x304))) -6|[1,0]-> p(+(s(x304),x)) joins: +(x,x304) -0|[0,0]-> +(x304,x) p(+(s(x304),x)) -3|0[0,0]-> p(s(+(x304,x))) -8|[0,0]-> +(x304,x) peak: s(x305) <-8|0[1,0]- s(p(s(x305))) -7|[1,0]-> s(x305) joins: Qed