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