blob: f94f091e8d25fdd0a3f6ec3110009333cfd39e17 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
|
type __ = Obj.t
type bool =
| True
| False
val negb : bool -> bool
type nat =
| O
| S of nat
type 'a option =
| Some of 'a
| None
type ('a, 'b) prod =
| Pair of 'a * 'b
type comparison =
| Eq
| Lt
| Gt
val compOpp : comparison -> comparison
type sumbool =
| Left
| Right
type 'a sumor =
| Inleft of 'a
| Inright
type 'a list =
| Nil
| Cons of 'a * 'a list
val app : 'a1 list -> 'a1 list -> 'a1 list
val nth : nat -> 'a1 list -> 'a1 -> 'a1
val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
type positive =
| XI of positive
| XO of positive
| XH
val psucc : positive -> positive
val pplus : positive -> positive -> positive
val pplus_carry : positive -> positive -> positive
val p_of_succ_nat : nat -> positive
val pdouble_minus_one : positive -> positive
type positive_mask =
| IsNul
| IsPos of positive
| IsNeg
val pdouble_plus_one_mask : positive_mask -> positive_mask
val pdouble_mask : positive_mask -> positive_mask
val pdouble_minus_two : positive -> positive_mask
val pminus_mask : positive -> positive -> positive_mask
val pminus_mask_carry : positive -> positive -> positive_mask
val pminus : positive -> positive -> positive
val pmult : positive -> positive -> positive
val pcompare : positive -> positive -> comparison -> comparison
type n =
| N0
| Npos of positive
type z =
| Z0
| Zpos of positive
| Zneg of positive
val zdouble_plus_one : z -> z
val zdouble_minus_one : z -> z
val zdouble : z -> z
val zPminus : positive -> positive -> z
val zplus : z -> z -> z
val zopp : z -> z
val zminus : z -> z -> z
val zmult : z -> z -> z
val zcompare : z -> z -> comparison
val dcompare_inf : comparison -> sumbool sumor
val zcompare_rec : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
val z_gt_dec : z -> z -> sumbool
val zle_bool : z -> z -> bool
val zge_bool : z -> z -> bool
val zgt_bool : z -> z -> bool
val zeq_bool : z -> z -> bool
val n_of_nat : nat -> n
val zdiv_eucl_POS : positive -> z -> (z, z) prod
val zdiv_eucl : z -> z -> (z, z) prod
type 'c pol =
| Pc of 'c
| Pinj of positive * 'c pol
| PX of 'c pol * positive * 'c pol
val p0 : 'a1 -> 'a1 pol
val p1 : 'a1 -> 'a1 pol
val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
val mkPX :
'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
val mkX : 'a1 -> 'a1 -> 'a1 pol
val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val paddI :
('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
positive -> 'a1 pol -> 'a1 pol
val psubI :
('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val paddX :
'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol
-> positive -> 'a1 pol -> 'a1 pol
val psubX :
'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val padd :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
'a1 pol
val psub :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val pmulC_aux :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1
pol
val pmulC :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
-> 'a1 pol
val pmulI :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val pmul :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
type 'c pExpr =
| PEc of 'c
| PEX of positive
| PEadd of 'c pExpr * 'c pExpr
| PEsub of 'c pExpr * 'c pExpr
| PEmul of 'c pExpr * 'c pExpr
| PEopp of 'c pExpr
| PEpow of 'c pExpr * n
val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
val ppow_pos :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
val ppow_N :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
val norm_aux :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
type 'a bFormula =
| TT
| FF
| X
| A of 'a
| Cj of 'a bFormula * 'a bFormula
| D of 'a bFormula * 'a bFormula
| N of 'a bFormula
| I of 'a bFormula * 'a bFormula
type 'term' clause = 'term' list
type 'term' cnf = 'term' clause list
val tt : 'a1 cnf
val ff : 'a1 cnf
val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf
val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
val xcnf :
('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool
val tauto_checker :
('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
bFormula -> 'a3 list -> bool
type 'c pExprC = 'c pExpr
type 'c polC = 'c pol
type op1 =
| Equal
| NonEqual
| Strict
| NonStrict
type 'c nFormula = ('c pExprC, op1) prod
type monoidMember = nat list
type 'c coneMember =
| S_In of nat
| S_Ideal of 'c pExprC * 'c coneMember
| S_Square of 'c pExprC
| S_Monoid of monoidMember
| S_Mult of 'c coneMember * 'c coneMember
| S_Add of 'c coneMember * 'c coneMember
| S_Pos of 'c
| S_Z
val nformula_times : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
val nformula_plus : 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula
val eval_monoid : 'a1 -> 'a1 nFormula list -> monoidMember -> 'a1 pExprC
val eval_cone :
'a1 -> 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula
list -> 'a1 coneMember -> 'a1 nFormula
val normalise_pexpr :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 polC
val check_inconsistent :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
nFormula -> bool
val check_normalised_formulas :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
nFormula list -> 'a1 coneMember -> bool
type op2 =
| OpEq
| OpNEq
| OpLe
| OpGe
| OpLt
| OpGt
type 'c formula = { flhs : 'c pExprC; fop : op2; frhs : 'c pExprC }
val flhs : 'a1 formula -> 'a1 pExprC
val fop : 'a1 formula -> op2
val frhs : 'a1 formula -> 'a1 pExprC
val xnormalise : 'a1 formula -> 'a1 nFormula list
val cnf_normalise : 'a1 formula -> 'a1 nFormula cnf
val xnegate : 'a1 formula -> 'a1 nFormula list
val cnf_negate : 'a1 formula -> 'a1 nFormula cnf
val simpl_expr : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pExprC -> 'a1 pExprC
val simpl_cone :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 coneMember
-> 'a1 coneMember
type q = { qnum : z; qden : positive }
val qnum : q -> z
val qden : q -> positive
val qplus : q -> q -> q
val qmult : q -> q -> q
val qopp : q -> q
val qminus : q -> q -> q
type 'a t =
| Empty
| Leaf of 'a
| Node of 'a t * 'a * 'a t
val find : 'a1 -> 'a1 t -> positive -> 'a1
type zWitness = z coneMember
val zWeakChecker : z nFormula list -> z coneMember -> bool
val xnormalise0 : z formula -> z nFormula list
val normalise : z formula -> z nFormula cnf
val xnegate0 : z formula -> z nFormula list
val negate : z formula -> z nFormula cnf
val ceiling : z -> z -> z
type proofTerm =
| RatProof of zWitness
| CutProof of z pExprC * q * zWitness * proofTerm
| EnumProof of q * z pExprC * q * zWitness * zWitness * proofTerm list
val makeLb : z pExpr -> q -> z nFormula
val qceiling : q -> z
val makeLbCut : z pExprC -> q -> z nFormula
val neg_nformula : z nFormula -> (z pExpr, op1) prod
val cutChecker :
z nFormula list -> z pExpr -> q -> zWitness -> z nFormula option
val zChecker : z nFormula list -> proofTerm -> bool
val zTautoChecker : z formula bFormula -> proofTerm list -> bool
val map_cone : (nat -> nat) -> zWitness -> zWitness
val indexes : zWitness -> nat list
val n_of_Z : z -> n
val qeq_bool : q -> q -> bool
val qle_bool : q -> q -> bool
type qWitness = q coneMember
val qWeakChecker : q nFormula list -> q coneMember -> bool
val qTautoChecker : q formula bFormula -> qWitness list -> bool
|
