---

Step * 2 1 1 1 1 2 1 of Lemma bar-separation-implies-twkl!


1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. eff-unique-path(T;A)
10. ∀L:T List
      ((¬↑null(L))
      ⇒ (∀s:T List. ∃t:{t:T| (t ∈ L)} . ∀t':{t:T| (t ∈ L)} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))))
⊢ ∀s:T List. ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
BY
{ ((InstLemma `finite-type-iff-list` [⌜T⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN (D -2
         THENA (D 2
                THEN With ⌜size⌝ (D 0)⋅
                THEN Auto
                THEN (FLemma `equipollent_inversion` [3] THENM (RepeatFor 2 (D (-1)) THEN With ⌜f⌝ (D 0)⋅ THEN Auto))
                THEN Auto)
         )
   THEN D (-1)
   THEN (With ⌜L⌝ (D (-4))⋅ THENA Auto)
   THEN (D -1 THENM RepeatFor 3 (ParallelLast))) }

1
.....antecedent..... 
1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. eff-unique-path(T;A)
10. finite-type(T) ⇐ ∃L:T List. ∀x:T. (x ∈ L)
11. L : T List
12. ∀x:T. (x ∈ L)
⊢ ¬↑null(L)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size
3.  BarSep(T;T)
4.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
5.  \mneg{}tbar(T;\mneg{}(A))
6.  Decidable(A)
7.  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (A  bs)  {}\mRightarrow{}  (A  as))
8.  T
9.  eff-unique-path(T;A)
10.  \mforall{}L:T  List
            ((\mneg{}\muparrow{}null(L))
            {}\mRightarrow{}  (\mforall{}s:T  List
                        \mexists{}t:\{t:T|  (t  \mmember{}  L)\} 
                          \mforall{}t':\{t:T|  (t  \mmember{}  L)\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))))
\mvdash{}  \mforall{}s:T  List.  \mexists{}t:T.  \mforall{}t':T.  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))


By

---

Latex:
((InstLemma  `finite-type-iff-list`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  (D  -2
              THENA  (D  2
                            THEN  With  \mkleeneopen{}size\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto
                            THEN  (FLemma  `equipollent\_inversion`  [3]
                            THENM  (RepeatFor  2  (D  (-1))  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
                            )
                            THEN  Auto)
              )
  THEN  D  (-1)
  THEN  (With  \mkleeneopen{}L\mkleeneclose{}  (D  (-4))\mcdot{}  THENA  Auto)
  THEN  (D  -1  THENM  RepeatFor  3  (ParallelLast)))

---

Home Index