/* Name = {(G0),(A0),(A1)} Alias = {(A0),(A1)} Group = {(G0)} RecentlyUsed = {(G0),(A1)} */ abstract sig Name {} sig Alias extends Name {} sig Group extends Name {} sig RecentlyUsed in Name {} fun Union []:set Name { Alias + Group } fun Intersection []: set Name { Alias & RecentlyUsed } fun Difference []: set Name { Name - RecentlyUsed } pred Subset [] { RecentlyUsed in Name } pred Equality [] { Name = Group + Alias } fact example { #Name = 3 #RecentlyUsed = 2 some g:Group | g in RecentlyUsed } pred show [] { Subset[] Equality[] } run show for exactly 2 Alias, exactly 1 Group