module addressBook sig Target {} part sig Addr, Name extends Target {} part sig Alias, Group extends Name {} sig Book {addr: Name -> Target} fact {all b: Book | no n: Name | n in n.^(b.addr)} fun add (b, b': Book, n: Name, t: Target) {b'.addr = b.addr + n->t} fun del (b, b': Book, n: Name) {b'.addr = b.addr - n->Addr} fun lookup (b: Book, n: Name): set Addr {result = n.^(b.addr) & Addr} assert addLocal {all b,b': Book, n,n': Name, a: Addr | add (b,b',n,a) and n != n' => lookup (b,n') = lookup (b',n') } check addLocal for 3 but 2 Book