13 Abstraction function, toEmpSet:
15 exists er (count(er, s.val) = 1
16 /\ getERef(known, e) = er)
20 (forall er: eref (count(er, s.val) <= 1)
22 /\ forall er: eref (count(er, s.val) = 1
28 # define empset_create() (erc_create())
29 # define empset_final(s) (erc_final(s))
30 # define empset_member(e, s) \
31 (!(eref_equal(_empset_get(e, s), erefNIL)))
32 # define empset_size(es) (erc_size(es))
33 # define empset_choose(es) (eref_get(erc_choose(es)))
34 # define empset_sprint(es) (erc_sprint(es))