---

Step * 1 1 of Lemma fan_theorem


1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ
2. ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
3. d : ∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])
4. k : ℕ
5. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]
6. K : ℤ
7. K = k ∈ ℤ
8. f : ℕ ⟶ 𝔹
9. ¬¬(∃n:ℕK. X[n;f])
⊢ outl(int_seg_decide(λn.(d n f);0;K)) ∈ ∃n:ℕK. X[n;f]
BY
{ (InstLemma `int_seg_decide_wf` [⌜parm{i}⌝;⌜0⌝;⌜K⌝;⌜λ2n.X[n;f]⌝;⌜λn.(d n f)⌝]⋅
   THEN Auto
   THEN GenConclAtAddr [2;1]⋅
   THEN D (-2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])
3.  d  :  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s])
4.  k  :  \mBbbN{}
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]
6.  K  :  \mBbbZ{}
7.  K  =  k
8.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
9.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}K.  X[n;f])
\mvdash{}  outl(int\_seg\_decide(\mlambda{}n.(d  n  f);0;K))  \mmember{}  \mexists{}n:\mBbbN{}K.  X[n;f]


By

---

Latex:
(InstLemma  `int\_seg\_decide\_wf`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.X[n;f]\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(d  n  f)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  GenConclAtAddr  [2;1]\mcdot{}
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index