---

Step * 1 1 1 1 1 1 of Lemma term-ext


1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
4. y2 : (varname() List × coterm(opr)) List
5. inr <y1, y2>  ∈ coterm(opr)
6. (1 + Σ(coterm-size(snd(bt)) | bt ∈ y2))↓
⊢ y2 ∈ (varname() List × term(opr)) List
BY
{ (Thin (-2) THEN ListInd (-2) THEN Reduce 0) }

1
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
⊢ (0 ≤ 0) ⇒ ([] ∈ (varname() List × term(opr)) List)

2
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
4. u : varname() List × coterm(opr)
5. v : (varname() List × coterm(opr)) List
6. (1 + Σ(coterm-size(snd(bt)) | bt ∈ v))↓ ⇒ (v ∈ (varname() List × term(opr)) List)
⊢ (1 + coterm-size(snd(u)) + Σ(coterm-size(snd(bt)) | bt ∈ v))↓ ⇒ ([u / v] ∈ (varname() List × term(opr)) List)

---

Latex:

---

Latex:

1.  opr  :  Type
2.  coterm(opr)  \mequiv{}  coterm-fun(opr;coterm(opr))
3.  y1  :  opr
4.  y2  :  (varname()  List  \mtimes{}  coterm(opr))  List
5.  inr  <y1,  y2>    \mmember{}  coterm(opr)
6.  (1  +  \mSigma{}(coterm-size(snd(bt))  |  bt  \mmember{}  y2))\mdownarrow{}
\mvdash{}  y2  \mmember{}  (varname()  List  \mtimes{}  term(opr))  List


By

---

Latex:
(Thin  (-2)  THEN  ListInd  (-2)  THEN  Reduce  0)

---

Home Index