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

purge(nil) → nil
purge(.(x, y)) → .(x, purge(remove(x, y)))
remove(x, nil) → nil
remove(x, .(y, z)) → if(=(x, y), remove(x, z), .(y, remove(x, z)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


purge'(nil') → nil'
purge'(.'(x, y)) → .'(x, purge'(remove'(x, y)))
remove'(x, nil') → nil'
remove'(x, .'(y, z)) → if'(='(x, y), remove'(x, z), .'(y, remove'(x, z)))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
.'/0
remove'/0
if'/0
='/0
='/1

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


purge'(nil') → nil'
purge'(.'(y)) → .'(purge'(remove'(y)))
remove'(nil') → nil'
remove'(.'(z)) → if'(remove'(z), .'(y, remove'(z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
purge'(nil') → nil'
purge'(.'(y)) → .'(purge'(remove'(y)))
remove'(nil') → nil'
remove'(.'(z)) → if'(remove'(z), .'(y, remove'(z)))

Types:
purge' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if'
remove' :: nil':.':if' → nil':.':if'
if' :: nil':.':if' → .' → nil':.':if'
.' :: y → nil':.':if' → .'
y :: y
_hole_nil':.':if'1 :: nil':.':if'
_hole_.'2 :: .'
_hole_y3 :: y
_gen_nil':.':if'4 :: Nat → nil':.':if'

Heuristically decided to analyse the following defined symbols:
purge', remove'

They will be analysed ascendingly in the following order:
remove' < purge'

Rules:
purge'(nil') → nil'
purge'(.'(y)) → .'(purge'(remove'(y)))
remove'(nil') → nil'
remove'(.'(z)) → if'(remove'(z), .'(y, remove'(z)))

Types:
purge' :: nil':.':if' → nil':.':if'
nil' :: nil':.':if'
.' :: nil':.':if' → nil':.':if'
remove' :: nil':.':if' → nil':.':if'
if' :: nil':.':if' → .' → nil':.':if'
.' :: y → nil':.':if' → .'
y :: y
_hole_nil':.':if'1 :: nil':.':if'
_hole_.'2 :: .'
_hole_y3 :: y
_gen_nil':.':if'4 :: Nat → nil':.':if'

Generator Equations:
_gen_nil':.':if'4(0) ⇔ nil'
_gen_nil':.':if'4(+(x, 1)) ⇔ .'(_gen_nil':.':if'4(x))

The following defined symbols remain to be analysed:
remove', purge'

They will be analysed ascendingly in the following order:
remove' < purge'

Proved the following rewrite lemma:
remove'(_gen_nil':.':if'4(+(1, _n6))) → _*5, rt ∈ Ω(2n)

Induction Base:
remove'(_gen_nil':.':if'4(+(1, 0)))

Induction Step:
remove'(_gen_nil':.':if'4(+(1, +(_$n7, 1)))) →RΩ(1)
if'(remove'(_gen_nil':.':if'4(+(1, _$n7))), .'(y, remove'(_gen_nil':.':if'4(+(1, _$n7))))) →IH
if'(_*5, .'(y, remove'(_gen_nil':.':if'4(+(1, _$n7))))) →IH
if'(_*5, .'(y, _*5))

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