Runtime Complexity TRS:
The TRS R consists of the following rules:

selects(x', revprefix, Cons(x, xs)) → Cons(Cons(x', revapp(revprefix, Cons(x, xs))), selects(x, Cons(x', revprefix), xs))
select(Cons(x, xs)) → selects(x, Nil, xs)
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
selects(x, revprefix, Nil) → Cons(Cons(x, revapp(revprefix, Nil)), Nil)
select(Nil) → Nil
revapp(Nil, rest) → rest

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


selects'(x', revprefix, Cons'(x, xs)) → Cons'(Cons'(x', revapp'(revprefix, Cons'(x, xs))), selects'(x, Cons'(x', revprefix), xs))
select'(Cons'(x, xs)) → selects'(x, Nil', xs)
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
selects'(x, revprefix, Nil') → Cons'(Cons'(x, revapp'(revprefix, Nil')), Nil')
select'(Nil') → Nil'
revapp'(Nil', rest) → rest

Rewrite Strategy: INNERMOST

Infered types.

Rules:
selects'(x', revprefix, Cons'(x, xs)) → Cons'(Cons'(x', revapp'(revprefix, Cons'(x, xs))), selects'(x, Cons'(x', revprefix), xs))
select'(Cons'(x, xs)) → selects'(x, Nil', xs)
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
selects'(x, revprefix, Nil') → Cons'(Cons'(x, revapp'(revprefix, Nil')), Nil')
select'(Nil') → Nil'
revapp'(Nil', rest) → rest

Types:
selects' :: Cons':Nil' → Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
select' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
selects', revapp'

They will be analysed ascendingly in the following order:
revapp' < selects'

Rules:
selects'(x', revprefix, Cons'(x, xs)) → Cons'(Cons'(x', revapp'(revprefix, Cons'(x, xs))), selects'(x, Cons'(x', revprefix), xs))
select'(Cons'(x, xs)) → selects'(x, Nil', xs)
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
selects'(x, revprefix, Nil') → Cons'(Cons'(x, revapp'(revprefix, Nil')), Nil')
select'(Nil') → Nil'
revapp'(Nil', rest) → rest

Types:
selects' :: Cons':Nil' → Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
select' :: Cons':Nil' → Cons':Nil'
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'(Nil', _gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
revapp', selects'

They will be analysed ascendingly in the following order:
revapp' < selects'

Could not prove a rewrite lemma for the defined symbol revapp'.

The following conjecture could not be proven:

revapp'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) →? _gen_Cons':Nil'2(+(_n4, b))

Rules:
selects'(x', revprefix, Cons'(x, xs)) → Cons'(Cons'(x', revapp'(revprefix, Cons'(x, xs))), selects'(x, Cons'(x', revprefix), xs))
select'(Cons'(x, xs)) → selects'(x, Nil', xs)
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
selects'(x, revprefix, Nil') → Cons'(Cons'(x, revapp'(revprefix, Nil')), Nil')
select'(Nil') → Nil'
revapp'(Nil', rest) → rest

Types:
selects' :: Cons':Nil' → Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
select' :: Cons':Nil' → Cons':Nil'
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'(Nil', _gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
selects'

Could not prove a rewrite lemma for the defined symbol selects'.

Rules:
selects'(x', revprefix, Cons'(x, xs)) → Cons'(Cons'(x', revapp'(revprefix, Cons'(x, xs))), selects'(x, Cons'(x', revprefix), xs))
select'(Cons'(x, xs)) → selects'(x, Nil', xs)
revapp'(Cons'(x, xs), rest) → revapp'(xs, Cons'(x, rest))
selects'(x, revprefix, Nil') → Cons'(Cons'(x, revapp'(revprefix, Nil')), Nil')
select'(Nil') → Nil'
revapp'(Nil', rest) → rest

Types:
selects' :: Cons':Nil' → Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
revapp' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
select' :: Cons':Nil' → Cons':Nil'
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'(Nil', _gen_Cons':Nil'2(x))

No more defined symbols left to analyse.