CLASS Traversable [elem]
DEFERRED
TYPE Traversable
OPERATIONS
  IsEmpty: Traversable -> Boolean;
  first: Traversable (t) -> elem
    pre: not IsEmpty(t);

  rest: Traversable (t) -> Traversable
    pre: not IsEmpty(t);

END-CLASS


CLASS PostBTree [Elem]
IS-SUBTYPE-OF BTree [Elem], Traversable [Elem]
  rename IsEmpty as PostBTree_IsEmpty
EFFECTIVE
TYPE PostBTree
OPERATIONS  
  first: PostBTree -> Elem;
  rest: PostBTree -> PostBTree;
  PostBTree_IsEmpty: PostBTree -> Boolean;
  AXIOMS   t1, t2: PostBTree; x: Elem;

  first(BTree_Create(t1, t2, x) as PostBTree) =
    if BTree_IsEmpty(t1) then 
      if BTree_IsEmpty(t2) then x
      else first(t2)
      endif
    else first(t1)
    endif;

  rest(BTree_Create(t1, t2, x) as PostBTree) =
    if BTree_IsEmpty(t1) then 
      if BTree_IsEmpty(t2) then BTree_Empty() as PostBTree
      else BTree_Create(t1, rest(t2), x) as PostBTree
      endif
    else BTree_Create(rest(t1), t2, x) as PostBTree
    endif;
END-CLASS
