Lines Matching +defs:SET +defs:UNION
12 (DEFUN SET-INTERSECT (X Y)
16 (CONS (CAR X) (SET-INTERSECT (CDR X) Y))
17 (SET-INTERSECT (CDR X) Y))))
19 (DEFUN SET-UNION (X Y)
23 (SET-UNION (CDR X) Y)
24 (CONS (CAR X) (SET-UNION (CDR X) Y)))))
26 (DEFUN SET-EQUAL (X Y) (IF (SUBSET X Y) (SUBSET Y X) 'NIL))
38 (DEFTHM SET-EQUAL-IS-AN-EQUIVALENCE
39 (IF (BOOLEANP (SET-EQUAL X Y))
40 (IF (SET-EQUAL X X)
41 (IF (IMPLIES (SET-EQUAL X Y)
42 (SET-EQUAL Y X))
43 (IMPLIES (IF (SET-EQUAL X Y)
44 (SET-EQUAL Y Z)
46 (SET-EQUAL X Z))
53 (SET-EQUAL X Y)))
55 (DEFTHM INTERSECT-IS-A-SUBSET-1 (SUBSET (SET-INTERSECT X Y) X))
57 (DEFTHM INTERSECT-IS-A-SUBSET-2 (SUBSET (SET-INTERSECT X Y) Y))
59 (DEFTHM UNION-IS-A-SUBSET-1 (SUBSET X (SET-UNION X Y)))
61 (DEFTHM UNION-IS-A-SUBSET-2 (SUBSET Y (SET-UNION X Y)))