| 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 | (261 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 | (33 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 | (28 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 | (93 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 | (32 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 | (11 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 | (12 entries) |
| Projection 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 | (14 entries) |
| 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 | (9 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 | (25 entries) |
| Record 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) |
Global Index
A
addchains [lemma, in Additions.main]addchain_spec_intro [constructor, in Additions.spec]
addchain_spec [inductive, in Additions.spec]
app [definition, in Additions.machine]
applications [section, in Additions.log2_spec]
applications.log2 [variable, in Additions.log2_spec]
a2x [lemma, in Additions.monoid]
B
big_int [axiom, in Additions.extract]binary [lemma, in Additions.binary_strat]
binary_strat [library]
C
Call [inductive, in Additions.spec]Call_measure [definition, in Additions.generation]
Call_lt [inductive, in Additions.generation]
Call_K [constructor, in Additions.spec]
Call_C [constructor, in Additions.spec]
Call_M [constructor, in Additions.spec]
ceiling_log2 [lemma, in Additions.log2_spec]
chain_algo [lemma, in Additions.generation]
chain_cases [lemma, in Additions.generation]
coarser [definition, in Additions.Wf_compl]
Code [inductive, in Additions.machine]
code_gen [definition, in Additions.main]
COND3 [lemma, in Additions.generation]
Config [record, in Additions.machine]
config [constructor, in Additions.machine]
Config_inv [lemma, in Additions.machine]
config_S [projection, in Additions.machine]
config_X [projection, in Additions.machine]
conform [definition, in Additions.spec]
Constants [library]
C_M_lt [constructor, in Additions.generation]
c_spec [constructor, in Additions.spec]
C2M [lemma, in Additions.develop]
D
decomp [lemma, in Additions.log2_implementation]develop [library]
dic [definition, in Additions.main]
dicho [lemma, in Additions.dicho_strat]
dicho_strat [library]
E
emptystack [constructor, in Additions.machine]End [constructor, in Additions.machine]
enum1 [lemma, in Additions.Le_lt_compl]
enum4 [lemma, in Additions.Le_lt_compl]
euclid [library]
exact [constructor, in Additions.log2_implementation]
Exec [definition, in Additions.machine]
Exec_app [lemma, in Additions.machine]
Exec1 [definition, in Additions.machine]
extract [library]
extract_scm [library]
extract_hs [library]
F
Fib [definition, in Additions.matrix]fibonacci [lemma, in Additions.main]
fib_computation [lemma, in Additions.matrix]
fib_n [lemma, in Additions.matrix]
fib_mat_n [lemma, in Additions.matrix]
fib_mat [definition, in Additions.matrix]
final [inductive, in Additions.log2_implementation]
final_inv [lemma, in Additions.log2_implementation]
floor_log2 [lemma, in Additions.log2_spec]
fmpc [library]
four [definition, in Additions.Constants]
funmono [lemma, in Additions.monofun]
fun_.Id [variable, in Additions.monofun]
fun_.comp [variable, in Additions.monofun]
fun_.eta_A [variable, in Additions.monofun]
fun_.A [variable, in Additions.monofun]
fun_ [section, in Additions.monofun]
G
gencode [inductive, in Additions.spec]gencode_intro [constructor, in Additions.spec]
generation [section, in Additions.generation]
generation [library]
generation.gamma [variable, in Additions.generation]
generation.log2_r [variable, in Additions.generation]
H
half_lt [lemma, in Additions.shift]holes_in_powers [lemma, in Additions.two_power]
I
Id2 [definition, in Additions.matrix]imperative [library]
import_log2.log2_r [variable, in Additions.dicho_strat]
import_log2 [section, in Additions.dicho_strat]
inexact [constructor, in Additions.log2_implementation]
Instr [inductive, in Additions.machine]
int [axiom, in Additions.extract]
int [axiom, in Additions.extract_scm]
int [axiom, in Additions.extract_hs]
invar [inductive, in Additions.log2_implementation]
invar_inv3 [lemma, in Additions.log2_implementation]
invar_inv2 [lemma, in Additions.log2_implementation]
invar_inv1 [lemma, in Additions.log2_implementation]
i2n [axiom, in Additions.extract]
i2n [axiom, in Additions.extract_scm]
i2n [axiom, in Additions.extract_hs]
K
KMC [lemma, in Additions.develop]KMK [lemma, in Additions.develop]
K_K_lt [constructor, in Additions.generation]
K_C_lt [constructor, in Additions.generation]
k_spec [constructor, in Additions.spec]
L
le_q_qbr [lemma, in Additions.euclid]Le_lt_compl [library]
le5 [lemma, in Additions.Le_lt_compl]
log2_unicity [lemma, in Additions.two_power]
log2_spec [definition, in Additions.log2_spec]
log2_impl [lemma, in Additions.log2_implementation]
log2_computation.init [variable, in Additions.log2_implementation]
log2_computation.pos_n0 [variable, in Additions.log2_implementation]
log2_computation.n0 [variable, in Additions.log2_implementation]
log2_computation [section, in Additions.log2_implementation]
log2_spec [library]
log2_implementation [library]
loopexec [lemma, in Additions.while]
lt_O_q [lemma, in Additions.euclid]
lt_q_qbr' [lemma, in Additions.euclid]
lt_q_qbr [lemma, in Additions.euclid]
lt_b_qbr [lemma, in Additions.euclid]
lt_a_a_plus_b [lemma, in Additions.Le_lt_compl]
lt_not_lt [lemma, in Additions.Le_lt_compl]
lt_or_Zero [lemma, in Additions.Le_lt_compl]
M
machine [library]main [library]
matrix [lemma, in Additions.matrix]
matrix [library]
Mat_assoc [axiom, in Additions.matrix]
Mat_mult [definition, in Additions.matrix]
Mat2 [record, in Additions.matrix]
mat2 [constructor, in Additions.matrix]
measure_compat [lemma, in Additions.generation]
mkfinal [constructor, in Additions.log2_implementation]
mkmonoid [constructor, in Additions.monoid]
mkstate [constructor, in Additions.log2_implementation]
mkstrat [constructor, in Additions.strategies]
MMC [lemma, in Additions.develop]
MMK [lemma, in Additions.develop]
monofun [library]
monoid [record, in Additions.monoid]
Monoid [section, in Additions.machine]
monoid [library]
monoid_def.o' [variable, in Additions.monoid]
monoid_def.u' [variable, in Additions.monoid]
monoid_def.MO [variable, in Additions.monoid]
monoid_def.M [variable, in Additions.monoid]
monoid_def [section, in Additions.monoid]
Monoid.M [variable, in Additions.machine]
Monoid.MO [variable, in Additions.machine]
Monoid.oM [variable, in Additions.machine]
Monoid.uM [variable, in Additions.machine]
MUL [constructor, in Additions.machine]
mult_p_le_pq [lemma, in Additions.Mult_compl]
mult_p_lt_pq [lemma, in Additions.Mult_compl]
mult_p_le_qp [lemma, in Additions.Mult_compl]
mult_p_lt_qp [lemma, in Additions.Mult_compl]
mult_inj_l [lemma, in Additions.Mult_compl]
mult_lt_r [lemma, in Additions.Mult_compl]
mult_le_r [lemma, in Additions.Mult_compl]
mult_lt_l [lemma, in Additions.Mult_compl]
mult_le_l [lemma, in Additions.Mult_compl]
Mult_compl [library]
M_K_lt [constructor, in Additions.generation]
M_C_lt [constructor, in Additions.generation]
M_M_lt [constructor, in Additions.generation]
m_spec [constructor, in Additions.spec]
M11 [projection, in Additions.matrix]
M12 [projection, in Additions.matrix]
M2q [lemma, in Additions.develop]
M21 [projection, in Additions.matrix]
M22 [projection, in Additions.matrix]
M3 [lemma, in Additions.develop]
N
not_lt_le [lemma, in Additions.Le_lt_compl]not_le_lt [lemma, in Additions.Le_lt_compl]
not_final [lemma, in Additions.log2_implementation]
O
o [projection, in Additions.monoid]obsolete_debug [lemma, in Additions.trivial]
ok [inductive, in Additions.log2_implementation]
okfalse [constructor, in Additions.log2_implementation]
oktrue [constructor, in Additions.log2_implementation]
one [definition, in Additions.Constants]
one_cases [lemma, in Additions.Le_lt_compl]
o'_assoc [lemma, in Additions.monoid]
P
plus_n_1 [lemma, in Additions.shift]point_assoc [projection, in Additions.monoid]
pop [definition, in Additions.machine]
power [definition, in Additions.monoid]
power_algo_r [definition, in Additions.main]
power_algo [lemma, in Additions.generation]
power_eucl [lemma, in Additions.monoid]
power_mult [lemma, in Additions.monoid]
power_sym [lemma, in Additions.monoid]
power_1 [lemma, in Additions.monoid]
power_plus [lemma, in Additions.monoid]
power_u [lemma, in Additions.monoid]
Prop_wfi [lemma, in Additions.Wf_compl]
Prop_induction.W [variable, in Additions.Wf_compl]
Prop_induction.R [variable, in Additions.Wf_compl]
Prop_induction.A [variable, in Additions.Wf_compl]
Prop_induction [section, in Additions.Wf_compl]
push [constructor, in Additions.machine]
PUSH [constructor, in Additions.machine]
Q
quotient_gt_one [lemma, in Additions.Mult_compl]quotient_positive [lemma, in Additions.Mult_compl]
S
seq [constructor, in Additions.machine]shift [definition, in Additions.shift]
shift [library]
shift_Fib [definition, in Additions.matrix]
Simpl_shift_Fib [lemma, in Additions.matrix]
Spec [inductive, in Additions.spec]
spec [library]
SQR [constructor, in Additions.machine]
Stack [inductive, in Additions.machine]
standard [lemma, in Additions.standard]
standard [library]
startloop [lemma, in Additions.while]
state [record, in Additions.log2_implementation]
state_b [projection, in Additions.log2_implementation]
state_p [projection, in Additions.log2_implementation]
state_n [projection, in Additions.log2_implementation]
stat_order [definition, in Additions.log2_implementation]
strategies [library]
strategy [inductive, in Additions.strategies]
SWAP [constructor, in Additions.machine]
T
three [definition, in Additions.Constants]top [definition, in Additions.machine]
trivial [lemma, in Additions.trivial]
trivial [library]
two [definition, in Additions.Constants]
two_power_monoR [lemma, in Additions.two_power]
two_power_le [lemma, in Additions.two_power]
two_power_mono [lemma, in Additions.two_power]
two_power_S_lt [lemma, in Additions.two_power]
two_power_S [lemma, in Additions.two_power]
two_power [definition, in Additions.two_power]
two_power [library]
U
u [projection, in Additions.monoid]Unfold_shift_Fib [lemma, in Additions.matrix]
Unfold_FibSSn [lemma, in Additions.matrix]
Unfold_Fib1 [lemma, in Additions.matrix]
Unfold_FibO [lemma, in Additions.matrix]
Unshift [lemma, in Additions.shift]
u_neutral_r [projection, in Additions.monoid]
u_neutral_l [projection, in Additions.monoid]
u'_neutral_r [lemma, in Additions.monoid]
u'_neutral_l [lemma, in Additions.monoid]
W
wf_coarser [lemma, in Additions.Wf_compl]Wf_Call_lt [lemma, in Additions.generation]
wf_stat_order [lemma, in Additions.log2_implementation]
Wf_compl [library]
while [library]
while_not [lemma, in Additions.while]
while_do.Termi [variable, in Additions.while]
while_do.loopstart [variable, in Additions.while]
while_do.LoopExit_ok [variable, in Additions.while]
while_do.Onestep [variable, in Additions.while]
while_do.LoopExit_dec [variable, in Additions.while]
while_do.LoopExit [variable, in Additions.while]
while_do.term_order [variable, in Additions.while]
while_do.Invar [variable, in Additions.while]
while_do.precond [variable, in Additions.while]
while_do.postcond [variable, in Additions.while]
while_do.St [variable, in Additions.while]
while_do [section, in Additions.while]
Z
zero_lt_pow [lemma, in Additions.two_power]z2b [axiom, in Additions.extract]
z2i [axiom, in Additions.extract_scm]
z2i [axiom, in Additions.extract_hs]
Variable Index
A
applications.log2 [in Additions.log2_spec]F
fun_.Id [in Additions.monofun]fun_.comp [in Additions.monofun]
fun_.eta_A [in Additions.monofun]
fun_.A [in Additions.monofun]
G
generation.gamma [in Additions.generation]generation.log2_r [in Additions.generation]
I
import_log2.log2_r [in Additions.dicho_strat]L
log2_computation.init [in Additions.log2_implementation]log2_computation.pos_n0 [in Additions.log2_implementation]
log2_computation.n0 [in Additions.log2_implementation]
M
monoid_def.o' [in Additions.monoid]monoid_def.u' [in Additions.monoid]
monoid_def.MO [in Additions.monoid]
monoid_def.M [in Additions.monoid]
Monoid.M [in Additions.machine]
Monoid.MO [in Additions.machine]
Monoid.oM [in Additions.machine]
Monoid.uM [in Additions.machine]
P
Prop_induction.W [in Additions.Wf_compl]Prop_induction.R [in Additions.Wf_compl]
Prop_induction.A [in Additions.Wf_compl]
W
while_do.Termi [in Additions.while]while_do.loopstart [in Additions.while]
while_do.LoopExit_ok [in Additions.while]
while_do.Onestep [in Additions.while]
while_do.LoopExit_dec [in Additions.while]
while_do.LoopExit [in Additions.while]
while_do.term_order [in Additions.while]
while_do.Invar [in Additions.while]
while_do.precond [in Additions.while]
while_do.postcond [in Additions.while]
while_do.St [in Additions.while]
Library Index
B
binary_stratC
ConstantsD
developdicho_strat
E
euclidextract
extract_scm
extract_hs
F
fmpcG
generationI
imperativeL
Le_lt_compllog2_spec
log2_implementation
M
machinemain
matrix
monofun
monoid
Mult_compl
S
shiftspec
standard
strategies
T
trivialtwo_power
W
Wf_complwhile
Lemma Index
A
addchains [in Additions.main]a2x [in Additions.monoid]
B
binary [in Additions.binary_strat]C
ceiling_log2 [in Additions.log2_spec]chain_algo [in Additions.generation]
chain_cases [in Additions.generation]
COND3 [in Additions.generation]
Config_inv [in Additions.machine]
C2M [in Additions.develop]
D
decomp [in Additions.log2_implementation]dicho [in Additions.dicho_strat]
E
enum1 [in Additions.Le_lt_compl]enum4 [in Additions.Le_lt_compl]
Exec_app [in Additions.machine]
F
fibonacci [in Additions.main]fib_computation [in Additions.matrix]
fib_n [in Additions.matrix]
fib_mat_n [in Additions.matrix]
final_inv [in Additions.log2_implementation]
floor_log2 [in Additions.log2_spec]
funmono [in Additions.monofun]
H
half_lt [in Additions.shift]holes_in_powers [in Additions.two_power]
I
invar_inv3 [in Additions.log2_implementation]invar_inv2 [in Additions.log2_implementation]
invar_inv1 [in Additions.log2_implementation]
K
KMC [in Additions.develop]KMK [in Additions.develop]
L
le_q_qbr [in Additions.euclid]le5 [in Additions.Le_lt_compl]
log2_unicity [in Additions.two_power]
log2_impl [in Additions.log2_implementation]
loopexec [in Additions.while]
lt_O_q [in Additions.euclid]
lt_q_qbr' [in Additions.euclid]
lt_q_qbr [in Additions.euclid]
lt_b_qbr [in Additions.euclid]
lt_a_a_plus_b [in Additions.Le_lt_compl]
lt_not_lt [in Additions.Le_lt_compl]
lt_or_Zero [in Additions.Le_lt_compl]
M
matrix [in Additions.matrix]measure_compat [in Additions.generation]
MMC [in Additions.develop]
MMK [in Additions.develop]
mult_p_le_pq [in Additions.Mult_compl]
mult_p_lt_pq [in Additions.Mult_compl]
mult_p_le_qp [in Additions.Mult_compl]
mult_p_lt_qp [in Additions.Mult_compl]
mult_inj_l [in Additions.Mult_compl]
mult_lt_r [in Additions.Mult_compl]
mult_le_r [in Additions.Mult_compl]
mult_lt_l [in Additions.Mult_compl]
mult_le_l [in Additions.Mult_compl]
M2q [in Additions.develop]
M3 [in Additions.develop]
N
not_lt_le [in Additions.Le_lt_compl]not_le_lt [in Additions.Le_lt_compl]
not_final [in Additions.log2_implementation]
O
obsolete_debug [in Additions.trivial]one_cases [in Additions.Le_lt_compl]
o'_assoc [in Additions.monoid]
P
plus_n_1 [in Additions.shift]power_algo [in Additions.generation]
power_eucl [in Additions.monoid]
power_mult [in Additions.monoid]
power_sym [in Additions.monoid]
power_1 [in Additions.monoid]
power_plus [in Additions.monoid]
power_u [in Additions.monoid]
Prop_wfi [in Additions.Wf_compl]
Q
quotient_gt_one [in Additions.Mult_compl]quotient_positive [in Additions.Mult_compl]
S
Simpl_shift_Fib [in Additions.matrix]standard [in Additions.standard]
startloop [in Additions.while]
T
trivial [in Additions.trivial]two_power_monoR [in Additions.two_power]
two_power_le [in Additions.two_power]
two_power_mono [in Additions.two_power]
two_power_S_lt [in Additions.two_power]
two_power_S [in Additions.two_power]
U
Unfold_shift_Fib [in Additions.matrix]Unfold_FibSSn [in Additions.matrix]
Unfold_Fib1 [in Additions.matrix]
Unfold_FibO [in Additions.matrix]
Unshift [in Additions.shift]
u'_neutral_r [in Additions.monoid]
u'_neutral_l [in Additions.monoid]
W
wf_coarser [in Additions.Wf_compl]Wf_Call_lt [in Additions.generation]
wf_stat_order [in Additions.log2_implementation]
while_not [in Additions.while]
Z
zero_lt_pow [in Additions.two_power]Constructor Index
A
addchain_spec_intro [in Additions.spec]C
Call_K [in Additions.spec]Call_C [in Additions.spec]
Call_M [in Additions.spec]
config [in Additions.machine]
C_M_lt [in Additions.generation]
c_spec [in Additions.spec]
E
emptystack [in Additions.machine]End [in Additions.machine]
exact [in Additions.log2_implementation]
G
gencode_intro [in Additions.spec]I
inexact [in Additions.log2_implementation]K
K_K_lt [in Additions.generation]K_C_lt [in Additions.generation]
k_spec [in Additions.spec]
M
mat2 [in Additions.matrix]mkfinal [in Additions.log2_implementation]
mkmonoid [in Additions.monoid]
mkstate [in Additions.log2_implementation]
mkstrat [in Additions.strategies]
MUL [in Additions.machine]
M_K_lt [in Additions.generation]
M_C_lt [in Additions.generation]
M_M_lt [in Additions.generation]
m_spec [in Additions.spec]
O
okfalse [in Additions.log2_implementation]oktrue [in Additions.log2_implementation]
P
push [in Additions.machine]PUSH [in Additions.machine]
S
seq [in Additions.machine]SQR [in Additions.machine]
SWAP [in Additions.machine]
Axiom Index
B
big_int [in Additions.extract]I
int [in Additions.extract]int [in Additions.extract_scm]
int [in Additions.extract_hs]
i2n [in Additions.extract]
i2n [in Additions.extract_scm]
i2n [in Additions.extract_hs]
M
Mat_assoc [in Additions.matrix]Z
z2b [in Additions.extract]z2i [in Additions.extract_scm]
z2i [in Additions.extract_hs]
Inductive Index
A
addchain_spec [in Additions.spec]C
Call [in Additions.spec]Call_lt [in Additions.generation]
Code [in Additions.machine]
F
final [in Additions.log2_implementation]G
gencode [in Additions.spec]I
Instr [in Additions.machine]invar [in Additions.log2_implementation]
O
ok [in Additions.log2_implementation]S
Spec [in Additions.spec]Stack [in Additions.machine]
strategy [in Additions.strategies]
Projection Index
C
config_S [in Additions.machine]config_X [in Additions.machine]
M
M11 [in Additions.matrix]M12 [in Additions.matrix]
M21 [in Additions.matrix]
M22 [in Additions.matrix]
O
o [in Additions.monoid]P
point_assoc [in Additions.monoid]S
state_b [in Additions.log2_implementation]state_p [in Additions.log2_implementation]
state_n [in Additions.log2_implementation]
U
u [in Additions.monoid]u_neutral_r [in Additions.monoid]
u_neutral_l [in Additions.monoid]
Section Index
A
applications [in Additions.log2_spec]F
fun_ [in Additions.monofun]G
generation [in Additions.generation]I
import_log2 [in Additions.dicho_strat]L
log2_computation [in Additions.log2_implementation]M
Monoid [in Additions.machine]monoid_def [in Additions.monoid]
P
Prop_induction [in Additions.Wf_compl]W
while_do [in Additions.while]Definition Index
A
app [in Additions.machine]C
Call_measure [in Additions.generation]coarser [in Additions.Wf_compl]
code_gen [in Additions.main]
conform [in Additions.spec]
D
dic [in Additions.main]E
Exec [in Additions.machine]Exec1 [in Additions.machine]
F
Fib [in Additions.matrix]fib_mat [in Additions.matrix]
four [in Additions.Constants]
I
Id2 [in Additions.matrix]L
log2_spec [in Additions.log2_spec]M
Mat_mult [in Additions.matrix]O
one [in Additions.Constants]P
pop [in Additions.machine]power [in Additions.monoid]
power_algo_r [in Additions.main]
S
shift [in Additions.shift]shift_Fib [in Additions.matrix]
stat_order [in Additions.log2_implementation]
T
three [in Additions.Constants]top [in Additions.machine]
two [in Additions.Constants]
two_power [in Additions.two_power]
Record Index
C
Config [in Additions.machine]M
Mat2 [in Additions.matrix]monoid [in Additions.monoid]
S
state [in Additions.log2_implementation]| 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 | (261 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 | (33 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 | (28 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 | (93 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 | (32 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 | (11 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 | (12 entries) |
| Projection 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 | (14 entries) |
| 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 | (9 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 | (25 entries) |
| Record 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) |