---

Step * 1 1 1 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))
5. (f (λp.if g (fst(p)) then ⊤ else ⊥ fi ) ⋅) = ⊤ ∈ Sierpinski ⇐⇒ ∃x:ℕ. g x = tt
⊢ ∃n:ℕ. g n = tt
BY
{ TACTIC:(BHyp -1 THEN BLemma `not-Sierpinski-bottom` THEN Auto) }

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:ℕ. g x = tt)
6. ((f (λp.if g (fst(p)) then ⊤ else ⊥ fi ) ⋅) = ⊤ ∈ Sierpinski) ⇐ ∃x:ℕ. g x = tt
⊢ ¬((f (λp.if g (fst(p)) then ⊤ else ⊥ fi ) ⋅) = ⊥ ∈ Sierpinski)

---

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{}))
5.  (f  (\mlambda{}p.if  g  (fst(p))  then  \mtop{}  else  \mbot{}  fi  )  \mcdot{})  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\mBbbN{}.  g  x  =  tt
\mvdash{}  \mexists{}n:\mBbbN{}.  g  n  =  tt


By

---

Latex:
TACTIC:(BHyp  -1  THEN  BLemma  `not-Sierpinski-bottom`  THEN  Auto)

---

Home Index