Add a verified balanced binary tree example

This is based on the implementation of weight balanced binary search
trees in the ghc Haskell compiler's standard library.

comparisonScript.sml has a basic theory of comparisons that return
either Less, Greater, or Equal. This is not compatible with the existing
totoScript.sml, because I don't require cmp x y = Equal ==> x = y, but
it does.

osetScript.sml uses the balanced trees to implement sets.

Functional correctenss of the operations is verified, along with the
balancing properties.