Step
*
of Lemma
ni-min-assoc
∀[x,y,z:ℕ∞].  (ni-min(ni-min(x;y);z) = ni-min(x;ni-min(y;z)) ∈ ℕ∞)
BY
{ (Auto
   THEN (Assert ni-min(ni-min(x;y);z) ∈ ℕ∞ BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN EqTypeCD
   THEN Auto
   THEN Thin (-1)) }
1
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)) ∈ (ℕ ⟶ 𝔹)
Latex:
Latex:
\mforall{}[x,y,z:\mBbbN{}\minfty{}].    (ni-min(ni-min(x;y);z)  =  ni-min(x;ni-min(y;z)))
By
Latex:
(Auto
  THEN  (Assert  ni-min(ni-min(x;y);z)  \mmember{}  \mBbbN{}\minfty{}  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Thin  (-1))
Home
Index