---

Step * 1 of Lemma not_has-value_decidable_on_base


1. magic : ∀t:Base. ((t)↓ ∨ (¬(t)↓))@i
⊢ False
BY
{ ((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)↓))@i
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.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))@i
\mvdash{}  False


By

---

Latex:
((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