Step * 1 2 1 1 of Lemma fan-implies-nwkl!-using-PFan


1. Fan
2. t : (š”¹ List) āŸ¶ ā„™
3. āˆ€as:š”¹ List. Dec(t as)
4. āˆ€as,bs:š”¹ List.  (as ā‰¤ bs ā‡’ (t bs) ā‡’ (t as))
5. eff-unique(t)
6. āˆ€n:ā„•
     āˆƒk:ā„•
      ((n ā‰¤ k)
      āˆ§ (āˆ€b,c:š”¹ List.
           ((||b|| = k āˆˆ ā„¤) ā‡’ (||c|| = k āˆˆ ā„¤) ā‡’ (t b) ā‡’ (t c) ā‡’ (firstn(n;b) = firstn(n;c) āˆˆ (š”¹ List)))))
7. a : n:ā„• āŸ¶ (š”¹ List)
8. āˆ€n:ā„•. ((||a n|| = n āˆˆ ā„¤) āˆ§ (t (a n)))
9. k0 : n:ā„• āŸ¶ ā„•
10. āˆ€n:ā„•
      ((n ā‰¤ (k0 n))
      āˆ§ (āˆ€b,c:š”¹ List.
           ((||b|| = (k0 n) āˆˆ ā„¤) ā‡’ (||c|| = (k0 n) āˆˆ ā„¤) ā‡’ (t b) ā‡’ (t c) ā‡’ (firstn(n;b) = firstn(n;c) āˆˆ (š”¹ List)))))
11. k : ā„• āŸ¶ ā„¤
12. āˆ€i,j:ā„•.  ((i ā‰¤ j) ā‡’ ((k i) ā‰¤ (k j)))
13. āˆ€n:ā„•. ((k0 n) ā‰¤ (k n))
āŠ¢ āˆƒf:ā„• āŸ¶ š”¹. is-path(t;f)
BY
{ ((Assert āˆ€n:ā„•. (n ā‰¤ (k n)) BY
          (ParallelLast THEN Auto' THEN InstHyp [āŒœnāŒ] (-6)ā‹… THEN Auto'))
   THEN (Assert āˆ€n:ā„•. (0 ā‰¤ (k n)) BY
               (ParallelLast THEN Auto'))
   ) }

1
1. Fan
2. t : (š”¹ List) āŸ¶ ā„™
3. āˆ€as:š”¹ List. Dec(t as)
4. āˆ€as,bs:š”¹ List.  (as ā‰¤ bs ā‡’ (t bs) ā‡’ (t as))
5. eff-unique(t)
6. āˆ€n:ā„•
     āˆƒk:ā„•
      ((n ā‰¤ k)
      āˆ§ (āˆ€b,c:š”¹ List.
           ((||b|| = k āˆˆ ā„¤) ā‡’ (||c|| = k āˆˆ ā„¤) ā‡’ (t b) ā‡’ (t c) ā‡’ (firstn(n;b) = firstn(n;c) āˆˆ (š”¹ List)))))
7. a : n:ā„• āŸ¶ (š”¹ List)
8. āˆ€n:ā„•. ((||a n|| = n āˆˆ ā„¤) āˆ§ (t (a n)))
9. k0 : n:ā„• āŸ¶ ā„•
10. āˆ€n:ā„•
      ((n ā‰¤ (k0 n))
      āˆ§ (āˆ€b,c:š”¹ List.
           ((||b|| = (k0 n) āˆˆ ā„¤) ā‡’ (||c|| = (k0 n) āˆˆ ā„¤) ā‡’ (t b) ā‡’ (t c) ā‡’ (firstn(n;b) = firstn(n;c) āˆˆ (š”¹ List)))))
11. k : ā„• āŸ¶ ā„¤
12. āˆ€i,j:ā„•.  ((i ā‰¤ j) ā‡’ ((k i) ā‰¤ (k j)))
13. āˆ€n:ā„•. ((k0 n) ā‰¤ (k n))
14. āˆ€n:ā„•. (n ā‰¤ (k n))
15. āˆ€n:ā„•. (0 ā‰¤ (k n))
āŠ¢ āˆƒf:ā„• āŸ¶ š”¹. is-path(t;f)

Latex:

Latex:

1.  Fan
2.  t  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}as:\mBbbB{}  List.  Dec(t  as)
4.  \mforall{}as,bs:\mBbbB{}  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (t  bs)  {}\mRightarrow{}  (t  as))
5.  eff-unique(t)
6.  \mforall{}n:\mBbbN{}
          \mexists{}k:\mBbbN{}
            ((n  \mleq{}  k)
            \mwedge{}  (\mforall{}b,c:\mBbbB{}  List.
                      ((||b||  =  k)  {}\mRightarrow{}  (||c||  =  k)  {}\mRightarrow{}  (t  b)  {}\mRightarrow{}  (t  c)  {}\mRightarrow{}  (firstn(n;b)  =  firstn(n;c)))))
7.  a  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  List)
8.  \mforall{}n:\mBbbN{}.  ((||a  n||  =  n)  \mwedge{}  (t  (a  n)))
9.  k0  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
10.  \mforall{}n:\mBbbN{}
            ((n  \mleq{}  (k0  n))
            \mwedge{}  (\mforall{}b,c:\mBbbB{}  List.
                      ((||b||  =  (k0  n))  {}\mRightarrow{}  (||c||  =  (k0  n))  {}\mRightarrow{}  (t  b)  {}\mRightarrow{}  (t  c)  {}\mRightarrow{}  (firstn(n;b)  =  firstn(n;c)))))
11.  k  :  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
12.  \mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  ((k  i)  \mleq{}  (k  j)))
13.  \mforall{}n:\mBbbN{}.  ((k0  n)  \mleq{}  (k  n))
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  is-path(t;f)


By

Latex:
((Assert  \mforall{}n:\mBbbN{}.  (n  \mleq{}  (k  n))  BY
                (ParallelLast  THEN  Auto'  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto'))
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (0  \mleq{}  (k  n))  BY
                          (ParallelLast  THEN  Auto'))
  )



Home Index