Problem:
 +(x,0()) -> x
 +(x,s(y)) -> s(+(x,y))
 +(x,p(y)) -> p(+(x,y))
 +(0(),y) -> y
 +(s(x),y) -> s(+(x,y))
 +(p(x),y) -> p(+(x,y))
 s(p(x)) -> x
 p(s(x)) -> x
 -(0()) -> 0()
 -(s(x)) -> p(-(x))
 -(p(x)) -> s(-(x))
 +(x,y) -> +(y,x)
 -(+(x,y)) -> +(-(x),-(y))

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 45
   0() <-0|[]- +(0(),0()) -3|[]-> 0()
   s(x) <-0|[]- +(s(x),0()) -4|[]-> s(+(x,0()))
   p(x) <-0|[]- +(p(x),0()) -5|[]-> p(+(x,0()))
   x <-0|[]- +(x,0()) -11|[]-> +(0(),x)
   -(x) <-0|0[]- -(+(x,0())) -12|[]-> +(-(x),-(0()))
   s(+(0(),x459)) <-1|[]- +(0(),s(x459)) -3|[]-> s(x459)
   s(+(s(x),x461)) <-1|[]- +(s(x),s(x461)) -4|[]-> s(+(x,s(x461)))
   s(+(p(x),x463)) <-1|[]- +(p(x),s(x463)) -5|[]-> p(+(x,s(x463)))
   s(+(x,x465)) <-1|[]- +(x,s(x465)) -11|[]-> +(s(x465),x)
   -(s(+(x,x467))) <-1|0[]- -(+(x,s(x467))) -12|[]-> +(-(x),-(s(x467)))
   p(+(0(),x469)) <-2|[]- +(0(),p(x469)) -3|[]-> p(x469)
   p(+(s(x),x471)) <-2|[]- +(s(x),p(x471)) -4|[]-> s(+(x,p(x471)))
   p(+(p(x),x473)) <-2|[]- +(p(x),p(x473)) -5|[]-> p(+(x,p(x473)))
   p(+(x,x475)) <-2|[]- +(x,p(x475)) -11|[]-> +(p(x475),x)
   -(p(+(x,x477))) <-2|0[]- -(+(x,p(x477))) -12|[]-> +(-(x),-(p(x477)))
   0() <-3|[]- +(0(),0()) -0|[]-> 0()
   s(y) <-3|[]- +(0(),s(y)) -1|[]-> s(+(0(),y))
   p(y) <-3|[]- +(0(),p(y)) -2|[]-> p(+(0(),y))
   y <-3|[]- +(0(),y) -11|[]-> +(y,0())
   -(y) <-3|0[]- -(+(0(),y)) -12|[]-> +(-(0()),-(y))
   s(+(x483,0())) <-4|[]- +(s(x483),0()) -0|[]-> s(x483)
   s(+(x485,s(y))) <-4|[]- +(s(x485),s(y)) -1|[]-> s(+(s(x485),y))
   s(+(x487,p(y))) <-4|[]- +(s(x487),p(y)) -2|[]-> p(+(s(x487),y))
   s(+(x489,y)) <-4|[]- +(s(x489),y) -11|[]-> +(y,s(x489))
   -(s(+(x491,y))) <-4|0[]- -(+(s(x491),y)) -12|[]-> +(-(s(x491)),-(y))
   p(+(x493,0())) <-5|[]- +(p(x493),0()) -0|[]-> p(x493)
   p(+(x495,s(y))) <-5|[]- +(p(x495),s(y)) -1|[]-> s(+(p(x495),y))
   p(+(x497,p(y))) <-5|[]- +(p(x497),p(y)) -2|[]-> p(+(p(x497),y))
   p(+(x499,y)) <-5|[]- +(p(x499),y) -11|[]-> +(y,p(x499))
   -(p(+(x501,y))) <-5|0[]- -(+(p(x501),y)) -12|[]-> +(-(p(x501)),-(y))
   +(x,x503) <-6|1[]- +(x,s(p(x503))) -1|[]-> s(+(x,p(x503)))
   +(x504,y) <-6|0[]- +(s(p(x504)),y) -4|[]-> s(+(p(x504),y))
   p(x505) <-6|0[]- p(s(p(x505))) -7|[]-> p(x505)
   -(x506) <-6|0[]- -(s(p(x506))) -9|[]-> p(-(p(x506)))
   +(x,x507) <-7|1[]- +(x,p(s(x507))) -2|[]-> p(+(x,s(x507)))
   +(x508,y) <-7|0[]- +(p(s(x508)),y) -5|[]-> p(+(s(x508),y))
   s(x509) <-7|0[]- s(p(s(x509))) -6|[]-> s(x509)
   -(x510) <-7|0[]- -(p(s(x510))) -10|[]-> s(-(s(x510)))
   +(0(),x) <-11|[]- +(x,0()) -0|[]-> x
   +(s(y),x) <-11|[]- +(x,s(y)) -1|[]-> s(+(x,y))
   +(p(y),x) <-11|[]- +(x,p(y)) -2|[]-> p(+(x,y))
   +(y,0()) <-11|[]- +(0(),y) -3|[]-> y
   +(y,s(x)) <-11|[]- +(s(x),y) -4|[]-> s(+(x,y))
   +(y,p(x)) <-11|[]- +(p(x),y) -5|[]-> p(+(x,y))
   -(+(y,x)) <-11|0[]- -(+(x,y)) -12|[]-> +(-(x),-(y))
  Shift Processor lab=left (dd) (force):
   strict:
    +(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)
    +(x,0()) -> x
    +(x,0()) -> +(0(),x)
    +(0(),x) -> x
    -(+(x,0())) -> -(x)
    -(+(x,0())) -> +(-(x),-(0()))
    +(-(x),-(0())) -> +(-(x),0())
    +(-(x),0()) -> -(x)
    +(0(),s(x459)) -> s(+(0(),x459))
    +(0(),s(x459)) -> s(x459)
    s(+(0(),x459)) -> s(x459)
    +(s(x),s(x461)) -> s(+(s(x),x461))
    +(s(x),s(x461)) -> s(+(x,s(x461)))
    s(+(s(x),x461)) -> s(s(+(x,x461)))
    s(+(x,s(x461))) -> s(s(+(x,x461)))
    +(p(x),s(x463)) -> s(+(p(x),x463))
    +(p(x),s(x463)) -> p(+(x,s(x463)))
    s(+(p(x),x463)) -> s(p(+(x,x463)))
    s(p(+(x,x463))) -> +(x,x463)
    p(+(x,s(x463))) -> p(s(+(x,x463)))
    p(s(+(x,x463))) -> +(x,x463)
    +(x,s(x465)) -> s(+(x,x465))
    +(x,s(x465)) -> +(s(x465),x)
    s(+(x,x465)) -> s(+(x465,x))
    +(s(x465),x) -> s(+(x465,x))
    -(+(x,s(x467))) -> -(s(+(x,x467)))
    -(+(x,s(x467))) -> +(-(x),-(s(x467)))
    -(s(+(x,x467))) -> p(-(+(x,x467)))
    p(-(+(x,x467))) -> p(+(-(x),-(x467)))
    +(-(x),-(s(x467))) -> +(-(x),p(-(x467)))
    +(-(x),p(-(x467))) -> p(+(-(x),-(x467)))
    +(0(),p(x469)) -> p(+(0(),x469))
    +(0(),p(x469)) -> p(x469)
    p(+(0(),x469)) -> p(x469)
    +(s(x),p(x471)) -> p(+(s(x),x471))
    +(s(x),p(x471)) -> s(+(x,p(x471)))
    p(+(s(x),x471)) -> p(s(+(x,x471)))
    p(s(+(x,x471))) -> +(x,x471)
    s(+(x,p(x471))) -> s(p(+(x,x471)))
    s(p(+(x,x471))) -> +(x,x471)
    +(p(x),p(x473)) -> p(+(p(x),x473))
    +(p(x),p(x473)) -> p(+(x,p(x473)))
    p(+(p(x),x473)) -> p(p(+(x,x473)))
    p(+(x,p(x473))) -> p(p(+(x,x473)))
    +(x,p(x475)) -> p(+(x,x475))
    +(x,p(x475)) -> +(p(x475),x)
    p(+(x,x475)) -> p(+(x475,x))
    +(p(x475),x) -> p(+(x475,x))
    -(+(x,p(x477))) -> -(p(+(x,x477)))
    -(+(x,p(x477))) -> +(-(x),-(p(x477)))
    -(p(+(x,x477))) -> s(-(+(x,x477)))
    s(-(+(x,x477))) -> s(+(-(x),-(x477)))
    +(-(x),-(p(x477))) -> +(-(x),s(-(x477)))
    +(-(x),s(-(x477))) -> s(+(-(x),-(x477)))
    +(0(),0()) -> 0()
    +(0(),0()) -> 0()
    +(0(),s(y)) -> s(y)
    +(0(),s(y)) -> s(+(0(),y))
    s(+(0(),y)) -> s(y)
    +(0(),p(y)) -> p(y)
    +(0(),p(y)) -> p(+(0(),y))
    p(+(0(),y)) -> p(y)
    +(0(),y) -> y
    +(0(),y) -> +(y,0())
    +(y,0()) -> y
    -(+(0(),y)) -> -(y)
    -(+(0(),y)) -> +(-(0()),-(y))
    +(-(0()),-(y)) -> +(0(),-(y))
    +(0(),-(y)) -> -(y)
    +(s(x483),0()) -> s(+(x483,0()))
    +(s(x483),0()) -> s(x483)
    s(+(x483,0())) -> s(x483)
    +(s(x485),s(y)) -> s(+(x485,s(y)))
    +(s(x485),s(y)) -> s(+(s(x485),y))
    s(+(x485,s(y))) -> s(s(+(x485,y)))
    s(+(s(x485),y)) -> s(s(+(x485,y)))
    +(s(x487),p(y)) -> s(+(x487,p(y)))
    +(s(x487),p(y)) -> p(+(s(x487),y))
    s(+(x487,p(y))) -> s(p(+(x487,y)))
    s(p(+(x487,y))) -> +(x487,y)
    p(+(s(x487),y)) -> p(s(+(x487,y)))
    p(s(+(x487,y))) -> +(x487,y)
    +(s(x489),y) -> s(+(x489,y))
    +(s(x489),y) -> +(y,s(x489))
    s(+(x489,y)) -> s(+(y,x489))
    +(y,s(x489)) -> s(+(y,x489))
    -(+(s(x491),y)) -> -(s(+(x491,y)))
    -(+(s(x491),y)) -> +(-(s(x491)),-(y))
    -(s(+(x491,y))) -> p(-(+(x491,y)))
    p(-(+(x491,y))) -> p(+(-(x491),-(y)))
    +(-(s(x491)),-(y)) -> +(p(-(x491)),-(y))
    +(p(-(x491)),-(y)) -> p(+(-(x491),-(y)))
    +(p(x493),0()) -> p(+(x493,0()))
    +(p(x493),0()) -> p(x493)
    p(+(x493,0())) -> p(x493)
    +(p(x495),s(y)) -> p(+(x495,s(y)))
    +(p(x495),s(y)) -> s(+(p(x495),y))
    p(+(x495,s(y))) -> p(s(+(x495,y)))
    p(s(+(x495,y))) -> +(x495,y)
    s(+(p(x495),y)) -> s(p(+(x495,y)))
    s(p(+(x495,y))) -> +(x495,y)
    +(p(x497),p(y)) -> p(+(x497,p(y)))
    +(p(x497),p(y)) -> p(+(p(x497),y))
    p(+(x497,p(y))) -> p(p(+(x497,y)))
    p(+(p(x497),y)) -> p(p(+(x497,y)))
    +(p(x499),y) -> p(+(x499,y))
    +(p(x499),y) -> +(y,p(x499))
    p(+(x499,y)) -> p(+(y,x499))
    +(y,p(x499)) -> p(+(y,x499))
    -(+(p(x501),y)) -> -(p(+(x501,y)))
    -(+(p(x501),y)) -> +(-(p(x501)),-(y))
    -(p(+(x501,y))) -> s(-(+(x501,y)))
    s(-(+(x501,y))) -> s(+(-(x501),-(y)))
    +(-(p(x501)),-(y)) -> +(s(-(x501)),-(y))
    +(s(-(x501)),-(y)) -> s(+(-(x501),-(y)))
    +(x,s(p(x503))) -> +(x,x503)
    +(x,s(p(x503))) -> s(+(x,p(x503)))
    s(+(x,p(x503))) -> s(p(+(x,x503)))
    s(p(+(x,x503))) -> +(x,x503)
    +(s(p(x504)),y) -> +(x504,y)
    +(s(p(x504)),y) -> s(+(p(x504),y))
    s(+(p(x504),y)) -> s(p(+(x504,y)))
    s(p(+(x504,y))) -> +(x504,y)
    p(s(p(x505))) -> p(x505)
    p(s(p(x505))) -> p(x505)
    -(s(p(x506))) -> -(x506)
    -(s(p(x506))) -> p(-(p(x506)))
    p(-(p(x506))) -> p(s(-(x506)))
    p(s(-(x506))) -> -(x506)
    +(x,p(s(x507))) -> +(x,x507)
    +(x,p(s(x507))) -> p(+(x,s(x507)))
    p(+(x,s(x507))) -> p(s(+(x,x507)))
    p(s(+(x,x507))) -> +(x,x507)
    +(p(s(x508)),y) -> +(x508,y)
    +(p(s(x508)),y) -> p(+(s(x508),y))
    p(+(s(x508),y)) -> p(s(+(x508,y)))
    p(s(+(x508,y))) -> +(x508,y)
    s(p(s(x509))) -> s(x509)
    s(p(s(x509))) -> s(x509)
    -(p(s(x510))) -> -(x510)
    -(p(s(x510))) -> s(-(s(x510)))
    s(-(s(x510))) -> s(p(-(x510)))
    s(p(-(x510))) -> -(x510)
    +(x,0()) -> +(0(),x)
    +(x,0()) -> x
    +(0(),x) -> x
    +(x,s(y)) -> +(s(y),x)
    +(x,s(y)) -> s(+(x,y))
    +(s(y),x) -> s(+(y,x))
    s(+(x,y)) -> s(+(y,x))
    +(x,p(y)) -> +(p(y),x)
    +(x,p(y)) -> p(+(x,y))
    +(p(y),x) -> p(+(y,x))
    p(+(x,y)) -> p(+(y,x))
    +(0(),y) -> +(y,0())
    +(0(),y) -> y
    +(y,0()) -> y
    +(s(x),y) -> +(y,s(x))
    +(s(x),y) -> s(+(x,y))
    +(y,s(x)) -> s(+(y,x))
    s(+(x,y)) -> s(+(y,x))
    +(p(x),y) -> +(y,p(x))
    +(p(x),y) -> p(+(x,y))
    +(y,p(x)) -> p(+(y,x))
    p(+(x,y)) -> p(+(y,x))
    -(+(x,y)) -> -(+(y,x))
    -(+(x,y)) -> +(-(x),-(y))
    -(+(y,x)) -> +(-(y),-(x))
    +(-(x),-(y)) -> +(-(y),-(x))
   weak:
    +(x,0()) -> x
    +(x,s(y)) -> s(+(x,y))
    +(x,p(y)) -> p(+(x,y))
    +(0(),y) -> y
    +(s(x),y) -> s(+(x,y))
    +(p(x),y) -> p(+(x,y))
    s(p(x)) -> x
    p(s(x)) -> x
    -(0()) -> 0()
    -(s(x)) -> p(-(x))
    -(p(x)) -> s(-(x))
    +(x,y) -> +(y,x)
    -(+(x,y)) -> +(-(x),-(y))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [-](x0) = 2x0,
     
     [+](x0, x1) = 4x0 + 4x1,
     
     [p](x0) = x0 + 1,
     
     [0] = 0,
     
     [s](x0) = x0 + 1
    orientation:
     +(0(),0()) = 0 >= 0 = 0()
     
     +(0(),0()) = 0 >= 0 = 0()
     
     +(s(x),0()) = 4x + 4 >= x + 1 = s(x)
     
     +(s(x),0()) = 4x + 4 >= 4x + 1 = s(+(x,0()))
     
     s(+(x,0())) = 4x + 1 >= x + 1 = s(x)
     
     +(p(x),0()) = 4x + 4 >= x + 1 = p(x)
     
     +(p(x),0()) = 4x + 4 >= 4x + 1 = p(+(x,0()))
     
     p(+(x,0())) = 4x + 1 >= x + 1 = p(x)
     
     +(x,0()) = 4x >= x = x
     
     +(x,0()) = 4x >= 4x = +(0(),x)
     
     +(0(),x) = 4x >= x = x
     
     -(+(x,0())) = 8x >= 2x = -(x)
     
     -(+(x,0())) = 8x >= 8x = +(-(x),-(0()))
     
     +(-(x),-(0())) = 8x >= 8x = +(-(x),0())
     
     +(-(x),0()) = 8x >= 2x = -(x)
     
     +(0(),s(x459)) = 4x459 + 4 >= 4x459 + 1 = s(+(0(),x459))
     
     +(0(),s(x459)) = 4x459 + 4 >= x459 + 1 = s(x459)
     
     s(+(0(),x459)) = 4x459 + 1 >= x459 + 1 = s(x459)
     
     +(s(x),s(x461)) = 4x + 4x461 + 8 >= 4x + 4x461 + 5 = s(+(s(x),x461))
     
     +(s(x),s(x461)) = 4x + 4x461 + 8 >= 4x + 4x461 + 5 = s(+(x,s(x461)))
     
     s(+(s(x),x461)) = 4x + 4x461 + 5 >= 4x + 4x461 + 2 = s(s(+(x,x461)))
     
     s(+(x,s(x461))) = 4x + 4x461 + 5 >= 4x + 4x461 + 2 = s(s(+(x,x461)))
     
     +(p(x),s(x463)) = 4x + 4x463 + 8 >= 4x + 4x463 + 5 = s(+(p(x),x463))
     
     +(p(x),s(x463)) = 4x + 4x463 + 8 >= 4x + 4x463 + 5 = p(+(x,s(x463)))
     
     s(+(p(x),x463)) = 4x + 4x463 + 5 >= 4x + 4x463 + 2 = s(p(+(x,x463)))
     
     s(p(+(x,x463))) = 4x + 4x463 + 2 >= 4x + 4x463 = +(x,x463)
     
     p(+(x,s(x463))) = 4x + 4x463 + 5 >= 4x + 4x463 + 2 = p(s(+(x,x463)))
     
     p(s(+(x,x463))) = 4x + 4x463 + 2 >= 4x + 4x463 = +(x,x463)
     
     +(x,s(x465)) = 4x + 4x465 + 4 >= 4x + 4x465 + 1 = s(+(x,x465))
     
     +(x,s(x465)) = 4x + 4x465 + 4 >= 4x + 4x465 + 4 = +(s(x465),x)
     
     s(+(x,x465)) = 4x + 4x465 + 1 >= 4x + 4x465 + 1 = s(+(x465,x))
     
     +(s(x465),x) = 4x + 4x465 + 4 >= 4x + 4x465 + 1 = s(+(x465,x))
     
     -(+(x,s(x467))) = 8x + 8x467 + 8 >= 8x + 8x467 + 2 = -(s(+(x,x467)))
     
     -(+(x,s(x467))) = 8x + 8x467 + 8 >= 8x + 8x467 + 8 = +(-(x),-(s(x467)))
     
     -(s(+(x,x467))) = 8x + 8x467 + 2 >= 8x + 8x467 + 1 = p(-(+(x,x467)))
     
     p(-(+(x,x467))) = 8x + 8x467 + 1 >= 8x + 8x467 + 1 = p(+(-(x),-(x467)))
     
     +(-(x),-(s(x467))) = 8x + 8x467 + 8 >= 8x + 8x467 + 4 = +(-(x),p(-(x467)))
     
     +(-(x),p(-(x467))) = 8x + 8x467 + 4 >= 8x + 8x467 + 1 = p(+(-(x),-(x467)))
     
     +(0(),p(x469)) = 4x469 + 4 >= 4x469 + 1 = p(+(0(),x469))
     
     +(0(),p(x469)) = 4x469 + 4 >= x469 + 1 = p(x469)
     
     p(+(0(),x469)) = 4x469 + 1 >= x469 + 1 = p(x469)
     
     +(s(x),p(x471)) = 4x + 4x471 + 8 >= 4x + 4x471 + 5 = p(+(s(x),x471))
     
     +(s(x),p(x471)) = 4x + 4x471 + 8 >= 4x + 4x471 + 5 = s(+(x,p(x471)))
     
     p(+(s(x),x471)) = 4x + 4x471 + 5 >= 4x + 4x471 + 2 = p(s(+(x,x471)))
     
     p(s(+(x,x471))) = 4x + 4x471 + 2 >= 4x + 4x471 = +(x,x471)
     
     s(+(x,p(x471))) = 4x + 4x471 + 5 >= 4x + 4x471 + 2 = s(p(+(x,x471)))
     
     s(p(+(x,x471))) = 4x + 4x471 + 2 >= 4x + 4x471 = +(x,x471)
     
     +(p(x),p(x473)) = 4x + 4x473 + 8 >= 4x + 4x473 + 5 = p(+(p(x),x473))
     
     +(p(x),p(x473)) = 4x + 4x473 + 8 >= 4x + 4x473 + 5 = p(+(x,p(x473)))
     
     p(+(p(x),x473)) = 4x + 4x473 + 5 >= 4x + 4x473 + 2 = p(p(+(x,x473)))
     
     p(+(x,p(x473))) = 4x + 4x473 + 5 >= 4x + 4x473 + 2 = p(p(+(x,x473)))
     
     +(x,p(x475)) = 4x + 4x475 + 4 >= 4x + 4x475 + 1 = p(+(x,x475))
     
     +(x,p(x475)) = 4x + 4x475 + 4 >= 4x + 4x475 + 4 = +(p(x475),x)
     
     p(+(x,x475)) = 4x + 4x475 + 1 >= 4x + 4x475 + 1 = p(+(x475,x))
     
     +(p(x475),x) = 4x + 4x475 + 4 >= 4x + 4x475 + 1 = p(+(x475,x))
     
     -(+(x,p(x477))) = 8x + 8x477 + 8 >= 8x + 8x477 + 2 = -(p(+(x,x477)))
     
     -(+(x,p(x477))) = 8x + 8x477 + 8 >= 8x + 8x477 + 8 = +(-(x),-(p(x477)))
     
     -(p(+(x,x477))) = 8x + 8x477 + 2 >= 8x + 8x477 + 1 = s(-(+(x,x477)))
     
     s(-(+(x,x477))) = 8x + 8x477 + 1 >= 8x + 8x477 + 1 = s(+(-(x),-(x477)))
     
     +(-(x),-(p(x477))) = 8x + 8x477 + 8 >= 8x + 8x477 + 4 = +(-(x),s(-(x477)))
     
     +(-(x),s(-(x477))) = 8x + 8x477 + 4 >= 8x + 8x477 + 1 = s(+(-(x),-(x477)))
     
     +(0(),0()) = 0 >= 0 = 0()
     
     +(0(),0()) = 0 >= 0 = 0()
     
     +(0(),s(y)) = 4y + 4 >= y + 1 = s(y)
     
     +(0(),s(y)) = 4y + 4 >= 4y + 1 = s(+(0(),y))
     
     s(+(0(),y)) = 4y + 1 >= y + 1 = s(y)
     
     +(0(),p(y)) = 4y + 4 >= y + 1 = p(y)
     
     +(0(),p(y)) = 4y + 4 >= 4y + 1 = p(+(0(),y))
     
     p(+(0(),y)) = 4y + 1 >= y + 1 = p(y)
     
     +(0(),y) = 4y >= y = y
     
     +(0(),y) = 4y >= 4y = +(y,0())
     
     +(y,0()) = 4y >= y = y
     
     -(+(0(),y)) = 8y >= 2y = -(y)
     
     -(+(0(),y)) = 8y >= 8y = +(-(0()),-(y))
     
     +(-(0()),-(y)) = 8y >= 8y = +(0(),-(y))
     
     +(0(),-(y)) = 8y >= 2y = -(y)
     
     +(s(x483),0()) = 4x483 + 4 >= 4x483 + 1 = s(+(x483,0()))
     
     +(s(x483),0()) = 4x483 + 4 >= x483 + 1 = s(x483)
     
     s(+(x483,0())) = 4x483 + 1 >= x483 + 1 = s(x483)
     
     +(s(x485),s(y)) = 4x485 + 4y + 8 >= 4x485 + 4y + 5 = s(+(x485,s(y)))
     
     +(s(x485),s(y)) = 4x485 + 4y + 8 >= 4x485 + 4y + 5 = s(+(s(x485),y))
     
     s(+(x485,s(y))) = 4x485 + 4y + 5 >= 4x485 + 4y + 2 = s(s(+(x485,y)))
     
     s(+(s(x485),y)) = 4x485 + 4y + 5 >= 4x485 + 4y + 2 = s(s(+(x485,y)))
     
     +(s(x487),p(y)) = 4x487 + 4y + 8 >= 4x487 + 4y + 5 = s(+(x487,p(y)))
     
     +(s(x487),p(y)) = 4x487 + 4y + 8 >= 4x487 + 4y + 5 = p(+(s(x487),y))
     
     s(+(x487,p(y))) = 4x487 + 4y + 5 >= 4x487 + 4y + 2 = s(p(+(x487,y)))
     
     s(p(+(x487,y))) = 4x487 + 4y + 2 >= 4x487 + 4y = +(x487,y)
     
     p(+(s(x487),y)) = 4x487 + 4y + 5 >= 4x487 + 4y + 2 = p(s(+(x487,y)))
     
     p(s(+(x487,y))) = 4x487 + 4y + 2 >= 4x487 + 4y = +(x487,y)
     
     +(s(x489),y) = 4x489 + 4y + 4 >= 4x489 + 4y + 1 = s(+(x489,y))
     
     +(s(x489),y) = 4x489 + 4y + 4 >= 4x489 + 4y + 4 = +(y,s(x489))
     
     s(+(x489,y)) = 4x489 + 4y + 1 >= 4x489 + 4y + 1 = s(+(y,x489))
     
     +(y,s(x489)) = 4x489 + 4y + 4 >= 4x489 + 4y + 1 = s(+(y,x489))
     
     -(+(s(x491),y)) = 8x491 + 8y + 8 >= 8x491 + 8y + 2 = -(s(+(x491,y)))
     
     -(+(s(x491),y)) = 8x491 + 8y + 8 >= 8x491 + 8y + 8 = +(-(s(x491)),-(y))
     
     -(s(+(x491,y))) = 8x491 + 8y + 2 >= 8x491 + 8y + 1 = p(-(+(x491,y)))
     
     p(-(+(x491,y))) = 8x491 + 8y + 1 >= 8x491 + 8y + 1 = p(+(-(x491),-(y)))
     
     +(-(s(x491)),-(y)) = 8x491 + 8y + 8 >= 8x491 + 8y + 4 = +(p(-(x491)),-(y))
     
     +(p(-(x491)),-(y)) = 8x491 + 8y + 4 >= 8x491 + 8y + 1 = p(+(-(x491),-(y)))
     
     +(p(x493),0()) = 4x493 + 4 >= 4x493 + 1 = p(+(x493,0()))
     
     +(p(x493),0()) = 4x493 + 4 >= x493 + 1 = p(x493)
     
     p(+(x493,0())) = 4x493 + 1 >= x493 + 1 = p(x493)
     
     +(p(x495),s(y)) = 4x495 + 4y + 8 >= 4x495 + 4y + 5 = p(+(x495,s(y)))
     
     +(p(x495),s(y)) = 4x495 + 4y + 8 >= 4x495 + 4y + 5 = s(+(p(x495),y))
     
     p(+(x495,s(y))) = 4x495 + 4y + 5 >= 4x495 + 4y + 2 = p(s(+(x495,y)))
     
     p(s(+(x495,y))) = 4x495 + 4y + 2 >= 4x495 + 4y = +(x495,y)
     
     s(+(p(x495),y)) = 4x495 + 4y + 5 >= 4x495 + 4y + 2 = s(p(+(x495,y)))
     
     s(p(+(x495,y))) = 4x495 + 4y + 2 >= 4x495 + 4y = +(x495,y)
     
     +(p(x497),p(y)) = 4x497 + 4y + 8 >= 4x497 + 4y + 5 = p(+(x497,p(y)))
     
     +(p(x497),p(y)) = 4x497 + 4y + 8 >= 4x497 + 4y + 5 = p(+(p(x497),y))
     
     p(+(x497,p(y))) = 4x497 + 4y + 5 >= 4x497 + 4y + 2 = p(p(+(x497,y)))
     
     p(+(p(x497),y)) = 4x497 + 4y + 5 >= 4x497 + 4y + 2 = p(p(+(x497,y)))
     
     +(p(x499),y) = 4x499 + 4y + 4 >= 4x499 + 4y + 1 = p(+(x499,y))
     
     +(p(x499),y) = 4x499 + 4y + 4 >= 4x499 + 4y + 4 = +(y,p(x499))
     
     p(+(x499,y)) = 4x499 + 4y + 1 >= 4x499 + 4y + 1 = p(+(y,x499))
     
     +(y,p(x499)) = 4x499 + 4y + 4 >= 4x499 + 4y + 1 = p(+(y,x499))
     
     -(+(p(x501),y)) = 8x501 + 8y + 8 >= 8x501 + 8y + 2 = -(p(+(x501,y)))
     
     -(+(p(x501),y)) = 8x501 + 8y + 8 >= 8x501 + 8y + 8 = +(-(p(x501)),-(y))
     
     -(p(+(x501,y))) = 8x501 + 8y + 2 >= 8x501 + 8y + 1 = s(-(+(x501,y)))
     
     s(-(+(x501,y))) = 8x501 + 8y + 1 >= 8x501 + 8y + 1 = s(+(-(x501),-(y)))
     
     +(-(p(x501)),-(y)) = 8x501 + 8y + 8 >= 8x501 + 8y + 4 = +(s(-(x501)),-(y))
     
     +(s(-(x501)),-(y)) = 8x501 + 8y + 4 >= 8x501 + 8y + 1 = s(+(-(x501),-(y)))
     
     +(x,s(p(x503))) = 4x + 4x503 + 8 >= 4x + 4x503 = +(x,x503)
     
     +(x,s(p(x503))) = 4x + 4x503 + 8 >= 4x + 4x503 + 5 = s(+(x,p(x503)))
     
     s(+(x,p(x503))) = 4x + 4x503 + 5 >= 4x + 4x503 + 2 = s(p(+(x,x503)))
     
     s(p(+(x,x503))) = 4x + 4x503 + 2 >= 4x + 4x503 = +(x,x503)
     
     +(s(p(x504)),y) = 4x504 + 4y + 8 >= 4x504 + 4y = +(x504,y)
     
     +(s(p(x504)),y) = 4x504 + 4y + 8 >= 4x504 + 4y + 5 = s(+(p(x504),y))
     
     s(+(p(x504),y)) = 4x504 + 4y + 5 >= 4x504 + 4y + 2 = s(p(+(x504,y)))
     
     s(p(+(x504,y))) = 4x504 + 4y + 2 >= 4x504 + 4y = +(x504,y)
     
     p(s(p(x505))) = x505 + 3 >= x505 + 1 = p(x505)
     
     p(s(p(x505))) = x505 + 3 >= x505 + 1 = p(x505)
     
     -(s(p(x506))) = 2x506 + 4 >= 2x506 = -(x506)
     
     -(s(p(x506))) = 2x506 + 4 >= 2x506 + 3 = p(-(p(x506)))
     
     p(-(p(x506))) = 2x506 + 3 >= 2x506 + 2 = p(s(-(x506)))
     
     p(s(-(x506))) = 2x506 + 2 >= 2x506 = -(x506)
     
     +(x,p(s(x507))) = 4x + 4x507 + 8 >= 4x + 4x507 = +(x,x507)
     
     +(x,p(s(x507))) = 4x + 4x507 + 8 >= 4x + 4x507 + 5 = p(+(x,s(x507)))
     
     p(+(x,s(x507))) = 4x + 4x507 + 5 >= 4x + 4x507 + 2 = p(s(+(x,x507)))
     
     p(s(+(x,x507))) = 4x + 4x507 + 2 >= 4x + 4x507 = +(x,x507)
     
     +(p(s(x508)),y) = 4x508 + 4y + 8 >= 4x508 + 4y = +(x508,y)
     
     +(p(s(x508)),y) = 4x508 + 4y + 8 >= 4x508 + 4y + 5 = p(+(s(x508),y))
     
     p(+(s(x508),y)) = 4x508 + 4y + 5 >= 4x508 + 4y + 2 = p(s(+(x508,y)))
     
     p(s(+(x508,y))) = 4x508 + 4y + 2 >= 4x508 + 4y = +(x508,y)
     
     s(p(s(x509))) = x509 + 3 >= x509 + 1 = s(x509)
     
     s(p(s(x509))) = x509 + 3 >= x509 + 1 = s(x509)
     
     -(p(s(x510))) = 2x510 + 4 >= 2x510 = -(x510)
     
     -(p(s(x510))) = 2x510 + 4 >= 2x510 + 3 = s(-(s(x510)))
     
     s(-(s(x510))) = 2x510 + 3 >= 2x510 + 2 = s(p(-(x510)))
     
     s(p(-(x510))) = 2x510 + 2 >= 2x510 = -(x510)
     
     +(x,0()) = 4x >= 4x = +(0(),x)
     
     +(x,0()) = 4x >= x = x
     
     +(0(),x) = 4x >= x = x
     
     +(x,s(y)) = 4x + 4y + 4 >= 4x + 4y + 4 = +(s(y),x)
     
     +(x,s(y)) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y))
     
     +(s(y),x) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(y,x))
     
     s(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = s(+(y,x))
     
     +(x,p(y)) = 4x + 4y + 4 >= 4x + 4y + 4 = +(p(y),x)
     
     +(x,p(y)) = 4x + 4y + 4 >= 4x + 4y + 1 = p(+(x,y))
     
     +(p(y),x) = 4x + 4y + 4 >= 4x + 4y + 1 = p(+(y,x))
     
     p(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = p(+(y,x))
     
     +(0(),y) = 4y >= 4y = +(y,0())
     
     +(0(),y) = 4y >= y = y
     
     +(y,0()) = 4y >= y = y
     
     +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 4 = +(y,s(x))
     
     +(s(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(x,y))
     
     +(y,s(x)) = 4x + 4y + 4 >= 4x + 4y + 1 = s(+(y,x))
     
     s(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = s(+(y,x))
     
     +(p(x),y) = 4x + 4y + 4 >= 4x + 4y + 4 = +(y,p(x))
     
     +(p(x),y) = 4x + 4y + 4 >= 4x + 4y + 1 = p(+(x,y))
     
     +(y,p(x)) = 4x + 4y + 4 >= 4x + 4y + 1 = p(+(y,x))
     
     p(+(x,y)) = 4x + 4y + 1 >= 4x + 4y + 1 = p(+(y,x))
     
     -(+(x,y)) = 8x + 8y >= 8x + 8y = -(+(y,x))
     
     -(+(x,y)) = 8x + 8y >= 8x + 8y = +(-(x),-(y))
     
     -(+(y,x)) = 8x + 8y >= 8x + 8y = +(-(y),-(x))
     
     +(-(x),-(y)) = 8x + 8y >= 8x + 8y = +(-(y),-(x))
     
     s(p(x)) = x + 2 >= x = x
     
     p(s(x)) = x + 2 >= x = x
     
     -(0()) = 0 >= 0 = 0()
     
     -(s(x)) = 2x + 2 >= 2x + 1 = p(-(x))
     
     -(p(x)) = 2x + 2 >= 2x + 1 = s(-(x))
     
     +(x,y) = 4x + 4y >= 4x + 4y = +(y,x)
    problem:
     strict:
      +(0(),0()) -> 0()
      +(0(),0()) -> 0()
      s(+(x,0())) -> s(x)
      p(+(x,0())) -> p(x)
      +(x,0()) -> x
      +(x,0()) -> +(0(),x)
      +(0(),x) -> x
      -(+(x,0())) -> -(x)
      -(+(x,0())) -> +(-(x),-(0()))
      +(-(x),-(0())) -> +(-(x),0())
      +(-(x),0()) -> -(x)
      s(+(0(),x459)) -> s(x459)
      +(x,s(x465)) -> +(s(x465),x)
      s(+(x,x465)) -> s(+(x465,x))
      -(+(x,s(x467))) -> +(-(x),-(s(x467)))
      p(-(+(x,x467))) -> p(+(-(x),-(x467)))
      p(+(0(),x469)) -> p(x469)
      +(x,p(x475)) -> +(p(x475),x)
      p(+(x,x475)) -> p(+(x475,x))
      -(+(x,p(x477))) -> +(-(x),-(p(x477)))
      s(-(+(x,x477))) -> s(+(-(x),-(x477)))
      +(0(),0()) -> 0()
      +(0(),0()) -> 0()
      s(+(0(),y)) -> s(y)
      p(+(0(),y)) -> p(y)
      +(0(),y) -> y
      +(0(),y) -> +(y,0())
      +(y,0()) -> y
      -(+(0(),y)) -> -(y)
      -(+(0(),y)) -> +(-(0()),-(y))
      +(-(0()),-(y)) -> +(0(),-(y))
      +(0(),-(y)) -> -(y)
      s(+(x483,0())) -> s(x483)
      +(s(x489),y) -> +(y,s(x489))
      s(+(x489,y)) -> s(+(y,x489))
      -(+(s(x491),y)) -> +(-(s(x491)),-(y))
      p(-(+(x491,y))) -> p(+(-(x491),-(y)))
      p(+(x493,0())) -> p(x493)
      +(p(x499),y) -> +(y,p(x499))
      p(+(x499,y)) -> p(+(y,x499))
      -(+(p(x501),y)) -> +(-(p(x501)),-(y))
      s(-(+(x501,y))) -> s(+(-(x501),-(y)))
      +(x,0()) -> +(0(),x)
      +(x,0()) -> x
      +(0(),x) -> x
      +(x,s(y)) -> +(s(y),x)
      s(+(x,y)) -> s(+(y,x))
      +(x,p(y)) -> +(p(y),x)
      p(+(x,y)) -> p(+(y,x))
      +(0(),y) -> +(y,0())
      +(0(),y) -> y
      +(y,0()) -> y
      +(s(x),y) -> +(y,s(x))
      s(+(x,y)) -> s(+(y,x))
      +(p(x),y) -> +(y,p(x))
      p(+(x,y)) -> p(+(y,x))
      -(+(x,y)) -> -(+(y,x))
      -(+(x,y)) -> +(-(x),-(y))
      -(+(y,x)) -> +(-(y),-(x))
      +(-(x),-(y)) -> +(-(y),-(x))
     weak:
      +(x,0()) -> x
      +(0(),y) -> y
      -(0()) -> 0()
      +(x,y) -> +(y,x)
      -(+(x,y)) -> +(-(x),-(y))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [-](x0) = 2x0,
      
      [+](x0, x1) = 2x0 + 2x1 + 2,
      
      [p](x0) = x0 + 2,
      
      [0] = 2,
      
      [s](x0) = x0
     orientation:
      +(0(),0()) = 10 >= 2 = 0()
      
      +(0(),0()) = 10 >= 2 = 0()
      
      s(+(x,0())) = 2x + 6 >= x = s(x)
      
      p(+(x,0())) = 2x + 8 >= x + 2 = p(x)
      
      +(x,0()) = 2x + 6 >= x = x
      
      +(x,0()) = 2x + 6 >= 2x + 6 = +(0(),x)
      
      +(0(),x) = 2x + 6 >= x = x
      
      -(+(x,0())) = 4x + 12 >= 2x = -(x)
      
      -(+(x,0())) = 4x + 12 >= 4x + 10 = +(-(x),-(0()))
      
      +(-(x),-(0())) = 4x + 10 >= 4x + 6 = +(-(x),0())
      
      +(-(x),0()) = 4x + 6 >= 2x = -(x)
      
      s(+(0(),x459)) = 2x459 + 6 >= x459 = s(x459)
      
      +(x,s(x465)) = 2x + 2x465 + 2 >= 2x + 2x465 + 2 = +(s(x465),x)
      
      s(+(x,x465)) = 2x + 2x465 + 2 >= 2x + 2x465 + 2 = s(+(x465,x))
      
      -(+(x,s(x467))) = 4x + 4x467 + 4 >= 4x + 4x467 + 2 = +(-(x),-(s(x467)))
      
      p(-(+(x,x467))) = 4x + 4x467 + 6 >= 4x + 4x467 + 4 = p(+(-(x),-(x467)))
      
      p(+(0(),x469)) = 2x469 + 8 >= x469 + 2 = p(x469)
      
      +(x,p(x475)) = 2x + 2x475 + 6 >= 2x + 2x475 + 6 = +(p(x475),x)
      
      p(+(x,x475)) = 2x + 2x475 + 4 >= 2x + 2x475 + 4 = p(+(x475,x))
      
      -(+(x,p(x477))) = 4x + 4x477 + 12 >= 4x + 4x477 + 10 = +(-(x),-(p(x477)))
      
      s(-(+(x,x477))) = 4x + 4x477 + 4 >= 4x + 4x477 + 2 = s(+(-(x),-(x477)))
      
      +(0(),0()) = 10 >= 2 = 0()
      
      +(0(),0()) = 10 >= 2 = 0()
      
      s(+(0(),y)) = 2y + 6 >= y = s(y)
      
      p(+(0(),y)) = 2y + 8 >= y + 2 = p(y)
      
      +(0(),y) = 2y + 6 >= y = y
      
      +(0(),y) = 2y + 6 >= 2y + 6 = +(y,0())
      
      +(y,0()) = 2y + 6 >= y = y
      
      -(+(0(),y)) = 4y + 12 >= 2y = -(y)
      
      -(+(0(),y)) = 4y + 12 >= 4y + 10 = +(-(0()),-(y))
      
      +(-(0()),-(y)) = 4y + 10 >= 4y + 6 = +(0(),-(y))
      
      +(0(),-(y)) = 4y + 6 >= 2y = -(y)
      
      s(+(x483,0())) = 2x483 + 6 >= x483 = s(x483)
      
      +(s(x489),y) = 2x489 + 2y + 2 >= 2x489 + 2y + 2 = +(y,s(x489))
      
      s(+(x489,y)) = 2x489 + 2y + 2 >= 2x489 + 2y + 2 = s(+(y,x489))
      
      -(+(s(x491),y)) = 4x491 + 4y + 4 >= 4x491 + 4y + 2 = +(-(s(x491)),-(y))
      
      p(-(+(x491,y))) = 4x491 + 4y + 6 >= 4x491 + 4y + 4 = p(+(-(x491),-(y)))
      
      p(+(x493,0())) = 2x493 + 8 >= x493 + 2 = p(x493)
      
      +(p(x499),y) = 2x499 + 2y + 6 >= 2x499 + 2y + 6 = +(y,p(x499))
      
      p(+(x499,y)) = 2x499 + 2y + 4 >= 2x499 + 2y + 4 = p(+(y,x499))
      
      -(+(p(x501),y)) = 4x501 + 4y + 12 >= 4x501 + 4y + 10 = +(-(p(x501)),-(y))
      
      s(-(+(x501,y))) = 4x501 + 4y + 4 >= 4x501 + 4y + 2 = s(+(-(x501),-(y)))
      
      +(x,0()) = 2x + 6 >= 2x + 6 = +(0(),x)
      
      +(x,0()) = 2x + 6 >= x = x
      
      +(0(),x) = 2x + 6 >= x = x
      
      +(x,s(y)) = 2x + 2y + 2 >= 2x + 2y + 2 = +(s(y),x)
      
      s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x))
      
      +(x,p(y)) = 2x + 2y + 6 >= 2x + 2y + 6 = +(p(y),x)
      
      p(+(x,y)) = 2x + 2y + 4 >= 2x + 2y + 4 = p(+(y,x))
      
      +(0(),y) = 2y + 6 >= 2y + 6 = +(y,0())
      
      +(0(),y) = 2y + 6 >= y = y
      
      +(y,0()) = 2y + 6 >= y = y
      
      +(s(x),y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,s(x))
      
      s(+(x,y)) = 2x + 2y + 2 >= 2x + 2y + 2 = s(+(y,x))
      
      +(p(x),y) = 2x + 2y + 6 >= 2x + 2y + 6 = +(y,p(x))
      
      p(+(x,y)) = 2x + 2y + 4 >= 2x + 2y + 4 = p(+(y,x))
      
      -(+(x,y)) = 4x + 4y + 4 >= 4x + 4y + 4 = -(+(y,x))
      
      -(+(x,y)) = 4x + 4y + 4 >= 4x + 4y + 2 = +(-(x),-(y))
      
      -(+(y,x)) = 4x + 4y + 4 >= 4x + 4y + 2 = +(-(y),-(x))
      
      +(-(x),-(y)) = 4x + 4y + 2 >= 4x + 4y + 2 = +(-(y),-(x))
      
      -(0()) = 4 >= 2 = 0()
      
      +(x,y) = 2x + 2y + 2 >= 2x + 2y + 2 = +(y,x)
     problem:
      strict:
       +(x,0()) -> +(0(),x)
       +(x,s(x465)) -> +(s(x465),x)
       s(+(x,x465)) -> s(+(x465,x))
       +(x,p(x475)) -> +(p(x475),x)
       p(+(x,x475)) -> p(+(x475,x))
       +(0(),y) -> +(y,0())
       +(s(x489),y) -> +(y,s(x489))
       s(+(x489,y)) -> s(+(y,x489))
       +(p(x499),y) -> +(y,p(x499))
       p(+(x499,y)) -> p(+(y,x499))
       +(x,0()) -> +(0(),x)
       +(x,s(y)) -> +(s(y),x)
       s(+(x,y)) -> s(+(y,x))
       +(x,p(y)) -> +(p(y),x)
       p(+(x,y)) -> p(+(y,x))
       +(0(),y) -> +(y,0())
       +(s(x),y) -> +(y,s(x))
       s(+(x,y)) -> s(+(y,x))
       +(p(x),y) -> +(y,p(x))
       p(+(x,y)) -> p(+(y,x))
       -(+(x,y)) -> -(+(y,x))
       +(-(x),-(y)) -> +(-(y),-(x))
      weak:
       +(x,y) -> +(y,x)
     Shift Processor (ldh) lab=left (force):
      strict:
       
      weak:
       
      Rule Labeling Processor:
       strict:
        
       weak:
        
       rule labeling (right):
        +(x,0()) -> x: 1
        +(x,s(y)) -> s(+(x,y)): 1
        +(x,p(y)) -> p(+(x,y)): 1
        +(0(),y) -> y: 0
        +(s(x),y) -> s(+(x,y)): 0
        +(p(x),y) -> p(+(x,y)): 0
        s(p(x)) -> x: 0
        p(s(x)) -> x: 0
        -(0()) -> 0(): 0
        -(s(x)) -> p(-(x)): 0
        -(p(x)) -> s(-(x)): 0
        +(x,y) -> +(y,x): 2
        -(+(x,y)) -> +(-(x),-(y)): 0
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (left):
         +(x,0()) -> x: 0
         +(x,s(y)) -> s(+(x,y)): 8
         +(x,p(y)) -> p(+(x,y)): 2
         +(0(),y) -> y: 2
         +(s(x),y) -> s(+(x,y)): 8
         +(p(x),y) -> p(+(x,y)): 0
         s(p(x)) -> x: 0
         p(s(x)) -> x: 8
         -(0()) -> 0(): 8
         -(s(x)) -> p(-(x)): 8
         -(p(x)) -> s(-(x)): 0
         +(x,y) -> +(y,x): 11
         -(+(x,y)) -> +(-(x),-(y)): 8
        Decreasing Processor:
         The following diagrams are decreasing:
         peak:
          0() <-0|[=>0,==1,=?1]- +(0(),0()) -3|[?=2,==1,>=0]-> 0()
         joins (1):
          
          
         peak:
          s(x) <-0|[=>0,==1,=?1]- +(s(x),0()) -4|[?=8,==1,>=0]-> s(+(x,0()))
         joins (1):
          
          s(+(x,0())) -0|0[=>0,>>0,=?1]-> s(x)
         peak:
          p(x) <-0|[==0,==1,=?1]- +(p(x),0()) -5|[==0,==1,>=0]-> p(+(x,0()))
         joins (1):
          
          p(+(x,0())) -0|0[==0,>>0,=?1]-> p(x)
         peak:
          x <-0|[=>0,==1,=>1]- +(x,0()) -11|[?=11,==1,?=2]-> +(0(),x)
         joins (1):
          
          +(0(),x) -3|[?>2,==1,>>0]-> x
         peak:
          -(x) <-0|0[=>0,==1,=?1]- -(+(x,0())) -12|[?=8,==1,>=0]-> +(-(x),-(0()))
         joins (1):
          
          +(-(x),-(0())) -8|1[?=8,>>0,>=0]-> +(-(x),0()) -0|[=>0,>>0,=?1]-> -(x)
         peak:
          s(+(0(),x459)) <-1|[=?8,==1,=?1]- +(0(),s(x459)) -3|[>=2,==1,>=0]-> s(x459)
         joins (1):
          s(+(0(),x459)) -3|0[>=2,>>0,>=0]-> s(x459)
          
         peak:
          s(+(s(x),x461)) <-1|[==8,==1,=?1]- +(s(x),s(x461)) -4|[==8,==1,>=0]-> s(+(x,s(x461)))
         joins (1):
          s(+(s(x),x461)) -4|0[==8,>>0,>=0]-> s(s(+(x,x461)))
          s(+(x,s(x461))) -1|0[==8,>>0,=?1]-> s(s(+(x,x461)))
         peak:
          s(+(p(x),x463)) <-1|[=?8,==1,=?1]- +(p(x),s(x463)) -5|[>=0,==1,>=0]-> p(+(x,s(x463)))
         joins (1):
          s(+(p(x),x463)) -5|0[>=0,>>0,>=0]-> s(p(+(x,x463))) -6|[>=0,>>0,>=0]-> +(x,x463)
          p(+(x,s(x463))) -1|0[=?8,>>0,=?1]-> p(s(+(x,x463))) -7|[=?8,>>0,>=0]-> +(x,x463)
         peak:
          s(+(x,x465)) <-1|[=>8,==1,=>1]- +(x,s(x465)) -11|[?=11,==1,?=2]-> +(s(x465),x)
         joins (1):
          s(+(x,x465)) -11|0[?=11,>>0,?=2]-> s(+(x465,x))
          +(s(x465),x) -4|[=>8,==1,>>0]-> s(+(x465,x))
         peak:
          -(s(+(x,x467))) <-1|0[==8,==1,=?1]- -(+(x,s(x467))) -12|[==8,==1,>=0]-> 
                                              +(-(x),-(s(x467)))
         joins (1):
          -(s(+(x,x467))) -9|[==8,>>0,>=0]-> p(-(+(x,x467))) -12|0[==8,>>0,>=0]-> 
                                             p(+(-(x),-(x467)))
          +(-(x),-(s(x467))) -9|1[==8,>>0,>=0]-> +(-(x),p(-(x467))) -2|
                                                 [>>2,>>0,=?1]-> p(+(-(x),-(x467)))
         peak:
          p(+(0(),x469)) <-2|[==2,==1,=?1]- +(0(),p(x469)) -3|[==2,==1,>=0]-> p(x469)
         joins (1):
          p(+(0(),x469)) -3|0[==2,>>0,>=0]-> p(x469)
          
         peak:
          p(+(s(x),x471)) <-2|[=>2,==1,=?1]- +(s(x),p(x471)) -4|[?=8,==1,>=0]-> s(+(x,p(x471)))
         joins (1):
          p(+(s(x),x471)) -4|0[?=8,>>0,>=0]-> p(s(+(x,x471))) -7|[?=8,>>0,>=0]-> +(x,x471)
          s(+(x,p(x471))) -2|0[=>2,>>0,=?1]-> s(p(+(x,x471))) -6|[>>0,>>0,>=0]-> +(x,x471)
         peak:
          p(+(p(x),x473)) <-2|[=?2,==1,=?1]- +(p(x),p(x473)) -5|[>=0,==1,>=0]-> p(+(x,p(x473)))
         joins (1):
          p(+(p(x),x473)) -5|0[>=0,>>0,>=0]-> p(p(+(x,x473)))
          p(+(x,p(x473))) -2|0[=?2,>>0,=?1]-> p(p(+(x,x473)))
         peak:
          p(+(x,x475)) <-2|[=>2,==1,=>1]- +(x,p(x475)) -11|[?=11,==1,?=2]-> +(p(x475),x)
         joins (1):
          p(+(x,x475)) -11|0[?=11,>>0,?=2]-> p(+(x475,x))
          +(p(x475),x) -5|[>>0,==1,>>0]-> p(+(x475,x))
         peak:
          -(p(+(x,x477))) <-2|0[=>2,==1,=?1]- -(+(x,p(x477))) -12|[?=8,==1,>=0]-> 
                                              +(-(x),-(p(x477)))
         joins (1):
          -(p(+(x,x477))) -10|[>>0,>>0,>=0]-> s(-(+(x,x477))) -12|0[?=8,>>0,>=0]-> 
                                              s(+(-(x),-(x477)))
          +(-(x),-(p(x477))) -10|1[>>0,>>0,>=0]-> +(-(x),s(-(x477))) -1|
                                                  [?=8,>>0,=?1]-> s(+(-(x),-(x477)))
         peak:
          0() <-3|[=?2,==1,=>0]- +(0(),0()) -0|[>=0,==1,?=1]-> 0()
         joins (1):
          
          
         peak:
          s(y) <-3|[=>2,==1,=>0]- +(0(),s(y)) -1|[?=8,==1,?=1]-> s(+(0(),y))
         joins (1):
          
          s(+(0(),y)) -3|0[=>2,>>0,=>0]-> s(y)
         peak:
          p(y) <-3|[==2,==1,=>0]- +(0(),p(y)) -2|[==2,==1,?=1]-> p(+(0(),y))
         joins (1):
          
          p(+(0(),y)) -3|0[==2,>>0,=>0]-> p(y)
         peak:
          y <-3|[=>2,==1,=>0]- +(0(),y) -11|[?=11,==1,?=2]-> +(y,0())
         joins (1):
          
          +(y,0()) -0|[>>0,==1,?>1]-> y
         peak:
          -(y) <-3|0[=>2,==1,==0]- -(+(0(),y)) -12|[?=8,==1,==0]-> +(-(0()),-(y))
         joins (1):
          
          +(-(0()),-(y)) -8|0[?=8,>>0,==0]-> +(0(),-(y)) -3|[=>2,>>0,==0]-> -(y)
         peak:
          s(+(x483,0())) <-4|[=?8,==1,=>0]- +(s(x483),0()) -0|[>=0,==1,?=1]-> s(x483)
         joins (1):
          s(+(x483,0())) -0|0[>=0,>>0,?=1]-> s(x483)
          
         peak:
          s(+(x485,s(y))) <-4|[==8,==1,=>0]- +(s(x485),s(y)) -1|[==8,==1,?=1]-> s(+(s(x485),y))
         joins (1):
          s(+(x485,s(y))) -1|0[==8,>>0,?=1]-> s(s(+(x485,y)))
          s(+(s(x485),y)) -4|0[==8,>>0,=>0]-> s(s(+(x485,y)))
         peak:
          s(+(x487,p(y))) <-4|[=?8,==1,=>0]- +(s(x487),p(y)) -2|[>=2,==1,?=1]-> p(+(s(x487),y))
         joins (1):
          s(+(x487,p(y))) -2|0[>=2,>>0,?=1]-> s(p(+(x487,y))) -6|[>>0,>>0,=>0]-> +(x487,y)
          p(+(s(x487),y)) -4|0[=?8,>>0,=>0]-> p(s(+(x487,y))) -7|[=?8,>>0,=>0]-> +(x487,y)
         peak:
          s(+(x489,y)) <-4|[=>8,==1,=>0]- +(s(x489),y) -11|[?=11,==1,?=2]-> +(y,s(x489))
         joins (1):
          s(+(x489,y)) -11|0[?=11,>>0,?=2]-> s(+(y,x489))
          +(y,s(x489)) -1|[=>8,==1,?>1]-> s(+(y,x489))
         peak:
          -(s(+(x491,y))) <-4|0[==8,==1,==0]- -(+(s(x491),y)) -12|[==8,==1,==0]-> 
                                              +(-(s(x491)),-(y))
         joins (1):
          -(s(+(x491,y))) -9|[==8,>>0,==0]-> p(-(+(x491,y))) -12|0[==8,>>0,==0]-> 
                                             p(+(-(x491),-(y)))
          +(-(s(x491)),-(y)) -9|0[==8,>>0,==0]-> +(p(-(x491)),-(y)) -5|
                                                 [>>0,>>0,==0]-> p(+(-(x491),-(y)))
         peak:
          p(+(x493,0())) <-5|[==0,==1,=>0]- +(p(x493),0()) -0|[==0,==1,?=1]-> p(x493)
         joins (1):
          p(+(x493,0())) -0|0[==0,>>0,?=1]-> p(x493)
          
         peak:
          p(+(x495,s(y))) <-5|[=>0,==1,=>0]- +(p(x495),s(y)) -1|[?=8,==1,?=1]-> s(+(p(x495),y))
         joins (1):
          p(+(x495,s(y))) -1|0[?=8,>>0,?=1]-> p(s(+(x495,y))) -7|[?=8,>>0,=>0]-> +(x495,y)
          s(+(p(x495),y)) -5|0[=>0,>>0,=>0]-> s(p(+(x495,y))) -6|[=>0,>>0,=>0]-> +(x495,y)
         peak:
          p(+(x497,p(y))) <-5|[=>0,==1,=>0]- +(p(x497),p(y)) -2|[?=2,==1,?=1]-> p(+(p(x497),y))
         joins (1):
          p(+(x497,p(y))) -2|0[?=2,>>0,?=1]-> p(p(+(x497,y)))
          p(+(p(x497),y)) -5|0[=>0,>>0,=>0]-> p(p(+(x497,y)))
         peak:
          p(+(x499,y)) <-5|[=>0,==1,=>0]- +(p(x499),y) -11|[?=11,==1,?=2]-> +(y,p(x499))
         joins (1):
          p(+(x499,y)) -11|0[?=11,>>0,?=2]-> p(+(y,x499))
          +(y,p(x499)) -2|[?>2,==1,?>1]-> p(+(y,x499))
         peak:
          -(p(+(x501,y))) <-5|0[=>0,==1,==0]- -(+(p(x501),y)) -12|[?=8,==1,==0]-> 
                                              +(-(p(x501)),-(y))
         joins (1):
          -(p(+(x501,y))) -10|[=>0,>>0,==0]-> s(-(+(x501,y))) -12|0[?=8,>>0,==0]-> 
                                              s(+(-(x501),-(y)))
          +(-(p(x501)),-(y)) -10|0[=>0,>>0,==0]-> +(s(-(x501)),-(y)) -4|
                                                  [?=8,>>0,==0]-> s(+(-(x501),-(y)))
         peak:
          +(x,x503) <-6|1[=>0,==1,=>0]- +(x,s(p(x503))) -1|[?=8,==1,?=1]-> s(+(x,p(x503)))
         joins (1):
          
          s(+(x,p(x503))) -2|0[?>2,>>0,?=1]-> s(p(+(x,x503))) -6|[=>0,>>0,=>0]-> +(x,x503)
         peak:
          +(x504,y) <-6|0[=>0,==1,==0]- +(s(p(x504)),y) -4|[?=8,==1,==0]-> s(+(p(x504),y))
         joins (1):
          
          s(+(p(x504),y)) -5|0[=>0,>>0,==0]-> s(p(+(x504,y))) -6|[=>0,>>0,==0]-> +(x504,y)
         peak:
          p(x505) <-6|0[=>0,==1,==0]- p(s(p(x505))) -7|[?=8,==1,==0]-> p(x505)
         joins (1):
          
          
         peak:
          -(x506) <-6|0[=>0,==1,==0]- -(s(p(x506))) -9|[?=8,==1,==0]-> p(-(p(x506)))
         joins (1):
          
          p(-(p(x506))) -10|0[=>0,>>0,==0]-> p(s(-(x506))) -7|[?=8,>>0,==0]-> -(x506)
         peak:
          +(x,x507) <-7|1[=?8,==1,=>0]- +(x,p(s(x507))) -2|[>=2,==1,?=1]-> p(+(x,s(x507)))
         joins (1):
          
          p(+(x,s(x507))) -1|0[=?8,>>0,?=1]-> p(s(+(x,x507))) -7|[=?8,>>0,=>0]-> +(x,x507)
         peak:
          +(x508,y) <-7|0[=?8,==1,==0]- +(p(s(x508)),y) -5|[>=0,==1,==0]-> p(+(s(x508),y))
         joins (1):
          
          p(+(s(x508),y)) -4|0[=?8,>>0,==0]-> p(s(+(x508,y))) -7|[=?8,>>0,==0]-> +(x508,y)
         peak:
          s(x509) <-7|0[=?8,==1,==0]- s(p(s(x509))) -6|[>=0,==1,==0]-> s(x509)
         joins (1):
          
          
         peak:
          -(x510) <-7|0[=?8,==1,==0]- -(p(s(x510))) -10|[>=0,==1,==0]-> s(-(s(x510)))
         joins (1):
          
          s(-(s(x510))) -9|0[=?8,>>0,==0]-> s(p(-(x510))) -6|[>=0,>>0,==0]-> -(x510)
         peak:
          +(0(),x) <-11|[=?11,==1,=?2]- +(x,0()) -0|[>=0,==1,>=1]-> x
         joins (1):
          +(0(),x) -3|[>?2,==1,>>0]-> x
          
         peak:
          +(s(y),x) <-11|[=?11,==1,=?2]- +(x,s(y)) -1|[>=8,==1,>=1]-> s(+(x,y))
         joins (1):
          +(s(y),x) -4|[>=8,==1,>>0]-> s(+(y,x))
          s(+(x,y)) -11|0[=?11,>>0,=?2]-> s(+(y,x))
         peak:
          +(p(y),x) <-11|[=?11,==1,=?2]- +(x,p(y)) -2|[>=2,==1,>=1]-> p(+(x,y))
         joins (1):
          +(p(y),x) -5|[>>0,==1,>>0]-> p(+(y,x))
          p(+(x,y)) -11|0[=?11,>>0,=?2]-> p(+(y,x))
         peak:
          +(y,0()) <-11|[=?11,==1,=?2]- +(0(),y) -3|[>=2,==1,>=0]-> y
         joins (1):
          +(y,0()) -0|[>>0,==1,>?1]-> y
          
         peak:
          +(y,s(x)) <-11|[=?11,==1,=?2]- +(s(x),y) -4|[>=8,==1,>=0]-> s(+(x,y))
         joins (1):
          +(y,s(x)) -1|[>=8,==1,>?1]-> s(+(y,x))
          s(+(x,y)) -11|0[=?11,>>0,=?2]-> s(+(y,x))
         peak:
          +(y,p(x)) <-11|[=?11,==1,=?2]- +(p(x),y) -5|[>=0,==1,>=0]-> p(+(x,y))
         joins (1):
          +(y,p(x)) -2|[>?2,==1,>?1]-> p(+(y,x))
          p(+(x,y)) -11|0[=?11,>>0,=?2]-> p(+(y,x))
         peak:
          -(+(y,x)) <-11|0[=?11,==1,=?2]- -(+(x,y)) -12|[>=8,==1,>=0]-> +(-(x),-(y))
         joins (1):
          -(+(y,x)) -12|[>=8,==1,>=0]-> +(-(y),-(x))
          +(-(x),-(y)) -11|[=?11,>>0,=?2]-> +(-(y),-(x))
         Qed