---

Step * 1 of Lemma nat-strong-overt-implies-Markov


1. g : ℕ ⟶ 𝔹@i
2. ¬(∀n:ℕ. g n = ff)
3. f : ((ℕ × Unit) ⟶ Sierpinski) ⟶ Unit ⟶ Sierpinski@i'
4. ∀A:(ℕ × Unit) ⟶ Sierpinski. ∀y:Unit.  ((f A y) = ⊤ ∈ Sierpinski ⇐⇒ ∃x:ℕ. ((A <x, y>) = ⊤ ∈ Sierpinski))
⊢ ∃n:ℕ. g n = tt
BY
{ TACTIC:((InstHyp [⌜λp.if g (fst(p)) then ⊤ else ⊥ fi ⌝;⌜⋅⌝] (-1)⋅ THENA Auto) THEN Reduce (-1)) }

1
1. g : ℕ ⟶ 𝔹@i
2. ¬(∀n:ℕ. g n = ff)
3. f : ((ℕ × Unit) ⟶ Sierpinski) ⟶ Unit ⟶ Sierpinski@i'
4. ∀A:(ℕ × Unit) ⟶ Sierpinski. ∀y:Unit.  ((f A y) = ⊤ ∈ Sierpinski ⇐⇒ ∃x:ℕ. ((A <x, y>) = ⊤ ∈ Sierpinski))
5. (f (λp.if g (fst(p)) then ⊤ else ⊥ fi ) ⋅) = ⊤ ∈ Sierpinski ⇐⇒ ∃x:ℕ. (if g x then ⊤ else ⊥ fi  = ⊤ ∈ Sierpinski)
⊢ ∃n:ℕ. g n = tt

---

Latex:

---

Latex:

1.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mneg{}(\mforall{}n:\mBbbN{}.  g  n  =  ff)
3.  f  :  ((\mBbbN{}  \mtimes{}  Unit)  {}\mrightarrow{}  Sierpinski)  {}\mrightarrow{}  Unit  {}\mrightarrow{}  Sierpinski@i'
4.  \mforall{}A:(\mBbbN{}  \mtimes{}  Unit)  {}\mrightarrow{}  Sierpinski.  \mforall{}y:Unit.    ((f  A  y)  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\mBbbN{}.  ((A  <x,  y>)  =  \mtop{}))
\mvdash{}  \mexists{}n:\mBbbN{}.  g  n  =  tt


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}\mlambda{}p.if  g  (fst(p))  then  \mtop{}  else  \mbot{}  fi  \mkleeneclose{};\mkleeneopen{}\mcdot{}\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1))

---

Home Index