text: # include "empset.h"
  
  static bool initDone = FALSE;
  
  eref _empset_get (employee e, erc s) 
  {
    erc_elements(s, er)
      {
        employee e1 = eref_get(er);
        if (employee_equal(&e1, &e))
  	return er;
      } end_erc_elements ;
    
    return erefNIL;
  }
  
  void empset_clear (empset s) 
  {
    erc_clear (s);
  }
  
  bool /*@alt void@*/ empset_insert (empset s, employee e) 
  {
    if (!eref_equal (_empset_get (e, s), erefNIL)) 
      {
        return FALSE;
      }
    
    empset_insertUnique (s, e);
    return TRUE;
  }
  
  void empset_insertUnique (empset s, employee e) 
  {
    eref er;
  
    er = ereftab_lookup (e, known);
  
    if (eref_equal (er, erefNIL)) 
      {
        er = eref_alloc ( );
        eref_assign (er,e);
        ereftab_insert (known, e, er);
      }
    
    erc_insert (s, er);
  }
  
  bool /*@alt void@*/ empset_delete (empset s, employee e) 
  {
    eref er;
  
    er = _empset_get (e, s);
  
    if (eref_equal (er, erefNIL)) 
      {
        return FALSE;
      }
    return erc_delete (s, er);
  }
  
  empset empset_disjointUnion (empset s1, empset s2) 
  {
    erc result;
    empset tmp;
    
    result = erc_create ( );
  
    if (erc_size (s1) > erc_size (s2)) 
      {
        tmp = s1;
        s1 = s2;
        s2 = tmp;
      }
    
    erc_join (result, s1);
  
    empset_elements(s2, emp)
      {
        empset_insertUnique(result, emp);
      } end_empset_elements ;
  
    return result;
  }
  
  empset empset_union (empset s1, empset s2) 
  {
    erc result;
    empset tmp;
  
    result = erc_create ();
  
    if (erc_size (s1) > erc_size (s2)) 
      {
        tmp = s1;
        s1 = s2;
        s2 = tmp;
      }
    erc_join (result, s2);
  
    empset_elements (s1, emp)
      {
        if (!empset_member(emp, s2))
  	empset_insert(result, emp);
      } end_empset_elements ;
  
    return result;
  }
  
  void empset_intersect (empset s1, empset s2) 
  {
    erc toDelete = erc_create();
  
    empset_elements (s2, emp)
      {
        if (!empset_member(emp, s2))
  	empset_insert(toDelete, emp);
      } end_empset_elements ;
  
    empset_elements (toDelete, emp)
      {
        empset_delete(s1, emp);
      } end_empset_elements;
  
    erc_final (toDelete);
  }
  
  bool empset_subset (empset s1, empset s2) 
  {
    empset_elements(s1, emp)
      {
        if (!empset_member(emp, s2)) return FALSE;
      } end_empset_elements ;
  
    return TRUE;
  }
  
  void empset_initMod (void) 
  {
    if (initDone) return;
  
    bool_initMod ();
    employee_initMod ();
    eref_initMod ();
    erc_initMod ();
    ereftab_initMod ();
    known = ereftab_create ();
    initDone = TRUE;
  }
  