*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
0() -> n__0()
U11(tt(),N) -> activate(N)
U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__isNat(X)) -> isNat(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(tt(),X) -> activate(X)
isNat(X) -> n__isNat(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2)))
isNat(n__s(V1)) -> isNat(activate(V1))
plus(N,0()) -> U11(isNat(N),N)
plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0}
Obligation:
Innermost
basic terms: {0,U11,U21,activate,and,isNat,plus,s}/{n__0,n__isNat,n__plus,n__s,tt}
Applied Processor:
InnermostRuleRemoval
Proof:
Arguments of following rules are not normal-forms.
plus(N,0()) -> U11(isNat(N),N)
plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N)
All above mentioned rules can be savely removed.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
0() -> n__0()
U11(tt(),N) -> activate(N)
U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__isNat(X)) -> isNat(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(tt(),X) -> activate(X)
isNat(X) -> n__isNat(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2)))
isNat(n__s(V1)) -> isNat(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0}
Obligation:
Innermost
basic terms: {0,U11,U21,activate,and,isNat,plus,s}/{n__0,n__isNat,n__plus,n__s,tt}
Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
Proof:
The problem is match-bounded by 5.
The enriched problem is compatible with follwoing automaton.
0_0() -> 1
0_1() -> 2
0_1() -> 4
0_1() -> 5
0_1() -> 19
0_1() -> 20
0_1() -> 23
0_1() -> 24
U11_0(7,7) -> 2
U11_0(7,8) -> 2
U11_0(7,9) -> 2
U11_0(7,10) -> 2
U11_0(7,13) -> 2
U11_0(8,7) -> 2
U11_0(8,8) -> 2
U11_0(8,9) -> 2
U11_0(8,10) -> 2
U11_0(8,13) -> 2
U11_0(9,7) -> 2
U11_0(9,8) -> 2
U11_0(9,9) -> 2
U11_0(9,10) -> 2
U11_0(9,13) -> 2
U11_0(10,7) -> 2
U11_0(10,8) -> 2
U11_0(10,9) -> 2
U11_0(10,10) -> 2
U11_0(10,13) -> 2
U11_0(13,7) -> 2
U11_0(13,8) -> 2
U11_0(13,9) -> 2
U11_0(13,10) -> 2
U11_0(13,13) -> 2
U21_0(7,7,7) -> 3
U21_0(7,7,8) -> 3
U21_0(7,7,9) -> 3
U21_0(7,7,10) -> 3
U21_0(7,7,13) -> 3
U21_0(7,8,7) -> 3
U21_0(7,8,8) -> 3
U21_0(7,8,9) -> 3
U21_0(7,8,10) -> 3
U21_0(7,8,13) -> 3
U21_0(7,9,7) -> 3
U21_0(7,9,8) -> 3
U21_0(7,9,9) -> 3
U21_0(7,9,10) -> 3
U21_0(7,9,13) -> 3
U21_0(7,10,7) -> 3
U21_0(7,10,8) -> 3
U21_0(7,10,9) -> 3
U21_0(7,10,10) -> 3
U21_0(7,10,13) -> 3
U21_0(7,13,7) -> 3
U21_0(7,13,8) -> 3
U21_0(7,13,9) -> 3
U21_0(7,13,10) -> 3
U21_0(7,13,13) -> 3
U21_0(8,7,7) -> 3
U21_0(8,7,8) -> 3
U21_0(8,7,9) -> 3
U21_0(8,7,10) -> 3
U21_0(8,7,13) -> 3
U21_0(8,8,7) -> 3
U21_0(8,8,8) -> 3
U21_0(8,8,9) -> 3
U21_0(8,8,10) -> 3
U21_0(8,8,13) -> 3
U21_0(8,9,7) -> 3
U21_0(8,9,8) -> 3
U21_0(8,9,9) -> 3
U21_0(8,9,10) -> 3
U21_0(8,9,13) -> 3
U21_0(8,10,7) -> 3
U21_0(8,10,8) -> 3
U21_0(8,10,9) -> 3
U21_0(8,10,10) -> 3
U21_0(8,10,13) -> 3
U21_0(8,13,7) -> 3
U21_0(8,13,8) -> 3
U21_0(8,13,9) -> 3
U21_0(8,13,10) -> 3
U21_0(8,13,13) -> 3
U21_0(9,7,7) -> 3
U21_0(9,7,8) -> 3
U21_0(9,7,9) -> 3
U21_0(9,7,10) -> 3
U21_0(9,7,13) -> 3
U21_0(9,8,7) -> 3
U21_0(9,8,8) -> 3
U21_0(9,8,9) -> 3
U21_0(9,8,10) -> 3
U21_0(9,8,13) -> 3
U21_0(9,9,7) -> 3
U21_0(9,9,8) -> 3
U21_0(9,9,9) -> 3
U21_0(9,9,10) -> 3
U21_0(9,9,13) -> 3
U21_0(9,10,7) -> 3
U21_0(9,10,8) -> 3
U21_0(9,10,9) -> 3
U21_0(9,10,10) -> 3
U21_0(9,10,13) -> 3
U21_0(9,13,7) -> 3
U21_0(9,13,8) -> 3
U21_0(9,13,9) -> 3
U21_0(9,13,10) -> 3
U21_0(9,13,13) -> 3
U21_0(10,7,7) -> 3
U21_0(10,7,8) -> 3
U21_0(10,7,9) -> 3
U21_0(10,7,10) -> 3
U21_0(10,7,13) -> 3
U21_0(10,8,7) -> 3
U21_0(10,8,8) -> 3
U21_0(10,8,9) -> 3
U21_0(10,8,10) -> 3
U21_0(10,8,13) -> 3
U21_0(10,9,7) -> 3
U21_0(10,9,8) -> 3
U21_0(10,9,9) -> 3
U21_0(10,9,10) -> 3
U21_0(10,9,13) -> 3
U21_0(10,10,7) -> 3
U21_0(10,10,8) -> 3
U21_0(10,10,9) -> 3
U21_0(10,10,10) -> 3
U21_0(10,10,13) -> 3
U21_0(10,13,7) -> 3
U21_0(10,13,8) -> 3
U21_0(10,13,9) -> 3
U21_0(10,13,10) -> 3
U21_0(10,13,13) -> 3
U21_0(13,7,7) -> 3
U21_0(13,7,8) -> 3
U21_0(13,7,9) -> 3
U21_0(13,7,10) -> 3
U21_0(13,7,13) -> 3
U21_0(13,8,7) -> 3
U21_0(13,8,8) -> 3
U21_0(13,8,9) -> 3
U21_0(13,8,10) -> 3
U21_0(13,8,13) -> 3
U21_0(13,9,7) -> 3
U21_0(13,9,8) -> 3
U21_0(13,9,9) -> 3
U21_0(13,9,10) -> 3
U21_0(13,9,13) -> 3
U21_0(13,10,7) -> 3
U21_0(13,10,8) -> 3
U21_0(13,10,9) -> 3
U21_0(13,10,10) -> 3
U21_0(13,10,13) -> 3
U21_0(13,13,7) -> 3
U21_0(13,13,8) -> 3
U21_0(13,13,9) -> 3
U21_0(13,13,10) -> 3
U21_0(13,13,13) -> 3
activate_0(7) -> 4
activate_0(8) -> 4
activate_0(9) -> 4
activate_0(10) -> 4
activate_0(13) -> 4
activate_1(7) -> 2
activate_1(7) -> 5
activate_1(8) -> 2
activate_1(8) -> 5
activate_1(9) -> 2
activate_1(9) -> 5
activate_1(10) -> 2
activate_1(10) -> 5
activate_1(13) -> 2
activate_1(13) -> 5
activate_1(16) -> 21
activate_1(16) -> 24
activate_1(18) -> 21
activate_1(18) -> 24
activate_2(7) -> 19
activate_2(7) -> 20
activate_2(8) -> 20
activate_2(9) -> 20
activate_2(10) -> 20
activate_2(13) -> 20
activate_2(16) -> 2
activate_2(16) -> 4
activate_2(16) -> 5
activate_2(16) -> 6
activate_2(16) -> 15
activate_2(16) -> 17
activate_2(16) -> 20
activate_2(16) -> 21
activate_2(16) -> 24
activate_2(18) -> 2
activate_2(18) -> 4
activate_2(18) -> 5
activate_2(18) -> 6
activate_2(18) -> 15
activate_2(18) -> 17
activate_2(18) -> 20
activate_2(18) -> 21
activate_2(18) -> 24
activate_2(22) -> 2
activate_2(22) -> 4
activate_2(22) -> 5
activate_2(22) -> 6
activate_2(22) -> 15
activate_2(22) -> 17
activate_2(22) -> 20
activate_2(22) -> 21
activate_2(22) -> 24
activate_3(7) -> 23
activate_3(7) -> 24
activate_3(8) -> 24
activate_3(9) -> 24
activate_3(10) -> 24
activate_3(13) -> 24
activate_3(18) -> 2
activate_3(18) -> 4
activate_3(18) -> 5
activate_3(18) -> 6
activate_3(18) -> 15
activate_3(18) -> 17
activate_3(18) -> 20
activate_3(18) -> 21
activate_3(18) -> 24
activate_3(22) -> 2
activate_3(22) -> 4
activate_3(22) -> 5
activate_3(22) -> 6
activate_3(22) -> 15
activate_3(22) -> 17
activate_3(22) -> 20
activate_3(22) -> 21
activate_3(22) -> 24
activate_4(22) -> 2
activate_4(22) -> 4
activate_4(22) -> 5
activate_4(22) -> 6
activate_4(22) -> 15
activate_4(22) -> 17
activate_4(22) -> 20
activate_4(22) -> 21
activate_4(22) -> 24
and_0(7,7) -> 5
and_0(7,8) -> 5
and_0(7,9) -> 5
and_0(7,10) -> 5
and_0(7,13) -> 5
and_0(8,7) -> 5
and_0(8,8) -> 5
and_0(8,9) -> 5
and_0(8,10) -> 5
and_0(8,13) -> 5
and_0(9,7) -> 5
and_0(9,8) -> 5
and_0(9,9) -> 5
and_0(9,10) -> 5
and_0(9,13) -> 5
and_0(10,7) -> 5
and_0(10,8) -> 5
and_0(10,9) -> 5
and_0(10,10) -> 5
and_0(10,13) -> 5
and_0(13,7) -> 5
and_0(13,8) -> 5
and_0(13,9) -> 5
and_0(13,10) -> 5
and_0(13,13) -> 5
and_1(15,16) -> 2
and_1(15,16) -> 4
and_1(15,16) -> 5
and_1(15,16) -> 6
and_1(15,16) -> 15
and_1(15,16) -> 17
and_1(15,16) -> 20
and_1(20,16) -> 21
and_1(20,16) -> 24
and_2(17,18) -> 2
and_2(17,18) -> 4
and_2(17,18) -> 5
and_2(17,18) -> 6
and_2(17,18) -> 15
and_2(17,18) -> 17
and_2(17,18) -> 20
and_2(20,18) -> 21
and_2(20,18) -> 24
and_3(21,22) -> 2
and_3(21,22) -> 4
and_3(21,22) -> 5
and_3(21,22) -> 6
and_3(21,22) -> 15
and_3(21,22) -> 17
and_3(21,22) -> 20
and_3(21,22) -> 21
and_3(21,22) -> 24
isNat_0(7) -> 6
isNat_0(8) -> 6
isNat_0(9) -> 6
isNat_0(10) -> 6
isNat_0(13) -> 6
isNat_1(5) -> 2
isNat_1(5) -> 4
isNat_1(5) -> 5
isNat_1(5) -> 6
isNat_1(5) -> 15
isNat_1(5) -> 17
isNat_1(5) -> 20
isNat_1(5) -> 21
isNat_1(5) -> 24
isNat_1(7) -> 2
isNat_1(7) -> 4
isNat_1(7) -> 5
isNat_1(7) -> 20
isNat_1(7) -> 24
isNat_1(8) -> 2
isNat_1(8) -> 4
isNat_1(8) -> 5
isNat_1(8) -> 20
isNat_1(8) -> 24
isNat_1(9) -> 2
isNat_1(9) -> 4
isNat_1(9) -> 5
isNat_1(9) -> 20
isNat_1(9) -> 24
isNat_1(10) -> 2
isNat_1(10) -> 4
isNat_1(10) -> 5
isNat_1(10) -> 20
isNat_1(10) -> 24
isNat_1(13) -> 2
isNat_1(13) -> 4
isNat_1(13) -> 5
isNat_1(13) -> 20
isNat_1(13) -> 24
isNat_2(5) -> 2
isNat_2(5) -> 4
isNat_2(5) -> 5
isNat_2(5) -> 6
isNat_2(5) -> 15
isNat_2(5) -> 17
isNat_2(5) -> 20
isNat_2(5) -> 21
isNat_2(5) -> 24
isNat_2(19) -> 17
isNat_2(20) -> 2
isNat_2(20) -> 4
isNat_2(20) -> 5
isNat_2(20) -> 6
isNat_2(20) -> 15
isNat_2(20) -> 17
isNat_2(20) -> 20
isNat_2(20) -> 21
isNat_2(20) -> 24
isNat_3(20) -> 2
isNat_3(20) -> 4
isNat_3(20) -> 5
isNat_3(20) -> 6
isNat_3(20) -> 15
isNat_3(20) -> 17
isNat_3(20) -> 20
isNat_3(20) -> 21
isNat_3(20) -> 24
isNat_3(23) -> 21
isNat_3(24) -> 2
isNat_3(24) -> 4
isNat_3(24) -> 5
isNat_3(24) -> 6
isNat_3(24) -> 15
isNat_3(24) -> 17
isNat_3(24) -> 20
isNat_3(24) -> 21
isNat_3(24) -> 24
isNat_4(24) -> 2
isNat_4(24) -> 4
isNat_4(24) -> 5
isNat_4(24) -> 6
isNat_4(24) -> 15
isNat_4(24) -> 17
isNat_4(24) -> 20
isNat_4(24) -> 21
isNat_4(24) -> 24
n__0_0() -> 2
n__0_0() -> 4
n__0_0() -> 5
n__0_0() -> 7
n__0_0() -> 19
n__0_0() -> 20
n__0_0() -> 23
n__0_0() -> 24
n__0_1() -> 1
n__0_2() -> 2
n__0_2() -> 4
n__0_2() -> 5
n__0_2() -> 19
n__0_2() -> 20
n__0_2() -> 23
n__0_2() -> 24
n__isNat_0(7) -> 2
n__isNat_0(7) -> 4
n__isNat_0(7) -> 5
n__isNat_0(7) -> 8
n__isNat_0(7) -> 20
n__isNat_0(7) -> 24
n__isNat_0(8) -> 2
n__isNat_0(8) -> 4
n__isNat_0(8) -> 5
n__isNat_0(8) -> 8
n__isNat_0(8) -> 20
n__isNat_0(8) -> 24
n__isNat_0(9) -> 2
n__isNat_0(9) -> 4
n__isNat_0(9) -> 5
n__isNat_0(9) -> 8
n__isNat_0(9) -> 20
n__isNat_0(9) -> 24
n__isNat_0(10) -> 2
n__isNat_0(10) -> 4
n__isNat_0(10) -> 5
n__isNat_0(10) -> 8
n__isNat_0(10) -> 20
n__isNat_0(10) -> 24
n__isNat_0(13) -> 2
n__isNat_0(13) -> 4
n__isNat_0(13) -> 5
n__isNat_0(13) -> 8
n__isNat_0(13) -> 20
n__isNat_0(13) -> 24
n__isNat_1(5) -> 2
n__isNat_1(5) -> 4
n__isNat_1(5) -> 5
n__isNat_1(5) -> 6
n__isNat_1(5) -> 15
n__isNat_1(5) -> 16
n__isNat_1(5) -> 17
n__isNat_1(5) -> 20
n__isNat_1(5) -> 21
n__isNat_1(5) -> 24
n__isNat_1(7) -> 6
n__isNat_1(8) -> 6
n__isNat_1(9) -> 6
n__isNat_1(10) -> 6
n__isNat_1(13) -> 6
n__isNat_2(5) -> 2
n__isNat_2(5) -> 4
n__isNat_2(5) -> 5
n__isNat_2(5) -> 6
n__isNat_2(5) -> 15
n__isNat_2(5) -> 17
n__isNat_2(5) -> 20
n__isNat_2(5) -> 21
n__isNat_2(5) -> 24
n__isNat_2(7) -> 2
n__isNat_2(7) -> 4
n__isNat_2(7) -> 5
n__isNat_2(7) -> 20
n__isNat_2(7) -> 24
n__isNat_2(8) -> 2
n__isNat_2(8) -> 4
n__isNat_2(8) -> 5
n__isNat_2(8) -> 20
n__isNat_2(8) -> 24
n__isNat_2(9) -> 2
n__isNat_2(9) -> 4
n__isNat_2(9) -> 5
n__isNat_2(9) -> 20
n__isNat_2(9) -> 24
n__isNat_2(10) -> 2
n__isNat_2(10) -> 4
n__isNat_2(10) -> 5
n__isNat_2(10) -> 20
n__isNat_2(10) -> 24
n__isNat_2(13) -> 2
n__isNat_2(13) -> 4
n__isNat_2(13) -> 5
n__isNat_2(13) -> 20
n__isNat_2(13) -> 24
n__isNat_2(20) -> 2
n__isNat_2(20) -> 4
n__isNat_2(20) -> 5
n__isNat_2(20) -> 6
n__isNat_2(20) -> 15
n__isNat_2(20) -> 17
n__isNat_2(20) -> 18
n__isNat_2(20) -> 20
n__isNat_2(20) -> 21
n__isNat_2(20) -> 24
n__isNat_3(5) -> 2
n__isNat_3(5) -> 4
n__isNat_3(5) -> 5
n__isNat_3(5) -> 6
n__isNat_3(5) -> 15
n__isNat_3(5) -> 17
n__isNat_3(5) -> 20
n__isNat_3(5) -> 21
n__isNat_3(5) -> 24
n__isNat_3(19) -> 17
n__isNat_3(20) -> 2
n__isNat_3(20) -> 4
n__isNat_3(20) -> 5
n__isNat_3(20) -> 6
n__isNat_3(20) -> 15
n__isNat_3(20) -> 17
n__isNat_3(20) -> 20
n__isNat_3(20) -> 21
n__isNat_3(20) -> 24
n__isNat_3(24) -> 2
n__isNat_3(24) -> 4
n__isNat_3(24) -> 5
n__isNat_3(24) -> 6
n__isNat_3(24) -> 15
n__isNat_3(24) -> 17
n__isNat_3(24) -> 20
n__isNat_3(24) -> 21
n__isNat_3(24) -> 22
n__isNat_3(24) -> 24
n__isNat_4(20) -> 2
n__isNat_4(20) -> 4
n__isNat_4(20) -> 5
n__isNat_4(20) -> 6
n__isNat_4(20) -> 15
n__isNat_4(20) -> 17
n__isNat_4(20) -> 20
n__isNat_4(20) -> 21
n__isNat_4(20) -> 24
n__isNat_4(23) -> 21
n__isNat_4(24) -> 2
n__isNat_4(24) -> 4
n__isNat_4(24) -> 5
n__isNat_4(24) -> 6
n__isNat_4(24) -> 15
n__isNat_4(24) -> 17
n__isNat_4(24) -> 20
n__isNat_4(24) -> 21
n__isNat_4(24) -> 24
n__isNat_5(24) -> 2
n__isNat_5(24) -> 4
n__isNat_5(24) -> 5
n__isNat_5(24) -> 6
n__isNat_5(24) -> 15
n__isNat_5(24) -> 17
n__isNat_5(24) -> 20
n__isNat_5(24) -> 21
n__isNat_5(24) -> 24
n__plus_0(7,7) -> 2
n__plus_0(7,7) -> 4
n__plus_0(7,7) -> 5
n__plus_0(7,7) -> 9
n__plus_0(7,7) -> 20
n__plus_0(7,7) -> 24
n__plus_0(7,8) -> 2
n__plus_0(7,8) -> 4
n__plus_0(7,8) -> 5
n__plus_0(7,8) -> 9
n__plus_0(7,8) -> 20
n__plus_0(7,8) -> 24
n__plus_0(7,9) -> 2
n__plus_0(7,9) -> 4
n__plus_0(7,9) -> 5
n__plus_0(7,9) -> 9
n__plus_0(7,9) -> 20
n__plus_0(7,9) -> 24
n__plus_0(7,10) -> 2
n__plus_0(7,10) -> 4
n__plus_0(7,10) -> 5
n__plus_0(7,10) -> 9
n__plus_0(7,10) -> 20
n__plus_0(7,10) -> 24
n__plus_0(7,13) -> 2
n__plus_0(7,13) -> 4
n__plus_0(7,13) -> 5
n__plus_0(7,13) -> 9
n__plus_0(7,13) -> 20
n__plus_0(7,13) -> 24
n__plus_0(8,7) -> 2
n__plus_0(8,7) -> 4
n__plus_0(8,7) -> 5
n__plus_0(8,7) -> 9
n__plus_0(8,7) -> 20
n__plus_0(8,7) -> 24
n__plus_0(8,8) -> 2
n__plus_0(8,8) -> 4
n__plus_0(8,8) -> 5
n__plus_0(8,8) -> 9
n__plus_0(8,8) -> 20
n__plus_0(8,8) -> 24
n__plus_0(8,9) -> 2
n__plus_0(8,9) -> 4
n__plus_0(8,9) -> 5
n__plus_0(8,9) -> 9
n__plus_0(8,9) -> 20
n__plus_0(8,9) -> 24
n__plus_0(8,10) -> 2
n__plus_0(8,10) -> 4
n__plus_0(8,10) -> 5
n__plus_0(8,10) -> 9
n__plus_0(8,10) -> 20
n__plus_0(8,10) -> 24
n__plus_0(8,13) -> 2
n__plus_0(8,13) -> 4
n__plus_0(8,13) -> 5
n__plus_0(8,13) -> 9
n__plus_0(8,13) -> 20
n__plus_0(8,13) -> 24
n__plus_0(9,7) -> 2
n__plus_0(9,7) -> 4
n__plus_0(9,7) -> 5
n__plus_0(9,7) -> 9
n__plus_0(9,7) -> 20
n__plus_0(9,7) -> 24
n__plus_0(9,8) -> 2
n__plus_0(9,8) -> 4
n__plus_0(9,8) -> 5
n__plus_0(9,8) -> 9
n__plus_0(9,8) -> 20
n__plus_0(9,8) -> 24
n__plus_0(9,9) -> 2
n__plus_0(9,9) -> 4
n__plus_0(9,9) -> 5
n__plus_0(9,9) -> 9
n__plus_0(9,9) -> 20
n__plus_0(9,9) -> 24
n__plus_0(9,10) -> 2
n__plus_0(9,10) -> 4
n__plus_0(9,10) -> 5
n__plus_0(9,10) -> 9
n__plus_0(9,10) -> 20
n__plus_0(9,10) -> 24
n__plus_0(9,13) -> 2
n__plus_0(9,13) -> 4
n__plus_0(9,13) -> 5
n__plus_0(9,13) -> 9
n__plus_0(9,13) -> 20
n__plus_0(9,13) -> 24
n__plus_0(10,7) -> 2
n__plus_0(10,7) -> 4
n__plus_0(10,7) -> 5
n__plus_0(10,7) -> 9
n__plus_0(10,7) -> 20
n__plus_0(10,7) -> 24
n__plus_0(10,8) -> 2
n__plus_0(10,8) -> 4
n__plus_0(10,8) -> 5
n__plus_0(10,8) -> 9
n__plus_0(10,8) -> 20
n__plus_0(10,8) -> 24
n__plus_0(10,9) -> 2
n__plus_0(10,9) -> 4
n__plus_0(10,9) -> 5
n__plus_0(10,9) -> 9
n__plus_0(10,9) -> 20
n__plus_0(10,9) -> 24
n__plus_0(10,10) -> 2
n__plus_0(10,10) -> 4
n__plus_0(10,10) -> 5
n__plus_0(10,10) -> 9
n__plus_0(10,10) -> 20
n__plus_0(10,10) -> 24
n__plus_0(10,13) -> 2
n__plus_0(10,13) -> 4
n__plus_0(10,13) -> 5
n__plus_0(10,13) -> 9
n__plus_0(10,13) -> 20
n__plus_0(10,13) -> 24
n__plus_0(13,7) -> 2
n__plus_0(13,7) -> 4
n__plus_0(13,7) -> 5
n__plus_0(13,7) -> 9
n__plus_0(13,7) -> 20
n__plus_0(13,7) -> 24
n__plus_0(13,8) -> 2
n__plus_0(13,8) -> 4
n__plus_0(13,8) -> 5
n__plus_0(13,8) -> 9
n__plus_0(13,8) -> 20
n__plus_0(13,8) -> 24
n__plus_0(13,9) -> 2
n__plus_0(13,9) -> 4
n__plus_0(13,9) -> 5
n__plus_0(13,9) -> 9
n__plus_0(13,9) -> 20
n__plus_0(13,9) -> 24
n__plus_0(13,10) -> 2
n__plus_0(13,10) -> 4
n__plus_0(13,10) -> 5
n__plus_0(13,10) -> 9
n__plus_0(13,10) -> 20
n__plus_0(13,10) -> 24
n__plus_0(13,13) -> 2
n__plus_0(13,13) -> 4
n__plus_0(13,13) -> 5
n__plus_0(13,13) -> 9
n__plus_0(13,13) -> 20
n__plus_0(13,13) -> 24
n__plus_1(7,7) -> 11
n__plus_1(7,8) -> 11
n__plus_1(7,9) -> 11
n__plus_1(7,10) -> 11
n__plus_1(7,13) -> 11
n__plus_1(8,7) -> 11
n__plus_1(8,8) -> 11
n__plus_1(8,9) -> 11
n__plus_1(8,10) -> 11
n__plus_1(8,13) -> 11
n__plus_1(9,7) -> 11
n__plus_1(9,8) -> 11
n__plus_1(9,9) -> 11
n__plus_1(9,10) -> 11
n__plus_1(9,13) -> 11
n__plus_1(10,7) -> 11
n__plus_1(10,8) -> 11
n__plus_1(10,9) -> 11
n__plus_1(10,10) -> 11
n__plus_1(10,13) -> 11
n__plus_1(13,7) -> 11
n__plus_1(13,8) -> 11
n__plus_1(13,9) -> 11
n__plus_1(13,10) -> 11
n__plus_1(13,13) -> 11
n__plus_2(2,2) -> 14
n__plus_2(7,7) -> 2
n__plus_2(7,7) -> 4
n__plus_2(7,7) -> 5
n__plus_2(7,7) -> 20
n__plus_2(7,7) -> 24
n__plus_2(7,8) -> 2
n__plus_2(7,8) -> 4
n__plus_2(7,8) -> 5
n__plus_2(7,8) -> 20
n__plus_2(7,8) -> 24
n__plus_2(7,9) -> 2
n__plus_2(7,9) -> 4
n__plus_2(7,9) -> 5
n__plus_2(7,9) -> 20
n__plus_2(7,9) -> 24
n__plus_2(7,10) -> 2
n__plus_2(7,10) -> 4
n__plus_2(7,10) -> 5
n__plus_2(7,10) -> 20
n__plus_2(7,10) -> 24
n__plus_2(7,13) -> 2
n__plus_2(7,13) -> 4
n__plus_2(7,13) -> 5
n__plus_2(7,13) -> 20
n__plus_2(7,13) -> 24
n__plus_2(8,7) -> 2
n__plus_2(8,7) -> 4
n__plus_2(8,7) -> 5
n__plus_2(8,7) -> 20
n__plus_2(8,7) -> 24
n__plus_2(8,8) -> 2
n__plus_2(8,8) -> 4
n__plus_2(8,8) -> 5
n__plus_2(8,8) -> 20
n__plus_2(8,8) -> 24
n__plus_2(8,9) -> 2
n__plus_2(8,9) -> 4
n__plus_2(8,9) -> 5
n__plus_2(8,9) -> 20
n__plus_2(8,9) -> 24
n__plus_2(8,10) -> 2
n__plus_2(8,10) -> 4
n__plus_2(8,10) -> 5
n__plus_2(8,10) -> 20
n__plus_2(8,10) -> 24
n__plus_2(8,13) -> 2
n__plus_2(8,13) -> 4
n__plus_2(8,13) -> 5
n__plus_2(8,13) -> 20
n__plus_2(8,13) -> 24
n__plus_2(9,7) -> 2
n__plus_2(9,7) -> 4
n__plus_2(9,7) -> 5
n__plus_2(9,7) -> 20
n__plus_2(9,7) -> 24
n__plus_2(9,8) -> 2
n__plus_2(9,8) -> 4
n__plus_2(9,8) -> 5
n__plus_2(9,8) -> 20
n__plus_2(9,8) -> 24
n__plus_2(9,9) -> 2
n__plus_2(9,9) -> 4
n__plus_2(9,9) -> 5
n__plus_2(9,9) -> 20
n__plus_2(9,9) -> 24
n__plus_2(9,10) -> 2
n__plus_2(9,10) -> 4
n__plus_2(9,10) -> 5
n__plus_2(9,10) -> 20
n__plus_2(9,10) -> 24
n__plus_2(9,13) -> 2
n__plus_2(9,13) -> 4
n__plus_2(9,13) -> 5
n__plus_2(9,13) -> 20
n__plus_2(9,13) -> 24
n__plus_2(10,7) -> 2
n__plus_2(10,7) -> 4
n__plus_2(10,7) -> 5
n__plus_2(10,7) -> 20
n__plus_2(10,7) -> 24
n__plus_2(10,8) -> 2
n__plus_2(10,8) -> 4
n__plus_2(10,8) -> 5
n__plus_2(10,8) -> 20
n__plus_2(10,8) -> 24
n__plus_2(10,9) -> 2
n__plus_2(10,9) -> 4
n__plus_2(10,9) -> 5
n__plus_2(10,9) -> 20
n__plus_2(10,9) -> 24
n__plus_2(10,10) -> 2
n__plus_2(10,10) -> 4
n__plus_2(10,10) -> 5
n__plus_2(10,10) -> 20
n__plus_2(10,10) -> 24
n__plus_2(10,13) -> 2
n__plus_2(10,13) -> 4
n__plus_2(10,13) -> 5
n__plus_2(10,13) -> 20
n__plus_2(10,13) -> 24
n__plus_2(13,7) -> 2
n__plus_2(13,7) -> 4
n__plus_2(13,7) -> 5
n__plus_2(13,7) -> 20
n__plus_2(13,7) -> 24
n__plus_2(13,8) -> 2
n__plus_2(13,8) -> 4
n__plus_2(13,8) -> 5
n__plus_2(13,8) -> 20
n__plus_2(13,8) -> 24
n__plus_2(13,9) -> 2
n__plus_2(13,9) -> 4
n__plus_2(13,9) -> 5
n__plus_2(13,9) -> 20
n__plus_2(13,9) -> 24
n__plus_2(13,10) -> 2
n__plus_2(13,10) -> 4
n__plus_2(13,10) -> 5
n__plus_2(13,10) -> 20
n__plus_2(13,10) -> 24
n__plus_2(13,13) -> 2
n__plus_2(13,13) -> 4
n__plus_2(13,13) -> 5
n__plus_2(13,13) -> 20
n__plus_2(13,13) -> 24
n__s_0(7) -> 2
n__s_0(7) -> 4
n__s_0(7) -> 5
n__s_0(7) -> 10
n__s_0(7) -> 20
n__s_0(7) -> 24
n__s_0(8) -> 2
n__s_0(8) -> 4
n__s_0(8) -> 5
n__s_0(8) -> 10
n__s_0(8) -> 20
n__s_0(8) -> 24
n__s_0(9) -> 2
n__s_0(9) -> 4
n__s_0(9) -> 5
n__s_0(9) -> 10
n__s_0(9) -> 20
n__s_0(9) -> 24
n__s_0(10) -> 2
n__s_0(10) -> 4
n__s_0(10) -> 5
n__s_0(10) -> 10
n__s_0(10) -> 20
n__s_0(10) -> 24
n__s_0(13) -> 2
n__s_0(13) -> 4
n__s_0(13) -> 5
n__s_0(13) -> 10
n__s_0(13) -> 20
n__s_0(13) -> 24
n__s_1(7) -> 12
n__s_1(8) -> 12
n__s_1(9) -> 12
n__s_1(10) -> 12
n__s_1(13) -> 12
n__s_2(7) -> 2
n__s_2(7) -> 4
n__s_2(7) -> 5
n__s_2(7) -> 20
n__s_2(7) -> 24
n__s_2(8) -> 2
n__s_2(8) -> 4
n__s_2(8) -> 5
n__s_2(8) -> 20
n__s_2(8) -> 24
n__s_2(9) -> 2
n__s_2(9) -> 4
n__s_2(9) -> 5
n__s_2(9) -> 20
n__s_2(9) -> 24
n__s_2(10) -> 2
n__s_2(10) -> 4
n__s_2(10) -> 5
n__s_2(10) -> 20
n__s_2(10) -> 24
n__s_2(13) -> 2
n__s_2(13) -> 4
n__s_2(13) -> 5
n__s_2(13) -> 20
n__s_2(13) -> 24
n__s_2(14) -> 3
plus_0(7,7) -> 11
plus_0(7,8) -> 11
plus_0(7,9) -> 11
plus_0(7,10) -> 11
plus_0(7,13) -> 11
plus_0(8,7) -> 11
plus_0(8,8) -> 11
plus_0(8,9) -> 11
plus_0(8,10) -> 11
plus_0(8,13) -> 11
plus_0(9,7) -> 11
plus_0(9,8) -> 11
plus_0(9,9) -> 11
plus_0(9,10) -> 11
plus_0(9,13) -> 11
plus_0(10,7) -> 11
plus_0(10,8) -> 11
plus_0(10,9) -> 11
plus_0(10,10) -> 11
plus_0(10,13) -> 11
plus_0(13,7) -> 11
plus_0(13,8) -> 11
plus_0(13,9) -> 11
plus_0(13,10) -> 11
plus_0(13,13) -> 11
plus_1(2,2) -> 14
plus_1(7,7) -> 2
plus_1(7,7) -> 4
plus_1(7,7) -> 5
plus_1(7,7) -> 20
plus_1(7,7) -> 24
plus_1(7,8) -> 2
plus_1(7,8) -> 4
plus_1(7,8) -> 5
plus_1(7,8) -> 20
plus_1(7,8) -> 24
plus_1(7,9) -> 2
plus_1(7,9) -> 4
plus_1(7,9) -> 5
plus_1(7,9) -> 20
plus_1(7,9) -> 24
plus_1(7,10) -> 2
plus_1(7,10) -> 4
plus_1(7,10) -> 5
plus_1(7,10) -> 20
plus_1(7,10) -> 24
plus_1(7,13) -> 2
plus_1(7,13) -> 4
plus_1(7,13) -> 5
plus_1(7,13) -> 20
plus_1(7,13) -> 24
plus_1(8,7) -> 2
plus_1(8,7) -> 4
plus_1(8,7) -> 5
plus_1(8,7) -> 20
plus_1(8,7) -> 24
plus_1(8,8) -> 2
plus_1(8,8) -> 4
plus_1(8,8) -> 5
plus_1(8,8) -> 20
plus_1(8,8) -> 24
plus_1(8,9) -> 2
plus_1(8,9) -> 4
plus_1(8,9) -> 5
plus_1(8,9) -> 20
plus_1(8,9) -> 24
plus_1(8,10) -> 2
plus_1(8,10) -> 4
plus_1(8,10) -> 5
plus_1(8,10) -> 20
plus_1(8,10) -> 24
plus_1(8,13) -> 2
plus_1(8,13) -> 4
plus_1(8,13) -> 5
plus_1(8,13) -> 20
plus_1(8,13) -> 24
plus_1(9,7) -> 2
plus_1(9,7) -> 4
plus_1(9,7) -> 5
plus_1(9,7) -> 20
plus_1(9,7) -> 24
plus_1(9,8) -> 2
plus_1(9,8) -> 4
plus_1(9,8) -> 5
plus_1(9,8) -> 20
plus_1(9,8) -> 24
plus_1(9,9) -> 2
plus_1(9,9) -> 4
plus_1(9,9) -> 5
plus_1(9,9) -> 20
plus_1(9,9) -> 24
plus_1(9,10) -> 2
plus_1(9,10) -> 4
plus_1(9,10) -> 5
plus_1(9,10) -> 20
plus_1(9,10) -> 24
plus_1(9,13) -> 2
plus_1(9,13) -> 4
plus_1(9,13) -> 5
plus_1(9,13) -> 20
plus_1(9,13) -> 24
plus_1(10,7) -> 2
plus_1(10,7) -> 4
plus_1(10,7) -> 5
plus_1(10,7) -> 20
plus_1(10,7) -> 24
plus_1(10,8) -> 2
plus_1(10,8) -> 4
plus_1(10,8) -> 5
plus_1(10,8) -> 20
plus_1(10,8) -> 24
plus_1(10,9) -> 2
plus_1(10,9) -> 4
plus_1(10,9) -> 5
plus_1(10,9) -> 20
plus_1(10,9) -> 24
plus_1(10,10) -> 2
plus_1(10,10) -> 4
plus_1(10,10) -> 5
plus_1(10,10) -> 20
plus_1(10,10) -> 24
plus_1(10,13) -> 2
plus_1(10,13) -> 4
plus_1(10,13) -> 5
plus_1(10,13) -> 20
plus_1(10,13) -> 24
plus_1(13,7) -> 2
plus_1(13,7) -> 4
plus_1(13,7) -> 5
plus_1(13,7) -> 20
plus_1(13,7) -> 24
plus_1(13,8) -> 2
plus_1(13,8) -> 4
plus_1(13,8) -> 5
plus_1(13,8) -> 20
plus_1(13,8) -> 24
plus_1(13,9) -> 2
plus_1(13,9) -> 4
plus_1(13,9) -> 5
plus_1(13,9) -> 20
plus_1(13,9) -> 24
plus_1(13,10) -> 2
plus_1(13,10) -> 4
plus_1(13,10) -> 5
plus_1(13,10) -> 20
plus_1(13,10) -> 24
plus_1(13,13) -> 2
plus_1(13,13) -> 4
plus_1(13,13) -> 5
plus_1(13,13) -> 20
plus_1(13,13) -> 24
s_0(7) -> 12
s_0(8) -> 12
s_0(9) -> 12
s_0(10) -> 12
s_0(13) -> 12
s_1(7) -> 2
s_1(7) -> 4
s_1(7) -> 5
s_1(7) -> 20
s_1(7) -> 24
s_1(8) -> 2
s_1(8) -> 4
s_1(8) -> 5
s_1(8) -> 20
s_1(8) -> 24
s_1(9) -> 2
s_1(9) -> 4
s_1(9) -> 5
s_1(9) -> 20
s_1(9) -> 24
s_1(10) -> 2
s_1(10) -> 4
s_1(10) -> 5
s_1(10) -> 20
s_1(10) -> 24
s_1(13) -> 2
s_1(13) -> 4
s_1(13) -> 5
s_1(13) -> 20
s_1(13) -> 24
s_1(14) -> 3
tt_0() -> 2
tt_0() -> 4
tt_0() -> 5
tt_0() -> 13
tt_0() -> 20
tt_0() -> 24
tt_1() -> 2
tt_1() -> 4
tt_1() -> 5
tt_1() -> 6
tt_1() -> 15
tt_1() -> 17
tt_1() -> 20
tt_1() -> 21
tt_1() -> 24
tt_2() -> 2
tt_2() -> 4
tt_2() -> 5
tt_2() -> 6
tt_2() -> 15
tt_2() -> 17
tt_2() -> 20
tt_2() -> 21
tt_2() -> 24
tt_3() -> 2
tt_3() -> 4
tt_3() -> 5
tt_3() -> 6
tt_3() -> 15
tt_3() -> 17
tt_3() -> 20
tt_3() -> 21
tt_3() -> 24
7 -> 2
7 -> 4
7 -> 5
7 -> 19
7 -> 20
7 -> 23
7 -> 24
8 -> 2
8 -> 4
8 -> 5
8 -> 20
8 -> 24
9 -> 2
9 -> 4
9 -> 5
9 -> 20
9 -> 24
10 -> 2
10 -> 4
10 -> 5
10 -> 20
10 -> 24
13 -> 2
13 -> 4
13 -> 5
13 -> 20
13 -> 24
16 -> 2
16 -> 4
16 -> 5
16 -> 6
16 -> 15
16 -> 17
16 -> 20
16 -> 21
16 -> 24
18 -> 2
18 -> 4
18 -> 5
18 -> 6
18 -> 15
18 -> 17
18 -> 20
18 -> 21
18 -> 24
22 -> 2
22 -> 4
22 -> 5
22 -> 6
22 -> 15
22 -> 17
22 -> 20
22 -> 21
22 -> 24
*** 1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),N) -> activate(N)
U21(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__isNat(X)) -> isNat(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(tt(),X) -> activate(X)
isNat(X) -> n__isNat(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2)))
isNat(n__s(V1)) -> isNat(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0}
Obligation:
Innermost
basic terms: {0,U11,U21,activate,and,isNat,plus,s}/{n__0,n__isNat,n__plus,n__s,tt}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).