---

Step * of Lemma tree_ind_wf

No Annotations
∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ {x:A| R[x;tree_leaf(value)]} ].
∀[node:left:tree(E) ⟶ right:tree(E) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;tree_node(left;right)]} ].
  (tree_ind(v;
            tree_leaf(value)⇒ leaf[value];
            tree_node(left,right)⇒ rec1,rec2.node[left;right;rec1;rec2])  ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma tree-definition) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[E,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  tree(E)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:tree(E)].  \mforall{}[leaf:value:E  {}\mrightarrow{}  \{x:A|  R[x;tree\_leaf(value)]\}  ].
\mforall{}[node:left:tree(E)
              {}\mrightarrow{}  right:tree(E)
              {}\mrightarrow{}  \{x:A|  R[x;left]\} 
              {}\mrightarrow{}  \{x:A|  R[x;right]\} 
              {}\mrightarrow{}  \{x:A|  R[x;tree\_node(left;right)]\}  ].
    (tree\_ind(v;
                        tree\_leaf(value){}\mRightarrow{}  leaf[value];
                        tree\_node(left,right){}\mRightarrow{}  rec1,rec2.node[left;right;rec1;rec2])    \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  tree-definition)

---

Home Index