test-zenon.why 399 Bytes
Newer Older
1 2 3

theory T

4
  use set.Set
5 6 7 8 9

  meta "rewrite" prop mem_empty

  meta "rewrite" prop add_def1

10 11
  meta "rewrite" prop union_def1

12 13 14 15
  meta "rewrite_def" predicate subset

  meta "rewrite_def" function singleton

16 17 18 19
  type t
  constant a:t
  constant b:t
  constant c:t
20 21 22 23 24 25

  goal g1: mem a (add b (add a (add c empty)))

  goal g2: mem a (add b (add a (singleton c)))

  goal g3: subset empty (singleton c)
26 27

end