---

Step * 1 of Lemma pi-rank-choices_wf


1. compList : (pi_prefix() × pi_term()) List
2. ¬(0 = ||compList|| ∈ ℤ)
⊢ (∃b∈map(λcmp.pi-rank(snd(cmp));compList). 0 ≤ b)
BY
{ ((BLemma `l_exists_map` THENM Reduce 0) THEN Auto)⋅ }

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

---

Latex:

---

Latex:

1.  compList  :  (pi\_prefix()  \mtimes{}  pi\_term())  List
2.  \mneg{}(0  =  ||compList||)
\mvdash{}  (\mexists{}b\mmember{}map(\mlambda{}cmp.pi-rank(snd(cmp));compList).  0  \mleq{}  b)


By

---

Latex:
((BLemma  `l\_exists\_map`  THENM  Reduce  0)  THEN  Auto)\mcdot{}

---

Home Index