---

Step * 1 1 of Lemma not-has-value-decidable-quot

.....assertion..... 
1. E : (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ ℙ
2. EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.E[f;g])
3. magic : ∀x:Base. ((x)↓ ∨ (¬(x)↓))@i
4. m1 : ∀x:Base. ((x)↓ ∨ (¬(x)↓))@i
5. E[magic;m1]@i
⊢ False
BY
{ (InstLemma `not_has-value_decidable_on_base` [] THEN Trivial) }

---

Latex:

---

Latex:
.....assertion..... 
1.  E  :  (\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  (\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  \mBbbP{}
2.  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.E[f;g])
3.  magic  :  \mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))@i
4.  m1  :  \mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))@i
5.  E[magic;m1]@i
\mvdash{}  False


By

---

Latex:
(InstLemma  `not\_has-value\_decidable\_on\_base`  []  THEN  Trivial)

---

Home Index