Problem:
 +(1(),x) -> +(+(0(),1()),x)
 +(0(),x) -> x

Proof:
 Uncurry Processor:
  11(x) -> 02(1(),x)
  02(x,x3) -> +(x,x3)
  01(x) -> x
  +(1(),x2) -> 11(x2)
  +(01(x1),x2) -> 02(x1,x2)
  +(0(),x2) -> 01(x2)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [02](x0, x1) = x0 + x1,
    
    [01](x0) = x0 + 5,
    
    [11](x0) = x0,
    
    [0] = 6,
    
    [+](x0, x1) = x0 + x1,
    
    [1] = 0
   orientation:
    11(x) = x >= x = 02(1(),x)
    
    02(x,x3) = x + x3 >= x + x3 = +(x,x3)
    
    01(x) = x + 5 >= x = x
    
    +(1(),x2) = x2 >= x2 = 11(x2)
    
    +(01(x1),x2) = x1 + x2 + 5 >= x1 + x2 = 02(x1,x2)
    
    +(0(),x2) = x2 + 6 >= x2 + 5 = 01(x2)
   problem:
    11(x) -> 02(1(),x)
    02(x,x3) -> +(x,x3)
    +(1(),x2) -> 11(x2)
   Unfolding Processor:
    loop length: 3
    terms:
     11(x26)
     02(1(),x26)
     +(1(),x26)
    context: []
    substitution:
     x26 -> x26
    Qed