---

Step * 2 1 1 1 1 of Lemma index-min_wf


1. u : ℤ
2. 0 < ||[]|| ⇒ (index-min([]) ∈ i:ℕ||[]|| × {x:ℤ| (x = [][i] ∈ ℤ) ∧ (∀z@0:ℤ. ((z@0 ∈ []) ⇒ (x ≤ z@0)))} )
3. u = u ∈ ℤ
4. z@0 : ℤ
5. (z@0 ∈ [u])
⊢ u ≤ z@0
BY
{ TACTIC:(RW ListC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  0  <  ||[]||
{}\mRightarrow{}  (index-min([])  \mmember{}  i:\mBbbN{}||[]||  \mtimes{}  \{x:\mBbbZ{}|  (x  =  [][i])  \mwedge{}  (\mforall{}z@0:\mBbbZ{}.  ((z@0  \mmember{}  [])  {}\mRightarrow{}  (x  \mleq{}  z@0)))\}  )
3.  u  =  u
4.  z@0  :  \mBbbZ{}
5.  (z@0  \mmember{}  [u])
\mvdash{}  u  \mleq{}  z@0


By

---

Latex:
TACTIC:(RW  ListC  (-1)  THEN  Auto)

---

Home Index