NO

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:
   dimension: 3
   interpretation:
               [1 0 1]     [1]
    [01](x0) = [1 1 1]x0 + [1]
               [1 1 1]     [1],
    
                   [1 0 1]     [1 0 1]     [0]
    [02](x0, x1) = [0 0 0]x0 + [1 1 1]x1 + [1]
                   [1 0 1]     [1 1 1]     [0],
    
               [1 0 1]     [0]
    [11](x0) = [1 1 1]x0 + [1]
               [1 1 1]     [0],
    
          [1]
    [0] = [0]
          [0],
    
                  [1 0 0]     [1 0 1]     [0]
    [+](x0, x1) = [0 0 0]x0 + [1 1 1]x1 + [1]
                  [1 0 0]     [1 1 1]     [0],
    
          [0]
    [1] = [0]
          [0]
   orientation:
            [1 0 1]    [0]    [1 0 1]    [0]            
    11(x) = [1 1 1]x + [1] >= [1 1 1]x + [1] = 02(1(),x)
            [1 1 1]    [0]    [1 1 1]    [0]            
    
               [1 0 1]    [1 0 1]     [0]    [1 0 0]    [1 0 1]     [0]          
    02(x,x3) = [0 0 0]x + [1 1 1]x3 + [1] >= [0 0 0]x + [1 1 1]x3 + [1] = +(x,x3)
               [1 0 1]    [1 1 1]     [0]    [1 0 0]    [1 1 1]     [0]          
    
            [1 0 1]    [1]         
    01(x) = [1 1 1]x + [1] >= x = x
            [1 1 1]    [1]         
    
                [1 0 1]     [0]    [1 0 1]     [0]         
    +(1(),x2) = [1 1 1]x2 + [1] >= [1 1 1]x2 + [1] = 11(x2)
                [1 1 1]     [0]    [1 1 1]     [0]         
    
                   [1 0 1]     [1 0 1]     [1]    [1 0 1]     [1 0 1]     [0]            
    +(01(x1),x2) = [0 0 0]x1 + [1 1 1]x2 + [1] >= [0 0 0]x1 + [1 1 1]x2 + [1] = 02(x1,x2)
                   [1 0 1]     [1 1 1]     [1]    [1 0 1]     [1 1 1]     [0]            
    
                [1 0 1]     [1]    [1 0 1]     [1]         
    +(0(),x2) = [1 1 1]x2 + [1] >= [1 1 1]x2 + [1] = 01(x2)
                [1 1 1]     [1]    [1 1 1]     [1]         
   problem:
    11(x) -> 02(1(),x)
    02(x,x3) -> +(x,x3)
    +(1(),x2) -> 11(x2)
    +(0(),x2) -> 01(x2)
   Matrix Interpretation Processor:
    dimension: 3
    interpretation:
                [1 0 0]     [0]
     [01](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [1],
     
                    [1 0 0]     [1 1 0]     [1]
     [02](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                    [0 1 0]     [0 0 0]     [0],
     
                [1 1 0]     [1]
     [11](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [0],
     
           [0]
     [0] = [1]
           [0],
     
                   [1 0 0]     [1 1 0]     [1]
     [+](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                   [0 1 0]     [0 0 0]     [0],
     
           [0]
     [1] = [0]
           [0]
    orientation:
             [1 1 0]    [1]    [1 1 0]    [1]            
     11(x) = [0 0 0]x + [0] >= [0 0 0]x + [0] = 02(1(),x)
             [0 0 0]    [0]    [0 0 0]    [0]            
     
                [1 0 0]    [1 1 0]     [1]    [1 0 0]    [1 1 0]     [1]          
     02(x,x3) = [0 0 0]x + [0 0 0]x3 + [0] >= [0 0 0]x + [0 0 0]x3 + [0] = +(x,x3)
                [0 1 0]    [0 0 0]     [0]    [0 1 0]    [0 0 0]     [0]          
     
                 [1 1 0]     [1]    [1 1 0]     [1]         
     +(1(),x2) = [0 0 0]x2 + [0] >= [0 0 0]x2 + [0] = 11(x2)
                 [0 0 0]     [0]    [0 0 0]     [0]         
     
                 [1 1 0]     [1]    [1 0 0]     [0]         
     +(0(),x2) = [0 0 0]x2 + [0] >= [0 0 0]x2 + [0] = 01(x2)
                 [0 0 0]     [1]    [0 0 0]     [1]         
    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