---

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


1. E : (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ ℙ
2. EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.E[f;g])
3. magic : f,g:∀x:Base. ((x)↓ ∨ (¬(x)↓))//E[f;g]@i
⊢ False
BY
{ (UseWitness ⌜Ax⌝⋅ THEN quotD (-1) THEN Assert ⌜False⌝⋅ THEN Auto) }

1
.....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

---

Latex:

---

Latex:

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  :  f,g:\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))//E[f;g]@i
\mvdash{}  False


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  quotD  (-1)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index