// Christian Semrau

Type SET[ITEM]

Functions:
  mt_set: --> SET[ITEM]				Konstruktor
  add: SET[ITEM] x ITEM --> SET[ITEM]		Konstruktor
  is_in: ITEM x SET[ITEM] --> BOOL		Praedikat
  delete: ITEM x SET[ITEM] --> SET[ITEM]
  union: SET[ITEM] x SET[ITEM] --> SET[ITEM]
  intersect: SET[ITEM] x SET[ITEM] --> SET[ITEM]
  setminus: SET[ITEM] x SET[ITEM] --> SET[ITEM]

Axioms: s, s2: SET[ITEM]; x, y: ITEM
  x = y -> add(add(s,x), y) = add(s,x)
  x != y -> add(add(s,x), y) = add(add(s,y), x)

  not(is_in(x, mt_set))
  x = y -> is_in(x, add(s,y))
  x != y -> is_in(x, add(s,y)) <-> is_in(x,s)

  delete(x, mt_set) = mt_set
  x = y -> delete(x, add(s,y)) = delete(x, s)
// "= s" funktioniert meiner Meinung nach nur,
// wenn y nicht in s ist, denn x muss auch aus s raus
  x != y -> delete(x, add(s,y)) = add(y, delete(x,s))

  is_in(x, union(s,s2)) <-> is_in(x, s) OR is_in(x, s2)
  is_in(x, intersect(s,s2)) <-> is_in(x, s) AND is_in(x, s2)
  is_in(x, setminus(s,s2)) <-> is_in(x, s) AND NOT is_in(x, s2)

Preconditions:
  keine