---

Step * 2 2 of Lemma term-ext

.....set predicate..... 
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. x : coterm-fun(opr;term(opr))
⊢ (coterm-size(x))↓
BY
{ D -1 }

1
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. x1 : {v:varname()| ¬(v = nullvar() ∈ varname())} 
⊢ (coterm-size(inl x1))↓

2
1. opr : Type
2. coterm(opr) ≡ coterm-fun(opr;coterm(opr))
3. y : opr × ((varname() List × term(opr)) List)
⊢ (coterm-size(inr y ))↓

---

Latex:

---

Latex:
.....set  predicate..... 
1.  opr  :  Type
2.  coterm(opr)  \mequiv{}  coterm-fun(opr;coterm(opr))
3.  x  :  coterm-fun(opr;term(opr))
\mvdash{}  (coterm-size(x))\mdownarrow{}


By

---

Latex:
D  -1

---

Home Index