---

Step * of Lemma no-excluded-middle-quot-true

¬(∀P:ℙ. ⇃(P ∨ (↓¬P)))
BY
{ ((D 0 THENA Auto)
   THEN RenameVar `magic' (-1)
   THEN (Assert ⌜(λn.case magic (n)↓ of inl(a) => ⊥ | inr(b) => λx.x) ⊥ ≤ (λn.case magic (n)↓
                                                                               of inl(a) =>
                                                                               ⊥
                                                                               | inr(b) =>
                                                                               λx.x) 
                                                                          (λx.x)⌝⋅
         THENA (SqLeCD THEN Try (SqLeCD) THEN Auto)
         )
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN Fold `not` 0
   THEN GenConclAtAddr [1;1;1]
   THEN GenConclAtAddr [1;2;1]) }

1
1. magic : ∀P:ℙ. ⇃(P ∨ (↓¬P))
2. v : ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
3. (magic (⊥)↓) = v ∈ ⇃((⊥)↓ ∨ (↓¬(⊥)↓))
4. v1 : ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
5. (magic (0 ≤ 0)) = v1 ∈ ⇃((0 ≤ 0) ∨ (↓¬(0 ≤ 0)))
⊢ ¬(case v of inl(a) => ⊥ | inr(b) => λx.x ≤ case v1 of inl(a) => ⊥ | inr(b) => λx.x)

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\mdownarrow{}\mneg{}P)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  RenameVar  `magic'  (-1)
  THEN  (Assert  \mkleeneopen{}(\mlambda{}n.case  magic  (n)\mdownarrow{}  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x)  \mbot{}  \mleq{}  (\mlambda{}n.case  magic  (n)\mdownarrow{}
                                                                                                                                                          of  inl(a)  =>
                                                                                                                                                          \mbot{}
                                                                                                                                                          |  inr(b)  =>
                                                                                                                                                          \mlambda{}x.x) 
                                                                                                                                                (\mlambda{}x.x)\mkleeneclose{}\mcdot{}
              THENA  (SqLeCD  THEN  Try  (SqLeCD)  THEN  Auto)
              )
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Fold  `not`  0
  THEN  GenConclAtAddr  [1;1;1]
  THEN  GenConclAtAddr  [1;2;1])

---

Home Index