---

Step * of Lemma sp-lub_wf1

∀[B:f,g:ℕ ⟶ ℕ ⟶ 𝔹//fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)]. (lub(n.B[n]) ∈ Sierpinski)
BY
{ ((Assert EquivRel(ℕ ⟶ ℕ ⟶ 𝔹;f,g.fun-equiv(ℕ;a,b.↓a = ⊥ ∈ (ℕ ⟶ 𝔹) ⇐⇒ b = ⊥ ∈ (ℕ ⟶ 𝔹);f;g)) BY
          (BLemma `fun-equiv-rel` THEN Auto THEN BLemma `equiv_rel_squash`⋅ THEN Auto))
   THEN Auto
   THEN Unfold `Sierpinski` 0
   THEN D 2
   THEN Unfold `sp-lub` 0
   THEN EqTypeCD
   THEN Auto
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConcl ⌜B = A1 ∈ (ℕ ⟶ ℕ ⟶ 𝔹)⌝⋅ THENA Auto)
   THEN (GenConcl ⌜B1 = A2 ∈ (ℕ ⟶ ℕ ⟶ 𝔹)⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN Unfold `fun-equiv` -2
   THEN All (\h. TACTIC:((RWO "equal-Sierpinski-bottom" h THENA Auto)
                         THEN Reduce h
                         THEN (RWW "assert-b-exists" h THENA Auto)))⋅
   THEN (Assert ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n))) BY
               (ParallelOp -2 THEN Auto))
   THEN Thin (-3)) }

1
1. A1 : ℕ ⟶ ℕ ⟶ 𝔹@i
2. A2 : ℕ ⟶ ℕ ⟶ 𝔹@i
3. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A1[i] j)
4. ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n)))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[i] j)

2
1. A1 : ℕ ⟶ ℕ ⟶ 𝔹@i
2. A2 : ℕ ⟶ ℕ ⟶ 𝔹@i
3. ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A2[i] j)
4. ∀x:ℕ. (∀n:ℕ. (¬↑(A1 x n)) ⇐⇒ ∀n:ℕ. (¬↑(A2 x n)))
⊢ ∀n:ℕ. (¬↑let i,j = coded-pair(n) in A1[i] j)

---

Latex:

---

Latex:
\mforall{}[B:f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}//fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g)].  (lub(n.B[n])  \mmember{}  Sierpinski)


By

---

Latex:
((Assert  EquivRel(\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{};f,g.fun-equiv(\mBbbN{};a,b.\mdownarrow{}a  =  \mbot{}  \mLeftarrow{}{}\mRightarrow{}  b  =  \mbot{};f;g))  BY
                (BLemma  `fun-equiv-rel`  THEN  Auto  THEN  BLemma  `equiv\_rel\_squash`\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  Unfold  `Sierpinski`  0
  THEN  D  2
  THEN  Unfold  `sp-lub`  0
  THEN  EqTypeCD
  THEN  Auto
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}B  =  A1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}B1  =  A2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  Unfold  `fun-equiv`  -2
  THEN  All  (\mbackslash{}h.  TACTIC:((RWO  "equal-Sierpinski-bottom"  h  THENA  Auto)
                                              THEN  Reduce  h
                                              THEN  (RWW  "assert-b-exists"  h  THENA  Auto)))\mcdot{}
  THEN  (Assert  \mforall{}x:\mBbbN{}.  (\mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A1  x  n))  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  (\mneg{}\muparrow{}(A2  x  n)))  BY
                          (ParallelOp  -2  THEN  Auto))
  THEN  Thin  (-3))

---

Home Index