---

Step * of Lemma pi-rank-choices_wf

∀[compList:(pi_prefix() × pi_term()) List]. (pi-rank-choices(compList) ∈ ℕ)
BY
{ (ProveWfLemma THEN BLemma `imax-list-ub` THEN Auto) }

1
1. compList : (pi_prefix() × pi_term()) List
2. ¬(0 = ||compList|| ∈ ℤ)
⊢ (∃b∈map(λcmp.pi-rank(snd(cmp));compList). 0 ≤ b)

---

Latex:

---

Latex:
\mforall{}[compList:(pi\_prefix()  \mtimes{}  pi\_term())  List].  (pi-rank-choices(compList)  \mmember{}  \mBbbN{})


By

---

Latex:
(ProveWfLemma  THEN  BLemma  `imax-list-ub`  THEN  Auto)

---

Home Index