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


1. Fan
2. (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹List) ⟶ ℙ.
     ((∀bc:(𝔹 × 𝔹List. Dec(ss bc))
      (∀bc,bc':(𝔹 × 𝔹List.  (bc ≤ bc'  (ss bc)  (ss bc')))
      (∀gh:ℕ ⟶ (𝔹 × 𝔹)
           ((¬(map(λi.(fst((gh i)));upto(n)) map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
            (∃m:ℕ(ss map(gh;upto(m))))))
      (∃k:ℕ
          ∀gh:ℕ ⟶ (𝔹 × 𝔹)
            ((¬(map(λi.(fst((gh i)));upto(n)) map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))  (ss map(gh;upto(k))))))
7. : ℕ
8. ∀ss:((𝔹 × 𝔹List) ⟶ ℙ
     ((∀bc:(𝔹 × 𝔹List. Dec(ss bc))
      (∀bc,bc':(𝔹 × 𝔹List.  (bc ≤ bc'  (ss bc)  (ss bc')))
      (∀gh:ℕ ⟶ (𝔹 × 𝔹)
           ((¬(map(λi.(fst((gh i)));upto(n)) map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
            (∃m:ℕ(ss map(gh;upto(m))))))
      (∃k:ℕ
          ∀gh:ℕ ⟶ (𝔹 × 𝔹)
            ((¬(map(λi.(fst((gh i)));upto(n)) map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))  (ss map(gh;upto(k))))))
9. bc (𝔹 × 𝔹List
10. bc' (𝔹 × 𝔹List
11. bc ≤ bc'
12. map(λp.(snd(p));bc')
13. map(λp.(fst(p));bc')
⊢ map(λp.(fst(p));bc)
BY
(Assert ⌜map(λp.(fst(p));bc) ≤ map(λp.(fst(p));bc')⌝⋅
   THEN Try (((D THEN FHyp [-1;-2]) THEN Auto))
   THEN BLemma `iseg-map`
   THEN Auto)⋅ }


Latex:


Latex:

1.  Fan
2.  t  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}as:\mBbbB{}  List.  Dec(t  as)
4.  infinite-tree(t)
5.  eff-unique(t)
6.  \mforall{}n:\mBbbN{}.  \mforall{}ss:((\mBbbB{}  \mtimes{}  \mBbbB{})  List)  {}\mrightarrow{}  \mBbbP{}.
          ((\mforall{}bc:(\mBbbB{}  \mtimes{}  \mBbbB{})  List.  Dec(ss  bc))
          {}\mRightarrow{}  (\mforall{}bc,bc':(\mBbbB{}  \mtimes{}  \mBbbB{})  List.    (bc  \mleq{}  bc'  {}\mRightarrow{}  (ss  bc)  {}\mRightarrow{}  (ss  bc')))
          {}\mRightarrow{}  (\mforall{}gh:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  \mtimes{}  \mBbbB{})
                      ((\mneg{}(map(\mlambda{}i.(fst((gh  i)));upto(n))  =  map(\mlambda{}i.(snd((gh  i)));upto(n))))
                      {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  (ss  map(gh;upto(m))))))
          {}\mRightarrow{}  (\mexists{}k:\mBbbN{}
                    \mforall{}gh:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  \mtimes{}  \mBbbB{})
                        ((\mneg{}(map(\mlambda{}i.(fst((gh  i)));upto(n))  =  map(\mlambda{}i.(snd((gh  i)));upto(n))))
                        {}\mRightarrow{}  (ss  map(gh;upto(k))))))
7.  n  :  \mBbbN{}
8.  \mforall{}ss:((\mBbbB{}  \mtimes{}  \mBbbB{})  List)  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}bc:(\mBbbB{}  \mtimes{}  \mBbbB{})  List.  Dec(ss  bc))
          {}\mRightarrow{}  (\mforall{}bc,bc':(\mBbbB{}  \mtimes{}  \mBbbB{})  List.    (bc  \mleq{}  bc'  {}\mRightarrow{}  (ss  bc)  {}\mRightarrow{}  (ss  bc')))
          {}\mRightarrow{}  (\mforall{}gh:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  \mtimes{}  \mBbbB{})
                      ((\mneg{}(map(\mlambda{}i.(fst((gh  i)));upto(n))  =  map(\mlambda{}i.(snd((gh  i)));upto(n))))
                      {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  (ss  map(gh;upto(m))))))
          {}\mRightarrow{}  (\mexists{}k:\mBbbN{}
                    \mforall{}gh:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  \mtimes{}  \mBbbB{})
                        ((\mneg{}(map(\mlambda{}i.(fst((gh  i)));upto(n))  =  map(\mlambda{}i.(snd((gh  i)));upto(n))))
                        {}\mRightarrow{}  (ss  map(gh;upto(k))))))
9.  bc  :  (\mBbbB{}  \mtimes{}  \mBbbB{})  List
10.  bc'  :  (\mBbbB{}  \mtimes{}  \mBbbB{})  List
11.  bc  \mleq{}  bc'
12.  t  map(\mlambda{}p.(snd(p));bc')
13.  t  map(\mlambda{}p.(fst(p));bc')
\mvdash{}  t  map(\mlambda{}p.(fst(p));bc)


By


Latex:
(Assert  \mkleeneopen{}map(\mlambda{}p.(fst(p));bc)  \mleq{}  map(\mlambda{}p.(fst(p));bc')\mkleeneclose{}\mcdot{}
  THEN  Try  (((D  4  THEN  FHyp  4  [-1;-2])  THEN  Auto))
  THEN  BLemma  `iseg-map`
  THEN  Auto)\mcdot{}




Home Index