We consider the following Problem:
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U61(tt()) -> 0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, plus(N, 0()) -> U41(isNat(N), N)
, plus(N, s(M)) -> U51(isNat(M), M, N)
, x(N, 0()) -> U61(isNat(N))
, x(N, s(M)) -> U71(isNat(M), M, N)
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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)) -> U51(isNat(M), M, N)
, x(N, s(M)) -> U71(isNat(M), M, N)
, plus(N, 0()) -> U41(isNat(N), N)
, x(N, 0()) -> U61(isNat(N))}
All above mentioned rules can be savely removed.
We consider the following Problem:
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U61(tt()) -> 0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U61(tt()) -> 0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, U32^#(tt()) -> c_5()
, U41^#(tt(), N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U61^#(tt()) -> 0^#()
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, isNat^#(n__0()) -> c_12()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, 0^#() -> c_16()
, plus^#(X1, X2) -> c_17()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_19()
, 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)
, activate^#(X) -> c_24()}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, U32^#(tt()) -> c_5()
, U41^#(tt(), N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U61^#(tt()) -> 0^#()
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, isNat^#(n__0()) -> c_12()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, 0^#() -> c_16()
, plus^#(X1, X2) -> c_17()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_19()
, 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)
, activate^#(X) -> c_24()}
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, U41(tt(), N) -> activate(N)
, U51(tt(), M, N) ->
U52(isNat(activate(N)), activate(M), activate(N))
, U52(tt(), M, N) -> s(plus(activate(N), activate(M)))
, U61(tt()) -> 0()
, U71(tt(), M, N) ->
U72(isNat(activate(N)), activate(M), activate(N))
, U72(tt(), M, N) -> plus(x(activate(N), activate(M)), activate(N))
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__s(X)) -> s(X)
, activate(n__x(X1, X2)) -> x(X1, X2)
, activate(X) -> X}
We consider the following Problem:
Strict DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, U32^#(tt()) -> c_5()
, U41^#(tt(), N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U61^#(tt()) -> 0^#()
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, isNat^#(n__0()) -> c_12()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, 0^#() -> c_16()
, plus^#(X1, X2) -> c_17()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_19()
, 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)
, activate^#(X) -> c_24()}
Strict Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, U32^#(tt()) -> c_5()
, isNat^#(n__0()) -> c_12()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
TRS Component:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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) = {1, 2}, Uargs(U12) = {1}, Uargs(isNat) = {1},
Uargs(activate) = {}, Uargs(U21) = {1}, Uargs(U31) = {1, 2},
Uargs(U32) = {1}, Uargs(U41) = {}, Uargs(U51) = {},
Uargs(U52) = {}, Uargs(s) = {}, Uargs(plus) = {1, 2},
Uargs(U61) = {}, Uargs(U71) = {}, Uargs(U72) = {},
Uargs(x) = {1, 2}, Uargs(n__plus) = {}, Uargs(n__s) = {},
Uargs(n__x) = {}, Uargs(U11^#) = {1, 2}, Uargs(U12^#) = {1},
Uargs(U21^#) = {1}, Uargs(U31^#) = {1, 2}, Uargs(U32^#) = {1},
Uargs(U41^#) = {}, Uargs(activate^#) = {}, Uargs(U51^#) = {},
Uargs(U52^#) = {1, 2, 3}, Uargs(s^#) = {1}, Uargs(U61^#) = {},
Uargs(U71^#) = {}, Uargs(U72^#) = {1, 2, 3},
Uargs(plus^#) = {1, 2}, Uargs(isNat^#) = {}, Uargs(x^#) = {}
We have the following constructor-based EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [1 1] x1 + [1 2] x2 + [0]
[0 0] [0 0] [1]
tt() = [3]
[1]
U12(x1) = [1 1] x1 + [0]
[0 0] [1]
isNat(x1) = [1 2] x1 + [0]
[0 0] [1]
activate(x1) = [1 0] x1 + [2]
[0 1] [0]
U21(x1) = [1 0] x1 + [3]
[0 0] [1]
U31(x1, x2) = [1 1] x1 + [1 2] x2 + [0]
[0 0] [0 0] [1]
U32(x1) = [1 0] x1 + [1]
[0 0] [1]
U41(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
U51(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
U52(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
s(x1) = [1 3] x1 + [1]
[0 0] [3]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
[0 1] [0 1] [2]
U61(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [2]
[2]
U71(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
U72(x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [0]
x(x1, x2) = [1 0] x1 + [1 2] x2 + [3]
[0 1] [0 0] [3]
n__0() = [1]
[2]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 1] [2]
n__s(x1) = [1 3] x1 + [0]
[0 0] [3]
n__x(x1, x2) = [1 0] x1 + [1 2] x2 + [2]
[0 1] [0 0] [3]
U11^#(x1, x2) = [1 0] x1 + [1 3] x2 + [0]
[0 0] [0 0] [0]
U12^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_2() = [0]
[0]
U21^#(x1) = [3 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
U31^#(x1, x2) = [1 0] x1 + [1 3] x2 + [0]
[0 0] [0 0] [0]
U32^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_5() = [0]
[0]
U41^#(x1, x2) = [0 0] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
activate^#(x1) = [1 0] x1 + [0]
[0 0] [0]
U51^#(x1, x2, x3) = [0 0] x1 + [2 2] x2 + [2 3] x3 + [0]
[0 0] [0 0] [0 0] [0]
U52^#(x1, x2, x3) = [1 0] x1 + [1 2] x2 + [1 1] x3 + [0]
[0 0] [0 0] [0 0] [0]
s^#(x1) = [1 0] x1 + [0]
[0 0] [0]
U61^#(x1) = [0 0] x1 + [0]
[0 0] [0]
0^#() = [0]
[0]
U71^#(x1, x2, x3) = [0 0] x1 + [2 2] x2 + [3 3] x3 + [0]
[0 0] [0 0] [0 0] [0]
U72^#(x1, x2, x3) = [1 0] x1 + [1 2] x2 + [2 1] x3 + [0]
[0 0] [0 0] [0 0] [0]
plus^#(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
isNat^#(x1) = [3 3] x1 + [0]
[0 0] [0]
c_12() = [0]
[0]
c_16() = [0]
[0]
c_17() = [0]
[0]
c_18() = [0]
[0]
x^#(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
c_19() = [0]
[0]
c_24() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict DPs:
{ U41^#(tt(), N) -> activate^#(N)
, U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, U61^#(tt()) -> 0^#()
, U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, 0^#() -> c_16()
, plus^#(X1, X2) -> c_17()
, s^#(X) -> c_18()
, x^#(X1, X2) -> c_19()
, activate^#(n__s(X)) -> s^#(X)
, activate^#(X) -> c_24()}
Weak DPs:
{ U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, U12^#(tt()) -> c_2()
, U21^#(tt()) -> c_3()
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, U32^#(tt()) -> c_5()
, isNat^#(n__0()) -> c_12()
, isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, isNat^#(n__x(V1, V2)) -> U31^#(isNat(activate(V1)), activate(V2))
, activate^#(n__0()) -> 0^#()
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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
->15:{1} [ YES(O(1),O(1)) ]
|
|->17:{11} [ YES(O(1),O(1)) ]
| |
| `->18:{9} [ YES(O(1),O(1)) ]
|
|->16:{12} [ YES(O(1),O(1)) ]
|
|->19:{22} [ subsumed ]
| |
| `->20:{7} [ YES(O(1),O(1)) ]
|
|->21:{23} [ subsumed ]
| |
| `->22:{8} [ YES(O(1),O(1)) ]
|
`->23:{24} [ subsumed ]
|
`->24:{10} [ YES(O(1),O(1)) ]
->13:{2} [ YES(O(1),O(1)) ]
|
`->14:{3} [ YES(O(1),O(1)) ]
|
`->18:{9} [ YES(O(1),O(1)) ]
->12:{4} [ YES(O(1),O(1)) ]
|
`->20:{7} [ YES(O(1),O(1)) ]
->10:{5} [ YES(O(1),O(1)) ]
|
`->11:{6} [ YES(O(1),O(1)) ]
|
`->22:{8} [ YES(O(1),O(1)) ]
->4:{18} [ YES(O(1),O(1)) ]
->3:{19} [ subsumed ]
|
`->8:{13} [ subsumed ]
|
`->9:{14} [ YES(O(1),O(1)) ]
->2:{20} [ subsumed ]
|
`->7:{15} [ YES(O(1),O(1)) ]
->1:{21} [ subsumed ]
|
`->5:{16} [ subsumed ]
|
`->6:{17} [ YES(O(1),O(1)) ]
Here dependency-pairs are as follows:
Strict DPs:
{ 1: U41^#(tt(), N) -> activate^#(N)
, 2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, 3: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 4: U61^#(tt()) -> 0^#()
, 5: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, 6: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, 7: 0^#() -> c_16()
, 8: plus^#(X1, X2) -> c_17()
, 9: s^#(X) -> c_18()
, 10: x^#(X1, X2) -> c_19()
, 11: activate^#(n__s(X)) -> s^#(X)
, 12: activate^#(X) -> c_24()}
WeakDPs DPs:
{ 13: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
, 14: U12^#(tt()) -> c_2()
, 15: U21^#(tt()) -> c_3()
, 16: U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
, 17: U32^#(tt()) -> c_5()
, 18: isNat^#(n__0()) -> c_12()
, 19: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 20: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
, 21: isNat^#(n__x(V1, V2)) ->
U31^#(isNat(activate(V1)), activate(V2))
, 22: activate^#(n__0()) -> 0^#()
, 23: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 24: activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
* Path 15:{1}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Strict DPs: {U41^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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(), N) -> activate^#(N)
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U41^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U41^#(tt(), N) -> activate^#(N)}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->17:{11}: YES(O(1),O(1))
------------------------------------
We consider the following Problem:
Strict DPs: {activate^#(n__s(X)) -> s^#(X)}
Weak DPs: {U41^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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__s(X)) -> s^#(X)
2: U41^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__s(X)) -> s^#(X) :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: activate^#(n__s(X)) -> s^#(X)}
WeakDPs DPs:
{2: U41^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U41^#(tt(), N) -> activate^#(N)
, 1: activate^#(n__s(X)) -> s^#(X)}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->17:{11}->18:{9}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_18()}
Weak DPs:
{ U41^#(tt(), N) -> activate^#(N)
, activate^#(n__s(X)) -> s^#(X)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_18()
2: U41^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__s(X)) -> s^#(X) :3
3: activate^#(n__s(X)) -> s^#(X) -->_1 s^#(X) -> c_18() :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_18()}
WeakDPs DPs:
{ 2: U41^#(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: U41^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__s(X)) -> s^#(X)
, 1: s^#(X) -> c_18()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->16:{12}: YES(O(1),O(1))
------------------------------------
We consider the following Problem:
Strict DPs: {activate^#(X) -> c_24()}
Weak DPs: {U41^#(tt(), N) -> activate^#(N)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_24()
2: U41^#(tt(), N) -> activate^#(N) -->_1 activate^#(X) -> c_24() :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_24()}
WeakDPs DPs:
{2: U41^#(tt(), N) -> activate^#(N)}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U41^#(tt(), N) -> activate^#(N)
, 1: activate^#(X) -> c_24()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->19:{22}: subsumed
------------------------------
This path is subsumed by the proof of paths 15:{1}->19:{22}->20:{7}.
* Path 15:{1}->19:{22}->20:{7}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_16()}
Weak DPs:
{ U41^#(tt(), N) -> activate^#(N)
, activate^#(n__0()) -> 0^#()}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_16()
2: U41^#(tt(), N) -> activate^#(N)
-->_1 activate^#(n__0()) -> 0^#() :3
3: activate^#(n__0()) -> 0^#() -->_1 0^#() -> c_16() :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_16()}
WeakDPs DPs:
{ 2: U41^#(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: U41^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__0()) -> 0^#()
, 1: 0^#() -> c_16()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->21:{23}: subsumed
------------------------------
This path is subsumed by the proof of paths 15:{1}->21:{23}->22:{8}.
* Path 15:{1}->21:{23}->22:{8}: YES(O(1),O(1))
--------------------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_17()}
Weak DPs:
{ U41^#(tt(), N) -> activate^#(N)
, activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_17()
2: U41^#(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_17() :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_17()}
WeakDPs DPs:
{ 2: U41^#(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: U41^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__plus(X1, X2)) -> plus^#(X1, X2)
, 1: plus^#(X1, X2) -> c_17()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 15:{1}->23:{24}: subsumed
------------------------------
This path is subsumed by the proof of paths 15:{1}->23:{24}->24:{10}.
* Path 15:{1}->23:{24}->24:{10}: YES(O(1),O(1))
---------------------------------------------
We consider the following Problem:
Strict DPs: {x^#(X1, X2) -> c_19()}
Weak DPs:
{ U41^#(tt(), N) -> activate^#(N)
, activate^#(n__x(X1, X2)) -> x^#(X1, X2)}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_19()
2: U41^#(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_19() :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_19()}
WeakDPs DPs:
{ 2: U41^#(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: U41^#(tt(), N) -> activate^#(N)
, 3: activate^#(n__x(X1, X2)) -> x^#(X1, X2)
, 1: x^#(X1, X2) -> c_19()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 13:{2}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Strict DPs:
{U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 13:{2}->14:{3}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict DPs:
{U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak DPs:
{U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M))) :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
WeakDPs DPs:
{2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, 1: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 13:{2}->14:{3}->18:{9}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {s^#(X) -> c_18()}
Weak DPs:
{ U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_18()
2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M))) :3
3: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
-->_1 s^#(X) -> c_18() :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_18()}
WeakDPs DPs:
{ 2: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, 3: U52^#(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: U51^#(tt(), M, N) ->
U52^#(isNat(activate(N)), activate(M), activate(N))
, 3: U52^#(tt(), M, N) -> s^#(plus(activate(N), activate(M)))
, 1: s^#(X) -> c_18()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 12:{4}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Strict DPs: {U61^#(tt()) -> 0^#()}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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: U61^#(tt()) -> 0^#()
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U61^#(tt()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U61^#(tt()) -> 0^#()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 12:{4}->20:{7}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict DPs: {0^#() -> c_16()}
Weak DPs: {U61^#(tt()) -> 0^#()}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_16()
2: U61^#(tt()) -> 0^#() -->_1 0^#() -> c_16() :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: 0^#() -> c_16()}
WeakDPs DPs:
{2: U61^#(tt()) -> 0^#()}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U61^#(tt()) -> 0^#()
, 1: 0^#() -> c_16()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 10:{5}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Strict DPs:
{U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
together with the congruence-graph
->1:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 10:{5}->11:{6}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Strict DPs:
{U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
Weak DPs:
{U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
2: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N)) :1
together with the congruence-graph
->1:{2} Weak SCC
|
`->2:{1} Noncyclic, trivial, SCC
Here dependency-pairs are as follows:
Strict DPs:
{1: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
WeakDPs DPs:
{2: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 2: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, 1: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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 10:{5}->11:{6}->22:{8}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Strict DPs: {plus^#(X1, X2) -> c_17()}
Weak DPs:
{ U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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_17()
2: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
-->_1 U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N)) :3
3: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
-->_1 plus^#(X1, X2) -> c_17() :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_17()}
WeakDPs DPs:
{ 2: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, 3: U72^#(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: U71^#(tt(), M, N) ->
U72^#(isNat(activate(N)), activate(M), activate(N))
, 3: U72^#(tt(), M, N) ->
plus^#(x(activate(N), activate(M)), activate(N))
, 1: plus^#(X1, X2) -> c_17()}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:{18}: YES(O(1),O(1))
---------------------------
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:{19}: subsumed
---------------------
This path is subsumed by the proof of paths 3:{19}->8:{13}.
* Path 3:{19}->8:{13}: subsumed
-----------------------------
This path is subsumed by the proof of paths 3:{19}->8:{13}->9:{14}.
* Path 3:{19}->8:{13}->9:{14}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Weak DPs:
{ isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
-->_1 U11^#(tt(), V2) -> U12^#(isNat(activate(V2))) :2
2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{2} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: isNat^#(n__plus(V1, V2)) ->
U11^#(isNat(activate(V1)), activate(V2))
, 2: U11^#(tt(), V2) -> U12^#(isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:{20}: subsumed
---------------------
This path is subsumed by the proof of paths 2:{20}->7:{15}.
* Path 2:{20}->7:{15}: YES(O(1),O(1))
-----------------------------------
We consider the following Problem:
Weak DPs: {isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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^#(n__s(V1)) -> U21^#(isNat(activate(V1)))
together with the congruence-graph
->1:{1} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{1: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{1: isNat^#(n__s(V1)) -> U21^#(isNat(activate(V1)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:{21}: subsumed
---------------------
This path is subsumed by the proof of paths 1:{21}->5:{16}.
* Path 1:{21}->5:{16}: subsumed
-----------------------------
This path is subsumed by the proof of paths 1:{21}->5:{16}->6:{17}.
* Path 1:{21}->5:{16}->6:{17}: YES(O(1),O(1))
-------------------------------------------
We consider the following Problem:
Weak DPs:
{ isNat^#(n__x(V1, V2)) ->
U31^#(isNat(activate(V1)), activate(V2))
, U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))}
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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^#(n__x(V1, V2)) ->
U31^#(isNat(activate(V1)), activate(V2))
-->_1 U31^#(tt(), V2) -> U32^#(isNat(activate(V2))) :2
2: U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))
together with the congruence-graph
->1:{1} Weak SCC
|
`->2:{2} Weak SCC
Here dependency-pairs are as follows:
WeakDPs DPs:
{ 1: isNat^#(n__x(V1, V2)) ->
U31^#(isNat(activate(V1)), activate(V2))
, 2: U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))}
The following rules are either leafs or part of trailing weak paths, and thus they can be removed:
{ 1: isNat^#(n__x(V1, V2)) ->
U31^#(isNat(activate(V1)), activate(V2))
, 2: U31^#(tt(), V2) -> U32^#(isNat(activate(V2)))}
We consider the following Problem:
Weak Trs:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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:
{ U11(tt(), V2) -> U12(isNat(activate(V2)))
, U12(tt()) -> tt()
, U21(tt()) -> tt()
, U31(tt(), V2) -> U32(isNat(activate(V2)))
, U32(tt()) -> tt()
, isNat(n__0()) -> tt()
, isNat(n__plus(V1, V2)) -> U11(isNat(activate(V1)), activate(V2))
, isNat(n__s(V1)) -> U21(isNat(activate(V1)))
, isNat(n__x(V1, V2)) -> U31(isNat(activate(V1)), activate(V2))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, 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__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))