---

Step * 2 2 2 1 of Lemma term-ext


1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
4. y2 : (varname() List × term(opr)) List
⊢ (1 + Σ(coterm-size(snd(bt)) | bt ∈ y2))↓
BY
{ (Unfold `lsum` 0 THEN (Unfold `l_sum` 0 THEN ListInd (-1)) THEN Reduce 0) }

1
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
⊢ 0 ≤ 0

2
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y1 : opr
4. u : varname() List × term(opr)
5. v : (varname() List × term(opr)) List
6. (1 + reduce(λx,y. (x + y);0;map(λbt.coterm-size(snd(bt));v)))↓
⊢ (1 + coterm-size(snd(u)) + reduce(λx,y. (x + y);0;map(λbt.coterm-size(snd(bt));v)))↓

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `lsum`  0  THEN  (Unfold  `l\_sum`  0  THEN  ListInd  (-1))  THEN  Reduce  0)

---

Home Index