1pub const BUILTIN_ENV_CODE_FOR_SET_OPERATORS: &str = r#"
4
5prop in_intersect_is_in_both(z set, A set, B set):
6 $in(z, A)
7 $in(z, B)
8
9prop in_set_minus_is_in_first_operand(z set, A set, B set):
10 $in(z, A)
11
12prop in_set_minus_is_not_in_second_operand(z set, A set, B set):
13 not $in(z, B)
14
15prop in_cup_via_member_set(z set, F set, Y set):
16 $in(z, cup(F))
17
18prop subset_of_finite_set_is_finite(A set, B finite_set):
19 $is_finite_set(A)
20
21know:
22 forall z set, A set, B set:
23 $in(z, A)
24 =>:
25 $in(z, union(A, B))
26
27 forall z set, A set, B set:
28 $in(z, B)
29 =>:
30 $in(z, union(A, B))
31
32 forall z set, A set, B set:
33 $in(z, union(A, B))
34 =>:
35 $in(z, A) or $in(z, B)
36
37 forall z set, A set, B set:
38 $in(z, A)
39 $in(z, B)
40 =>:
41 $in(z, intersect(A, B))
42
43 forall z set, A set, B set:
44 $in(z, intersect(A, B))
45 =>:
46 $in_intersect_is_in_both(z, A, B)
47
48 forall z set, A set, B set:
49 not $in(z, A)
50 =>:
51 not $in(z, intersect(A, B))
52
53 forall z set, A set, B set:
54 not $in(z, B)
55 =>:
56 not $in(z, intersect(A, B))
57
58 forall A, B set:
59 intersect(A, B) $subset A
60
61 forall A, B set:
62 intersect(A, B) $subset B
63
64 forall A, B set:
65 A $subset union(A, B)
66
67 forall A, B set:
68 B $subset union(A, B)
69
70 forall A, B set:
71 union(A, B) = union(B, A)
72
73 forall A, B set:
74 intersect(A, B) = intersect(B, A)
75
76 forall A, B, C set:
77 union(union(A, B), C) = union(A, union(B, C))
78
79 forall A, B, C set:
80 intersect(intersect(A, B), C) = intersect(A, intersect(B, C))
81
82 forall A, B set:
83 union(A, intersect(A, B)) = A
84
85 forall A, B set:
86 intersect(A, union(A, B)) = A
87
88 forall A set:
89 union(A, A) = A
90
91 forall A set:
92 intersect(A, A) = A
93
94 forall A set:
95 union(A, {}) = A
96
97 forall A set:
98 intersect(A, {}) = {}
99
100 forall A, B, C set:
101 intersect(A, union(B, C)) = union(intersect(A, B), intersect(A, C))
102
103 forall A, B, C set:
104 union(A, intersect(B, C)) = intersect(union(A, B), union(A, C))
105
106 forall z set, A set, B set:
107 $in(z, A)
108 not $in(z, B)
109 =>:
110 $in(z, set_minus(A, B))
111
112 forall z set, A set, B set:
113 $in(z, set_minus(A, B))
114 =>:
115 $in_set_minus_is_in_first_operand(z, A, B)
116
117 forall z set, A set, B set:
118 $in(z, set_minus(A, B))
119 =>:
120 $in_set_minus_is_not_in_second_operand(z, A, B)
121
122 forall A, B set:
123 set_minus(A, B) $subset A
124
125 forall A, B set:
126 set_diff(A, B) = union(set_minus(A, B), set_minus(B, A))
127
128 forall z set, F set, Y set:
129 $in(Y, F)
130 $in(z, Y)
131 =>:
132 $in_cup_via_member_set(z, F, Y)
133
134 forall A, B finite_set:
135 $is_finite_set(union(A, B))
136 $is_finite_set(intersect(A, B))
137 $is_finite_set(set_minus(A, B))
138 $is_finite_set(set_diff(A, B))
139
140 forall A finite_set:
141 count(A) $in N
142
143 forall A set, B finite_set:
144 A $subset B
145 =>:
146 $subset_of_finite_set_is_finite(A, B)
147
148 forall A finite_set, B set:
149 B $subset A
150 =>:
151 $is_finite_set(B)
152 $is_finite_set(set_minus(A, B))
153 count(set_minus(A, B)) = count(A) - count(B)
154
155 forall A, B finite_set:
156 count(union(A, B)) = count(A) + count(B) - count(intersect(A, B))
157 count(A) = count(intersect(A, B)) + count(set_minus(A, B))
158 count(B) = count(intersect(A, B)) + count(set_minus(B, A))
159 count(set_minus(A, B)) = count(A) - count(intersect(A, B))
160 count(set_minus(B, A)) = count(B) - count(intersect(A, B))
161 count(set_diff(A, B)) = count(set_minus(A, B)) + count(set_minus(B, A))
162
163 forall A, B finite_set:
164 A $subset B
165 =>:
166 count(A) <= count(B)
167
168 forall A, B finite_set:
169 A $superset B
170 =>:
171 count(A) >= count(B)
172
173 forall A, B finite_set:
174 count(intersect(A, B)) <= count(A)
175 count(intersect(A, B)) <= count(B)
176 count(set_minus(A, B)) <= count(A)
177 count(union(A, B)) <= count(A) + count(B)
178 count(set_diff(A, B)) <= count(A) + count(B)
179"#;