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
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
|
%------------------------------------------------------------------------------
% File : MSC001-2 : TPTP v6.4.0. Released v3.2.0.
% Domain : Miscellaneous
% Axioms : Sets, numbers, lists, etc, that make up the Isabelle/HOL library
% Version : [Pau06] axioms.
% English : The files MSC001-[012].ax .ax are really about everything: sets,
% numbers, lists and all the other things that make up the basic
% Isabelle/HOL library. Also, many of the axioms in MSC001-0.ax
% describe the Isabelle/HOL type class hierarchy.
% Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe
% Source : [Pau06]
% Names : set.ax [Pau06]
% Status : Satisfiable
% Syntax : Number of clauses : 198 ( 11 non-Horn; 57 unit; 166 RR)
% Number of atoms : 371 ( 157 equality)
% Maximal clause size : 3 ( 2 average)
% Number of predicates : 10 ( 0 propositional; 1-3 arity)
% Number of functors : 60 ( 15 constant; 0-4 arity)
% Number of variables : 557 ( 144 singleton)
% Maximal term depth : 4 ( 1 average)
% SPC :
% Comments : Requires MSC001-0.ax
%------------------------------------------------------------------------------
cnf(cls_Datatype_Oelem__o2s__iff1_0,axiom,
( ~ c_in(V_x,c_Datatype_Oo2s(V_xo,T_a),T_a)
| V_xo = c_Datatype_Ooption_OSome(V_x,T_a) )).
cnf(cls_Datatype_Oelem__o2s__iff2_0,axiom,
( c_in(V_x,c_Datatype_Oo2s(c_Datatype_Ooption_OSome(V_x,T_a),T_a),T_a) )).
cnf(cls_Datatype_Onot__None__eq__iff1_0,axiom,
( V_x = c_Datatype_Ooption_ONone
| V_x = c_Datatype_Ooption_OSome(c_Main_Onot__None__eq__iff1__1(V_x,T_a),T_a) )).
cnf(cls_Datatype_Onot__Some__eq__iff1_0,axiom,
( V_x = c_Datatype_Ooption_ONone
| V_x = c_Datatype_Ooption_OSome(c_Main_Onot__Some__eq__iff1__1(V_x,T_a),T_a) )).
cnf(cls_Datatype_Ooption_Odistinct__1__iff1_0,axiom,
( c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a) )).
cnf(cls_Datatype_Ooption_Odistinct__2__iff1_0,axiom,
( c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone )).
cnf(cls_Datatype_Ooption_Oinject__iff1_0,axiom,
( c_Datatype_Ooption_OSome(V_a,T_a) != c_Datatype_Ooption_OSome(V_a_H,T_a)
| V_a = V_a_H )).
cnf(cls_Datatype__Universe_OAtom__Atom__eq__iff1_0,axiom,
( c_Datatype__Universe_OAtom(V_a,T_a,T_b) != c_Datatype__Universe_OAtom(V_b,T_a,T_b)
| V_a = V_b )).
cnf(cls_Datatype__Universe_OAtom__not__Scons__iff1_0,axiom,
( c_Datatype__Universe_OAtom(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) )).
cnf(cls_Datatype__Universe_OIn0__eq__iff1_0,axiom,
( c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn0(V_N,T_a,T_b)
| V_M = V_N )).
cnf(cls_Datatype__Universe_OIn0__not__In1__iff1_0,axiom,
( c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b) )).
cnf(cls_Datatype__Universe_OIn1__eq__iff1_0,axiom,
( c_Datatype__Universe_OIn1(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b)
| V_M = V_N )).
cnf(cls_Datatype__Universe_OIn1__not__In0__iff1_0,axiom,
( c_Datatype__Universe_OIn1(V_N,T_a,T_b) != c_Datatype__Universe_OIn0(V_M,T_a,T_b) )).
cnf(cls_Datatype__Universe_OLeaf__not__Numb__iff1_0,axiom,
( c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b) )).
cnf(cls_Datatype__Universe_OLeaf__not__Scons__iff1_0,axiom,
( c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) )).
cnf(cls_Datatype__Universe_ONumb__not__Leaf__iff1_0,axiom,
( c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b) )).
cnf(cls_Datatype__Universe_ONumb__not__Scons__iff1_0,axiom,
( c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) )).
cnf(cls_Datatype__Universe_OScons__Scons__eq__iff1_0,axiom,
( c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OScons(V_M_H,V_N_H,T_a,T_b)
| V_M = V_M_H )).
cnf(cls_Datatype__Universe_OScons__Scons__eq__iff1_1,axiom,
( c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OScons(V_M_H,V_N_H,T_a,T_b)
| V_N = V_N_H )).
cnf(cls_Datatype__Universe_OScons__not__Atom__iff1_0,axiom,
( c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OAtom(V_a,T_a,T_b) )).
cnf(cls_Datatype__Universe_OScons__not__Leaf__iff1_0,axiom,
( c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b) )).
cnf(cls_Datatype__Universe_OScons__not__Numb__iff1_0,axiom,
( c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b) )).
cnf(cls_Divides_Odvd__0__left__iff__iff1_0,axiom,
( ~ c_Divides_Oop_Advd(c_0,V_m,tc_nat)
| V_m = c_0 )).
cnf(cls_Divides_Odvd__0__left__iff__iff2_0,axiom,
( c_Divides_Oop_Advd(c_0,c_0,tc_nat) )).
cnf(cls_Equiv__Relations_Oquotient__is__empty2__iff1_0,axiom,
( c_emptyset != c_Equiv__Relations_Oquotient(V_A,V_r,T_a)
| V_A = c_emptyset )).
cnf(cls_Equiv__Relations_Oquotient__is__empty2__iff2_0,axiom,
( c_emptyset = c_Equiv__Relations_Oquotient(c_emptyset,V_r,T_a) )).
cnf(cls_Equiv__Relations_Oquotient__is__empty__iff1_0,axiom,
( c_Equiv__Relations_Oquotient(V_A,V_r,T_a) != c_emptyset
| V_A = c_emptyset )).
cnf(cls_Equiv__Relations_Oquotient__is__empty__iff2_0,axiom,
( c_Equiv__Relations_Oquotient(c_emptyset,V_r,T_a) = c_emptyset )).
cnf(cls_Extraction_Osumbool_Odistinct__1__iff1_0,axiom,
( c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight )).
cnf(cls_Extraction_Osumbool_Odistinct__2__iff1_0,axiom,
( c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft )).
cnf(cls_Finite__Set_Ofinite__Diff__insert__iff1_0,axiom,
( ~ c_in(c_minus(V_A,c_insert(V_a,V_B,T_a),tc_set(T_a)),c_Finite__Set_OFinites,tc_set(T_a))
| c_in(c_minus(V_A,V_B,tc_set(T_a)),c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__Diff__insert__iff2_0,axiom,
( ~ c_in(c_minus(V_A,V_B,tc_set(T_a)),c_Finite__Set_OFinites,tc_set(T_a))
| c_in(c_minus(V_A,c_insert(V_a,V_B,T_a),tc_set(T_a)),c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__Pow__iff__iff1_0,axiom,
( ~ c_in(c_Pow(V_A,T_a),c_Finite__Set_OFinites,tc_set(tc_set(T_a)))
| c_in(V_A,c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__Pow__iff__iff2_0,axiom,
( ~ c_in(V_A,c_Finite__Set_OFinites,tc_set(T_a))
| c_in(c_Pow(V_A,T_a),c_Finite__Set_OFinites,tc_set(tc_set(T_a))) )).
cnf(cls_Finite__Set_Ofinite__Un__iff1_0,axiom,
( ~ c_in(c_union(V_F,V_G,T_a),c_Finite__Set_OFinites,tc_set(T_a))
| c_in(V_F,c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__Un__iff1_1,axiom,
( ~ c_in(c_union(V_F,V_G,T_a),c_Finite__Set_OFinites,tc_set(T_a))
| c_in(V_G,c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__Un__iff2_0,axiom,
( ~ c_in(V_G,c_Finite__Set_OFinites,tc_set(T_a))
| ~ c_in(V_F,c_Finite__Set_OFinites,tc_set(T_a))
| c_in(c_union(V_F,V_G,T_a),c_Finite__Set_OFinites,tc_set(T_a)) )).
cnf(cls_Finite__Set_Ofinite__converse__iff1_0,axiom,
( ~ c_in(c_Relation_Oconverse(V_r,T_b,T_a),c_Finite__Set_OFinites,tc_set(tc_prod(T_a,T_b)))
| c_in(V_r,c_Finite__Set_OFinites,tc_set(tc_prod(T_b,T_a))) )).
cnf(cls_Finite__Set_Ofinite__converse__iff2_0,axiom,
( ~ c_in(V_r,c_Finite__Set_OFinites,tc_set(tc_prod(T_b,T_a)))
| c_in(c_Relation_Oconverse(V_r,T_b,T_a),c_Finite__Set_OFinites,tc_set(tc_prod(T_a,T_b))) )).
cnf(cls_GCD_Ogcd__greatest__iff__iff1_0,axiom,
( ~ c_Divides_Oop_Advd(V_k,c_GCD_Ogcd(c_Pair(V_m,V_n,tc_nat,tc_nat)),tc_nat)
| c_Divides_Oop_Advd(V_k,V_m,tc_nat) )).
cnf(cls_GCD_Ogcd__greatest__iff__iff1_1,axiom,
( ~ c_Divides_Oop_Advd(V_k,c_GCD_Ogcd(c_Pair(V_m,V_n,tc_nat,tc_nat)),tc_nat)
| c_Divides_Oop_Advd(V_k,V_n,tc_nat) )).
cnf(cls_GCD_Ogcd__greatest__iff__iff2_0,axiom,
( ~ c_Divides_Oop_Advd(V_k,V_n,tc_nat)
| ~ c_Divides_Oop_Advd(V_k,V_m,tc_nat)
| c_Divides_Oop_Advd(V_k,c_GCD_Ogcd(c_Pair(V_m,V_n,tc_nat,tc_nat)),tc_nat) )).
cnf(cls_Infinite__Set_Onat__not__finite_0,axiom,
( ~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)) )).
cnf(cls_IntDef_Oint__int__eq__iff1_0,axiom,
( c_IntDef_Oint(V_m) != c_IntDef_Oint(V_n)
| V_m = V_n )).
cnf(cls_IntDiv_Odvd__zminus__iff__iff1_0,axiom,
( ~ c_Divides_Oop_Advd(V_z,c_uminus(V_w,tc_IntDef_Oint),tc_IntDef_Oint)
| c_Divides_Oop_Advd(V_z,V_w,tc_IntDef_Oint) )).
cnf(cls_IntDiv_Odvd__zminus__iff__iff2_0,axiom,
( ~ c_Divides_Oop_Advd(V_z,V_w,tc_IntDef_Oint)
| c_Divides_Oop_Advd(V_z,c_uminus(V_w,tc_IntDef_Oint),tc_IntDef_Oint) )).
cnf(cls_IntDiv_Ozdvd__0__left__iff1_0,axiom,
( ~ c_Divides_Oop_Advd(c_0,V_m,tc_IntDef_Oint)
| V_m = c_0 )).
cnf(cls_IntDiv_Ozdvd__0__left__iff2_0,axiom,
( c_Divides_Oop_Advd(c_0,c_0,tc_IntDef_Oint) )).
cnf(cls_IntDiv_Ozminus__dvd__iff__iff1_0,axiom,
( ~ c_Divides_Oop_Advd(c_uminus(V_z,tc_IntDef_Oint),V_w,tc_IntDef_Oint)
| c_Divides_Oop_Advd(V_z,V_w,tc_IntDef_Oint) )).
cnf(cls_IntDiv_Ozminus__dvd__iff__iff2_0,axiom,
( ~ c_Divides_Oop_Advd(V_z,V_w,tc_IntDef_Oint)
| c_Divides_Oop_Advd(c_uminus(V_z,tc_IntDef_Oint),V_w,tc_IntDef_Oint) )).
cnf(cls_List_ONil2__notin__lex__iff1_0,axiom,
( ~ c_in(c_Pair(V_xs,c_List_Olist_ONil,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))) )).
cnf(cls_List_ONil__is__append__conv__iff1_0,axiom,
( c_List_Olist_ONil != c_append(V_xs,V_ys,T_a)
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_ONil__is__append__conv__iff1_1,axiom,
( c_List_Olist_ONil != c_append(V_xs,V_ys,T_a)
| V_ys = c_List_Olist_ONil )).
cnf(cls_List_ONil__is__append__conv__iff2_0,axiom,
( c_List_Olist_ONil = c_append(c_List_Olist_ONil,c_List_Olist_ONil,T_a) )).
cnf(cls_List_ONil__is__rev__conv__iff1_0,axiom,
( c_List_Olist_ONil != c_List_Orev(V_xs,T_a)
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_ONil__is__rev__conv__iff2_0,axiom,
( c_List_Olist_ONil = c_List_Orev(c_List_Olist_ONil,T_a) )).
cnf(cls_List_ONil__notin__lex__iff1_0,axiom,
( ~ c_in(c_Pair(c_List_Olist_ONil,V_ys,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))) )).
cnf(cls_List_Oappend1__eq__conv__iff1_0,axiom,
( c_append(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil,T_a),T_a) != c_append(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a)
| V_xs = V_ys )).
cnf(cls_List_Oappend1__eq__conv__iff1_1,axiom,
( c_append(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil,T_a),T_a) != c_append(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a)
| V_x = V_y )).
cnf(cls_List_Oappend__in__lists__conv__iff1_0,axiom,
( ~ c_in(c_append(V_xs,V_ys,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) )).
cnf(cls_List_Oappend__in__lists__conv__iff1_1,axiom,
( ~ c_in(c_append(V_xs,V_ys,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| c_in(V_ys,c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) )).
cnf(cls_List_Oappend__in__lists__conv__iff2_0,axiom,
( ~ c_in(V_ys,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| ~ c_in(V_xs,c_List_Olists(V_A,T_a),tc_List_Olist(T_a))
| c_in(c_append(V_xs,V_ys,T_a),c_List_Olists(V_A,T_a),tc_List_Olist(T_a)) )).
cnf(cls_List_Oappend__is__Nil__conv__iff1_0,axiom,
( c_append(V_xs,V_ys,T_a) != c_List_Olist_ONil
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Oappend__is__Nil__conv__iff1_1,axiom,
( c_append(V_xs,V_ys,T_a) != c_List_Olist_ONil
| V_ys = c_List_Olist_ONil )).
cnf(cls_List_Oappend__is__Nil__conv__iff2_0,axiom,
( c_append(c_List_Olist_ONil,c_List_Olist_ONil,T_a) = c_List_Olist_ONil )).
cnf(cls_List_Oappend__same__eq__iff1_0,axiom,
( c_append(V_ys,V_xs,T_a) != c_append(V_zs,V_xs,T_a)
| V_ys = V_zs )).
cnf(cls_List_Oappend__self__conv2__iff1_0,axiom,
( c_append(V_xs,V_ys,T_a) != V_ys
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Oappend__self__conv2__iff2_0,axiom,
( c_append(c_List_Olist_ONil,V_ys,T_a) = V_ys )).
cnf(cls_List_Oappend__self__conv__iff1_0,axiom,
( c_append(V_xs,V_ys,T_a) != V_xs
| V_ys = c_List_Olist_ONil )).
cnf(cls_List_Oappend__self__conv__iff2_0,axiom,
( c_append(V_xs,c_List_Olist_ONil,T_a) = V_xs )).
cnf(cls_List_Ochar_Oinject__iff1_0,axiom,
( c_List_Ochar_OChar(V_nibble1,V_nibble2) != c_List_Ochar_OChar(V_nibble1_H,V_nibble2_H)
| V_nibble1 = V_nibble1_H )).
cnf(cls_List_Ochar_Oinject__iff1_1,axiom,
( c_List_Ochar_OChar(V_nibble1,V_nibble2) != c_List_Ochar_OChar(V_nibble1_H,V_nibble2_H)
| V_nibble2 = V_nibble2_H )).
cnf(cls_List_Olength__0__conv__iff1_0,axiom,
( c_Nat_Osize(V_xs,tc_List_Olist(T_a)) != c_0
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Olength__0__conv__iff2_0,axiom,
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)) = c_0 )).
cnf(cls_List_Olength__greater__0__conv__iff1_0,axiom,
( ~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)),tc_nat) )).
cnf(cls_List_Olength__greater__0__conv__iff2_0,axiom,
( c_less(c_0,c_Nat_Osize(V_xs,tc_List_Olist(T_a)),tc_nat)
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Olength__remdups__eq__iff1_0,axiom,
( c_Nat_Osize(c_List_Oremdups(V_xs,T_a),tc_List_Olist(T_a)) != c_Nat_Osize(V_xs,tc_List_Olist(T_a))
| c_List_Oremdups(V_xs,T_a) = V_xs )).
cnf(cls_List_Olength__remdups__eq__iff2_0,axiom,
( c_List_Oremdups(V_xs,T_a) != V_xs
| c_Nat_Osize(c_List_Oremdups(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize(V_xs,tc_List_Olist(T_a)) )).
cnf(cls_List_Olist_Odistinct__1__iff1_0,axiom,
( c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a) )).
cnf(cls_List_Olist_Odistinct__2__iff1_0,axiom,
( c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil )).
cnf(cls_List_Olist_Oinject__iff1_0,axiom,
( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a)
| V_a = V_a_H )).
cnf(cls_List_Olist_Oinject__iff1_1,axiom,
( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a)
| V_list = V_list_H )).
cnf(cls_List_Orev__eq__Cons__iff__iff1_0,axiom,
( c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a)
| V_xs = c_append(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a) )).
cnf(cls_List_Orev__eq__Cons__iff__iff2_0,axiom,
( c_List_Orev(c_append(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil,T_a),T_a),T_a) = c_List_Olist_OCons(V_y,V_ys,T_a) )).
cnf(cls_List_Orev__is__Nil__conv__iff1_0,axiom,
( c_List_Orev(V_xs,T_a) != c_List_Olist_ONil
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Orev__is__Nil__conv__iff2_0,axiom,
( c_List_Orev(c_List_Olist_ONil,T_a) = c_List_Olist_ONil )).
cnf(cls_List_Orev__is__rev__conv__iff1_0,axiom,
( c_List_Orev(V_xs,T_a) != c_List_Orev(V_ys,T_a)
| V_xs = V_ys )).
cnf(cls_List_Osame__append__eq__iff1_0,axiom,
( c_append(V_xs,V_ys,T_a) != c_append(V_xs,V_zs,T_a)
| V_ys = V_zs )).
cnf(cls_List_Oself__append__conv2__iff1_0,axiom,
( V_ys != c_append(V_xs,V_ys,T_a)
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Oself__append__conv2__iff2_0,axiom,
( V_ys = c_append(c_List_Olist_ONil,V_ys,T_a) )).
cnf(cls_List_Oself__append__conv__iff1_0,axiom,
( V_xs != c_append(V_xs,V_ys,T_a)
| V_ys = c_List_Olist_ONil )).
cnf(cls_List_Oself__append__conv__iff2_0,axiom,
( V_xs = c_append(V_xs,c_List_Olist_ONil,T_a) )).
cnf(cls_List_Oset__empty2__iff1_0,axiom,
( c_emptyset != c_List_Oset(V_xs,T_a)
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Oset__empty2__iff2_0,axiom,
( c_emptyset = c_List_Oset(c_List_Olist_ONil,T_a) )).
cnf(cls_List_Oset__empty__iff1_0,axiom,
( c_List_Oset(V_xs,T_a) != c_emptyset
| V_xs = c_List_Olist_ONil )).
cnf(cls_List_Oset__empty__iff2_0,axiom,
( c_List_Oset(c_List_Olist_ONil,T_a) = c_emptyset )).
cnf(cls_Nat_OSuc__Suc__eq__iff1_0,axiom,
( c_Suc(V_m) != c_Suc(V_n)
| V_m = V_n )).
cnf(cls_Nat_OSuc__le__mono__iff1_0,axiom,
( ~ c_lessequals(c_Suc(V_n),c_Suc(V_m),tc_nat)
| c_lessequals(V_n,V_m,tc_nat) )).
cnf(cls_Nat_OSuc__le__mono__iff2_0,axiom,
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_lessequals(c_Suc(V_n),c_Suc(V_m),tc_nat) )).
cnf(cls_Nat_OSuc__less__eq__iff1_0,axiom,
( ~ c_less(c_Suc(V_m),c_Suc(V_n),tc_nat)
| c_less(V_m,V_n,tc_nat) )).
cnf(cls_Nat_OSuc__less__eq__iff2_0,axiom,
( ~ c_less(V_m,V_n,tc_nat)
| c_less(c_Suc(V_m),c_Suc(V_n),tc_nat) )).
cnf(cls_Nat_OSuc__not__Zero__iff1_0,axiom,
( c_Suc(V_m) != c_0 )).
cnf(cls_Nat_OZero__not__Suc__iff1_0,axiom,
( c_0 != c_Suc(V_m) )).
cnf(cls_Nat_Oadd__gr__0__iff1_0,axiom,
( ~ c_less(c_0,c_plus(V_m,V_n,tc_nat),tc_nat)
| c_less(c_0,V_n,tc_nat)
| c_less(c_0,V_m,tc_nat) )).
cnf(cls_Nat_Oadd__gr__0__iff2_0,axiom,
( ~ c_less(c_0,V_m,tc_nat)
| c_less(c_0,c_plus(V_m,V_n,tc_nat),tc_nat) )).
cnf(cls_Nat_Oadd__gr__0__iff2_1,axiom,
( ~ c_less(c_0,V_n,tc_nat)
| c_less(c_0,c_plus(V_m,V_n,tc_nat),tc_nat) )).
cnf(cls_Nat_Oadd__is__0__iff1_0,axiom,
( c_plus(V_m,V_n,tc_nat) != c_0
| V_m = c_0 )).
cnf(cls_Nat_Oadd__is__0__iff1_1,axiom,
( c_plus(V_m,V_n,tc_nat) != c_0
| V_n = c_0 )).
cnf(cls_Nat_Oadd__is__0__iff2_0,axiom,
( c_plus(c_0,c_0,tc_nat) = c_0 )).
cnf(cls_Nat_Ole__0__eq__iff1_0,axiom,
( ~ c_lessequals(V_i,c_0,tc_nat)
| V_i = c_0 )).
cnf(cls_Nat_Ole__0__eq__iff2_0,axiom,
( c_lessequals(c_0,c_0,tc_nat) )).
cnf(cls_Nat_Oless__Suc0__iff1_0,axiom,
( ~ c_less(V_n,c_Suc(c_0),tc_nat)
| V_n = c_0 )).
cnf(cls_Nat_Oless__Suc0__iff2_0,axiom,
( c_less(c_0,c_Suc(c_0),tc_nat) )).
cnf(cls_Nat_Oless__one__iff1_0,axiom,
( ~ c_less(V_n,c_1,tc_nat)
| V_n = c_0 )).
cnf(cls_Nat_Oless__one__iff2_0,axiom,
( c_less(c_0,c_1,tc_nat) )).
cnf(cls_Nat_Oneq0__conv__iff1_0,axiom,
( c_less(c_0,V_n,tc_nat)
| V_n = c_0 )).
cnf(cls_Nat_Oneq0__conv__iff2_0,axiom,
( ~ c_less(c_0,c_0,tc_nat) )).
cnf(cls_Nat_Onot__add__less1__iff1_0,axiom,
( ~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat) )).
cnf(cls_Nat_Onot__add__less2__iff1_0,axiom,
( ~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat) )).
cnf(cls_Nat_Onot__less0__iff1_0,axiom,
( ~ c_less(V_n,c_0,tc_nat) )).
cnf(cls_Numeral_Obit_Odistinct__1__iff1_0,axiom,
( c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1 )).
cnf(cls_Numeral_Obit_Odistinct__2__iff1_0,axiom,
( c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0 )).
cnf(cls_Orderings_Oorder__less__irrefl__iff1_0,axiom,
( ~ class_Orderings_Oorder(T_a)
| ~ c_less(V_x,V_x,T_a) )).
cnf(cls_Product__Type_OPair__eq__iff1_0,axiom,
( c_Pair(V_a,V_b,T_a,T_b) != c_Pair(V_a_H,V_b_H,T_a,T_b)
| V_a = V_a_H )).
cnf(cls_Product__Type_OPair__eq__iff1_1,axiom,
( c_Pair(V_a,V_b,T_a,T_b) != c_Pair(V_a_H,V_b_H,T_a,T_b)
| V_b = V_b_H )).
cnf(cls_Relation_OIdI_0,axiom,
( c_in(c_Pair(V_a,V_a,T_a,T_a),c_Relation_OId,tc_prod(T_a,T_a)) )).
cnf(cls_Relation_OImage__singleton__iff__iff1_0,axiom,
( ~ c_in(V_b,c_Relation_OImage(V_r,c_insert(V_a,c_emptyset,T_b),T_b,T_a),T_a)
| c_in(c_Pair(V_a,V_b,T_b,T_a),V_r,tc_prod(T_b,T_a)) )).
cnf(cls_Relation_OImage__singleton__iff__iff2_0,axiom,
( ~ c_in(c_Pair(V_a,V_b,T_b,T_a),V_r,tc_prod(T_b,T_a))
| c_in(V_b,c_Relation_OImage(V_r,c_insert(V_a,c_emptyset,T_b),T_b,T_a),T_a) )).
cnf(cls_Relation_Oconverse__iff__iff1_0,axiom,
( ~ c_in(c_Pair(V_a,V_b,T_a,T_b),c_Relation_Oconverse(V_r,T_b,T_a),tc_prod(T_a,T_b))
| c_in(c_Pair(V_b,V_a,T_b,T_a),V_r,tc_prod(T_b,T_a)) )).
cnf(cls_Relation_Oconverse__iff__iff2_0,axiom,
( ~ c_in(c_Pair(V_b,V_a,T_b,T_a),V_r,tc_prod(T_b,T_a))
| c_in(c_Pair(V_a,V_b,T_a,T_b),c_Relation_Oconverse(V_r,T_b,T_a),tc_prod(T_a,T_b)) )).
cnf(cls_Relation_Opair__in__Id__conv__iff1_0,axiom,
( ~ c_in(c_Pair(V_a,V_b,T_a,T_a),c_Relation_OId,tc_prod(T_a,T_a))
| V_a = V_b )).
cnf(cls_SetInterval_OatLeast__eq__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| c_SetInterval_OatLeast(V_x,T_a) != c_SetInterval_OatLeast(V_y,T_a)
| V_x = V_y )).
cnf(cls_SetInterval_OatLeast__iff__iff1_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_in(V_i,c_SetInterval_OatLeast(V_k,T_a),T_a)
| c_lessequals(V_k,V_i,T_a) )).
cnf(cls_SetInterval_OatLeast__iff__iff2_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_lessequals(V_k,V_i,T_a)
| c_in(V_i,c_SetInterval_OatLeast(V_k,T_a),T_a) )).
cnf(cls_SetInterval_OatLeast__subset__iff__iff1_0,axiom,
( ~ class_Orderings_Oorder(T_a)
| ~ c_lessequals(c_SetInterval_OatLeast(V_x,T_a),c_SetInterval_OatLeast(V_y,T_a),tc_set(T_a))
| c_lessequals(V_y,V_x,T_a) )).
cnf(cls_SetInterval_OatLeast__subset__iff__iff2_0,axiom,
( ~ class_Orderings_Oorder(T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| c_lessequals(c_SetInterval_OatLeast(V_x,T_a),c_SetInterval_OatLeast(V_y,T_a),tc_set(T_a)) )).
cnf(cls_SetInterval_OatMost__eq__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| c_SetInterval_OatMost(V_x,T_a) != c_SetInterval_OatMost(V_y,T_a)
| V_x = V_y )).
cnf(cls_SetInterval_OatMost__iff__iff1_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_in(V_i,c_SetInterval_OatMost(V_k,T_a),T_a)
| c_lessequals(V_i,V_k,T_a) )).
cnf(cls_SetInterval_OatMost__iff__iff2_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_lessequals(V_i,V_k,T_a)
| c_in(V_i,c_SetInterval_OatMost(V_k,T_a),T_a) )).
cnf(cls_SetInterval_OatMost__subset__iff__iff1_0,axiom,
( ~ class_Orderings_Oorder(T_a)
| ~ c_lessequals(c_SetInterval_OatMost(V_x,T_a),c_SetInterval_OatMost(V_y,T_a),tc_set(T_a))
| c_lessequals(V_x,V_y,T_a) )).
cnf(cls_SetInterval_OatMost__subset__iff__iff2_0,axiom,
( ~ class_Orderings_Oorder(T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| c_lessequals(c_SetInterval_OatMost(V_x,T_a),c_SetInterval_OatMost(V_y,T_a),tc_set(T_a)) )).
cnf(cls_SetInterval_OgreaterThan__eq__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| c_SetInterval_OgreaterThan(V_x,T_a) != c_SetInterval_OgreaterThan(V_y,T_a)
| V_x = V_y )).
cnf(cls_SetInterval_OgreaterThan__iff__iff1_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_in(V_i,c_SetInterval_OgreaterThan(V_k,T_a),T_a)
| c_less(V_k,V_i,T_a) )).
cnf(cls_SetInterval_OgreaterThan__iff__iff2_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_less(V_k,V_i,T_a)
| c_in(V_i,c_SetInterval_OgreaterThan(V_k,T_a),T_a) )).
cnf(cls_SetInterval_OgreaterThan__subset__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| ~ c_lessequals(c_SetInterval_OgreaterThan(V_x,T_a),c_SetInterval_OgreaterThan(V_y,T_a),tc_set(T_a))
| c_lessequals(V_y,V_x,T_a) )).
cnf(cls_SetInterval_OgreaterThan__subset__iff__iff2_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| c_lessequals(c_SetInterval_OgreaterThan(V_x,T_a),c_SetInterval_OgreaterThan(V_y,T_a),tc_set(T_a)) )).
cnf(cls_SetInterval_OlessThan__eq__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| c_SetInterval_OlessThan(V_x,T_a) != c_SetInterval_OlessThan(V_y,T_a)
| V_x = V_y )).
cnf(cls_SetInterval_OlessThan__iff__iff1_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_in(V_i,c_SetInterval_OlessThan(V_k,T_a),T_a)
| c_less(V_i,V_k,T_a) )).
cnf(cls_SetInterval_OlessThan__iff__iff2_0,axiom,
( ~ class_Orderings_Oord(T_a)
| ~ c_less(V_i,V_k,T_a)
| c_in(V_i,c_SetInterval_OlessThan(V_k,T_a),T_a) )).
cnf(cls_SetInterval_OlessThan__subset__iff__iff1_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| ~ c_lessequals(c_SetInterval_OlessThan(V_x,T_a),c_SetInterval_OlessThan(V_y,T_a),tc_set(T_a))
| c_lessequals(V_x,V_y,T_a) )).
cnf(cls_SetInterval_OlessThan__subset__iff__iff2_0,axiom,
( ~ class_Orderings_Olinorder(T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| c_lessequals(c_SetInterval_OlessThan(V_x,T_a),c_SetInterval_OlessThan(V_y,T_a),tc_set(T_a)) )).
cnf(cls_Set_OComplD__dest_0,axiom,
( ~ c_in(V_c,V_A,T_a)
| ~ c_in(V_c,c_uminus(V_A,tc_set(T_a)),T_a) )).
cnf(cls_Set_OComplI_0,axiom,
( c_in(V_c,V_A,T_a)
| c_in(V_c,c_uminus(V_A,tc_set(T_a)),T_a) )).
cnf(cls_Set_OCompl__eq__Compl__iff__iff1_0,axiom,
( c_uminus(V_A,tc_set(T_a)) != c_uminus(V_B,tc_set(T_a))
| V_A = V_B )).
cnf(cls_Set_OCompl__subset__Compl__iff__iff1_0,axiom,
( ~ c_lessequals(c_uminus(V_A,tc_set(T_a)),c_uminus(V_B,tc_set(T_a)),tc_set(T_a))
| c_lessequals(V_B,V_A,tc_set(T_a)) )).
cnf(cls_Set_OCompl__subset__Compl__iff__iff2_0,axiom,
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| c_lessequals(c_uminus(V_A,tc_set(T_a)),c_uminus(V_B,tc_set(T_a)),tc_set(T_a)) )).
cnf(cls_Set_ODiffE_0,axiom,
( ~ c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a) )).
cnf(cls_Set_ODiffE_1,axiom,
( ~ c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a)
| c_in(V_c,V_A,T_a) )).
cnf(cls_Set_ODiffI_0,axiom,
( ~ c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a) )).
cnf(cls_Set_OIntE_0,axiom,
( ~ c_in(V_c,c_inter(V_A,V_B,T_a),T_a)
| c_in(V_c,V_B,T_a) )).
cnf(cls_Set_OIntE_1,axiom,
( ~ c_in(V_c,c_inter(V_A,V_B,T_a),T_a)
| c_in(V_c,V_A,T_a) )).
cnf(cls_Set_OIntI_0,axiom,
( ~ c_in(V_c,V_B,T_a)
| ~ c_in(V_c,V_A,T_a)
| c_in(V_c,c_inter(V_A,V_B,T_a),T_a) )).
cnf(cls_Set_OInterD_0,axiom,
( ~ c_in(V_X,V_C,tc_set(T_a))
| ~ c_in(V_A,c_Inter(V_C,T_a),T_a)
| c_in(V_A,V_X,T_a) )).
cnf(cls_Set_OPow__iff__iff1_0,axiom,
( ~ c_in(V_A,c_Pow(V_B,T_a),tc_set(T_a))
| c_lessequals(V_A,V_B,tc_set(T_a)) )).
cnf(cls_Set_OPow__iff__iff2_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(V_A,c_Pow(V_B,T_a),tc_set(T_a)) )).
cnf(cls_Set_OUNIV__not__empty__iff1_0,axiom,
( c_UNIV != c_emptyset )).
cnf(cls_Set_OUnCI_0,axiom,
( ~ c_in(V_c,V_B,T_a)
| c_in(V_c,c_union(V_A,V_B,T_a),T_a) )).
cnf(cls_Set_OUnCI_1,axiom,
( ~ c_in(V_c,V_A,T_a)
| c_in(V_c,c_union(V_A,V_B,T_a),T_a) )).
cnf(cls_Set_OUnE_0,axiom,
( ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| c_in(V_c,V_B,T_a)
| c_in(V_c,V_A,T_a) )).
cnf(cls_Set_OUn__empty__iff1_0,axiom,
( c_union(V_A,V_B,T_a) != c_emptyset
| V_A = c_emptyset )).
cnf(cls_Set_OUn__empty__iff1_1,axiom,
( c_union(V_A,V_B,T_a) != c_emptyset
| V_B = c_emptyset )).
cnf(cls_Set_OUn__empty__iff2_0,axiom,
( c_union(c_emptyset,c_emptyset,T_a) = c_emptyset )).
cnf(cls_Set_OUnionI_0,axiom,
( ~ c_in(V_A,V_X,T_a)
| ~ c_in(V_X,V_C,tc_set(T_a))
| c_in(V_A,c_Union(V_C,T_a),T_a) )).
cnf(cls_Set_OemptyE_0,axiom,
( ~ c_in(V_a,c_emptyset,T_a) )).
cnf(cls_Set_OinsertCI_0,axiom,
( ~ c_in(V_a,V_B,T_a)
| c_in(V_a,c_insert(V_b,V_B,T_a),T_a) )).
cnf(cls_Set_OinsertCI_1,axiom,
( c_in(V_x,c_insert(V_x,V_B,T_a),T_a) )).
cnf(cls_Set_OinsertE_0,axiom,
( ~ c_in(V_a,c_insert(V_b,V_A,T_a),T_a)
| c_in(V_a,V_A,T_a)
| V_a = V_b )).
cnf(cls_Set_Onot__psubset__empty__iff1_0,axiom,
( ~ c_less(V_A,c_emptyset,tc_set(T_a)) )).
cnf(cls_Set_Osingleton__insert__inj__eq_H__iff1_0,axiom,
( c_insert(V_a,V_A,T_a) != c_insert(V_b,c_emptyset,T_a)
| V_a = V_b )).
cnf(cls_Set_Osingleton__insert__inj__eq_H__iff1_1,axiom,
( c_insert(V_a,V_A,T_a) != c_insert(V_b,c_emptyset,T_a)
| c_lessequals(V_A,c_insert(V_b,c_emptyset,T_a),tc_set(T_a)) )).
cnf(cls_Set_Osingleton__insert__inj__eq_H__iff2_0,axiom,
( ~ c_lessequals(V_A,c_insert(V_x,c_emptyset,T_a),tc_set(T_a))
| c_insert(V_x,V_A,T_a) = c_insert(V_x,c_emptyset,T_a) )).
cnf(cls_Set_Osingleton__insert__inj__eq__iff1_0,axiom,
( c_insert(V_b,c_emptyset,T_a) != c_insert(V_a,V_A,T_a)
| V_a = V_b )).
cnf(cls_Set_Osingleton__insert__inj__eq__iff1_1,axiom,
( c_insert(V_b,c_emptyset,T_a) != c_insert(V_a,V_A,T_a)
| c_lessequals(V_A,c_insert(V_b,c_emptyset,T_a),tc_set(T_a)) )).
cnf(cls_Set_Osingleton__insert__inj__eq__iff2_0,axiom,
( ~ c_lessequals(V_A,c_insert(V_x,c_emptyset,T_a),tc_set(T_a))
| c_insert(V_x,c_emptyset,T_a) = c_insert(V_x,V_A,T_a) )).
cnf(cls_Sum__Type_OInl__eq__iff1_0,axiom,
( c_Sum__Type_OInl(V_x,T_a,T_b) != c_Sum__Type_OInl(V_y,T_a,T_b)
| V_x = V_y )).
cnf(cls_Sum__Type_OInl__not__Inr__iff1_0,axiom,
( c_Sum__Type_OInl(V_a,T_a,T_b) != c_Sum__Type_OInr(V_b,T_b,T_a) )).
cnf(cls_Sum__Type_OInr__eq__iff1_0,axiom,
( c_Sum__Type_OInr(V_x,T_b,T_a) != c_Sum__Type_OInr(V_y,T_b,T_a)
| V_x = V_y )).
cnf(cls_Sum__Type_OInr__not__Inl__iff1_0,axiom,
( c_Sum__Type_OInr(V_b,T_b,T_a) != c_Sum__Type_OInl(V_a,T_a,T_b) )).
cnf(cls_Wellfounded__Recursion_Oacyclic__converse__iff1_0,axiom,
( ~ c_Wellfounded__Recursion_Oacyclic(c_Relation_Oconverse(V_r,T_a,T_a),T_a)
| c_Wellfounded__Recursion_Oacyclic(V_r,T_a) )).
cnf(cls_Wellfounded__Recursion_Oacyclic__converse__iff2_0,axiom,
( ~ c_Wellfounded__Recursion_Oacyclic(V_r,T_a)
| c_Wellfounded__Recursion_Oacyclic(c_Relation_Oconverse(V_r,T_a,T_a),T_a) )).
cnf(cls_Wellfounded__Recursion_Oacyclic__insert__iff1_0,axiom,
( ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| c_Wellfounded__Recursion_Oacyclic(V_r,T_a) )).
cnf(cls_Wellfounded__Recursion_Oacyclic__insert__iff1_1,axiom,
( ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) )).
cnf(cls_Wellfounded__Recursion_Oacyclic__insert__iff2_0,axiom,
( ~ c_Wellfounded__Recursion_Oacyclic(V_r,T_a)
| c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) )).
cnf(cls_Wellfounded__Recursion_Owf__insert__iff1_0,axiom,
( ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| c_Wellfounded__Recursion_Owf(V_r,T_a) )).
cnf(cls_Wellfounded__Recursion_Owf__insert__iff1_1,axiom,
( ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) )).
cnf(cls_Wellfounded__Recursion_Owf__insert__iff2_0,axiom,
( ~ c_Wellfounded__Recursion_Owf(V_r,T_a)
| c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)) )).
cnf(cls_Wellfounded__Relations_Oless__than__iff__iff1_0,axiom,
( ~ c_in(c_Pair(V_x,V_y,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat))
| c_less(V_x,V_y,tc_nat) )).
cnf(cls_Wellfounded__Relations_Oless__than__iff__iff2_0,axiom,
( ~ c_less(V_x,V_y,tc_nat)
| c_in(c_Pair(V_x,V_y,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat)) )).
%------------------------------------------------------------------------------
|
