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