YES

Problem:
 +(0(),0()) -> 0()
 +(0(),1()) -> 1()
 +(0(),2()) -> 2()
 +(0(),3()) -> 3()
 +(0(),4()) -> 4()
 +(0(),5()) -> 5()
 +(0(),6()) -> 6()
 +(0(),7()) -> 7()
 +(0(),8()) -> 8()
 +(0(),9()) -> 9()
 +(1(),0()) -> 1()
 +(1(),1()) -> 2()
 +(1(),2()) -> 3()
 +(1(),3()) -> 4()
 +(1(),4()) -> 5()
 +(1(),5()) -> 6()
 +(1(),6()) -> 7()
 +(1(),7()) -> 8()
 +(1(),8()) -> 9()
 +(1(),9()) -> c(1(),0())
 +(2(),0()) -> 2()
 +(2(),1()) -> 3()
 +(2(),2()) -> 4()
 +(2(),3()) -> 5()
 +(2(),4()) -> 6()
 +(2(),5()) -> 7()
 +(2(),6()) -> 8()
 +(2(),7()) -> 9()
 +(2(),8()) -> c(1(),0())
 +(2(),9()) -> c(1(),1())
 +(3(),0()) -> 3()
 +(3(),1()) -> 4()
 +(3(),2()) -> 5()
 +(3(),3()) -> 6()
 +(3(),4()) -> 7()
 +(3(),5()) -> 8()
 +(3(),6()) -> 9()
 +(3(),7()) -> c(1(),0())
 +(3(),8()) -> c(1(),1())
 +(3(),9()) -> c(1(),2())
 +(4(),0()) -> 4()
 +(4(),1()) -> 5()
 +(4(),2()) -> 6()
 +(4(),3()) -> 7()
 +(4(),4()) -> 8()
 +(4(),5()) -> 9()
 +(4(),6()) -> c(1(),0())
 +(4(),7()) -> c(1(),1())
 +(4(),8()) -> c(1(),2())
 +(4(),9()) -> c(1(),3())
 +(5(),0()) -> 5()
 +(5(),1()) -> 6()
 +(5(),2()) -> 7()
 +(5(),3()) -> 8()
 +(5(),4()) -> 9()
 +(5(),5()) -> c(1(),0())
 +(5(),6()) -> c(1(),1())
 +(5(),7()) -> c(1(),2())
 +(5(),8()) -> c(1(),3())
 +(5(),9()) -> c(1(),4())
 +(6(),0()) -> 6()
 +(6(),1()) -> 7()
 +(6(),2()) -> 8()
 +(6(),3()) -> 9()
 +(6(),4()) -> c(1(),0())
 +(6(),5()) -> c(1(),1())
 +(6(),6()) -> c(1(),2())
 +(6(),7()) -> c(1(),3())
 +(6(),8()) -> c(1(),4())
 +(6(),9()) -> c(1(),5())
 +(7(),0()) -> 7()
 +(7(),1()) -> 8()
 +(7(),2()) -> 9()
 +(7(),3()) -> c(1(),0())
 +(7(),4()) -> c(1(),1())
 +(7(),5()) -> c(1(),2())
 +(7(),6()) -> c(1(),3())
 +(7(),7()) -> c(1(),4())
 +(7(),8()) -> c(1(),5())
 +(7(),9()) -> c(1(),6())
 +(8(),0()) -> 8()
 +(8(),1()) -> 9()
 +(8(),2()) -> c(1(),0())
 +(8(),3()) -> c(1(),1())
 +(8(),4()) -> c(1(),2())
 +(8(),5()) -> c(1(),3())
 +(8(),6()) -> c(1(),4())
 +(8(),7()) -> c(1(),5())
 +(8(),8()) -> c(1(),6())
 +(8(),9()) -> c(1(),7())
 +(9(),0()) -> 9()
 +(9(),1()) -> c(1(),0())
 +(9(),2()) -> c(1(),1())
 +(9(),3()) -> c(1(),2())
 +(9(),4()) -> c(1(),3())
 +(9(),5()) -> c(1(),4())
 +(9(),6()) -> c(1(),5())
 +(9(),7()) -> c(1(),6())
 +(9(),8()) -> c(1(),7())
 +(9(),9()) -> c(1(),8())
 +(x,c(y,z)) -> c(y,+(x,z))
 +(c(x,y),z) -> c(x,+(y,z))
 c(0(),x) -> x
 c(x,c(y,z)) -> c(+(x,y),z)

Proof:
 DP Processor:
  DPs:
   +#(1(),9()) -> c#(1(),0())
   +#(2(),8()) -> c#(1(),0())
   +#(2(),9()) -> c#(1(),1())
   +#(3(),7()) -> c#(1(),0())
   +#(3(),8()) -> c#(1(),1())
   +#(3(),9()) -> c#(1(),2())
   +#(4(),6()) -> c#(1(),0())
   +#(4(),7()) -> c#(1(),1())
   +#(4(),8()) -> c#(1(),2())
   +#(4(),9()) -> c#(1(),3())
   +#(5(),5()) -> c#(1(),0())
   +#(5(),6()) -> c#(1(),1())
   +#(5(),7()) -> c#(1(),2())
   +#(5(),8()) -> c#(1(),3())
   +#(5(),9()) -> c#(1(),4())
   +#(6(),4()) -> c#(1(),0())
   +#(6(),5()) -> c#(1(),1())
   +#(6(),6()) -> c#(1(),2())
   +#(6(),7()) -> c#(1(),3())
   +#(6(),8()) -> c#(1(),4())
   +#(6(),9()) -> c#(1(),5())
   +#(7(),3()) -> c#(1(),0())
   +#(7(),4()) -> c#(1(),1())
   +#(7(),5()) -> c#(1(),2())
   +#(7(),6()) -> c#(1(),3())
   +#(7(),7()) -> c#(1(),4())
   +#(7(),8()) -> c#(1(),5())
   +#(7(),9()) -> c#(1(),6())
   +#(8(),2()) -> c#(1(),0())
   +#(8(),3()) -> c#(1(),1())
   +#(8(),4()) -> c#(1(),2())
   +#(8(),5()) -> c#(1(),3())
   +#(8(),6()) -> c#(1(),4())
   +#(8(),7()) -> c#(1(),5())
   +#(8(),8()) -> c#(1(),6())
   +#(8(),9()) -> c#(1(),7())
   +#(9(),1()) -> c#(1(),0())
   +#(9(),2()) -> c#(1(),1())
   +#(9(),3()) -> c#(1(),2())
   +#(9(),4()) -> c#(1(),3())
   +#(9(),5()) -> c#(1(),4())
   +#(9(),6()) -> c#(1(),5())
   +#(9(),7()) -> c#(1(),6())
   +#(9(),8()) -> c#(1(),7())
   +#(9(),9()) -> c#(1(),8())
   +#(x,c(y,z)) -> +#(x,z)
   +#(x,c(y,z)) -> c#(y,+(x,z))
   +#(c(x,y),z) -> +#(y,z)
   +#(c(x,y),z) -> c#(x,+(y,z))
   c#(x,c(y,z)) -> +#(x,y)
   c#(x,c(y,z)) -> c#(+(x,y),z)
  TRS:
   +(0(),0()) -> 0()
   +(0(),1()) -> 1()
   +(0(),2()) -> 2()
   +(0(),3()) -> 3()
   +(0(),4()) -> 4()
   +(0(),5()) -> 5()
   +(0(),6()) -> 6()
   +(0(),7()) -> 7()
   +(0(),8()) -> 8()
   +(0(),9()) -> 9()
   +(1(),0()) -> 1()
   +(1(),1()) -> 2()
   +(1(),2()) -> 3()
   +(1(),3()) -> 4()
   +(1(),4()) -> 5()
   +(1(),5()) -> 6()
   +(1(),6()) -> 7()
   +(1(),7()) -> 8()
   +(1(),8()) -> 9()
   +(1(),9()) -> c(1(),0())
   +(2(),0()) -> 2()
   +(2(),1()) -> 3()
   +(2(),2()) -> 4()
   +(2(),3()) -> 5()
   +(2(),4()) -> 6()
   +(2(),5()) -> 7()
   +(2(),6()) -> 8()
   +(2(),7()) -> 9()
   +(2(),8()) -> c(1(),0())
   +(2(),9()) -> c(1(),1())
   +(3(),0()) -> 3()
   +(3(),1()) -> 4()
   +(3(),2()) -> 5()
   +(3(),3()) -> 6()
   +(3(),4()) -> 7()
   +(3(),5()) -> 8()
   +(3(),6()) -> 9()
   +(3(),7()) -> c(1(),0())
   +(3(),8()) -> c(1(),1())
   +(3(),9()) -> c(1(),2())
   +(4(),0()) -> 4()
   +(4(),1()) -> 5()
   +(4(),2()) -> 6()
   +(4(),3()) -> 7()
   +(4(),4()) -> 8()
   +(4(),5()) -> 9()
   +(4(),6()) -> c(1(),0())
   +(4(),7()) -> c(1(),1())
   +(4(),8()) -> c(1(),2())
   +(4(),9()) -> c(1(),3())
   +(5(),0()) -> 5()
   +(5(),1()) -> 6()
   +(5(),2()) -> 7()
   +(5(),3()) -> 8()
   +(5(),4()) -> 9()
   +(5(),5()) -> c(1(),0())
   +(5(),6()) -> c(1(),1())
   +(5(),7()) -> c(1(),2())
   +(5(),8()) -> c(1(),3())
   +(5(),9()) -> c(1(),4())
   +(6(),0()) -> 6()
   +(6(),1()) -> 7()
   +(6(),2()) -> 8()
   +(6(),3()) -> 9()
   +(6(),4()) -> c(1(),0())
   +(6(),5()) -> c(1(),1())
   +(6(),6()) -> c(1(),2())
   +(6(),7()) -> c(1(),3())
   +(6(),8()) -> c(1(),4())
   +(6(),9()) -> c(1(),5())
   +(7(),0()) -> 7()
   +(7(),1()) -> 8()
   +(7(),2()) -> 9()
   +(7(),3()) -> c(1(),0())
   +(7(),4()) -> c(1(),1())
   +(7(),5()) -> c(1(),2())
   +(7(),6()) -> c(1(),3())
   +(7(),7()) -> c(1(),4())
   +(7(),8()) -> c(1(),5())
   +(7(),9()) -> c(1(),6())
   +(8(),0()) -> 8()
   +(8(),1()) -> 9()
   +(8(),2()) -> c(1(),0())
   +(8(),3()) -> c(1(),1())
   +(8(),4()) -> c(1(),2())
   +(8(),5()) -> c(1(),3())
   +(8(),6()) -> c(1(),4())
   +(8(),7()) -> c(1(),5())
   +(8(),8()) -> c(1(),6())
   +(8(),9()) -> c(1(),7())
   +(9(),0()) -> 9()
   +(9(),1()) -> c(1(),0())
   +(9(),2()) -> c(1(),1())
   +(9(),3()) -> c(1(),2())
   +(9(),4()) -> c(1(),3())
   +(9(),5()) -> c(1(),4())
   +(9(),6()) -> c(1(),5())
   +(9(),7()) -> c(1(),6())
   +(9(),8()) -> c(1(),7())
   +(9(),9()) -> c(1(),8())
   +(x,c(y,z)) -> c(y,+(x,z))
   +(c(x,y),z) -> c(x,+(y,z))
   c(0(),x) -> x
   c(x,c(y,z)) -> c(+(x,y),z)
  Matrix Interpretation Processor: dim=2
   
   interpretation:
    [c#](x0, x1) = [0 1]x0 + [0 1]x1,
    
    [+#](x0, x1) = [0 1]x0 + [0 2]x1,
    
                  [0 0]          [0]
    [c](x0, x1) = [0 2]x0 + x1 + [2],
    
          [0]
    [9] = [1],
    
          [1]
    [8] = [1],
    
          [1]
    [7] = [1],
    
          [0]
    [6] = [1],
    
          [0]
    [5] = [1],
    
          [0]
    [4] = [0],
    
          [0]
    [3] = [0],
    
          [0]
    [2] = [0],
    
          [0]
    [1] = [0],
    
                  [0 0]     [1 2]     [1]
    [+](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
    
          [1]
    [0] = [0]
   orientation:
    +#(1(),9()) = 2 >= 0 = c#(1(),0())
    
    +#(2(),8()) = 2 >= 0 = c#(1(),0())
    
    +#(2(),9()) = 2 >= 0 = c#(1(),1())
    
    +#(3(),7()) = 2 >= 0 = c#(1(),0())
    
    +#(3(),8()) = 2 >= 0 = c#(1(),1())
    
    +#(3(),9()) = 2 >= 0 = c#(1(),2())
    
    +#(4(),6()) = 2 >= 0 = c#(1(),0())
    
    +#(4(),7()) = 2 >= 0 = c#(1(),1())
    
    +#(4(),8()) = 2 >= 0 = c#(1(),2())
    
    +#(4(),9()) = 2 >= 0 = c#(1(),3())
    
    +#(5(),5()) = 3 >= 0 = c#(1(),0())
    
    +#(5(),6()) = 3 >= 0 = c#(1(),1())
    
    +#(5(),7()) = 3 >= 0 = c#(1(),2())
    
    +#(5(),8()) = 3 >= 0 = c#(1(),3())
    
    +#(5(),9()) = 3 >= 0 = c#(1(),4())
    
    +#(6(),4()) = 1 >= 0 = c#(1(),0())
    
    +#(6(),5()) = 3 >= 0 = c#(1(),1())
    
    +#(6(),6()) = 3 >= 0 = c#(1(),2())
    
    +#(6(),7()) = 3 >= 0 = c#(1(),3())
    
    +#(6(),8()) = 3 >= 0 = c#(1(),4())
    
    +#(6(),9()) = 3 >= 1 = c#(1(),5())
    
    +#(7(),3()) = 1 >= 0 = c#(1(),0())
    
    +#(7(),4()) = 1 >= 0 = c#(1(),1())
    
    +#(7(),5()) = 3 >= 0 = c#(1(),2())
    
    +#(7(),6()) = 3 >= 0 = c#(1(),3())
    
    +#(7(),7()) = 3 >= 0 = c#(1(),4())
    
    +#(7(),8()) = 3 >= 1 = c#(1(),5())
    
    +#(7(),9()) = 3 >= 1 = c#(1(),6())
    
    +#(8(),2()) = 1 >= 0 = c#(1(),0())
    
    +#(8(),3()) = 1 >= 0 = c#(1(),1())
    
    +#(8(),4()) = 1 >= 0 = c#(1(),2())
    
    +#(8(),5()) = 3 >= 0 = c#(1(),3())
    
    +#(8(),6()) = 3 >= 0 = c#(1(),4())
    
    +#(8(),7()) = 3 >= 1 = c#(1(),5())
    
    +#(8(),8()) = 3 >= 1 = c#(1(),6())
    
    +#(8(),9()) = 3 >= 1 = c#(1(),7())
    
    +#(9(),1()) = 1 >= 0 = c#(1(),0())
    
    +#(9(),2()) = 1 >= 0 = c#(1(),1())
    
    +#(9(),3()) = 1 >= 0 = c#(1(),2())
    
    +#(9(),4()) = 1 >= 0 = c#(1(),3())
    
    +#(9(),5()) = 3 >= 0 = c#(1(),4())
    
    +#(9(),6()) = 3 >= 1 = c#(1(),5())
    
    +#(9(),7()) = 3 >= 1 = c#(1(),6())
    
    +#(9(),8()) = 3 >= 1 = c#(1(),7())
    
    +#(9(),9()) = 3 >= 1 = c#(1(),8())
    
    +#(x,c(y,z)) = [0 1]x + [0 4]y + [0 2]z + [4] >= [0 1]x + [0 2]z = +#(x,z)
    
    +#(x,c(y,z)) = [0 1]x + [0 4]y + [0 2]z + [4] >= [0 1]x + [0 1]y + [0 1]z + [1] = c#(y,+(x,z))
    
    +#(c(x,y),z) = [0 2]x + [0 1]y + [0 2]z + [2] >= [0 1]y + [0 2]z = +#(y,z)
    
    +#(c(x,y),z) = [0 2]x + [0 1]y + [0 2]z + [2] >= [0 1]x + [0 1]y + [0 1]z + [1] = c#(x,+(y,z))
    
    c#(x,c(y,z)) = [0 1]x + [0 2]y + [0 1]z + [2] >= [0 1]x + [0 2]y = +#(x,y)
    
    c#(x,c(y,z)) = [0 1]x + [0 2]y + [0 1]z + [2] >= [0 1]x + [0 1]y + [0 1]z + [1] = c#(+(x,y),z)
    
                 [2]    [1]      
    +(0(),0()) = [1] >= [0] = 0()
    
                 [1]    [0]      
    +(0(),1()) = [1] >= [0] = 1()
    
                 [1]    [0]      
    +(0(),2()) = [1] >= [0] = 2()
    
                 [1]    [0]      
    +(0(),3()) = [1] >= [0] = 3()
    
                 [1]    [0]      
    +(0(),4()) = [1] >= [0] = 4()
    
                 [3]    [0]      
    +(0(),5()) = [2] >= [1] = 5()
    
                 [3]    [0]      
    +(0(),6()) = [2] >= [1] = 6()
    
                 [4]    [1]      
    +(0(),7()) = [2] >= [1] = 7()
    
                 [4]    [1]      
    +(0(),8()) = [2] >= [1] = 8()
    
                 [3]    [0]      
    +(0(),9()) = [2] >= [1] = 9()
    
                 [2]    [0]      
    +(1(),0()) = [1] >= [0] = 1()
    
                 [1]    [0]      
    +(1(),1()) = [1] >= [0] = 2()
    
                 [1]    [0]      
    +(1(),2()) = [1] >= [0] = 3()
    
                 [1]    [0]      
    +(1(),3()) = [1] >= [0] = 4()
    
                 [1]    [0]      
    +(1(),4()) = [1] >= [1] = 5()
    
                 [3]    [0]      
    +(1(),5()) = [2] >= [1] = 6()
    
                 [3]    [1]      
    +(1(),6()) = [2] >= [1] = 7()
    
                 [4]    [1]      
    +(1(),7()) = [2] >= [1] = 8()
    
                 [4]    [0]      
    +(1(),8()) = [2] >= [1] = 9()
    
                 [3]    [1]             
    +(1(),9()) = [2] >= [2] = c(1(),0())
    
                 [2]    [0]      
    +(2(),0()) = [1] >= [0] = 2()
    
                 [1]    [0]      
    +(2(),1()) = [1] >= [0] = 3()
    
                 [1]    [0]      
    +(2(),2()) = [1] >= [0] = 4()
    
                 [1]    [0]      
    +(2(),3()) = [1] >= [1] = 5()
    
                 [1]    [0]      
    +(2(),4()) = [1] >= [1] = 6()
    
                 [3]    [1]      
    +(2(),5()) = [2] >= [1] = 7()
    
                 [3]    [1]      
    +(2(),6()) = [2] >= [1] = 8()
    
                 [4]    [0]      
    +(2(),7()) = [2] >= [1] = 9()
    
                 [4]    [1]             
    +(2(),8()) = [2] >= [2] = c(1(),0())
    
                 [3]    [0]             
    +(2(),9()) = [2] >= [2] = c(1(),1())
    
                 [2]    [0]      
    +(3(),0()) = [1] >= [0] = 3()
    
                 [1]    [0]      
    +(3(),1()) = [1] >= [0] = 4()
    
                 [1]    [0]      
    +(3(),2()) = [1] >= [1] = 5()
    
                 [1]    [0]      
    +(3(),3()) = [1] >= [1] = 6()
    
                 [1]    [1]      
    +(3(),4()) = [1] >= [1] = 7()
    
                 [3]    [1]      
    +(3(),5()) = [2] >= [1] = 8()
    
                 [3]    [0]      
    +(3(),6()) = [2] >= [1] = 9()
    
                 [4]    [1]             
    +(3(),7()) = [2] >= [2] = c(1(),0())
    
                 [4]    [0]             
    +(3(),8()) = [2] >= [2] = c(1(),1())
    
                 [3]    [0]             
    +(3(),9()) = [2] >= [2] = c(1(),2())
    
                 [2]    [0]      
    +(4(),0()) = [1] >= [0] = 4()
    
                 [1]    [0]      
    +(4(),1()) = [1] >= [1] = 5()
    
                 [1]    [0]      
    +(4(),2()) = [1] >= [1] = 6()
    
                 [1]    [1]      
    +(4(),3()) = [1] >= [1] = 7()
    
                 [1]    [1]      
    +(4(),4()) = [1] >= [1] = 8()
    
                 [3]    [0]      
    +(4(),5()) = [2] >= [1] = 9()
    
                 [3]    [1]             
    +(4(),6()) = [2] >= [2] = c(1(),0())
    
                 [4]    [0]             
    +(4(),7()) = [2] >= [2] = c(1(),1())
    
                 [4]    [0]             
    +(4(),8()) = [2] >= [2] = c(1(),2())
    
                 [3]    [0]             
    +(4(),9()) = [2] >= [2] = c(1(),3())
    
                 [2]    [0]      
    +(5(),0()) = [2] >= [1] = 5()
    
                 [1]    [0]      
    +(5(),1()) = [2] >= [1] = 6()
    
                 [1]    [1]      
    +(5(),2()) = [2] >= [1] = 7()
    
                 [1]    [1]      
    +(5(),3()) = [2] >= [1] = 8()
    
                 [1]    [0]      
    +(5(),4()) = [2] >= [1] = 9()
    
                 [3]    [1]             
    +(5(),5()) = [3] >= [2] = c(1(),0())
    
                 [3]    [0]             
    +(5(),6()) = [3] >= [2] = c(1(),1())
    
                 [4]    [0]             
    +(5(),7()) = [3] >= [2] = c(1(),2())
    
                 [4]    [0]             
    +(5(),8()) = [3] >= [2] = c(1(),3())
    
                 [3]    [0]             
    +(5(),9()) = [3] >= [2] = c(1(),4())
    
                 [2]    [0]      
    +(6(),0()) = [2] >= [1] = 6()
    
                 [1]    [1]      
    +(6(),1()) = [2] >= [1] = 7()
    
                 [1]    [1]      
    +(6(),2()) = [2] >= [1] = 8()
    
                 [1]    [0]      
    +(6(),3()) = [2] >= [1] = 9()
    
                 [1]    [1]             
    +(6(),4()) = [2] >= [2] = c(1(),0())
    
                 [3]    [0]             
    +(6(),5()) = [3] >= [2] = c(1(),1())
    
                 [3]    [0]             
    +(6(),6()) = [3] >= [2] = c(1(),2())
    
                 [4]    [0]             
    +(6(),7()) = [3] >= [2] = c(1(),3())
    
                 [4]    [0]             
    +(6(),8()) = [3] >= [2] = c(1(),4())
    
                 [3]    [0]             
    +(6(),9()) = [3] >= [3] = c(1(),5())
    
                 [2]    [1]      
    +(7(),0()) = [2] >= [1] = 7()
    
                 [1]    [1]      
    +(7(),1()) = [2] >= [1] = 8()
    
                 [1]    [0]      
    +(7(),2()) = [2] >= [1] = 9()
    
                 [1]    [1]             
    +(7(),3()) = [2] >= [2] = c(1(),0())
    
                 [1]    [0]             
    +(7(),4()) = [2] >= [2] = c(1(),1())
    
                 [3]    [0]             
    +(7(),5()) = [3] >= [2] = c(1(),2())
    
                 [3]    [0]             
    +(7(),6()) = [3] >= [2] = c(1(),3())
    
                 [4]    [0]             
    +(7(),7()) = [3] >= [2] = c(1(),4())
    
                 [4]    [0]             
    +(7(),8()) = [3] >= [3] = c(1(),5())
    
                 [3]    [0]             
    +(7(),9()) = [3] >= [3] = c(1(),6())
    
                 [2]    [1]      
    +(8(),0()) = [2] >= [1] = 8()
    
                 [1]    [0]      
    +(8(),1()) = [2] >= [1] = 9()
    
                 [1]    [1]             
    +(8(),2()) = [2] >= [2] = c(1(),0())
    
                 [1]    [0]             
    +(8(),3()) = [2] >= [2] = c(1(),1())
    
                 [1]    [0]             
    +(8(),4()) = [2] >= [2] = c(1(),2())
    
                 [3]    [0]             
    +(8(),5()) = [3] >= [2] = c(1(),3())
    
                 [3]    [0]             
    +(8(),6()) = [3] >= [2] = c(1(),4())
    
                 [4]    [0]             
    +(8(),7()) = [3] >= [3] = c(1(),5())
    
                 [4]    [0]             
    +(8(),8()) = [3] >= [3] = c(1(),6())
    
                 [3]    [1]             
    +(8(),9()) = [3] >= [3] = c(1(),7())
    
                 [2]    [0]      
    +(9(),0()) = [2] >= [1] = 9()
    
                 [1]    [1]             
    +(9(),1()) = [2] >= [2] = c(1(),0())
    
                 [1]    [0]             
    +(9(),2()) = [2] >= [2] = c(1(),1())
    
                 [1]    [0]             
    +(9(),3()) = [2] >= [2] = c(1(),2())
    
                 [1]    [0]             
    +(9(),4()) = [2] >= [2] = c(1(),3())
    
                 [3]    [0]             
    +(9(),5()) = [3] >= [2] = c(1(),4())
    
                 [3]    [0]             
    +(9(),6()) = [3] >= [3] = c(1(),5())
    
                 [4]    [0]             
    +(9(),7()) = [3] >= [3] = c(1(),6())
    
                 [4]    [1]             
    +(9(),8()) = [3] >= [3] = c(1(),7())
    
                 [3]    [1]             
    +(9(),9()) = [3] >= [3] = c(1(),8())
    
                  [0 0]    [0 4]    [1 2]    [5]    [0 0]    [0 0]    [1 2]    [1]              
    +(x,c(y,z)) = [0 1]x + [0 2]y + [0 1]z + [3] >= [0 1]x + [0 2]y + [0 1]z + [3] = c(y,+(x,z))
    
                  [0 0]    [0 0]    [1 2]    [1]    [0 0]    [0 0]    [1 2]    [1]              
    +(c(x,y),z) = [0 2]x + [0 1]y + [0 1]z + [3] >= [0 2]x + [0 1]y + [0 1]z + [3] = c(x,+(y,z))
    
                   [0]         
    c(0(),x) = x + [2] >= x = x
    
                  [0 0]    [0 0]        [0]    [0 0]    [0 0]        [0]              
    c(x,c(y,z)) = [0 2]x + [0 2]y + z + [4] >= [0 2]x + [0 2]y + z + [4] = c(+(x,y),z)
   problem:
    DPs:
     
    TRS:
     +(0(),0()) -> 0()
     +(0(),1()) -> 1()
     +(0(),2()) -> 2()
     +(0(),3()) -> 3()
     +(0(),4()) -> 4()
     +(0(),5()) -> 5()
     +(0(),6()) -> 6()
     +(0(),7()) -> 7()
     +(0(),8()) -> 8()
     +(0(),9()) -> 9()
     +(1(),0()) -> 1()
     +(1(),1()) -> 2()
     +(1(),2()) -> 3()
     +(1(),3()) -> 4()
     +(1(),4()) -> 5()
     +(1(),5()) -> 6()
     +(1(),6()) -> 7()
     +(1(),7()) -> 8()
     +(1(),8()) -> 9()
     +(1(),9()) -> c(1(),0())
     +(2(),0()) -> 2()
     +(2(),1()) -> 3()
     +(2(),2()) -> 4()
     +(2(),3()) -> 5()
     +(2(),4()) -> 6()
     +(2(),5()) -> 7()
     +(2(),6()) -> 8()
     +(2(),7()) -> 9()
     +(2(),8()) -> c(1(),0())
     +(2(),9()) -> c(1(),1())
     +(3(),0()) -> 3()
     +(3(),1()) -> 4()
     +(3(),2()) -> 5()
     +(3(),3()) -> 6()
     +(3(),4()) -> 7()
     +(3(),5()) -> 8()
     +(3(),6()) -> 9()
     +(3(),7()) -> c(1(),0())
     +(3(),8()) -> c(1(),1())
     +(3(),9()) -> c(1(),2())
     +(4(),0()) -> 4()
     +(4(),1()) -> 5()
     +(4(),2()) -> 6()
     +(4(),3()) -> 7()
     +(4(),4()) -> 8()
     +(4(),5()) -> 9()
     +(4(),6()) -> c(1(),0())
     +(4(),7()) -> c(1(),1())
     +(4(),8()) -> c(1(),2())
     +(4(),9()) -> c(1(),3())
     +(5(),0()) -> 5()
     +(5(),1()) -> 6()
     +(5(),2()) -> 7()
     +(5(),3()) -> 8()
     +(5(),4()) -> 9()
     +(5(),5()) -> c(1(),0())
     +(5(),6()) -> c(1(),1())
     +(5(),7()) -> c(1(),2())
     +(5(),8()) -> c(1(),3())
     +(5(),9()) -> c(1(),4())
     +(6(),0()) -> 6()
     +(6(),1()) -> 7()
     +(6(),2()) -> 8()
     +(6(),3()) -> 9()
     +(6(),4()) -> c(1(),0())
     +(6(),5()) -> c(1(),1())
     +(6(),6()) -> c(1(),2())
     +(6(),7()) -> c(1(),3())
     +(6(),8()) -> c(1(),4())
     +(6(),9()) -> c(1(),5())
     +(7(),0()) -> 7()
     +(7(),1()) -> 8()
     +(7(),2()) -> 9()
     +(7(),3()) -> c(1(),0())
     +(7(),4()) -> c(1(),1())
     +(7(),5()) -> c(1(),2())
     +(7(),6()) -> c(1(),3())
     +(7(),7()) -> c(1(),4())
     +(7(),8()) -> c(1(),5())
     +(7(),9()) -> c(1(),6())
     +(8(),0()) -> 8()
     +(8(),1()) -> 9()
     +(8(),2()) -> c(1(),0())
     +(8(),3()) -> c(1(),1())
     +(8(),4()) -> c(1(),2())
     +(8(),5()) -> c(1(),3())
     +(8(),6()) -> c(1(),4())
     +(8(),7()) -> c(1(),5())
     +(8(),8()) -> c(1(),6())
     +(8(),9()) -> c(1(),7())
     +(9(),0()) -> 9()
     +(9(),1()) -> c(1(),0())
     +(9(),2()) -> c(1(),1())
     +(9(),3()) -> c(1(),2())
     +(9(),4()) -> c(1(),3())
     +(9(),5()) -> c(1(),4())
     +(9(),6()) -> c(1(),5())
     +(9(),7()) -> c(1(),6())
     +(9(),8()) -> c(1(),7())
     +(9(),9()) -> c(1(),8())
     +(x,c(y,z)) -> c(y,+(x,z))
     +(c(x,y),z) -> c(x,+(y,z))
     c(0(),x) -> x
     c(x,c(y,z)) -> c(+(x,y),z)
   Qed