YES

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 (redex):
  strict:
   
  weak:
   -(+(x,y)) -> +(-(x),-(y))
   +(x,y) -> +(y,x)
   -(p(x)) -> s(-(x))
   -(s(x)) -> p(-(x))
   -(0()) -> 0()
   p(s(x)) -> x
   s(p(x)) -> x
   +(p(x),y) -> p(+(x,y))
   +(s(x),y) -> s(+(x,y))
   +(0(),y) -> y
   +(x,p(y)) -> p(+(x,y))
   +(x,s(y)) -> s(+(x,y))
   +(x,0()) -> x
  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(),x458)) <-1|[]- +(0(),s(x458)) -3|[]-> s(x458)
   s(+(s(x),x460)) <-1|[]- +(s(x),s(x460)) -4|[]-> s(+(x,s(x460)))
   s(+(p(x),x462)) <-1|[]- +(p(x),s(x462)) -5|[]-> p(+(x,s(x462)))
   s(+(x,x464)) <-1|[]- +(x,s(x464)) -11|[]-> +(s(x464),x)
   -(s(+(x,x466))) <-1|0[]- -(+(x,s(x466))) -12|[]-> +(-(x),-(s(x466)))
   p(+(0(),x468)) <-2|[]- +(0(),p(x468)) -3|[]-> p(x468)
   p(+(s(x),x470)) <-2|[]- +(s(x),p(x470)) -4|[]-> s(+(x,p(x470)))
   p(+(p(x),x472)) <-2|[]- +(p(x),p(x472)) -5|[]-> p(+(x,p(x472)))
   p(+(x,x474)) <-2|[]- +(x,p(x474)) -11|[]-> +(p(x474),x)
   -(p(+(x,x476))) <-2|0[]- -(+(x,p(x476))) -12|[]-> +(-(x),-(p(x476)))
   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(+(x482,0())) <-4|[]- +(s(x482),0()) -0|[]-> s(x482)
   s(+(x484,s(y))) <-4|[]- +(s(x484),s(y)) -1|[]-> s(+(s(x484),y))
   s(+(x486,p(y))) <-4|[]- +(s(x486),p(y)) -2|[]-> p(+(s(x486),y))
   s(+(x488,y)) <-4|[]- +(s(x488),y) -11|[]-> +(y,s(x488))
   -(s(+(x490,y))) <-4|0[]- -(+(s(x490),y)) -12|[]-> +(-(s(x490)),-(y))
   p(+(x492,0())) <-5|[]- +(p(x492),0()) -0|[]-> p(x492)
   p(+(x494,s(y))) <-5|[]- +(p(x494),s(y)) -1|[]-> s(+(p(x494),y))
   p(+(x496,p(y))) <-5|[]- +(p(x496),p(y)) -2|[]-> p(+(p(x496),y))
   p(+(x498,y)) <-5|[]- +(p(x498),y) -11|[]-> +(y,p(x498))
   -(p(+(x500,y))) <-5|0[]- -(+(p(x500),y)) -12|[]-> +(-(p(x500)),-(y))
   +(x,x502) <-6|1[]- +(x,s(p(x502))) -1|[]-> s(+(x,p(x502)))
   +(x503,y) <-6|0[]- +(s(p(x503)),y) -4|[]-> s(+(p(x503),y))
   p(x504) <-6|0[]- p(s(p(x504))) -7|[]-> p(x504)
   -(x505) <-6|0[]- -(s(p(x505))) -9|[]-> p(-(p(x505)))
   +(x,x506) <-7|1[]- +(x,p(s(x506))) -2|[]-> p(+(x,s(x506)))
   +(x507,y) <-7|0[]- +(p(s(x507)),y) -5|[]-> p(+(s(x507),y))
   s(x508) <-7|0[]- s(p(s(x508))) -6|[]-> s(x508)
   -(x509) <-7|0[]- -(p(s(x509))) -10|[]-> s(-(s(x509)))
   +(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 (no label):
   strict:
    
   weak:
    
   Shift Processor lab=left (dd):
    strict:
     +(0(),0()) -> 0()
     +(0(),0()) -> 0()
     +(s(x),0()) -> s(x)
     +(s(x),0()) -> s(+(x,0()))
     s(+(x,0())) -> s(x)
     +(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(x458)) -> s(+(0(),x458))
     +(0(),s(x458)) -> s(x458)
     s(+(0(),x458)) -> s(x458)
     +(s(x),s(x460)) -> s(+(s(x),x460))
     +(s(x),s(x460)) -> s(+(x,s(x460)))
     s(+(s(x),x460)) -> s(s(+(x,x460)))
     s(+(x,s(x460))) -> s(s(+(x,x460)))
     +(p(x),s(x462)) -> s(+(p(x),x462))
     +(p(x),s(x462)) -> p(+(x,s(x462)))
     s(+(p(x),x462)) -> s(p(+(x,x462)))
     s(p(+(x,x462))) -> +(x,x462)
     p(+(x,s(x462))) -> p(s(+(x,x462)))
     p(s(+(x,x462))) -> +(x,x462)
     +(x,s(x464)) -> s(+(x,x464))
     +(x,s(x464)) -> +(s(x464),x)
     s(+(x,x464)) -> s(+(x464,x))
     +(s(x464),x) -> s(+(x464,x))
     -(+(x,s(x466))) -> -(s(+(x,x466)))
     -(+(x,s(x466))) -> +(-(x),-(s(x466)))
     -(s(+(x,x466))) -> p(-(+(x,x466)))
     p(-(+(x,x466))) -> p(+(-(x),-(x466)))
     +(-(x),-(s(x466))) -> +(-(x),p(-(x466)))
     +(-(x),p(-(x466))) -> p(+(-(x),-(x466)))
     +(0(),p(x468)) -> p(+(0(),x468))
     +(0(),p(x468)) -> p(x468)
     p(+(0(),x468)) -> p(x468)
     +(s(x),p(x470)) -> p(+(s(x),x470))
     +(s(x),p(x470)) -> s(+(x,p(x470)))
     p(+(s(x),x470)) -> p(s(+(x,x470)))
     p(s(+(x,x470))) -> +(x,x470)
     s(+(x,p(x470))) -> s(p(+(x,x470)))
     s(p(+(x,x470))) -> +(x,x470)
     +(p(x),p(x472)) -> p(+(p(x),x472))
     +(p(x),p(x472)) -> p(+(x,p(x472)))
     p(+(p(x),x472)) -> p(p(+(x,x472)))
     p(+(x,p(x472))) -> p(p(+(x,x472)))
     +(x,p(x474)) -> p(+(x,x474))
     +(x,p(x474)) -> +(p(x474),x)
     p(+(x,x474)) -> p(+(x474,x))
     +(p(x474),x) -> p(+(x474,x))
     -(+(x,p(x476))) -> -(p(+(x,x476)))
     -(+(x,p(x476))) -> +(-(x),-(p(x476)))
     -(p(+(x,x476))) -> s(-(+(x,x476)))
     s(-(+(x,x476))) -> s(+(-(x),-(x476)))
     +(-(x),-(p(x476))) -> +(-(x),s(-(x476)))
     +(-(x),s(-(x476))) -> s(+(-(x),-(x476)))
     +(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(x482),0()) -> s(+(x482,0()))
     +(s(x482),0()) -> s(x482)
     s(+(x482,0())) -> s(x482)
     +(s(x484),s(y)) -> s(+(x484,s(y)))
     +(s(x484),s(y)) -> s(+(s(x484),y))
     s(+(x484,s(y))) -> s(s(+(x484,y)))
     s(+(s(x484),y)) -> s(s(+(x484,y)))
     +(s(x486),p(y)) -> s(+(x486,p(y)))
     +(s(x486),p(y)) -> p(+(s(x486),y))
     s(+(x486,p(y))) -> s(p(+(x486,y)))
     s(p(+(x486,y))) -> +(x486,y)
     p(+(s(x486),y)) -> p(s(+(x486,y)))
     p(s(+(x486,y))) -> +(x486,y)
     +(s(x488),y) -> s(+(x488,y))
     +(s(x488),y) -> +(y,s(x488))
     s(+(x488,y)) -> s(+(y,x488))
     +(y,s(x488)) -> s(+(y,x488))
     -(+(s(x490),y)) -> -(s(+(x490,y)))
     -(+(s(x490),y)) -> +(-(s(x490)),-(y))
     -(s(+(x490,y))) -> p(-(+(x490,y)))
     p(-(+(x490,y))) -> p(+(-(x490),-(y)))
     +(-(s(x490)),-(y)) -> +(p(-(x490)),-(y))
     +(p(-(x490)),-(y)) -> p(+(-(x490),-(y)))
     +(p(x492),0()) -> p(+(x492,0()))
     +(p(x492),0()) -> p(x492)
     p(+(x492,0())) -> p(x492)
     +(p(x494),s(y)) -> p(+(x494,s(y)))
     +(p(x494),s(y)) -> s(+(p(x494),y))
     p(+(x494,s(y))) -> p(s(+(x494,y)))
     p(s(+(x494,y))) -> +(x494,y)
     s(+(p(x494),y)) -> s(p(+(x494,y)))
     s(p(+(x494,y))) -> +(x494,y)
     +(p(x496),p(y)) -> p(+(x496,p(y)))
     +(p(x496),p(y)) -> p(+(p(x496),y))
     p(+(x496,p(y))) -> p(p(+(x496,y)))
     p(+(p(x496),y)) -> p(p(+(x496,y)))
     +(p(x498),y) -> p(+(x498,y))
     +(p(x498),y) -> +(y,p(x498))
     p(+(x498,y)) -> p(+(y,x498))
     +(y,p(x498)) -> p(+(y,x498))
     -(+(p(x500),y)) -> -(p(+(x500,y)))
     -(+(p(x500),y)) -> +(-(p(x500)),-(y))
     -(p(+(x500,y))) -> s(-(+(x500,y)))
     s(-(+(x500,y))) -> s(+(-(x500),-(y)))
     +(-(p(x500)),-(y)) -> +(s(-(x500)),-(y))
     +(s(-(x500)),-(y)) -> s(+(-(x500),-(y)))
     +(x,s(p(x502))) -> +(x,x502)
     +(x,s(p(x502))) -> s(+(x,p(x502)))
     s(+(x,p(x502))) -> s(p(+(x,x502)))
     s(p(+(x,x502))) -> +(x,x502)
     +(s(p(x503)),y) -> +(x503,y)
     +(s(p(x503)),y) -> s(+(p(x503),y))
     s(+(p(x503),y)) -> s(p(+(x503,y)))
     s(p(+(x503,y))) -> +(x503,y)
     p(s(p(x504))) -> p(x504)
     p(s(p(x504))) -> p(x504)
     -(s(p(x505))) -> -(x505)
     -(s(p(x505))) -> p(-(p(x505)))
     p(-(p(x505))) -> p(s(-(x505)))
     p(s(-(x505))) -> -(x505)
     +(x,p(s(x506))) -> +(x,x506)
     +(x,p(s(x506))) -> p(+(x,s(x506)))
     p(+(x,s(x506))) -> p(s(+(x,x506)))
     p(s(+(x,x506))) -> +(x,x506)
     +(p(s(x507)),y) -> +(x507,y)
     +(p(s(x507)),y) -> p(+(s(x507),y))
     p(+(s(x507),y)) -> p(s(+(x507,y)))
     p(s(+(x507,y))) -> +(x507,y)
     s(p(s(x508))) -> s(x508)
     s(p(s(x508))) -> s(x508)
     -(p(s(x509))) -> -(x509)
     -(p(s(x509))) -> s(-(s(x509)))
     s(-(s(x509))) -> s(p(-(x509)))
     s(p(-(x509))) -> -(x509)
     +(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(x458)) = 4x458 + 4 >= 4x458 + 1 = s(+(0(),x458))
      
      +(0(),s(x458)) = 4x458 + 4 >= x458 + 1 = s(x458)
      
      s(+(0(),x458)) = 4x458 + 1 >= x458 + 1 = s(x458)
      
      +(s(x),s(x460)) = 4x + 4x460 + 8 >= 4x + 4x460 + 5 = s(+(s(x),x460))
      
      +(s(x),s(x460)) = 4x + 4x460 + 8 >= 4x + 4x460 + 5 = s(+(x,s(x460)))
      
      s(+(s(x),x460)) = 4x + 4x460 + 5 >= 4x + 4x460 + 2 = s(s(+(x,x460)))
      
      s(+(x,s(x460))) = 4x + 4x460 + 5 >= 4x + 4x460 + 2 = s(s(+(x,x460)))
      
      +(p(x),s(x462)) = 4x + 4x462 + 8 >= 4x + 4x462 + 5 = s(+(p(x),x462))
      
      +(p(x),s(x462)) = 4x + 4x462 + 8 >= 4x + 4x462 + 5 = p(+(x,s(x462)))
      
      s(+(p(x),x462)) = 4x + 4x462 + 5 >= 4x + 4x462 + 2 = s(p(+(x,x462)))
      
      s(p(+(x,x462))) = 4x + 4x462 + 2 >= 4x + 4x462 = +(x,x462)
      
      p(+(x,s(x462))) = 4x + 4x462 + 5 >= 4x + 4x462 + 2 = p(s(+(x,x462)))
      
      p(s(+(x,x462))) = 4x + 4x462 + 2 >= 4x + 4x462 = +(x,x462)
      
      +(x,s(x464)) = 4x + 4x464 + 4 >= 4x + 4x464 + 1 = s(+(x,x464))
      
      +(x,s(x464)) = 4x + 4x464 + 4 >= 4x + 4x464 + 4 = +(s(x464),x)
      
      s(+(x,x464)) = 4x + 4x464 + 1 >= 4x + 4x464 + 1 = s(+(x464,x))
      
      +(s(x464),x) = 4x + 4x464 + 4 >= 4x + 4x464 + 1 = s(+(x464,x))
      
      -(+(x,s(x466))) = 8x + 8x466 + 8 >= 8x + 8x466 + 2 = -(s(+(x,x466)))
      
      -(+(x,s(x466))) = 8x + 8x466 + 8 >= 8x + 8x466 + 8 = +(-(x),-(s(x466)))
      
      -(s(+(x,x466))) = 8x + 8x466 + 2 >= 8x + 8x466 + 1 = p(-(+(x,x466)))
      
      p(-(+(x,x466))) = 8x + 8x466 + 1 >= 8x + 8x466 + 1 = p(+(-(x),-(x466)))
      
      +(-(x),-(s(x466))) = 8x + 8x466 + 8 >= 8x + 8x466 + 4 = +(-(x),p(-(x466)))
      
      +(-(x),p(-(x466))) = 8x + 8x466 + 4 >= 8x + 8x466 + 1 = p(+(-(x),-(x466)))
      
      +(0(),p(x468)) = 4x468 + 4 >= 4x468 + 1 = p(+(0(),x468))
      
      +(0(),p(x468)) = 4x468 + 4 >= x468 + 1 = p(x468)
      
      p(+(0(),x468)) = 4x468 + 1 >= x468 + 1 = p(x468)
      
      +(s(x),p(x470)) = 4x + 4x470 + 8 >= 4x + 4x470 + 5 = p(+(s(x),x470))
      
      +(s(x),p(x470)) = 4x + 4x470 + 8 >= 4x + 4x470 + 5 = s(+(x,p(x470)))
      
      p(+(s(x),x470)) = 4x + 4x470 + 5 >= 4x + 4x470 + 2 = p(s(+(x,x470)))
      
      p(s(+(x,x470))) = 4x + 4x470 + 2 >= 4x + 4x470 = +(x,x470)
      
      s(+(x,p(x470))) = 4x + 4x470 + 5 >= 4x + 4x470 + 2 = s(p(+(x,x470)))
      
      s(p(+(x,x470))) = 4x + 4x470 + 2 >= 4x + 4x470 = +(x,x470)
      
      +(p(x),p(x472)) = 4x + 4x472 + 8 >= 4x + 4x472 + 5 = p(+(p(x),x472))
      
      +(p(x),p(x472)) = 4x + 4x472 + 8 >= 4x + 4x472 + 5 = p(+(x,p(x472)))
      
      p(+(p(x),x472)) = 4x + 4x472 + 5 >= 4x + 4x472 + 2 = p(p(+(x,x472)))
      
      p(+(x,p(x472))) = 4x + 4x472 + 5 >= 4x + 4x472 + 2 = p(p(+(x,x472)))
      
      +(x,p(x474)) = 4x + 4x474 + 4 >= 4x + 4x474 + 1 = p(+(x,x474))
      
      +(x,p(x474)) = 4x + 4x474 + 4 >= 4x + 4x474 + 4 = +(p(x474),x)
      
      p(+(x,x474)) = 4x + 4x474 + 1 >= 4x + 4x474 + 1 = p(+(x474,x))
      
      +(p(x474),x) = 4x + 4x474 + 4 >= 4x + 4x474 + 1 = p(+(x474,x))
      
      -(+(x,p(x476))) = 8x + 8x476 + 8 >= 8x + 8x476 + 2 = -(p(+(x,x476)))
      
      -(+(x,p(x476))) = 8x + 8x476 + 8 >= 8x + 8x476 + 8 = +(-(x),-(p(x476)))
      
      -(p(+(x,x476))) = 8x + 8x476 + 2 >= 8x + 8x476 + 1 = s(-(+(x,x476)))
      
      s(-(+(x,x476))) = 8x + 8x476 + 1 >= 8x + 8x476 + 1 = s(+(-(x),-(x476)))
      
      +(-(x),-(p(x476))) = 8x + 8x476 + 8 >= 8x + 8x476 + 4 = +(-(x),s(-(x476)))
      
      +(-(x),s(-(x476))) = 8x + 8x476 + 4 >= 8x + 8x476 + 1 = s(+(-(x),-(x476)))
      
      +(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(x482),0()) = 4x482 + 4 >= 4x482 + 1 = s(+(x482,0()))
      
      +(s(x482),0()) = 4x482 + 4 >= x482 + 1 = s(x482)
      
      s(+(x482,0())) = 4x482 + 1 >= x482 + 1 = s(x482)
      
      +(s(x484),s(y)) = 4x484 + 4y + 8 >= 4x484 + 4y + 5 = s(+(x484,s(y)))
      
      +(s(x484),s(y)) = 4x484 + 4y + 8 >= 4x484 + 4y + 5 = s(+(s(x484),y))
      
      s(+(x484,s(y))) = 4x484 + 4y + 5 >= 4x484 + 4y + 2 = s(s(+(x484,y)))
      
      s(+(s(x484),y)) = 4x484 + 4y + 5 >= 4x484 + 4y + 2 = s(s(+(x484,y)))
      
      +(s(x486),p(y)) = 4x486 + 4y + 8 >= 4x486 + 4y + 5 = s(+(x486,p(y)))
      
      +(s(x486),p(y)) = 4x486 + 4y + 8 >= 4x486 + 4y + 5 = p(+(s(x486),y))
      
      s(+(x486,p(y))) = 4x486 + 4y + 5 >= 4x486 + 4y + 2 = s(p(+(x486,y)))
      
      s(p(+(x486,y))) = 4x486 + 4y + 2 >= 4x486 + 4y = +(x486,y)
      
      p(+(s(x486),y)) = 4x486 + 4y + 5 >= 4x486 + 4y + 2 = p(s(+(x486,y)))
      
      p(s(+(x486,y))) = 4x486 + 4y + 2 >= 4x486 + 4y = +(x486,y)
      
      +(s(x488),y) = 4x488 + 4y + 4 >= 4x488 + 4y + 1 = s(+(x488,y))
      
      +(s(x488),y) = 4x488 + 4y + 4 >= 4x488 + 4y + 4 = +(y,s(x488))
      
      s(+(x488,y)) = 4x488 + 4y + 1 >= 4x488 + 4y + 1 = s(+(y,x488))
      
      +(y,s(x488)) = 4x488 + 4y + 4 >= 4x488 + 4y + 1 = s(+(y,x488))
      
      -(+(s(x490),y)) = 8x490 + 8y + 8 >= 8x490 + 8y + 2 = -(s(+(x490,y)))
      
      -(+(s(x490),y)) = 8x490 + 8y + 8 >= 8x490 + 8y + 8 = +(-(s(x490)),-(y))
      
      -(s(+(x490,y))) = 8x490 + 8y + 2 >= 8x490 + 8y + 1 = p(-(+(x490,y)))
      
      p(-(+(x490,y))) = 8x490 + 8y + 1 >= 8x490 + 8y + 1 = p(+(-(x490),-(y)))
      
      +(-(s(x490)),-(y)) = 8x490 + 8y + 8 >= 8x490 + 8y + 4 = +(p(-(x490)),-(y))
      
      +(p(-(x490)),-(y)) = 8x490 + 8y + 4 >= 8x490 + 8y + 1 = p(+(-(x490),-(y)))
      
      +(p(x492),0()) = 4x492 + 4 >= 4x492 + 1 = p(+(x492,0()))
      
      +(p(x492),0()) = 4x492 + 4 >= x492 + 1 = p(x492)
      
      p(+(x492,0())) = 4x492 + 1 >= x492 + 1 = p(x492)
      
      +(p(x494),s(y)) = 4x494 + 4y + 8 >= 4x494 + 4y + 5 = p(+(x494,s(y)))
      
      +(p(x494),s(y)) = 4x494 + 4y + 8 >= 4x494 + 4y + 5 = s(+(p(x494),y))
      
      p(+(x494,s(y))) = 4x494 + 4y + 5 >= 4x494 + 4y + 2 = p(s(+(x494,y)))
      
      p(s(+(x494,y))) = 4x494 + 4y + 2 >= 4x494 + 4y = +(x494,y)
      
      s(+(p(x494),y)) = 4x494 + 4y + 5 >= 4x494 + 4y + 2 = s(p(+(x494,y)))
      
      s(p(+(x494,y))) = 4x494 + 4y + 2 >= 4x494 + 4y = +(x494,y)
      
      +(p(x496),p(y)) = 4x496 + 4y + 8 >= 4x496 + 4y + 5 = p(+(x496,p(y)))
      
      +(p(x496),p(y)) = 4x496 + 4y + 8 >= 4x496 + 4y + 5 = p(+(p(x496),y))
      
      p(+(x496,p(y))) = 4x496 + 4y + 5 >= 4x496 + 4y + 2 = p(p(+(x496,y)))
      
      p(+(p(x496),y)) = 4x496 + 4y + 5 >= 4x496 + 4y + 2 = p(p(+(x496,y)))
      
      +(p(x498),y) = 4x498 + 4y + 4 >= 4x498 + 4y + 1 = p(+(x498,y))
      
      +(p(x498),y) = 4x498 + 4y + 4 >= 4x498 + 4y + 4 = +(y,p(x498))
      
      p(+(x498,y)) = 4x498 + 4y + 1 >= 4x498 + 4y + 1 = p(+(y,x498))
      
      +(y,p(x498)) = 4x498 + 4y + 4 >= 4x498 + 4y + 1 = p(+(y,x498))
      
      -(+(p(x500),y)) = 8x500 + 8y + 8 >= 8x500 + 8y + 2 = -(p(+(x500,y)))
      
      -(+(p(x500),y)) = 8x500 + 8y + 8 >= 8x500 + 8y + 8 = +(-(p(x500)),-(y))
      
      -(p(+(x500,y))) = 8x500 + 8y + 2 >= 8x500 + 8y + 1 = s(-(+(x500,y)))
      
      s(-(+(x500,y))) = 8x500 + 8y + 1 >= 8x500 + 8y + 1 = s(+(-(x500),-(y)))
      
      +(-(p(x500)),-(y)) = 8x500 + 8y + 8 >= 8x500 + 8y + 4 = +(s(-(x500)),-(y))
      
      +(s(-(x500)),-(y)) = 8x500 + 8y + 4 >= 8x500 + 8y + 1 = s(+(-(x500),-(y)))
      
      +(x,s(p(x502))) = 4x + 4x502 + 8 >= 4x + 4x502 = +(x,x502)
      
      +(x,s(p(x502))) = 4x + 4x502 + 8 >= 4x + 4x502 + 5 = s(+(x,p(x502)))
      
      s(+(x,p(x502))) = 4x + 4x502 + 5 >= 4x + 4x502 + 2 = s(p(+(x,x502)))
      
      s(p(+(x,x502))) = 4x + 4x502 + 2 >= 4x + 4x502 = +(x,x502)
      
      +(s(p(x503)),y) = 4x503 + 4y + 8 >= 4x503 + 4y = +(x503,y)
      
      +(s(p(x503)),y) = 4x503 + 4y + 8 >= 4x503 + 4y + 5 = s(+(p(x503),y))
      
      s(+(p(x503),y)) = 4x503 + 4y + 5 >= 4x503 + 4y + 2 = s(p(+(x503,y)))
      
      s(p(+(x503,y))) = 4x503 + 4y + 2 >= 4x503 + 4y = +(x503,y)
      
      p(s(p(x504))) = x504 + 3 >= x504 + 1 = p(x504)
      
      p(s(p(x504))) = x504 + 3 >= x504 + 1 = p(x504)
      
      -(s(p(x505))) = 2x505 + 4 >= 2x505 = -(x505)
      
      -(s(p(x505))) = 2x505 + 4 >= 2x505 + 3 = p(-(p(x505)))
      
      p(-(p(x505))) = 2x505 + 3 >= 2x505 + 2 = p(s(-(x505)))
      
      p(s(-(x505))) = 2x505 + 2 >= 2x505 = -(x505)
      
      +(x,p(s(x506))) = 4x + 4x506 + 8 >= 4x + 4x506 = +(x,x506)
      
      +(x,p(s(x506))) = 4x + 4x506 + 8 >= 4x + 4x506 + 5 = p(+(x,s(x506)))
      
      p(+(x,s(x506))) = 4x + 4x506 + 5 >= 4x + 4x506 + 2 = p(s(+(x,x506)))
      
      p(s(+(x,x506))) = 4x + 4x506 + 2 >= 4x + 4x506 = +(x,x506)
      
      +(p(s(x507)),y) = 4x507 + 4y + 8 >= 4x507 + 4y = +(x507,y)
      
      +(p(s(x507)),y) = 4x507 + 4y + 8 >= 4x507 + 4y + 5 = p(+(s(x507),y))
      
      p(+(s(x507),y)) = 4x507 + 4y + 5 >= 4x507 + 4y + 2 = p(s(+(x507,y)))
      
      p(s(+(x507,y))) = 4x507 + 4y + 2 >= 4x507 + 4y = +(x507,y)
      
      s(p(s(x508))) = x508 + 3 >= x508 + 1 = s(x508)
      
      s(p(s(x508))) = x508 + 3 >= x508 + 1 = s(x508)
      
      -(p(s(x509))) = 2x509 + 4 >= 2x509 = -(x509)
      
      -(p(s(x509))) = 2x509 + 4 >= 2x509 + 3 = s(-(s(x509)))
      
      s(-(s(x509))) = 2x509 + 3 >= 2x509 + 2 = s(p(-(x509)))
      
      s(p(-(x509))) = 2x509 + 2 >= 2x509 = -(x509)
      
      +(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(),x458)) -> s(x458)
       +(x,s(x464)) -> +(s(x464),x)
       s(+(x,x464)) -> s(+(x464,x))
       -(+(x,s(x466))) -> +(-(x),-(s(x466)))
       p(-(+(x,x466))) -> p(+(-(x),-(x466)))
       p(+(0(),x468)) -> p(x468)
       +(x,p(x474)) -> +(p(x474),x)
       p(+(x,x474)) -> p(+(x474,x))
       -(+(x,p(x476))) -> +(-(x),-(p(x476)))
       s(-(+(x,x476))) -> s(+(-(x),-(x476)))
       +(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(+(x482,0())) -> s(x482)
       +(s(x488),y) -> +(y,s(x488))
       s(+(x488,y)) -> s(+(y,x488))
       -(+(s(x490),y)) -> +(-(s(x490)),-(y))
       p(-(+(x490,y))) -> p(+(-(x490),-(y)))
       p(+(x492,0())) -> p(x492)
       +(p(x498),y) -> +(y,p(x498))
       p(+(x498,y)) -> p(+(y,x498))
       -(+(p(x500),y)) -> +(-(p(x500)),-(y))
       s(-(+(x500,y))) -> s(+(-(x500),-(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(),x458)) = 2x458 + 6 >= x458 = s(x458)
       
       +(x,s(x464)) = 2x + 2x464 + 2 >= 2x + 2x464 + 2 = +(s(x464),x)
       
       s(+(x,x464)) = 2x + 2x464 + 2 >= 2x + 2x464 + 2 = s(+(x464,x))
       
       -(+(x,s(x466))) = 4x + 4x466 + 4 >= 4x + 4x466 + 2 = +(-(x),-(s(x466)))
       
       p(-(+(x,x466))) = 4x + 4x466 + 6 >= 4x + 4x466 + 4 = p(+(-(x),-(x466)))
       
       p(+(0(),x468)) = 2x468 + 8 >= x468 + 2 = p(x468)
       
       +(x,p(x474)) = 2x + 2x474 + 6 >= 2x + 2x474 + 6 = +(p(x474),x)
       
       p(+(x,x474)) = 2x + 2x474 + 4 >= 2x + 2x474 + 4 = p(+(x474,x))
       
       -(+(x,p(x476))) = 4x + 4x476 + 12 >= 4x + 4x476 + 10 = +(-(x),-(p(x476)))
       
       s(-(+(x,x476))) = 4x + 4x476 + 4 >= 4x + 4x476 + 2 = s(+(-(x),-(x476)))
       
       +(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(+(x482,0())) = 2x482 + 6 >= x482 = s(x482)
       
       +(s(x488),y) = 2x488 + 2y + 2 >= 2x488 + 2y + 2 = +(y,s(x488))
       
       s(+(x488,y)) = 2x488 + 2y + 2 >= 2x488 + 2y + 2 = s(+(y,x488))
       
       -(+(s(x490),y)) = 4x490 + 4y + 4 >= 4x490 + 4y + 2 = +(-(s(x490)),-(y))
       
       p(-(+(x490,y))) = 4x490 + 4y + 6 >= 4x490 + 4y + 4 = p(+(-(x490),-(y)))
       
       p(+(x492,0())) = 2x492 + 8 >= x492 + 2 = p(x492)
       
       +(p(x498),y) = 2x498 + 2y + 6 >= 2x498 + 2y + 6 = +(y,p(x498))
       
       p(+(x498,y)) = 2x498 + 2y + 4 >= 2x498 + 2y + 4 = p(+(y,x498))
       
       -(+(p(x500),y)) = 4x500 + 4y + 12 >= 4x500 + 4y + 10 = +(-(p(x500)),-(y))
       
       s(-(+(x500,y))) = 4x500 + 4y + 4 >= 4x500 + 4y + 2 = s(+(-(x500),-(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(x464)) -> +(s(x464),x)
        s(+(x,x464)) -> s(+(x464,x))
        +(x,p(x474)) -> +(p(x474),x)
        p(+(x,x474)) -> p(+(x474,x))
        +(0(),y) -> +(y,0())
        +(s(x488),y) -> +(y,s(x488))
        s(+(x488,y)) -> s(+(y,x488))
        +(p(x498),y) -> +(y,p(x498))
        p(+(x498,y)) -> p(+(y,x498))
        +(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:
        
       Decreasing Processor:
        The following diagrams are decreasing:
        peak:
         0() <-0|[==1]- +(0(),0()) -3|[==1]-> 0()
        joins (1):
         
         
        peak:
         s(x) <-0|[==1]- +(s(x),0()) -4|[==1]-> s(+(x,0()))
        joins (1):
         
         s(+(x,0())) -0|0[>>0]-> s(x)
        peak:
         p(x) <-0|[==1]- +(p(x),0()) -5|[==1]-> p(+(x,0()))
        joins (1):
         
         p(+(x,0())) -0|0[>>0]-> p(x)
        peak:
         x <-0|[==1]- +(x,0()) -11|[==1]-> +(0(),x)
        joins (1):
         
         +(0(),x) -3|[==1]-> x
        peak:
         -(x) <-0|0[==1]- -(+(x,0())) -12|[==1]-> +(-(x),-(0()))
        joins (1):
         
         +(-(x),-(0())) -8|1[>>0]-> +(-(x),0()) -0|[>>0]-> -(x)
        peak:
         s(+(0(),x458)) <-1|[==1]- +(0(),s(x458)) -3|[==1]-> s(x458)
        joins (1):
         s(+(0(),x458)) -3|0[>>0]-> s(x458)
         
        peak:
         s(+(s(x),x460)) <-1|[==1]- +(s(x),s(x460)) -4|[==1]-> s(+(x,s(x460)))
        joins (1):
         s(+(s(x),x460)) -4|0[>>0]-> s(s(+(x,x460)))
         s(+(x,s(x460))) -1|0[>>0]-> s(s(+(x,x460)))
        peak:
         s(+(p(x),x462)) <-1|[==1]- +(p(x),s(x462)) -5|[==1]-> p(+(x,s(x462)))
        joins (1):
         s(+(p(x),x462)) -5|0[>>0]-> s(p(+(x,x462))) -6|[>>0]-> +(x,x462)
         p(+(x,s(x462))) -1|0[>>0]-> p(s(+(x,x462))) -7|[>>0]-> +(x,x462)
        peak:
         s(+(x,x464)) <-1|[==1]- +(x,s(x464)) -11|[==1]-> +(s(x464),x)
        joins (1):
         s(+(x,x464)) -11|0[>>0]-> s(+(x464,x))
         +(s(x464),x) -4|[==1]-> s(+(x464,x))
        peak:
         -(s(+(x,x466))) <-1|0[==1]- -(+(x,s(x466))) -12|[==1]-> +(-(x),-(s(x466)))
        joins (1):
         -(s(+(x,x466))) -9|[>>0]-> p(-(+(x,x466))) -12|0[>>0]-> p(+(-(x),-(x466)))
         +(-(x),-(s(x466))) -9|1[>>0]-> +(-(x),p(-(x466))) -2|[>>0]-> p(+(-(x),-(x466)))
        peak:
         p(+(0(),x468)) <-2|[==1]- +(0(),p(x468)) -3|[==1]-> p(x468)
        joins (1):
         p(+(0(),x468)) -3|0[>>0]-> p(x468)
         
        peak:
         p(+(s(x),x470)) <-2|[==1]- +(s(x),p(x470)) -4|[==1]-> s(+(x,p(x470)))
        joins (1):
         p(+(s(x),x470)) -4|0[>>0]-> p(s(+(x,x470))) -7|[>>0]-> +(x,x470)
         s(+(x,p(x470))) -2|0[>>0]-> s(p(+(x,x470))) -6|[>>0]-> +(x,x470)
        peak:
         p(+(p(x),x472)) <-2|[==1]- +(p(x),p(x472)) -5|[==1]-> p(+(x,p(x472)))
        joins (1):
         p(+(p(x),x472)) -5|0[>>0]-> p(p(+(x,x472)))
         p(+(x,p(x472))) -2|0[>>0]-> p(p(+(x,x472)))
        peak:
         p(+(x,x474)) <-2|[==1]- +(x,p(x474)) -11|[==1]-> +(p(x474),x)
        joins (1):
         p(+(x,x474)) -11|0[>>0]-> p(+(x474,x))
         +(p(x474),x) -5|[==1]-> p(+(x474,x))
        peak:
         -(p(+(x,x476))) <-2|0[==1]- -(+(x,p(x476))) -12|[==1]-> +(-(x),-(p(x476)))
        joins (1):
         -(p(+(x,x476))) -10|[>>0]-> s(-(+(x,x476))) -12|0[>>0]-> s(+(-(x),-(x476)))
         +(-(x),-(p(x476))) -10|1[>>0]-> +(-(x),s(-(x476))) -1|[>>0]-> s(+(-(x),-(x476)))
        peak:
         0() <-3|[==1]- +(0(),0()) -0|[==1]-> 0()
        joins (1):
         
         
        peak:
         s(y) <-3|[==1]- +(0(),s(y)) -1|[==1]-> s(+(0(),y))
        joins (1):
         
         s(+(0(),y)) -3|0[>>0]-> s(y)
        peak:
         p(y) <-3|[==1]- +(0(),p(y)) -2|[==1]-> p(+(0(),y))
        joins (1):
         
         p(+(0(),y)) -3|0[>>0]-> p(y)
        peak:
         y <-3|[==1]- +(0(),y) -11|[==1]-> +(y,0())
        joins (1):
         
         +(y,0()) -0|[==1]-> y
        peak:
         -(y) <-3|0[==1]- -(+(0(),y)) -12|[==1]-> +(-(0()),-(y))
        joins (1):
         
         +(-(0()),-(y)) -8|0[>>0]-> +(0(),-(y)) -3|[>>0]-> -(y)
        peak:
         s(+(x482,0())) <-4|[==1]- +(s(x482),0()) -0|[==1]-> s(x482)
        joins (1):
         s(+(x482,0())) -0|0[>>0]-> s(x482)
         
        peak:
         s(+(x484,s(y))) <-4|[==1]- +(s(x484),s(y)) -1|[==1]-> s(+(s(x484),y))
        joins (1):
         s(+(x484,s(y))) -1|0[>>0]-> s(s(+(x484,y)))
         s(+(s(x484),y)) -4|0[>>0]-> s(s(+(x484,y)))
        peak:
         s(+(x486,p(y))) <-4|[==1]- +(s(x486),p(y)) -2|[==1]-> p(+(s(x486),y))
        joins (1):
         s(+(x486,p(y))) -2|0[>>0]-> s(p(+(x486,y))) -6|[>>0]-> +(x486,y)
         p(+(s(x486),y)) -4|0[>>0]-> p(s(+(x486,y))) -7|[>>0]-> +(x486,y)
        peak:
         s(+(x488,y)) <-4|[==1]- +(s(x488),y) -11|[==1]-> +(y,s(x488))
        joins (1):
         s(+(x488,y)) -11|0[>>0]-> s(+(y,x488))
         +(y,s(x488)) -1|[==1]-> s(+(y,x488))
        peak:
         -(s(+(x490,y))) <-4|0[==1]- -(+(s(x490),y)) -12|[==1]-> +(-(s(x490)),-(y))
        joins (1):
         -(s(+(x490,y))) -9|[>>0]-> p(-(+(x490,y))) -12|0[>>0]-> p(+(-(x490),-(y)))
         +(-(s(x490)),-(y)) -9|0[>>0]-> +(p(-(x490)),-(y)) -5|[>>0]-> p(+(-(x490),-(y)))
        peak:
         p(+(x492,0())) <-5|[==1]- +(p(x492),0()) -0|[==1]-> p(x492)
        joins (1):
         p(+(x492,0())) -0|0[>>0]-> p(x492)
         
        peak:
         p(+(x494,s(y))) <-5|[==1]- +(p(x494),s(y)) -1|[==1]-> s(+(p(x494),y))
        joins (1):
         p(+(x494,s(y))) -1|0[>>0]-> p(s(+(x494,y))) -7|[>>0]-> +(x494,y)
         s(+(p(x494),y)) -5|0[>>0]-> s(p(+(x494,y))) -6|[>>0]-> +(x494,y)
        peak:
         p(+(x496,p(y))) <-5|[==1]- +(p(x496),p(y)) -2|[==1]-> p(+(p(x496),y))
        joins (1):
         p(+(x496,p(y))) -2|0[>>0]-> p(p(+(x496,y)))
         p(+(p(x496),y)) -5|0[>>0]-> p(p(+(x496,y)))
        peak:
         p(+(x498,y)) <-5|[==1]- +(p(x498),y) -11|[==1]-> +(y,p(x498))
        joins (1):
         p(+(x498,y)) -11|0[>>0]-> p(+(y,x498))
         +(y,p(x498)) -2|[==1]-> p(+(y,x498))
        peak:
         -(p(+(x500,y))) <-5|0[==1]- -(+(p(x500),y)) -12|[==1]-> +(-(p(x500)),-(y))
        joins (1):
         -(p(+(x500,y))) -10|[>>0]-> s(-(+(x500,y))) -12|0[>>0]-> s(+(-(x500),-(y)))
         +(-(p(x500)),-(y)) -10|0[>>0]-> +(s(-(x500)),-(y)) -4|[>>0]-> s(+(-(x500),-(y)))
        peak:
         +(x,x502) <-6|1[==1]- +(x,s(p(x502))) -1|[==1]-> s(+(x,p(x502)))
        joins (1):
         
         s(+(x,p(x502))) -2|0[>>0]-> s(p(+(x,x502))) -6|[>>0]-> +(x,x502)
        peak:
         +(x503,y) <-6|0[==1]- +(s(p(x503)),y) -4|[==1]-> s(+(p(x503),y))
        joins (1):
         
         s(+(p(x503),y)) -5|0[>>0]-> s(p(+(x503,y))) -6|[>>0]-> +(x503,y)
        peak:
         p(x504) <-6|0[==1]- p(s(p(x504))) -7|[==1]-> p(x504)
        joins (1):
         
         
        peak:
         -(x505) <-6|0[==1]- -(s(p(x505))) -9|[==1]-> p(-(p(x505)))
        joins (1):
         
         p(-(p(x505))) -10|0[>>0]-> p(s(-(x505))) -7|[>>0]-> -(x505)
        peak:
         +(x,x506) <-7|1[==1]- +(x,p(s(x506))) -2|[==1]-> p(+(x,s(x506)))
        joins (1):
         
         p(+(x,s(x506))) -1|0[>>0]-> p(s(+(x,x506))) -7|[>>0]-> +(x,x506)
        peak:
         +(x507,y) <-7|0[==1]- +(p(s(x507)),y) -5|[==1]-> p(+(s(x507),y))
        joins (1):
         
         p(+(s(x507),y)) -4|0[>>0]-> p(s(+(x507,y))) -7|[>>0]-> +(x507,y)
        peak:
         s(x508) <-7|0[==1]- s(p(s(x508))) -6|[==1]-> s(x508)
        joins (1):
         
         
        peak:
         -(x509) <-7|0[==1]- -(p(s(x509))) -10|[==1]-> s(-(s(x509)))
        joins (1):
         
         s(-(s(x509))) -9|0[>>0]-> s(p(-(x509))) -6|[>>0]-> -(x509)
        peak:
         +(0(),x) <-11|[==1]- +(x,0()) -0|[==1]-> x
        joins (1):
         +(0(),x) -3|[==1]-> x
         
        peak:
         +(s(y),x) <-11|[==1]- +(x,s(y)) -1|[==1]-> s(+(x,y))
        joins (1):
         +(s(y),x) -4|[==1]-> s(+(y,x))
         s(+(x,y)) -11|0[>>0]-> s(+(y,x))
        peak:
         +(p(y),x) <-11|[==1]- +(x,p(y)) -2|[==1]-> p(+(x,y))
        joins (1):
         +(p(y),x) -5|[==1]-> p(+(y,x))
         p(+(x,y)) -11|0[>>0]-> p(+(y,x))
        peak:
         +(y,0()) <-11|[==1]- +(0(),y) -3|[==1]-> y
        joins (1):
         +(y,0()) -0|[==1]-> y
         
        peak:
         +(y,s(x)) <-11|[==1]- +(s(x),y) -4|[==1]-> s(+(x,y))
        joins (1):
         +(y,s(x)) -1|[==1]-> s(+(y,x))
         s(+(x,y)) -11|0[>>0]-> s(+(y,x))
        peak:
         +(y,p(x)) <-11|[==1]- +(p(x),y) -5|[==1]-> p(+(x,y))
        joins (1):
         +(y,p(x)) -2|[==1]-> p(+(y,x))
         p(+(x,y)) -11|0[>>0]-> p(+(y,x))
        peak:
         -(+(y,x)) <-11|0[==1]- -(+(x,y)) -12|[==1]-> +(-(x),-(y))
        joins (1):
         -(+(y,x)) -12|[==1]-> +(-(y),-(x))
         +(-(x),-(y)) -11|[>>0]-> +(-(y),-(x))
        Qed