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

immatcopy(Cons(x, xs)) → Cons(Nil, immatcopy(xs))
nestimeql(Nil) → number42(Nil)
nestimeql(Cons(x, xs)) → nestimeql(immatcopy(Cons(x, xs)))
immatcopy(Nil) → Nil
number42(x) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))))))))))))))))))))))))))))
goal(x) → nestimeql(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


immatcopy'(Cons'(x, xs)) → Cons'(Nil', immatcopy'(xs))
nestimeql'(Nil') → number42'(Nil')
nestimeql'(Cons'(x, xs)) → nestimeql'(immatcopy'(Cons'(x, xs)))
immatcopy'(Nil') → Nil'
number42'(x) → Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Cons'(Nil', Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0
number42'/0

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


immatcopy'(Cons'(xs)) → Cons'(immatcopy'(xs))
nestimeql'(Nil') → number42'
nestimeql'(Cons'(xs)) → nestimeql'(immatcopy'(Cons'(xs)))
immatcopy'(Nil') → Nil'
number42' → Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
immatcopy'(Cons'(xs)) → Cons'(immatcopy'(xs))
nestimeql'(Nil') → number42'
nestimeql'(Cons'(xs)) → nestimeql'(immatcopy'(Cons'(xs)))
immatcopy'(Nil') → Nil'
number42' → Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Types:
immatcopy' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
nestimeql' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
number42' :: 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:
immatcopy', nestimeql'

They will be analysed ascendingly in the following order:
immatcopy' < nestimeql'

Rules:
immatcopy'(Cons'(xs)) → Cons'(immatcopy'(xs))
nestimeql'(Nil') → number42'
nestimeql'(Cons'(xs)) → nestimeql'(immatcopy'(Cons'(xs)))
immatcopy'(Nil') → Nil'
number42' → Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Types:
immatcopy' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
nestimeql' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
number42' :: 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:
immatcopy', nestimeql'

They will be analysed ascendingly in the following order:
immatcopy' < nestimeql'

Proved the following rewrite lemma:
immatcopy'(_gen_Cons':Nil'2(_n4)) → _gen_Cons':Nil'2(_n4), rt ∈ Ω(1 + n4)

Induction Base:
immatcopy'(_gen_Cons':Nil'2(0)) →RΩ(1)
Nil'

Induction Step:
immatcopy'(_gen_Cons':Nil'2(+(_$n5, 1))) →RΩ(1)
Cons'(immatcopy'(_gen_Cons':Nil'2(_$n5))) →IH
Cons'(_gen_Cons':Nil'2(_$n5))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
immatcopy'(Cons'(xs)) → Cons'(immatcopy'(xs))
nestimeql'(Nil') → number42'
nestimeql'(Cons'(xs)) → nestimeql'(immatcopy'(Cons'(xs)))
immatcopy'(Nil') → Nil'
number42' → Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Types:
immatcopy' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
nestimeql' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
number42' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
immatcopy'(_gen_Cons':Nil'2(_n4)) → _gen_Cons':Nil'2(_n4), 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:
nestimeql'

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

Rules:
immatcopy'(Cons'(xs)) → Cons'(immatcopy'(xs))
nestimeql'(Nil') → number42'
nestimeql'(Cons'(xs)) → nestimeql'(immatcopy'(Cons'(xs)))
immatcopy'(Nil') → Nil'
number42' → Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Cons'(Nil'))))))))))))))))))))))))))))))))))))))))))
goal'(x) → nestimeql'(x)

Types:
immatcopy' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
nestimeql' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
number42' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
immatcopy'(_gen_Cons':Nil'2(_n4)) → _gen_Cons':Nil'2(_n4), rt ∈ Ω(1 + n4)

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:
immatcopy'(_gen_Cons':Nil'2(_n4)) → _gen_Cons':Nil'2(_n4), rt ∈ Ω(1 + n4)