---

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

.....wf..... 
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)
⊢ λ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))\000C)
  ∈ {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
BY
{ MemTypeCD }

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)
⊢ λ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))\000C)
  ∈ (T List) ⟶ ℙ

2
.....set predicate..... 
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)
⊢ down-closed(T;λ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))))
∧ Unbounded(λ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))))

3
.....wf..... 
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. A : (T List) ⟶ ℙ
⊢ down-closed(T;A) ∧ Unbounded(A) ∈ Type

---

Latex:

---

Latex:
.....wf..... 
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)
\mvdash{}  \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||)))))  \mmember{}  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}| 
                                                                                                                    down-closed(T;A)  \mwedge{}  Unbounded(A)\} 


By

---

Latex:
MemTypeCD

---

Home Index