blob: d228e3abf70e6fa1b8644f03b546aa5ee6223616 (
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
|
1 mulC_id
2 mulC_zero
3 mulC_dist
4 mul1m
5 mulm1
6 mulmA
7 iteropE
8 mulmC
9 mulmCA
10 mulmAC
11 mulmACA
12 mul0m
13 mulm0
14 addmA
15 addmC
16 addmCA
17 addmAC
18 add0m
19 addm0
20 mulm_addl
21 mulm_addr
22 bigopE
23 mem_index_iota
24 mem_index_enum
25 filter_index_enum
26 big_load
27 big_rec3
28 big_ind3
29 big_rec2
30 big_ind2
31 big_morph
32 big_rec
33 big_ind
34 eq_big_op
35 big_endo
36 big_filter
37 big_filter_cond
38 eq_bigl
39 big_andbC
40 eq_bigr
41 eq_big
42 congr_big
43 big_nil
44 big_cons
45 big_map
46 big_nth
47 big_hasC
48 big_pred0_eq
49 big_pred0
50 big_cat_nested
51 big_catl
52 big_catr
53 big_const_seq
54 big_seq_cond
55 big_seq
56 eq_big_seq
57 big_nat_cond
58 big_nat
59 congr_big_nat
60 eq_big_nat
61 big_geq
62 big_ltn_cond
63 big_ltn
64 big_addn
65 big_add1
66 big_nat_recl
67 big_mkord
68 big_nat_widen
69 big_ord_widen_cond
70 big_ord_widen
71 big_ord_widen_leq
72 big_ord0
73 big_tnth
74 big_ord_narrow_cond
75 big_ord_narrow_cond_leq
76 big_ord_narrow
77 big_ord_narrow_leq
78 big_ord_recl
79 big_const
80 big_const_nat
81 big_const_ord
82 eq_big_idx_seq
83 eq_big_idx
84 big1_eq
85 big1
86 big1_seq
87 big_seq1
88 big_mkcond
89 big_cat
90 big_pred1_eq
91 big_pred1
92 big_cat_nat
93 big_nat1
94 big_nat_recr
95 big_ord_recr
96 big_sumType
97 big_split_ord
98 eq_big_perm
99 big_uniq
100 big_index_uniq
101 big_rem
102 big_undup
103 eq_big_idem
104 big_split
105 bigID
106 bigU
107 bigD1
108 bigD1_seq
109 cardD1x
110 partition_big
111 reindex_onto
112 reindex
113 reindex_inj
114 big_nat_rev
115 pair_big_dep
116 pair_big
117 pair_bigA
118 exchange_big_dep
119 exchange_big
120 exchange_big_dep_nat
121 exchange_big_nat
122 big_distrl
123 big_distrr
124 big_distrlr
125 big_distr_big_dep
126 big_distr_big
127 bigA_distr_big_dep
128 bigA_distr_big
129 bigA_distr_bigA
130 big_has
131 big_all
132 big_has_cond
133 big_all_cond
134 big_orE
135 big_andE
136 sum_nat_const
137 sum1_card
138 prod_nat_const
139 sum_nat_const_nat
140 prod_nat_const_nat
141 leqif_sum
142 leq_sum
143 sum_nat_eq0
144 prodn_cond_gt0
145 prodn_gt0
146 leq_bigmax_cond
147 leq_bigmax
148 bigmax_leqP
149 bigmax_sup
150 bigmax_eq_arg
151 eq_bigmax_cond
152 eq_bigmax
153 expn_sum
154 dvdn_biglcmP
155 biglcmn_sup
156 dvdn_biggcdP
157 biggcdn_inf
|
