---

Step * of Lemma C_TYPE-rank_wf

∀[ctyp:C_TYPE()]. (C_TYPE-rank(ctyp) ∈ ℕ)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
.....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||)

---

Latex:

---

Latex:
\mforall{}[ctyp:C\_TYPE()].  (C\_TYPE-rank(ctyp)  \mmember{}  \mBbbN{})


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index