---

Step * 1 1 of Lemma pi-rank-choices_wf


1. compList : (pi_prefix() × pi_term()) List
2. ¬(0 = ||compList|| ∈ ℤ)
⊢ (∃b∈compList. 0 ≤ pi-rank(snd(b)))
BY
{ (D 1 THEN All Reduce THEN Auto) }

1
1. u : pi_prefix() × pi_term()
2. v : (pi_prefix() × pi_term()) List
3. ¬(0 = (||v|| + 1) ∈ ℤ)
⊢ (∃b∈[u / v]. 0 ≤ pi-rank(snd(b)))

---

Latex:

---

Latex:

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


By

---

Latex:
(D  1  THEN  All  Reduce  THEN  Auto)

---

Home Index