---

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

¬(∀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 (GenConclAtAddrType ⌜⇃((⊥)↓) ∨ ⇃(¬(⊥)↓)⌝ [1;1;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜⇃((λx.x)↓) ∨ ⇃(¬(λx.x)↓)⌝ [1;2;1]⋅ THENA Auto)
   THEN DProdsAndUnions
   THEN AllReduce
   THEN (D 0 THENA Auto)
   THEN Try ((InstLemma `not_id_sqeq_bottom` [] THEN D (-1) THEN SqequalSqle THEN Complete (Auto)))
   THEN Try ((UseWitness ⌜Ax⌝⋅ THEN  quotD 2 THEN Auto THEN Complete (BotDiv)))
   THEN Try ((UseWitness ⌜Ax⌝⋅ THEN  quotD 4 THEN Auto THEN BotDiv THEN D -2 THEN SqLeCD))) }

---

Latex:

---

Latex:
\mneg{}(\mforall{}P:\mBbbP{}.  \00D9(P  \mvee{}  (\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  (GenConclAtAddrType  \mkleeneopen{}\00D9((\mbot{})\mdownarrow{})  \mvee{}  \00D9(\mneg{}(\mbot{})\mdownarrow{})\mkleeneclose{}  [1;1;1]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\00D9((\mlambda{}x.x)\mdownarrow{})  \mvee{}  \00D9(\mneg{}(\mlambda{}x.x)\mdownarrow{})\mkleeneclose{}  [1;2;1]\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  (D  0  THENA  Auto)
  THEN  Try  ((InstLemma  `not\_id\_sqeq\_bottom`  []  THEN  D  (-1)  THEN  SqequalSqle  THEN  Complete  (Auto)))
  THEN  Try  ((UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN    quotD  2  THEN  Auto  THEN  Complete  (BotDiv)))
  THEN  Try  ((UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN    quotD  4  THEN  Auto  THEN  BotDiv  THEN  D  -2  THEN  SqLeCD)))

---

Home Index