module email
sig Name, Addr {}
sig AddrBook {map: Name -> Addr}
fun add (b, b': AddrBook, a: Addr, n: Name) {b'.map = b.map + n->a}
fun del (b, b': AddrBook, n: Name) {b'.map = b.map - n->Addr}
fun lookup (b: AddrBook, n: Name): set Addr {result = b.map[n]}

assert delUndoesAdd {all b,b',b": AddrBook, n: Name, a: Addr |
	add (b,b',a,n) and del (b',b",n) => b.map = b".map }
assert addIdempotent {all b,b',b": AddrBook, n: Name, a: Addr |
	add (b,b',a,n) and add (b',b",a,n) => b'.map = b".map }
assert addLocal {all b,b': AddrBook, n,n': Name, a: Addr |
	add (b,b',a,n) and n != n' => lookup (b,n') = lookup (b',n') }

check delUndoesAdd for 1 but 2 AddrBook
check addIdempotent
check addLocal