Step
*
of Lemma
ni-max-com
∀[x,y:ℕ∞]. (ni-max(x;y) = ni-max(y;x) ∈ ℕ∞)
BY
{ (Auto
THEN (Assert ni-max(x;y) ∈ ℕ∞ BY
Auto)
THEN (MemTypeHD (-1) THENA Auto)
THEN EqTypeCD
THEN Auto
THEN Thin (-1)) }
1
1. x : ℕ∞
2. y : ℕ∞
3. ni-max(x;y) = ni-max(x;y) ∈ (ℕ ⟶ 𝔹)
⊢ ni-max(x;y) = ni-max(y;x) ∈ (ℕ ⟶ 𝔹)
Latex:
Latex:
\mforall{}[x,y:\mBbbN{}\minfty{}]. (ni-max(x;y) = ni-max(y;x))
By
Latex:
(Auto
THEN (Assert ni-max(x;y) \mmember{} \mBbbN{}\minfty{} BY
Auto)
THEN (MemTypeHD (-1) THENA Auto)
THEN EqTypeCD
THEN Auto
THEN Thin (-1))
Home
Index