---

Step * 1 1 1 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)
6. (⊥ = ⊤ ∈ Sierpinski) ⇐ ∃x:ℕ. g x = tt
7. (f (λp.if g (fst(p)) then ⊤ else ⊥ fi ) ⋅) = ⊥ ∈ Sierpinski
⊢ False
BY
{ TACTIC:(D 2 THEN Auto) }

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

---

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


By

---

Latex:
TACTIC:(D  2  THEN  Auto)

---

Home Index