We consider the following Problem:
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, 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))
, plus(N, 0()) -> U11(isNat(N), N)
, plus(N, s(M)) -> U21(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)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
Arguments of following rules are not normal-forms:
{ plus(N, s(M)) -> U21(and(isNat(M), n__isNat(N)), M, N)
, plus(N, 0()) -> U11(isNat(N), 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)))
, 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))
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[1 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [3]
[0 0] [1]
U21(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
s(x1) = [1 0] x1 + [1]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
isNat(x1) = [1 0] x1 + [1]
[1 0] [1]
n__0() = [0]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [0]
[0 0] [0]
n__s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ U11(tt(), N) -> activate(N)
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, and(tt(), X) -> activate(X)
, isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
Weak Trs:
{ isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
U21(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
s(x1) = [1 0] x1 + [1]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
isNat(x1) = [1 0] x1 + [1]
[0 0] [1]
n__0() = [0]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [0]
[0 0] [0]
n__s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
Weak Trs:
{ U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {isNat(n__s(V1)) -> isNat(activate(V1))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 0] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 0] [0]
U21(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
s(x1) = [1 0] x1 + [1]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
isNat(x1) = [1 0] x1 + [1]
[0 0] [1]
n__0() = [0]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [0]
[0 0] [1]
n__s(x1) = [1 0] x1 + [1]
[0 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
Weak Trs:
{ isNat(n__s(V1)) -> isNat(activate(V1))
, U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{U21(tt(), M, N) -> s(plus(activate(N), activate(M)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
tt() = [0]
[1]
activate(x1) = [1 0] x1 + [0]
[0 0] [1]
U21(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [1]
[0 1] [0 0] [0 0] [0]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 3] x1 + [1 1] x2 + [1]
[0 0] [0 0] [1]
isNat(x1) = [1 0] x1 + [0]
[0 0] [3]
n__0() = [0]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [0]
[0 0] [3]
n__s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__isNat(X)) -> isNat(X)
, activate(n__s(X)) -> s(activate(X))
, activate(X) -> X}
Weak Trs:
{ U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ activate(n__isNat(X)) -> isNat(X)
, activate(X) -> X}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [0 0] x1 + [1 0] x2 + [3]
[0 0] [0 1] [1]
tt() = [3]
[1]
activate(x1) = [1 0] x1 + [2]
[0 1] [1]
U21(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [3]
[0 0] [0 0] [0 0] [1]
s(x1) = [1 0] x1 + [2]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [0]
isNat(x1) = [1 0] x1 + [1]
[0 0] [1]
n__0() = [2]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [1]
[0 0] [0]
n__s(x1) = [1 0] x1 + [2]
[0 0] [0]
0() = [2]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))}
Weak Trs:
{ activate(n__isNat(X)) -> isNat(X)
, activate(X) -> X
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 1] [0 1] [1]
tt() = [0]
[0]
activate(x1) = [1 0] x1 + [0]
[0 1] [1]
U21(x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 0] x3 + [3]
[0 0] [0 0] [0 0] [1]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
plus(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 1] [0 0] [0]
and(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
isNat(x1) = [1 0] x1 + [0]
[0 0] [1]
n__0() = [0]
[0]
n__plus(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
[0 0] [0 0] [0]
n__isNat(x1) = [1 0] x1 + [0]
[0 0] [0]
n__s(x1) = [1 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))}
Weak Trs:
{ isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, activate(n__isNat(X)) -> isNat(X)
, activate(X) -> X
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2))
, activate(n__s(X)) -> s(activate(X))}
Weak Trs:
{ isNat(n__plus(V1, V2)) ->
and(isNat(activate(V1)), n__isNat(activate(V2)))
, activate(n__isNat(X)) -> isNat(X)
, activate(X) -> X
, U21(tt(), M, N) -> s(plus(activate(N), activate(M)))
, isNat(n__s(V1)) -> isNat(activate(V1))
, U11(tt(), N) -> activate(N)
, and(tt(), X) -> activate(X)
, isNat(n__0()) -> tt()
, 0() -> n__0()
, plus(X1, X2) -> n__plus(X1, X2)
, isNat(X) -> n__isNat(X)
, s(X) -> n__s(X)
, activate(n__0()) -> 0()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The following argument positions are usable:
Uargs(U11) = {}, Uargs(activate) = {}, Uargs(U21) = {},
Uargs(s) = {1}, Uargs(plus) = {1, 2}, Uargs(and) = {1, 2},
Uargs(isNat) = {1}, Uargs(n__plus) = {}, Uargs(n__isNat) = {1},
Uargs(n__s) = {}
We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
U11(x1, x2) = [0 0 0] x1 + [2 2 0] x2 + [1]
[0 0 0] [0 2 0] [1]
[0 0 0] [0 0 1] [1]
tt() = [2]
[0]
[1]
activate(x1) = [1 2 0] x1 + [0]
[0 1 0] [0]
[0 0 1] [0]
U21(x1, x2, x3) = [0 0 0] x1 + [2 2 0] x2 + [2 2 0] x3 + [1]
[0 0 2] [0 1 0] [0 2 0] [2]
[1 0 0] [0 2 1] [0 2 2] [2]
s(x1) = [1 0 0] x1 + [0]
[0 1 0] [2]
[0 1 1] [0]
plus(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 1 1] [0 1 1] [1]
and(x1, x2) = [1 0 0] x1 + [1 2 0] x2 + [0]
[0 0 0] [0 1 0] [0]
[0 0 0] [0 0 1] [0]
isNat(x1) = [1 0 2] x1 + [2]
[0 0 0] [1]
[0 0 0] [1]
n__0() = [2]
[1]
[0]
n__plus(x1, x2) = [1 0 0] x1 + [1 0 0] x2 + [0]
[0 1 0] [0 1 0] [2]
[0 1 1] [0 1 1] [1]
n__isNat(x1) = [1 0 2] x1 + [0]
[0 0 0] [1]
[0 0 0] [1]
n__s(x1) = [1 0 0] x1 + [0]
[0 1 0] [2]
[0 1 1] [0]
0() = [2]
[1]
[0]
Hurray, we answered YES(?,O(n^2))