// All the ways to partition a set into two disjoint subsets

Define "(T,U) is a partition of S" to mean
          T is a subset of S
   and    U is a subset of S
   and    T union U = S
   and    T intersect U = empty

// Part (a)
proc <E> part2BU( S : set<E> ) : set< set<E> x set<E> >
    ensures result is the set of all pairs of sets (T,U)
               such that (T,U) is a partition of S


// Part (b) 
// A bottom up approach builds the result as we come up from the recursion
proc <E> part2BU( S : set<E> ) : set< set<E> x set<E> >
    ensures result is the set of all pairs of sets (T,U)
               such that (T,U) is a partition of S
    
    if S is empty
        return { ( empty, empty ) }
    else 
        val x := any element of S 
        val P := part2( S - {x} ) 
        var R := {} 
        for each (T, U) in P do
            R := R union { (T, U union {x} ), ( T union {x}, U ) }
        return R

 // Part (c)
 // A top down approach builds the partition on the way down.
proc <E> part2TD( S : set<E> ) : set< set<E> x set<E> >
    ensures result is the set of all pairs of sets (T,U)
                such that (T,U) is a partition of S
    return part2TD_aux( S, empty, empty )
 
// This auxiliary procedure takes extra parameters representing the work done so far.
// In this case (T_in, U_in) is a partially build partition of the original set.
// Parameter S represents the elements not yet assigned to a partition.
proc <E> part2TD_aux( S : set<E>, T_in : set<E>, U_in : set<E> ) : set< set<E> x set<E> >
    ensures result is the set of all pairs of sets (T,U)
                such that (T,U) is a partition of S union T_in union U_in
                and T is a superset of T_in
                and U is a superset of U_in

    if S is empty then
        return {(T_in, U_in)}
    else 
        val x := any element of S
        return       part2TD_aux( S-{x}, T_in union {x}, U_in )
               union part2TD_aux( S-{x}, T_in, U_in union {x} )