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

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(x, xs))) → dec(Cons(x, xs))
dec(Cons(Cons(x, xs), Nil)) → dec(Nil)
dec(Cons(Cons(x', xs'), Cons(x, xs))) → dec(Cons(x, xs))
isNilNil(Cons(Nil, Nil)) → True
isNilNil(Cons(Nil, Cons(x, xs))) → False
isNilNil(Cons(Cons(x, xs), Nil)) → False
isNilNil(Cons(Cons(x', xs'), Cons(x, xs))) → False
nestdec(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)))))))))))))))))
nestdec(Cons(x, xs)) → nestdec(dec(Cons(x, xs)))
number17(n) → 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) → nestdec(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17'(n) → 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) → nestdec'(x)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
number17'/0

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


dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17' → 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) → nestdec'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17' → 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) → nestdec'(x)

Types:
dec' :: Nil':Cons' → Nil':Cons'
Cons' :: Nil':Cons' → Nil':Cons' → Nil':Cons'
Nil' :: Nil':Cons'
isNilNil' :: Nil':Cons' → True':False'
True' :: True':False'
False' :: True':False'
nestdec' :: Nil':Cons' → Nil':Cons'
number17' :: Nil':Cons'
goal' :: Nil':Cons' → Nil':Cons'
_hole_Nil':Cons'1 :: Nil':Cons'
_hole_True':False'2 :: True':False'
_gen_Nil':Cons'3 :: Nat → Nil':Cons'

Heuristically decided to analyse the following defined symbols:
dec', nestdec'

They will be analysed ascendingly in the following order:
dec' < nestdec'

Rules:
dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17' → 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) → nestdec'(x)

Types:
dec' :: Nil':Cons' → Nil':Cons'
Cons' :: Nil':Cons' → Nil':Cons' → Nil':Cons'
Nil' :: Nil':Cons'
isNilNil' :: Nil':Cons' → True':False'
True' :: True':False'
False' :: True':False'
nestdec' :: Nil':Cons' → Nil':Cons'
number17' :: Nil':Cons'
goal' :: Nil':Cons' → Nil':Cons'
_hole_Nil':Cons'1 :: Nil':Cons'
_hole_True':False'2 :: True':False'
_gen_Nil':Cons'3 :: Nat → Nil':Cons'

Generator Equations:
_gen_Nil':Cons'3(0) ⇔ Nil'
_gen_Nil':Cons'3(+(x, 1)) ⇔ Cons'(Nil', _gen_Nil':Cons'3(x))

The following defined symbols remain to be analysed:
dec', nestdec'

They will be analysed ascendingly in the following order:
dec' < nestdec'

Proved the following rewrite lemma:
dec'(_gen_Nil':Cons'3(+(1, _n5))) → _gen_Nil':Cons'3(0), rt ∈ Ω(1 + n5)

Induction Base:
dec'(_gen_Nil':Cons'3(+(1, 0))) →RΩ(1)
Nil'

Induction Step:
dec'(_gen_Nil':Cons'3(+(1, +(_$n6, 1)))) →RΩ(1)
dec'(Cons'(Nil', _gen_Nil':Cons'3(_$n6))) →IH
_gen_Nil':Cons'3(0)

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

Rules:
dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17' → 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) → nestdec'(x)

Types:
dec' :: Nil':Cons' → Nil':Cons'
Cons' :: Nil':Cons' → Nil':Cons' → Nil':Cons'
Nil' :: Nil':Cons'
isNilNil' :: Nil':Cons' → True':False'
True' :: True':False'
False' :: True':False'
nestdec' :: Nil':Cons' → Nil':Cons'
number17' :: Nil':Cons'
goal' :: Nil':Cons' → Nil':Cons'
_hole_Nil':Cons'1 :: Nil':Cons'
_hole_True':False'2 :: True':False'
_gen_Nil':Cons'3 :: Nat → Nil':Cons'

Lemmas:
dec'(_gen_Nil':Cons'3(+(1, _n5))) → _gen_Nil':Cons'3(0), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_Nil':Cons'3(0) ⇔ Nil'
_gen_Nil':Cons'3(+(x, 1)) ⇔ Cons'(Nil', _gen_Nil':Cons'3(x))

The following defined symbols remain to be analysed:
nestdec'

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

Rules:
dec'(Cons'(Nil', Nil')) → Nil'
dec'(Cons'(Nil', Cons'(x, xs))) → dec'(Cons'(x, xs))
dec'(Cons'(Cons'(x, xs), Nil')) → dec'(Nil')
dec'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → dec'(Cons'(x, xs))
isNilNil'(Cons'(Nil', Nil')) → True'
isNilNil'(Cons'(Nil', Cons'(x, xs))) → False'
isNilNil'(Cons'(Cons'(x, xs), Nil')) → False'
isNilNil'(Cons'(Cons'(x', xs'), Cons'(x, xs))) → False'
nestdec'(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')))))))))))))))))
nestdec'(Cons'(x, xs)) → nestdec'(dec'(Cons'(x, xs)))
number17' → 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) → nestdec'(x)

Types:
dec' :: Nil':Cons' → Nil':Cons'
Cons' :: Nil':Cons' → Nil':Cons' → Nil':Cons'
Nil' :: Nil':Cons'
isNilNil' :: Nil':Cons' → True':False'
True' :: True':False'
False' :: True':False'
nestdec' :: Nil':Cons' → Nil':Cons'
number17' :: Nil':Cons'
goal' :: Nil':Cons' → Nil':Cons'
_hole_Nil':Cons'1 :: Nil':Cons'
_hole_True':False'2 :: True':False'
_gen_Nil':Cons'3 :: Nat → Nil':Cons'

Lemmas:
dec'(_gen_Nil':Cons'3(+(1, _n5))) → _gen_Nil':Cons'3(0), rt ∈ Ω(1 + n5)

Generator Equations:
_gen_Nil':Cons'3(0) ⇔ Nil'
_gen_Nil':Cons'3(+(x, 1)) ⇔ Cons'(Nil', _gen_Nil':Cons'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
dec'(_gen_Nil':Cons'3(+(1, _n5))) → _gen_Nil':Cons'3(0), rt ∈ Ω(1 + n5)