---

Step * 2 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)))} )
⊢ <0, u> ∈ i:ℕ1 × {x:ℤ| (x = [u][i] ∈ ℤ) ∧ (∀z@0:ℤ. ((z@0 ∈ [u]) ⇒ (x ≤ z@0)))} 
BY
{ TACTIC:(MemCD THEN Reduce 0 THEN Try (MemTypeCD) THEN Auto) }

1
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

---

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)))\}  )
\mvdash{}  ɘ,  u>  \mmember{}  i:\mBbbN{}1  \mtimes{}  \{x:\mBbbZ{}|  (x  =  [u][i])  \mwedge{}  (\mforall{}z@0:\mBbbZ{}.  ((z@0  \mmember{}  [u])  {}\mRightarrow{}  (x  \mleq{}  z@0)))\} 


By

---

Latex:
TACTIC:(MemCD  THEN  Reduce  0  THEN  Try  (MemTypeCD)  THEN  Auto)

---

Home Index