---

Step * 1 of Lemma ni-min-assoc


1. x : ℕ∞
2. y : ℕ∞
3. z : ℕ∞
4. ni-min(ni-min(x;y);z) = ni-min(ni-min(x;y);z) ∈ (ℕ ⟶ 𝔹)
⊢ ni-min(ni-min(x;y);z) = ni-min(x;ni-min(y;z)) ∈ (ℕ ⟶ 𝔹)
BY
{ (Ext⋅ THEN Auto THEN RenameVar `i' (-1) THEN RepUR ``ni-min`` 0 THEN AutoBoolCase ⌜x i⌝⋅) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  y  :  \mBbbN{}\minfty{}
3.  z  :  \mBbbN{}\minfty{}
4.  ni-min(ni-min(x;y);z)  =  ni-min(ni-min(x;y);z)
\mvdash{}  ni-min(ni-min(x;y);z)  =  ni-min(x;ni-min(y;z))


By

---

Latex:
(Ext\mcdot{}  THEN  Auto  THEN  RenameVar  `i'  (-1)  THEN  RepUR  ``ni-min``  0  THEN  AutoBoolCase  \mkleeneopen{}x  i\mkleeneclose{}\mcdot{})

---

Home Index