We consider the following Problem: Strict Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X))) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X))) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} Interpretation of nonconstant growth: ------------------------------------- We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [1] [0 0] [1] __(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [1] [0 0] [1] nil() = [0] [0] U11(x1) = [1 0] x1 + [0] [0 0] [1] tt() = [0] [0] U12(x1) = [1 0] x1 + [0] [0 0] [1] isNePal(x1) = [1 0] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {active(isNePal(__(I, __(P, I)))) -> mark(U11(tt()))} Interpretation of nonconstant growth: ------------------------------------- We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 1] x1 + [1] [0 0] [1] __(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] mark(x1) = [1 0] x1 + [1] [0 0] [1] nil() = [0] [0] U11(x1) = [1 0] x1 + [0] [0 0] [0] tt() = [0] [0] U12(x1) = [1 0] x1 + [0] [0 0] [0] isNePal(x1) = [1 0] x1 + [0] [0 0] [3] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt())} Interpretation of nonconstant growth: ------------------------------------- We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 1] x1 + [1] [0 0] [0] __(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] mark(x1) = [1 0] x1 + [1] [0 0] [0] nil() = [0] [0] U11(x1) = [1 0] x1 + [3] [0 0] [2] tt() = [0] [0] U12(x1) = [1 0] x1 + [1] [0 0] [2] isNePal(x1) = [1 0] x1 + [0] [0 0] [3] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X)} Interpretation of nonconstant growth: ------------------------------------- We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [1] [0 0] [1] __(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] nil() = [0] [0] U11(x1) = [1 0] x1 + [0] [1 0] [3] tt() = [0] [0] U12(x1) = [1 0] x1 + [0] [0 0] [1] isNePal(x1) = [1 0] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(nil()) -> active(nil()) , mark(U11(X)) -> active(U11(mark(X))) , mark(tt()) -> active(tt()) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { mark(nil()) -> active(nil()) , mark(tt()) -> active(tt())} Interpretation of nonconstant growth: ------------------------------------- We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 1] x1 + [0] [0 0] [0] __(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [3] mark(x1) = [1 0] x1 + [1] [0 0] [0] nil() = [0] [0] U11(x1) = [1 0] x1 + [0] [0 0] [2] tt() = [0] [0] U12(x1) = [1 0] x1 + [1] [0 0] [0] isNePal(x1) = [1 0] x1 + [2] [0 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(U11(X)) -> active(U11(mark(X))) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { mark(nil()) -> active(nil()) , mark(tt()) -> active(tt()) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { mark(__(X1, X2)) -> active(__(mark(X1), mark(X2))) , mark(U11(X)) -> active(U11(mark(X))) , mark(U12(X)) -> active(U12(mark(X))) , mark(isNePal(X)) -> active(isNePal(mark(X)))} Weak Trs: { mark(nil()) -> active(nil()) , mark(tt()) -> active(tt()) , active(__(__(X, Y), Z)) -> mark(__(X, __(Y, Z))) , active(__(X, nil())) -> mark(X) , active(__(nil(), X)) -> mark(X) , active(U11(tt())) -> mark(U12(tt())) , active(U12(tt())) -> mark(tt()) , active(isNePal(__(I, __(P, I)))) -> mark(U11(tt())) , __(mark(X1), X2) -> __(X1, X2) , __(X1, mark(X2)) -> __(X1, X2) , __(active(X1), X2) -> __(X1, X2) , __(X1, active(X2)) -> __(X1, X2) , U11(mark(X)) -> U11(X) , U11(active(X)) -> U11(X) , U12(mark(X)) -> U12(X) , U12(active(X)) -> U12(X) , isNePal(mark(X)) -> isNePal(X) , isNePal(active(X)) -> isNePal(X)} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The problem is match-bounded by 0. The enriched problem is compatible with the following automaton: { active_0(2) -> 1 , ___0(2, 2) -> 1 , mark_0(2) -> 1 , nil_0() -> 2 , U11_0(2) -> 1 , tt_0() -> 2 , U12_0(2) -> 1 , isNePal_0(2) -> 1} Hurray, we answered YES(?,O(n^1))