---

Step * 1 1 2 1 of Lemma fan-theorem


1. X : (𝔹 List) ⟶ ℙ
2. bar : tbar(𝔹;X)@i
3. d : Decidable(X)@i
4. k : ℕ
5. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))
6. f : ℕ ⟶ 𝔹@i
7. ¬¬(∃n:ℕk. (X map(f;upto(n))))
⊢ outl(int_seg_decide(λn.(d map(f;upto(n)));0;k)) ∈ ∃n:ℕk. (X map(f;upto(n)))
BY
{ ((InstLemma `int_seg_decide_wf` [⌜parm{i}⌝;⌜0⌝;⌜k⌝;⌜λn.(X map(f;upto(n)))⌝;⌜λn.(d map(f;upto(n)))⌝]⋅
    THENA Try (Complete (Auto))
    )
   THEN RepUR ``so_apply`` (-1)
   THEN GenConclAtAddr [2;1]
   THEN D (-2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
2.  bar  :  tbar(\mBbbB{};X)@i
3.  d  :  Decidable(X)@i
4.  k  :  \mBbbN{}
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  (X  map(f;upto(n)))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
7.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}k.  (X  map(f;upto(n))))
\mvdash{}  outl(int\_seg\_decide(\mlambda{}n.(d  map(f;upto(n)));0;k))  \mmember{}  \mexists{}n:\mBbbN{}k.  (X  map(f;upto(n)))


By

---

Latex:
((InstLemma  `int\_seg\_decide\_wf`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(X  map(f;upto(n)))\mkleeneclose{};\mkleeneopen{}\mlambda{}n.(d  map(f;upto(n)))\mkleeneclose{}]\mcdot{}
    THENA  Try  (Complete  (Auto))
    )
  THEN  RepUR  ``so\_apply``  (-1)
  THEN  GenConclAtAddr  [2;1]
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index