---

Step * of Lemma no-limited-omniscience

¬LPO
BY
{ (InstLemma `no-weak-limited-omniscience` []
   THEN ParallelLast
   THEN Unfold `limited-omniscience` 1
   THEN ParallelLast
   THEN D -1) }

1
1. ∀f:ℕ ⟶ 𝔹. ((∀n:ℕ. f n = ff) ∨ (∃n:ℕ. f n = tt))
2. f : ℕ ⟶ 𝔹
3. ∀n:ℕ. f n = ff
⊢ Dec(∀n:ℕ. f n = ff)

2
1. ∀f:ℕ ⟶ 𝔹. ((∀n:ℕ. f n = ff) ∨ (∃n:ℕ. f n = tt))
2. f : ℕ ⟶ 𝔹
3. ∃n:ℕ. f n = tt
⊢ Dec(∀n:ℕ. f n = ff)

---

Latex:

---

Latex:
\mneg{}LPO


By

---

Latex:
(InstLemma  `no-weak-limited-omniscience`  []
  THEN  ParallelLast
  THEN  Unfold  `limited-omniscience`  1
  THEN  ParallelLast
  THEN  D  -1)

---

Home Index