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

admit(x, nil) → nil
admit(x, .(u, .(v, .(w, z)))) → cond(=(sum(x, u, v), w), .(u, .(v, .(w, admit(carry(x, u, v), z)))))
cond(true, y) → y

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


admit'(x, nil') → nil'
admit'(x, .'(u, .'(v, .'(w', z)))) → cond'(='(sum'(x, u, v), w'), .'(u, .'(v, .'(w', admit'(carry'(x, u, v), z)))))
cond'(true', y) → y

Rewrite Strategy: INNERMOST

Sliced the following arguments:
admit'/0
='/0
='/1
sum'/0
sum'/1
sum'/2
carry'/0
carry'/1
carry'/2

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


admit'(nil') → nil'
admit'(.'(u, .'(v, .'(w', z)))) → cond'(=', .'(u, .'(v, .'(w', admit'(z)))))
cond'(true', y) → y

Rewrite Strategy: INNERMOST

Infered types.

Rules:
admit'(nil') → nil'
admit'(.'(u, .'(v, .'(w', z)))) → cond'(=', .'(u, .'(v, .'(w', admit'(z)))))
cond'(true', y) → y

Types:
admit' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: w' → nil':.' → nil':.'
w' :: w'
cond' :: =':true' → nil':.' → nil':.'
=' :: =':true'
true' :: =':true'
_hole_nil':.'1 :: nil':.'
_hole_w'2 :: w'
_hole_=':true'3 :: =':true'
_gen_nil':.'4 :: Nat → nil':.'

Heuristically decided to analyse the following defined symbols:
admit'

Rules:
admit'(nil') → nil'
admit'(.'(u, .'(v, .'(w', z)))) → cond'(=', .'(u, .'(v, .'(w', admit'(z)))))
cond'(true', y) → y

Types:
admit' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: w' → nil':.' → nil':.'
w' :: w'
cond' :: =':true' → nil':.' → nil':.'
=' :: =':true'
true' :: =':true'
_hole_nil':.'1 :: nil':.'
_hole_w'2 :: w'
_hole_=':true'3 :: =':true'
_gen_nil':.'4 :: Nat → nil':.'

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

The following defined symbols remain to be analysed:
admit'

Proved the following rewrite lemma:
admit'(_gen_nil':.'4(+(3, *(3, _n6)))) → _*5, rt ∈ Ω(n6)

Induction Base:
admit'(_gen_nil':.'4(+(3, *(3, 0))))

Induction Step:
admit'(_gen_nil':.'4(+(3, *(3, +(_$n7, 1))))) →RΩ(1)
cond'(=', .'(w', .'(w', .'(w', admit'(_gen_nil':.'4(+(3, *(3, _$n7)))))))) →IH
cond'(=', .'(w', .'(w', .'(w', _*5))))

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

Rules:
admit'(nil') → nil'
admit'(.'(u, .'(v, .'(w', z)))) → cond'(=', .'(u, .'(v, .'(w', admit'(z)))))
cond'(true', y) → y

Types:
admit' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: w' → nil':.' → nil':.'
w' :: w'
cond' :: =':true' → nil':.' → nil':.'
=' :: =':true'
true' :: =':true'
_hole_nil':.'1 :: nil':.'
_hole_w'2 :: w'
_hole_=':true'3 :: =':true'
_gen_nil':.'4 :: Nat → nil':.'

Lemmas:
admit'(_gen_nil':.'4(+(3, *(3, _n6)))) → _*5, rt ∈ Ω(n6)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
admit'(_gen_nil':.'4(+(3, *(3, _n6)))) → _*5, rt ∈ Ω(n6)