set{T : TYPE; } : CONTEXT = BEGIN Set : TYPE = [T -> BOOLEAN]; empty_set : Set = LAMBDA (e : T) : FALSE; full_set : Set = LAMBDA (e : T) : TRUE; insert (aset : Set, e : T) : Set = LAMBDA (e1 : T) : e = e1 OR aset(e1); remove (aset : Set, e : T) : Set = LAMBDA (e1 : T) : e /= e1 AND aset(e1); contains? (aset : Set, e : T) : BOOLEAN = aset(e); empty? (aset : Set) : BOOLEAN = (FORALL (e : T) : aset(e) = FALSE); union(aset1 : Set, aset2 : Set) : Set = LAMBDA (e : T) : aset1(e) OR aset2(e); intersection(aset1 : Set, aset2 : Set) : Set = LAMBDA (e : T) : aset1(e) AND aset2(e); difference(aset1 : Set, aset2 : Set) : Set = LAMBDA (e : T) : aset1(e) AND NOT aset2(e); END