---

Step * of Lemma binary-tree_ind_wf_simple

∀[A:Type]. ∀[v:binary-tree()]. ∀[Leaf:val:ℤ ⟶ A]. ∀[Node:left:binary-tree() ⟶ right:binary-tree() ⟶ A ⟶ A ⟶ A].
  (binary-tree_ind(v;
                   btr_Leaf(val)⇒ Leaf[val];
                   btr_Node(left,right)⇒ rec1,rec2.Node[left;right;rec1;rec2])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `binary-tree_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:binary-tree()].  \mforall{}[Leaf:val:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[Node:left:binary-tree()
                                                                                                                    {}\mrightarrow{}  right:binary-tree()
                                                                                                                    {}\mrightarrow{}  A
                                                                                                                    {}\mrightarrow{}  A
                                                                                                                    {}\mrightarrow{}  A].
    (binary-tree\_ind(v;
                                      btr\_Leaf(val){}\mRightarrow{}  Leaf[val];
                                      btr\_Node(left,right){}\mRightarrow{}  rec1,rec2.Node[left;right;rec1;rec2])    \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  0  `binary-tree\_ind\_wf`

---

Home Index