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

del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))

Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'

Heuristically decided to analyse the following defined symbols:
del', ='

They will be analysed ascendingly in the following order:
=' < del'

Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))

Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'

Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))

The following defined symbols remain to be analysed:
=', del'

They will be analysed ascendingly in the following order:
=' < del'

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

Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))

Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'

Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))

The following defined symbols remain to be analysed:
del'

Proved the following rewrite lemma:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)

Induction Base:
del'(_gen_.':nil':u':v'3(+(2, 0)))

Induction Step:
del'(_gen_.':nil':u':v'3(+(2, +(_\$n117, 1)))) →RΩ(1)
f'(='(nil', nil'), nil', nil', _gen_.':nil':u':v'3(+(1, _\$n117))) →RΩ(1)
f'(true', nil', nil', _gen_.':nil':u':v'3(+(1, _\$n117))) →RΩ(1)
del'(.'(nil', _gen_.':nil':u':v'3(+(1, _\$n117)))) →IH
_*5

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

Rules:
del'(.'(x, .'(y, z))) → f'(='(x, y), x, y, z)
f'(true', x, y, z) → del'(.'(y, z))
f'(false', x, y, z) → .'(x, del'(.'(y, z)))
='(nil', nil') → true'
='(.'(x, y), nil') → false'
='(nil', .'(y, z)) → false'
='(.'(x, y), .'(u', v')) → and'(='(x, u'), ='(y, v'))

Types:
del' :: .':nil':u':v' → .':nil':u':v'
.' :: .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
f' :: true':false':and' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v' → .':nil':u':v'
=' :: .':nil':u':v' → .':nil':u':v' → true':false':and'
true' :: true':false':and'
false' :: true':false':and'
nil' :: .':nil':u':v'
u' :: .':nil':u':v'
v' :: .':nil':u':v'
and' :: true':false':and' → true':false':and' → true':false':and'
_hole_.':nil':u':v'1 :: .':nil':u':v'
_hole_true':false':and'2 :: true':false':and'
_gen_.':nil':u':v'3 :: Nat → .':nil':u':v'
_gen_true':false':and'4 :: Nat → true':false':and'

Lemmas:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)

Generator Equations:
_gen_.':nil':u':v'3(0) ⇔ nil'
_gen_.':nil':u':v'3(+(x, 1)) ⇔ .'(nil', _gen_.':nil':u':v'3(x))
_gen_true':false':and'4(0) ⇔ false'
_gen_true':false':and'4(+(x, 1)) ⇔ and'(false', _gen_true':false':and'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
del'(_gen_.':nil':u':v'3(+(2, _n116))) → _*5, rt ∈ Ω(n116)