Step
*
of Lemma
index-of-min_wf
∀[zs:ℤ List+]. (index-of-min(zs) ∈ {i:ℕ||zs||| ∀x:ℤ. ((x ∈ zs)
⇒ (zs[i] ≤ x))} )
BY
{ ProveWfLemma }
Latex:
Latex:
\mforall{}[zs:\mBbbZ{} List\msupplus{}]. (index-of-min(zs) \mmember{} \{i:\mBbbN{}||zs||| \mforall{}x:\mBbbZ{}. ((x \mmember{} zs) {}\mRightarrow{} (zs[i] \mleq{} x))\} )
By
Latex:
ProveWfLemma
Home
Index