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))
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))
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)