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
 +(x,y) -> +(y,x)

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   +(0)(x) -> +(1)(x)
   +(1)(y) -> +(0)(y)
   p(0)(s(0)(x)) -> x
   s(0)(p(0)(x)) -> x
   +(0)(p(0)(x)) -> p(0)(+(0)(x))
   +(1)(y) -> p(0)(+(1)(y))
   +(0)(s(0)(x)) -> s(0)(+(0)(x))
   +(1)(y) -> s(0)(+(1)(y))
   +(1)(y) -> y
   +(0)(x) -> p(0)(+(0)(x))
   +(1)(p(0)(y)) -> p(0)(+(1)(y))
   +(0)(x) -> s(0)(+(0)(x))
   +(1)(s(0)(y)) -> s(0)(+(1)(y))
   +(0)(x) -> x
  critical peaks: 36
  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()) -8|[]-> +(0(),x)
  s(+(0(),x246)) <-1|[]- +(0(),s(x246)) -3|[]-> s(x246)
  s(+(s(x),x248)) <-1|[]- +(s(x),s(x248)) -4|[]-> s(+(x,s(x248)))
  s(+(p(x),x250)) <-1|[]- +(p(x),s(x250)) -5|[]-> p(+(x,s(x250)))
  s(+(x,x252)) <-1|[]- +(x,s(x252)) -8|[]-> +(s(x252),x)
  p(+(0(),x254)) <-2|[]- +(0(),p(x254)) -3|[]-> p(x254)
  p(+(s(x),x256)) <-2|[]- +(s(x),p(x256)) -4|[]-> s(+(x,p(x256)))
  p(+(p(x),x258)) <-2|[]- +(p(x),p(x258)) -5|[]-> p(+(x,p(x258)))
  p(+(x,x260)) <-2|[]- +(x,p(x260)) -8|[]-> +(p(x260),x)
  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) -8|[]-> +(y,0())
  s(+(x265,0())) <-4|[]- +(s(x265),0()) -0|[]-> s(x265)
  s(+(x267,s(y))) <-4|[]- +(s(x267),s(y)) -1|[]-> s(+(s(x267),y))
  s(+(x269,p(y))) <-4|[]- +(s(x269),p(y)) -2|[]-> p(+(s(x269),y))
  s(+(x271,y)) <-4|[]- +(s(x271),y) -8|[]-> +(y,s(x271))
  p(+(x273,0())) <-5|[]- +(p(x273),0()) -0|[]-> p(x273)
  p(+(x275,s(y))) <-5|[]- +(p(x275),s(y)) -1|[]-> s(+(p(x275),y))
  p(+(x277,p(y))) <-5|[]- +(p(x277),p(y)) -2|[]-> p(+(p(x277),y))
  p(+(x279,y)) <-5|[]- +(p(x279),y) -8|[]-> +(y,p(x279))
  +(x,x281) <-6|1[]- +(x,s(p(x281))) -1|[]-> s(+(x,p(x281)))
  +(x282,y) <-6|0[]- +(s(p(x282)),y) -4|[]-> s(+(p(x282),y))
  p(x283) <-6|0[]- p(s(p(x283))) -7|[]-> p(x283)
  +(x,x284) <-7|1[]- +(x,p(s(x284))) -2|[]-> p(+(x,s(x284)))
  +(x285,y) <-7|0[]- +(p(s(x285)),y) -5|[]-> p(+(s(x285),y))
  s(x286) <-7|0[]- s(p(s(x286))) -6|[]-> s(x286)
  +(0(),x) <-8|[]- +(x,0()) -0|[]-> x
  +(s(y),x) <-8|[]- +(x,s(y)) -1|[]-> s(+(x,y))
  +(p(y),x) <-8|[]- +(x,p(y)) -2|[]-> p(+(x,y))
  +(y,0()) <-8|[]- +(0(),y) -3|[]-> y
  +(y,s(x)) <-8|[]- +(s(x),y) -4|[]-> s(+(x,y))
  +(y,p(x)) <-8|[]- +(p(x),y) -5|[]-> p(+(x,y))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [s(0)](x0) = x0,
    
    [p(0)](x0) = x0,
    
    [+(1)](x0) = 2x0 + 1,
    
    [+(0)](x0) = 2x0 + 1
   orientation:
    +(0)(x) = 2x + 1 >= 2x + 1 = +(1)(x)
    
    +(1)(y) = 2y + 1 >= 2y + 1 = +(0)(y)
    
    p(0)(s(0)(x)) = x >= x = x
    
    s(0)(p(0)(x)) = x >= x = x
    
    +(0)(p(0)(x)) = 2x + 1 >= 2x + 1 = p(0)(+(0)(x))
    
    +(1)(y) = 2y + 1 >= 2y + 1 = p(0)(+(1)(y))
    
    +(0)(s(0)(x)) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x))
    
    +(1)(y) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y))
    
    +(1)(y) = 2y + 1 >= y = y
    
    +(0)(x) = 2x + 1 >= 2x + 1 = p(0)(+(0)(x))
    
    +(1)(p(0)(y)) = 2y + 1 >= 2y + 1 = p(0)(+(1)(y))
    
    +(0)(x) = 2x + 1 >= 2x + 1 = s(0)(+(0)(x))
    
    +(1)(s(0)(y)) = 2y + 1 >= 2y + 1 = s(0)(+(1)(y))
    
    +(0)(x) = 2x + 1 >= x = x
   problem:
    
    strict:
     
    weak:
     +(0)(x) -> +(1)(x)
     +(1)(y) -> +(0)(y)
     p(0)(s(0)(x)) -> x
     s(0)(p(0)(x)) -> x
     +(0)(p(0)(x)) -> p(0)(+(0)(x))
     +(1)(y) -> p(0)(+(1)(y))
     +(0)(s(0)(x)) -> s(0)(+(0)(x))
     +(1)(y) -> s(0)(+(1)(y))
     +(0)(x) -> p(0)(+(0)(x))
     +(1)(p(0)(y)) -> p(0)(+(1)(y))
     +(0)(x) -> s(0)(+(0)(x))
     +(1)(s(0)(y)) -> s(0)(+(1)(y))
   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
     +(0(),s(x246)) -> s(+(0(),x246))
     +(0(),s(x246)) -> s(x246)
     s(+(0(),x246)) -> s(x246)
     +(s(x),s(x248)) -> s(+(s(x),x248))
     +(s(x),s(x248)) -> s(+(x,s(x248)))
     s(+(s(x),x248)) -> s(s(+(x,x248)))
     s(+(x,s(x248))) -> s(s(+(x,x248)))
     +(p(x),s(x250)) -> s(+(p(x),x250))
     +(p(x),s(x250)) -> p(+(x,s(x250)))
     s(+(p(x),x250)) -> s(p(+(x,x250)))
     s(p(+(x,x250))) -> +(x,x250)
     p(+(x,s(x250))) -> p(s(+(x,x250)))
     p(s(+(x,x250))) -> +(x,x250)
     +(x,s(x252)) -> s(+(x,x252))
     +(x,s(x252)) -> +(s(x252),x)
     s(+(x,x252)) -> s(+(x252,x))
     +(s(x252),x) -> s(+(x252,x))
     +(0(),p(x254)) -> p(+(0(),x254))
     +(0(),p(x254)) -> p(x254)
     p(+(0(),x254)) -> p(x254)
     +(s(x),p(x256)) -> p(+(s(x),x256))
     +(s(x),p(x256)) -> s(+(x,p(x256)))
     p(+(s(x),x256)) -> p(s(+(x,x256)))
     p(s(+(x,x256))) -> +(x,x256)
     s(+(x,p(x256))) -> s(p(+(x,x256)))
     s(p(+(x,x256))) -> +(x,x256)
     +(p(x),p(x258)) -> p(+(p(x),x258))
     +(p(x),p(x258)) -> p(+(x,p(x258)))
     p(+(p(x),x258)) -> p(p(+(x,x258)))
     p(+(x,p(x258))) -> p(p(+(x,x258)))
     +(x,p(x260)) -> p(+(x,x260))
     +(x,p(x260)) -> +(p(x260),x)
     p(+(x,x260)) -> p(+(x260,x))
     +(p(x260),x) -> p(+(x260,x))
     +(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
     +(s(x265),0()) -> s(+(x265,0()))
     +(s(x265),0()) -> s(x265)
     s(+(x265,0())) -> s(x265)
     +(s(x267),s(y)) -> s(+(x267,s(y)))
     +(s(x267),s(y)) -> s(+(s(x267),y))
     s(+(x267,s(y))) -> s(s(+(x267,y)))
     s(+(s(x267),y)) -> s(s(+(x267,y)))
     +(s(x269),p(y)) -> s(+(x269,p(y)))
     +(s(x269),p(y)) -> p(+(s(x269),y))
     s(+(x269,p(y))) -> s(p(+(x269,y)))
     s(p(+(x269,y))) -> +(x269,y)
     p(+(s(x269),y)) -> p(s(+(x269,y)))
     p(s(+(x269,y))) -> +(x269,y)
     +(s(x271),y) -> s(+(x271,y))
     +(s(x271),y) -> +(y,s(x271))
     s(+(x271,y)) -> s(+(y,x271))
     +(y,s(x271)) -> s(+(y,x271))
     +(p(x273),0()) -> p(+(x273,0()))
     +(p(x273),0()) -> p(x273)
     p(+(x273,0())) -> p(x273)
     +(p(x275),s(y)) -> p(+(x275,s(y)))
     +(p(x275),s(y)) -> s(+(p(x275),y))
     p(+(x275,s(y))) -> p(s(+(x275,y)))
     p(s(+(x275,y))) -> +(x275,y)
     s(+(p(x275),y)) -> s(p(+(x275,y)))
     s(p(+(x275,y))) -> +(x275,y)
     +(p(x277),p(y)) -> p(+(x277,p(y)))
     +(p(x277),p(y)) -> p(+(p(x277),y))
     p(+(x277,p(y))) -> p(p(+(x277,y)))
     p(+(p(x277),y)) -> p(p(+(x277,y)))
     +(p(x279),y) -> p(+(x279,y))
     +(p(x279),y) -> +(y,p(x279))
     p(+(x279,y)) -> p(+(y,x279))
     +(y,p(x279)) -> p(+(y,x279))
     +(x,s(p(x281))) -> +(x,x281)
     +(x,s(p(x281))) -> s(+(x,p(x281)))
     s(+(x,p(x281))) -> s(p(+(x,x281)))
     s(p(+(x,x281))) -> +(x,x281)
     +(s(p(x282)),y) -> +(x282,y)
     +(s(p(x282)),y) -> s(+(p(x282),y))
     s(+(p(x282),y)) -> s(p(+(x282,y)))
     s(p(+(x282,y))) -> +(x282,y)
     p(s(p(x283))) -> p(x283)
     p(s(p(x283))) -> p(x283)
     +(x,p(s(x284))) -> +(x,x284)
     +(x,p(s(x284))) -> p(+(x,s(x284)))
     p(+(x,s(x284))) -> p(s(+(x,x284)))
     p(s(+(x,x284))) -> +(x,x284)
     +(p(s(x285)),y) -> +(x285,y)
     +(p(s(x285)),y) -> p(+(s(x285),y))
     p(+(s(x285),y)) -> p(s(+(x285,y)))
     p(s(+(x285,y))) -> +(x285,y)
     s(p(s(x286))) -> s(x286)
     s(p(s(x286))) -> s(x286)
     +(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))
    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
     +(x,y) -> +(y,x)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [p](x0) = x0 + 6,
      
      [s](x0) = x0 + 3,
      
      [+](x0, x1) = x0 + x1,
      
      [0] = 5
     orientation:
      +(0(),0()) = 10 >= 5 = 0()
      
      +(0(),0()) = 10 >= 5 = 0()
      
      +(s(x),0()) = x + 8 >= x + 3 = s(x)
      
      +(s(x),0()) = x + 8 >= x + 8 = s(+(x,0()))
      
      s(+(x,0())) = x + 8 >= x + 3 = s(x)
      
      +(p(x),0()) = x + 11 >= x + 6 = p(x)
      
      +(p(x),0()) = x + 11 >= x + 11 = p(+(x,0()))
      
      p(+(x,0())) = x + 11 >= x + 6 = p(x)
      
      +(x,0()) = x + 5 >= x = x
      
      +(x,0()) = x + 5 >= x + 5 = +(0(),x)
      
      +(0(),x) = x + 5 >= x = x
      
      +(0(),s(x246)) = x246 + 8 >= x246 + 8 = s(+(0(),x246))
      
      +(0(),s(x246)) = x246 + 8 >= x246 + 3 = s(x246)
      
      s(+(0(),x246)) = x246 + 8 >= x246 + 3 = s(x246)
      
      +(s(x),s(x248)) = x + x248 + 6 >= x + x248 + 6 = s(+(s(x),x248))
      
      +(s(x),s(x248)) = x + x248 + 6 >= x + x248 + 6 = s(+(x,s(x248)))
      
      s(+(s(x),x248)) = x + x248 + 6 >= x + x248 + 6 = s(s(+(x,x248)))
      
      s(+(x,s(x248))) = x + x248 + 6 >= x + x248 + 6 = s(s(+(x,x248)))
      
      +(p(x),s(x250)) = x + x250 + 9 >= x + x250 + 9 = s(+(p(x),x250))
      
      +(p(x),s(x250)) = x + x250 + 9 >= x + x250 + 9 = p(+(x,s(x250)))
      
      s(+(p(x),x250)) = x + x250 + 9 >= x + x250 + 9 = s(p(+(x,x250)))
      
      s(p(+(x,x250))) = x + x250 + 9 >= x + x250 = +(x,x250)
      
      p(+(x,s(x250))) = x + x250 + 9 >= x + x250 + 9 = p(s(+(x,x250)))
      
      p(s(+(x,x250))) = x + x250 + 9 >= x + x250 = +(x,x250)
      
      +(x,s(x252)) = x + x252 + 3 >= x + x252 + 3 = s(+(x,x252))
      
      +(x,s(x252)) = x + x252 + 3 >= x + x252 + 3 = +(s(x252),x)
      
      s(+(x,x252)) = x + x252 + 3 >= x + x252 + 3 = s(+(x252,x))
      
      +(s(x252),x) = x + x252 + 3 >= x + x252 + 3 = s(+(x252,x))
      
      +(0(),p(x254)) = x254 + 11 >= x254 + 11 = p(+(0(),x254))
      
      +(0(),p(x254)) = x254 + 11 >= x254 + 6 = p(x254)
      
      p(+(0(),x254)) = x254 + 11 >= x254 + 6 = p(x254)
      
      +(s(x),p(x256)) = x + x256 + 9 >= x + x256 + 9 = p(+(s(x),x256))
      
      +(s(x),p(x256)) = x + x256 + 9 >= x + x256 + 9 = s(+(x,p(x256)))
      
      p(+(s(x),x256)) = x + x256 + 9 >= x + x256 + 9 = p(s(+(x,x256)))
      
      p(s(+(x,x256))) = x + x256 + 9 >= x + x256 = +(x,x256)
      
      s(+(x,p(x256))) = x + x256 + 9 >= x + x256 + 9 = s(p(+(x,x256)))
      
      s(p(+(x,x256))) = x + x256 + 9 >= x + x256 = +(x,x256)
      
      +(p(x),p(x258)) = x + x258 + 12 >= x + x258 + 12 = p(+(p(x),x258))
      
      +(p(x),p(x258)) = x + x258 + 12 >= x + x258 + 12 = p(+(x,p(x258)))
      
      p(+(p(x),x258)) = x + x258 + 12 >= x + x258 + 12 = p(p(+(x,x258)))
      
      p(+(x,p(x258))) = x + x258 + 12 >= x + x258 + 12 = p(p(+(x,x258)))
      
      +(x,p(x260)) = x + x260 + 6 >= x + x260 + 6 = p(+(x,x260))
      
      +(x,p(x260)) = x + x260 + 6 >= x + x260 + 6 = +(p(x260),x)
      
      p(+(x,x260)) = x + x260 + 6 >= x + x260 + 6 = p(+(x260,x))
      
      +(p(x260),x) = x + x260 + 6 >= x + x260 + 6 = p(+(x260,x))
      
      +(0(),0()) = 10 >= 5 = 0()
      
      +(0(),0()) = 10 >= 5 = 0()
      
      +(0(),s(y)) = y + 8 >= y + 3 = s(y)
      
      +(0(),s(y)) = y + 8 >= y + 8 = s(+(0(),y))
      
      s(+(0(),y)) = y + 8 >= y + 3 = s(y)
      
      +(0(),p(y)) = y + 11 >= y + 6 = p(y)
      
      +(0(),p(y)) = y + 11 >= y + 11 = p(+(0(),y))
      
      p(+(0(),y)) = y + 11 >= y + 6 = p(y)
      
      +(0(),y) = y + 5 >= y = y
      
      +(0(),y) = y + 5 >= y + 5 = +(y,0())
      
      +(y,0()) = y + 5 >= y = y
      
      +(s(x265),0()) = x265 + 8 >= x265 + 8 = s(+(x265,0()))
      
      +(s(x265),0()) = x265 + 8 >= x265 + 3 = s(x265)
      
      s(+(x265,0())) = x265 + 8 >= x265 + 3 = s(x265)
      
      +(s(x267),s(y)) = x267 + y + 6 >= x267 + y + 6 = s(+(x267,s(y)))
      
      +(s(x267),s(y)) = x267 + y + 6 >= x267 + y + 6 = s(+(s(x267),y))
      
      s(+(x267,s(y))) = x267 + y + 6 >= x267 + y + 6 = s(s(+(x267,y)))
      
      s(+(s(x267),y)) = x267 + y + 6 >= x267 + y + 6 = s(s(+(x267,y)))
      
      +(s(x269),p(y)) = x269 + y + 9 >= x269 + y + 9 = s(+(x269,p(y)))
      
      +(s(x269),p(y)) = x269 + y + 9 >= x269 + y + 9 = p(+(s(x269),y))
      
      s(+(x269,p(y))) = x269 + y + 9 >= x269 + y + 9 = s(p(+(x269,y)))
      
      s(p(+(x269,y))) = x269 + y + 9 >= x269 + y = +(x269,y)
      
      p(+(s(x269),y)) = x269 + y + 9 >= x269 + y + 9 = p(s(+(x269,y)))
      
      p(s(+(x269,y))) = x269 + y + 9 >= x269 + y = +(x269,y)
      
      +(s(x271),y) = x271 + y + 3 >= x271 + y + 3 = s(+(x271,y))
      
      +(s(x271),y) = x271 + y + 3 >= x271 + y + 3 = +(y,s(x271))
      
      s(+(x271,y)) = x271 + y + 3 >= x271 + y + 3 = s(+(y,x271))
      
      +(y,s(x271)) = x271 + y + 3 >= x271 + y + 3 = s(+(y,x271))
      
      +(p(x273),0()) = x273 + 11 >= x273 + 11 = p(+(x273,0()))
      
      +(p(x273),0()) = x273 + 11 >= x273 + 6 = p(x273)
      
      p(+(x273,0())) = x273 + 11 >= x273 + 6 = p(x273)
      
      +(p(x275),s(y)) = x275 + y + 9 >= x275 + y + 9 = p(+(x275,s(y)))
      
      +(p(x275),s(y)) = x275 + y + 9 >= x275 + y + 9 = s(+(p(x275),y))
      
      p(+(x275,s(y))) = x275 + y + 9 >= x275 + y + 9 = p(s(+(x275,y)))
      
      p(s(+(x275,y))) = x275 + y + 9 >= x275 + y = +(x275,y)
      
      s(+(p(x275),y)) = x275 + y + 9 >= x275 + y + 9 = s(p(+(x275,y)))
      
      s(p(+(x275,y))) = x275 + y + 9 >= x275 + y = +(x275,y)
      
      +(p(x277),p(y)) = x277 + y + 12 >= x277 + y + 12 = p(+(x277,p(y)))
      
      +(p(x277),p(y)) = x277 + y + 12 >= x277 + y + 12 = p(+(p(x277),y))
      
      p(+(x277,p(y))) = x277 + y + 12 >= x277 + y + 12 = p(p(+(x277,y)))
      
      p(+(p(x277),y)) = x277 + y + 12 >= x277 + y + 12 = p(p(+(x277,y)))
      
      +(p(x279),y) = x279 + y + 6 >= x279 + y + 6 = p(+(x279,y))
      
      +(p(x279),y) = x279 + y + 6 >= x279 + y + 6 = +(y,p(x279))
      
      p(+(x279,y)) = x279 + y + 6 >= x279 + y + 6 = p(+(y,x279))
      
      +(y,p(x279)) = x279 + y + 6 >= x279 + y + 6 = p(+(y,x279))
      
      +(x,s(p(x281))) = x + x281 + 9 >= x + x281 = +(x,x281)
      
      +(x,s(p(x281))) = x + x281 + 9 >= x + x281 + 9 = s(+(x,p(x281)))
      
      s(+(x,p(x281))) = x + x281 + 9 >= x + x281 + 9 = s(p(+(x,x281)))
      
      s(p(+(x,x281))) = x + x281 + 9 >= x + x281 = +(x,x281)
      
      +(s(p(x282)),y) = x282 + y + 9 >= x282 + y = +(x282,y)
      
      +(s(p(x282)),y) = x282 + y + 9 >= x282 + y + 9 = s(+(p(x282),y))
      
      s(+(p(x282),y)) = x282 + y + 9 >= x282 + y + 9 = s(p(+(x282,y)))
      
      s(p(+(x282,y))) = x282 + y + 9 >= x282 + y = +(x282,y)
      
      p(s(p(x283))) = x283 + 15 >= x283 + 6 = p(x283)
      
      p(s(p(x283))) = x283 + 15 >= x283 + 6 = p(x283)
      
      +(x,p(s(x284))) = x + x284 + 9 >= x + x284 = +(x,x284)
      
      +(x,p(s(x284))) = x + x284 + 9 >= x + x284 + 9 = p(+(x,s(x284)))
      
      p(+(x,s(x284))) = x + x284 + 9 >= x + x284 + 9 = p(s(+(x,x284)))
      
      p(s(+(x,x284))) = x + x284 + 9 >= x + x284 = +(x,x284)
      
      +(p(s(x285)),y) = x285 + y + 9 >= x285 + y = +(x285,y)
      
      +(p(s(x285)),y) = x285 + y + 9 >= x285 + y + 9 = p(+(s(x285),y))
      
      p(+(s(x285),y)) = x285 + y + 9 >= x285 + y + 9 = p(s(+(x285,y)))
      
      p(s(+(x285,y))) = x285 + y + 9 >= x285 + y = +(x285,y)
      
      s(p(s(x286))) = x286 + 12 >= x286 + 3 = s(x286)
      
      s(p(s(x286))) = x286 + 12 >= x286 + 3 = s(x286)
      
      +(x,0()) = x + 5 >= x + 5 = +(0(),x)
      
      +(x,0()) = x + 5 >= x = x
      
      +(0(),x) = x + 5 >= x = x
      
      +(x,s(y)) = x + y + 3 >= x + y + 3 = +(s(y),x)
      
      +(x,s(y)) = x + y + 3 >= x + y + 3 = s(+(x,y))
      
      +(s(y),x) = x + y + 3 >= x + y + 3 = s(+(y,x))
      
      s(+(x,y)) = x + y + 3 >= x + y + 3 = s(+(y,x))
      
      +(x,p(y)) = x + y + 6 >= x + y + 6 = +(p(y),x)
      
      +(x,p(y)) = x + y + 6 >= x + y + 6 = p(+(x,y))
      
      +(p(y),x) = x + y + 6 >= x + y + 6 = p(+(y,x))
      
      p(+(x,y)) = x + y + 6 >= x + y + 6 = p(+(y,x))
      
      +(0(),y) = y + 5 >= y + 5 = +(y,0())
      
      +(0(),y) = y + 5 >= y = y
      
      +(y,0()) = y + 5 >= y = y
      
      +(s(x),y) = x + y + 3 >= x + y + 3 = +(y,s(x))
      
      +(s(x),y) = x + y + 3 >= x + y + 3 = s(+(x,y))
      
      +(y,s(x)) = x + y + 3 >= x + y + 3 = s(+(y,x))
      
      s(+(x,y)) = x + y + 3 >= x + y + 3 = s(+(y,x))
      
      +(p(x),y) = x + y + 6 >= x + y + 6 = +(y,p(x))
      
      +(p(x),y) = x + y + 6 >= x + y + 6 = p(+(x,y))
      
      +(y,p(x)) = x + y + 6 >= x + y + 6 = p(+(y,x))
      
      p(+(x,y)) = x + y + 6 >= x + y + 6 = p(+(y,x))
      
      s(p(x)) = x + 9 >= x = x
      
      p(s(x)) = x + 9 >= x = x
      
      +(x,y) = x + y >= x + y = +(y,x)
     problem:
      
      strict:
       +(s(x),0()) -> s(+(x,0()))
       +(p(x),0()) -> p(+(x,0()))
       +(x,0()) -> +(0(),x)
       +(0(),s(x246)) -> s(+(0(),x246))
       +(s(x),s(x248)) -> s(+(s(x),x248))
       +(s(x),s(x248)) -> s(+(x,s(x248)))
       s(+(s(x),x248)) -> s(s(+(x,x248)))
       s(+(x,s(x248))) -> s(s(+(x,x248)))
       +(p(x),s(x250)) -> s(+(p(x),x250))
       +(p(x),s(x250)) -> p(+(x,s(x250)))
       s(+(p(x),x250)) -> s(p(+(x,x250)))
       p(+(x,s(x250))) -> p(s(+(x,x250)))
       +(x,s(x252)) -> s(+(x,x252))
       +(x,s(x252)) -> +(s(x252),x)
       s(+(x,x252)) -> s(+(x252,x))
       +(s(x252),x) -> s(+(x252,x))
       +(0(),p(x254)) -> p(+(0(),x254))
       +(s(x),p(x256)) -> p(+(s(x),x256))
       +(s(x),p(x256)) -> s(+(x,p(x256)))
       p(+(s(x),x256)) -> p(s(+(x,x256)))
       s(+(x,p(x256))) -> s(p(+(x,x256)))
       +(p(x),p(x258)) -> p(+(p(x),x258))
       +(p(x),p(x258)) -> p(+(x,p(x258)))
       p(+(p(x),x258)) -> p(p(+(x,x258)))
       p(+(x,p(x258))) -> p(p(+(x,x258)))
       +(x,p(x260)) -> p(+(x,x260))
       +(x,p(x260)) -> +(p(x260),x)
       p(+(x,x260)) -> p(+(x260,x))
       +(p(x260),x) -> p(+(x260,x))
       +(0(),s(y)) -> s(+(0(),y))
       +(0(),p(y)) -> p(+(0(),y))
       +(0(),y) -> +(y,0())
       +(s(x265),0()) -> s(+(x265,0()))
       +(s(x267),s(y)) -> s(+(x267,s(y)))
       +(s(x267),s(y)) -> s(+(s(x267),y))
       s(+(x267,s(y))) -> s(s(+(x267,y)))
       s(+(s(x267),y)) -> s(s(+(x267,y)))
       +(s(x269),p(y)) -> s(+(x269,p(y)))
       +(s(x269),p(y)) -> p(+(s(x269),y))
       s(+(x269,p(y))) -> s(p(+(x269,y)))
       p(+(s(x269),y)) -> p(s(+(x269,y)))
       +(s(x271),y) -> s(+(x271,y))
       +(s(x271),y) -> +(y,s(x271))
       s(+(x271,y)) -> s(+(y,x271))
       +(y,s(x271)) -> s(+(y,x271))
       +(p(x273),0()) -> p(+(x273,0()))
       +(p(x275),s(y)) -> p(+(x275,s(y)))
       +(p(x275),s(y)) -> s(+(p(x275),y))
       p(+(x275,s(y))) -> p(s(+(x275,y)))
       s(+(p(x275),y)) -> s(p(+(x275,y)))
       +(p(x277),p(y)) -> p(+(x277,p(y)))
       +(p(x277),p(y)) -> p(+(p(x277),y))
       p(+(x277,p(y))) -> p(p(+(x277,y)))
       p(+(p(x277),y)) -> p(p(+(x277,y)))
       +(p(x279),y) -> p(+(x279,y))
       +(p(x279),y) -> +(y,p(x279))
       p(+(x279,y)) -> p(+(y,x279))
       +(y,p(x279)) -> p(+(y,x279))
       +(x,s(p(x281))) -> s(+(x,p(x281)))
       s(+(x,p(x281))) -> s(p(+(x,x281)))
       +(s(p(x282)),y) -> s(+(p(x282),y))
       s(+(p(x282),y)) -> s(p(+(x282,y)))
       +(x,p(s(x284))) -> p(+(x,s(x284)))
       p(+(x,s(x284))) -> p(s(+(x,x284)))
       +(p(s(x285)),y) -> p(+(s(x285),y))
       p(+(s(x285),y)) -> p(s(+(x285,y)))
       +(x,0()) -> +(0(),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())
       +(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))
      weak:
       +(x,s(y)) -> s(+(x,y))
       +(x,p(y)) -> p(+(x,y))
       +(s(x),y) -> s(+(x,y))
       +(p(x),y) -> p(+(x,y))
       +(x,y) -> +(y,x)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [p](x0) = x0 + 2,
       
       [s](x0) = x0 + 1,
       
       [+](x0, x1) = 3x0 + 3x1 + 2,
       
       [0] = 0
      orientation:
       +(s(x),0()) = 3x + 5 >= 3x + 3 = s(+(x,0()))
       
       +(p(x),0()) = 3x + 8 >= 3x + 4 = p(+(x,0()))
       
       +(x,0()) = 3x + 2 >= 3x + 2 = +(0(),x)
       
       +(0(),s(x246)) = 3x246 + 5 >= 3x246 + 3 = s(+(0(),x246))
       
       +(s(x),s(x248)) = 3x + 3x248 + 8 >= 3x + 3x248 + 6 = s(+(s(x),x248))
       
       +(s(x),s(x248)) = 3x + 3x248 + 8 >= 3x + 3x248 + 6 = s(+(x,s(x248)))
       
       s(+(s(x),x248)) = 3x + 3x248 + 6 >= 3x + 3x248 + 4 = s(s(+(x,x248)))
       
       s(+(x,s(x248))) = 3x + 3x248 + 6 >= 3x + 3x248 + 4 = s(s(+(x,x248)))
       
       +(p(x),s(x250)) = 3x + 3x250 + 11 >= 3x + 3x250 + 9 = s(+(p(x),x250))
       
       +(p(x),s(x250)) = 3x + 3x250 + 11 >= 3x + 3x250 + 7 = p(+(x,s(x250)))
       
       s(+(p(x),x250)) = 3x + 3x250 + 9 >= 3x + 3x250 + 5 = s(p(+(x,x250)))
       
       p(+(x,s(x250))) = 3x + 3x250 + 7 >= 3x + 3x250 + 5 = p(s(+(x,x250)))
       
       +(x,s(x252)) = 3x + 3x252 + 5 >= 3x + 3x252 + 3 = s(+(x,x252))
       
       +(x,s(x252)) = 3x + 3x252 + 5 >= 3x + 3x252 + 5 = +(s(x252),x)
       
       s(+(x,x252)) = 3x + 3x252 + 3 >= 3x + 3x252 + 3 = s(+(x252,x))
       
       +(s(x252),x) = 3x + 3x252 + 5 >= 3x + 3x252 + 3 = s(+(x252,x))
       
       +(0(),p(x254)) = 3x254 + 8 >= 3x254 + 4 = p(+(0(),x254))
       
       +(s(x),p(x256)) = 3x + 3x256 + 11 >= 3x + 3x256 + 7 = p(+(s(x),x256))
       
       +(s(x),p(x256)) = 3x + 3x256 + 11 >= 3x + 3x256 + 9 = s(+(x,p(x256)))
       
       p(+(s(x),x256)) = 3x + 3x256 + 7 >= 3x + 3x256 + 5 = p(s(+(x,x256)))
       
       s(+(x,p(x256))) = 3x + 3x256 + 9 >= 3x + 3x256 + 5 = s(p(+(x,x256)))
       
       +(p(x),p(x258)) = 3x + 3x258 + 14 >= 3x + 3x258 + 10 = p(+(p(x),x258))
       
       +(p(x),p(x258)) = 3x + 3x258 + 14 >= 3x + 3x258 + 10 = p(+(x,p(x258)))
       
       p(+(p(x),x258)) = 3x + 3x258 + 10 >= 3x + 3x258 + 6 = p(p(+(x,x258)))
       
       p(+(x,p(x258))) = 3x + 3x258 + 10 >= 3x + 3x258 + 6 = p(p(+(x,x258)))
       
       +(x,p(x260)) = 3x + 3x260 + 8 >= 3x + 3x260 + 4 = p(+(x,x260))
       
       +(x,p(x260)) = 3x + 3x260 + 8 >= 3x + 3x260 + 8 = +(p(x260),x)
       
       p(+(x,x260)) = 3x + 3x260 + 4 >= 3x + 3x260 + 4 = p(+(x260,x))
       
       +(p(x260),x) = 3x + 3x260 + 8 >= 3x + 3x260 + 4 = p(+(x260,x))
       
       +(0(),s(y)) = 3y + 5 >= 3y + 3 = s(+(0(),y))
       
       +(0(),p(y)) = 3y + 8 >= 3y + 4 = p(+(0(),y))
       
       +(0(),y) = 3y + 2 >= 3y + 2 = +(y,0())
       
       +(s(x265),0()) = 3x265 + 5 >= 3x265 + 3 = s(+(x265,0()))
       
       +(s(x267),s(y)) = 3x267 + 3y + 8 >= 3x267 + 3y + 6 = s(+(x267,s(y)))
       
       +(s(x267),s(y)) = 3x267 + 3y + 8 >= 3x267 + 3y + 6 = s(+(s(x267),y))
       
       s(+(x267,s(y))) = 3x267 + 3y + 6 >= 3x267 + 3y + 4 = s(s(+(x267,y)))
       
       s(+(s(x267),y)) = 3x267 + 3y + 6 >= 3x267 + 3y + 4 = s(s(+(x267,y)))
       
       +(s(x269),p(y)) = 3x269 + 3y + 11 >= 3x269 + 3y + 9 = s(+(x269,p(y)))
       
       +(s(x269),p(y)) = 3x269 + 3y + 11 >= 3x269 + 3y + 7 = p(+(s(x269),y))
       
       s(+(x269,p(y))) = 3x269 + 3y + 9 >= 3x269 + 3y + 5 = s(p(+(x269,y)))
       
       p(+(s(x269),y)) = 3x269 + 3y + 7 >= 3x269 + 3y + 5 = p(s(+(x269,y)))
       
       +(s(x271),y) = 3x271 + 3y + 5 >= 3x271 + 3y + 3 = s(+(x271,y))
       
       +(s(x271),y) = 3x271 + 3y + 5 >= 3x271 + 3y + 5 = +(y,s(x271))
       
       s(+(x271,y)) = 3x271 + 3y + 3 >= 3x271 + 3y + 3 = s(+(y,x271))
       
       +(y,s(x271)) = 3x271 + 3y + 5 >= 3x271 + 3y + 3 = s(+(y,x271))
       
       +(p(x273),0()) = 3x273 + 8 >= 3x273 + 4 = p(+(x273,0()))
       
       +(p(x275),s(y)) = 3x275 + 3y + 11 >= 3x275 + 3y + 7 = p(+(x275,s(y)))
       
       +(p(x275),s(y)) = 3x275 + 3y + 11 >= 3x275 + 3y + 9 = s(+(p(x275),y))
       
       p(+(x275,s(y))) = 3x275 + 3y + 7 >= 3x275 + 3y + 5 = p(s(+(x275,y)))
       
       s(+(p(x275),y)) = 3x275 + 3y + 9 >= 3x275 + 3y + 5 = s(p(+(x275,y)))
       
       +(p(x277),p(y)) = 3x277 + 3y + 14 >= 3x277 + 3y + 10 = p(+(x277,p(y)))
       
       +(p(x277),p(y)) = 3x277 + 3y + 14 >= 3x277 + 3y + 10 = p(+(p(x277),y))
       
       p(+(x277,p(y))) = 3x277 + 3y + 10 >= 3x277 + 3y + 6 = p(p(+(x277,y)))
       
       p(+(p(x277),y)) = 3x277 + 3y + 10 >= 3x277 + 3y + 6 = p(p(+(x277,y)))
       
       +(p(x279),y) = 3x279 + 3y + 8 >= 3x279 + 3y + 4 = p(+(x279,y))
       
       +(p(x279),y) = 3x279 + 3y + 8 >= 3x279 + 3y + 8 = +(y,p(x279))
       
       p(+(x279,y)) = 3x279 + 3y + 4 >= 3x279 + 3y + 4 = p(+(y,x279))
       
       +(y,p(x279)) = 3x279 + 3y + 8 >= 3x279 + 3y + 4 = p(+(y,x279))
       
       +(x,s(p(x281))) = 3x + 3x281 + 11 >= 3x + 3x281 + 9 = s(+(x,p(x281)))
       
       s(+(x,p(x281))) = 3x + 3x281 + 9 >= 3x + 3x281 + 5 = s(p(+(x,x281)))
       
       +(s(p(x282)),y) = 3x282 + 3y + 11 >= 3x282 + 3y + 9 = s(+(p(x282),y))
       
       s(+(p(x282),y)) = 3x282 + 3y + 9 >= 3x282 + 3y + 5 = s(p(+(x282,y)))
       
       +(x,p(s(x284))) = 3x + 3x284 + 11 >= 3x + 3x284 + 7 = p(+(x,s(x284)))
       
       p(+(x,s(x284))) = 3x + 3x284 + 7 >= 3x + 3x284 + 5 = p(s(+(x,x284)))
       
       +(p(s(x285)),y) = 3x285 + 3y + 11 >= 3x285 + 3y + 7 = p(+(s(x285),y))
       
       p(+(s(x285),y)) = 3x285 + 3y + 7 >= 3x285 + 3y + 5 = p(s(+(x285,y)))
       
       +(x,0()) = 3x + 2 >= 3x + 2 = +(0(),x)
       
       +(x,s(y)) = 3x + 3y + 5 >= 3x + 3y + 5 = +(s(y),x)
       
       +(x,s(y)) = 3x + 3y + 5 >= 3x + 3y + 3 = s(+(x,y))
       
       +(s(y),x) = 3x + 3y + 5 >= 3x + 3y + 3 = s(+(y,x))
       
       s(+(x,y)) = 3x + 3y + 3 >= 3x + 3y + 3 = s(+(y,x))
       
       +(x,p(y)) = 3x + 3y + 8 >= 3x + 3y + 8 = +(p(y),x)
       
       +(x,p(y)) = 3x + 3y + 8 >= 3x + 3y + 4 = p(+(x,y))
       
       +(p(y),x) = 3x + 3y + 8 >= 3x + 3y + 4 = p(+(y,x))
       
       p(+(x,y)) = 3x + 3y + 4 >= 3x + 3y + 4 = p(+(y,x))
       
       +(0(),y) = 3y + 2 >= 3y + 2 = +(y,0())
       
       +(s(x),y) = 3x + 3y + 5 >= 3x + 3y + 5 = +(y,s(x))
       
       +(s(x),y) = 3x + 3y + 5 >= 3x + 3y + 3 = s(+(x,y))
       
       +(y,s(x)) = 3x + 3y + 5 >= 3x + 3y + 3 = s(+(y,x))
       
       s(+(x,y)) = 3x + 3y + 3 >= 3x + 3y + 3 = s(+(y,x))
       
       +(p(x),y) = 3x + 3y + 8 >= 3x + 3y + 8 = +(y,p(x))
       
       +(p(x),y) = 3x + 3y + 8 >= 3x + 3y + 4 = p(+(x,y))
       
       +(y,p(x)) = 3x + 3y + 8 >= 3x + 3y + 4 = p(+(y,x))
       
       p(+(x,y)) = 3x + 3y + 4 >= 3x + 3y + 4 = p(+(y,x))
       
       +(x,y) = 3x + 3y + 2 >= 3x + 3y + 2 = +(y,x)
      problem:
       
       strict:
        +(x,0()) -> +(0(),x)
        +(x,s(x252)) -> +(s(x252),x)
        s(+(x,x252)) -> s(+(x252,x))
        +(x,p(x260)) -> +(p(x260),x)
        p(+(x,x260)) -> p(+(x260,x))
        +(0(),y) -> +(y,0())
        +(s(x271),y) -> +(y,s(x271))
        s(+(x271,y)) -> s(+(y,x271))
        +(p(x279),y) -> +(y,p(x279))
        p(+(x279,y)) -> p(+(y,x279))
        +(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))
       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(),0()) -3|[1,0]-> 0()
        joins:
         
         
        peak:
         s(x) <-0|[1,0]- +(s(x),0()) -4|[1,0]-> s(+(x,0()))
        joins:
         
         s(+(x,0())) -0|0[0,0]-> s(x)
        peak:
         p(x) <-0|[1,0]- +(p(x),0()) -5|[1,0]-> p(+(x,0()))
        joins:
         
         p(+(x,0())) -0|0[0,0]-> p(x)
        peak:
         x <-0|[1,0]- +(x,0()) -8|[1,0]-> +(0(),x)
        joins:
         
         +(0(),x) -3|[1,0]-> x
        peak:
         s(+(0(),x246)) <-1|[1,0]- +(0(),s(x246)) -3|[1,0]-> s(x246)
        joins:
         s(+(0(),x246)) -3|0[0,0]-> s(x246)
         
        peak:
         s(+(s(x),x248)) <-1|[1,0]- +(s(x),s(x248)) -4|[1,0]-> s(+(x,s(x248)))
        joins:
         s(+(s(x),x248)) -4|0[0,0]-> s(s(+(x,x248)))
         s(+(x,s(x248))) -1|0[0,0]-> s(s(+(x,x248)))
        peak:
         s(+(p(x),x250)) <-1|[1,0]- +(p(x),s(x250)) -5|[1,0]-> p(+(x,s(x250)))
        joins:
         s(+(p(x),x250)) -5|0[0,0]-> s(p(+(x,x250))) -6|[0,0]-> +(x,x250)
         p(+(x,s(x250))) -1|0[0,0]-> p(s(+(x,x250))) -7|[0,0]-> +(x,x250)
        peak:
         s(+(x,x252)) <-1|[1,0]- +(x,s(x252)) -8|[1,0]-> +(s(x252),x)
        joins:
         s(+(x,x252)) -8|0[0,0]-> s(+(x252,x))
         +(s(x252),x) -4|[1,0]-> s(+(x252,x))
        peak:
         p(+(0(),x254)) <-2|[1,0]- +(0(),p(x254)) -3|[1,0]-> p(x254)
        joins:
         p(+(0(),x254)) -3|0[0,0]-> p(x254)
         
        peak:
         p(+(s(x),x256)) <-2|[1,0]- +(s(x),p(x256)) -4|[1,0]-> s(+(x,p(x256)))
        joins:
         p(+(s(x),x256)) -4|0[0,0]-> p(s(+(x,x256))) -7|[0,0]-> +(x,x256)
         s(+(x,p(x256))) -2|0[0,0]-> s(p(+(x,x256))) -6|[0,0]-> +(x,x256)
        peak:
         p(+(p(x),x258)) <-2|[1,0]- +(p(x),p(x258)) -5|[1,0]-> p(+(x,p(x258)))
        joins:
         p(+(p(x),x258)) -5|0[0,0]-> p(p(+(x,x258)))
         p(+(x,p(x258))) -2|0[0,0]-> p(p(+(x,x258)))
        peak:
         p(+(x,x260)) <-2|[1,0]- +(x,p(x260)) -8|[1,0]-> +(p(x260),x)
        joins:
         p(+(x,x260)) -8|0[0,0]-> p(+(x260,x))
         +(p(x260),x) -5|[1,0]-> p(+(x260,x))
        peak:
         0() <-3|[1,0]- +(0(),0()) -0|[1,0]-> 0()
        joins:
         
         
        peak:
         s(y) <-3|[1,0]- +(0(),s(y)) -1|[1,0]-> s(+(0(),y))
        joins:
         
         s(+(0(),y)) -3|0[0,0]-> s(y)
        peak:
         p(y) <-3|[1,0]- +(0(),p(y)) -2|[1,0]-> p(+(0(),y))
        joins:
         
         p(+(0(),y)) -3|0[0,0]-> p(y)
        peak:
         y <-3|[1,0]- +(0(),y) -8|[1,0]-> +(y,0())
        joins:
         
         +(y,0()) -0|[1,0]-> y
        peak:
         s(+(x265,0())) <-4|[1,0]- +(s(x265),0()) -0|[1,0]-> s(x265)
        joins:
         s(+(x265,0())) -0|0[0,0]-> s(x265)
         
        peak:
         s(+(x267,s(y))) <-4|[1,0]- +(s(x267),s(y)) -1|[1,0]-> s(+(s(x267),y))
        joins:
         s(+(x267,s(y))) -1|0[0,0]-> s(s(+(x267,y)))
         s(+(s(x267),y)) -4|0[0,0]-> s(s(+(x267,y)))
        peak:
         s(+(x269,p(y))) <-4|[1,0]- +(s(x269),p(y)) -2|[1,0]-> p(+(s(x269),y))
        joins:
         s(+(x269,p(y))) -2|0[0,0]-> s(p(+(x269,y))) -6|[0,0]-> +(x269,y)
         p(+(s(x269),y)) -4|0[0,0]-> p(s(+(x269,y))) -7|[0,0]-> +(x269,y)
        peak:
         s(+(x271,y)) <-4|[1,0]- +(s(x271),y) -8|[1,0]-> +(y,s(x271))
        joins:
         s(+(x271,y)) -8|0[0,0]-> s(+(y,x271))
         +(y,s(x271)) -1|[1,0]-> s(+(y,x271))
        peak:
         p(+(x273,0())) <-5|[1,0]- +(p(x273),0()) -0|[1,0]-> p(x273)
        joins:
         p(+(x273,0())) -0|0[0,0]-> p(x273)
         
        peak:
         p(+(x275,s(y))) <-5|[1,0]- +(p(x275),s(y)) -1|[1,0]-> s(+(p(x275),y))
        joins:
         p(+(x275,s(y))) -1|0[0,0]-> p(s(+(x275,y))) -7|[0,0]-> +(x275,y)
         s(+(p(x275),y)) -5|0[0,0]-> s(p(+(x275,y))) -6|[0,0]-> +(x275,y)
        peak:
         p(+(x277,p(y))) <-5|[1,0]- +(p(x277),p(y)) -2|[1,0]-> p(+(p(x277),y))
        joins:
         p(+(x277,p(y))) -2|0[0,0]-> p(p(+(x277,y)))
         p(+(p(x277),y)) -5|0[0,0]-> p(p(+(x277,y)))
        peak:
         p(+(x279,y)) <-5|[1,0]- +(p(x279),y) -8|[1,0]-> +(y,p(x279))
        joins:
         p(+(x279,y)) -8|0[0,0]-> p(+(y,x279))
         +(y,p(x279)) -2|[1,0]-> p(+(y,x279))
        peak:
         +(x,x281) <-6|1[1,1]- +(x,s(p(x281))) -1|[1,0]-> s(+(x,p(x281)))
        joins:
         
         s(+(x,p(x281))) -2|0[0,0]-> s(p(+(x,x281))) -6|[0,0]-> +(x,x281)
        peak:
         +(x282,y) <-6|0[1,1]- +(s(p(x282)),y) -4|[1,0]-> s(+(p(x282),y))
        joins:
         
         s(+(p(x282),y)) -5|0[0,0]-> s(p(+(x282,y))) -6|[0,0]-> +(x282,y)
        peak:
         p(x283) <-6|0[1,0]- p(s(p(x283))) -7|[1,0]-> p(x283)
        joins:
         
         
        peak:
         +(x,x284) <-7|1[1,1]- +(x,p(s(x284))) -2|[1,0]-> p(+(x,s(x284)))
        joins:
         
         p(+(x,s(x284))) -1|0[0,0]-> p(s(+(x,x284))) -7|[0,0]-> +(x,x284)
        peak:
         +(x285,y) <-7|0[1,1]- +(p(s(x285)),y) -5|[1,0]-> p(+(s(x285),y))
        joins:
         
         p(+(s(x285),y)) -4|0[0,0]-> p(s(+(x285,y))) -7|[0,0]-> +(x285,y)
        peak:
         s(x286) <-7|0[1,0]- s(p(s(x286))) -6|[1,0]-> s(x286)
        joins:
         
         
        peak:
         +(0(),x) <-8|[1,0]- +(x,0()) -0|[1,0]-> x
        joins:
         +(0(),x) -3|[1,0]-> x
         
        peak:
         +(s(y),x) <-8|[1,0]- +(x,s(y)) -1|[1,0]-> s(+(x,y))
        joins:
         +(s(y),x) -4|[1,0]-> s(+(y,x))
         s(+(x,y)) -8|0[0,0]-> s(+(y,x))
        peak:
         +(p(y),x) <-8|[1,0]- +(x,p(y)) -2|[1,0]-> p(+(x,y))
        joins:
         +(p(y),x) -5|[1,0]-> p(+(y,x))
         p(+(x,y)) -8|0[0,0]-> p(+(y,x))
        peak:
         +(y,0()) <-8|[1,0]- +(0(),y) -3|[1,0]-> y
        joins:
         +(y,0()) -0|[1,0]-> y
         
        peak:
         +(y,s(x)) <-8|[1,0]- +(s(x),y) -4|[1,0]-> s(+(x,y))
        joins:
         +(y,s(x)) -1|[1,0]-> s(+(y,x))
         s(+(x,y)) -8|0[0,0]-> s(+(y,x))
        peak:
         +(y,p(x)) <-8|[1,0]- +(p(x),y) -5|[1,0]-> p(+(x,y))
        joins:
         +(y,p(x)) -2|[1,0]-> p(+(y,x))
         p(+(x,y)) -8|0[0,0]-> p(+(y,x))
        Qed