---

Step * 2 2 1 2 1 1 1 4 of Lemma twkl!-implies-dfan


1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ.  ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)}  ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} 
      (||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} .  ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T.  Dec(a = b ∈ T)
18. ∃f:{ℕ ⟶ T| is-path(λb.((upwd-closure(T;s) b)
                           ⇒ (tree-big(T;upwd-closure(T;s);||b||)
                              ∧ let as = a ||b|| in
                                    b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List)));f)}
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))
BY
{ ((D -1 THEN RepUR ``is-path`` -1)
   THEN (InstHyp [⌜f⌝] 7⋅ THENA Auto)
   THEN ExRepD
   THEN With ⌜n + 1⌝ (D 0)⋅
   THEN Auto
   THEN (Unhide THENA Auto)
   THEN (InstHyp [⌜n⌝] (-4)⋅
         THENA (Auto
                THEN RepUR ``upwd-closure`` 0
                THEN With ⌜map(f;upto(n))⌝ (D 0)⋅
                THEN Auto
                THEN BLemma `iseg_weakening`
                THEN Auto)
         )⋅)⋅ }

1
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ.  ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)}  ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} 
      (||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} .  ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T.  Dec(a = b ∈ T)
18. f : ℕ ⟶ T
19. ∀n:ℕ
      ((upwd-closure(T;s) map(f;upto(n)))
      ⇒ (tree-big(T;upwd-closure(T;s);||map(f;upto(n))||)
         ∧ let as = a ||map(f;upto(n))|| in
               map(f;upto(n)) = (as @ map(λi.t;upto(||map(f;upto(n))|| - ||as||))) ∈ (T List)))
20. n : ℕ
21. s map(f;upto(n))
22. f1 : ℕ ⟶ T
23. tree-big(T;upwd-closure(T;s);||map(f;upto(n))||)
∧ let as = a ||map(f;upto(n))|| in
      map(f;upto(n)) = (as @ map(λi.t;upto(||map(f;upto(n))|| - ||as||))) ∈ (T List)
⊢ ∃n:ℕn + 1. (s map(f1;upto(n)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  k  :  \mBbbN{}
3.  T  \msim{}  \mBbbN{}k
4.  \mforall{}A:\{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
          (Decidable(A)  {}\mRightarrow{}  eff-unique-path(T;A)  {}\mRightarrow{}  (\mexists{}f:\{\mBbbN{}  {}\mrightarrow{}  T|  is-path(A;f)\}))
5.  s  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}t:T  List.  Dec(s  t)
7.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}.  (s  map(f;upto(n)))
8.  \mneg{}(s  [])
9.  \mforall{}a,b:\mBbbN{}.    ((a  \mleq{}  b)  {}\mRightarrow{}  tree-big(T;upwd-closure(T;s);a)  {}\mRightarrow{}  tree-big(T;upwd-closure(T;s);b))
10.  a  :  \{n:\mBbbN{}|  tree-big(T;upwd-closure(T;s);n)\}    {}\mrightarrow{}  (T  List)
11.  \mforall{}n:\{n:\mBbbN{}|  tree-big(T;upwd-closure(T;s);n)\} 
            (||a  n||  <  n  \mwedge{}  (\mneg{}(upwd-closure(T;s)  (a  n)))  \mwedge{}  tree-big(T;upwd-closure(T;s);||a  n||  +  1))
12.  \mforall{}n,m:\{n:\mBbbN{}|  tree-big(T;upwd-closure(T;s);n)\}  .    ((a  n)  =  (a  m))
13.  \mneg{}(k  =  0)
14.  t  :  T
15.  Decidable(upwd-closure(T;s))
16.  \mforall{}n:\mBbbN{}.  Dec(tree-big(T;upwd-closure(T;s);n))
17.  \mforall{}a,b:T.    Dec(a  =  b)
18.  \mexists{}f:\{\mBbbN{}  {}\mrightarrow{}  T|  is-path(\mlambda{}b.((upwd-closure(T;s)  b)
                                                      {}\mRightarrow{}  (tree-big(T;upwd-closure(T;s);||b||)
                                                            \mwedge{}  let  as  =  a  ||b||  in
                                                                        b  =  (as  @  map(\mlambda{}i.t;upto(||b||  -  ||as||)))));f)\}
\mvdash{}  \mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}k.  (s  map(f;upto(n)))


By

---

Latex:
((D  -1  THEN  RepUR  ``is-path``  -1)
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  7\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  With  \mkleeneopen{}n  +  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Unhide  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-4)\mcdot{}
              THENA  (Auto
                            THEN  RepUR  ``upwd-closure``  0
                            THEN  With  \mkleeneopen{}map(f;upto(n))\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto
                            THEN  BLemma  `iseg\_weakening`
                            THEN  Auto)
              )\mcdot{})\mcdot{}

---

Home Index