We consider the following Problem: Strict Trs: { active(f(X, X)) -> mark(f(a(), b())) , active(b()) -> mark(a()) , active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { active(f(X, X)) -> mark(f(a(), b())) , active(b()) -> mark(a()) , active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , f(ok(X1), ok(X2)) -> ok(f(X1, X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {f(ok(X1), ok(X2)) -> ok(f(X1, X2))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1, 2}, Uargs(mark) = {1}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(top) = {1} 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] f(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [1] [0 0] [1] a() = [0] [0] b() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [1] ok(x1) = [1 0] x1 + [1] [0 0] [1] top(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(f(X, X)) -> mark(f(a(), b())) , active(b()) -> mark(a()) , active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X))} Weak Trs: {f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { active(b()) -> mark(a()) , top(ok(X)) -> top(active(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1, 2}, Uargs(mark) = {1}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(top) = {1} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: active(x1) = [1 0] x1 + [0] [0 0] [1] f(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] a() = [0] [0] b() = [1] [0] proper(x1) = [0 0] x1 + [0] [0 0] [1] ok(x1) = [1 0] x1 + [1] [0 0] [1] top(x1) = [1 0] x1 + [1] [0 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(f(X, X)) -> mark(f(a(), b())) , active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , top(mark(X)) -> top(proper(X))} Weak Trs: { active(b()) -> mark(a()) , top(ok(X)) -> top(active(X)) , f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { proper(a()) -> ok(a()) , proper(b()) -> ok(b())} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1, 2}, Uargs(mark) = {1}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(top) = {1} 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] f(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [1] [0 0] [1] a() = [0] [0] b() = [0] [0] proper(x1) = [0 0] x1 + [3] [0 0] [0] ok(x1) = [1 0] x1 + [1] [0 0] [0] top(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(f(X, X)) -> mark(f(a(), b())) , active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X))} Weak Trs: { proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , active(b()) -> mark(a()) , top(ok(X)) -> top(active(X)) , f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {active(f(X, X)) -> mark(f(a(), b()))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1, 2}, Uargs(mark) = {1}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(top) = {1} 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] f(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [1] mark(x1) = [1 0] x1 + [0] [0 0] [1] a() = [0] [0] b() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [1] ok(x1) = [1 0] x1 + [1] [0 0] [1] top(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(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X))} Weak Trs: { active(f(X, X)) -> mark(f(a(), b())) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , active(b()) -> mark(a()) , top(ok(X)) -> top(active(X)) , f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {top(mark(X)) -> top(proper(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(f) = {1, 2}, Uargs(mark) = {1}, Uargs(proper) = {}, Uargs(ok) = {1}, Uargs(top) = {1} 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] f(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 0] [2] mark(x1) = [1 0] x1 + [1] [0 0] [0] a() = [0] [0] b() = [1] [0] proper(x1) = [1 0] x1 + [0] [0 0] [0] ok(x1) = [1 0] x1 + [0] [0 1] [0] top(x1) = [1 1] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2))} Weak Trs: { top(mark(X)) -> top(proper(X)) , active(f(X, X)) -> mark(f(a(), b())) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , active(b()) -> mark(a()) , top(ok(X)) -> top(active(X)) , f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { active(f(X1, X2)) -> f(active(X1), X2) , f(mark(X1), X2) -> mark(f(X1, X2)) , proper(f(X1, X2)) -> f(proper(X1), proper(X2))} Weak Trs: { top(mark(X)) -> top(proper(X)) , active(f(X, X)) -> mark(f(a(), b())) , proper(a()) -> ok(a()) , proper(b()) -> ok(b()) , active(b()) -> mark(a()) , top(ok(X)) -> top(active(X)) , f(ok(X1), ok(X2)) -> ok(f(X1, X2))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The problem is match-bounded by 1. The enriched problem is compatible with the following automaton: { active_0(3) -> 1 , active_0(4) -> 1 , active_0(5) -> 1 , active_0(7) -> 1 , f_0(3, 3) -> 2 , f_0(3, 4) -> 2 , f_0(3, 5) -> 2 , f_0(3, 7) -> 2 , f_0(4, 3) -> 2 , f_0(4, 4) -> 2 , f_0(4, 5) -> 2 , f_0(4, 7) -> 2 , f_0(5, 3) -> 2 , f_0(5, 4) -> 2 , f_0(5, 5) -> 2 , f_0(5, 7) -> 2 , f_0(7, 3) -> 2 , f_0(7, 4) -> 2 , f_0(7, 5) -> 2 , f_0(7, 7) -> 2 , f_1(3, 3) -> 9 , f_1(3, 4) -> 9 , f_1(3, 5) -> 9 , f_1(3, 7) -> 9 , f_1(4, 3) -> 9 , f_1(4, 4) -> 9 , f_1(4, 5) -> 9 , f_1(4, 7) -> 9 , f_1(5, 3) -> 9 , f_1(5, 4) -> 9 , f_1(5, 5) -> 9 , f_1(5, 7) -> 9 , f_1(7, 3) -> 9 , f_1(7, 4) -> 9 , f_1(7, 5) -> 9 , f_1(7, 7) -> 9 , mark_0(3) -> 3 , mark_0(4) -> 1 , mark_0(4) -> 3 , mark_0(5) -> 3 , mark_0(7) -> 3 , mark_1(9) -> 2 , mark_1(9) -> 9 , a_0() -> 4 , b_0() -> 5 , proper_0(3) -> 6 , proper_0(4) -> 6 , proper_0(5) -> 6 , proper_0(7) -> 6 , ok_0(2) -> 2 , ok_0(3) -> 7 , ok_0(4) -> 6 , ok_0(4) -> 7 , ok_0(5) -> 6 , ok_0(5) -> 7 , ok_0(7) -> 7 , ok_1(9) -> 9 , top_0(1) -> 8 , top_0(3) -> 8 , top_0(4) -> 8 , top_0(5) -> 8 , top_0(6) -> 8 , top_0(7) -> 8} Hurray, we answered YES(?,O(n^1))