View difference between Paste ID: 4ULWk6b7 and rzW9KkPC

 #import: member(ele,set).
-#import: written-on(word,paper).
+
 
 my-minus-one(N,M) <->  (N > 1)  &  (M = N-1)
 
 forall x. same(x,x)
 
 
-legal-pad(paper) <-> min-elements(1, paper)
+exactly-n-elements(1,set) <->
 (exists set ele.
-exactly-n-elements(1,paper) <->
+    (   member(ele,set)
-(exists paper word.
+      & ~(exists other-ele.
-    (   written-on(word,paper)
+           (  member(other-ele,set)
-      & ~(exists other-word.
+             & ~same(other-ele,ele)))))
-           (  written-on(other-word,paper)
+
-             & ~same(other-word,word)))))
+exactly-n-elements(2,set) <->
 (exists set ele1 ele2.
-exactly-n-elements(2,paper) <->
+  (  member(ele1,set)
-(exists paper word1 word2.
+   & member(ele2,set)
-  (  written-on(word1,paper)
+   & ~same(ele1,ele2)
-   & written-on(word2,paper)
+   & ~ (exists other-ele.
-   & ~same(word1,word2)
+         (   member(other-ele,set)
-   & ~ (exists other-word.
+          & ~same(other-ele,ele1)
-         (   written-on(other-word,paper)
+          & ~same(other-ele,ele2)))))
-          & ~same(other-word,word1)
+
-          & ~same(other-word,word2)))))
+exactly-n-elements(N,set) <->
    range-elements(N,N,set)
-exactly-n-elements(N,paper) <->
+
-   range-elements(N,N,paper)
+range-elements(N,M,set) <->
  (exists set.
-range-elements(N,M,paper) <->
+  ( min-elements(N,set)
- (exists paper.
+    & max-elements(M,set)))
-  ( min-elements(N,paper)
+
-    & max-elements(M,paper)))
+min-elements(1,set) <->
  (exists set ele1.
-min-elements(1,paper) <->
+     (member(ele1,set)))
- (exists paper word1.
+
-     (written-on(word1,paper)))
+min-elements(2,set) <->
  (exists set ele1 ele2.
-min-elements(2,paper) <->
+   (  member(ele1,set)
- (exists paper word1 word2.
+    & member(ele2,set)
-   (  written-on(word1,paper)
+    & ~same(ele1,ele2)))
-    & written-on(word2,paper)
+
-    & ~same(word1,word2)))
+max-elements(2,set) <->
 (exists set ele1 ele2.
-max-elements(2,paper) <->
+   (  member(ele1,set)
-(exists paper word1 word2.
+    & member(ele2,set)
-   (  written-on(word1,paper)
+    &  ~(exists other-ele.
-    & written-on(word2,paper)
+          (  member(other-ele,set)
-    &  ~(exists other-word.
+            & ~same(other-ele,ele1)
-          (  written-on(other-word,paper)
+            & ~same(other-ele,ele2)))))
-            & ~same(other-word,word1)
+
-            & ~same(other-word,word2)))))
+% exists a set with no elements
 exactly-n-elements(0,set) <->
-% exists a paper with no elements
+  (exists set
-exactly-n-elements(0,paper) <->
+     ~(exists ele1. member(ele1,set)))
-  (exists paper
+
-     ~(exists word1. written-on(word1,paper)))
+max-elements(1,set) <->
  exactly-n-elements(0,set) v exactly-n-elements(1,set)
-max-elements(1,paper) <->
+
- exactly-n-elements(0,paper) v exactly-n-elements(1,paper)
+containsAtLeastOneUnique(set1,set2) <->
   (exists ele. (member(ele,set1) -> ~member(ele,set2)))
-containsAtLeastOneUnique(paper1,paper2) <->
+
-  (exists word. (written-on(word,paper1) -> ~written-on(word,paper2)))
+disjoint(set1,set2) <->
   ~(exists ele. (member(ele,set1) & member(ele,set2)))
-disjoint(paper1,paper2) <->
+
-  ~(exists word. (written-on(word,paper1) & written-on(word,paper2)))
+subset(set1,set2) <->
     (forall ele.
-subset(paper1,paper2) <->
+      member(ele,set1) -> member(ele,set2) )
-    (forall word.
+
-      written-on(word,paper1) -> written-on(word,paper2) )
+union(set1,set2,set) <->
  (forall ele.
-union(paper1,paper2,paper) <->
+   (member(ele,set) <->
- (forall word.
+       (member(ele,set1) v member(ele,set2))))
-   (written-on(word,paper) <->
+
-       (written-on(word,paper1) v written-on(word,paper2))))
+union(set1,set2,set) <->
   (exists scratchpad.
-union(paper1,paper2,paper) <->
+      union(set1,set2,scratchpad)
      & ~containsAtLeastOneUnique(set,scratchpad))
-      union(paper1,paper2,scratchpad)
+
-     & ~containsAtLeastOneUnique(paper,scratchpad))
+
 union-disjoint(set1,set2,set) <->
    (   union(set1,set2,set)
-union-disjoint(paper1,paper2,paper) <->
+     & disjoint(set1,set2))
-   (   union(paper1,paper2,paper)
+
-     & disjoint(paper1,paper2))
+
 min-elements(4,set) <->
   (exists set1 set2.
-min-elements(4,paper) <->
+     min-elements(2,set1)
-  (exists paper1 paper2.
+   & min-elements(2,set2)
-     min-elements(2,paper1)
+   & union-disjoint(set1,set2))
-   & min-elements(2,paper2)
+
-   & union-disjoint(paper1,paper2))
+min-elements(N,set) <->
   (exists set1 set2.
-min-elements(N,paper) <->
+     min-elements(1,set1)
-  (exists paper1 paper2.
+   & min-elements(M,set2)
-     min-elements(1,paper1)
+   & non-empty(set2)
-   & min-elements(M,paper2)
+   & union-disjoint(set1,set2)
-   & legal-pad(paper2)
+
-   & union-disjoint(paper1,paper2)
+
 
 max-elements(N,set) <->
   (exists set1 set2.
-max-elements(N,paper) <->
+     max-elements(1,set1)
-  (exists paper1 paper2.
+   & max-elements(M,set2)
-     max-elements(1,paper1)
+   & union-disjoint(set1,set2)
-   & max-elements(M,paper2)
+
-   & legal-pad(paper2)
+
-   & union-disjoint(paper1,paper2)
+
 equal_sets_v2(set1,set2) <->
    ( ~containsAtLeastOneUnique(set1,set2)
      & ~containsAtLeastOneUnique(set2,set1))
-equal_papers_v2(paper1,paper2) <->
+
-   ( ~containsAtLeastOneUnique(paper1,paper2)
+equal_sets_v1(set1,set2) <->
-     & ~containsAtLeastOneUnique(paper2,paper1)
+ ( non-empty(set1)
-     & legal-pad(paper1)
+   & (forall ele.
-     & legal-pad(paper2))
+      (member(ele,set1) <-> member(ele,set2))))