Consider the following function on binary trees, which is supposed to tell whether a given `int`

is a member of a binary tree `t`

:

`type tree = Leaf | Node of int * tree * tree;; let rec tmember (t:tree) (x:int) : bool = match t with Leaf -> false | Node (j,left,right) -> j = x || tmember left x || tmember right x ;; `

If one wants to prove that this function is correct, one would need to *define* first what tree membership actually means, but then I can find no formal way of doing this except for saying that `x`

is a member of `t`

if and only if it is either equal to the root of `t`

, or it is a member of the left or right subtree of `t`

. This is essentially saying that `x`

is a member of `t`

if and only if `tmember t x`

outputs `true`

.

What am I missing here?