We consider the following Problem:
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, plus(N, 0()) -> U11(isNat(N), N)
, plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N)
, x(N, 0()) -> U31(isNat(N))
, x(N, s(M)) -> U41(and(isNat(M), n__isNat(N)), M, N)
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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)) -> U21(and(isNat(M), n__isNat(N)), M, N)
, x(N, s(M)) -> U41(and(isNat(M), n__isNat(N)), M, N)
, plus(N, 0()) -> U11(isNat(N), N)
, x(N, 0()) -> U31(isNat(N))}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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(), N) -> activate^#(N)
, U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U31^#(tt()) -> 0^#()
, U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__0()) -> c_6()
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, isNat^#(X) -> c_12()
, s^#(X) -> c_13()
, x^#(X1, X2) -> c_14()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__isNat(X)) -> isNat^#(X)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, activate^#(X) -> c_20()}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), N) -> activate^#(N)
, U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U31^#(tt()) -> 0^#()
, U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__0()) -> c_6()
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, isNat^#(X) -> c_12()
, s^#(X) -> c_13()
, x^#(X1, X2) -> c_14()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__isNat(X)) -> isNat^#(X)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, activate^#(X) -> c_20()}
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), N) -> activate^#(N)
, U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U31^#(tt()) -> 0^#()
, U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__0()) -> c_6()
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, isNat^#(X) -> c_12()
, s^#(X) -> c_13()
, x^#(X1, X2) -> c_14()
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__isNat(X)) -> isNat^#(X)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, activate^#(X) -> c_20()}
Strict Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:
{ and^#(tt(), X) -> activate^#(X)
, isNat^#(n__0()) -> c_6()
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
TRS Component:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
Interpretation of constant growth:
----------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {}, Uargs(plus) = {1, 2}, Uargs(U31) = {},
Uargs(U41) = {}, Uargs(x) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}, Uargs(n__x) = {}, Uargs(U11^#) = {},
Uargs(activate^#) = {}, Uargs(U21^#) = {}, Uargs(s^#) = {1},
Uargs(U31^#) = {}, Uargs(U41^#) = {}, Uargs(plus^#) = {1, 2},
Uargs(and^#) = {1, 2}, Uargs(isNat^#) = {1}, Uargs(x^#) = {}
We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
tt() = [3]
[0]
activate(x1) = [1 0] x1 + [2]
[0 1] [0]
U21(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] [2]
plus(x1, x2) = [1 3] x1 + [1 2] x2 + [2]
[0 0] [0 0] [2]
U31(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [2]
[2]
U41(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
x(x1, x2) = [1 2] x1 + [1 0] x2 + [3]
[0 0] [0 1] [2]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 2] [0]
isNat(x1) = [1 2] x1 + [1]
[0 0] [0]
n__0() = [1]
[2]
n__plus(x1, x2) = [1 3] x1 + [1 2] x2 + [1]
[0 0] [0 0] [2]
n__isNat(x1) = [1 2] x1 + [0]
[0 0] [0]
n__s(x1) = [1 0] x1 + [2]
[0 1] [2]
n__x(x1, x2) = [1 2] x1 + [1 0] x2 + [2]
[0 0] [0 1] [2]
U11^#(x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
activate^#(x1) = [1 0] x1 + [0]
[0 0] [0]
U21^#(x1, x2, x3) = [0 0] x1 + [2 2] x2 + [2 3] x3 + [0]
[0 0] [0 0] [0 0] [0]
s^#(x1) = [1 0] x1 + [0]
[0 0] [0]
U31^#(x1) = [0 0] x1 + [0]
[0 0] [0]
0^#() = [0]
[0]
U41^#(x1, x2, x3) = [0 0] x1 + [2 0] x2 + [2 2] x3 + [0]
[0 0] [0 0] [0 0] [0]
plus^#(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
and^#(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
isNat^#(x1) = [1 2] x1 + [0]
[0 0] [0]
c_6() = [0]
[0]
c_10() = [0]
[0]
c_11() = [0]
[0]
c_12() = [0]
[0]
c_13() = [0]
[0]
x^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_14() = [0]
[0]
c_20() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), N) -> activate^#(N)
, U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U31^#(tt()) -> 0^#()
, U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 0^#() -> c_10()
, plus^#(X1, X2) -> c_11()
, isNat^#(X) -> c_12()
, s^#(X) -> c_13()
, x^#(X1, X2) -> c_14()
, activate^#(n__isNat(X)) -> isNat^#(X)
, activate^#(X) -> c_20()}
Weak DPs:
{ and^#(tt(), X) -> activate^#(X)
, isNat^#(n__0()) -> c_6()
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__s(X)) -> s^#(X)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We use following congruence DG for path analysis
->4:{1} [ YES(O(1),O(1)) ]
|
|->5:{11,13,16,15,5} [ YES(O(1),O(1)) ]
| |
| |->6:{8} [ YES(O(1),O(1)) ]
| |
| |->8:{12} [ YES(O(1),O(1)) ]
| |
| |->7:{14} [ YES(O(1),O(1)) ]
| |
| |->9:{17} [ subsumed ]
| | |
| | `->10:{6} [ YES(O(1),O(1)) ]
| |
| |->11:{18} [ subsumed ]
| | |
| | `->12:{7} [ YES(O(1),O(1)) ]
| |
| |->13:{19} [ subsumed ]
| | |
| | `->14:{9} [ YES(O(1),O(1)) ]
| |
| `->15:{20} [ subsumed ]
| |
| `->16:{10} [ YES(O(1),O(1)) ]
|
|->8:{12} [ YES(O(1),O(1)) ]
|
|->9:{17} [ subsumed ]
| |
| `->10:{6} [ YES(O(1),O(1)) ]
|
|->11:{18} [ subsumed ]
| |
| `->12:{7} [ YES(O(1),O(1)) ]
|
|->13:{19} [ subsumed ]
| |
| `->14:{9} [ YES(O(1),O(1)) ]
|
`->15:{20} [ subsumed ]
|
`->16:{10} [ YES(O(1),O(1)) ]
->3:{2} [ YES(O(1),O(1)) ]
|
`->14:{9} [ YES(O(1),O(1)) ]
->2:{3} [ YES(O(1),O(1)) ]
|
`->10:{6} [ YES(O(1),O(1)) ]
->1:{4} [ YES(O(1),O(1)) ]
|
`->12:{7} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: U11^#(tt(), N) -> activate^#(N)
, 2: U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 3: U31^#(tt()) -> 0^#()
, 4: U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, 5: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 6: 0^#() -> c_10()
, 7: plus^#(X1, X2) -> c_11()
, 8: isNat^#(X) -> c_12()
, 9: s^#(X) -> c_13()
, 10: x^#(X1, X2) -> c_14()
, 11: activate^#(n__isNat(X)) -> isNat^#(X)
, 12: activate^#(X) -> c_20()}
WeakDPs DPs:
{ 13: and^#(tt(), X) -> activate^#(X)
, 14: isNat^#(n__0()) -> c_6()
, 15: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 16: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 17: activate^#(n__0()) -> 0^#()
, 18: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 19: activate^#(n__s(X)) -> s^#(X)
, 20: activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
* Path 4:{1}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {U11^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U11^#(tt(), N) -> activate^#(N)
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U11^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U11^#(tt(), N) -> activate^#(N)}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}: YES(O(1),O(1))
---------------------------------------------
We consider the following Problem:
Strict DPs:
{ activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak DPs: {U11^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :2
2: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
3: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :1
together with the congruence-graph
->1:{3} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
|
`->3:{2} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{ 1: activate^#(n__isNat(X)) -> isNat^#(X)
, 2: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
WeakDPs DPs:
{3: U11^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 3: U11^#(tt(), N) -> activate^#(N)
, 1: activate^#(n__isNat(X)) -> isNat^#(X)
, 2: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->6:{8}: YES(O(1),O(1))
----------------------------------------------------
We consider the following Problem:
Strict DPs: {isNat^#(X) -> c_12()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: isNat^#(X) -> c_12()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
-->_1 isNat^#(X) -> c_12() :1
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
-->_1 isNat^#(X) -> c_12() :1
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{6,3,7,5,4} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: isNat^#(X) -> c_12()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 1: isNat^#(X) -> c_12()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->6:{8}: YES(O(1),O(1))
----------------------------------------------------
We consider the following Problem:
Strict DPs: {isNat^#(X) -> c_12()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: isNat^#(X) -> c_12()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
-->_1 isNat^#(X) -> c_12() :1
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
-->_1 isNat^#(X) -> c_12() :1
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{6,3,7,5,4} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: isNat^#(X) -> c_12()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 1: isNat^#(X) -> c_12()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->8:{12}: YES(O(1),O(1))
-----------------------------------------------------
We consider the following Problem:
Strict DPs: {activate^#(X) -> c_20()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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_20()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
-->_1 activate^#(X) -> c_20() :1
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
-->_1 activate^#(X) -> c_20() :1
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
together with the congruence-graph
->1:{2} Weak SCC
|
|->3:{1} Noncyclic, trivial, SCC
|
`->2:{6,3,7,5,4} Weak SCC
|
`->3:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: activate^#(X) -> c_20()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 1: activate^#(X) -> c_20()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->7:{14}: YES(O(1),O(1))
-----------------------------------------------------
We consider the following Problem:
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :5
2: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :5
3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :2
4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :6
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :4
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :3
5: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :6
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :4
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :3
6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :2
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{5,2,6,4,3} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: U11^#(tt(), N) -> activate^#(N)
, 2: and^#(tt(), X) -> activate^#(X)
, 3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 5: activate^#(n__isNat(X)) -> isNat^#(X)
, 6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: U11^#(tt(), N) -> activate^#(N)
, 5: activate^#(n__isNat(X)) -> isNat^#(X)
, 2: and^#(tt(), X) -> activate^#(X)
, 6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->7:{14}: YES(O(1),O(1))
-----------------------------------------------------
We consider the following Problem:
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :5
2: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :5
3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :2
4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :6
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :4
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :3
5: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :6
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :4
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :3
6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :2
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{5,2,6,4,3} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: U11^#(tt(), N) -> activate^#(N)
, 2: and^#(tt(), X) -> activate^#(X)
, 3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 5: activate^#(n__isNat(X)) -> isNat^#(X)
, 6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: U11^#(tt(), N) -> activate^#(N)
, 5: activate^#(n__isNat(X)) -> isNat^#(X)
, 2: and^#(tt(), X) -> activate^#(X)
, 6: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 4: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 3: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->9:{17}: subsumed
-----------------------------------------------
This path is subsumed by the proof of paths 4:{1}->5:{11,13,16,15,5}->9:{17}->10:{6}.
* Path 4:{1}->5:{11,13,16,15,5}->9:{17}->10:{6}: YES(O(1),O(1))
-------------------------------------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_10()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__0()) -> 0^#()}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__0()) -> 0^#() :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__0()) -> 0^#() :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
8: activate^#(n__0()) -> 0^#() -->_1 0^#() -> c_10() :1
together with the congruence-graph
->1:{2} Weak SCC
|
|->2:{6,3,7,5,4} Weak SCC
| |
| `->3:{8} Weak SCC
| |
| `->4:{1} Noncyclic, trivial, SCC
|
`->3:{8} Weak SCC
|
`->4:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: 0^#() -> c_10()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__0()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__0()) -> 0^#()
, 1: 0^#() -> c_10()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->11:{18}: subsumed
------------------------------------------------
This path is subsumed by the proof of paths 4:{1}->5:{11,13,16,15,5}->11:{18}->12:{7}.
* Path 4:{1}->5:{11,13,16,15,5}->11:{18}->12:{7}: YES(O(1),O(1))
--------------------------------------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_11()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__plus(X1, X2)) -> plus^#(X1, X2) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__plus(X1, X2)) -> plus^#(X1, X2) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
8: 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:{6,3,7,5,4} Weak SCC
| |
| `->3:{8} Weak SCC
| |
| `->4:{1} Noncyclic, trivial, SCC
|
`->3:{8} Weak SCC
|
`->4:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: plus^#(X1, X2) -> c_11()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: 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: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 1: plus^#(X1, X2) -> c_11()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->13:{19}: subsumed
------------------------------------------------
This path is subsumed by the proof of paths 4:{1}->5:{11,13,16,15,5}->13:{19}->14:{9}.
* Path 4:{1}->5:{11,13,16,15,5}->13:{19}->14:{9}: YES(O(1),O(1))
--------------------------------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_13()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__s(X)) -> s^#(X)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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_13()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__s(X)) -> s^#(X) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__s(X)) -> s^#(X) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
8: activate^#(n__s(X)) -> s^#(X) -->_1 s^#(X) -> c_13() :1
together with the congruence-graph
->1:{2} Weak SCC
|
|->2:{6,3,7,5,4} Weak SCC
| |
| `->3:{8} Weak SCC
| |
| `->4:{1} Noncyclic, trivial, SCC
|
`->3:{8} Weak SCC
|
`->4:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: s^#(X) -> c_13()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: 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: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__s(X)) -> s^#(X)
, 1: s^#(X) -> c_13()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->5:{11,13,16,15,5}->15:{20}: subsumed
------------------------------------------------
This path is subsumed by the proof of paths 4:{1}->5:{11,13,16,15,5}->15:{20}->16:{10}.
* Path 4:{1}->5:{11,13,16,15,5}->15:{20}->16:{10}: YES(O(1),O(1))
---------------------------------------------------------------
We consider the following Problem:
Strict DPs: {x^#(X1, X2) -> c_14()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, and^#(tt(), X) -> activate^#(X)
, isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, activate^#(n__isNat(X)) -> isNat^#(X)
, isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: x^#(X1, X2) -> c_14()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__x(X1, X2)) -> x^#(X1, X2) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
3: and^#(tt(), X) -> activate^#(X)
-->_1 activate^#(n__x(X1, X2)) -> x^#(X1, X2) :8
-->_1 activate^#(n__isNat(X)) -> isNat^#(X) :6
4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
6: activate^#(n__isNat(X)) -> isNat^#(X)
-->_1 isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :7
-->_1 isNat^#(n__s(V1)) -> isNat^#(activate(V1)) :5
-->_1 isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2))) :4
7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
-->_1 and^#(tt(), X) -> activate^#(X) :3
8: activate^#(n__x(X1, X2)) -> x^#(X1, X2)
-->_1 x^#(X1, X2) -> c_14() :1
together with the congruence-graph
->1:{2} Weak SCC
|
|->2:{6,3,7,5,4} Weak SCC
| |
| `->3:{8} Weak SCC
| |
| `->4:{1} Noncyclic, trivial, SCC
|
`->3:{8} Weak SCC
|
`->4:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: x^#(X1, X2) -> c_14()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: and^#(tt(), X) -> activate^#(X)
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 6: activate^#(n__isNat(X)) -> isNat^#(X)
, 3: and^#(tt(), X) -> activate^#(X)
, 7: isNat^#(n__plus(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 5: isNat^#(n__s(V1)) -> isNat^#(activate(V1))
, 4: isNat^#(n__x(V1, V2)) ->
and^#(isNat(activate(V1)), n__isNat(activate(V2)))
, 8: activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, 1: x^#(X1, X2) -> c_14()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->8:{12}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {activate^#(X) -> c_20()}
Weak DPs: {U11^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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_20()
2: U11^#(tt(), N) -> activate^#(N) -->_1 activate^#(X) -> c_20() :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_20()}
WeakDPs DPs:
{2: U11^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 1: activate^#(X) -> c_20()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->9:{17}: subsumed
----------------------------
This path is subsumed by the proof of paths 4:{1}->9:{17}->10:{6}.
* Path 4:{1}->9:{17}->10:{6}: YES(O(1),O(1))
------------------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_10()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, activate^#(n__0()) -> 0^#()}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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: U11^#(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: U11^#(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: U11^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__0()) -> 0^#()
, 1: 0^#() -> c_10()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->11:{18}: subsumed
-----------------------------
This path is subsumed by the proof of paths 4:{1}->11:{18}->12:{7}.
* Path 4:{1}->11:{18}->12:{7}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_11()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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: U11^#(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: U11^#(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: U11^#(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:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->13:{19}: subsumed
-----------------------------
This path is subsumed by the proof of paths 4:{1}->13:{19}->14:{9}.
* Path 4:{1}->13:{19}->14:{9}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_13()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, activate^#(n__s(X)) -> s^#(X)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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_13()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__s(X)) -> s^#(X) :3
3: activate^#(n__s(X)) -> s^#(X) -->_1 s^#(X) -> c_13() :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_13()}
WeakDPs DPs:
{ 2: U11^#(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: U11^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__s(X)) -> s^#(X)
, 1: s^#(X) -> c_13()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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 4:{1}->15:{20}: subsumed
-----------------------------
This path is subsumed by the proof of paths 4:{1}->15:{20}->16:{10}.
* Path 4:{1}->15:{20}->16:{10}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Strict DPs: {x^#(X1, X2) -> c_14()}
Weak DPs:
{ U11^#(tt(), N) -> activate^#(N)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: x^#(X1, X2) -> c_14()
2: U11^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__x(X1, X2)) -> x^#(X1, X2) :3
3: activate^#(n__x(X1, X2)) -> x^#(X1, X2)
-->_1 x^#(X1, X2) -> c_14() :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: x^#(X1, X2) -> c_14()}
WeakDPs DPs:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U11^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, 1: x^#(X1, X2) -> c_14()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{2}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs:
{U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U21^#(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:
{1: U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{2}->14:{9}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_13()}
Weak DPs:
{U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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_13()
2: U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
-->_1 s^#(X) -> c_13() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: s^#(X) -> c_13()}
WeakDPs DPs:
{2: U21^#(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: U21^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 1: s^#(X) -> c_13()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{3}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs: {U31^#(tt()) -> 0^#()}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the the dependency-graph
1: U31^#(tt()) -> 0^#()
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U31^#(tt()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U31^#(tt()) -> 0^#()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{3}->10:{6}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_10()}
Weak DPs: {U31^#(tt()) -> 0^#()}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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()) -> 0^#() -->_1 0^#() -> c_10() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: 0^#() -> c_10()}
WeakDPs DPs:
{2: U31^#(tt()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U31^#(tt()) -> 0^#()
, 1: 0^#() -> c_10()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{4}: YES(O(1),O(1))
--------------------------
We consider the following Problem:
Strict DPs:
{U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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) ->
plus^#(x(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) ->
plus^#(x(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) ->
plus^#(x(activate(N), activate(M)), activate(N))}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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:{4}->12:{7}: YES(O(1),O(1))
----------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_11()}
Weak DPs:
{U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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: U41^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
-->_1 plus^#(X1, X2) -> c_11() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: plus^#(X1, X2) -> c_11()}
WeakDPs DPs:
{2: U41^#(tt(), M, N) ->
plus^#(x(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) ->
plus^#(x(activate(N), activate(M)), activate(N))
, 1: plus^#(X1, X2) -> c_11()}
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ and(tt(), X) -> activate(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))
, isNat(n__x(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, x(X1, X2) -> n__x(X1, X2)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(X1, X2)
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, 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))