---

Step * 1 of Lemma mk-wfd-tree_wf


1. A : Type
2. f : A ⟶ wfd-tree(A)
3. mk-wfd-tree(f) ∈ co-w(A)
4. p : ℕ ⟶ A
5. n : ℕ
6. ↑co-w-null(f (p 0)@map(λn.(p (n + 1));upto(n)))
⊢ ↑co-w-null(mk-wfd-tree(f)@map(p;upto(n + 1)))
BY
{ (RecUnfold `co-w-select` 0 THEN Fold `co-w-null` 0)⋅ }

1
1. A : Type
2. f : A ⟶ wfd-tree(A)
3. mk-wfd-tree(f) ∈ co-w(A)
4. p : ℕ ⟶ A
5. n : ℕ
6. ↑co-w-null(f (p 0)@map(λn.(p (n + 1));upto(n)))
⊢ ↑co-w-null(if null(map(p;upto(n + 1))) ∨bco-w-null(mk-wfd-tree(f))
then mk-wfd-tree(f)
else outr(mk-wfd-tree(f)) hd(map(p;upto(n + 1)))@tl(map(p;upto(n + 1)))
fi )

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  wfd-tree(A)
3.  mk-wfd-tree(f)  \mmember{}  co-w(A)
4.  p  :  \mBbbN{}  {}\mrightarrow{}  A
5.  n  :  \mBbbN{}
6.  \muparrow{}co-w-null(f  (p  0)@map(\mlambda{}n.(p  (n  +  1));upto(n)))
\mvdash{}  \muparrow{}co-w-null(mk-wfd-tree(f)@map(p;upto(n  +  1)))


By

---

Latex:
(RecUnfold  `co-w-select`  0  THEN  Fold  `co-w-null`  0)\mcdot{}

---

Home Index