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