We consider the following Problem: Strict Trs: { flatten(nil()) -> nil() , flatten(unit(x)) -> flatten(x) , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(++(x, y)) -> ++(rev(y), rev(x)) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y , ++(++(x, y), z) -> ++(x, ++(y, z))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { flatten(nil()) -> nil() , flatten(unit(x)) -> flatten(x) , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(++(x, y)) -> ++(rev(y), rev(x)) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y , ++(++(x, y), z) -> ++(x, ++(y, z))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { flatten(nil()) -> nil() , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(flatten) = {}, Uargs(unit) = {}, Uargs(++) = {1, 2}, Uargs(rev) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: flatten(x1) = [0 0] x1 + [1] [0 0] [1] nil() = [0] [0] unit(x1) = [0 0] x1 + [0] [0 0] [0] ++(x1, x2) = [1 0] x1 + [1 0] x2 + [1] [0 1] [0 1] [1] rev(x1) = [0 1] x1 + [1] [1 0] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { flatten(unit(x)) -> flatten(x) , flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , rev(++(x, y)) -> ++(rev(y), rev(x)) , ++(++(x, y), z) -> ++(x, ++(y, z))} Weak Trs: { flatten(nil()) -> nil() , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: { flatten(unit(x)) -> flatten(x) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x)} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(flatten) = {}, Uargs(unit) = {}, Uargs(++) = {1, 2}, Uargs(rev) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: flatten(x1) = [0 2] x1 + [0] [0 1] [1] nil() = [0] [3] unit(x1) = [0 0] x1 + [0] [0 1] [2] ++(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [0] rev(x1) = [1 0] x1 + [0] [0 1] [0] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , rev(++(x, y)) -> ++(rev(y), rev(x)) , ++(++(x, y), z) -> ++(x, ++(y, z))} Weak Trs: { flatten(unit(x)) -> flatten(x) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , flatten(nil()) -> nil() , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The weightgap principle applies, where following rules are oriented strictly: TRS Component: {flatten(++(x, y)) -> ++(flatten(x), flatten(y))} Interpretation of nonconstant growth: ------------------------------------- The following argument positions are usable: Uargs(flatten) = {}, Uargs(unit) = {}, Uargs(++) = {1, 2}, Uargs(rev) = {} We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation: Interpretation Functions: flatten(x1) = [0 1] x1 + [0] [0 1] [0] nil() = [0] [3] unit(x1) = [1 0] x1 + [0] [0 1] [3] ++(x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 1] [1] rev(x1) = [1 0] x1 + [0] [0 1] [1] The strictly oriented rules are moved into the weak component. We consider the following Problem: Strict Trs: { rev(++(x, y)) -> ++(rev(y), rev(x)) , ++(++(x, y), z) -> ++(x, ++(y, z))} Weak Trs: { flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , flatten(unit(x)) -> flatten(x) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , flatten(nil()) -> nil() , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: { rev(++(x, y)) -> ++(rev(y), rev(x)) , ++(++(x, y), z) -> ++(x, ++(y, z))} Weak Trs: { flatten(++(x, y)) -> ++(flatten(x), flatten(y)) , flatten(unit(x)) -> flatten(x) , flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)) , flatten(flatten(x)) -> flatten(x) , flatten(nil()) -> nil() , rev(nil()) -> nil() , rev(unit(x)) -> unit(x) , rev(rev(x)) -> x , ++(x, nil()) -> x , ++(nil(), y) -> y} 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: { flatten_0(2) -> 1 , nil_0() -> 1 , nil_0() -> 2 , unit_0(2) -> 1 , unit_0(2) -> 2 , ++_0(2, 2) -> 1 , rev_0(2) -> 1} Hurray, we answered YES(?,O(n^1))