QuantifyOnSets

#import: member(ele,set).


my-minus-one(N,M) <->  (N > 1)  &  (M = N-1)

forall x. same(x,x)


exactly-n-elements(1,set) <->
(exists set ele.
    (   member(ele,set)
      & ~(exists other-ele.
           (  member(other-ele,set)
             & ~same(other-ele,ele)))))

exactly-n-elements(2,set) <->
(exists set ele1 ele2.
  (  member(ele1,set)
   & member(ele2,set)
   & ~same(ele1,ele2)
   & ~ (exists other-ele.
         (   member(other-ele,set)
          & ~same(other-ele,ele1)
          & ~same(other-ele,ele2)))))

exactly-n-elements(N,set) <->
   range-elements(N,N,set)

range-elements(N,M,set) <->
 (exists set.
  ( min-elements(N,set)
    & max-elements(M,set)))

min-elements(1,set) <->
 (exists set ele1.
     (member(ele1,set)))

min-elements(2,set) <->
 (exists set ele1 ele2.
   (  member(ele1,set)
    & member(ele2,set)
    & ~same(ele1,ele2)))

max-elements(2,set) <->
(exists set ele1 ele2.
   (  member(ele1,set)
    & member(ele2,set)
    &  ~(exists other-ele.
          (  member(other-ele,set)
            & ~same(other-ele,ele1)
            & ~same(other-ele,ele2)))))

% exists a set with no elements
exactly-n-elements(0,set) <->
  (exists set
     ~(exists ele1. member(ele1,set)))

max-elements(1,set) <->
 exactly-n-elements(0,set) v exactly-n-elements(1,set)

containsAtLeastOneUnique(set1,set2) <->
  (exists ele. (member(ele,set1) -> ~member(ele,set2)))

disjoint(set1,set2) <->
  ~(exists ele. (member(ele,set1) & member(ele,set2)))

subset(set1,set2) <->
    (forall ele.
      member(ele,set1) -> member(ele,set2) )

union(set1,set2,set) <->
 (forall ele.
   (member(ele,set) <->
       (member(ele,set1) v member(ele,set2))))

union(set1,set2,set) <->
  (exists scratchpad.
      union(set1,set2,scratchpad)
     & ~containsAtLeastOneUnique(set,scratchpad))


union-disjoint(set1,set2,set) <->
   (   union(set1,set2,set)
     & disjoint(set1,set2))


min-elements(4,set) <->
  (exists set1 set2.
     min-elements(2,set1)
   & min-elements(2,set2)
   & union-disjoint(set1,set2))

min-elements(N,set) <->
  (exists set1 set2.
     min-elements(1,set1)
   & min-elements(M,set2)
   & non-empty(set2)
   & union-disjoint(set1,set2)
   & my-minus-one(N,M))


max-elements(N,set) <->
  (exists set1 set2.
     max-elements(1,set1)
   & max-elements(M,set2)
   & union-disjoint(set1,set2)
   & my-minus-one(N,M))


equal_sets_v2(set1,set2) <->
   ( ~containsAtLeastOneUnique(set1,set2)
     & ~containsAtLeastOneUnique(set2,set1))

equal_sets_v1(set1,set2) <->
 ( non-empty(set1)
   & (forall ele.
      (member(ele,set1) <-> member(ele,set2))))