---

Step * of Lemma l_tree-definition

∀[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ].
  ((∀val:L. {x:A| R[x;l_tree_leaf(val)]} )
  ⇒ (∀val:T. ∀left_subtree,right_subtree:l_tree(L;T).
        ({x:A| R[x;left_subtree]} 
        ⇒ {x:A| R[x;right_subtree]} 
        ⇒ {x:A| R[x;l_tree_node(val;left_subtree;right_subtree)]} ))
  ⇒ {∀v:l_tree(L;T). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `l_tree-induction` }

---

Latex:


\mforall{}[L,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  l\_tree(L;T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}val:L.  \{x:A|  R[x;l\_tree\_leaf(val)]\}  )
    {}\mRightarrow{}  (\mforall{}val:T.  \mforall{}left$_{subtree}$,right$_{subtree}$:l\_tree(L;T\000C).
                (\{x:A|  R[x;left$_{subtree}$]\} 
                {}\mRightarrow{}  \{x:A|  R[x;right$_{subtree}$]\} 
                {}\mRightarrow{}  \{x:A|  R[x;l\_tree\_node(val;left$_{subtree}$;right$_{subtre\000Ce}$)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:l\_tree(L;T).  \{x:A|  R[x;v]\}  \})


By

ProveDatatypeDefinition  `l\_tree-induction`

---

Home Index