---

Step * of Lemma not-Sierpinski-top

∀[x:Sierpinski]. ((¬(x = ⊤ ∈ Sierpinski)) ⇒ (x = ⊥ ∈ Sierpinski))
BY
{ TACTIC:(InstLemma `Sierpinski-unequal-1` []
          THEN Auto
          THEN Thin 2
          THEN D 2
          THEN ThinVar `x1'
          THEN EqTypeCD
          THEN Auto
          THEN Ext
          THEN Auto
          THEN RenameVar `n' (-1)
          THEN RepUR ``Sierpinski-bottom`` 0
          THEN AutoBoolCase ⌜x n⌝⋅
          THEN D -4
          THEN EqTypeCD
          THEN Auto) }

1
1. (⊥ = ⊤ ∈ (ℕ ⟶ 𝔹)) ⇒ False
2. x : Base
3. x ∈ ℕ ⟶ 𝔹
4. ⊥ = ⊥ ∈ (ℕ ⟶ 𝔹)
5. n : ℕ
6. ↑(x n)
7. x = ⊥ ∈ (ℕ ⟶ 𝔹)
⊢ ⊤ = ⊥ ∈ (ℕ ⟶ 𝔹)

---

Latex:

---

Latex:
\mforall{}[x:Sierpinski].  ((\mneg{}(x  =  \mtop{}))  {}\mRightarrow{}  (x  =  \mbot{}))


By

---

Latex:
TACTIC:(InstLemma  `Sierpinski-unequal-1`  []
                THEN  Auto
                THEN  Thin  2
                THEN  D  2
                THEN  ThinVar  `x1'
                THEN  EqTypeCD
                THEN  Auto
                THEN  Ext
                THEN  Auto
                THEN  RenameVar  `n'  (-1)
                THEN  RepUR  ``Sierpinski-bottom``  0
                THEN  AutoBoolCase  \mkleeneopen{}x  n\mkleeneclose{}\mcdot{}
                THEN  D  -4
                THEN  EqTypeCD
                THEN  Auto)

---

Home Index