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