We consider the following Problem:
Strict 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)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict 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)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
0() = [0]
[0]
1() = [0]
[0]
2() = [0]
[0]
3() = [0]
[0]
4() = [0]
[0]
5() = [0]
[0]
6() = [0]
[0]
7() = [0]
[0]
8() = [0]
[1]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(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)) -> 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 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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {c(0(), x) -> x}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
0() = [0]
[0]
1() = [0]
[0]
2() = [0]
[0]
3() = [0]
[0]
4() = [0]
[0]
5() = [0]
[0]
6() = [0]
[0]
7() = [0]
[0]
8() = [0]
[0]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(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)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))
, c(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
0() = [2]
[0]
1() = [3]
[2]
2() = [0]
[3]
3() = [3]
[2]
4() = [1]
[2]
5() = [1]
[3]
6() = [1]
[0]
7() = [2]
[1]
8() = [0]
[0]
9() = [1]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(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(), 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(), 4()) -> c(1(), 1())
, +(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)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))
, c(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [1]
0() = [0]
[0]
1() = [0]
[0]
2() = [0]
[0]
3() = [0]
[0]
4() = [0]
[0]
5() = [1]
[1]
6() = [0]
[0]
7() = [0]
[1]
8() = [0]
[0]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(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())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 7()) -> c(1(), 3())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(7(), 4()) -> c(1(), 1())
, +(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(), 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(), 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(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
0() = [0]
[0]
1() = [0]
[0]
2() = [0]
[1]
3() = [0]
[0]
4() = [0]
[0]
5() = [0]
[1]
6() = [0]
[0]
7() = [1]
[1]
8() = [0]
[0]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(7(), 8()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(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(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {+(7(), 8()) -> c(1(), 5())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
0() = [0]
[0]
1() = [0]
[0]
2() = [0]
[0]
3() = [0]
[0]
4() = [0]
[0]
5() = [0]
[0]
6() = [0]
[0]
7() = [1]
[0]
8() = [0]
[0]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(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(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(7(), 8()) -> c(1(), 5())
, +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(9(), 8()) -> c(1(), 7())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [1]
0() = [1]
[0]
1() = [0]
[0]
2() = [2]
[1]
3() = [2]
[2]
4() = [0]
[2]
5() = [0]
[2]
6() = [0]
[2]
7() = [0]
[2]
8() = [1]
[3]
9() = [0]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(9(), 9()) -> c(1(), 8())
, +(x, c(y, z)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))
, c(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(9(), 8()) -> c(1(), 7())
, +(7(), 8()) -> c(1(), 5())
, +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {+(9(), 9()) -> c(1(), 8())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [1]
0() = [0]
[0]
1() = [0]
[3]
2() = [0]
[2]
3() = [0]
[1]
4() = [1]
[0]
5() = [1]
[2]
6() = [1]
[1]
7() = [2]
[2]
8() = [2]
[1]
9() = [2]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(x, c(y, z)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))
, c(x, c(y, z)) -> c(+(x, y), z)}
Weak Trs:
{ +(9(), 9()) -> c(1(), 8())
, +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(9(), 8()) -> c(1(), 7())
, +(7(), 8()) -> c(1(), 5())
, +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {c(x, c(y, z)) -> c(+(x, y), z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(+) = {}, Uargs(c) = {1, 2}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
+(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
0() = [1]
[0]
1() = [1]
[0]
2() = [1]
[0]
3() = [2]
[0]
4() = [2]
[0]
5() = [3]
[0]
6() = [3]
[0]
7() = [3]
[0]
8() = [3]
[0]
9() = [3]
[0]
c(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ +(x, c(y, z)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))}
Weak Trs:
{ c(x, c(y, z)) -> c(+(x, y), z)
, +(9(), 9()) -> c(1(), 8())
, +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(9(), 8()) -> c(1(), 7())
, +(7(), 8()) -> c(1(), 5())
, +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ +(x, c(y, z)) -> c(y, +(x, z))
, +(c(x, y), z) -> c(x, +(y, z))}
Weak Trs:
{ c(x, c(y, z)) -> c(+(x, y), z)
, +(9(), 9()) -> c(1(), 8())
, +(1(), 9()) -> c(1(), 0())
, +(2(), 8()) -> c(1(), 0())
, +(2(), 9()) -> c(1(), 1())
, +(3(), 8()) -> c(1(), 1())
, +(3(), 9()) -> c(1(), 2())
, +(4(), 6()) -> c(1(), 0())
, +(4(), 8()) -> c(1(), 2())
, +(4(), 9()) -> c(1(), 3())
, +(6(), 4()) -> c(1(), 0())
, +(6(), 6()) -> c(1(), 2())
, +(6(), 8()) -> c(1(), 4())
, +(6(), 9()) -> c(1(), 5())
, +(8(), 2()) -> c(1(), 0())
, +(8(), 3()) -> c(1(), 1())
, +(8(), 4()) -> c(1(), 2())
, +(8(), 6()) -> c(1(), 4())
, +(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(), 6()) -> c(1(), 5())
, +(9(), 8()) -> c(1(), 7())
, +(7(), 8()) -> c(1(), 5())
, +(4(), 7()) -> c(1(), 1())
, +(6(), 7()) -> c(1(), 3())
, +(7(), 4()) -> c(1(), 1())
, +(7(), 6()) -> c(1(), 3())
, +(7(), 7()) -> c(1(), 4())
, +(7(), 9()) -> c(1(), 6())
, +(8(), 7()) -> c(1(), 5())
, +(9(), 7()) -> c(1(), 6())
, +(5(), 5()) -> c(1(), 0())
, +(5(), 6()) -> c(1(), 1())
, +(5(), 8()) -> c(1(), 3())
, +(5(), 9()) -> c(1(), 4())
, +(6(), 5()) -> c(1(), 1())
, +(8(), 5()) -> c(1(), 3())
, +(9(), 5()) -> c(1(), 4())
, +(3(), 7()) -> c(1(), 0())
, +(5(), 7()) -> c(1(), 2())
, +(7(), 3()) -> c(1(), 0())
, +(7(), 5()) -> c(1(), 2())
, c(0(), x) -> x
, +(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()
, +(2(), 0()) -> 2()
, +(2(), 1()) -> 3()
, +(2(), 2()) -> 4()
, +(2(), 3()) -> 5()
, +(2(), 4()) -> 6()
, +(2(), 5()) -> 7()
, +(2(), 6()) -> 8()
, +(2(), 7()) -> 9()
, +(3(), 0()) -> 3()
, +(3(), 1()) -> 4()
, +(3(), 2()) -> 5()
, +(3(), 3()) -> 6()
, +(3(), 4()) -> 7()
, +(3(), 5()) -> 8()
, +(3(), 6()) -> 9()
, +(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()
, +(6(), 0()) -> 6()
, +(6(), 1()) -> 7()
, +(6(), 2()) -> 8()
, +(6(), 3()) -> 9()
, +(7(), 0()) -> 7()
, +(7(), 1()) -> 8()
, +(7(), 2()) -> 9()
, +(8(), 0()) -> 8()
, +(8(), 1()) -> 9()
, +(9(), 0()) -> 9()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The problem is match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ +_0(2, 2) -> 1
, 0_0() -> 1
, 0_0() -> 2
, 1_0() -> 1
, 1_0() -> 2
, 2_0() -> 1
, 2_0() -> 2
, 3_0() -> 1
, 3_0() -> 2
, 4_0() -> 1
, 4_0() -> 2
, 5_0() -> 1
, 5_0() -> 2
, 6_0() -> 1
, 6_0() -> 2
, 7_0() -> 1
, 7_0() -> 2
, 8_0() -> 1
, 8_0() -> 2
, 9_0() -> 1
, 9_0() -> 2
, c_0(2, 2) -> 1}
Hurray, we answered YES(?,O(n^1))