Step
*
of Lemma
btr_Node-right_wf
∀[v:binary-tree()]. btr_Node-right(v) ∈ binary-tree() supposing ↑btr_Node?(v)
BY
{ DepprodCoDatatypeSelectorWf }
Latex:
\mforall{}[v:binary-tree()].  btr\_Node-right(v)  \mmember{}  binary-tree()  supposing  \muparrow{}btr\_Node?(v)
By
DepprodCoDatatypeSelectorWf
Home
Index