fmod BIN-TREE is
    
    sorts BinTree Elt .
    
    op null : -> BinTree .
    op getData : BinTree -> Elt .
    ops rightTree leftTree : BinTree -> BinTree .
    op isLeaf : BinTree -> Bool .
    op makeTree : BinTree Elt BinTree -> BinTree .
    
    *** Next operator is just makeTree with different syntax
    op [_<-_->_] : BinTree Elt BinTree -> BinTree .
    
    vars L R : BinTree .
    var D : Elt .
    
    *** For reductions only
    vars D1 D2 D3 D4 D5 : Elt .

    ceq isLeaf([L <- D -> R]) = true if (L == null) and (R == null) .
    eq rightTree([L <- D -> R]) = R .
    eq leftTree([L <- D -> R]) = L .
    eq getData([L <- D -> R]) = D .
    
    eq makeTree(L,D,R) = [L <- D -> R] .
endfm

*** Make a binary tree that looks like this:
***
***                    D1
***                    |
***               D2------ D4
***               |
***         D5 ------D3
***
*** And navigate from the root D1 to D3
*** (leftTree to D2, then rightTree to D3,
*** then getData)
red getData(rightTree(leftTree(
*** The next line is D2 (left) subtree
[[[null <- D5 -> null] <- D2 -> [null <- D3 -> null]]
*** The next line is the root of the tree
  <- D1 ->
*** The next line is D4 (right) subtree
[null <- D4 -> null]]))) .