select(x', revprefix, Cons(x, xs)) → mapconsapp(x', permute(revapp(revprefix, Cons(x, xs))), select(x, Cons(x', revprefix), xs))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
permute(Cons(x, xs)) → select(x, Nil, xs)
mapconsapp(x', Cons(x, xs), rest) → Cons(Cons(x', x), mapconsapp(x', xs, rest))
select(x, revprefix, Nil) → mapconsapp(x, permute(revapp(revprefix, Nil)), Nil)
revapp(Nil, rest) → rest
permute(Nil) → Cons(Nil, Nil)
mapconsapp(x, Nil, rest) → rest
goal(xs) → permute(xs)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
select'(x', revprefix, Cons'(x, xs)) → mapconsapp'(x', permute'(revapp'(revprefix, Cons'(x, xs))), select'(x, Cons'(x', revprefix), xs))
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
permute'(Cons'(x, xs)) → select'(x, Nil', xs)
mapconsapp'(x', Cons'(x, xs), rest) → Cons'(Cons'(x', x), mapconsapp'(x', xs, rest))
select'(x, revprefix, Nil') → mapconsapp'(x, permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil', Nil')
mapconsapp'(x, Nil', rest) → rest
goal'(xs) → permute'(xs)
Sliced the following arguments:
select'/0
Cons'/0
mapconsapp'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Infered types.
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Heuristically decided to analyse the following defined symbols:
select', mapconsapp', permute', revapp'
They will be analysed ascendingly in the following order:
mapconsapp' < select'
select' = permute'
revapp' < select'
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))
The following defined symbols remain to be analysed:
mapconsapp', select', permute', revapp'
They will be analysed ascendingly in the following order:
mapconsapp' < select'
select' = permute'
revapp' < select'
Proved the following rewrite lemma:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
Induction Base:
mapconsapp'(_gen_Cons':Nil'2(0), _gen_Cons':Nil'2(b)) →RΩ(1)
_gen_Cons':Nil'2(b)
Induction Step:
mapconsapp'(_gen_Cons':Nil'2(+(_$n5, 1)), _gen_Cons':Nil'2(_b139)) →RΩ(1)
Cons'(mapconsapp'(_gen_Cons':Nil'2(_$n5), _gen_Cons':Nil'2(_b139))) →IH
Cons'(_gen_Cons':Nil'2(+(_$n5, _b139)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Lemmas:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))
The following defined symbols remain to be analysed:
revapp', select', permute'
They will be analysed ascendingly in the following order:
select' = permute'
revapp' < select'
Could not prove a rewrite lemma for the defined symbol revapp'.
The following conjecture could not be proven:
revapp'(_gen_Cons':Nil'2(_n586), _gen_Cons':Nil'2(b)) →? _gen_Cons':Nil'2(+(_n586, b))
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Lemmas:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))
The following defined symbols remain to be analysed:
permute', select'
They will be analysed ascendingly in the following order:
select' = permute'
Proved the following rewrite lemma:
permute'(_gen_Cons':Nil'2(+(1, _n1856))) → _*3, rt ∈ Ω(n1856)
Induction Base:
permute'(_gen_Cons':Nil'2(+(1, 0)))
Induction Step:
permute'(_gen_Cons':Nil'2(+(1, +(_$n1857, 1)))) →RΩ(1)
select'(Nil', _gen_Cons':Nil'2(+(1, _$n1857))) →RΩ(1)
mapconsapp'(permute'(revapp'(Nil', Cons'(_gen_Cons':Nil'2(_$n1857)))), select'(Cons'(Nil'), _gen_Cons':Nil'2(_$n1857))) →RΩ(1)
mapconsapp'(permute'(Cons'(_gen_Cons':Nil'2(_$n1857))), select'(Cons'(Nil'), _gen_Cons':Nil'2(_$n1857))) →IH
mapconsapp'(_*3, select'(Cons'(Nil'), _gen_Cons':Nil'2(_$n1857)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Lemmas:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
permute'(_gen_Cons':Nil'2(+(1, _n1856))) → _*3, rt ∈ Ω(n1856)
Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))
The following defined symbols remain to be analysed:
select'
They will be analysed ascendingly in the following order:
select' = permute'
Could not prove a rewrite lemma for the defined symbol select'.
Rules:
select'(revprefix, Cons'(xs)) → mapconsapp'(permute'(revapp'(revprefix, Cons'(xs))), select'(Cons'(revprefix), xs))
revapp'(Cons'(xs), rest) → revapp'(xs, Cons'(rest))
permute'(Cons'(xs)) → select'(Nil', xs)
mapconsapp'(Cons'(xs), rest) → Cons'(mapconsapp'(xs, rest))
select'(revprefix, Nil') → mapconsapp'(permute'(revapp'(revprefix, Nil')), Nil')
revapp'(Nil', rest) → rest
permute'(Nil') → Cons'(Nil')
mapconsapp'(Nil', rest) → rest
goal'(xs) → permute'(xs)
Types:
select' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
mapconsapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
permute' :: Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'
Lemmas:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
permute'(_gen_Cons':Nil'2(+(1, _n1856))) → _*3, rt ∈ Ω(n1856)
Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
mapconsapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)