%{ Another supported domain are 32-bit integers. This domain is used
mainly in Proof Carrying Code applications, and because of this, it
has fairly different structure and features than the extension for
(unrestricted) integers (see section 6.4 Integer Constraints). First
of all, the algorithms used were kept short and simple, so that they
can be easily read and verified to be correct. Secondly, the set of
arithmetic operators provided has been kept to a minimum. Also, each
of these is implemented as a type family instead of a function symbol,
so that unification of arithmetic expressions follows the same rule as
that of regular terms. Finally, for each arithmetic operator, we also
provide a type family which, in addition to carry out the computation,
also provides a proof object for it.

Declaring

%uses word32.
causes the following signature to be loaded into the system:
}%

word32 : type.
+ : word32 -> word32 -> word32 -> type.
* : word32 -> word32 -> word32 -> type.
/ : word32 -> word32 -> word32 -> type.
prove+ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} type.
proof+ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} prove+ X Y Z P.
prove* : {X:word32} {Y:word32} {Z:word32} {P:* X Y Z} type.
proof* : {X:word32} {Y:word32} {Z:word32} {P:* X Y Z} prove* X Y Z P.
prove/ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} type.
proof/ : {X:word32} {Y:word32} {Z:word32} {P:+ X Y Z} prove/ X Y Z P.

%% Not mentioned in the documentation:

0 : word32.
1 : word32.
2 : word32.
3 : word32.
4 : word32.
5 : word32.
6 : word32.
7 : word32.
8 : word32.
9 : word32.
10 : word32.
11 : word32.
12 : word32.
13 : word32.
14 : word32.
15 : word32.
16 : word32.
17 : word32.
18 : word32.
19 : word32.
20 : word32.
21 : word32.
22 : word32.
23 : word32.
24 : word32.
25 : word32.
26 : word32.
27 : word32.
28 : word32.
29 : word32.
30 : word32.
31 : word32.
32 : word32.
33 : word32.
34 : word32.
35 : word32.
36 : word32.
37 : word32.
38 : word32.
39 : word32.
40 : word32.
41 : word32.
42 : word32.
43 : word32.
44 : word32.
45 : word32.
46 : word32.
47 : word32.
48 : word32.
49 : word32.
50 : word32.
51 : word32.
52 : word32.
53 : word32.
54 : word32.
55 : word32.
56 : word32.
57 : word32.
58 : word32.
59 : word32.
60 : word32.
61 : word32.
62 : word32.
63 : word32.
64 : word32.
65 : word32.
66 : word32.
67 : word32.
68 : word32.
69 : word32.
70 : word32.
71 : word32.
72 : word32.
73 : word32.
74 : word32.
75 : word32.
76 : word32.
77 : word32.
78 : word32.
79 : word32.
80 : word32.
81 : word32.
82 : word32.
83 : word32.
84 : word32.
85 : word32.
86 : word32.
87 : word32.
88 : word32.
89 : word32.
90 : word32.
91 : word32.
92 : word32.
93 : word32.
94 : word32.
95 : word32.
96 : word32.
97 : word32.
98 : word32.
99 : word32.
100 : word32.
101 : word32.
102 : word32.
103 : word32.
104 : word32.
105 : word32.
106 : word32.
107 : word32.
108 : word32.
109 : word32.
110 : word32.
111 : word32.
112 : word32.
113 : word32.
114 : word32.
115 : word32.
116 : word32.
117 : word32.
118 : word32.
119 : word32.
120 : word32.
121 : word32.
122 : word32.
123 : word32.
124 : word32.
125 : word32.
126 : word32.
127 : word32.
128 : word32.
129 : word32.
130 : word32.
131 : word32.
132 : word32.
133 : word32.
134 : word32.
135 : word32.
136 : word32.
137 : word32.
138 : word32.
139 : word32.
140 : word32.
141 : word32.
142 : word32.
143 : word32.
144 : word32.
145 : word32.
146 : word32.
147 : word32.
148 : word32.
149 : word32.
150 : word32.
151 : word32.
152 : word32.
153 : word32.
154 : word32.
155 : word32.
156 : word32.
157 : word32.
158 : word32.
159 : word32.
160 : word32.
161 : word32.
162 : word32.
163 : word32.
164 : word32.
165 : word32.
166 : word32.
167 : word32.
168 : word32.
169 : word32.
170 : word32.
171 : word32.
172 : word32.
173 : word32.
174 : word32.
175 : word32.
176 : word32.
177 : word32.
178 : word32.
179 : word32.
180 : word32.
181 : word32.
182 : word32.
183 : word32.
184 : word32.
185 : word32.
186 : word32.
187 : word32.
188 : word32.
189 : word32.
190 : word32.
191 : word32.
192 : word32.
193 : word32.
194 : word32.
195 : word32.
196 : word32.
197 : word32.
198 : word32.
199 : word32.
200 : word32.
201 : word32.
202 : word32.
203 : word32.
204 : word32.
205 : word32.
206 : word32.
207 : word32.
208 : word32.
209 : word32.
210 : word32.
211 : word32.
212 : word32.
213 : word32.
214 : word32.
215 : word32.
216 : word32.
217 : word32.
218 : word32.
219 : word32.
220 : word32.
221 : word32.
222 : word32.
223 : word32.
224 : word32.
225 : word32.
226 : word32.
227 : word32.
228 : word32.
229 : word32.
230 : word32.
231 : word32.
232 : word32.
233 : word32.
234 : word32.
235 : word32.
236 : word32.
237 : word32.
238 : word32.
239 : word32.
240 : word32.
241 : word32.
242 : word32.
243 : word32.
244 : word32.
245 : word32.
246 : word32.
247 : word32.
248 : word32.
249 : word32.
250 : word32.
251 : word32.
252 : word32.
253 : word32.
254 : word32.
255 : word32.
256 : word32.
257 : word32.
258 : word32.
259 : word32.
260 : word32.
261 : word32.
262 : word32.
263 : word32.
264 : word32.
265 : word32.
266 : word32.
267 : word32.
268 : word32.
269 : word32.
270 : word32.
271 : word32.
272 : word32.
273 : word32.
274 : word32.
275 : word32.
276 : word32.
277 : word32.
278 : word32.
279 : word32.
280 : word32.
281 : word32.
282 : word32.
283 : word32.
284 : word32.
285 : word32.
286 : word32.
287 : word32.
288 : word32.
289 : word32.
290 : word32.
291 : word32.
292 : word32.
293 : word32.
294 : word32.
295 : word32.
296 : word32.
297 : word32.
298 : word32.
299 : word32.

1000 : word32.

512   : word32.
1024  : word32.
2048  : word32.
4096  : word32.
8192  : word32.
16384 : word32.
32768 : word32.
65536 : word32.
2147483648 : word32.
4294967295 : word32.
%{
Goals involving + and * are immediately solved if at least two of
the arguments are ground objects (i.e. numbers), and delayed as
constraints otherwise. In particular

?- + 3 X 9.

is solved immediately and can be used to compute 9-3. Goals involving
/ are delayed unless both the first and the second argument are
known. The type families prove+, prove*, prove/ can be used to obtain
proof object for the arithmetic operation, and use them in the
remaining part of the computation:

?- P : + 3 X 9.
Solving...
X = 6.
P = 3+6.
More? n
?- prove+ 3 X 9 P.
Solving...
P = 3+6;
X = 6.
More? n

It is important to stress that the domain modeled here is not the ring
of integers modulo 32 but rather the restriction of the integer ring
to the interval 0...4294967295, so that for example the query:

?- + 1 X 0.
will not admit a solution.
}%