Step * of Lemma no-limited-omniscience

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

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

2
1. ∀f:ℕ ⟶ 𝔹((∀n:ℕff) ∨ (∃n:ℕtt))
2. : ℕ ⟶ 𝔹
3. ∃n:ℕtt
⊢ Dec(∀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