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

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Types:
circ' :: cons':id' → cons':id' → cons':id'
cons' :: lift' → cons':id' → cons':id'
msubst' :: lift' → cons':id' → lift'
lift' :: lift'
id' :: cons':id'
subst' :: subst' → cons':id' → subst'
_hole_cons':id'1 :: cons':id'
_hole_lift'2 :: lift'
_hole_subst'3 :: subst'
_gen_cons':id'4 :: Nat → cons':id'

Heuristically decided to analyse the following defined symbols:
circ', msubst'

They will be analysed ascendingly in the following order:
circ' = msubst'

Rules:
circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Types:
circ' :: cons':id' → cons':id' → cons':id'
cons' :: lift' → cons':id' → cons':id'
msubst' :: lift' → cons':id' → lift'
lift' :: lift'
id' :: cons':id'
subst' :: subst' → cons':id' → subst'
_hole_cons':id'1 :: cons':id'
_hole_lift'2 :: lift'
_hole_subst'3 :: subst'
_gen_cons':id'4 :: Nat → cons':id'

Generator Equations:
_gen_cons':id'4(0) ⇔ id'
_gen_cons':id'4(+(x, 1)) ⇔ cons'(lift', _gen_cons':id'4(x))

The following defined symbols remain to be analysed:
msubst', circ'

They will be analysed ascendingly in the following order:
circ' = msubst'

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

Rules:
circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Types:
circ' :: cons':id' → cons':id' → cons':id'
cons' :: lift' → cons':id' → cons':id'
msubst' :: lift' → cons':id' → lift'
lift' :: lift'
id' :: cons':id'
subst' :: subst' → cons':id' → subst'
_hole_cons':id'1 :: cons':id'
_hole_lift'2 :: lift'
_hole_subst'3 :: subst'
_gen_cons':id'4 :: Nat → cons':id'

Generator Equations:
_gen_cons':id'4(0) ⇔ id'
_gen_cons':id'4(+(x, 1)) ⇔ cons'(lift', _gen_cons':id'4(x))

The following defined symbols remain to be analysed:
circ'

They will be analysed ascendingly in the following order:
circ' = msubst'

Proved the following rewrite lemma:
circ'(_gen_cons':id'4(_n24), _gen_cons':id'4(_n24)) → _gen_cons':id'4(_n24), rt ∈ Ω(1 + n24)

Induction Base:
circ'(_gen_cons':id'4(0), _gen_cons':id'4(0)) →RΩ(1)
_gen_cons':id'4(0)

Induction Step:
circ'(_gen_cons':id'4(+(_\$n25, 1)), _gen_cons':id'4(+(_\$n25, 1))) →RΩ(1)
cons'(lift', circ'(_gen_cons':id'4(_\$n25), _gen_cons':id'4(_\$n25))) →IH
cons'(lift', _gen_cons':id'4(_\$n25))

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

Rules:
circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Types:
circ' :: cons':id' → cons':id' → cons':id'
cons' :: lift' → cons':id' → cons':id'
msubst' :: lift' → cons':id' → lift'
lift' :: lift'
id' :: cons':id'
subst' :: subst' → cons':id' → subst'
_hole_cons':id'1 :: cons':id'
_hole_lift'2 :: lift'
_hole_subst'3 :: subst'
_gen_cons':id'4 :: Nat → cons':id'

Lemmas:
circ'(_gen_cons':id'4(_n24), _gen_cons':id'4(_n24)) → _gen_cons':id'4(_n24), rt ∈ Ω(1 + n24)

Generator Equations:
_gen_cons':id'4(0) ⇔ id'
_gen_cons':id'4(+(x, 1)) ⇔ cons'(lift', _gen_cons':id'4(x))

The following defined symbols remain to be analysed:
msubst'

They will be analysed ascendingly in the following order:
circ' = msubst'

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

Rules:
circ'(cons'(a, s), t) → cons'(msubst'(a, t), circ'(s, t))
circ'(cons'(lift', s), cons'(a, t)) → cons'(a, circ'(s, t))
circ'(cons'(lift', s), cons'(lift', t)) → cons'(lift', circ'(s, t))
circ'(circ'(s, t), u) → circ'(s, circ'(t, u))
circ'(s, id') → s
circ'(id', s) → s
circ'(cons'(lift', s), circ'(cons'(lift', t), u)) → circ'(cons'(lift', circ'(s, t)), u)
subst'(a, id') → a
msubst'(a, id') → a
msubst'(msubst'(a, s), t) → msubst'(a, circ'(s, t))

Types:
circ' :: cons':id' → cons':id' → cons':id'
cons' :: lift' → cons':id' → cons':id'
msubst' :: lift' → cons':id' → lift'
lift' :: lift'
id' :: cons':id'
subst' :: subst' → cons':id' → subst'
_hole_cons':id'1 :: cons':id'
_hole_lift'2 :: lift'
_hole_subst'3 :: subst'
_gen_cons':id'4 :: Nat → cons':id'

Lemmas:
circ'(_gen_cons':id'4(_n24), _gen_cons':id'4(_n24)) → _gen_cons':id'4(_n24), rt ∈ Ω(1 + n24)

Generator Equations:
_gen_cons':id'4(0) ⇔ id'
_gen_cons':id'4(+(x, 1)) ⇔ cons'(lift', _gen_cons':id'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
circ'(_gen_cons':id'4(_n24), _gen_cons':id'4(_n24)) → _gen_cons':id'4(_n24), rt ∈ Ω(1 + n24)