---

Step * 1 of Lemma not_has-value_decidable_on_base_quot_true


1. magic : ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓))
⊢ False
BY
{ TACTIC:((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) BY
                 Auto)
          THEN Reduce (-1)
          THEN MoveToConcl (-1)
          THEN Fold `not` 0
          THEN Assert ⌜(λx.x)↓⌝⋅
          THEN Try (Complete ((RepUR ``has-value true member`` 0 THEN Auto)))) }

1
1. magic : ∀t:Base. ⇃((t)↓ ∨ (¬(t)↓))
2. (λx.x)↓
⊢ ¬(case magic ⊥ of inl(a) => ⊥ | inr(b) => λx.x ≤ case magic (λx.x) of inl(a) => ⊥ | inr(b) => λx.x)

---

Latex:

---

Latex:

1.  magic  :  \mforall{}t:Base.  \00D9((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))
\mvdash{}  False


By

---

Latex:
TACTIC:((Assert  (\mlambda{}n.case  magic  n  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x)  \mbot{}  \mleq{}  (\mlambda{}n.case  magic  n
                                                                                                                                                      of  inl(a)  =>
                                                                                                                                                      \mbot{}
                                                                                                                                                      |  inr(b)  =>
                                                                                                                                                      \mlambda{}x.x) 
                                                                                                                                            (\mlambda{}x.x)  BY
                              Auto)
                THEN  Reduce  (-1)
                THEN  MoveToConcl  (-1)
                THEN  Fold  `not`  0
                THEN  Assert  \mkleeneopen{}(\mlambda{}x.x)\mdownarrow{}\mkleeneclose{}\mcdot{}
                THEN  Try  (Complete  ((RepUR  ``has-value  true  member``  0  THEN  Auto))))

---

Home Index