Lines Matching defs:SUBSET
5 (DEFUN SUBSET (X Y)
9 (SUBSET (CDR X) Y)
26 (DEFUN SET-EQUAL (X Y) (IF (SUBSET X Y) (SUBSET Y X) 'NIL))
28 (DEFTHM SUBSET-IS-REFLEXIVE (SUBSET X X))
30 (DEFTHM SUBSET-IS-TRANSITIVE
31 (IMPLIES (IF (SUBSET X Y) (SUBSET Y Z) 'NIL)
32 (SUBSET X Z)))
34 (DEFTHM SUBSET-OF-EMPTY-IS-EMPTY
35 (IMPLIES (IF (NOT (CONSP X)) (SUBSET Y X) 'NIL)
51 (DEFTHM SUBSET-IS-ANTISYMMETRIC
52 (IMPLIES (IF (SUBSET X Y) (SUBSET Y X) 'NIL)
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)))
64 (IMPLIES (IF (MEMBERP E X) (SUBSET X Y) 'NIL)
67 (DEFTHM SUBSET-OF-NIL-IS-NIL
68 (IMPLIES (IF (NOT (CONSP Y)) (SUBSET X Y) 'NIL)
71 (DEFUN PROPER-SUBSET (X Y) (IF (SUBSET X Y) (NOT (SUBSET Y X)) 'NIL))
73 (DEFTHM PROPER-SUBSET-IS-IRREFLEXIVE (NOT (PROPER-SUBSET X X)))
75 (DEFTHM PROPER-SUBSET-IS-TRANSITIVE
76 (IMPLIES (IF (PROPER-SUBSET X Y)
77 (PROPER-SUBSET Y Z)
79 (PROPER-SUBSET X Z)))
81 (DEFTHM PROPER-SUBSET-IS-STRONGER-THAN-SUBSET
82 (IMPLIES (PROPER-SUBSET X Y)
83 (SUBSET X Y)))