---

Step * 1 of Lemma C_TYPE-rank_wf

.....set predicate..... 
1. ctyp : C_TYPE()
2. fields : (Atom × C_TYPE()) List@i
3. recL : (∀u∈fields.let u1,u2 = u 
                     in ℕ)@i
⊢ 0 ≤ Σ(recL j | j < ||fields||)
BY
{ CondAuto1 }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  ctyp  :  C\_TYPE()
2.  fields  :  (Atom  \mtimes{}  C\_TYPE())  List@i
3.  recL  :  (\mforall{}u\mmember{}fields.let  u1,u2  =  u 
                                          in  \mBbbN{})@i
\mvdash{}  0  \mleq{}  \mSigma{}(recL  j  |  j  <  ||fields||)


By

---

Latex:
CondAuto1

---

Home Index