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))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
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))
Infered types.
Rules:
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))
Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'
Heuristically decided to analyse the following defined symbols:
flatten', ++', rev'
They will be analysed ascendingly in the following order:
++' < flatten'
++' < rev'
Rules:
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))
Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'
Generator Equations:
_gen_nil':unit'2(0) ⇔ nil'
_gen_nil':unit'2(+(x, 1)) ⇔ unit'(_gen_nil':unit'2(x))
The following defined symbols remain to be analysed:
++', flatten', rev'
They will be analysed ascendingly in the following order:
++' < flatten'
++' < rev'
Could not prove a rewrite lemma for the defined symbol ++'.
Rules:
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))
Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'
Generator Equations:
_gen_nil':unit'2(0) ⇔ nil'
_gen_nil':unit'2(+(x, 1)) ⇔ unit'(_gen_nil':unit'2(x))
The following defined symbols remain to be analysed:
flatten', rev'
Proved the following rewrite lemma:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)
Induction Base:
flatten'(_gen_nil':unit'2(0)) →RΩ(1)
nil'
Induction Step:
flatten'(_gen_nil':unit'2(+(_$n33, 1))) →RΩ(1)
flatten'(_gen_nil':unit'2(_$n33)) →IH
_gen_nil':unit'2(0)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
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))
Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'
Lemmas:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)
Generator Equations:
_gen_nil':unit'2(0) ⇔ nil'
_gen_nil':unit'2(+(x, 1)) ⇔ unit'(_gen_nil':unit'2(x))
The following defined symbols remain to be analysed:
rev'
Could not prove a rewrite lemma for the defined symbol rev'.
Rules:
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))
Types:
flatten' :: nil':unit' → nil':unit'
nil' :: nil':unit'
unit' :: nil':unit' → nil':unit'
++' :: nil':unit' → nil':unit' → nil':unit'
rev' :: nil':unit' → nil':unit'
_hole_nil':unit'1 :: nil':unit'
_gen_nil':unit'2 :: Nat → nil':unit'
Lemmas:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)
Generator Equations:
_gen_nil':unit'2(0) ⇔ nil'
_gen_nil':unit'2(+(x, 1)) ⇔ unit'(_gen_nil':unit'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
flatten'(_gen_nil':unit'2(_n32)) → _gen_nil':unit'2(0), rt ∈ Ω(1 + n32)