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=1
   
   usable rules:
    +(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)
   interpretation:
    [c#](x0, x1) = 1/2x0 + 1/2x1,
    
    [+#](x0, x1) = 1/2x0 + x1 + 1/2,
    
    [c](x0, x1) = 2x0 + x1 + 2,
    
    [9] = 2,
    
    [8] = 2,
    
    [7] = 3,
    
    [6] = 2,
    
    [5] = 2,
    
    [4] = 1,
    
    [3] = 1,
    
    [2] = 0,
    
    [1] = 0,
    
    [+](x0, x1) = x0 + x1 + 1,
    
    [0] = 0
   orientation:
    +#(1(),9()) = 5/2 >= 0 = c#(1(),0())
    
    +#(2(),8()) = 5/2 >= 0 = c#(1(),0())
    
    +#(2(),9()) = 5/2 >= 0 = c#(1(),1())
    
    +#(3(),7()) = 4 >= 0 = c#(1(),0())
    
    +#(3(),8()) = 3 >= 0 = c#(1(),1())
    
    +#(3(),9()) = 3 >= 0 = c#(1(),2())
    
    +#(4(),6()) = 3 >= 0 = c#(1(),0())
    
    +#(4(),7()) = 4 >= 0 = c#(1(),1())
    
    +#(4(),8()) = 3 >= 0 = c#(1(),2())
    
    +#(4(),9()) = 3 >= 1/2 = c#(1(),3())
    
    +#(5(),5()) = 7/2 >= 0 = c#(1(),0())
    
    +#(5(),6()) = 7/2 >= 0 = c#(1(),1())
    
    +#(5(),7()) = 9/2 >= 0 = c#(1(),2())
    
    +#(5(),8()) = 7/2 >= 1/2 = c#(1(),3())
    
    +#(5(),9()) = 7/2 >= 1/2 = c#(1(),4())
    
    +#(6(),4()) = 5/2 >= 0 = c#(1(),0())
    
    +#(6(),5()) = 7/2 >= 0 = c#(1(),1())
    
    +#(6(),6()) = 7/2 >= 0 = c#(1(),2())
    
    +#(6(),7()) = 9/2 >= 1/2 = c#(1(),3())
    
    +#(6(),8()) = 7/2 >= 1/2 = c#(1(),4())
    
    +#(6(),9()) = 7/2 >= 1 = c#(1(),5())
    
    +#(7(),3()) = 3 >= 0 = c#(1(),0())
    
    +#(7(),4()) = 3 >= 0 = c#(1(),1())
    
    +#(7(),5()) = 4 >= 0 = c#(1(),2())
    
    +#(7(),6()) = 4 >= 1/2 = c#(1(),3())
    
    +#(7(),7()) = 5 >= 1/2 = c#(1(),4())
    
    +#(7(),8()) = 4 >= 1 = c#(1(),5())
    
    +#(7(),9()) = 4 >= 1 = c#(1(),6())
    
    +#(8(),2()) = 3/2 >= 0 = c#(1(),0())
    
    +#(8(),3()) = 5/2 >= 0 = c#(1(),1())
    
    +#(8(),4()) = 5/2 >= 0 = c#(1(),2())
    
    +#(8(),5()) = 7/2 >= 1/2 = c#(1(),3())
    
    +#(8(),6()) = 7/2 >= 1/2 = c#(1(),4())
    
    +#(8(),7()) = 9/2 >= 1 = c#(1(),5())
    
    +#(8(),8()) = 7/2 >= 1 = c#(1(),6())
    
    +#(8(),9()) = 7/2 >= 3/2 = c#(1(),7())
    
    +#(9(),1()) = 3/2 >= 0 = c#(1(),0())
    
    +#(9(),2()) = 3/2 >= 0 = c#(1(),1())
    
    +#(9(),3()) = 5/2 >= 0 = c#(1(),2())
    
    +#(9(),4()) = 5/2 >= 1/2 = c#(1(),3())
    
    +#(9(),5()) = 7/2 >= 1/2 = c#(1(),4())
    
    +#(9(),6()) = 7/2 >= 1 = c#(1(),5())
    
    +#(9(),7()) = 9/2 >= 1 = c#(1(),6())
    
    +#(9(),8()) = 7/2 >= 3/2 = c#(1(),7())
    
    +#(9(),9()) = 7/2 >= 1 = c#(1(),8())
    
    +#(x,c(y,z)) = 1/2x + 2y + z + 5/2 >= 1/2x + z + 1/2 = +#(x,z)
    
    +#(x,c(y,z)) = 1/2x + 2y + z + 5/2 >= 1/2x + 1/2y + 1/2z + 1/2 = c#(y,+(x,z))
    
    +#(c(x,y),z) = x + 1/2y + z + 3/2 >= 1/2y + z + 1/2 = +#(y,z)
    
    +#(c(x,y),z) = x + 1/2y + z + 3/2 >= 1/2x + 1/2y + 1/2z + 1/2 = c#(x,+(y,z))
    
    c#(x,c(y,z)) = 1/2x + y + 1/2z + 1 >= 1/2x + y + 1/2 = +#(x,y)
    
    c#(x,c(y,z)) = 1/2x + y + 1/2z + 1 >= 1/2x + 1/2y + 1/2z + 1/2 = c#(+(x,y),z)
    
    +(0(),0()) = 1 >= 0 = 0()
    
    +(0(),1()) = 1 >= 0 = 1()
    
    +(0(),2()) = 1 >= 0 = 2()
    
    +(0(),3()) = 2 >= 1 = 3()
    
    +(0(),4()) = 2 >= 1 = 4()
    
    +(0(),5()) = 3 >= 2 = 5()
    
    +(0(),6()) = 3 >= 2 = 6()
    
    +(0(),7()) = 4 >= 3 = 7()
    
    +(0(),8()) = 3 >= 2 = 8()
    
    +(0(),9()) = 3 >= 2 = 9()
    
    +(1(),0()) = 1 >= 0 = 1()
    
    +(1(),1()) = 1 >= 0 = 2()
    
    +(1(),2()) = 1 >= 1 = 3()
    
    +(1(),3()) = 2 >= 1 = 4()
    
    +(1(),4()) = 2 >= 2 = 5()
    
    +(1(),5()) = 3 >= 2 = 6()
    
    +(1(),6()) = 3 >= 3 = 7()
    
    +(1(),7()) = 4 >= 2 = 8()
    
    +(1(),8()) = 3 >= 2 = 9()
    
    +(1(),9()) = 3 >= 2 = c(1(),0())
    
    +(2(),0()) = 1 >= 0 = 2()
    
    +(2(),1()) = 1 >= 1 = 3()
    
    +(2(),2()) = 1 >= 1 = 4()
    
    +(2(),3()) = 2 >= 2 = 5()
    
    +(2(),4()) = 2 >= 2 = 6()
    
    +(2(),5()) = 3 >= 3 = 7()
    
    +(2(),6()) = 3 >= 2 = 8()
    
    +(2(),7()) = 4 >= 2 = 9()
    
    +(2(),8()) = 3 >= 2 = c(1(),0())
    
    +(2(),9()) = 3 >= 2 = c(1(),1())
    
    +(3(),0()) = 2 >= 1 = 3()
    
    +(3(),1()) = 2 >= 1 = 4()
    
    +(3(),2()) = 2 >= 2 = 5()
    
    +(3(),3()) = 3 >= 2 = 6()
    
    +(3(),4()) = 3 >= 3 = 7()
    
    +(3(),5()) = 4 >= 2 = 8()
    
    +(3(),6()) = 4 >= 2 = 9()
    
    +(3(),7()) = 5 >= 2 = c(1(),0())
    
    +(3(),8()) = 4 >= 2 = c(1(),1())
    
    +(3(),9()) = 4 >= 2 = c(1(),2())
    
    +(4(),0()) = 2 >= 1 = 4()
    
    +(4(),1()) = 2 >= 2 = 5()
    
    +(4(),2()) = 2 >= 2 = 6()
    
    +(4(),3()) = 3 >= 3 = 7()
    
    +(4(),4()) = 3 >= 2 = 8()
    
    +(4(),5()) = 4 >= 2 = 9()
    
    +(4(),6()) = 4 >= 2 = c(1(),0())
    
    +(4(),7()) = 5 >= 2 = c(1(),1())
    
    +(4(),8()) = 4 >= 2 = c(1(),2())
    
    +(4(),9()) = 4 >= 3 = c(1(),3())
    
    +(5(),0()) = 3 >= 2 = 5()
    
    +(5(),1()) = 3 >= 2 = 6()
    
    +(5(),2()) = 3 >= 3 = 7()
    
    +(5(),3()) = 4 >= 2 = 8()
    
    +(5(),4()) = 4 >= 2 = 9()
    
    +(5(),5()) = 5 >= 2 = c(1(),0())
    
    +(5(),6()) = 5 >= 2 = c(1(),1())
    
    +(5(),7()) = 6 >= 2 = c(1(),2())
    
    +(5(),8()) = 5 >= 3 = c(1(),3())
    
    +(5(),9()) = 5 >= 3 = c(1(),4())
    
    +(6(),0()) = 3 >= 2 = 6()
    
    +(6(),1()) = 3 >= 3 = 7()
    
    +(6(),2()) = 3 >= 2 = 8()
    
    +(6(),3()) = 4 >= 2 = 9()
    
    +(6(),4()) = 4 >= 2 = c(1(),0())
    
    +(6(),5()) = 5 >= 2 = c(1(),1())
    
    +(6(),6()) = 5 >= 2 = c(1(),2())
    
    +(6(),7()) = 6 >= 3 = c(1(),3())
    
    +(6(),8()) = 5 >= 3 = c(1(),4())
    
    +(6(),9()) = 5 >= 4 = c(1(),5())
    
    +(7(),0()) = 4 >= 3 = 7()
    
    +(7(),1()) = 4 >= 2 = 8()
    
    +(7(),2()) = 4 >= 2 = 9()
    
    +(7(),3()) = 5 >= 2 = c(1(),0())
    
    +(7(),4()) = 5 >= 2 = c(1(),1())
    
    +(7(),5()) = 6 >= 2 = c(1(),2())
    
    +(7(),6()) = 6 >= 3 = c(1(),3())
    
    +(7(),7()) = 7 >= 3 = c(1(),4())
    
    +(7(),8()) = 6 >= 4 = c(1(),5())
    
    +(7(),9()) = 6 >= 4 = c(1(),6())
    
    +(8(),0()) = 3 >= 2 = 8()
    
    +(8(),1()) = 3 >= 2 = 9()
    
    +(8(),2()) = 3 >= 2 = c(1(),0())
    
    +(8(),3()) = 4 >= 2 = c(1(),1())
    
    +(8(),4()) = 4 >= 2 = c(1(),2())
    
    +(8(),5()) = 5 >= 3 = c(1(),3())
    
    +(8(),6()) = 5 >= 3 = c(1(),4())
    
    +(8(),7()) = 6 >= 4 = c(1(),5())
    
    +(8(),8()) = 5 >= 4 = c(1(),6())
    
    +(8(),9()) = 5 >= 5 = c(1(),7())
    
    +(9(),0()) = 3 >= 2 = 9()
    
    +(9(),1()) = 3 >= 2 = c(1(),0())
    
    +(9(),2()) = 3 >= 2 = c(1(),1())
    
    +(9(),3()) = 4 >= 2 = c(1(),2())
    
    +(9(),4()) = 4 >= 3 = c(1(),3())
    
    +(9(),5()) = 5 >= 3 = c(1(),4())
    
    +(9(),6()) = 5 >= 4 = c(1(),5())
    
    +(9(),7()) = 6 >= 4 = c(1(),6())
    
    +(9(),8()) = 5 >= 5 = c(1(),7())
    
    +(9(),9()) = 5 >= 4 = c(1(),8())
    
    +(x,c(y,z)) = x + 2y + z + 3 >= x + 2y + z + 3 = c(y,+(x,z))
    
    +(c(x,y),z) = 2x + y + z + 3 >= 2x + y + z + 3 = c(x,+(y,z))
    
    c(0(),x) = x + 2 >= x = x
    
    c(x,c(y,z)) = 2x + 2y + z + 4 >= 2x + 2y + 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