---

Step * of Lemma mk-wfd-tree_wf

∀[A:Type]. ∀[f:A ⟶ wfd-tree(A)].  (mk-wfd-tree(f) ∈ wfd-tree(A))
BY
{ ((Auto
    THEN (Assert mk-wfd-tree(f) ∈ co-w(A) BY
                ((InstLemma `co-w-ext` [A]⋅ THENA Auto)
                 THEN Try (((SubsumeC ⌜Unit + (A ⟶ co-w(A))⌝⋅ THEN Auto)⋅ THEN ProveWfLemma))
                 ))
    )
   THEN MemTypeCD
   THEN Auto
   THEN ((Assert w-bars(f (p 0);λn.(p (n + 1))) BY
                (GenConclAtAddr [1] THEN Unfold `w-bars` 0 THEN D -2 THEN Fold `w-bars` 0 THEN BHyp (-2) THEN Auto))
         THEN (RepeatFor 2 (ParallelLast) THEN ExRepD THEN With ⌜n + 1⌝ (D 0)⋅ THEN Auto)⋅
         )⋅)⋅ }

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(mk-wfd-tree(f)@map(p;upto(n + 1)))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  wfd-tree(A)].    (mk-wfd-tree(f)  \mmember{}  wfd-tree(A))


By

---

Latex:
((Auto
    THEN  (Assert  mk-wfd-tree(f)  \mmember{}  co-w(A)  BY
                            ((InstLemma  `co-w-ext`  [A]\mcdot{}  THENA  Auto)
                              THEN  Try  (((SubsumeC  \mkleeneopen{}Unit  +  (A  {}\mrightarrow{}  co-w(A))\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}  THEN  ProveWfLemma))
                              ))
    )
  THEN  MemTypeCD
  THEN  Auto
  THEN  ((Assert  w-bars(f  (p  0);\mlambda{}n.(p  (n  +  1)))  BY
                            (GenConclAtAddr  [1]
                              THEN  Unfold  `w-bars`  0
                              THEN  D  -2
                              THEN  Fold  `w-bars`  0
                              THEN  BHyp  (-2)
                              THEN  Auto))
              THEN  (RepeatFor  2  (ParallelLast)  THEN  ExRepD  THEN  With  \mkleeneopen{}n  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}
              )\mcdot{})\mcdot{}

---

Home Index