---

Step * of Lemma l_tree_ind_wf

∀[L,T,A:Type]. ∀[R:A ─→ l_tree(L;T) ─→ ℙ]. ∀[v:l_tree(L;T)]. ∀[leaf:val:L ─→ {x:A| R[x;l_tree_leaf(val)]} ].
∀[node:val:T
       ─→ left_subtree:l_tree(L;T)
       ─→ 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)]} ].
  (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]) 
   ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{l_tree-definition:o, 1:l, i:l}⋅ }

---

Latex:


\mforall{}[L,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  l\_tree(L;T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:l\_tree(L;T)].
\mforall{}[leaf:val:L  {}\mrightarrow{}  \{x:A|  R[x;l\_tree\_leaf(val)]\}  ].
\mforall{}[node:val:T
              {}\mrightarrow{}  left$_{subtree}$:l\_tree(L;T)
              {}\mrightarrow{}  right$_{subtree}$:l\_tree(L;T)
              {}\mrightarrow{}  \{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$_{subtree\000C}$)]\}  ].
    (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{}  \{x:A|  R[x;v]\}  )


By

ProveDatatypeIndWf  TERMOF\{l\_tree-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index