We consider the following Problem:
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), N) -> activate(N)
, U41(tt(), M, N) ->
U42(isNat(activate(N)), activate(M), activate(N))
, U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, plus(N, 0()) -> U31(isNat(N), N)
, plus(N, s(M)) -> U41(isNat(M), M, N)
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
Arguments of following rules are not normal-forms:
{ plus(N, s(M)) -> U41(isNat(M), M, N)
, plus(N, 0()) -> U31(isNat(N), N)}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), N) -> activate(N)
, U41(tt(), M, N) ->
U42(isNat(activate(N)), activate(M), activate(N))
, U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), N) -> activate(N)
, U41(tt(), M, N) ->
U42(isNat(activate(N)), activate(M), activate(N))
, U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We have computed the following dependency pairs
Strict DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), N) -> activate^#(N)
, U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, isNat^#(n__0()) -> c_7()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, s^#(X) -> c_12()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(X) -> c_16()}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), N) -> activate^#(N)
, U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, isNat^#(n__0()) -> c_7()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, s^#(X) -> c_12()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(X) -> c_16()}
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), N) -> activate(N)
, U41(tt(), M, N) ->
U42(isNat(activate(N)), activate(M), activate(N))
, U42(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), N) -> activate^#(N)
, U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, isNat^#(n__0()) -> c_7()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, s^#(X) -> c_12()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(X) -> c_16()}
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
Dependency Pairs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, isNat^#(n__0()) -> c_7()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)}
TRS Component:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
Interpretation of constant growth:
----------------------------------
The following argument positions are usable:
Uargs(U11) = {1, 2}, Uargs(U12) = {1}, Uargs(isNat) = {1},
Uargs(activate) = {}, Uargs(U21) = {1}, Uargs(U31) = {},
Uargs(U41) = {}, Uargs(U42) = {}, Uargs(s) = {},
Uargs(plus) = {1, 2}, Uargs(n__plus) = {}, Uargs(n__s) = {},
Uargs(U11^#) = {1, 2}, Uargs(U12^#) = {1}, Uargs(U21^#) = {1},
Uargs(U31^#) = {}, Uargs(activate^#) = {}, Uargs(U41^#) = {},
Uargs(U42^#) = {1, 2, 3}, Uargs(s^#) = {1}, Uargs(isNat^#) = {},
Uargs(plus^#) = {}
We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [1 0] x1 + [1 2] x2 + [1]
[0 0] [0 0] [1]
tt() = [3]
[0]
U12(x1) = [1 0] x1 + [1]
[0 0] [1]
isNat(x1) = [1 2] x1 + [0]
[0 2] [0]
activate(x1) = [1 0] x1 + [2]
[0 1] [0]
U21(x1) = [1 0] x1 + [1]
[0 0] [0]
U31(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
U41(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
U42(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
s(x1) = [1 0] x1 + [3]
[0 1] [3]
plus(x1, x2) = [1 0] x1 + [1 2] x2 + [3]
[0 1] [0 0] [2]
n__0() = [0]
[3]
n__plus(x1, x2) = [1 0] x1 + [1 2] x2 + [2]
[0 1] [0 0] [2]
n__s(x1) = [1 0] x1 + [2]
[0 1] [3]
0() = [1]
[3]
U11^#(x1, x2) = [1 0] x1 + [1 3] x2 + [0]
[0 0] [0 0] [0]
U12^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_2() = [0]
[0]
U21^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
U31^#(x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
activate^#(x1) = [2 0] x1 + [0]
[0 0] [0]
U41^#(x1, x2, x3) = [0 0] x1 + [2 2] x2 + [2 2] x3 + [0]
[0 0] [0 0] [0 0] [0]
U42^#(x1, x2, x3) = [1 0] x1 + [1 2] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
s^#(x1) = [1 0] x1 + [0]
[0 0] [0]
isNat^#(x1) = [2 2] x1 + [0]
[0 0] [0]
c_7() = [0]
[0]
0^#() = [0]
[0]
c_10() = [0]
[0]
plus^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_11() = [0]
[0]
c_12() = [0]
[0]
c_16() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ U31^#(tt(), N) -> activate^#(N)
, U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, s^#(X) -> c_12()
, activate^#(n__0()) -> 0^#()
, activate^#(X) -> c_16()}
Weak DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, isNat^#(n__0()) -> c_7()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->9:{1} [ YES(O(1),O(1)) ]
|
|->11:{7} [ YES(O(1),O(1)) ]
| |
| `->12:{4} [ YES(O(1),O(1)) ]
|
|->10:{8} [ YES(O(1),O(1)) ]
|
|->13:{15} [ subsumed ]
| |
| `->14:{5} [ YES(O(1),O(1)) ]
|
`->15:{16} [ subsumed ]
|
`->16:{6} [ YES(O(1),O(1)) ]
->7:{2} [ YES(O(1),O(1)) ]
|
`->8:{3} [ YES(O(1),O(1)) ]
|
`->16:{6} [ YES(O(1),O(1)) ]
->3:{12} [ YES(O(1),O(1)) ]
->2:{13} [ subsumed ]
|
`->5:{9} [ subsumed ]
|
`->6:{10} [ YES(O(1),O(1)) ]
->1:{14} [ subsumed ]
|
`->4:{11} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: U31^#(tt(), N) -> activate^#(N)
, 2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, 3: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 4: 0^#() -> c_10()
, 5: plus^#(X1, X2) -> c_11()
, 6: s^#(X) -> c_12()
, 7: activate^#(n__0()) -> 0^#()
, 8: activate^#(X) -> c_16()}
WeakDPs DPs:
{ 9: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, 10: U12^#(tt()) -> c_2()
, 11: U21^#(tt()) -> c_3()
, 12: isNat^#(n__0()) -> c_7()
, 13: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 14: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, 15: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 16: activate^#(n__s(X)) -> s^#(X)}
* Path 9:{1}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {U31^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U31^#(tt(), N) -> activate^#(N)
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U31^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U31^#(tt(), N) -> activate^#(N)}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 9:{1}->11:{7}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {activate^#(n__0()) -> 0^#()}
Weak DPs: {U31^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: activate^#(n__0()) -> 0^#()
2: U31^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__0()) -> 0^#() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: activate^#(n__0()) -> 0^#()}
WeakDPs DPs:
{2: U31^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 1: activate^#(n__0()) -> 0^#()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 9:{1}->11:{7}->12:{4}: YES(O(1),O(1))
------------------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_10()}
Weak DPs:
{ U31^#(tt(), N) -> activate^#(N)
, activate^#(n__0()) -> 0^#()}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: 0^#() -> c_10()
2: U31^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__0()) -> 0^#() :3
3: activate^#(n__0()) -> 0^#() -->_1 0^#() -> c_10() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{3} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: 0^#() -> c_10()}
WeakDPs DPs:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__0()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__0()) -> 0^#()
, 1: 0^#() -> c_10()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 9:{1}->10:{8}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {activate^#(X) -> c_16()}
Weak DPs: {U31^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: activate^#(X) -> c_16()
2: U31^#(tt(), N) -> activate^#(N) -->_1 activate^#(X) -> c_16() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: activate^#(X) -> c_16()}
WeakDPs DPs:
{2: U31^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 1: activate^#(X) -> c_16()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 9:{1}->13:{15}: subsumed
-----------------------------
This path is subsumed by the proof of paths 9:{1}->13:{15}->14:{5}.
* Path 9:{1}->13:{15}->14:{5}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_11()}
Weak DPs:
{ U31^#(tt(), N) -> activate^#(N)
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: plus^#(X1, X2) -> c_11()
2: U31^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__plus(X1, X2)) -> plus^#(X1, X2) :3
3: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
-->_1 plus^#(X1, X2) -> c_11() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{3} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: plus^#(X1, X2) -> c_11()}
WeakDPs DPs:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 1: plus^#(X1, X2) -> c_11()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 9:{1}->15:{16}: subsumed
-----------------------------
This path is subsumed by the proof of paths 9:{1}->15:{16}->16:{6}.
* Path 9:{1}->15:{16}->16:{6}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_12()}
Weak DPs:
{ U31^#(tt(), N) -> activate^#(N)
, activate^#(n__s(X)) -> s^#(X)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: s^#(X) -> c_12()
2: U31^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__s(X)) -> s^#(X) :3
3: activate^#(n__s(X)) -> s^#(X) -->_1 s^#(X) -> c_12() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{3} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: s^#(X) -> c_12()}
WeakDPs DPs:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__s(X)) -> s^#(X)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__s(X)) -> s^#(X)
, 1: s^#(X) -> c_12()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 7:{2}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs:
{U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 7:{2}->8:{3}: YES(O(1),O(1))
---------------------------------
We consider the following Problem:
Strict DPs:
{U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak DPs:
{U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M))) :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
WeakDPs DPs:
{2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, 1: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 7:{2}->8:{3}->16:{6}: YES(O(1),O(1))
-----------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_12()}
Weak DPs:
{ U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: s^#(X) -> c_12()
2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M))) :3
3: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
-->_1 s^#(X) -> c_12() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{3} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: s^#(X) -> c_12()}
WeakDPs DPs:
{ 2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, 3: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U41^#(tt(), M, N) ->
U42^#(isNat(activate(N)), activate(M), activate(N))
, 3: U42^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 1: s^#(X) -> c_12()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 3:{12}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 2:{13}: subsumed
---------------------
This path is subsumed by the proof of paths 2:{13}->5:{9}.
* Path 2:{13}->5:{9}: subsumed
----------------------------
This path is subsumed by the proof of paths 2:{13}->5:{9}->6:{10}.
* Path 2:{13}->5:{9}->6:{10}: YES(O(1),O(1))
------------------------------------------
We consider the following Problem:
Weak DPs:
{ isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
-->_1 U11^#(tt(), V2) -> U12^#(isNat(activate(V2))) :2
2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{2} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
* Path 1:{14}: subsumed
---------------------
This path is subsumed by the proof of paths 1:{14}->4:{11}.
* Path 1:{14}->4:{11}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Weak DPs: {isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
together with the congruence-graph
->1:{1} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{1: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__s(X)) -> s(X)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
No rule is usable.
We consider the following Problem:
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))