---

Step * 1 1 1 of Lemma mk-wfd-tree_wf


1. A : Type
2. f : A ⟶ wfd-tree(A)
3. ¬↑co-w-null(mk-wfd-tree(f))
4. mk-wfd-tree(f) ∈ co-w(A)
5. p : ℕ ⟶ A
6. n : ℕ
7. n + 1 ≠ 0
8. ↑co-w-null(f (p 0)@map(λn.(p (n + 1));upto(n)))
⊢ map(p;map(λi.(i + 1);upto((n + 1) - 1))) ~ map(λn.(p (n + 1));upto(n))
BY
{ ((RWO "map-map" 0 THENA Auto) THEN RepUR ``compose`` 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "map-map"  0  THENA  Auto)  THEN  RepUR  ``compose``  0  THEN  Auto)

---

Home Index