---

Step * 1 1 1 of Lemma not_has-value_decidable_on_base


1. magic : ∀t:Base. ((t)↓ ∨ (¬(t)↓))@i
2. (λx.x)↓
3. ¬(⊥)↓
4. ¬(λx.x ≤ ⊥)
⊢ ¬(case magic ⊥ of inl(a) => ⊥ | inr(b) => λx.x ≤ case magic (λx.x) of inl(a) => ⊥ | inr(b) => λx.x)
BY
{ (GenConclAtAddr [1;1;1] THEN GenConclAtAddr [1;2;1] THEN SplitOrHyps THEN Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  magic  :  \mforall{}t:Base.  ((t)\mdownarrow{}  \mvee{}  (\mneg{}(t)\mdownarrow{}))@i
2.  (\mlambda{}x.x)\mdownarrow{}
3.  \mneg{}(\mbot{})\mdownarrow{}
4.  \mneg{}(\mlambda{}x.x  \mleq{}  \mbot{})
\mvdash{}  \mneg{}(case  magic  \mbot{}  of  inl(a)  =>  \mbot{}  |  inr(b)  =>  \mlambda{}x.x  \mleq{}  case  magic  (\mlambda{}x.x)
          of  inl(a)  =>
          \mbot{}
          |  inr(b)  =>
          \mlambda{}x.x)


By

---

Latex:
(GenConclAtAddr  [1;1;1]  THEN  GenConclAtAddr  [1;2;1]  THEN  SplitOrHyps  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index