---

Step * 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:ℕ. (if g x then ⊤ else ⊥ fi  = ⊤ ∈ Sierpinski)
⊢ ∃n:ℕ. g n = tt
BY
{ TACTIC:(Assert ∃n:ℕ. (if g n then ⊤ else ⊥ fi  = ⊤ ∈ Sierpinski) ⇐⇒ ∃n:ℕ. g n = tt BY
                (Auto THEN ParallelLast THEN InstLemma `Sierpinski-unequal` [] THEN AutoBoolCase ⌜g n⌝⋅)) }

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)
6. ∃n:ℕ. (if g n then ⊤ else ⊥ fi  = ⊤ ∈ Sierpinski) ⇐⇒ ∃n:ℕ. g n = tt
⊢ ∃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{}))
5.  (f  (\mlambda{}p.if  g  (fst(p))  then  \mtop{}  else  \mbot{}  fi  )  \mcdot{})  =  \mtop{}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:\mBbbN{}.  (if  g  x  then  \mtop{}  else  \mbot{}  fi    =  \mtop{})
\mvdash{}  \mexists{}n:\mBbbN{}.  g  n  =  tt


By

---

Latex:
TACTIC:(Assert  \mexists{}n:\mBbbN{}.  (if  g  n  then  \mtop{}  else  \mbot{}  fi    =  \mtop{})  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  g  n  =  tt  BY
                            (Auto
                              THEN  ParallelLast
                              THEN  InstLemma  `Sierpinski-unequal`  []
                              THEN  AutoBoolCase  \mkleeneopen{}g  n\mkleeneclose{}\mcdot{}))

---

Home Index