---

Step * of Lemma binary-tree_ind_wf

∀[A:Type]. ∀[R:A ─→ binary-tree() ─→ ℙ]. ∀[v:binary-tree()]. ∀[Leaf:val:ℤ ─→ {x:A| R[x;btr_Leaf(val)]} ].
∀[Node:left:binary-tree()
       ─→ right:binary-tree()
       ─→ {x:A| R[x;left]} 
       ─→ {x:A| R[x;right]} 
       ─→ {x:A| R[x;btr_Node(left;right)]} ].
  (binary-tree_ind(v;
                   btr_Leaf(val)⇒ Leaf[val];
                   btr_Node(left,right)⇒ rec1,rec2.Node[left;right;rec1;rec2])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{binary-tree-definition:o, 1:l, i:l}⋅ }

---

Latex:


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


By

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

---

Home Index