-
Notifications
You must be signed in to change notification settings - Fork 2
/
00vizar
12370 lines (12370 loc) · 259 KB
/
00vizar
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
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
m1_hidden set
r1_hidden =
r1_hidden <>
r2_hidden ∈
k1_tarski \{###1\}
k2_tarski \{..\}
r1_tarski ⊆
k3_tarski union
k4_tarski [..]
r2_tarski are_equipotent
v1_xboole_0 ###1 = Ø
k1_xboole_0 Ø
k2_xboole_0 ∪
k3_xboole_0 ∩
k4_xboole_0 \
k5_xboole_0 \+\
r1_xboole_0 ###1 ∩ ###2 = Ø
r2_xboole_0 c<
r3_xboole_0 are_c=-comparable
r1_xboole_0 meets
k1_enumset1 \{..\}
k2_enumset1 \{..\}
k3_enumset1 \{..\}
k4_enumset1 \{..\}
k5_enumset1 \{..\}
k6_enumset1 \{..\}
k7_enumset1 \{..\}
k8_enumset1 \{..\}
v1_xtuple_0 pair
k1_xtuple_0 `1
k2_xtuple_0 `2
k3_xtuple_0 [..]
v2_xtuple_0 triple
k4_xtuple_0 `1_3
k5_xtuple_0 `2_3
k2_xtuple_0 `3_3
k6_xtuple_0 [..]
v3_xtuple_0 quadruple
k7_xtuple_0 `1_4
k8_xtuple_0 `2_4
k5_xtuple_0 `3_4
k2_xtuple_0 `4_4
k9_xtuple_0 proj₁
k10_xtuple_0 proj₂
k11_xtuple_0 proj1_3
k12_xtuple_0 proj2_3
k10_xtuple_0 proj3_3
k13_xtuple_0 proj1_4
k14_xtuple_0 proj2_4
k12_xtuple_0 proj3_4
k10_xtuple_0 proj4_4
k1_zfmisc_1 𝒫(###1)
k2_zfmisc_1 ###1 × ###2
k3_zfmisc_1 [:..:]
k4_zfmisc_1 [:..:]
r1_zfmisc_1 are_mutually_different
r2_zfmisc_1 are_mutually_different
r3_zfmisc_1 are_mutually_different
r4_zfmisc_1 are_mutually_different
r5_zfmisc_1 are_mutually_different
v1_zfmisc_1 trivial
m1_subset_1 ∈
m2_subset_1 ###1 ∈ ###3 ⊆ ###2
k1_subset_1 \{\}
k2_subset_1 [#]
k3_subset_1 `
k4_subset_1 (###2 ∪ ###3) ∩ ###1
k5_subset_1 \+\
k6_subset_1 \
k7_subset_1 \
k8_subset_1 /\
k9_subset_1 /\
r1_subset_1 misses
r2_subset_1 meets
k10_subset_1 choose
v1_subset_1 proper
k1_setfam_1 meet
r1_setfam_1 is_finer_than
r2_setfam_1 is_coarser_than
k2_setfam_1 UNION
k3_setfam_1 INTERSECTION
k4_setfam_1 DIFFERENCE
k5_setfam_1 union
k6_setfam_1 meet
k7_setfam_1 COMPLEMENT
v1_setfam_1 with_non-empty_elements
k8_setfam_1 Intersect
v2_setfam_1 empty-membered
v2_setfam_1 with_non-empty_element
m1_setfam_1 Cover
v3_setfam_1 with_proper_subsets
k9_setfam_1 bool
v1_relat_1 relation
k1_relat_1 field
k2_relat_1 ~
k3_relat_1 (#)
k3_relat_1 *
v2_relat_1 non-empty
k4_relat_1 id
k5_relat_1 restrict
k6_relat_1 restrict`
k7_relat_1 .:
k8_relat_1 "
v3_relat_1 empty-yielding
k9_relat_1 Im
k10_relat_1 Coim
v4_relat_1 -defined
v5_relat_1 -valued
v1_funct_1 function
k1_funct_1 ###1(###2)
v2_funct_1 function
k2_funct_1 "
v3_funct_1 constant
k3_funct_1 the_value_of
v4_funct_1 functional
v5_funct_1 -compatible
r1_relat_2 is_reflexive_in
r2_relat_2 is_irreflexive_in
r3_relat_2 is_symmetric_in
r4_relat_2 is_antisymmetric_in
r5_relat_2 is_asymmetric_in
r6_relat_2 is_connected_in
r7_relat_2 is_strongly_connected_in
r8_relat_2 is_transitive_in
v1_relat_2 reflexive
v2_relat_2 irreflexive
v3_relat_2 symmetric
v4_relat_2 antisymmetric
v5_relat_2 asymmetric
v6_relat_2 connected
v7_relat_2 strongly_connected
v8_relat_2 transitive
k1_ordinal1 succ
v1_ordinal1 epsilon-transitive
v2_ordinal1 epsilon-connected
v3_ordinal1 ordinal
r1_ordinal1 c=
v4_ordinal1 limit_ordinal
v5_ordinal1 T-Sequence-like
v6_ordinal1 c=-linear
k2_ordinal1 On
k3_ordinal1 Lim
k4_ordinal1 ω
v7_ordinal1 ###1 ∈ ℕ
k1_wellord1 -Seg
v1_wellord1 well_founded
r1_wellord1 is_well_founded_in
v2_wellord1 well-ordering
r2_wellord1 well_orders
k2_wellord1 \|_2
r3_wellord1 is_isomorphism_of
r4_wellord1 are_isomorphic
k3_wellord1 canonical_isomorphism_of
r1_relset_1 c=
r2_relset_1 =
k1_relset_1 dom
k2_relset_1 rng
k3_relset_1 ~
k4_relset_1 *
k5_relset_1 \|
k6_relset_1 \|`
k7_relset_1 .:
k8_relset_1 "
k1_partfun1 *
k2_partfun1 \|
k3_partfun1 <:..:>
v1_partfun1 total
k4_partfun1 PFuncs
r1_partfun1 tolerates
k5_partfun1 TotFuncs
k6_partfun1 id
k7_partfun1 /.
k1_mcart_1 `1_3
k2_mcart_1 `2_3
k3_mcart_1 `3_3
k4_mcart_1 `1_4
k5_mcart_1 `2_4
k6_mcart_1 `3_4
k7_mcart_1 `4_4
k8_mcart_1 [:..:]
k9_mcart_1 [:..:]
k10_mcart_1 [:..:]
k11_mcart_1 pr1
k12_mcart_1 pr2
k13_mcart_1 `11
k14_mcart_1 `12
k15_mcart_1 `21
k16_mcart_1 `22
k1_wellord2 RelIncl
k2_wellord2 order_type_of
r1_wellord2 is_order_type_of
r2_wellord2 \|###1\| = \|###2\|
v1_funct_2 quasi_total
k1_funct_2 \{f:###1 → ###2\}
v2_funct_2 onto
v3_funct_2 bijective
k2_funct_2 "
k3_funct_2 .
k4_funct_2 pr1
k5_funct_2 pr2
r1_funct_2 =
r2_funct_2 =
k6_funct_2 "
k7_funct_2 .:
k8_funct_2 /*
m1_funct_2 FUNCTION_DOMAIN
k9_funct_2 Funcs
m2_funct_2 ∈
k10_funct_2 /.
k1_binop_1 .
k2_binop_1 .
k3_binop_1 .
v1_binop_1 commutative
v2_binop_1 associative
v3_binop_1 idempotent
r1_binop_1 is_a_left_unity_wrt
r2_binop_1 is_a_right_unity_wrt
r3_binop_1 is_a_unity_wrt
k4_binop_1 the_unity_wrt
r4_binop_1 is_left_distributive_wrt
r5_binop_1 is_right_distributive_wrt
r6_binop_1 is_distributive_wrt
r7_binop_1 is_distributive_wrt
r1_binop_1 is_a_left_unity_wrt
r2_binop_1 is_a_right_unity_wrt
r4_binop_1 is_left_distributive_wrt
r5_binop_1 is_right_distributive_wrt
r7_binop_1 is_distributive_wrt
k5_binop_1 .
r8_binop_1 =
k1_domain_1 [..]
k2_domain_1 `1
k3_domain_1 `2
k4_domain_1 [..]
k5_domain_1 [..]
k6_domain_1 \{..\}
k7_domain_1 \{..\}
k8_domain_1 \{..\}
k9_domain_1 \{..\}
k10_domain_1 \{..\}
k11_domain_1 \{..\}
k12_domain_1 \{..\}
k13_domain_1 \{..\}
k14_domain_1 `11
k15_domain_1 `12
k16_domain_1 `21
k17_domain_1 `22
k1_funct_3 .:
k2_funct_3 .:
k3_funct_3 "
k4_funct_3 chi
k5_funct_3 chi
k6_funct_3 incl
k7_funct_3 pr1
k8_funct_3 pr2
k9_funct_3 pr1
k10_funct_3 pr2
k11_funct_3 delta
k12_funct_3 delta
k13_funct_3 <:..:>
k14_funct_3 <:..:>
k15_funct_3 [:..:]
k16_funct_3 [:..:]
k1_funcop_1 ~
k2_funcop_1 -->
k3_funcop_1 .:
k4_funcop_1 [:]
k5_funcop_1 [;]
k6_funcop_1 .:
k7_funcop_1 -->
k8_funcop_1 -->
k9_funcop_1 [:]
k10_funcop_1 [;]
k11_funcop_1 rng
k12_funcop_1 ~
v1_funcop_1 Function-yielding
k13_funcop_1 .-->
k14_funcop_1 IFEQ
k15_funcop_1 IFEQ
k16_funcop_1 .-->
k13_funcop_1 :->
k17_funcop_1 :->
k16_funcop_1 :->
k18_funcop_1 :->
v2_funcop_1 Relation-yielding
k1_funct_4 +*
k2_funct_4 ~
k3_funct_4 \|:..:\|
k4_funct_4 -->
k5_funct_4 -->
k6_funct_4 +~
k7_funct_4 +*
k1_ordinal2 last
k2_ordinal2 inf
k3_ordinal2 sup
v1_ordinal2 Ordinal-yielding
k4_ordinal2 sup
k5_ordinal2 inf
k6_ordinal2 lim_sup
k7_ordinal2 lim_inf
r1_ordinal2 is_limes_of
k8_ordinal2 lim
k9_ordinal2 lim
v2_ordinal2 increasing
v3_ordinal2 continuous
k10_ordinal2 +^
k11_ordinal2 *^
k12_ordinal2 exp
r2_ordinal2 is_cofinal_with
k1_ordinal3 +^
k2_ordinal3 +^
k3_ordinal3 *^
k4_ordinal3 *^
k5_ordinal3 -^
k6_ordinal3 div^
k7_ordinal3 mod^
k8_ordinal3 +^
k9_ordinal3 *^
k1_multop_1 .
k2_multop_1 .
k3_multop_1 .
k4_multop_1 .
k1_sysrel CL
k1_gate_1 NOT1
k2_gate_1 AND2
k3_gate_1 OR2
k4_gate_1 XOR2
k5_gate_1 EQV2
k6_gate_1 NAND2
k7_gate_1 NOR2
k8_gate_1 AND3
k9_gate_1 OR3
k10_gate_1 XOR3
k11_gate_1 MAJ3
k12_gate_1 NAND3
k13_gate_1 NOR3
k14_gate_1 AND4
k15_gate_1 OR4
k16_gate_1 NAND4
k17_gate_1 NOR4
k18_gate_1 AND5
k19_gate_1 OR5
k20_gate_1 NAND5
k21_gate_1 NOR5
k22_gate_1 AND6
k23_gate_1 OR6
k24_gate_1 NAND6
k25_gate_1 NOR6
k26_gate_1 AND7
k27_gate_1 OR7
k28_gate_1 NAND7
k29_gate_1 NOR7
k30_gate_1 AND8
k31_gate_1 OR8
k32_gate_1 NAND8
k33_gate_1 NOR8
k34_gate_1 MODADD2
k10_gate_1 ADD1
k11_gate_1 CARR1
k35_gate_1 ADD2
k36_gate_1 CARR2
k37_gate_1 ADD3
k38_gate_1 CARR3
k39_gate_1 ADD4
k40_gate_1 CARR4
k1_gate_5 MULT210
k2_gate_5 MULT211
k3_gate_5 MULT212
k4_gate_5 MULT213
k5_gate_5 MULT310
k6_gate_5 MULT311
k7_gate_5 MULT312
k8_gate_5 MULT313
k9_gate_5 MULT314
k10_gate_5 MULT321
k11_gate_5 MULT322
k12_gate_5 MULT323
k13_gate_5 MULT324
k14_gate_5 CLAADD2
k15_gate_5 CLACARR2
k16_gate_5 CLAADD3
k17_gate_5 CLACARR3
k18_gate_5 CLAADD4
k19_gate_5 CLACARR4
v1_finset_1 finite
v1_finset_1 infinite
v2_finset_1 finite-yielding
v3_finset_1 centered
v2_finset_1 finite-yielding
v4_finset_1 finite-yielding
v5_finset_1 finite-membered
v1_finsub_1 cup-closed
v2_finsub_1 cap-closed
v3_finsub_1 diff-closed
v4_finsub_1 preBoolean
k1_finsub_1 \/
k2_finsub_1 \
k3_finsub_1 /\
k4_finsub_1 \+\
k5_finsub_1 Fin
m1_orders_1 Choice_Function
k1_orders_1 BOOL
v1_orders_1 being_quasi-order
v2_orders_1 being_partial-order
v3_orders_1 being_linear-order
r1_orders_1 quasi_orders
r2_orders_1 partially_orders
r3_orders_1 linearly_orders
r4_orders_1 has_upper_Zorn_property_wrt
r5_orders_1 has_lower_Zorn_property_wrt
r6_orders_1 is_maximal_in
r7_orders_1 is_minimal_in
r8_orders_1 is_superior_of
r9_orders_1 is_inferior_of
k1_setwiseo \{\}.
v1_setwiseo having_a_unity
k2_setwiseo \{....\}
k3_setwiseo \{....\}
k4_setwiseo \{....\}
k5_setwiseo \/
k6_setwiseo \
k7_setwiseo $$
k8_setwiseo .:
k9_setwiseo FinUnion
k10_setwiseo FinUnion
k11_setwiseo singleton
v1_card_1 ###1 ∈ Card
k1_card_1 \|###1\|
k2_card_1 nextcard
v2_card_1 limit_cardinal
k3_card_1 alef
k4_card_1 succ
k5_card_1 card
k6_card_1 Segm
k7_card_1 Segm
v3_card_1 \|###1\|=###2
k1_funct_5 curry
k2_funct_5 uncurry
k3_funct_5 curry'
k4_funct_5 uncurry'
k5_funct_5 op0
k6_funct_5 op1
k7_funct_5 op2
k8_funct_5 op1
k9_funct_5 op2
k10_funct_5 .
k11_funct_5 curry
k12_funct_5 curry'
k13_funct_5 uncurry
k1_partfun2 id
k2_partfun2 "
k3_partfun2 \|`
k4_partfun2 -->
v1_partfun2 constant
v1_classes1 subset-closed
v2_classes1 Tarski
r1_classes1 is_Tarski-Class_of
k1_classes1 Tarski-Class
k2_classes1 Tarski-Class
k3_classes1 Tarski-Class
k4_classes1 Rank
k5_classes1 the_transitive-closure_of
k6_classes1 the_rank_of
r2_classes1 are_fiberwise_equipotent
r1_pboole in
r2_pboole c=
r3_pboole in
k1_pboole [[0]]
k2_pboole \/
k3_pboole /\
k4_pboole \
r4_pboole overlapsoverlap
r5_pboole misses
r5_pboole meets
k5_pboole \+\
r6_pboole =
r7_pboole [=
v1_pboole empty-yielding
v2_pboole non-empty
m1_pboole ∈
m2_pboole ManySortedFunction
k6_pboole [\|..\|]
k7_pboole (Funcs)
m3_pboole ManySortedSubset
k8_pboole **
k9_pboole .:.:
r8_pboole =
v1_card_3 Cardinal-yielding
k1_card_3 Card
k2_card_3 disjoin
k3_card_3 Union
k4_card_3 product
k5_card_3 pi
k6_card_3 Sum
k7_card_3 Product
k8_card_3 sproduct
v2_card_3 with_common_domain
k9_card_3 DOM
k10_card_3 product"
v3_card_3 product-like
k11_card_3 \|
v4_card_3 countable
v5_card_3 denumerable
k12_card_3 proj
k13_card_3 down
k1_funct_6 SubFuncs
k2_funct_6 doms
k3_funct_6 rngs
k4_funct_6 meet
k5_funct_6 ..
k6_funct_6 <:..:>
k7_funct_6 Frege
k8_funct_6 Funcs
k9_funct_6 Funcs
k10_funct_6 commute
k1_arytm_3 one
r1_arytm_3 are_relative_prime
r2_arytm_3 ।
k2_arytm_3 lcm
k3_arytm_3 hcf
k4_arytm_3 RED
k5_arytm_3 RAT+
k6_arytm_3 numerator
k7_arytm_3 denominator
k8_arytm_3 /
k8_arytm_3 quotient
k9_arytm_3 +
k10_arytm_3 *'
k11_arytm_3 \{\}
k12_arytm_3 one
r3_arytm_3 <='
r3_arytm_3 <
k1_arytm_2 DEDEKIND_CUTS
k2_arytm_2 REAL+
k3_arytm_2 DEDEKIND_CUT
k4_arytm_2 GLUED
r1_arytm_2 <='
r1_arytm_2 <
k5_arytm_2 +
k6_arytm_2 *'
k7_arytm_2 +
k8_arytm_2 *'
k1_arytm_1 -'
k2_arytm_1 -
k1_numbers ℝ
k2_numbers COMPLEX
k3_numbers RAT
k4_numbers INT
k5_numbers ℕ
k6_numbers 0
k7_numbers ExtREAL
k1_arytm_0 +
k2_arytm_0 *
k3_arytm_0 opp
k4_arytm_0 inv
k5_arytm_0 [*..*]
k1_xcmplx_0 <i>
v1_xcmplx_0 ###1 ∈ ℂ
k2_xcmplx_0 +
k3_xcmplx_0 *
k4_xcmplx_0 -###1
k5_xcmplx_0 "
k6_xcmplx_0 ###1 - ###2
k7_xcmplx_0 /
v1_xxreal_0 ###1 ∈ 𝔼
k1_xxreal_0 +infty
k2_xxreal_0 -infty
r1_xxreal_0 ≤
nr1_xxreal_0 >
v2_xxreal_0 ###1 > 0
v3_xxreal_0 ###1 < 0
k3_xxreal_0 min
k4_xxreal_0 max
k5_xxreal_0 IFGT
v1_xreal_0 ###1 ∈ ℝ
k1_xreal_0 -'
k1_real_1 -
k2_real_1 "
k3_real_1 +
k4_real_1 *
k5_real_1 -
k6_real_1 /
k7_real_1 +
k8_real_1 *
k9_real_1 -
k10_real_1 /
k1_square_1 min
k2_square_1 max
k3_square_1 ###1 ^ 2
k4_square_1 ^2
k5_square_1 ^2
k6_square_1 √###1
k7_square_1 √###1
k1_nat_1 +
k2_nat_1 +
k3_nat_1 *
k4_nat_1 *
k5_nat_1 min*
k6_nat_1 min
k7_nat_1 max
k8_nat_1 .
k9_nat_1 ^\
k10_nat_1 ^\
v1_int_1 ###1 ∈ ℤ
r1_int_1 ।
r2_int_1 are_congruent_mod
r2_int_1 are_congruent_mod
k1_int_1 [\../]
k2_int_1 [/..\]
k3_int_1 frac
k4_int_1 frac
k5_int_1 div
k6_int_1 mod
v1_rat_1 rational
k1_rat_1 denominator
k2_rat_1 numerator
v1_membered complex-membered
v2_membered ext-real-membered
v3_membered ###1 ⊆ ℝ
v4_membered rational-membered
v5_membered ###1 ⊆ ℤ
v6_membered ###1 ⊆ ℕ
v7_membered add-closed
v1_valued_0 complex-valued
v2_valued_0 ext-real-valued
v3_valued_0 real-valued
v4_valued_0 natural-valued
v1_valued_0 complex-valued
v2_valued_0 ext-real-valued
v3_valued_0 real-valued
v4_valued_0 natural-valued
v5_valued_0 increasing
v6_valued_0 decreasing
v7_valued_0 non-decreasing
v8_valued_0 non-increasing
m1_valued_0 subsequence
m2_valued_0 subsequence
k1_valued_0 ^\
k2_valued_0 *
v9_valued_0 constant
v10_valued_0 zeroed
k1_complex1 Re
k2_complex1 Im
k3_complex1 Re
k4_complex1 Im
k5_complex1 0c
k6_complex1 1r
k7_complex1 <i>
k8_complex1 +
k9_complex1 *
k10_complex1 -
k11_complex1 -
k12_complex1 "
k13_complex1 /
k14_complex1 *'
k15_complex1 *'
k16_complex1 \|....\|
k17_complex1 \|....\|
k16_complex1 abs
k18_complex1 abs
k1_absvalue sgn
k2_absvalue sgn
k1_int_2 abs
k2_int_2 lcm
k3_int_2 gcd
r1_int_2 rel-prime
v1_int_2 prime
k1_nat_d div
k2_nat_d mod
k3_nat_d div
k4_nat_d mod
r1_nat_d ।
k5_nat_d lcm
k6_nat_d gcd
k7_nat_d -'
k1_binop_2 -
k2_binop_2 "
k3_binop_2 +
k4_binop_2 -
k5_binop_2 *
k6_binop_2 /
k7_binop_2 -
k8_binop_2 "
k9_binop_2 +
k10_binop_2 -
k11_binop_2 *
k12_binop_2 /
k13_binop_2 -
k14_binop_2 "
k15_binop_2 +
k16_binop_2 -
k17_binop_2 *
k18_binop_2 /
k19_binop_2 -
k20_binop_2 +
k21_binop_2 -
k22_binop_2 *
k23_binop_2 +
k24_binop_2 *
k25_binop_2 compcomplex
k26_binop_2 invcomplex
k27_binop_2 addcomplex
k28_binop_2 diffcomplex
k29_binop_2 multcomplex
k30_binop_2 divcomplex
k31_binop_2 compreal
k32_binop_2 invreal
k33_binop_2 addreal
k34_binop_2 diffreal
k35_binop_2 multreal
k36_binop_2 divreal
k37_binop_2 comprat
k38_binop_2 invrat
k39_binop_2 addrat
k40_binop_2 diffrat
k41_binop_2 multrat
k42_binop_2 divrat
k43_binop_2 compint
k44_binop_2 addint
k45_binop_2 diffint
k46_binop_2 multint
k47_binop_2 addnat
k48_binop_2 multnat
k1_xxreal_1 [....]
k2_xxreal_1 [....[
k3_xxreal_1 ]....]
k4_xxreal_1 ]....[
k1_card_2 +
k2_card_2 *
k3_card_2 ^
m1_xxreal_2 UpperBound
m2_xxreal_2 LowerBound
k1_xxreal_2 sup
k2_xxreal_2 inf
v1_xxreal_2 left_end
v2_xxreal_2 right_end
k2_xxreal_2 min
k1_xxreal_2 max
k2_xxreal_2 min
k1_xxreal_2 max
v3_xxreal_2 bounded_below
v4_xxreal_2 bounded_above
v5_xxreal_2 real-bounded
v6_xxreal_2 interval
k1_xxreal_3 +
k2_xxreal_3 -
k3_xxreal_3 -
k4_xxreal_3 *
k5_xxreal_3 "
k6_xxreal_3 /
k1_member_1 -
k2_member_1 "
k3_member_1 *
k4_member_1 --
k5_member_1 --
k6_member_1 ""
k7_member_1 ""
k8_member_1 ++
k9_member_1 ++
k10_member_1 --
k11_member_1 --
k12_member_1 **
k13_member_1 **
k14_member_1 ///
k15_member_1 ///
k16_member_1 ++
k17_member_1 ++
k18_member_1 --
k19_member_1 --
k20_member_1 --
k21_member_1 --
k22_member_1 **
k23_member_1 **
k24_member_1 ///
k25_member_1 ///
k26_member_1 ///
k27_member_1 ///
k1_supinf_1 +infty
k2_supinf_1 -infty
k3_supinf_1 SetMajorant
k4_supinf_1 SetMinorant
k5_supinf_1 SUP
k6_supinf_1 INF
k1_quin_1 delta
k2_quin_1 delta
m1_realset1 Preserv
k1_realset1 \|\|
k2_realset1 \|\|
r1_realset1 is_Bin_Op_Preserv
m2_realset1 Presv
k3_realset1 \|\|\|
m3_realset1 DnT
k4_realset1 !
v1_classes2 universal
k1_classes2 \{..\}
k2_classes2 bool
k3_classes2 union
k4_classes2 meet
k5_classes2 \{..\}
k6_classes2 [..]
k7_classes2 \/
k8_classes2 /\
k9_classes2 \
k10_classes2 \+\
k11_classes2 [:..:]
k12_classes2 Funcs
k13_classes2 FinSETS
k14_classes2 SETS
k15_classes2 Universe_closure
k16_classes2 UNIVERSE
k1_ordinal4 ^
k2_ordinal4 0-element_of
k3_ordinal4 1-element_of
k4_ordinal4 .
k5_ordinal4 *
k6_ordinal4 succ
k7_ordinal4 +^
k8_ordinal4 *^
k1_finseq_1 Seg
k2_finseq_1 Seg
v1_finseq_1 FinSequence-like
k3_finseq_1 len
k4_finseq_1 dom
m1_finseq_1 FinSequence
m2_finseq_1 ###1 ∈ fin-seq(###2)
k5_finseq_1 <###1>
k6_finseq_1 <*>
k7_finseq_1 ^
k8_finseq_1 ^
k9_finseq_1 <###1>
k10_finseq_1 <*..*>
k11_finseq_1 <*..*>
k12_finseq_1 <###2>
k13_finseq_1 *
v2_finseq_1 FinSubsequence-like
k14_finseq_1 Sgm
k15_finseq_1 Seq
k16_finseq_1 \|
k17_finseq_1 \|
k18_finseq_1 [*]
v3_finseq_1 FinSequence-membered
k1_recdef_1 .
k1_valued_1 +
k2_valued_1 +
k3_valued_1 +
k4_valued_1 +
k5_valued_1 +
k6_valued_1 +
k7_valued_1 +
k7_valued_1 +
k8_valued_1 +
k9_valued_1 +
k10_valued_1 +
k11_valued_1 +
k12_valued_1 +
k13_valued_1 -
k14_valued_1 -
k15_valued_1 -
k16_valued_1 -
k17_valued_1 -
k18_valued_1 (#)
k19_valued_1 (#)
k20_valued_1 (#)
k21_valued_1 (#)
k22_valued_1 (#)
k23_valued_1 (#)
k24_valued_1 (#)
k24_valued_1 (#)
k25_valued_1 (#)
k26_valued_1 (#)
k27_valued_1 (#)
k28_valued_1 (#)
k29_valued_1 (#)
k30_valued_1 -
k31_valued_1 -
k32_valued_1 -
k33_valued_1 -
k34_valued_1 -
k35_valued_1 "
k36_valued_1 "
k37_valued_1 "
k38_valued_1 "
k39_valued_1 ^2
k40_valued_1 ^2
k41_valued_1 ^2
k42_valued_1 ^2
k43_valued_1 ^2
k44_valued_1 ^2
k45_valued_1 -
k46_valued_1 -
k47_valued_1 -
k48_valued_1 -
k49_valued_1 -
k50_valued_1 /"
k51_valued_1 /"
k52_valued_1 /"
k53_valued_1 /"
k54_valued_1 \|....\|
k54_valued_1 abs
k55_valued_1 \|....\|
k56_valued_1 abs
k57_valued_1 \|....\|
k58_valued_1 abs
k59_valued_1 \|....\|
k60_valued_1 abs
k61_valued_1 Shift
v1_valued_1 increasing
v2_valued_1 decreasing
v3_valued_1 non-decreasing
v4_valued_1 non-increasing
k62_valued_1 LastLoc
k63_valued_1 CutLastLoc
k64_valued_1 FirstLoc
k1_finseq_2 idseq
k2_finseq_2 \|->
m1_finseq_2 FinSequenceSet
m2_finseq_2 ∈
k3_finseq_2 *
k4_finseq_2 ###1-tuples(###2)
k5_finseq_2 \|->
k6_finseq_2 #
k7_finseq_2 *-->
k1_seq_1 .
k1_xboolean FALSE
k2_xboolean TRUE
v1_xboolean boolean
k3_xboolean 'not'
k4_xboolean '&'
k5_xboolean 'or'
k6_xboolean =>
k7_xboolean <=>
k8_xboolean 'nand'
k9_xboolean 'nor'
k10_xboolean 'xor'
k11_xboolean '\'
k1_eqrel_1 nabla
k2_eqrel_1 /\
k3_eqrel_1 \/
k4_eqrel_1 /\
k5_eqrel_1 "\/"
k6_eqrel_1 Class
k7_eqrel_1 Class
m1_eqrel_1 a_partition
k8_eqrel_1 Class
k9_eqrel_1 EqClass
k10_eqrel_1 SmallestPartition
k11_eqrel_1 EqClass
v1_eqrel_1 partition-membered
k12_eqrel_1 Intersection
k13_eqrel_1 proj
k1_comseq_2 *'
k2_comseq_2 *'
v1_comseq_2 bounded
v1_comseq_2 bounded
v2_comseq_2 convergent
k3_comseq_2 lim
v1_seq_2 bounded_above
v2_seq_2 bounded_below
v1_seq_2 bounded_above
v2_seq_2 bounded_below
k1_seq_2 lim
k2_seq_2 lim
k1_finseqop .:
k2_finseqop [:]
k3_finseqop [;]
k4_finseqop *
r1_finseqop is_an_inverseOp_wrt
v1_finseqop having_an_inverseOp
k5_finseqop the_inverseOp_wrt
k6_finseqop *
k7_finseqop *
k1_finseq_3 -
k2_finseq_3 Del
k3_finseq_3 ExtendRel
r1_finseq_3 is_representatives_FS
k1_margrel1 -->
k2_margrel1 the_arity_of
m1_margrel1 relation_length
m2_margrel1 relation
m3_margrel1 relation
k3_margrel1 relations_on
r1_margrel1 =
k4_margrel1 empty_rel
k5_margrel1 the_arity_of
k6_margrel1 BOOLEAN
k7_margrel1 FALSE
k8_margrel1 TRUE
k9_margrel1 'not'
k10_margrel1 '&'
k11_margrel1 ALL
k12_margrel1 ALL
v1_margrel1 boolean-valued
k13_margrel1 'not'
k14_margrel1 '&'
k15_margrel1 'not'
k16_margrel1 '&'
v2_margrel1 homogeneous
v3_margrel1 quasi_total
v4_margrel1 homogeneous
v5_margrel1 quasi_total