---

Step * 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. (coterm-size(inr <y1, y2> ))↓
⊢ y2 ∈ (varname() List × term(opr)) List
BY
{ (Unfold `coterm-size` -1 THEN RW  (SweepUpC UnrollRecursionC) (-1) THEN Reduce -1 THEN Fold `coterm-size` (-1)) }

1
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

---

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.  (coterm-size(inr  <y1,  y2>  ))\mdownarrow{}
\mvdash{}  y2  \mmember{}  (varname()  List  \mtimes{}  term(opr))  List


By

---

Latex:
(Unfold  `coterm-size`  -1
  THEN  RW    (SweepUpC  UnrollRecursionC)  (-1)
  THEN  Reduce  -1
  THEN  Fold  `coterm-size`  (-1))

---

Home Index