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:
Complexity Transformation Processor:
strict:
+(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)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0, x1) = x0 + x1 + 12,
[9] = 12,
[8] = 1,
[7] = 3,
[6] = 3,
[5] = 8,
[4] = 1,
[3] = 3,
[2] = 10,
[1] = 6,
[+](x0, x1) = x0 + x1 + 4,
[0] = 1
orientation:
+(0(),0()) = 6 >= 1 = 0()
+(0(),1()) = 11 >= 6 = 1()
+(0(),2()) = 15 >= 10 = 2()
+(0(),3()) = 8 >= 3 = 3()
+(0(),4()) = 6 >= 1 = 4()
+(0(),5()) = 13 >= 8 = 5()
+(0(),6()) = 8 >= 3 = 6()
+(0(),7()) = 8 >= 3 = 7()
+(0(),8()) = 6 >= 1 = 8()
+(0(),9()) = 17 >= 12 = 9()
+(1(),0()) = 11 >= 6 = 1()
+(1(),1()) = 16 >= 10 = 2()
+(1(),2()) = 20 >= 3 = 3()
+(1(),3()) = 13 >= 1 = 4()
+(1(),4()) = 11 >= 8 = 5()
+(1(),5()) = 18 >= 3 = 6()
+(1(),6()) = 13 >= 3 = 7()
+(1(),7()) = 13 >= 1 = 8()
+(1(),8()) = 11 >= 12 = 9()
+(1(),9()) = 22 >= 19 = c(1(),0())
+(2(),0()) = 15 >= 10 = 2()
+(2(),1()) = 20 >= 3 = 3()
+(2(),2()) = 24 >= 1 = 4()
+(2(),3()) = 17 >= 8 = 5()
+(2(),4()) = 15 >= 3 = 6()
+(2(),5()) = 22 >= 3 = 7()
+(2(),6()) = 17 >= 1 = 8()
+(2(),7()) = 17 >= 12 = 9()
+(2(),8()) = 15 >= 19 = c(1(),0())
+(2(),9()) = 26 >= 24 = c(1(),1())
+(3(),0()) = 8 >= 3 = 3()
+(3(),1()) = 13 >= 1 = 4()
+(3(),2()) = 17 >= 8 = 5()
+(3(),3()) = 10 >= 3 = 6()
+(3(),4()) = 8 >= 3 = 7()
+(3(),5()) = 15 >= 1 = 8()
+(3(),6()) = 10 >= 12 = 9()
+(3(),7()) = 10 >= 19 = c(1(),0())
+(3(),8()) = 8 >= 24 = c(1(),1())
+(3(),9()) = 19 >= 28 = c(1(),2())
+(4(),0()) = 6 >= 1 = 4()
+(4(),1()) = 11 >= 8 = 5()
+(4(),2()) = 15 >= 3 = 6()
+(4(),3()) = 8 >= 3 = 7()
+(4(),4()) = 6 >= 1 = 8()
+(4(),5()) = 13 >= 12 = 9()
+(4(),6()) = 8 >= 19 = c(1(),0())
+(4(),7()) = 8 >= 24 = c(1(),1())
+(4(),8()) = 6 >= 28 = c(1(),2())
+(4(),9()) = 17 >= 21 = c(1(),3())
+(5(),0()) = 13 >= 8 = 5()
+(5(),1()) = 18 >= 3 = 6()
+(5(),2()) = 22 >= 3 = 7()
+(5(),3()) = 15 >= 1 = 8()
+(5(),4()) = 13 >= 12 = 9()
+(5(),5()) = 20 >= 19 = c(1(),0())
+(5(),6()) = 15 >= 24 = c(1(),1())
+(5(),7()) = 15 >= 28 = c(1(),2())
+(5(),8()) = 13 >= 21 = c(1(),3())
+(5(),9()) = 24 >= 19 = c(1(),4())
+(6(),0()) = 8 >= 3 = 6()
+(6(),1()) = 13 >= 3 = 7()
+(6(),2()) = 17 >= 1 = 8()
+(6(),3()) = 10 >= 12 = 9()
+(6(),4()) = 8 >= 19 = c(1(),0())
+(6(),5()) = 15 >= 24 = c(1(),1())
+(6(),6()) = 10 >= 28 = c(1(),2())
+(6(),7()) = 10 >= 21 = c(1(),3())
+(6(),8()) = 8 >= 19 = c(1(),4())
+(6(),9()) = 19 >= 26 = c(1(),5())
+(7(),0()) = 8 >= 3 = 7()
+(7(),1()) = 13 >= 1 = 8()
+(7(),2()) = 17 >= 12 = 9()
+(7(),3()) = 10 >= 19 = c(1(),0())
+(7(),4()) = 8 >= 24 = c(1(),1())
+(7(),5()) = 15 >= 28 = c(1(),2())
+(7(),6()) = 10 >= 21 = c(1(),3())
+(7(),7()) = 10 >= 19 = c(1(),4())
+(7(),8()) = 8 >= 26 = c(1(),5())
+(7(),9()) = 19 >= 21 = c(1(),6())
+(8(),0()) = 6 >= 1 = 8()
+(8(),1()) = 11 >= 12 = 9()
+(8(),2()) = 15 >= 19 = c(1(),0())
+(8(),3()) = 8 >= 24 = c(1(),1())
+(8(),4()) = 6 >= 28 = c(1(),2())
+(8(),5()) = 13 >= 21 = c(1(),3())
+(8(),6()) = 8 >= 19 = c(1(),4())
+(8(),7()) = 8 >= 26 = c(1(),5())
+(8(),8()) = 6 >= 21 = c(1(),6())
+(8(),9()) = 17 >= 21 = c(1(),7())
+(9(),0()) = 17 >= 12 = 9()
+(9(),1()) = 22 >= 19 = c(1(),0())
+(9(),2()) = 26 >= 24 = c(1(),1())
+(9(),3()) = 19 >= 28 = c(1(),2())
+(9(),4()) = 17 >= 21 = c(1(),3())
+(9(),5()) = 24 >= 19 = c(1(),4())
+(9(),6()) = 19 >= 26 = c(1(),5())
+(9(),7()) = 19 >= 21 = c(1(),6())
+(9(),8()) = 17 >= 21 = c(1(),7())
+(9(),9()) = 28 >= 19 = c(1(),8())
+(x,c(y,z)) = x + y + z + 16 >= x + y + z + 16 = c(y,+(x,z))
+(c(x,y),z) = x + y + z + 16 >= x + y + z + 16 = c(x,+(y,z))
c(0(),x) = x + 13 >= x = x
c(x,c(y,z)) = x + y + z + 24 >= x + y + z + 16 = c(+(x,y),z)
problem:
strict:
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(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(),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(),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(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),6()) -> c(1(),5())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(x,c(y,z)) -> c(y,+(x,z))
+(c(x,y),z) -> c(x,+(y,z))
weak:
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0, x1) = x0 + x1 + 1,
[9] = 9,
[8] = 10,
[7] = 6,
[6] = 2,
[5] = 8,
[4] = 12,
[3] = 12,
[2] = 8,
[1] = 4,
[+](x0, x1) = x0 + x1,
[0] = 0
orientation:
+(1(),8()) = 14 >= 9 = 9()
+(2(),8()) = 18 >= 5 = c(1(),0())
+(3(),6()) = 14 >= 9 = 9()
+(3(),7()) = 18 >= 5 = c(1(),0())
+(3(),8()) = 22 >= 9 = c(1(),1())
+(3(),9()) = 21 >= 13 = c(1(),2())
+(4(),6()) = 14 >= 5 = c(1(),0())
+(4(),7()) = 18 >= 9 = c(1(),1())
+(4(),8()) = 22 >= 13 = c(1(),2())
+(4(),9()) = 21 >= 17 = c(1(),3())
+(5(),6()) = 10 >= 9 = c(1(),1())
+(5(),7()) = 14 >= 13 = c(1(),2())
+(5(),8()) = 18 >= 17 = c(1(),3())
+(6(),3()) = 14 >= 9 = 9()
+(6(),4()) = 14 >= 5 = c(1(),0())
+(6(),5()) = 10 >= 9 = c(1(),1())
+(6(),6()) = 4 >= 13 = c(1(),2())
+(6(),7()) = 8 >= 17 = c(1(),3())
+(6(),8()) = 12 >= 17 = c(1(),4())
+(6(),9()) = 11 >= 13 = c(1(),5())
+(7(),3()) = 18 >= 5 = c(1(),0())
+(7(),4()) = 18 >= 9 = c(1(),1())
+(7(),5()) = 14 >= 13 = c(1(),2())
+(7(),6()) = 8 >= 17 = c(1(),3())
+(7(),7()) = 12 >= 17 = c(1(),4())
+(7(),8()) = 16 >= 13 = c(1(),5())
+(7(),9()) = 15 >= 7 = c(1(),6())
+(8(),1()) = 14 >= 9 = 9()
+(8(),2()) = 18 >= 5 = c(1(),0())
+(8(),3()) = 22 >= 9 = c(1(),1())
+(8(),4()) = 22 >= 13 = c(1(),2())
+(8(),5()) = 18 >= 17 = c(1(),3())
+(8(),6()) = 12 >= 17 = c(1(),4())
+(8(),7()) = 16 >= 13 = c(1(),5())
+(8(),8()) = 20 >= 7 = c(1(),6())
+(8(),9()) = 19 >= 11 = c(1(),7())
+(9(),3()) = 21 >= 13 = c(1(),2())
+(9(),4()) = 21 >= 17 = c(1(),3())
+(9(),6()) = 11 >= 13 = c(1(),5())
+(9(),7()) = 15 >= 7 = c(1(),6())
+(9(),8()) = 19 >= 11 = c(1(),7())
+(x,c(y,z)) = x + y + z + 1 >= x + y + z + 1 = c(y,+(x,z))
+(c(x,y),z) = x + y + z + 1 >= x + y + z + 1 = c(x,+(y,z))
+(0(),0()) = 0 >= 0 = 0()
+(0(),1()) = 4 >= 4 = 1()
+(0(),2()) = 8 >= 8 = 2()
+(0(),3()) = 12 >= 12 = 3()
+(0(),4()) = 12 >= 12 = 4()
+(0(),5()) = 8 >= 8 = 5()
+(0(),6()) = 2 >= 2 = 6()
+(0(),7()) = 6 >= 6 = 7()
+(0(),8()) = 10 >= 10 = 8()
+(0(),9()) = 9 >= 9 = 9()
+(1(),0()) = 4 >= 4 = 1()
+(1(),1()) = 8 >= 8 = 2()
+(1(),2()) = 12 >= 12 = 3()
+(1(),3()) = 16 >= 12 = 4()
+(1(),4()) = 16 >= 8 = 5()
+(1(),5()) = 12 >= 2 = 6()
+(1(),6()) = 6 >= 6 = 7()
+(1(),7()) = 10 >= 10 = 8()
+(1(),9()) = 13 >= 5 = c(1(),0())
+(2(),0()) = 8 >= 8 = 2()
+(2(),1()) = 12 >= 12 = 3()
+(2(),2()) = 16 >= 12 = 4()
+(2(),3()) = 20 >= 8 = 5()
+(2(),4()) = 20 >= 2 = 6()
+(2(),5()) = 16 >= 6 = 7()
+(2(),6()) = 10 >= 10 = 8()
+(2(),7()) = 14 >= 9 = 9()
+(2(),9()) = 17 >= 9 = c(1(),1())
+(3(),0()) = 12 >= 12 = 3()
+(3(),1()) = 16 >= 12 = 4()
+(3(),2()) = 20 >= 8 = 5()
+(3(),3()) = 24 >= 2 = 6()
+(3(),4()) = 24 >= 6 = 7()
+(3(),5()) = 20 >= 10 = 8()
+(4(),0()) = 12 >= 12 = 4()
+(4(),1()) = 16 >= 8 = 5()
+(4(),2()) = 20 >= 2 = 6()
+(4(),3()) = 24 >= 6 = 7()
+(4(),4()) = 24 >= 10 = 8()
+(4(),5()) = 20 >= 9 = 9()
+(5(),0()) = 8 >= 8 = 5()
+(5(),1()) = 12 >= 2 = 6()
+(5(),2()) = 16 >= 6 = 7()
+(5(),3()) = 20 >= 10 = 8()
+(5(),4()) = 20 >= 9 = 9()
+(5(),5()) = 16 >= 5 = c(1(),0())
+(5(),9()) = 17 >= 17 = c(1(),4())
+(6(),0()) = 2 >= 2 = 6()
+(6(),1()) = 6 >= 6 = 7()
+(6(),2()) = 10 >= 10 = 8()
+(7(),0()) = 6 >= 6 = 7()
+(7(),1()) = 10 >= 10 = 8()
+(7(),2()) = 14 >= 9 = 9()
+(8(),0()) = 10 >= 10 = 8()
+(9(),0()) = 9 >= 9 = 9()
+(9(),1()) = 13 >= 5 = c(1(),0())
+(9(),2()) = 17 >= 9 = c(1(),1())
+(9(),5()) = 17 >= 17 = c(1(),4())
+(9(),9()) = 18 >= 15 = c(1(),8())
c(0(),x) = x + 1 >= x = x
c(x,c(y,z)) = x + y + z + 2 >= x + y + z + 1 = c(+(x,y),z)
problem:
strict:
+(6(),6()) -> c(1(),2())
+(6(),7()) -> c(1(),3())
+(6(),8()) -> c(1(),4())
+(6(),9()) -> c(1(),5())
+(7(),6()) -> c(1(),3())
+(7(),7()) -> c(1(),4())
+(8(),6()) -> c(1(),4())
+(9(),6()) -> c(1(),5())
+(x,c(y,z)) -> c(y,+(x,z))
+(c(x,y),z) -> c(x,+(y,z))
weak:
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(6(),3()) -> 9()
+(6(),4()) -> c(1(),0())
+(6(),5()) -> c(1(),1())
+(7(),3()) -> c(1(),0())
+(7(),4()) -> c(1(),1())
+(7(),5()) -> c(1(),2())
+(7(),8()) -> c(1(),5())
+(7(),9()) -> c(1(),6())
+(8(),1()) -> 9()
+(8(),2()) -> c(1(),0())
+(8(),3()) -> c(1(),1())
+(8(),4()) -> c(1(),2())
+(8(),5()) -> c(1(),3())
+(8(),7()) -> c(1(),5())
+(8(),8()) -> c(1(),6())
+(8(),9()) -> c(1(),7())
+(9(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0, x1) = x0 + x1,
[9] = 8,
[8] = 8,
[7] = 4,
[6] = 5,
[5] = 6,
[4] = 8,
[3] = 8,
[2] = 4,
[1] = 4,
[+](x0, x1) = x0 + x1,
[0] = 8
orientation:
+(6(),6()) = 10 >= 8 = c(1(),2())
+(6(),7()) = 9 >= 12 = c(1(),3())
+(6(),8()) = 13 >= 12 = c(1(),4())
+(6(),9()) = 13 >= 10 = c(1(),5())
+(7(),6()) = 9 >= 12 = c(1(),3())
+(7(),7()) = 8 >= 12 = c(1(),4())
+(8(),6()) = 13 >= 12 = c(1(),4())
+(9(),6()) = 13 >= 10 = c(1(),5())
+(x,c(y,z)) = x + y + z >= x + y + z = c(y,+(x,z))
+(c(x,y),z) = x + y + z >= x + y + z = c(x,+(y,z))
+(1(),8()) = 12 >= 8 = 9()
+(2(),8()) = 12 >= 12 = c(1(),0())
+(3(),6()) = 13 >= 8 = 9()
+(3(),7()) = 12 >= 12 = c(1(),0())
+(3(),8()) = 16 >= 8 = c(1(),1())
+(3(),9()) = 16 >= 8 = c(1(),2())
+(4(),6()) = 13 >= 12 = c(1(),0())
+(4(),7()) = 12 >= 8 = c(1(),1())
+(4(),8()) = 16 >= 8 = c(1(),2())
+(4(),9()) = 16 >= 12 = c(1(),3())
+(5(),6()) = 11 >= 8 = c(1(),1())
+(5(),7()) = 10 >= 8 = c(1(),2())
+(5(),8()) = 14 >= 12 = c(1(),3())
+(6(),3()) = 13 >= 8 = 9()
+(6(),4()) = 13 >= 12 = c(1(),0())
+(6(),5()) = 11 >= 8 = c(1(),1())
+(7(),3()) = 12 >= 12 = c(1(),0())
+(7(),4()) = 12 >= 8 = c(1(),1())
+(7(),5()) = 10 >= 8 = c(1(),2())
+(7(),8()) = 12 >= 10 = c(1(),5())
+(7(),9()) = 12 >= 9 = c(1(),6())
+(8(),1()) = 12 >= 8 = 9()
+(8(),2()) = 12 >= 12 = c(1(),0())
+(8(),3()) = 16 >= 8 = c(1(),1())
+(8(),4()) = 16 >= 8 = c(1(),2())
+(8(),5()) = 14 >= 12 = c(1(),3())
+(8(),7()) = 12 >= 10 = c(1(),5())
+(8(),8()) = 16 >= 9 = c(1(),6())
+(8(),9()) = 16 >= 8 = c(1(),7())
+(9(),3()) = 16 >= 8 = c(1(),2())
+(9(),4()) = 16 >= 12 = c(1(),3())
+(9(),7()) = 12 >= 9 = c(1(),6())
+(9(),8()) = 16 >= 8 = c(1(),7())
+(0(),0()) = 16 >= 8 = 0()
+(0(),1()) = 12 >= 4 = 1()
+(0(),2()) = 12 >= 4 = 2()
+(0(),3()) = 16 >= 8 = 3()
+(0(),4()) = 16 >= 8 = 4()
+(0(),5()) = 14 >= 6 = 5()
+(0(),6()) = 13 >= 5 = 6()
+(0(),7()) = 12 >= 4 = 7()
+(0(),8()) = 16 >= 8 = 8()
+(0(),9()) = 16 >= 8 = 9()
+(1(),0()) = 12 >= 4 = 1()
+(1(),1()) = 8 >= 4 = 2()
+(1(),2()) = 8 >= 8 = 3()
+(1(),3()) = 12 >= 8 = 4()
+(1(),4()) = 12 >= 6 = 5()
+(1(),5()) = 10 >= 5 = 6()
+(1(),6()) = 9 >= 4 = 7()
+(1(),7()) = 8 >= 8 = 8()
+(1(),9()) = 12 >= 12 = c(1(),0())
+(2(),0()) = 12 >= 4 = 2()
+(2(),1()) = 8 >= 8 = 3()
+(2(),2()) = 8 >= 8 = 4()
+(2(),3()) = 12 >= 6 = 5()
+(2(),4()) = 12 >= 5 = 6()
+(2(),5()) = 10 >= 4 = 7()
+(2(),6()) = 9 >= 8 = 8()
+(2(),7()) = 8 >= 8 = 9()
+(2(),9()) = 12 >= 8 = c(1(),1())
+(3(),0()) = 16 >= 8 = 3()
+(3(),1()) = 12 >= 8 = 4()
+(3(),2()) = 12 >= 6 = 5()
+(3(),3()) = 16 >= 5 = 6()
+(3(),4()) = 16 >= 4 = 7()
+(3(),5()) = 14 >= 8 = 8()
+(4(),0()) = 16 >= 8 = 4()
+(4(),1()) = 12 >= 6 = 5()
+(4(),2()) = 12 >= 5 = 6()
+(4(),3()) = 16 >= 4 = 7()
+(4(),4()) = 16 >= 8 = 8()
+(4(),5()) = 14 >= 8 = 9()
+(5(),0()) = 14 >= 6 = 5()
+(5(),1()) = 10 >= 5 = 6()
+(5(),2()) = 10 >= 4 = 7()
+(5(),3()) = 14 >= 8 = 8()
+(5(),4()) = 14 >= 8 = 9()
+(5(),5()) = 12 >= 12 = c(1(),0())
+(5(),9()) = 14 >= 12 = c(1(),4())
+(6(),0()) = 13 >= 5 = 6()
+(6(),1()) = 9 >= 4 = 7()
+(6(),2()) = 9 >= 8 = 8()
+(7(),0()) = 12 >= 4 = 7()
+(7(),1()) = 8 >= 8 = 8()
+(7(),2()) = 8 >= 8 = 9()
+(8(),0()) = 16 >= 8 = 8()
+(9(),0()) = 16 >= 8 = 9()
+(9(),1()) = 12 >= 12 = c(1(),0())
+(9(),2()) = 12 >= 8 = c(1(),1())
+(9(),5()) = 14 >= 12 = c(1(),4())
+(9(),9()) = 16 >= 12 = c(1(),8())
c(0(),x) = x + 8 >= x = x
c(x,c(y,z)) = x + y + z >= x + y + z = c(+(x,y),z)
problem:
strict:
+(6(),7()) -> c(1(),3())
+(7(),6()) -> c(1(),3())
+(7(),7()) -> c(1(),4())
+(x,c(y,z)) -> c(y,+(x,z))
+(c(x,y),z) -> c(x,+(y,z))
weak:
+(6(),6()) -> c(1(),2())
+(6(),8()) -> c(1(),4())
+(6(),9()) -> c(1(),5())
+(8(),6()) -> c(1(),4())
+(9(),6()) -> c(1(),5())
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(6(),3()) -> 9()
+(6(),4()) -> c(1(),0())
+(6(),5()) -> c(1(),1())
+(7(),3()) -> c(1(),0())
+(7(),4()) -> c(1(),1())
+(7(),5()) -> c(1(),2())
+(7(),8()) -> c(1(),5())
+(7(),9()) -> c(1(),6())
+(8(),1()) -> 9()
+(8(),2()) -> c(1(),0())
+(8(),3()) -> c(1(),1())
+(8(),4()) -> c(1(),2())
+(8(),5()) -> c(1(),3())
+(8(),7()) -> c(1(),5())
+(8(),8()) -> c(1(),6())
+(8(),9()) -> c(1(),7())
+(9(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[c](x0, x1) = x0 + x1 + 33,
[9] = 16,
[8] = 32,
[7] = 32,
[6] = 16,
[5] = 24,
[4] = 34,
[3] = 17,
[2] = 2,
[1] = 0,
[+](x0, x1) = x0 + x1 + 33,
[0] = 0
orientation:
+(6(),7()) = 81 >= 50 = c(1(),3())
+(7(),6()) = 81 >= 50 = c(1(),3())
+(7(),7()) = 97 >= 67 = c(1(),4())
+(x,c(y,z)) = x + y + z + 66 >= x + y + z + 66 = c(y,+(x,z))
+(c(x,y),z) = x + y + z + 66 >= x + y + z + 66 = c(x,+(y,z))
+(6(),6()) = 65 >= 35 = c(1(),2())
+(6(),8()) = 81 >= 67 = c(1(),4())
+(6(),9()) = 65 >= 57 = c(1(),5())
+(8(),6()) = 81 >= 67 = c(1(),4())
+(9(),6()) = 65 >= 57 = c(1(),5())
+(1(),8()) = 65 >= 16 = 9()
+(2(),8()) = 67 >= 33 = c(1(),0())
+(3(),6()) = 66 >= 16 = 9()
+(3(),7()) = 82 >= 33 = c(1(),0())
+(3(),8()) = 82 >= 33 = c(1(),1())
+(3(),9()) = 66 >= 35 = c(1(),2())
+(4(),6()) = 83 >= 33 = c(1(),0())
+(4(),7()) = 99 >= 33 = c(1(),1())
+(4(),8()) = 99 >= 35 = c(1(),2())
+(4(),9()) = 83 >= 50 = c(1(),3())
+(5(),6()) = 73 >= 33 = c(1(),1())
+(5(),7()) = 89 >= 35 = c(1(),2())
+(5(),8()) = 89 >= 50 = c(1(),3())
+(6(),3()) = 66 >= 16 = 9()
+(6(),4()) = 83 >= 33 = c(1(),0())
+(6(),5()) = 73 >= 33 = c(1(),1())
+(7(),3()) = 82 >= 33 = c(1(),0())
+(7(),4()) = 99 >= 33 = c(1(),1())
+(7(),5()) = 89 >= 35 = c(1(),2())
+(7(),8()) = 97 >= 57 = c(1(),5())
+(7(),9()) = 81 >= 49 = c(1(),6())
+(8(),1()) = 65 >= 16 = 9()
+(8(),2()) = 67 >= 33 = c(1(),0())
+(8(),3()) = 82 >= 33 = c(1(),1())
+(8(),4()) = 99 >= 35 = c(1(),2())
+(8(),5()) = 89 >= 50 = c(1(),3())
+(8(),7()) = 97 >= 57 = c(1(),5())
+(8(),8()) = 97 >= 49 = c(1(),6())
+(8(),9()) = 81 >= 65 = c(1(),7())
+(9(),3()) = 66 >= 35 = c(1(),2())
+(9(),4()) = 83 >= 50 = c(1(),3())
+(9(),7()) = 81 >= 49 = c(1(),6())
+(9(),8()) = 81 >= 65 = c(1(),7())
+(0(),0()) = 33 >= 0 = 0()
+(0(),1()) = 33 >= 0 = 1()
+(0(),2()) = 35 >= 2 = 2()
+(0(),3()) = 50 >= 17 = 3()
+(0(),4()) = 67 >= 34 = 4()
+(0(),5()) = 57 >= 24 = 5()
+(0(),6()) = 49 >= 16 = 6()
+(0(),7()) = 65 >= 32 = 7()
+(0(),8()) = 65 >= 32 = 8()
+(0(),9()) = 49 >= 16 = 9()
+(1(),0()) = 33 >= 0 = 1()
+(1(),1()) = 33 >= 2 = 2()
+(1(),2()) = 35 >= 17 = 3()
+(1(),3()) = 50 >= 34 = 4()
+(1(),4()) = 67 >= 24 = 5()
+(1(),5()) = 57 >= 16 = 6()
+(1(),6()) = 49 >= 32 = 7()
+(1(),7()) = 65 >= 32 = 8()
+(1(),9()) = 49 >= 33 = c(1(),0())
+(2(),0()) = 35 >= 2 = 2()
+(2(),1()) = 35 >= 17 = 3()
+(2(),2()) = 37 >= 34 = 4()
+(2(),3()) = 52 >= 24 = 5()
+(2(),4()) = 69 >= 16 = 6()
+(2(),5()) = 59 >= 32 = 7()
+(2(),6()) = 51 >= 32 = 8()
+(2(),7()) = 67 >= 16 = 9()
+(2(),9()) = 51 >= 33 = c(1(),1())
+(3(),0()) = 50 >= 17 = 3()
+(3(),1()) = 50 >= 34 = 4()
+(3(),2()) = 52 >= 24 = 5()
+(3(),3()) = 67 >= 16 = 6()
+(3(),4()) = 84 >= 32 = 7()
+(3(),5()) = 74 >= 32 = 8()
+(4(),0()) = 67 >= 34 = 4()
+(4(),1()) = 67 >= 24 = 5()
+(4(),2()) = 69 >= 16 = 6()
+(4(),3()) = 84 >= 32 = 7()
+(4(),4()) = 101 >= 32 = 8()
+(4(),5()) = 91 >= 16 = 9()
+(5(),0()) = 57 >= 24 = 5()
+(5(),1()) = 57 >= 16 = 6()
+(5(),2()) = 59 >= 32 = 7()
+(5(),3()) = 74 >= 32 = 8()
+(5(),4()) = 91 >= 16 = 9()
+(5(),5()) = 81 >= 33 = c(1(),0())
+(5(),9()) = 73 >= 67 = c(1(),4())
+(6(),0()) = 49 >= 16 = 6()
+(6(),1()) = 49 >= 32 = 7()
+(6(),2()) = 51 >= 32 = 8()
+(7(),0()) = 65 >= 32 = 7()
+(7(),1()) = 65 >= 32 = 8()
+(7(),2()) = 67 >= 16 = 9()
+(8(),0()) = 65 >= 32 = 8()
+(9(),0()) = 49 >= 16 = 9()
+(9(),1()) = 49 >= 33 = c(1(),0())
+(9(),2()) = 51 >= 33 = c(1(),1())
+(9(),5()) = 73 >= 67 = c(1(),4())
+(9(),9()) = 65 >= 65 = c(1(),8())
c(0(),x) = x + 33 >= x = x
c(x,c(y,z)) = x + y + z + 66 >= x + y + z + 66 = c(+(x,y),z)
problem:
strict:
+(x,c(y,z)) -> c(y,+(x,z))
+(c(x,y),z) -> c(x,+(y,z))
weak:
+(6(),7()) -> c(1(),3())
+(7(),6()) -> c(1(),3())
+(7(),7()) -> c(1(),4())
+(6(),6()) -> c(1(),2())
+(6(),8()) -> c(1(),4())
+(6(),9()) -> c(1(),5())
+(8(),6()) -> c(1(),4())
+(9(),6()) -> c(1(),5())
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(6(),3()) -> 9()
+(6(),4()) -> c(1(),0())
+(6(),5()) -> c(1(),1())
+(7(),3()) -> c(1(),0())
+(7(),4()) -> c(1(),1())
+(7(),5()) -> c(1(),2())
+(7(),8()) -> c(1(),5())
+(7(),9()) -> c(1(),6())
+(8(),1()) -> 9()
+(8(),2()) -> c(1(),0())
+(8(),3()) -> c(1(),1())
+(8(),4()) -> c(1(),2())
+(8(),5()) -> c(1(),3())
+(8(),7()) -> c(1(),5())
+(8(),8()) -> c(1(),6())
+(8(),9()) -> c(1(),7())
+(9(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {12,11}
transitions:
+0(8,1) -> 11*
+0(3,1) -> 11*
+0(8,3) -> 11*
+0(3,3) -> 11*
+0(8,5) -> 11*
+0(3,5) -> 11*
+0(8,7) -> 11*
+0(3,7) -> 11*
+0(8,9) -> 11*
+0(3,9) -> 11*
+0(9,2) -> 11*
+0(4,2) -> 11*
+0(9,4) -> 11*
+0(4,4) -> 11*
+0(9,6) -> 11*
+0(4,6) -> 11*
+0(9,8) -> 11*
+0(4,8) -> 11*
+0(9,10) -> 11*
+0(4,10) -> 11*
+0(10,1) -> 11*
+0(5,1) -> 11*
+0(10,3) -> 11*
+0(5,3) -> 11*
+0(10,5) -> 11*
+0(5,5) -> 11*
+0(10,7) -> 11*
+0(5,7) -> 11*
+0(10,9) -> 11*
+0(5,9) -> 11*
+0(6,2) -> 11*
+0(1,2) -> 11*
+0(6,4) -> 11*
+0(1,4) -> 11*
+0(6,6) -> 11*
+0(1,6) -> 11*
+0(6,8) -> 11*
+0(1,8) -> 11*
+0(6,10) -> 11*
+0(1,10) -> 11*
+0(7,1) -> 11*
+0(2,1) -> 11*
+0(7,3) -> 11*
+0(2,3) -> 11*
+0(7,5) -> 11*
+0(2,5) -> 11*
+0(7,7) -> 11*
+0(2,7) -> 11*
+0(7,9) -> 11*
+0(2,9) -> 11*
+0(8,2) -> 11*
+0(3,2) -> 11*
+0(8,4) -> 11*
+0(3,4) -> 11*
+0(8,6) -> 11*
+0(3,6) -> 11*
+0(8,8) -> 11*
+0(3,8) -> 11*
+0(8,10) -> 11*
+0(3,10) -> 11*
+0(9,1) -> 11*
+0(4,1) -> 11*
+0(9,3) -> 11*
+0(4,3) -> 11*
+0(9,5) -> 11*
+0(4,5) -> 11*
+0(9,7) -> 11*
+0(4,7) -> 11*
+0(9,9) -> 11*
+0(4,9) -> 11*
+0(10,2) -> 11*
+0(5,2) -> 11*
+0(10,4) -> 11*
+0(5,4) -> 11*
+0(10,6) -> 11*
+0(5,6) -> 11*
+0(10,8) -> 11*
+0(5,8) -> 11*
+0(10,10) -> 11*
+0(5,10) -> 11*
+0(6,1) -> 11*
+0(1,1) -> 11*
+0(6,3) -> 11*
+0(1,3) -> 11*
+0(6,5) -> 11*
+0(1,5) -> 11*
+0(6,7) -> 11*
+0(1,7) -> 11*
+0(6,9) -> 11*
+0(1,9) -> 11*
+0(7,2) -> 11*
+0(2,2) -> 11*
+0(7,4) -> 11*
+0(2,4) -> 11*
+0(7,6) -> 11*
+0(2,6) -> 11*
+0(7,8) -> 11*
+0(2,8) -> 11*
+0(7,10) -> 11*
+0(2,10) -> 11*
c0(8,1) -> 12*
c0(3,1) -> 11,12
c0(8,3) -> 12*
c0(3,3) -> 11,12
c0(8,5) -> 12*
c0(3,5) -> 11,12
c0(8,7) -> 12*
c0(3,7) -> 11,12
c0(8,9) -> 12*
c0(3,9) -> 11,12
c0(9,2) -> 12*
c0(4,2) -> 12*
c0(9,4) -> 12*
c0(4,4) -> 12*
c0(9,6) -> 12*
c0(4,6) -> 12*
c0(9,8) -> 12*
c0(4,8) -> 12*
c0(9,10) -> 12*
c0(4,10) -> 12*
c0(10,1) -> 12*
c0(5,1) -> 12*
c0(10,3) -> 12*
c0(5,3) -> 12*
c0(10,5) -> 12*
c0(5,5) -> 12*
c0(10,7) -> 12*
c0(5,7) -> 12*
c0(10,9) -> 12*
c0(5,9) -> 12*
c0(6,2) -> 12*
c0(1,2) -> 12*
c0(6,4) -> 12*
c0(1,4) -> 12*
c0(6,6) -> 12*
c0(1,6) -> 12*
c0(6,8) -> 12*
c0(1,8) -> 12*
c0(6,10) -> 12*
c0(1,10) -> 12*
c0(7,1) -> 12*
c0(2,1) -> 12*
c0(7,3) -> 12*
c0(2,3) -> 12*
c0(7,5) -> 12*
c0(2,5) -> 12*
c0(7,7) -> 12*
c0(2,7) -> 12*
c0(7,9) -> 12*
c0(2,9) -> 12*
c0(8,2) -> 12*
c0(3,2) -> 11,12
c0(8,4) -> 12*
c0(3,4) -> 11,12
c0(8,6) -> 12*
c0(3,6) -> 11,12
c0(8,8) -> 12*
c0(3,8) -> 12*
c0(8,10) -> 12*
c0(3,10) -> 11,12
c0(9,1) -> 12*
c0(4,1) -> 12*
c0(9,3) -> 12*
c0(4,3) -> 12*
c0(9,5) -> 12*
c0(4,5) -> 12*
c0(9,7) -> 12*
c0(4,7) -> 12*
c0(9,9) -> 12*
c0(4,9) -> 12*
c0(10,2) -> 12*
c0(5,2) -> 12*
c0(10,4) -> 12*
c0(5,4) -> 12*
c0(10,6) -> 12*
c0(5,6) -> 12*
c0(10,8) -> 12*
c0(5,8) -> 12*
c0(10,10) -> 12*
c0(5,10) -> 12*
c0(6,1) -> 12*
c0(1,1) -> 12*
c0(6,3) -> 12*
c0(1,3) -> 12*
c0(6,5) -> 12*
c0(1,5) -> 12*
c0(6,7) -> 12*
c0(1,7) -> 12*
c0(6,9) -> 12*
c0(1,9) -> 12*
c0(7,2) -> 12*
c0(2,2) -> 12*
c0(7,4) -> 12*
c0(2,4) -> 12*
c0(7,6) -> 12*
c0(2,6) -> 12*
c0(7,8) -> 12*
c0(2,8) -> 12*
c0(7,10) -> 12*
c0(2,10) -> 12*
60() -> 11,1
70() -> 11,2
10() -> 11,3
30() -> 11,4
40() -> 11,5
20() -> 11,6
80() -> 11,7
90() -> 11,8
50() -> 11,9
00() -> 11,10
1 -> 12*
2 -> 12*
3 -> 12*
4 -> 12*
5 -> 12*
6 -> 12*
7 -> 12*
8 -> 12*
9 -> 12*
10 -> 12*
problem:
strict:
+(c(x,y),z) -> c(x,+(y,z))
weak:
+(x,c(y,z)) -> c(y,+(x,z))
+(6(),7()) -> c(1(),3())
+(7(),6()) -> c(1(),3())
+(7(),7()) -> c(1(),4())
+(6(),6()) -> c(1(),2())
+(6(),8()) -> c(1(),4())
+(6(),9()) -> c(1(),5())
+(8(),6()) -> c(1(),4())
+(9(),6()) -> c(1(),5())
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(6(),3()) -> 9()
+(6(),4()) -> c(1(),0())
+(6(),5()) -> c(1(),1())
+(7(),3()) -> c(1(),0())
+(7(),4()) -> c(1(),1())
+(7(),5()) -> c(1(),2())
+(7(),8()) -> c(1(),5())
+(7(),9()) -> c(1(),6())
+(8(),1()) -> 9()
+(8(),2()) -> c(1(),0())
+(8(),3()) -> c(1(),1())
+(8(),4()) -> c(1(),2())
+(8(),5()) -> c(1(),3())
+(8(),7()) -> c(1(),5())
+(8(),8()) -> c(1(),6())
+(8(),9()) -> c(1(),7())
+(9(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {12,11}
transitions:
+0(8,1) -> 11*
+0(3,1) -> 11*
+0(8,3) -> 11*
+0(3,3) -> 11*
+0(8,5) -> 11*
+0(3,5) -> 11*
+0(8,7) -> 11*
+0(3,7) -> 11*
+0(8,9) -> 11*
+0(3,9) -> 11*
+0(9,2) -> 11*
+0(4,2) -> 11*
+0(9,4) -> 11*
+0(4,4) -> 11*
+0(9,6) -> 11*
+0(4,6) -> 11*
+0(9,8) -> 11*
+0(4,8) -> 11*
+0(9,10) -> 11*
+0(4,10) -> 11*
+0(10,1) -> 11*
+0(5,1) -> 11*
+0(10,3) -> 11*
+0(5,3) -> 11*
+0(10,5) -> 11*
+0(5,5) -> 11*
+0(10,7) -> 11*
+0(5,7) -> 11*
+0(10,9) -> 11*
+0(5,9) -> 11*
+0(6,2) -> 11*
+0(1,2) -> 11*
+0(6,4) -> 11*
+0(1,4) -> 11*
+0(6,6) -> 11*
+0(1,6) -> 11*
+0(6,8) -> 11*
+0(1,8) -> 11*
+0(6,10) -> 11*
+0(1,10) -> 11*
+0(7,1) -> 11*
+0(2,1) -> 11*
+0(7,3) -> 11*
+0(2,3) -> 11*
+0(7,5) -> 11*
+0(2,5) -> 11*
+0(7,7) -> 11*
+0(2,7) -> 11*
+0(7,9) -> 11*
+0(2,9) -> 11*
+0(8,2) -> 11*
+0(3,2) -> 11*
+0(8,4) -> 11*
+0(3,4) -> 11*
+0(8,6) -> 11*
+0(3,6) -> 11*
+0(8,8) -> 11*
+0(3,8) -> 11*
+0(8,10) -> 11*
+0(3,10) -> 11*
+0(9,1) -> 11*
+0(4,1) -> 11*
+0(9,3) -> 11*
+0(4,3) -> 11*
+0(9,5) -> 11*
+0(4,5) -> 11*
+0(9,7) -> 11*
+0(4,7) -> 11*
+0(9,9) -> 11*
+0(4,9) -> 11*
+0(10,2) -> 11*
+0(5,2) -> 11*
+0(10,4) -> 11*
+0(5,4) -> 11*
+0(10,6) -> 11*
+0(5,6) -> 11*
+0(10,8) -> 11*
+0(5,8) -> 11*
+0(10,10) -> 11*
+0(5,10) -> 11*
+0(6,1) -> 11*
+0(1,1) -> 11*
+0(6,3) -> 11*
+0(1,3) -> 11*
+0(6,5) -> 11*
+0(1,5) -> 11*
+0(6,7) -> 11*
+0(1,7) -> 11*
+0(6,9) -> 11*
+0(1,9) -> 11*
+0(7,2) -> 11*
+0(2,2) -> 11*
+0(7,4) -> 11*
+0(2,4) -> 11*
+0(7,6) -> 11*
+0(2,6) -> 11*
+0(7,8) -> 11*
+0(2,8) -> 11*
+0(7,10) -> 11*
+0(2,10) -> 11*
c0(8,1) -> 12*
c0(3,1) -> 11,12
c0(8,3) -> 12*
c0(3,3) -> 11,12
c0(8,5) -> 12*
c0(3,5) -> 11,12
c0(8,7) -> 12*
c0(3,7) -> 11,12
c0(8,9) -> 12*
c0(3,9) -> 11,12
c0(9,2) -> 12*
c0(4,2) -> 12*
c0(9,4) -> 12*
c0(4,4) -> 12*
c0(9,6) -> 12*
c0(4,6) -> 12*
c0(9,8) -> 12*
c0(4,8) -> 12*
c0(9,10) -> 12*
c0(4,10) -> 12*
c0(10,1) -> 12*
c0(5,1) -> 12*
c0(10,3) -> 12*
c0(5,3) -> 12*
c0(10,5) -> 12*
c0(5,5) -> 12*
c0(10,7) -> 12*
c0(5,7) -> 12*
c0(10,9) -> 12*
c0(5,9) -> 12*
c0(6,2) -> 12*
c0(1,2) -> 12*
c0(6,4) -> 12*
c0(1,4) -> 12*
c0(6,6) -> 12*
c0(1,6) -> 12*
c0(6,8) -> 12*
c0(1,8) -> 12*
c0(6,10) -> 12*
c0(1,10) -> 12*
c0(7,1) -> 12*
c0(2,1) -> 12*
c0(7,3) -> 12*
c0(2,3) -> 12*
c0(7,5) -> 12*
c0(2,5) -> 12*
c0(7,7) -> 12*
c0(2,7) -> 12*
c0(7,9) -> 12*
c0(2,9) -> 12*
c0(8,2) -> 12*
c0(3,2) -> 11,12
c0(8,4) -> 12*
c0(3,4) -> 11,12
c0(8,6) -> 12*
c0(3,6) -> 11,12
c0(8,8) -> 12*
c0(3,8) -> 12*
c0(8,10) -> 12*
c0(3,10) -> 11,12
c0(9,1) -> 12*
c0(4,1) -> 12*
c0(9,3) -> 12*
c0(4,3) -> 12*
c0(9,5) -> 12*
c0(4,5) -> 12*
c0(9,7) -> 12*
c0(4,7) -> 12*
c0(9,9) -> 12*
c0(4,9) -> 12*
c0(10,2) -> 12*
c0(5,2) -> 12*
c0(10,4) -> 12*
c0(5,4) -> 12*
c0(10,6) -> 12*
c0(5,6) -> 12*
c0(10,8) -> 12*
c0(5,8) -> 12*
c0(10,10) -> 12*
c0(5,10) -> 12*
c0(6,1) -> 12*
c0(1,1) -> 12*
c0(6,3) -> 12*
c0(1,3) -> 12*
c0(6,5) -> 12*
c0(1,5) -> 12*
c0(6,7) -> 12*
c0(1,7) -> 12*
c0(6,9) -> 12*
c0(1,9) -> 12*
c0(7,2) -> 12*
c0(2,2) -> 12*
c0(7,4) -> 12*
c0(2,4) -> 12*
c0(7,6) -> 12*
c0(2,6) -> 12*
c0(7,8) -> 12*
c0(2,8) -> 12*
c0(7,10) -> 12*
c0(2,10) -> 12*
60() -> 11,1
70() -> 11,2
10() -> 11,3
30() -> 11,4
40() -> 11,5
20() -> 11,6
80() -> 11,7
90() -> 11,8
50() -> 11,9
00() -> 11,10
1 -> 12*
2 -> 12*
3 -> 12*
4 -> 12*
5 -> 12*
6 -> 12*
7 -> 12*
8 -> 12*
9 -> 12*
10 -> 12*
problem:
strict:
weak:
+(c(x,y),z) -> c(x,+(y,z))
+(x,c(y,z)) -> c(y,+(x,z))
+(6(),7()) -> c(1(),3())
+(7(),6()) -> c(1(),3())
+(7(),7()) -> c(1(),4())
+(6(),6()) -> c(1(),2())
+(6(),8()) -> c(1(),4())
+(6(),9()) -> c(1(),5())
+(8(),6()) -> c(1(),4())
+(9(),6()) -> c(1(),5())
+(1(),8()) -> 9()
+(2(),8()) -> c(1(),0())
+(3(),6()) -> 9()
+(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(),6()) -> c(1(),1())
+(5(),7()) -> c(1(),2())
+(5(),8()) -> c(1(),3())
+(6(),3()) -> 9()
+(6(),4()) -> c(1(),0())
+(6(),5()) -> c(1(),1())
+(7(),3()) -> c(1(),0())
+(7(),4()) -> c(1(),1())
+(7(),5()) -> c(1(),2())
+(7(),8()) -> c(1(),5())
+(7(),9()) -> c(1(),6())
+(8(),1()) -> 9()
+(8(),2()) -> c(1(),0())
+(8(),3()) -> c(1(),1())
+(8(),4()) -> c(1(),2())
+(8(),5()) -> c(1(),3())
+(8(),7()) -> c(1(),5())
+(8(),8()) -> c(1(),6())
+(8(),9()) -> c(1(),7())
+(9(),3()) -> c(1(),2())
+(9(),4()) -> c(1(),3())
+(9(),7()) -> c(1(),6())
+(9(),8()) -> c(1(),7())
+(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(),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(),9()) -> c(1(),1())
+(3(),0()) -> 3()
+(3(),1()) -> 4()
+(3(),2()) -> 5()
+(3(),3()) -> 6()
+(3(),4()) -> 7()
+(3(),5()) -> 8()
+(4(),0()) -> 4()
+(4(),1()) -> 5()
+(4(),2()) -> 6()
+(4(),3()) -> 7()
+(4(),4()) -> 8()
+(4(),5()) -> 9()
+(5(),0()) -> 5()
+(5(),1()) -> 6()
+(5(),2()) -> 7()
+(5(),3()) -> 8()
+(5(),4()) -> 9()
+(5(),5()) -> c(1(),0())
+(5(),9()) -> c(1(),4())
+(6(),0()) -> 6()
+(6(),1()) -> 7()
+(6(),2()) -> 8()
+(7(),0()) -> 7()
+(7(),1()) -> 8()
+(7(),2()) -> 9()
+(8(),0()) -> 8()
+(9(),0()) -> 9()
+(9(),1()) -> c(1(),0())
+(9(),2()) -> c(1(),1())
+(9(),5()) -> c(1(),4())
+(9(),9()) -> c(1(),8())
c(0(),x) -> x
c(x,c(y,z)) -> c(+(x,y),z)
Qed