---

Step * 1 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(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 )
BY
{ ((RWO "null-map" 0 THENA Auto)
   THEN (((RWO "null-upto" 0 THENA Auto)
          THEN (RepeatFor 2 (AutoSplit)
                THEN RepUR ``mk-wfd-tree`` 0
                THEN NthHypSq (-1)
                THEN RepeatFor 3 (EqCD)
                THEN Auto)⋅
          )
         THEN (RW (AddrC [1] (SweepUpC (LemmaC `upto_decomp2`))) 0 THENA Auto)
         THEN Reduce 0
         THEN Try (Complete (Auto)))⋅
   ) }

1
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))

---

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(if  null(map(p;upto(n  +  1)))  \mvee{}\msubb{}co-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  )


By

---

Latex:
((RWO  "null-map"  0  THENA  Auto)
  THEN  (((RWO  "null-upto"  0  THENA  Auto)
                THEN  (RepeatFor  2  (AutoSplit)
                            THEN  RepUR  ``mk-wfd-tree``  0
                            THEN  NthHypSq  (-1)
                            THEN  RepeatFor  3  (EqCD)
                            THEN  Auto)\mcdot{}
                )
              THEN  (RW  (AddrC  [1]  (SweepUpC  (LemmaC  `upto\_decomp2`)))  0  THENA  Auto)
              THEN  Reduce  0
              THEN  Try  (Complete  (Auto)))\mcdot{}
  )

---

Home Index