| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (360 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (220 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |
Global Index
A
abit [definition, in Circuits.GENE.BV]Adder [library]
AdderProof [library]
addr [definition, in Circuits.GENE.Memo]
AddrOK [definition, in Circuits.GENE.Memo]
ad_2_1 [definition, in Circuits.BLOCK.Fill_impl]
ad' [definition, in Circuits.BLOCK.Fill_impl]
ad1 [definition, in Circuits.BLOCK.Fill_impl]
ad2 [definition, in Circuits.BLOCK.Fill_impl]
ad2_t [lemma, in Circuits.BLOCK.Fill_impl]
ad3 [definition, in Circuits.BLOCK.Fill_impl]
al [definition, in Circuits.BLOCK.Fill_spec]
al_2_1 [definition, in Circuits.BLOCK.Fill_impl]
al_constant [lemma, in Circuits.BLOCK.Fill_spec]
al_t [lemma, in Circuits.BLOCK.Fill_spec]
al_al' [lemma, in Circuits.BLOCK.Fill_proof]
al_initsize [axiom, in Circuits.BLOCK.Fill_defs]
al_init [axiom, in Circuits.BLOCK.Fill_defs]
al' [definition, in Circuits.BLOCK.Fill_impl]
al1 [definition, in Circuits.BLOCK.Fill_impl]
al2 [definition, in Circuits.BLOCK.Fill_impl]
al2_constant [lemma, in Circuits.BLOCK.Fill_impl]
al2_t [lemma, in Circuits.BLOCK.Fill_impl]
al3 [definition, in Circuits.BLOCK.Fill_impl]
appbv [definition, in Circuits.GENE.BV]
app_lowbit_highs [lemma, in Circuits.MULTIPLIER.Definitions]
app_trunc_elemlist [lemma, in Circuits.GENE.Lists_field]
app_trunc_strip [lemma, in Circuits.GENE.Lists_field]
app_v_trunc [lemma, in Circuits.GENE.Lists_field]
app_assoc_l [definition, in Circuits.GENE.Lists_compl]
app_assoc_r [definition, in Circuits.GENE.Lists_compl]
app_v_nil_sym [lemma, in Circuits.GENE.Lists_compl]
app_v_nil_inv [lemma, in Circuits.GENE.Lists_compl]
app_v_nil_idem [lemma, in Circuits.GENE.Lists_compl]
app_v_nil [lemma, in Circuits.GENE.Lists_compl]
app_eq2 [lemma, in Circuits.GENE.Lists_compl]
app_eq1 [lemma, in Circuits.GENE.Lists_compl]
Arith_compl [library]
a_size [axiom, in Circuits.BLOCK.Fill_defs]
B
bitset [definition, in Circuits.GENE.BV]bool_to_nat_all [lemma, in Circuits.GENE.Bool_compl]
bool_to_nat [definition, in Circuits.GENE.Bool_compl]
Bool_compl [library]
BV [definition, in Circuits.GENE.BV]
BV [library]
BVnot [definition, in Circuits.GENE.BV]
BV_null_nat [lemma, in Circuits.GENE.BV]
BV_to_nat_app2 [lemma, in Circuits.GENE.BV]
BV_to_nat_app [lemma, in Circuits.GENE.BV]
BV_to_nat_eq2 [lemma, in Circuits.GENE.BV]
BV_to_nat_eq1 [lemma, in Circuits.GENE.BV]
BV_to_nat [definition, in Circuits.GENE.BV]
BV_null [definition, in Circuits.GENE.BV]
BV_full_adder_sym [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry_sym [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum_sym [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry_v_nil_false [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum_v_nil_false [lemma, in Circuits.ADDER.Adder]
BV_full_adder [definition, in Circuits.ADDER.Adder]
BV_full_adder_carry_eq4 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry_eq3 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry_eq2 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry_eq1 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_carry [definition, in Circuits.ADDER.Adder]
BV_full_adder_sum_eq4 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum_eq3 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum_eq2 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum_eq1 [lemma, in Circuits.ADDER.Adder]
BV_full_adder_sum [definition, in Circuits.ADDER.Adder]
BV_incr_decr [lemma, in Circuits.ADDER.IncrDecr]
BV_decr_incr [lemma, in Circuits.ADDER.IncrDecr]
BV_increment_ok [lemma, in Circuits.ADDER.IncrDecr]
BV_increment_adder [lemma, in Circuits.ADDER.IncrDecr]
BV_decrement_limit_carry [lemma, in Circuits.ADDER.IncrDecr]
BV_increment_limit_carry [lemma, in Circuits.ADDER.IncrDecr]
BV_decrement_limit [lemma, in Circuits.ADDER.IncrDecr]
BV_increment_limit [lemma, in Circuits.ADDER.IncrDecr]
BV_decrement_carry [definition, in Circuits.ADDER.IncrDecr]
BV_decrement [definition, in Circuits.ADDER.IncrDecr]
BV_increment_carry [definition, in Circuits.ADDER.IncrDecr]
BV_increment [definition, in Circuits.ADDER.IncrDecr]
BV_nat_lem1 [lemma, in Circuits.MULTIPLIER.LemPrelim]
BV_to_nat_lem0 [lemma, in Circuits.MULTIPLIER.LemPrelim]
BV_full_adder_ok [lemma, in Circuits.ADDER.AdderProof]
BV_full_adder_nil_ok [lemma, in Circuits.ADDER.AdderProof]
BV_full_adder_nil_true_ok [lemma, in Circuits.ADDER.AdderProof]
C
compo_2_1 [definition, in Circuits.BLOCK.Fill_impl]compo' [definition, in Circuits.BLOCK.Fill_impl]
consbv [definition, in Circuits.GENE.BV]
Correct [lemma, in Circuits.MULTIPLIER.MultSeq]
cx [definition, in Circuits.BLOCK.Fill_spec]
cx_2_1 [definition, in Circuits.BLOCK.Fill_impl]
cx_t [lemma, in Circuits.BLOCK.Fill_spec]
cx_cx' [lemma, in Circuits.BLOCK.Fill_proof]
cx_initsize [axiom, in Circuits.BLOCK.Fill_defs]
cx_init [axiom, in Circuits.BLOCK.Fill_defs]
cx' [definition, in Circuits.BLOCK.Fill_impl]
cx1 [definition, in Circuits.BLOCK.Fill_impl]
cx2 [definition, in Circuits.BLOCK.Fill_impl]
cx2_t [lemma, in Circuits.BLOCK.Fill_impl]
cx3 [definition, in Circuits.BLOCK.Fill_impl]
D
da_2_1 [definition, in Circuits.BLOCK.Fill_impl]da' [definition, in Circuits.BLOCK.Fill_impl]
da1 [definition, in Circuits.BLOCK.Fill_impl]
da2 [definition, in Circuits.BLOCK.Fill_impl]
da2_constant [lemma, in Circuits.BLOCK.Fill_impl]
da2_t [lemma, in Circuits.BLOCK.Fill_impl]
da3 [definition, in Circuits.BLOCK.Fill_impl]
DC_dsize [axiom, in Circuits.BLOCK.Fill_proof]
DC_d [axiom, in Circuits.BLOCK.Fill_proof]
DC_asize [axiom, in Circuits.BLOCK.Fill_proof]
DC_a [axiom, in Circuits.BLOCK.Fill_proof]
Definitions [library]
di [definition, in Circuits.BLOCK.Fill_spec]
di_2_1 [definition, in Circuits.BLOCK.Fill_impl]
di_t [lemma, in Circuits.BLOCK.Fill_spec]
di_di' [lemma, in Circuits.BLOCK.Fill_proof]
di_initsize [axiom, in Circuits.BLOCK.Fill_defs]
di_init [axiom, in Circuits.BLOCK.Fill_defs]
di' [definition, in Circuits.BLOCK.Fill_impl]
di1 [definition, in Circuits.BLOCK.Fill_impl]
di2 [definition, in Circuits.BLOCK.Fill_impl]
di2_constant [lemma, in Circuits.BLOCK.Fill_impl]
di2_t [lemma, in Circuits.BLOCK.Fill_impl]
di3 [definition, in Circuits.BLOCK.Fill_impl]
d_size [axiom, in Circuits.BLOCK.Fill_defs]
E
elemlist [definition, in Circuits.GENE.Lists_field]elemlist_inv [lemma, in Circuits.GENE.Lists_field]
elemlist_cons_O [lemma, in Circuits.GENE.Lists_field]
elemlist_cons_S [lemma, in Circuits.GENE.Lists_field]
elemlist_is_sublist [lemma, in Circuits.GENE.Lists_field]
eq_list_dec [axiom, in Circuits.GENE.Lists_compl]
eq_cons [lemma, in Circuits.GENE.Lists_compl]
F
false_to_true [lemma, in Circuits.GENE.Bool_compl]field [definition, in Circuits.GENE.BV]
Fill_ok [lemma, in Circuits.BLOCK.Fill_proof]
Fill_impl [library]
Fill_defs [library]
Fill_proof [library]
Fill_spec [library]
FullAdder [library]
full_adder_ok [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_neg [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_true_false [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_true [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_false [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_sym2 [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry_sym1 [lemma, in Circuits.ADDER.FullAdder]
full_adder_sum_true [lemma, in Circuits.ADDER.FullAdder]
full_adder_sum_false [lemma, in Circuits.ADDER.FullAdder]
full_adder_sum_sym2 [lemma, in Circuits.ADDER.FullAdder]
full_adder_sum_sym1 [lemma, in Circuits.ADDER.FullAdder]
full_adder_carry [definition, in Circuits.ADDER.FullAdder]
full_adder_sum [definition, in Circuits.ADDER.FullAdder]
F_If [lemma, in Circuits.GENE.Bool_compl]
G
gt_double_S_n [lemma, in Circuits.GENE.Arith_compl]gt_double_n_S [lemma, in Circuits.GENE.Arith_compl]
gt_double_inv [lemma, in Circuits.GENE.Arith_compl]
gt_double [lemma, in Circuits.GENE.Arith_compl]
H
HalfAdder [library]half_adder_ok [lemma, in Circuits.ADDER.HalfAdder]
half_adder_carry_true [lemma, in Circuits.ADDER.HalfAdder]
half_adder_sum_true [lemma, in Circuits.ADDER.HalfAdder]
half_adder_carry_false [lemma, in Circuits.ADDER.HalfAdder]
half_adder_sum_false [lemma, in Circuits.ADDER.HalfAdder]
half_adder_carry_sym [lemma, in Circuits.ADDER.HalfAdder]
half_adder_sum_sym [lemma, in Circuits.ADDER.HalfAdder]
half_adder_carry [definition, in Circuits.ADDER.HalfAdder]
half_adder_sum [definition, in Circuits.ADDER.HalfAdder]
highs [definition, in Circuits.MULTIPLIER.Definitions]
highs_is_strip [lemma, in Circuits.MULTIPLIER.Definitions]
I
If [definition, in Circuits.GENE.Bool_compl]IfIf [lemma, in Circuits.GENE.Bool_compl]
If_cond_false [lemma, in Circuits.GENE.Bool_compl]
If_cond_true [lemma, in Circuits.GENE.Bool_compl]
If_eq [lemma, in Circuits.GENE.Bool_compl]
If_neg [lemma, in Circuits.GENE.Bool_compl]
IncrDecr [library]
Invariant [lemma, in Circuits.MULTIPLIER.MultSeq]
Invariant_t_O [lemma, in Circuits.MULTIPLIER.MultSeq]
inv_ind_true [lemma, in Circuits.MULTIPLIER.MultSeq]
inv_ind_false [lemma, in Circuits.MULTIPLIER.MultSeq]
IsNull [definition, in Circuits.BLOCK.Fill_defs]
IsNull_BV_null [lemma, in Circuits.BLOCK.Fill_defs]
IsNull_null [lemma, in Circuits.BLOCK.Fill_defs]
IsNull_cons [lemma, in Circuits.BLOCK.Fill_defs]
IsNull_false [lemma, in Circuits.BLOCK.Fill_defs]
IsNull_nil [lemma, in Circuits.BLOCK.Fill_defs]
L
LemPrelim [library]lem_le_minus_v1_Sn [lemma, in Circuits.MULTIPLIER.LemPrelim]
len [inductive, in Circuits.GENE.Lists_compl]
lenbv [definition, in Circuits.GENE.BV]
lengthbv [definition, in Circuits.GENE.BV]
length_BV_null [lemma, in Circuits.GENE.BV]
length_R2 [lemma, in Circuits.MULTIPLIER.Definitions]
length_R1 [lemma, in Circuits.MULTIPLIER.Definitions]
length_V2_V1 [lemma, in Circuits.MULTIPLIER.Definitions]
length_V2 [lemma, in Circuits.MULTIPLIER.Definitions]
length_V1 [lemma, in Circuits.MULTIPLIER.Definitions]
length_V2_size [axiom, in Circuits.MULTIPLIER.Definitions]
length_V1_size [axiom, in Circuits.MULTIPLIER.Definitions]
length_abit [lemma, in Circuits.MULTIPLIER.Definitions]
length_highs [lemma, in Circuits.MULTIPLIER.Definitions]
length_BV_full_adder_sum [lemma, in Circuits.ADDER.Adder]
length_BV_decrement [lemma, in Circuits.ADDER.IncrDecr]
length_BV_increment [lemma, in Circuits.ADDER.IncrDecr]
length_al [lemma, in Circuits.BLOCK.Fill_spec]
length_cx [lemma, in Circuits.BLOCK.Fill_spec]
length_di [lemma, in Circuits.BLOCK.Fill_spec]
length_elemlist [lemma, in Circuits.GENE.Lists_field]
length_strip [lemma, in Circuits.GENE.Lists_field]
length_trunc [lemma, in Circuits.GENE.Lists_field]
length_map [lemma, in Circuits.GENE.Lists_compl]
length_rev [lemma, in Circuits.GENE.Lists_compl]
length_list_const [lemma, in Circuits.GENE.Lists_compl]
length_app [lemma, in Circuits.GENE.Lists_compl]
length_eq [lemma, in Circuits.GENE.Lists_compl]
length_eq2 [lemma, in Circuits.GENE.Lists_compl]
length_eq1 [lemma, in Circuits.GENE.Lists_compl]
length_replace [lemma, in Circuits.GENE.Lists_replace]
len_list_const [lemma, in Circuits.GENE.Lists_compl]
len_length [lemma, in Circuits.GENE.Lists_compl]
len_app [lemma, in Circuits.GENE.Lists_compl]
len_nil_inv [lemma, in Circuits.GENE.Lists_compl]
len_cons_not_O [lemma, in Circuits.GENE.Lists_compl]
len_cons [constructor, in Circuits.GENE.Lists_compl]
len_nil [constructor, in Circuits.GENE.Lists_compl]
le_SO_length_V1 [lemma, in Circuits.MULTIPLIER.Definitions]
le_SO_size [lemma, in Circuits.MULTIPLIER.Definitions]
le_length_strip [lemma, in Circuits.GENE.Lists_field]
le_length_trunc [lemma, in Circuits.GENE.Lists_field]
le_SO_length_v [lemma, in Circuits.GENE.Lists_compl]
le_minus_minus [lemma, in Circuits.GENE.Arith_compl]
le_plus_lem2 [lemma, in Circuits.GENE.Arith_compl]
le_plus_lem1 [lemma, in Circuits.GENE.Arith_compl]
le_plus_n_m [lemma, in Circuits.GENE.Arith_compl]
Lists_field.A [variable, in Circuits.GENE.Lists_field]
Lists_field [section, in Circuits.GENE.Lists_field]
Lists_compl.B [variable, in Circuits.GENE.Lists_compl]
Lists_compl.A [variable, in Circuits.GENE.Lists_compl]
Lists_compl [section, in Circuits.GENE.Lists_compl]
Lists_replace.A [variable, in Circuits.GENE.Lists_replace]
Lists_replace [section, in Circuits.GENE.Lists_replace]
Lists_field [library]
Lists_compl [library]
Lists_replace [library]
list_const_eq2 [lemma, in Circuits.GENE.Lists_compl]
list_const_eq1 [lemma, in Circuits.GENE.Lists_compl]
list_const [definition, in Circuits.GENE.Lists_compl]
lowbit [definition, in Circuits.MULTIPLIER.Definitions]
lowbit_is_abit [lemma, in Circuits.MULTIPLIER.Definitions]
lowbit_is_trunc [lemma, in Circuits.MULTIPLIER.Definitions]
lt_plus_n_m [lemma, in Circuits.GENE.Arith_compl]
M
map [definition, in Circuits.GENE.Lists_compl]mem [definition, in Circuits.BLOCK.Fill_spec]
Memo [definition, in Circuits.GENE.Memo]
Memo [library]
MemoEmpty [definition, in Circuits.GENE.Memo]
MemoRead [definition, in Circuits.GENE.Memo]
MemoSize [definition, in Circuits.GENE.Memo]
MemoWrite [definition, in Circuits.GENE.Memo]
MemoZone [definition, in Circuits.GENE.Memo]
mem_2_1 [definition, in Circuits.BLOCK.Fill_impl]
mem_t [lemma, in Circuits.BLOCK.Fill_spec]
mem_mem' [lemma, in Circuits.BLOCK.Fill_proof]
mem_initsize [axiom, in Circuits.BLOCK.Fill_defs]
mem_init [axiom, in Circuits.BLOCK.Fill_defs]
mem' [definition, in Circuits.BLOCK.Fill_impl]
mem1 [definition, in Circuits.BLOCK.Fill_impl]
mem2 [definition, in Circuits.BLOCK.Fill_impl]
mem2_t [lemma, in Circuits.BLOCK.Fill_impl]
mem3 [definition, in Circuits.BLOCK.Fill_impl]
minus_minus_lem2 [lemma, in Circuits.GENE.Arith_compl]
minus_minus_lem1 [lemma, in Circuits.GENE.Arith_compl]
minus_le_lem2 [lemma, in Circuits.GENE.Arith_compl]
minus_le_lem2c [lemma, in Circuits.GENE.Arith_compl]
minus_n_SO [lemma, in Circuits.GENE.Arith_compl]
minus_le_O [lemma, in Circuits.GENE.Arith_compl]
MMemo [definition, in Circuits.GENE.Memo]
MultSeq [library]
mult_plus_distr2 [lemma, in Circuits.GENE.Arith_compl]
mult_permute [lemma, in Circuits.GENE.Arith_compl]
mult_sym [lemma, in Circuits.GENE.Arith_compl]
Mux [definition, in Circuits.MULTIPLIER.Definitions]
N
neg_eq [lemma, in Circuits.GENE.Bool_compl]nilbv [definition, in Circuits.GENE.BV]
nil_cons [lemma, in Circuits.GENE.Lists_compl]
not_eq_cons [lemma, in Circuits.GENE.Lists_compl]
not_nil [lemma, in Circuits.GENE.Lists_compl]
not_len_nil_Sn [lemma, in Circuits.GENE.Lists_compl]
not_cons_eq [lemma, in Circuits.GENE.Lists_compl]
P
plus_O_O [lemma, in Circuits.GENE.Arith_compl]plus_permute2 [lemma, in Circuits.GENE.Arith_compl]
plus_n_SO [lemma, in Circuits.GENE.Arith_compl]
power2 [definition, in Circuits.GENE.Arith_compl]
power2_plus [lemma, in Circuits.GENE.Arith_compl]
power2_eq2 [lemma, in Circuits.GENE.Arith_compl]
R
read_write [lemma, in Circuits.GENE.Memo]replace [definition, in Circuits.GENE.Lists_replace]
replace_newer [lemma, in Circuits.GENE.Lists_replace]
replace_sym [lemma, in Circuits.GENE.Lists_replace]
replace_keep_others [lemma, in Circuits.GENE.Lists_replace]
replace_ok [lemma, in Circuits.GENE.Lists_replace]
rev [definition, in Circuits.GENE.Lists_compl]
rev_rev [lemma, in Circuits.GENE.Lists_compl]
rev_app [lemma, in Circuits.GENE.Lists_compl]
rev_eq [lemma, in Circuits.GENE.Lists_compl]
rev_eq2 [lemma, in Circuits.GENE.Lists_compl]
rev_eq1 [lemma, in Circuits.GENE.Lists_compl]
R1 [definition, in Circuits.MULTIPLIER.Definitions]
R1_never_nil [lemma, in Circuits.MULTIPLIER.Definitions]
R1_eq2 [lemma, in Circuits.MULTIPLIER.Definitions]
R1_eq1 [lemma, in Circuits.MULTIPLIER.Definitions]
R1_lem3 [lemma, in Circuits.MULTIPLIER.LemPrelim]
R1_lem [lemma, in Circuits.MULTIPLIER.LemPrelim]
R2 [definition, in Circuits.MULTIPLIER.Definitions]
R2_eq2 [lemma, in Circuits.MULTIPLIER.Definitions]
R2_eq1 [lemma, in Circuits.MULTIPLIER.Definitions]
S
size [axiom, in Circuits.MULTIPLIER.Definitions]size_not_O [axiom, in Circuits.MULTIPLIER.Definitions]
strip [definition, in Circuits.GENE.Lists_field]
stripbv [definition, in Circuits.GENE.BV]
strip_trunc [lemma, in Circuits.GENE.Lists_field]
strip_trunc_i [lemma, in Circuits.GENE.Lists_field]
strip_strip [lemma, in Circuits.GENE.Lists_field]
strip_eq [lemma, in Circuits.GENE.Lists_field]
strip_sym [lemma, in Circuits.GENE.Lists_field]
strip_strip_S [lemma, in Circuits.GENE.Lists_field]
strip_app [lemma, in Circuits.GENE.Lists_field]
strip_O [lemma, in Circuits.GENE.Lists_field]
strip_max [lemma, in Circuits.GENE.Lists_field]
strip_all [lemma, in Circuits.GENE.Lists_field]
strip_inv [lemma, in Circuits.GENE.Lists_field]
strip_cons_S [lemma, in Circuits.GENE.Lists_field]
strip_nil [lemma, in Circuits.GENE.Lists_field]
sublist [definition, in Circuits.GENE.Lists_field]
T
true_to_false [lemma, in Circuits.GENE.Bool_compl]trunc [definition, in Circuits.GENE.Lists_field]
truncbv [definition, in Circuits.GENE.BV]
trunc_strip [lemma, in Circuits.GENE.Lists_field]
trunc_plus_petit [lemma, in Circuits.GENE.Lists_field]
trunc_trunc3 [lemma, in Circuits.GENE.Lists_field]
trunc_trunc2 [lemma, in Circuits.GENE.Lists_field]
trunc_trunc1 [lemma, in Circuits.GENE.Lists_field]
trunc_sym [lemma, in Circuits.GENE.Lists_field]
trunc_eq [lemma, in Circuits.GENE.Lists_field]
trunc_app [lemma, in Circuits.GENE.Lists_field]
trunc_O [lemma, in Circuits.GENE.Lists_field]
trunc_max [lemma, in Circuits.GENE.Lists_field]
trunc_all [lemma, in Circuits.GENE.Lists_field]
trunc_inv [lemma, in Circuits.GENE.Lists_field]
V
v_not_nil_length [lemma, in Circuits.GENE.Lists_compl]V1 [axiom, in Circuits.MULTIPLIER.Definitions]
V1_not_nil [lemma, in Circuits.MULTIPLIER.Definitions]
V2 [axiom, in Circuits.MULTIPLIER.Definitions]
V2_not_nil [lemma, in Circuits.MULTIPLIER.Definitions]
X
xorb [definition, in Circuits.GENE.Bool_compl]xorb_b_true [lemma, in Circuits.GENE.Bool_compl]
xorb_b_false [lemma, in Circuits.GENE.Bool_compl]
xorb_b_b [lemma, in Circuits.GENE.Bool_compl]
Variable Index
L
Lists_field.A [in Circuits.GENE.Lists_field]Lists_compl.B [in Circuits.GENE.Lists_compl]
Lists_compl.A [in Circuits.GENE.Lists_compl]
Lists_replace.A [in Circuits.GENE.Lists_replace]
Library Index
A
AdderAdderProof
Arith_compl
B
Bool_complBV
D
DefinitionsF
Fill_implFill_defs
Fill_proof
Fill_spec
FullAdder
H
HalfAdderI
IncrDecrL
LemPrelimLists_field
Lists_compl
Lists_replace
M
MemoMultSeq
Lemma Index
A
ad2_t [in Circuits.BLOCK.Fill_impl]al_constant [in Circuits.BLOCK.Fill_spec]
al_t [in Circuits.BLOCK.Fill_spec]
al_al' [in Circuits.BLOCK.Fill_proof]
al2_constant [in Circuits.BLOCK.Fill_impl]
al2_t [in Circuits.BLOCK.Fill_impl]
app_lowbit_highs [in Circuits.MULTIPLIER.Definitions]
app_trunc_elemlist [in Circuits.GENE.Lists_field]
app_trunc_strip [in Circuits.GENE.Lists_field]
app_v_trunc [in Circuits.GENE.Lists_field]
app_v_nil_sym [in Circuits.GENE.Lists_compl]
app_v_nil_inv [in Circuits.GENE.Lists_compl]
app_v_nil_idem [in Circuits.GENE.Lists_compl]
app_v_nil [in Circuits.GENE.Lists_compl]
app_eq2 [in Circuits.GENE.Lists_compl]
app_eq1 [in Circuits.GENE.Lists_compl]
B
bool_to_nat_all [in Circuits.GENE.Bool_compl]BV_null_nat [in Circuits.GENE.BV]
BV_to_nat_app2 [in Circuits.GENE.BV]
BV_to_nat_app [in Circuits.GENE.BV]
BV_to_nat_eq2 [in Circuits.GENE.BV]
BV_to_nat_eq1 [in Circuits.GENE.BV]
BV_full_adder_sym [in Circuits.ADDER.Adder]
BV_full_adder_carry_sym [in Circuits.ADDER.Adder]
BV_full_adder_sum_sym [in Circuits.ADDER.Adder]
BV_full_adder_carry_v_nil_false [in Circuits.ADDER.Adder]
BV_full_adder_sum_v_nil_false [in Circuits.ADDER.Adder]
BV_full_adder_carry_eq4 [in Circuits.ADDER.Adder]
BV_full_adder_carry_eq3 [in Circuits.ADDER.Adder]
BV_full_adder_carry_eq2 [in Circuits.ADDER.Adder]
BV_full_adder_carry_eq1 [in Circuits.ADDER.Adder]
BV_full_adder_sum_eq4 [in Circuits.ADDER.Adder]
BV_full_adder_sum_eq3 [in Circuits.ADDER.Adder]
BV_full_adder_sum_eq2 [in Circuits.ADDER.Adder]
BV_full_adder_sum_eq1 [in Circuits.ADDER.Adder]
BV_incr_decr [in Circuits.ADDER.IncrDecr]
BV_decr_incr [in Circuits.ADDER.IncrDecr]
BV_increment_ok [in Circuits.ADDER.IncrDecr]
BV_increment_adder [in Circuits.ADDER.IncrDecr]
BV_decrement_limit_carry [in Circuits.ADDER.IncrDecr]
BV_increment_limit_carry [in Circuits.ADDER.IncrDecr]
BV_decrement_limit [in Circuits.ADDER.IncrDecr]
BV_increment_limit [in Circuits.ADDER.IncrDecr]
BV_nat_lem1 [in Circuits.MULTIPLIER.LemPrelim]
BV_to_nat_lem0 [in Circuits.MULTIPLIER.LemPrelim]
BV_full_adder_ok [in Circuits.ADDER.AdderProof]
BV_full_adder_nil_ok [in Circuits.ADDER.AdderProof]
BV_full_adder_nil_true_ok [in Circuits.ADDER.AdderProof]
C
Correct [in Circuits.MULTIPLIER.MultSeq]cx_t [in Circuits.BLOCK.Fill_spec]
cx_cx' [in Circuits.BLOCK.Fill_proof]
cx2_t [in Circuits.BLOCK.Fill_impl]
D
da2_constant [in Circuits.BLOCK.Fill_impl]da2_t [in Circuits.BLOCK.Fill_impl]
di_t [in Circuits.BLOCK.Fill_spec]
di_di' [in Circuits.BLOCK.Fill_proof]
di2_constant [in Circuits.BLOCK.Fill_impl]
di2_t [in Circuits.BLOCK.Fill_impl]
E
elemlist_inv [in Circuits.GENE.Lists_field]elemlist_cons_O [in Circuits.GENE.Lists_field]
elemlist_cons_S [in Circuits.GENE.Lists_field]
elemlist_is_sublist [in Circuits.GENE.Lists_field]
eq_cons [in Circuits.GENE.Lists_compl]
F
false_to_true [in Circuits.GENE.Bool_compl]Fill_ok [in Circuits.BLOCK.Fill_proof]
full_adder_ok [in Circuits.ADDER.FullAdder]
full_adder_carry_neg [in Circuits.ADDER.FullAdder]
full_adder_carry_true_false [in Circuits.ADDER.FullAdder]
full_adder_carry_true [in Circuits.ADDER.FullAdder]
full_adder_carry_false [in Circuits.ADDER.FullAdder]
full_adder_carry_sym2 [in Circuits.ADDER.FullAdder]
full_adder_carry_sym1 [in Circuits.ADDER.FullAdder]
full_adder_sum_true [in Circuits.ADDER.FullAdder]
full_adder_sum_false [in Circuits.ADDER.FullAdder]
full_adder_sum_sym2 [in Circuits.ADDER.FullAdder]
full_adder_sum_sym1 [in Circuits.ADDER.FullAdder]
F_If [in Circuits.GENE.Bool_compl]
G
gt_double_S_n [in Circuits.GENE.Arith_compl]gt_double_n_S [in Circuits.GENE.Arith_compl]
gt_double_inv [in Circuits.GENE.Arith_compl]
gt_double [in Circuits.GENE.Arith_compl]
H
half_adder_ok [in Circuits.ADDER.HalfAdder]half_adder_carry_true [in Circuits.ADDER.HalfAdder]
half_adder_sum_true [in Circuits.ADDER.HalfAdder]
half_adder_carry_false [in Circuits.ADDER.HalfAdder]
half_adder_sum_false [in Circuits.ADDER.HalfAdder]
half_adder_carry_sym [in Circuits.ADDER.HalfAdder]
half_adder_sum_sym [in Circuits.ADDER.HalfAdder]
highs_is_strip [in Circuits.MULTIPLIER.Definitions]
I
IfIf [in Circuits.GENE.Bool_compl]If_cond_false [in Circuits.GENE.Bool_compl]
If_cond_true [in Circuits.GENE.Bool_compl]
If_eq [in Circuits.GENE.Bool_compl]
If_neg [in Circuits.GENE.Bool_compl]
Invariant [in Circuits.MULTIPLIER.MultSeq]
Invariant_t_O [in Circuits.MULTIPLIER.MultSeq]
inv_ind_true [in Circuits.MULTIPLIER.MultSeq]
inv_ind_false [in Circuits.MULTIPLIER.MultSeq]
IsNull_BV_null [in Circuits.BLOCK.Fill_defs]
IsNull_null [in Circuits.BLOCK.Fill_defs]
IsNull_cons [in Circuits.BLOCK.Fill_defs]
IsNull_false [in Circuits.BLOCK.Fill_defs]
IsNull_nil [in Circuits.BLOCK.Fill_defs]
L
lem_le_minus_v1_Sn [in Circuits.MULTIPLIER.LemPrelim]length_BV_null [in Circuits.GENE.BV]
length_R2 [in Circuits.MULTIPLIER.Definitions]
length_R1 [in Circuits.MULTIPLIER.Definitions]
length_V2_V1 [in Circuits.MULTIPLIER.Definitions]
length_V2 [in Circuits.MULTIPLIER.Definitions]
length_V1 [in Circuits.MULTIPLIER.Definitions]
length_abit [in Circuits.MULTIPLIER.Definitions]
length_highs [in Circuits.MULTIPLIER.Definitions]
length_BV_full_adder_sum [in Circuits.ADDER.Adder]
length_BV_decrement [in Circuits.ADDER.IncrDecr]
length_BV_increment [in Circuits.ADDER.IncrDecr]
length_al [in Circuits.BLOCK.Fill_spec]
length_cx [in Circuits.BLOCK.Fill_spec]
length_di [in Circuits.BLOCK.Fill_spec]
length_elemlist [in Circuits.GENE.Lists_field]
length_strip [in Circuits.GENE.Lists_field]
length_trunc [in Circuits.GENE.Lists_field]
length_map [in Circuits.GENE.Lists_compl]
length_rev [in Circuits.GENE.Lists_compl]
length_list_const [in Circuits.GENE.Lists_compl]
length_app [in Circuits.GENE.Lists_compl]
length_eq [in Circuits.GENE.Lists_compl]
length_eq2 [in Circuits.GENE.Lists_compl]
length_eq1 [in Circuits.GENE.Lists_compl]
length_replace [in Circuits.GENE.Lists_replace]
len_list_const [in Circuits.GENE.Lists_compl]
len_length [in Circuits.GENE.Lists_compl]
len_app [in Circuits.GENE.Lists_compl]
len_nil_inv [in Circuits.GENE.Lists_compl]
len_cons_not_O [in Circuits.GENE.Lists_compl]
le_SO_length_V1 [in Circuits.MULTIPLIER.Definitions]
le_SO_size [in Circuits.MULTIPLIER.Definitions]
le_length_strip [in Circuits.GENE.Lists_field]
le_length_trunc [in Circuits.GENE.Lists_field]
le_SO_length_v [in Circuits.GENE.Lists_compl]
le_minus_minus [in Circuits.GENE.Arith_compl]
le_plus_lem2 [in Circuits.GENE.Arith_compl]
le_plus_lem1 [in Circuits.GENE.Arith_compl]
le_plus_n_m [in Circuits.GENE.Arith_compl]
list_const_eq2 [in Circuits.GENE.Lists_compl]
list_const_eq1 [in Circuits.GENE.Lists_compl]
lowbit_is_abit [in Circuits.MULTIPLIER.Definitions]
lowbit_is_trunc [in Circuits.MULTIPLIER.Definitions]
lt_plus_n_m [in Circuits.GENE.Arith_compl]
M
mem_t [in Circuits.BLOCK.Fill_spec]mem_mem' [in Circuits.BLOCK.Fill_proof]
mem2_t [in Circuits.BLOCK.Fill_impl]
minus_minus_lem2 [in Circuits.GENE.Arith_compl]
minus_minus_lem1 [in Circuits.GENE.Arith_compl]
minus_le_lem2 [in Circuits.GENE.Arith_compl]
minus_le_lem2c [in Circuits.GENE.Arith_compl]
minus_n_SO [in Circuits.GENE.Arith_compl]
minus_le_O [in Circuits.GENE.Arith_compl]
mult_plus_distr2 [in Circuits.GENE.Arith_compl]
mult_permute [in Circuits.GENE.Arith_compl]
mult_sym [in Circuits.GENE.Arith_compl]
N
neg_eq [in Circuits.GENE.Bool_compl]nil_cons [in Circuits.GENE.Lists_compl]
not_eq_cons [in Circuits.GENE.Lists_compl]
not_nil [in Circuits.GENE.Lists_compl]
not_len_nil_Sn [in Circuits.GENE.Lists_compl]
not_cons_eq [in Circuits.GENE.Lists_compl]
P
plus_O_O [in Circuits.GENE.Arith_compl]plus_permute2 [in Circuits.GENE.Arith_compl]
plus_n_SO [in Circuits.GENE.Arith_compl]
power2_plus [in Circuits.GENE.Arith_compl]
power2_eq2 [in Circuits.GENE.Arith_compl]
R
read_write [in Circuits.GENE.Memo]replace_newer [in Circuits.GENE.Lists_replace]
replace_sym [in Circuits.GENE.Lists_replace]
replace_keep_others [in Circuits.GENE.Lists_replace]
replace_ok [in Circuits.GENE.Lists_replace]
rev_rev [in Circuits.GENE.Lists_compl]
rev_app [in Circuits.GENE.Lists_compl]
rev_eq [in Circuits.GENE.Lists_compl]
rev_eq2 [in Circuits.GENE.Lists_compl]
rev_eq1 [in Circuits.GENE.Lists_compl]
R1_never_nil [in Circuits.MULTIPLIER.Definitions]
R1_eq2 [in Circuits.MULTIPLIER.Definitions]
R1_eq1 [in Circuits.MULTIPLIER.Definitions]
R1_lem3 [in Circuits.MULTIPLIER.LemPrelim]
R1_lem [in Circuits.MULTIPLIER.LemPrelim]
R2_eq2 [in Circuits.MULTIPLIER.Definitions]
R2_eq1 [in Circuits.MULTIPLIER.Definitions]
S
strip_trunc [in Circuits.GENE.Lists_field]strip_trunc_i [in Circuits.GENE.Lists_field]
strip_strip [in Circuits.GENE.Lists_field]
strip_eq [in Circuits.GENE.Lists_field]
strip_sym [in Circuits.GENE.Lists_field]
strip_strip_S [in Circuits.GENE.Lists_field]
strip_app [in Circuits.GENE.Lists_field]
strip_O [in Circuits.GENE.Lists_field]
strip_max [in Circuits.GENE.Lists_field]
strip_all [in Circuits.GENE.Lists_field]
strip_inv [in Circuits.GENE.Lists_field]
strip_cons_S [in Circuits.GENE.Lists_field]
strip_nil [in Circuits.GENE.Lists_field]
T
true_to_false [in Circuits.GENE.Bool_compl]trunc_strip [in Circuits.GENE.Lists_field]
trunc_plus_petit [in Circuits.GENE.Lists_field]
trunc_trunc3 [in Circuits.GENE.Lists_field]
trunc_trunc2 [in Circuits.GENE.Lists_field]
trunc_trunc1 [in Circuits.GENE.Lists_field]
trunc_sym [in Circuits.GENE.Lists_field]
trunc_eq [in Circuits.GENE.Lists_field]
trunc_app [in Circuits.GENE.Lists_field]
trunc_O [in Circuits.GENE.Lists_field]
trunc_max [in Circuits.GENE.Lists_field]
trunc_all [in Circuits.GENE.Lists_field]
trunc_inv [in Circuits.GENE.Lists_field]
V
v_not_nil_length [in Circuits.GENE.Lists_compl]V1_not_nil [in Circuits.MULTIPLIER.Definitions]
V2_not_nil [in Circuits.MULTIPLIER.Definitions]
X
xorb_b_true [in Circuits.GENE.Bool_compl]xorb_b_false [in Circuits.GENE.Bool_compl]
xorb_b_b [in Circuits.GENE.Bool_compl]
Axiom Index
A
al_initsize [in Circuits.BLOCK.Fill_defs]al_init [in Circuits.BLOCK.Fill_defs]
a_size [in Circuits.BLOCK.Fill_defs]
C
cx_initsize [in Circuits.BLOCK.Fill_defs]cx_init [in Circuits.BLOCK.Fill_defs]
D
DC_dsize [in Circuits.BLOCK.Fill_proof]DC_d [in Circuits.BLOCK.Fill_proof]
DC_asize [in Circuits.BLOCK.Fill_proof]
DC_a [in Circuits.BLOCK.Fill_proof]
di_initsize [in Circuits.BLOCK.Fill_defs]
di_init [in Circuits.BLOCK.Fill_defs]
d_size [in Circuits.BLOCK.Fill_defs]
E
eq_list_dec [in Circuits.GENE.Lists_compl]L
length_V2_size [in Circuits.MULTIPLIER.Definitions]length_V1_size [in Circuits.MULTIPLIER.Definitions]
M
mem_initsize [in Circuits.BLOCK.Fill_defs]mem_init [in Circuits.BLOCK.Fill_defs]
S
size [in Circuits.MULTIPLIER.Definitions]size_not_O [in Circuits.MULTIPLIER.Definitions]
V
V1 [in Circuits.MULTIPLIER.Definitions]V2 [in Circuits.MULTIPLIER.Definitions]
Constructor Index
L
len_cons [in Circuits.GENE.Lists_compl]len_nil [in Circuits.GENE.Lists_compl]
Inductive Index
L
len [in Circuits.GENE.Lists_compl]Section Index
L
Lists_field [in Circuits.GENE.Lists_field]Lists_compl [in Circuits.GENE.Lists_compl]
Lists_replace [in Circuits.GENE.Lists_replace]
Definition Index
A
abit [in Circuits.GENE.BV]addr [in Circuits.GENE.Memo]
AddrOK [in Circuits.GENE.Memo]
ad_2_1 [in Circuits.BLOCK.Fill_impl]
ad' [in Circuits.BLOCK.Fill_impl]
ad1 [in Circuits.BLOCK.Fill_impl]
ad2 [in Circuits.BLOCK.Fill_impl]
ad3 [in Circuits.BLOCK.Fill_impl]
al [in Circuits.BLOCK.Fill_spec]
al_2_1 [in Circuits.BLOCK.Fill_impl]
al' [in Circuits.BLOCK.Fill_impl]
al1 [in Circuits.BLOCK.Fill_impl]
al2 [in Circuits.BLOCK.Fill_impl]
al3 [in Circuits.BLOCK.Fill_impl]
appbv [in Circuits.GENE.BV]
app_assoc_l [in Circuits.GENE.Lists_compl]
app_assoc_r [in Circuits.GENE.Lists_compl]
B
bitset [in Circuits.GENE.BV]bool_to_nat [in Circuits.GENE.Bool_compl]
BV [in Circuits.GENE.BV]
BVnot [in Circuits.GENE.BV]
BV_to_nat [in Circuits.GENE.BV]
BV_null [in Circuits.GENE.BV]
BV_full_adder [in Circuits.ADDER.Adder]
BV_full_adder_carry [in Circuits.ADDER.Adder]
BV_full_adder_sum [in Circuits.ADDER.Adder]
BV_decrement_carry [in Circuits.ADDER.IncrDecr]
BV_decrement [in Circuits.ADDER.IncrDecr]
BV_increment_carry [in Circuits.ADDER.IncrDecr]
BV_increment [in Circuits.ADDER.IncrDecr]
C
compo_2_1 [in Circuits.BLOCK.Fill_impl]compo' [in Circuits.BLOCK.Fill_impl]
consbv [in Circuits.GENE.BV]
cx [in Circuits.BLOCK.Fill_spec]
cx_2_1 [in Circuits.BLOCK.Fill_impl]
cx' [in Circuits.BLOCK.Fill_impl]
cx1 [in Circuits.BLOCK.Fill_impl]
cx2 [in Circuits.BLOCK.Fill_impl]
cx3 [in Circuits.BLOCK.Fill_impl]
D
da_2_1 [in Circuits.BLOCK.Fill_impl]da' [in Circuits.BLOCK.Fill_impl]
da1 [in Circuits.BLOCK.Fill_impl]
da2 [in Circuits.BLOCK.Fill_impl]
da3 [in Circuits.BLOCK.Fill_impl]
di [in Circuits.BLOCK.Fill_spec]
di_2_1 [in Circuits.BLOCK.Fill_impl]
di' [in Circuits.BLOCK.Fill_impl]
di1 [in Circuits.BLOCK.Fill_impl]
di2 [in Circuits.BLOCK.Fill_impl]
di3 [in Circuits.BLOCK.Fill_impl]
E
elemlist [in Circuits.GENE.Lists_field]F
field [in Circuits.GENE.BV]full_adder_carry [in Circuits.ADDER.FullAdder]
full_adder_sum [in Circuits.ADDER.FullAdder]
H
half_adder_carry [in Circuits.ADDER.HalfAdder]half_adder_sum [in Circuits.ADDER.HalfAdder]
highs [in Circuits.MULTIPLIER.Definitions]
I
If [in Circuits.GENE.Bool_compl]IsNull [in Circuits.BLOCK.Fill_defs]
L
lenbv [in Circuits.GENE.BV]lengthbv [in Circuits.GENE.BV]
list_const [in Circuits.GENE.Lists_compl]
lowbit [in Circuits.MULTIPLIER.Definitions]
M
map [in Circuits.GENE.Lists_compl]mem [in Circuits.BLOCK.Fill_spec]
Memo [in Circuits.GENE.Memo]
MemoEmpty [in Circuits.GENE.Memo]
MemoRead [in Circuits.GENE.Memo]
MemoSize [in Circuits.GENE.Memo]
MemoWrite [in Circuits.GENE.Memo]
MemoZone [in Circuits.GENE.Memo]
mem_2_1 [in Circuits.BLOCK.Fill_impl]
mem' [in Circuits.BLOCK.Fill_impl]
mem1 [in Circuits.BLOCK.Fill_impl]
mem2 [in Circuits.BLOCK.Fill_impl]
mem3 [in Circuits.BLOCK.Fill_impl]
MMemo [in Circuits.GENE.Memo]
Mux [in Circuits.MULTIPLIER.Definitions]
N
nilbv [in Circuits.GENE.BV]P
power2 [in Circuits.GENE.Arith_compl]R
replace [in Circuits.GENE.Lists_replace]rev [in Circuits.GENE.Lists_compl]
R1 [in Circuits.MULTIPLIER.Definitions]
R2 [in Circuits.MULTIPLIER.Definitions]
S
strip [in Circuits.GENE.Lists_field]stripbv [in Circuits.GENE.BV]
sublist [in Circuits.GENE.Lists_field]
T
trunc [in Circuits.GENE.Lists_field]truncbv [in Circuits.GENE.BV]
X
xorb [in Circuits.GENE.Bool_compl]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (360 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (220 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (90 entries) |