---

Step * of Lemma wfd-tree-induction-ext

∀[A:Type]. ∀[P:wfd-tree(A) ⟶ ℙ].
  (P[w-nil()] ⇒ (∀f:A ⟶ wfd-tree(A). ((∀a:A. P[f a]) ⇒ P[mk-wfd-tree(f)])) ⇒ (∀w:wfd-tree(A). P[w]))
BY
{ xxxExtract of Obid: wfd-tree-induction
     not unfolding  bbar-recursion co-w-select wfd-subtrees co-w-null nil outr ifthenelse assert list_ind
     finishing with Auto
     normalizes to:
     
     λnilcase,indhyp,w. bbar-recursion(λs.co-w-null(w@s);
                                       λs.nilcase;
                                       λs,pfs. (rec-case(s) of
                                                [] => λw,pfs. (indhyp wfd-subtrees(w) (λa.(pfs a)))
                                                a::L =>
                                                 r.λw,pfs. (r (wfd-subtrees(w) a) (λt.(pfs t))) 
                                                w 
                                                pfs);
                                       [])xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:wfd-tree(A)  {}\mrightarrow{}  \mBbbP{}].
    (P[w-nil()]
    {}\mRightarrow{}  (\mforall{}f:A  {}\mrightarrow{}  wfd-tree(A).  ((\mforall{}a:A.  P[f  a])  {}\mRightarrow{}  P[mk-wfd-tree(f)]))
    {}\mRightarrow{}  (\mforall{}w:wfd-tree(A).  P[w]))


By

---

Latex:
xxx...xxx

---

Home Index