---

Step * of Lemma l_tree_ind_wf_simple

∀[L,T,A:Type]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ A]. ∀[node:val:T
                                                            ─→ left_subtree:l_tree(L;T)
                                                            ─→ right_subtree:l_tree(L;T)
                                                            ─→ A
                                                            ─→ A
                                                            ─→ A].
  (l_tree_ind(v;
              l_tree_leaf(val)⇒ leaf[val];
              l_tree_node(val,left_subtree,right_subtree)⇒ rec1,rec2.node[val;left_subtree;right_subtree;rec1;rec2]) 
   ∈ A)
BY
{ ProveDatatypeIndWfSimple 2 `l_tree_ind_wf` }

---

Latex:


\mforall{}[L,T,A:Type].  \mforall{}[v:l\_tree(L;T)].  \mforall{}[leaf:val:L  {}\mrightarrow{}  A].  \mforall{}[node:val:T
                                                                                                                        {}\mrightarrow{}  left$_{subtree}$:\000Cl\_tree(L;T)
                                                                                                                        {}\mrightarrow{}  right$_{subtree}$\000C:l\_tree(L;T)
                                                                                                                        {}\mrightarrow{}  A
                                                                                                                        {}\mrightarrow{}  A
                                                                                                                        {}\mrightarrow{}  A].
    (l\_tree\_ind(v;
                            l\_tree\_leaf(val){}\mRightarrow{}  leaf[val];
                            l\_tree\_node(val,left$_{subtree}$,right$_{subtree}\mbackslash{}\000Cff24){}\mRightarrow{}  rec1,rec2.node[val;...;...;rec1;rec2]) 
      \mmember{}  A)


By

ProveDatatypeIndWfSimple  2  `l\_tree\_ind\_wf`

---

Home Index