isAncestor be a relation on binary tree nodes such that
isAncestor x y means
y can be reached from
n steps from parent to child, where
n may be zero. It is clear from this definition that
isAncestor is a partial order. (Two nodes are mutual ancestors if and only if they are identical, and ancestors of ancestors are also ancestors.)
But on a second reflection,
isAncestor is not just a partial order. For instance, it has the property
forall x y z, isAncestor x z -> isAncestor y z -> ( isAncestor x y \/ isAncestor y x ), which I don't think is common to all partial orders.
Is there a kind of order that precisely designates
isAncestor? Since binary trees are extensively studied in CS, I'm guessing there must be a name and a well known set of properties for this kind of relation.