---

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

∀[E:(∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ (∀x:Base. ((x)↓ ∨ (¬(x)↓))) ⟶ ℙ]
  ¬(f,g:∀x:Base. ((x)↓ ∨ (¬(x)↓))//E[f;g]) supposing EquivRel(∀x:Base. ((x)↓ ∨ (¬(x)↓));f,g.E[f;g])
BY
{ (Auto THEN (D 0 THENA Auto) THEN RenameVar `magic' (-1)) }

1
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

---

Latex:

---

Latex:
\mforall{}[E:(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  (\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{})))  {}\mrightarrow{}  \mBbbP{}]
    \mneg{}(f,g:\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}))//E[f;g])  supposing  EquivRel(\mforall{}x:Base.  ((x)\mdownarrow{}  \mvee{}  (\mneg{}(x)\mdownarrow{}));f,g.E[f;g])


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  RenameVar  `magic'  (-1))

---

Home Index