interface Set {
  var elems: set[int]

  constructor Empty()
    ensures elems = {}

  constructor SingletonZero()
    ensures elems = {0}

  constructor Singleton(t: int)
    ensures elems = {t}

  constructor Sum(p: int, q: int)
    ensures elems = {p + q}

  constructor Double(p: int, q: int)
    requires p != q
    ensures elems = {p q}

}

datamodel Set {
  var root: SetNode

  frame
    root

  invariant
    root = null ==> elems = {}
    root != null ==> elems = root.elems
}

interface SetNode {
  var elems: set[int]

  constructor Init(x: int)
    ensures elems = {x}

  constructor Double(a: int, b: int)
    requires a != b
    ensures elems = {a b}

  constructor DoubleBase(x: int, y: int)
    requires x > y
    ensures elems = {x y}

  constructor Triple(x: int, y: int, z: int)
    requires x != y && y != z && z != x
    ensures elems = {x y z}

  constructor TripleBase(x: int, y: int, z: int)
    requires x < y && y < z
    ensures elems = {x y z}
	
  method Find(n: int) returns (ret: bool)
    ensures ret = (n in elems)
	
}

datamodel SetNode {
  var data: int
  var left: SetNode
  var right: SetNode

  frame 
    left * right

  invariant
    elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})
    left != null  ==> forall e :: e in left.elems ==> e < data
    right != null ==> forall e :: e in right.elems ==> e > data
}