We consider the following Problem: Strict Trs: { active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , 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(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , 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: {top(ok(X)) -> top(active(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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] [1 0] [1] g(x1) = [1 0] x1 + [0] [0 0] [1] mark(x1) = [1 0] x1 + [1] [1 0] [1] h(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] d() = [0] [0] proper(x1) = [0 0] x1 + [1] [0 0] [0] ok(x1) = [1 0] x1 + [3] [0 1] [3] top(x1) = [1 0] x1 + [0] [1 0] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , top(mark(X)) -> top(proper(X))} Weak Trs: {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: { proper(c()) -> ok(c()) , proper(d()) -> ok(d())} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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] [1 0] [1] g(x1) = [1 0] x1 + [0] [0 0] [0] mark(x1) = [1 0] x1 + [1] [1 0] [1] h(x1) = [1 0] x1 + [0] [0 0] [0] c() = [0] [0] d() = [0] [0] proper(x1) = [0 0] x1 + [3] [0 0] [2] 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(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , top(mark(X)) -> top(proper(X))} Weak Trs: { proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , 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: {active(h(d())) -> mark(g(c()))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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] [1 0] [1] g(x1) = [1 0] x1 + [0] [0 0] [0] mark(x1) = [1 0] x1 + [1] [1 0] [1] h(x1) = [1 0] x1 + [0] [0 0] [1] c() = [0] [0] d() = [1] [0] proper(x1) = [0 0] x1 + [2] [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(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , top(mark(X)) -> top(proper(X))} Weak Trs: { active(h(d())) -> mark(g(c())) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , 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: { active(g(X)) -> mark(h(X)) , active(c()) -> mark(d())} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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] [1 0] [0] g(x1) = [1 0] x1 + [0] [0 0] [1] mark(x1) = [1 0] x1 + [0] [1 0] [0] h(x1) = [1 0] x1 + [0] [0 0] [0] c() = [0] [0] d() = [0] [0] proper(x1) = [0 0] x1 + [2] [0 1] [0] ok(x1) = [1 0] x1 + [2] [0 1] [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: { proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X)) , top(mark(X)) -> top(proper(X))} Weak Trs: { active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , 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: {top(mark(X)) -> top(proper(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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 + [3] [0 0] [0] g(x1) = [1 0] x1 + [1] [0 0] [0] mark(x1) = [1 2] x1 + [1] [0 0] [0] h(x1) = [1 0] x1 + [1] [0 0] [0] c() = [2] [2] d() = [0] [2] proper(x1) = [1 0] x1 + [0] [0 1] [0] ok(x1) = [1 0] x1 + [0] [0 0] [2] top(x1) = [1 2] x1 + [0] [0 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X))} Weak Trs: { top(mark(X)) -> top(proper(X)) , active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , 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: { proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(active) = {}, Uargs(g) = {1}, Uargs(mark) = {1}, Uargs(h) = {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] [1] g(x1) = [1 0] x1 + [0] [0 1] [1] mark(x1) = [1 1] x1 + [0] [0 0] [1] h(x1) = [1 0] x1 + [0] [0 1] [1] c() = [0] [0] d() = [0] [0] proper(x1) = [0 1] x1 + [0] [0 1] [0] ok(x1) = [1 2] x1 + [0] [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: { g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X))} Weak Trs: { proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , top(mark(X)) -> top(proper(X)) , active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , top(ok(X)) -> top(active(X))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { g(ok(X)) -> ok(g(X)) , h(ok(X)) -> ok(h(X))} Weak Trs: { proper(g(X)) -> g(proper(X)) , proper(h(X)) -> h(proper(X)) , top(mark(X)) -> top(proper(X)) , active(g(X)) -> mark(h(X)) , active(c()) -> mark(d()) , active(h(d())) -> mark(g(c())) , proper(c()) -> ok(c()) , proper(d()) -> ok(d()) , top(ok(X)) -> top(active(X))} 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(5) -> 1 , active_0(6) -> 1 , active_0(8) -> 1 , g_0(3) -> 2 , g_0(5) -> 2 , g_0(6) -> 2 , g_0(8) -> 2 , g_1(3) -> 10 , g_1(5) -> 10 , g_1(6) -> 10 , g_1(8) -> 10 , mark_0(3) -> 3 , mark_0(5) -> 3 , mark_0(6) -> 1 , mark_0(6) -> 3 , mark_0(8) -> 3 , h_0(3) -> 4 , h_0(5) -> 4 , h_0(6) -> 4 , h_0(8) -> 4 , h_1(3) -> 11 , h_1(5) -> 11 , h_1(6) -> 11 , h_1(8) -> 11 , c_0() -> 5 , d_0() -> 6 , proper_0(3) -> 7 , proper_0(5) -> 7 , proper_0(6) -> 7 , proper_0(8) -> 7 , ok_0(3) -> 8 , ok_0(5) -> 7 , ok_0(5) -> 8 , ok_0(6) -> 7 , ok_0(6) -> 8 , ok_0(8) -> 8 , ok_1(10) -> 2 , ok_1(10) -> 10 , ok_1(11) -> 4 , ok_1(11) -> 11 , top_0(1) -> 9 , top_0(3) -> 9 , top_0(5) -> 9 , top_0(6) -> 9 , top_0(7) -> 9 , top_0(8) -> 9} Hurray, we answered YES(?,O(n^1))