Global Index

J

Y

Z

_

(958 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

(23 entries)

Variable Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(171 entries)

Library Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(32 entries)

Lemma Index

J

Q

X

Y

Z

_

other

(366 entries)

Constructor Index

A

D

F

G

H

J

K

O

Q

U

Y

Z

_

other

(60 entries)

Axiom Index

A

B

D

G

H

I

J

K

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Inductive Index

A

B

D

F

G

H

J

K

O

Q

U

X

Y

Z

_

other

(24 entries)

Projection Index

A

B

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

Y

Z

_

other

(15 entries)

Section Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(36 entries)

Abbreviation Index

D

H

J

L

O

Q

T

U

X

Y

Z

_

other

(76 entries)

Definition Index

J

O

U

X

Y

Z

_

other

(145 entries)

Record Index

A

B

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)

Global Index

A

AccSl [lemma, in Kildall.inst.inst_types]
AccSSE [lemma, in Kildall.inst.inst_shapes]
AccTop_T [lemma, in Kildall.inst.inst_types]
AccTop_S [lemma, in Kildall.inst.inst_shapes]
Acc_ssw [abbreviation, in Kildall.kildall.itera_property]
acc_ssw [lemma, in Kildall.kildall.iteraterme]
alt_monostep_aux2 [lemma, in Kildall.lists.m_list]
alt_monostep_aux1 [lemma, in Kildall.lists.m_list]
antisymmetric_vector_pointwise [lemma, in Kildall.lists.vector_results]
apply [definition, in Kildall.inst.substitutions]
apply_elem_pattern [lemma, in Kildall.inst.substitutions]
apply_elem_commut [lemma, in Kildall.inst.substitutions]
apply_applied [lemma, in Kildall.inst.substitutions]
apply_elem_in_subst [lemma, in Kildall.inst.substitutions]
apply_elem_var_not_in_unchanged [lemma, in Kildall.inst.substitutions]
apply_substitution_concat [lemma, in Kildall.inst.substitutions]
apply_substitution_cons [lemma, in Kildall.inst.substitutions]
apply_cons [lemma, in Kildall.inst.substitutions]
apply_to_forest [lemma, in Kildall.inst.substitutions]
apply_elem_to_forest [lemma, in Kildall.inst.substitutions]
apply_unchanged [lemma, in Kildall.inst.substitutions]
apply_elem_forest_unchanged [lemma, in Kildall.inst.substitutions]
apply_elem_unchanged [lemma, in Kildall.inst.substitutions]
apply_elem_tree [definition, in Kildall.inst.substitutions]
app_list_typing [lemma, in Kildall.inst.typing]
args_to_tree_typing [lemma, in Kildall.inst.typing]
ascending_chain [definition, in Kildall.aux.relations]
asc_vector_pointwise [lemma, in Kildall.lists.well_founded]
asc_list.eq_A_dec [variable, in Kildall.lists.well_founded]
asc_list.ra [variable, in Kildall.lists.well_founded]
asc_list.A [variable, in Kildall.lists.well_founded]
asc_list [section, in Kildall.lists.well_founded]
aug_wl [lemma, in Kildall.kildall.kildall]
aux [lemma, in Kildall.kildall.kildall]
aux_arith [section, in Kildall.aux.aux_arith]
aux_init_vars_length [lemma, in Kildall.inst.substitutions]
aux_arith [library]
aux2 [lemma, in Kildall.kildall.kildall]

B

bc [abbreviation, in Kildall.inst.inst_types]
bc [abbreviation, in Kildall.inst.inst_shapes]
belong_list_to_pred_list [lemma, in Kildall.lists.pred_list]
belong_pred_list_to_list [lemma, in Kildall.lists.pred_list]
belong_and_snd [lemma, in Kildall.lists.m_list]
belong_and_fst [lemma, in Kildall.lists.m_list]
belong_element_vector [definition, in Kildall.lists.vector]
binop [definition, in Kildall.aux.relations]
Bot_T_bot [lemma, in Kildall.inst.inst_types]
Bot_T [constructor, in Kildall.inst.inst_types]
Bot_S_bot [lemma, in Kildall.inst.inst_shapes]
Bot_S [constructor, in Kildall.inst.inst_shapes]

C

combaux1 [lemma, in Kildall.lists.m_list]
combaux2 [lemma, in Kildall.lists.m_list]
combine [definition, in Kildall.lists.m_list]
commutative_replace [lemma, in Kildall.lists.vector_results]
compose [definition, in Kildall.kildall.iteraterme]
compose_map [lemma, in Kildall.lists.lists]
concat_map [lemma, in Kildall.lists.lists]
concat_In [lemma, in Kildall.lists.lists]
concat_length [lemma, in Kildall.lists.lists]
configuration [abbreviation, in Kildall.inst.machine_shapes]
configuration [abbreviation, in Kildall.inst.instructions]
configuration [abbreviation, in Kildall.inst.machine_types]
configuration [abbreviation, in Kildall.inst.machine]
configuration [abbreviation, in Kildall.inst.fresh_variables]
config_wrap_wt_list [constructor, in Kildall.inst.machine_types]
config_wrap_result [constructor, in Kildall.inst.machine_types]
config_wrap_error [constructor, in Kildall.inst.machine_types]
config_wrap [inductive, in Kildall.inst.machine_types]
config_runtime [constructor, in Kildall.inst.machine]
config_stopped [constructor, in Kildall.inst.machine]
config_error [inductive, in Kildall.inst.machine]
config_is_result [constructor, in Kildall.inst.machine]
config_result [inductive, in Kildall.inst.machine]
constant_list [definition, in Kildall.lists.vector]
constr [record, in Kildall.inst.instructions]
constructors [axiom, in Kildall.inst.machine]
cons_eq [lemma, in Kildall.lists.lists]
cons_ret [projection, in Kildall.inst.instructions]
cons_args [projection, in Kildall.inst.instructions]
cons_name [projection, in Kildall.inst.instructions]
cons_list_typing [lemma, in Kildall.inst.typing]
contrap [lemma, in Kildall.kildall.kildall_dfa]

D

Data_flow_analysis.r_is_order [variable, in Kildall.kildall.dfa]
Data_flow_analysis.step_succs_same_length [variable, in Kildall.kildall.dfa]
Data_flow_analysis.T [variable, in Kildall.kildall.dfa]
Data_flow_analysis.r [variable, in Kildall.kildall.dfa]
Data_flow_analysis.wi [variable, in Kildall.kildall.dfa]
Data_flow_analysis.step [variable, in Kildall.kildall.dfa]
Data_flow_analysis.succs [variable, in Kildall.kildall.dfa]
Data_flow_analysis.n [variable, in Kildall.kildall.dfa]
Data_flow_analysis.Sigma [variable, in Kildall.kildall.dfa]
Data_flow_analysis [section, in Kildall.kildall.dfa]
dec_belong [lemma, in Kildall.lists.vector_results]
dep_r_Top_T_2 [lemma, in Kildall.inst.inst_types]
dep_r_Bot_T_2 [lemma, in Kildall.inst.inst_types]
dep_r_Top_T_1 [lemma, in Kildall.inst.inst_types]
dep_r_Bot_T_1 [lemma, in Kildall.inst.inst_types]
dep_r_Top_2 [lemma, in Kildall.inst.inst_shapes]
dep_r_Bot_2 [lemma, in Kildall.inst.inst_shapes]
dep_r_Top_1 [lemma, in Kildall.inst.inst_shapes]
dep_r_Bot_1 [lemma, in Kildall.inst.inst_shapes]
dfa [library]
dfa_is_bv [lemma, in Kildall.kildall.dfa]
dfa_type [definition, in Kildall.kildall.dfa]
does_not_belong_is_not_element [lemma, in Kildall.lists.vector_results]

E

element_at_unsafe_some [lemma, in Kildall.lists.vector_results]
element_at_unsafe_none [lemma, in Kildall.lists.vector_results]
element_at_to_unsafe [lemma, in Kildall.lists.vector_results]
element_at_unsafe_to_safe [lemma, in Kildall.lists.vector_results]
element_at_constant_list [lemma, in Kildall.lists.vector_results]
element_at_0_is_head [lemma, in Kildall.lists.vector_results]
element_at_belong [lemma, in Kildall.lists.vector_results]
element_at_irrel [lemma, in Kildall.lists.vector_results]
element_at_in_replaced' [lemma, in Kildall.lists.vector_results]
element_at_in_replaced [lemma, in Kildall.lists.vector_results]
element_at_list_map' [lemma, in Kildall.lists.lists]
element_at_list_map [lemma, in Kildall.lists.lists]
element_at_list_rev [lemma, in Kildall.lists.lists]
element_at_list_concat' [lemma, in Kildall.lists.lists]
element_at_list_concat [lemma, in Kildall.lists.lists]
element_at_list_in [lemma, in Kildall.lists.lists]
element_at_list_none [lemma, in Kildall.lists.lists]
element_at_list_some [lemma, in Kildall.lists.lists]
element_at_list [definition, in Kildall.lists.lists]
element_at_init_subst [lemma, in Kildall.inst.substitutions]
element_at_init_vars [lemma, in Kildall.inst.substitutions]
element_at_list_typing [lemma, in Kildall.inst.typing]
element_at_unsafe [definition, in Kildall.lists.vector]
element_at [definition, in Kildall.lists.vector]
empty [lemma, in Kildall.lists.vector]
empty_dep [lemma, in Kildall.lists.vector]
eq_dec_to_list_eq_dec [lemma, in Kildall.lists.vector_results]
eq_Sigma_dec [lemma, in Kildall.inst.inst_types]
eq_list_name_dec [lemma, in Kildall.inst.inst_types]
eq_tree_dec [lemma, in Kildall.aux.tree]
eq_value_dec [abbreviation, in Kildall.inst.instructions]
eq_name_dec [axiom, in Kildall.inst.instructions]
eq_configuration_nil_dec [lemma, in Kildall.inst.machine_types]
eq_Sigma_S_dec [lemma, in Kildall.inst.inst_shapes]
eq_Substitution_dec [lemma, in Kildall.inst.substitutions]
eq_list_Expression_dec [lemma, in Kildall.inst.substitutions]
eq_Expression_dec [lemma, in Kildall.inst.substitutions]
eq_Name_dec [lemma, in Kildall.inst.substitutions]
eq_prod_dec [lemma, in Kildall.lists.m_list]
eq_list [definition, in Kildall.lists.vector]
execution [inductive, in Kildall.inst.machine]
execution_length [lemma, in Kildall.inst.machine_types]
execution_step [constructor, in Kildall.inst.machine]
execution_init [constructor, in Kildall.inst.machine]
Expression [abbreviation, in Kildall.inst.machine_shapes]
Expression [abbreviation, in Kildall.inst.inst_shapes]
Expression [abbreviation, in Kildall.inst.substitutions]
Expression [abbreviation, in Kildall.inst.fresh_variables]

F

f [definition, in Kildall.inst.inst_types]
fcn_bytecode [projection, in Kildall.inst.instructions]
fcn_size [projection, in Kildall.inst.instructions]
fcn_ret [projection, in Kildall.inst.instructions]
fcn_args [projection, in Kildall.inst.instructions]
fcn_name [projection, in Kildall.inst.instructions]
fl [definition, in Kildall.kildall.iteraterme]
fold_inc [lemma, in Kildall.aux.tree]
fold_dom [lemma, in Kildall.aux.tree]
fold_bool_or_true [lemma, in Kildall.lists.lists]
fold_bool_or_false [lemma, in Kildall.lists.lists]
fold_bool_or_first_true [lemma, in Kildall.lists.lists]
fold_bool_and_true [lemma, in Kildall.lists.lists]
fold_bool_and_false [lemma, in Kildall.lists.lists]
fold_bool_and_first_false [lemma, in Kildall.lists.lists]
fold_bool.f [variable, in Kildall.lists.lists]
fold_bool.A [variable, in Kildall.lists.lists]
fold_bool [section, in Kildall.lists.lists]
fold_left2 [definition, in Kildall.inst.typing]
fonctionnal_reduction [definition, in Kildall.inst.machine_types]
forall_element_to_vector_pointwise [lemma, in Kildall.lists.vector_results]
forest [abbreviation, in Kildall.aux.tree]
frame [record, in Kildall.inst.instructions]
frames_args_length [definition, in Kildall.inst.machine_types]
fresh [definition, in Kildall.inst.substitutions]
fresh_variables.Passed_Kildall [variable, in Kildall.inst.fresh_variables]
fresh_variables.Passed_Kildall_Types [variable, in Kildall.inst.fresh_variables]
fresh_variables.fwd_jmp [variable, in Kildall.inst.fresh_variables]
fresh_variables [section, in Kildall.inst.fresh_variables]
fresh_variables [library]
Frm [abbreviation, in Kildall.inst.machine_shapes]
Frm [abbreviation, in Kildall.inst.machine_types]
Frm [abbreviation, in Kildall.inst.fresh_variables]
frm_args [projection, in Kildall.inst.instructions]
frm_stack [projection, in Kildall.inst.instructions]
frm_pc [projection, in Kildall.inst.instructions]
frm_fun [projection, in Kildall.inst.instructions]
function [record, in Kildall.inst.instructions]
functions [axiom, in Kildall.inst.machine]
f_is_lub [lemma, in Kildall.inst.inst_types]

G

Get_constr [abbreviation, in Kildall.inst.machine_shapes]
Get_function [abbreviation, in Kildall.inst.machine_shapes]
Get_constr [abbreviation, in Kildall.inst.inst_types]
Get_function [abbreviation, in Kildall.inst.inst_types]
get_some_in_functions [lemma, in Kildall.inst.instructions]
get_constr_by_name [definition, in Kildall.inst.instructions]
get_function_by_name [definition, in Kildall.inst.instructions]
Get_constr [abbreviation, in Kildall.inst.machine_types]
Get_function [abbreviation, in Kildall.inst.machine_types]
Get_constr [abbreviation, in Kildall.inst.inst_shapes]
Get_function [abbreviation, in Kildall.inst.inst_shapes]
Get_function [abbreviation, in Kildall.inst.substitutions]
Get_constr [abbreviation, in Kildall.inst.typing]
Get_constr [abbreviation, in Kildall.inst.machine]
Get_function [abbreviation, in Kildall.inst.machine]
Get_constr [abbreviation, in Kildall.inst.fresh_variables]
Get_function [abbreviation, in Kildall.inst.fresh_variables]

H

hd' [definition, in Kildall.lists.vector]
head [definition, in Kildall.lists.vector]
head' [definition, in Kildall.lists.vector]
Hvars [definition, in Kildall.inst.machine_shapes]
Hvars [definition, in Kildall.inst.fresh_variables]
Hvars_Kildall_Shapes [lemma, in Kildall.inst.fresh_variables]
Hvars_Shapes [lemma, in Kildall.inst.fresh_variables]
Hvars_Sp_Bot [lemma, in Kildall.inst.fresh_variables]
Hvars_Sp_Top [lemma, in Kildall.inst.fresh_variables]
Hvars_Bot_S [lemma, in Kildall.inst.fresh_variables]
Hvars_Top_S [lemma, in Kildall.inst.fresh_variables]
Hvars_replace_Bot [lemma, in Kildall.inst.fresh_variables]
Hvars_replace_Top [lemma, in Kildall.inst.fresh_variables]
hyp_belong_convert [lemma, in Kildall.lists.pred_list]

I

idempotent_replace [lemma, in Kildall.lists.vector_results]
idempotent_lub [lemma, in Kildall.aux.semilattices]
immediate_subtree_size [lemma, in Kildall.aux.tree]
inc_w_propa_w [lemma, in Kildall.kildall.propa]
inc_propa_w_propa_replace_ss_w [lemma, in Kildall.kildall.propa_property]
init_stack_shaping [lemma, in Kildall.inst.substitutions]
init_subst_apply [lemma, in Kildall.inst.substitutions]
init_subst_member [lemma, in Kildall.inst.substitutions]
init_vars_length [lemma, in Kildall.inst.substitutions]
init_subst [definition, in Kildall.inst.substitutions]
init_vars [definition, in Kildall.inst.substitutions]
Init_configuration [definition, in Kildall.inst.machine]
Instruction [abbreviation, in Kildall.inst.inst_types]
instruction [inductive, in Kildall.inst.instructions]
Instruction [abbreviation, in Kildall.inst.inst_shapes]
instructions [section, in Kildall.inst.instructions]
instructions [library]
inst_types.fcn [variable, in Kildall.inst.inst_types]
inst_types [section, in Kildall.inst.inst_types]
inst_shapes.fcn [variable, in Kildall.inst.inst_shapes]
inst_shapes [section, in Kildall.inst.inst_shapes]
inst_shapes [library]
inst_types [library]
inv [definition, in Kildall.aux.relations]
Invariant [definition, in Kildall.inst.machine]
In_mapped [lemma, in Kildall.lists.lists]
In_rev [lemma, in Kildall.lists.lists]
In_concat [lemma, in Kildall.lists.lists]
In_fresh [lemma, in Kildall.inst.substitutions]
In_fresh_not_var_in [lemma, in Kildall.inst.substitutions]
in_snd_in_snd_combine [lemma, in Kildall.lists.m_list]
in_snd_combine_in_snd [lemma, in Kildall.lists.m_list]
in_fst_in_fst_combine [lemma, in Kildall.lists.m_list]
in_fst_combine_in_fst [lemma, in Kildall.lists.m_list]
IS_bytecode_verifier [abbreviation, in Kildall.kildall.kildall_bv]
IS_data_flow_analyser [abbreviation, in Kildall.kildall.kildall_bv]
is_not_element_does_not_belong [lemma, in Kildall.lists.vector_results]
Is_bytecode_verifier [definition, in Kildall.kildall.dfa]
Is_data_flow_analyser [definition, in Kildall.kildall.dfa]
is_top_element [definition, in Kildall.kildall.dfa]
is_stable_list_irrel [lemma, in Kildall.kildall.kildall]
is_stable_irrel [lemma, in Kildall.kildall.kildall]
is_stable [definition, in Kildall.kildall.kildall]
is_stable_stable [lemma, in Kildall.kildall.kildall_dfa]
IS_data_flow_analyser [abbreviation, in Kildall.kildall.kildall_dfa]
iter [section, in Kildall.kildall.itera]
Itera [abbreviation, in Kildall.kildall.itera_eq]
itera [definition, in Kildall.kildall.itera]
Itera [abbreviation, in Kildall.kildall.kildall]
Itera [abbreviation, in Kildall.kildall.itera_property]
itera [library]
Iteraterme [abbreviation, in Kildall.kildall.itera]
iteraterme [lemma, in Kildall.kildall.iteraterme]
iteraterme [section, in Kildall.kildall.iteraterme]
iteraterme [library]
iteraterme.eq_Sigma_dec [variable, in Kildall.kildall.iteraterme]
iteraterme.n [variable, in Kildall.kildall.iteraterme]
iteraterme.r [variable, in Kildall.kildall.iteraterme]
iteraterme.r_is_semilattice [variable, in Kildall.kildall.iteraterme]
iteraterme.Sigma [variable, in Kildall.kildall.iteraterme]
iteraterme.step [variable, in Kildall.kildall.iteraterme]
iteraterme.step_succs_same_length [variable, in Kildall.kildall.iteraterme]
iteraterme.succs [variable, in Kildall.kildall.iteraterme]
iteraterme.sup [variable, in Kildall.kildall.iteraterme]
iteraterme.wfr [variable, in Kildall.kildall.iteraterme]
itera_eq [lemma, in Kildall.kildall.itera_eq]
itera_eq.wfr [variable, in Kildall.kildall.itera_eq]
itera_eq.r_is_semilattice [variable, in Kildall.kildall.itera_eq]
itera_eq.eq_Sigma_dec [variable, in Kildall.kildall.itera_eq]
itera_eq.step_succs_same_length [variable, in Kildall.kildall.itera_eq]
itera_eq.sup [variable, in Kildall.kildall.itera_eq]
itera_eq.r [variable, in Kildall.kildall.itera_eq]
itera_eq.step [variable, in Kildall.kildall.itera_eq]
itera_eq.succs [variable, in Kildall.kildall.itera_eq]
itera_eq.n [variable, in Kildall.kildall.itera_eq]
itera_eq.Sigma [variable, in Kildall.kildall.itera_eq]
itera_eq [section, in Kildall.kildall.itera_eq]
Itera_eq [abbreviation, in Kildall.kildall.itera_property]
itera_property.step_equiv [variable, in Kildall.kildall.itera_property]
itera_property.succs_equiv [variable, in Kildall.kildall.itera_property]
itera_property.wfr [variable, in Kildall.kildall.itera_property]
itera_property.r_is_semilattice [variable, in Kildall.kildall.itera_property]
itera_property.eq_Sigma_dec [variable, in Kildall.kildall.itera_property]
itera_property.step_succs_same_length [variable, in Kildall.kildall.itera_property]
itera_property.sup [variable, in Kildall.kildall.itera_property]
itera_property.T [variable, in Kildall.kildall.itera_property]
itera_property.r [variable, in Kildall.kildall.itera_property]
itera_property.wi [variable, in Kildall.kildall.itera_property]
itera_property.step [variable, in Kildall.kildall.itera_property]
itera_property.succs [variable, in Kildall.kildall.itera_property]
itera_property.n [variable, in Kildall.kildall.itera_property]
itera_property.Sigma [variable, in Kildall.kildall.itera_property]
itera_property [section, in Kildall.kildall.itera_property]
itera_shapes_Hvars [lemma, in Kildall.inst.fresh_variables]
itera_shapes_cons [lemma, in Kildall.inst.fresh_variables]
itera_shapes_nil [lemma, in Kildall.inst.fresh_variables]
itera_shapes [definition, in Kildall.inst.fresh_variables]
itera_eq [library]
itera_property [library]
iter_lub [lemma, in Kildall.kildall.itera_property]
iter_decrease [lemma, in Kildall.kildall.itera_property]
iter_preserves_stable [lemma, in Kildall.kildall.itera_property]
iter.eq_Sigma_dec [variable, in Kildall.kildall.itera]
iter.n [variable, in Kildall.kildall.itera]
iter.r [variable, in Kildall.kildall.itera]
iter.r_is_semilattice [variable, in Kildall.kildall.itera]
iter.Sigma [variable, in Kildall.kildall.itera]
iter.step [variable, in Kildall.kildall.itera]
iter.step_succs_same_length [variable, in Kildall.kildall.itera]
iter.succs [variable, in Kildall.kildall.itera]
iter.sup [variable, in Kildall.kildall.itera]
iter.wfr [variable, in Kildall.kildall.itera]
i_branch [constructor, in Kildall.inst.instructions]
i_build [constructor, in Kildall.inst.instructions]
i_call [constructor, in Kildall.inst.instructions]
i_load [constructor, in Kildall.inst.instructions]
i_stop [constructor, in Kildall.inst.instructions]
i_return [constructor, in Kildall.inst.instructions]

K

KIldall [abbreviation, in Kildall.kildall.kildall_bv]
Kildall [definition, in Kildall.kildall.kildall]
kildall [section, in Kildall.kildall.kildall]
KIldall [abbreviation, in Kildall.kildall.kildall_dfa]
kildall [library]
Kildall_Shapes_0 [lemma, in Kildall.inst.machine_shapes]
Kildall_Shapes [definition, in Kildall.inst.machine_shapes]
Kildall_is_bytecode_verifier [lemma, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.step_equiv [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.succs_equiv [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.wfr [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.r_is_semilattice [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.eq_Sigma_dec [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.step_succs_same_length [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.sup [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.T [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.r [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.wi [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.step [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.succs [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.n [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.Sigma [variable, in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier [section, in Kildall.kildall.kildall_bv]
Kildall_Is_Bytecode_Verifier [lemma, in Kildall.inst.inst_types]
Kildall_types [definition, in Kildall.inst.inst_types]
Kildall_Types_0 [lemma, in Kildall.inst.machine_types]
Kildall_Types [definition, in Kildall.inst.machine_types]
kildall_data_flow_analizer.step_equiv [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.succs_equiv [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.wfr [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.r_is_semilattice [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.eq_Sigma_dec [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.step_succs_same_length [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.sup [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.T [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.r [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.wi [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.step [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.succs [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.n [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.Sigma [variable, in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer [section, in Kildall.kildall.kildall_dfa]
Kildall_Shape_Is_Bytecode_Verifier [lemma, in Kildall.inst.inst_shapes]
Kildall_shapes [definition, in Kildall.inst.inst_shapes]
Kildall_Shapes [definition, in Kildall.inst.fresh_variables]
kildall_bv [library]
kildall_dfa [library]
kildall.eq_Sigma_dec [variable, in Kildall.kildall.kildall]
kildall.n [variable, in Kildall.kildall.kildall]
kildall.r [variable, in Kildall.kildall.kildall]
kildall.r_is_semilattice [variable, in Kildall.kildall.kildall]
kildall.Sigma [variable, in Kildall.kildall.kildall]
kildall.step [variable, in Kildall.kildall.kildall]
kildall.step_equiv [variable, in Kildall.kildall.kildall]
kildall.step_succs_same_length [variable, in Kildall.kildall.kildall]
kildall.succs [variable, in Kildall.kildall.kildall]
kildall.succs_equiv [variable, in Kildall.kildall.kildall]
kildall.sup [variable, in Kildall.kildall.kildall]
kildall.T [variable, in Kildall.kildall.kildall]
kildall.wfr [variable, in Kildall.kildall.kildall]
kildall.wi [variable, in Kildall.kildall.kildall]

L

last_return_or_stop [definition, in Kildall.inst.instructions]
Leaf [constructor, in Kildall.aux.tree]
lexicographic [inductive, in Kildall.lists.well_founded]
lexicographic_wf_step [lemma, in Kildall.lists.well_founded]
lexicographic_intro2 [constructor, in Kildall.lists.well_founded]
lexicographic_intro1 [constructor, in Kildall.lists.well_founded]
lexprod_eq [constructor, in Kildall.aux.relations]
lexprod_inf [constructor, in Kildall.aux.relations]
le_lt_Sn_m [definition, in Kildall.kildall.kildall]
le_cons [constructor, in Kildall.lists.vector]
le_nil [constructor, in Kildall.lists.vector]
lists [section, in Kildall.lists.lists]
lists [library]
lists.A [variable, in Kildall.lists.lists]
_ [ _ ] [notation, in Kildall.lists.lists]
list_concat_nil [lemma, in Kildall.lists.lists]
list_tail [lemma, in Kildall.lists.lists]
list_concat_cons [lemma, in Kildall.lists.lists]
list_typing_length [lemma, in Kildall.inst.typing]
list_from_pred_convertion [lemma, in Kildall.lists.pred_list]
list_to_pred_list_belong [lemma, in Kildall.lists.pred_list]
list_to_pred_list_length [lemma, in Kildall.lists.pred_list]
list_to_pred_list_to_list [lemma, in Kildall.lists.pred_list]
list_to_pred_list [definition, in Kildall.lists.pred_list]
list_to_pred_list_convert_hyp [lemma, in Kildall.lists.pred_list]
list_pointwise_to_m_list_pointwise [lemma, in Kildall.lists.m_list]
list_pointwise_cons [constructor, in Kildall.lists.m_list]
list_pointwise_nil [constructor, in Kildall.lists.m_list]
list_pointwise [inductive, in Kildall.lists.m_list]
lrs_functions [axiom, in Kildall.inst.machine]
lt_nb_length [definition, in Kildall.lists.nat_bounded_list]
lt_not_ge [lemma, in Kildall.aux.aux_arith]
lt_S_neq_lt [lemma, in Kildall.aux.aux_arith]
lt_pred_length [definition, in Kildall.lists.pred_list]
lt_m_length [definition, in Kildall.lists.m_list]
lub [definition, in Kildall.aux.relations]
lub_refl [lemma, in Kildall.aux.semilattices]
lub_r_sup2 [lemma, in Kildall.aux.semilattices]
lub_r_sup [lemma, in Kildall.aux.semilattices]
lub_circ [lemma, in Kildall.aux.semilattices]

M

machine [section, in Kildall.inst.machine]
machine [library]
machine_shapes.Pattern_branch [variable, in Kildall.inst.machine_shapes]
machine_shapes.Passed_Kildall [variable, in Kildall.inst.machine_shapes]
machine_shapes.Passed_Kildall_Types [variable, in Kildall.inst.machine_shapes]
machine_shapes.fwd_jmp [variable, in Kildall.inst.machine_shapes]
machine_shapes [section, in Kildall.inst.machine_shapes]
machine_types.Passed_Kildall [variable, in Kildall.inst.machine_types]
machine_types [section, in Kildall.inst.machine_types]
machine_types [library]
machine_shapes [library]
make_substitution_simpl_in_branch_then_elem [lemma, in Kildall.inst.substitutions]
make_substitution_invariant [lemma, in Kildall.inst.substitutions]
make_substitution_apply [lemma, in Kildall.inst.substitutions]
make_substitution_vars [lemma, in Kildall.inst.substitutions]
make_substitution_some [lemma, in Kildall.inst.substitutions]
make_substitution [definition, in Kildall.inst.substitutions]
map_rev_commut [lemma, in Kildall.lists.lists]
map_to_elements [lemma, in Kildall.lists.lists]
map_length [lemma, in Kildall.lists.lists]
map_unchanged_elements [lemma, in Kildall.lists.lists]
map_id [lemma, in Kildall.lists.lists]
map_apply_to_element [lemma, in Kildall.inst.substitutions]
map_apply_substitution_concat [lemma, in Kildall.inst.substitutions]
map_apply_substitution_cons [lemma, in Kildall.inst.substitutions]
Map2 [definition, in Kildall.lists.vector]
map2 [definition, in Kildall.lists.vector]
mkconstr [constructor, in Kildall.inst.instructions]
mkframe [constructor, in Kildall.inst.instructions]
mkfunction [constructor, in Kildall.inst.instructions]
mksubst [constructor, in Kildall.inst.substitutions]
MonotoneStep [abbreviation, in Kildall.kildall.kildall_bv]
monotonestep [definition, in Kildall.kildall.propa_property2]
MonotoneStep [abbreviation, in Kildall.kildall.kildall_dfa]
monotone_Step [lemma, in Kildall.inst.inst_types]
monotone_lub [lemma, in Kildall.aux.semilattices]
monotone_step_imp_kildall_dfa [lemma, in Kildall.kildall.kildall_dfa]
monotone_Step_S [lemma, in Kildall.inst.inst_shapes]
m_list_inc_refl [lemma, in Kildall.lists.m_list]
m_list_inc_trans [lemma, in Kildall.lists.m_list]
m_list_inc_equiv [lemma, in Kildall.lists.m_list]
m_cons_inc [constructor, in Kildall.lists.m_list]
m_equiv_inc [constructor, in Kildall.lists.m_list]
m_list_inc [inductive, in Kildall.lists.m_list]
m_list_convert_belong [lemma, in Kildall.lists.m_list]
m_list_belong_convert [lemma, in Kildall.lists.m_list]
m_list_equiv_combine [lemma, in Kildall.lists.m_list]
m_list_pointwise_cons [constructor, in Kildall.lists.m_list]
m_list_pointwise_nil [constructor, in Kildall.lists.m_list]
m_list_pointwise [inductive, in Kildall.lists.m_list]
m_list_get_second_element [lemma, in Kildall.lists.m_list]
m_list_get_first_element [lemma, in Kildall.lists.m_list]
m_list_belong_fst_dec [lemma, in Kildall.lists.m_list]
_ INsnd _ [notation, in Kildall.lists.m_list]
m_list_belong_snd [definition, in Kildall.lists.m_list]
_ INfst _ [notation, in Kildall.lists.m_list]
m_list_belong_fst [definition, in Kildall.lists.m_list]
_ INm _ [notation, in Kildall.lists.m_list]
m_list_equiv [definition, in Kildall.lists.m_list]
m_length [definition, in Kildall.lists.m_list]
m_list_remove [definition, in Kildall.lists.m_list]
m_list_get_witness [definition, in Kildall.lists.m_list]
m_list_belong_dec [definition, in Kildall.lists.m_list]
m_list_belong [definition, in Kildall.lists.m_list]
m_list_add_element [definition, in Kildall.lists.m_list]
m_cons [definition, in Kildall.lists.m_list]
m_nil [definition, in Kildall.lists.m_list]
m_list [definition, in Kildall.lists.m_list]
m_list.r [variable, in Kildall.lists.m_list]
m_list.eq_A_dec [variable, in Kildall.lists.m_list]
m_list.A [variable, in Kildall.lists.m_list]
m_list.n [variable, in Kildall.lists.m_list]
m_list [section, in Kildall.lists.m_list]
m_list_inc_2 [lemma, in Kildall.inst.fresh_variables]
m_list_inc_1 [lemma, in Kildall.inst.fresh_variables]
m_list [library]

N

n [abbreviation, in Kildall.inst.inst_types]
n [abbreviation, in Kildall.inst.inst_shapes]
name [axiom, in Kildall.inst.instructions]
Name [inductive, in Kildall.inst.substitutions]
nat_bounded_list.n [variable, in Kildall.lists.nat_bounded_list]
nat_bounded_list [section, in Kildall.lists.nat_bounded_list]
nat_bounded_list [library]
nb_list_convert_belong [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong_convert [definition, in Kildall.lists.nat_bounded_list]
nb_list_convert_length [definition, in Kildall.lists.nat_bounded_list]
nb_list_convert_equiv [definition, in Kildall.lists.nat_bounded_list]
nb_list_convert [definition, in Kildall.lists.nat_bounded_list]
nb_list_equiv [definition, in Kildall.lists.nat_bounded_list]
nb_length [definition, in Kildall.lists.nat_bounded_list]
nb_list_remove [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong_added [definition, in Kildall.lists.nat_bounded_list]
nb_list_add_already_there_added [definition, in Kildall.lists.nat_bounded_list]
nb_list_add_already_there [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong_rem [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong_add [definition, in Kildall.lists.nat_bounded_list]
nb_list_get_witness [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong_dec [definition, in Kildall.lists.nat_bounded_list]
nb_list_belong [definition, in Kildall.lists.nat_bounded_list]
nb_list_add_element [definition, in Kildall.lists.nat_bounded_list]
nb_cons [definition, in Kildall.lists.nat_bounded_list]
nb_nil [definition, in Kildall.lists.nat_bounded_list]
nb_list [definition, in Kildall.lists.nat_bounded_list]
neq_replace [lemma, in Kildall.lists.vector_results]
neq_n_Sn [lemma, in Kildall.aux.aux_arith]
Node [constructor, in Kildall.aux.tree]
nodep_prod_of_dep [definition, in Kildall.aux.product_results]
nondep_lexprod [inductive, in Kildall.aux.relations]
nonempty_progress' [lemma, in Kildall.inst.machine_types]
nonempty_progress [lemma, in Kildall.inst.machine_types]
nonvoidfcn [axiom, in Kildall.inst.machine]
Non_empty_Hd [lemma, in Kildall.lists.vector]
non_empty [lemma, in Kildall.lists.vector]
non_empty_dep [lemma, in Kildall.lists.vector]
not_lt_S [lemma, in Kildall.aux.aux_arith]
not_S_le [lemma, in Kildall.aux.aux_arith]
not_pred_lt_S_lt [lemma, in Kildall.aux.aux_arith]
not_var_in_tree_value [lemma, in Kildall.inst.substitutions]
no_change_at_p_not_in_succs [lemma, in Kildall.kildall.propa_property2]
no_change_at_p_not_in_w [lemma, in Kildall.kildall.propa_property]
no_loop_forest [lemma, in Kildall.aux.tree]
no_loop_tree [lemma, in Kildall.aux.tree]

O

order_subtree [lemma, in Kildall.aux.tree]
overwrite_replace [lemma, in Kildall.lists.vector_results]

P

P [definition, in Kildall.lists.nat_bounded_list]
pred_list_convert_belong [lemma, in Kildall.lists.pred_list]
pred_list_belong_convert [lemma, in Kildall.lists.pred_list]
pred_list_convert_length [lemma, in Kildall.lists.pred_list]
pred_list_convert_equiv [lemma, in Kildall.lists.pred_list]
pred_list_convert [definition, in Kildall.lists.pred_list]
pred_list_convertion.eq_A_dec [variable, in Kildall.lists.pred_list]
pred_list_convertion.Q [variable, in Kildall.lists.pred_list]
pred_list_convertion.P [variable, in Kildall.lists.pred_list]
pred_list_convertion.A [variable, in Kildall.lists.pred_list]
pred_list_convertion [section, in Kildall.lists.pred_list]
pred_list_equiv_belong [lemma, in Kildall.lists.pred_list]
pred_list_split_equiv [lemma, in Kildall.lists.pred_list]
pred_list_equiv_split [lemma, in Kildall.lists.pred_list]
pred_list_equiv_sym [lemma, in Kildall.lists.pred_list]
pred_list_equiv_trans [lemma, in Kildall.lists.pred_list]
pred_list_equiv_refl [lemma, in Kildall.lists.pred_list]
_ =p= _ [notation, in Kildall.lists.pred_list]
pred_list_equiv [definition, in Kildall.lists.pred_list]
pred_list_equivalence.A [variable, in Kildall.lists.pred_list]
pred_list_equivalence [section, in Kildall.lists.pred_list]
pred_list_add_already_there_added [lemma, in Kildall.lists.pred_list]
pred_list_belong_added [lemma, in Kildall.lists.pred_list]
pred_list_add_already_there [lemma, in Kildall.lists.pred_list]
pred_list_belong_rem [lemma, in Kildall.lists.pred_list]
pred_list_belong_add [lemma, in Kildall.lists.pred_list]
pred_list_get_witness [lemma, in Kildall.lists.pred_list]
pred_list_belong_dec [lemma, in Kildall.lists.pred_list]
pred_list_belong_remove [lemma, in Kildall.lists.pred_list]
pred_list_to_list_belong [lemma, in Kildall.lists.pred_list]
pred_list_to_list_length [lemma, in Kildall.lists.pred_list]
pred_list_to_list [definition, in Kildall.lists.pred_list]
pred_pointwise_cons [constructor, in Kildall.lists.pred_list]
pred_pointwise_nil [constructor, in Kildall.lists.pred_list]
pred_pointwise [inductive, in Kildall.lists.pred_list]
pred_length [definition, in Kildall.lists.pred_list]
_ \ _ [notation, in Kildall.lists.pred_list]
pred_list_remove [definition, in Kildall.lists.pred_list]
_ INp _ [notation, in Kildall.lists.pred_list]
pred_list_belong [definition, in Kildall.lists.pred_list]
pred_list_add_element [definition, in Kildall.lists.pred_list]
pred_cons [constructor, in Kildall.lists.pred_list]
pred_nil [constructor, in Kildall.lists.pred_list]
pred_list [inductive, in Kildall.lists.pred_list]
pred_list.eq_A_dec [variable, in Kildall.lists.pred_list]
pred_list.P [variable, in Kildall.lists.pred_list]
pred_list.A [variable, in Kildall.lists.pred_list]
pred_list [section, in Kildall.lists.pred_list]
pred_list [library]
product_results.r [variable, in Kildall.aux.product_results]
product_results.R [variable, in Kildall.aux.product_results]
product_results.rb [variable, in Kildall.aux.product_results]
product_results.ra [variable, in Kildall.aux.product_results]
product_results.Beta [variable, in Kildall.aux.product_results]
product_results.Alpha [variable, in Kildall.aux.product_results]
product_results [section, in Kildall.aux.product_results]
product_results [library]
prod_eq [lemma, in Kildall.kildall.propa_property2]
prod_eq [lemma, in Kildall.kildall.propa_property]
Propa [abbreviation, in Kildall.kildall.itera_eq]
Propa [abbreviation, in Kildall.kildall.propa_property2]
propa [section, in Kildall.kildall.propa]
Propa [abbreviation, in Kildall.kildall.propa_property]
Propa [abbreviation, in Kildall.kildall.itera_property]
Propa [abbreviation, in Kildall.kildall.iteraterme]
propa [library]
propagate [definition, in Kildall.kildall.propa]
propagate_shapes [definition, in Kildall.inst.fresh_variables]
propa_lub [lemma, in Kildall.kildall.propa_property2]
propa_decrease [lemma, in Kildall.kildall.propa_property2]
propa_property2.r_is_semilattice [variable, in Kildall.kildall.propa_property2]
propa_property2.eq_Sigma_dec [variable, in Kildall.kildall.propa_property2]
propa_property2.step_succs_same_length [variable, in Kildall.kildall.propa_property2]
propa_property2.sup [variable, in Kildall.kildall.propa_property2]
propa_property2.r [variable, in Kildall.kildall.propa_property2]
propa_property2.step [variable, in Kildall.kildall.propa_property2]
propa_property2.succs [variable, in Kildall.kildall.propa_property2]
propa_property2.n [variable, in Kildall.kildall.propa_property2]
propa_property2.Sigma [variable, in Kildall.kildall.propa_property2]
propa_property2 [section, in Kildall.kildall.propa_property2]
propa_case [lemma, in Kildall.kildall.propa]
propa_replace_commut [lemma, in Kildall.kildall.propa_property]
propa_nondep_lexprod [lemma, in Kildall.kildall.propa_property]
propa_property.r_is_semilattice [variable, in Kildall.kildall.propa_property]
propa_property.eq_Sigma_dec [variable, in Kildall.kildall.propa_property]
propa_property.step_succs_same_length [variable, in Kildall.kildall.propa_property]
propa_property.sup [variable, in Kildall.kildall.propa_property]
propa_property.r [variable, in Kildall.kildall.propa_property]
propa_property.step [variable, in Kildall.kildall.propa_property]
propa_property.succs [variable, in Kildall.kildall.propa_property]
propa_property.n [variable, in Kildall.kildall.propa_property]
propa_property.Sigma [variable, in Kildall.kildall.propa_property]
propa_property [section, in Kildall.kildall.propa_property]
Propa_nondep_lexprod [abbreviation, in Kildall.kildall.itera_property]
propa_shapes_hvars [lemma, in Kildall.inst.fresh_variables]
propa_property [library]
propa_property2 [library]
propa.eq_Sigma_dec [variable, in Kildall.kildall.propa]
propa.r [variable, in Kildall.kildall.propa]
propa.r_is_semilattice [variable, in Kildall.kildall.propa]
propa.Sigma [variable, in Kildall.kildall.propa]
propa.sup [variable, in Kildall.kildall.propa]
propa.wfr [variable, in Kildall.kildall.propa]
push_list_is_app_rev [lemma, in Kildall.lists.lists]
push_list [definition, in Kildall.lists.lists]

Q

Q [definition, in Kildall.lists.m_list]

R

r [definition, in Kildall.inst.inst_types]
ra [abbreviation, in Kildall.kildall.propa_property2]
ra [abbreviation, in Kildall.kildall.propa]
ra [abbreviation, in Kildall.kildall.propa_property]
ra [abbreviation, in Kildall.kildall.itera_property]
ra [abbreviation, in Kildall.kildall.iteraterme]
ra_replace [lemma, in Kildall.kildall.propa]
rb [definition, in Kildall.kildall.propa_property]
really_fresh_alt [lemma, in Kildall.inst.fresh_variables]
Really_fresh [lemma, in Kildall.inst.fresh_variables]
reduction [inductive, in Kildall.inst.machine]
reduction_keeps_wellshaped [lemma, in Kildall.inst.machine_shapes]
reduction_length [lemma, in Kildall.inst.machine_types]
reduction_progress [lemma, in Kildall.inst.machine_types]
reduction_keeps_welltyped [lemma, in Kildall.inst.machine_types]
reduction_keeps_wellformed [lemma, in Kildall.inst.machine]
reduction_to_execution [lemma, in Kildall.inst.machine]
reduction_determinism [lemma, in Kildall.inst.machine]
red_branch_else_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_branch_then_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_build_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_call_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_load_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_return_keeps_welltyped [lemma, in Kildall.inst.machine_types]
red_branch_else_keeps_wellformed [lemma, in Kildall.inst.machine]
red_branch_then_keeps_wellformed [lemma, in Kildall.inst.machine]
red_build_keeps_wellformed [lemma, in Kildall.inst.machine]
red_call_keeps_wellformed [lemma, in Kildall.inst.machine]
red_load_keeps_wellformed [lemma, in Kildall.inst.machine]
red_return_keeps_wellformed [lemma, in Kildall.inst.machine]
red_branch_else [constructor, in Kildall.inst.machine]
red_branch_then [constructor, in Kildall.inst.machine]
red_build [constructor, in Kildall.inst.machine]
red_call [constructor, in Kildall.inst.machine]
red_load [constructor, in Kildall.inst.machine]
red_stop [constructor, in Kildall.inst.machine]
red_return [constructor, in Kildall.inst.machine]
reflexive_vector_pointwise [lemma, in Kildall.lists.vector_results]
refl_dep_r [lemma, in Kildall.inst.inst_types]
refl_dep_r [lemma, in Kildall.inst.inst_shapes]
relations [section, in Kildall.aux.relations]
relations [library]
relations.Alpha [variable, in Kildall.aux.relations]
relations.r [variable, in Kildall.aux.relations]
relations.sup [variable, in Kildall.aux.relations]
remove_compat [lemma, in Kildall.lists.m_list]
reverse_apply [lemma, in Kildall.inst.substitutions]
rev_map [lemma, in Kildall.lists.lists]
rev_length [lemma, in Kildall.lists.lists]
rev_lin_is_rev [lemma, in Kildall.lists.lists]
rev_lin [definition, in Kildall.lists.lists]
rev_list_typing [lemma, in Kildall.inst.typing]
Rt [abbreviation, in Kildall.inst.inst_types]
R_to_r [lemma, in Kildall.aux.product_results]
r_is_semilattice [lemma, in Kildall.inst.inst_types]
r_is_order [lemma, in Kildall.inst.inst_types]
r_propa_ss_ts [lemma, in Kildall.kildall.propa_property2]
r_ss_propa_ss [lemma, in Kildall.kildall.propa_property]
r_S_is_semilattice [lemma, in Kildall.inst.inst_shapes]
r_S_is_order [lemma, in Kildall.inst.inst_shapes]
r_S [definition, in Kildall.inst.inst_shapes]

S

semilattice [definition, in Kildall.aux.semilattices]
semilattices [section, in Kildall.aux.semilattices]
semilattices [library]
semilattices.Alpha [variable, in Kildall.aux.semilattices]
semilattices.r [variable, in Kildall.aux.semilattices]
semilattices.sup [variable, in Kildall.aux.semilattices]
Shapes [constructor, in Kildall.inst.inst_shapes]
Sigma [inductive, in Kildall.inst.inst_types]
Sigma_S [inductive, in Kildall.inst.inst_shapes]
SI_vector_pointwise_or_eq_imp_vector_pointwise [lemma, in Kildall.lists.vector_results]
SI_vector_pointwise [definition, in Kildall.lists.vector]
sl_to_list_sl [lemma, in Kildall.lists.vector_results]
sl_lub_to_list_sl_lub [lemma, in Kildall.lists.vector_results]
sl_order_to_list_sl_order [lemma, in Kildall.lists.vector_results]
split_vector_pointwise [lemma, in Kildall.lists.vector_results]
split_k_elements_none [lemma, in Kildall.lists.lists]
split_k_elements_some [lemma, in Kildall.lists.lists]
split_k_elements_length [lemma, in Kildall.lists.lists]
split_k_elements_ok [lemma, in Kildall.lists.lists]
split_k_elements [definition, in Kildall.lists.lists]
split_vector [lemma, in Kildall.lists.vector]
Sss_init [definition, in Kildall.inst.machine_shapes]
Sss_init_Hvars [lemma, in Kildall.inst.fresh_variables]
Sss_init [definition, in Kildall.inst.fresh_variables]
ss_init [definition, in Kildall.inst.machine_shapes]
ss_init [definition, in Kildall.inst.machine_types]
ss_init [definition, in Kildall.inst.fresh_variables]
stable [definition, in Kildall.kildall.itera]
Stable [abbreviation, in Kildall.kildall.dfa]
stables [definition, in Kildall.kildall.itera]
Stables [abbreviation, in Kildall.kildall.dfa]
stable_imp_Wti [lemma, in Kildall.inst.inst_types]
stable_equality [lemma, in Kildall.kildall.propa_property2]
stable_p_by_propa [lemma, in Kildall.kildall.propa_property]
stable_imp_Wshi [lemma, in Kildall.inst.inst_shapes]
stack_shaping [definition, in Kildall.inst.substitutions]
stack_typing [definition, in Kildall.inst.typing]
Step [definition, in Kildall.inst.inst_types]
Step_Succs_same_length [lemma, in Kildall.inst.inst_types]
Step_Succs_aux_same_length [lemma, in Kildall.inst.inst_types]
Step_equiv [lemma, in Kildall.inst.inst_types]
Step_S_Succs_same_length [lemma, in Kildall.inst.inst_shapes]
Step_S_Succs_aux_same_length [lemma, in Kildall.inst.inst_shapes]
Step_S_equiv [lemma, in Kildall.inst.inst_shapes]
Step_S [definition, in Kildall.inst.inst_shapes]
Step_S' [definition, in Kildall.inst.fresh_variables]
Step' [abbreviation, in Kildall.kildall.itera_eq]
Step' [abbreviation, in Kildall.kildall.kildall_bv]
Step' [abbreviation, in Kildall.kildall.propa_property2]
Step' [abbreviation, in Kildall.kildall.itera]
step' [definition, in Kildall.kildall.propa_property]
Step' [abbreviation, in Kildall.kildall.kildall]
Step' [abbreviation, in Kildall.kildall.itera_property]
Step' [abbreviation, in Kildall.kildall.kildall_dfa]
Step' [abbreviation, in Kildall.kildall.iteraterme]
strict [definition, in Kildall.aux.relations]
strict_subtree_is_subtree_neq [lemma, in Kildall.aux.tree]
strict_subtree_size [lemma, in Kildall.aux.tree]
strict_subtree_cons [constructor, in Kildall.aux.tree]
strict_subtree [inductive, in Kildall.aux.tree]
strongest_r_R [lemma, in Kildall.aux.product_results]
Substitution [abbreviation, in Kildall.inst.machine_shapes]
Substitution [abbreviation, in Kildall.inst.inst_shapes]
Substitution [abbreviation, in Kildall.inst.substitutions]
Substitution [abbreviation, in Kildall.inst.fresh_variables]
substitutions [section, in Kildall.inst.substitutions]
substitutions [library]
subst_unchanged [lemma, in Kildall.inst.substitutions]
subst_length [lemma, in Kildall.inst.substitutions]
subst_expr [projection, in Kildall.inst.substitutions]
subst_elem [record, in Kildall.inst.substitutions]
subtree [inductive, in Kildall.aux.tree]
subtree_size [lemma, in Kildall.aux.tree]
subtree_cons [constructor, in Kildall.aux.tree]
subtree_refl [constructor, in Kildall.aux.tree]
sub_pattern [lemma, in Kildall.inst.substitutions]
sub_list_typing_left [lemma, in Kildall.inst.typing]
sub_list_typing_right [lemma, in Kildall.inst.typing]
Succs [definition, in Kildall.inst.instructions]
Succs_equiv [lemma, in Kildall.inst.instructions]
Succs_aux_equiv [lemma, in Kildall.inst.instructions]
Succs_better_bound [lemma, in Kildall.inst.instructions]
Succs_aux [definition, in Kildall.inst.instructions]
sup_iter [abbreviation, in Kildall.kildall.propa_property2]
sup_iter_m_r [lemma, in Kildall.kildall.propa_property]
sup_iter_stable [lemma, in Kildall.kildall.propa_property]
sup_iter_r_in [lemma, in Kildall.kildall.propa_property]
sup_iter_r_arg [lemma, in Kildall.kildall.propa_property]
sup_iter_r [lemma, in Kildall.kildall.propa_property]
sup_iter [definition, in Kildall.kildall.propa_property]
sup_S_is_lub [lemma, in Kildall.inst.inst_shapes]
sup_S [definition, in Kildall.inst.inst_shapes]
symbol [constructor, in Kildall.inst.substitutions]

T

tail [definition, in Kildall.lists.vector]
tail_neq [lemma, in Kildall.lists.lists]
tail_length [lemma, in Kildall.lists.m_list]
Theorem_iter [lemma, in Kildall.kildall.itera_property]
top_free_dominates_args_implies_top_free_kildall [lemma, in Kildall.kildall.kildall_bv]
top_free_to_wi [lemma, in Kildall.kildall.kildall_bv]
Top_T_top [lemma, in Kildall.inst.inst_types]
Top_T [constructor, in Kildall.inst.inst_types]
Top_S_top [lemma, in Kildall.inst.inst_shapes]
Top_S [constructor, in Kildall.inst.inst_shapes]
transition [lemma, in Kildall.kildall.itera_property]
transitive_SI_vector_pointwise [lemma, in Kildall.lists.vector_results]
transitive_vector_pointwise [lemma, in Kildall.lists.vector_results]
tree [inductive, in Kildall.aux.tree]
tree [section, in Kildall.aux.tree]
tree [library]
tree_rec [lemma, in Kildall.aux.tree]
tree_ind [lemma, in Kildall.aux.tree]
tree_rec_aux [lemma, in Kildall.aux.tree]
tree_ind_aux [lemma, in Kildall.aux.tree]
tree_size [definition, in Kildall.aux.tree]
tree_name_to_tree_Name [definition, in Kildall.inst.substitutions]
tree_is_pattern [definition, in Kildall.inst.substitutions]
tree_is_pattern_bool [definition, in Kildall.inst.substitutions]
tree_typing_args_length [lemma, in Kildall.inst.typing]
tree_to_args_typing [lemma, in Kildall.inst.typing]
tree_typing [definition, in Kildall.inst.typing]
tree_list_typing_cons [constructor, in Kildall.inst.typing]
tree_list_typing_nil [constructor, in Kildall.inst.typing]
tree_list_typing [inductive, in Kildall.inst.typing]
tree.eq_L_dec [variable, in Kildall.aux.tree]
tree.eq_N_dec [variable, in Kildall.aux.tree]
tree.L [variable, in Kildall.aux.tree]
tree.N [variable, in Kildall.aux.tree]
Types [constructor, in Kildall.inst.inst_types]
typing [section, in Kildall.inst.typing]
typing [library]
T_free [lemma, in Kildall.kildall.dfa]

U

up_wl [lemma, in Kildall.kildall.kildall]

V

value [definition, in Kildall.inst.instructions]
value [abbreviation, in Kildall.inst.substitutions]
var_in_apply_elem_tree_aux2 [lemma, in Kildall.inst.substitutions]
var_in_apply_elem_tree_aux [lemma, in Kildall.inst.substitutions]
var_not_in_subst_unchanged [lemma, in Kildall.inst.substitutions]
var_not_in_subst_elem_unchanged [lemma, in Kildall.inst.substitutions]
var_not_in_subst_not_in_apply [lemma, in Kildall.inst.substitutions]
var_not_in_subst_not_in_apply_elem [lemma, in Kildall.inst.substitutions]
var_not_in_subst_elem [lemma, in Kildall.inst.substitutions]
var_in_subst_elem [definition, in Kildall.inst.substitutions]
var_not_in_tree [definition, in Kildall.inst.substitutions]
var_in_tree_bool [definition, in Kildall.inst.substitutions]
vector [inductive, in Kildall.lists.vector]
Vector [section, in Kildall.lists.vector]
vector [library]
vector_pointwise_imp_SI_vector_pointwise_or_eq [lemma, in Kildall.lists.vector_results]
vector_pointwise_to_element [lemma, in Kildall.lists.vector_results]
vector_pointwise_replace [lemma, in Kildall.lists.vector_results]
Vector_results.sup [variable, in Kildall.lists.vector_results]
Vector_results.r [variable, in Kildall.lists.vector_results]
Vector_results.A [variable, in Kildall.lists.vector_results]
Vector_results [section, in Kildall.lists.vector_results]
vector_pointwise_to_lexicographic_inv [lemma, in Kildall.lists.well_founded]
vector_map [definition, in Kildall.lists.vector]
vector_replace [definition, in Kildall.lists.vector]
Vector_pointwise [definition, in Kildall.lists.vector]
vector_pointwise [inductive, in Kildall.lists.vector]
vector_cons [constructor, in Kildall.lists.vector]
vector_nil [constructor, in Kildall.lists.vector]
vector_results [library]
Vector.A [variable, in Kildall.lists.vector]

W

wellformed_execution [lemma, in Kildall.inst.machine]
wellformed_init_configuration [lemma, in Kildall.inst.machine]
wellformed_epsilon [lemma, in Kildall.inst.machine]
wellformed_configuration [definition, in Kildall.inst.machine]
wellshaped_execution [lemma, in Kildall.inst.machine_shapes]
wellshaped_init_configuration [lemma, in Kildall.inst.machine_shapes]
wellshaped_conf [constructor, in Kildall.inst.machine_shapes]
wellshaped_configuration [inductive, in Kildall.inst.machine_shapes]
wellshaped_plus_frame [definition, in Kildall.inst.machine_shapes]
welltyped_execution [lemma, in Kildall.inst.machine_types]
welltyped_init_configuration [lemma, in Kildall.inst.machine_types]
welltyped_conf [constructor, in Kildall.inst.machine_types]
welltyped_configuration [inductive, in Kildall.inst.machine_types]
welltyped_frame [definition, in Kildall.inst.machine_types]
welltyping [definition, in Kildall.kildall.dfa]
well_founded [library]
wfr [lemma, in Kildall.inst.inst_types]
wfr_S [lemma, in Kildall.inst.inst_shapes]
wf_nondep_lexprod [lemma, in Kildall.aux.product_results]
wf_R_to_r [lemma, in Kildall.aux.product_results]
wf_dep_nodep_lexprod [lemma, in Kildall.aux.product_results]
wf_lexicographic [lemma, in Kildall.lists.well_founded]
wf_lexicographic_step [lemma, in Kildall.lists.well_founded]
wf_lexicographic0 [lemma, in Kildall.lists.well_founded]
wf_list.R_wf [variable, in Kildall.lists.well_founded]
wf_list.ra [variable, in Kildall.lists.well_founded]
wf_list.A [variable, in Kildall.lists.well_founded]
wf_list [section, in Kildall.lists.well_founded]
wf_lt_dep_length [lemma, in Kildall.kildall.iteraterme]
Wi_and_stable_agree [abbreviation, in Kildall.kildall.kildall_bv]
wi_and_stable_agree [definition, in Kildall.kildall.dfa]
work_list_irrel_inc [lemma, in Kildall.kildall.kildall]
work_list [definition, in Kildall.kildall.kildall]
work_list_not_stable [lemma, in Kildall.kildall.kildall_dfa]
Wshi [definition, in Kildall.inst.inst_shapes]
Wshi_Kildall [lemma, in Kildall.inst.machine_shapes]
Wshi_and_stable_agree [lemma, in Kildall.inst.inst_shapes]
Wshi_imp_stable [lemma, in Kildall.inst.inst_shapes]
Wti [definition, in Kildall.inst.inst_types]
Wti_and_stable_agree [lemma, in Kildall.inst.inst_types]
Wti_imp_stable [lemma, in Kildall.inst.inst_types]
Wti_Kildall [lemma, in Kildall.inst.machine_types]

X

x [constructor, in Kildall.inst.substitutions]
xi [projection, in Kildall.inst.substitutions]
xj [projection, in Kildall.inst.substitutions]

other

_ [ _ | _ -> _ ] [notation, in Kildall.lists.vector_results]
_ =nb= _ [notation, in Kildall.lists.nat_bounded_list]
_ INnb _ [notation, in Kildall.lists.nat_bounded_list]
_ [ _ ] [notation, in Kildall.lists.lists]
_ =p= _ [notation, in Kildall.lists.pred_list]
_ \ _ [notation, in Kildall.lists.pred_list]
_ INp _ [notation, in Kildall.lists.pred_list]
_ INC _ [notation, in Kildall.lists.m_list]
_ =m= _ [notation, in Kildall.lists.m_list]
_ INsnd _ [notation, in Kildall.lists.m_list]
_ INfst _ [notation, in Kildall.lists.m_list]
_ INm _ [notation, in Kildall.lists.m_list]
_ [ _ |_] [notation, in Kildall.lists.vector]
_ [ _ | _ ] [notation, in Kildall.lists.vector]
_ INv _ [notation, in Kildall.lists.vector]
_ [ _ <- _ ] [notation, in Kildall.lists.vector]

Notation Index

L

_ [ _ ] [in Kildall.lists.lists]

M

_ INsnd _ [in Kildall.lists.m_list]
_ INfst _ [in Kildall.lists.m_list]
_ INm _ [in Kildall.lists.m_list]

P

_ =p= _ [in Kildall.lists.pred_list]
_ \ _ [in Kildall.lists.pred_list]
_ INp _ [in Kildall.lists.pred_list]

other

_ [ _ | _ -> _ ] [in Kildall.lists.vector_results]
_ =nb= _ [in Kildall.lists.nat_bounded_list]
_ INnb _ [in Kildall.lists.nat_bounded_list]
_ [ _ ] [in Kildall.lists.lists]
_ =p= _ [in Kildall.lists.pred_list]
_ \ _ [in Kildall.lists.pred_list]
_ INp _ [in Kildall.lists.pred_list]
_ INC _ [in Kildall.lists.m_list]
_ =m= _ [in Kildall.lists.m_list]
_ INsnd _ [in Kildall.lists.m_list]
_ INfst _ [in Kildall.lists.m_list]
_ INm _ [in Kildall.lists.m_list]
_ [ _ |_] [in Kildall.lists.vector]
_ [ _ | _ ] [in Kildall.lists.vector]
_ INv _ [in Kildall.lists.vector]
_ [ _ <- _ ] [in Kildall.lists.vector]

Variable Index

A

asc_list.eq_A_dec [in Kildall.lists.well_founded]
asc_list.ra [in Kildall.lists.well_founded]
asc_list.A [in Kildall.lists.well_founded]

D

Data_flow_analysis.r_is_order [in Kildall.kildall.dfa]
Data_flow_analysis.step_succs_same_length [in Kildall.kildall.dfa]
Data_flow_analysis.T [in Kildall.kildall.dfa]
Data_flow_analysis.r [in Kildall.kildall.dfa]
Data_flow_analysis.wi [in Kildall.kildall.dfa]
Data_flow_analysis.step [in Kildall.kildall.dfa]
Data_flow_analysis.succs [in Kildall.kildall.dfa]
Data_flow_analysis.n [in Kildall.kildall.dfa]
Data_flow_analysis.Sigma [in Kildall.kildall.dfa]

F

fold_bool.f [in Kildall.lists.lists]
fold_bool.A [in Kildall.lists.lists]
fresh_variables.Passed_Kildall [in Kildall.inst.fresh_variables]
fresh_variables.Passed_Kildall_Types [in Kildall.inst.fresh_variables]
fresh_variables.fwd_jmp [in Kildall.inst.fresh_variables]

I

inst_types.fcn [in Kildall.inst.inst_types]
inst_shapes.fcn [in Kildall.inst.inst_shapes]
iteraterme.eq_Sigma_dec [in Kildall.kildall.iteraterme]
iteraterme.n [in Kildall.kildall.iteraterme]
iteraterme.r [in Kildall.kildall.iteraterme]
iteraterme.r_is_semilattice [in Kildall.kildall.iteraterme]
iteraterme.Sigma [in Kildall.kildall.iteraterme]
iteraterme.step [in Kildall.kildall.iteraterme]
iteraterme.step_succs_same_length [in Kildall.kildall.iteraterme]
iteraterme.succs [in Kildall.kildall.iteraterme]
iteraterme.sup [in Kildall.kildall.iteraterme]
iteraterme.wfr [in Kildall.kildall.iteraterme]
itera_eq.wfr [in Kildall.kildall.itera_eq]
itera_eq.r_is_semilattice [in Kildall.kildall.itera_eq]
itera_eq.eq_Sigma_dec [in Kildall.kildall.itera_eq]
itera_eq.step_succs_same_length [in Kildall.kildall.itera_eq]
itera_eq.sup [in Kildall.kildall.itera_eq]
itera_eq.r [in Kildall.kildall.itera_eq]
itera_eq.step [in Kildall.kildall.itera_eq]
itera_eq.succs [in Kildall.kildall.itera_eq]
itera_eq.n [in Kildall.kildall.itera_eq]
itera_eq.Sigma [in Kildall.kildall.itera_eq]
itera_property.step_equiv [in Kildall.kildall.itera_property]
itera_property.succs_equiv [in Kildall.kildall.itera_property]
itera_property.wfr [in Kildall.kildall.itera_property]
itera_property.r_is_semilattice [in Kildall.kildall.itera_property]
itera_property.eq_Sigma_dec [in Kildall.kildall.itera_property]
itera_property.step_succs_same_length [in Kildall.kildall.itera_property]
itera_property.sup [in Kildall.kildall.itera_property]
itera_property.T [in Kildall.kildall.itera_property]
itera_property.r [in Kildall.kildall.itera_property]
itera_property.wi [in Kildall.kildall.itera_property]
itera_property.step [in Kildall.kildall.itera_property]
itera_property.succs [in Kildall.kildall.itera_property]
itera_property.n [in Kildall.kildall.itera_property]
itera_property.Sigma [in Kildall.kildall.itera_property]
iter.eq_Sigma_dec [in Kildall.kildall.itera]
iter.n [in Kildall.kildall.itera]
iter.r [in Kildall.kildall.itera]
iter.r_is_semilattice [in Kildall.kildall.itera]
iter.Sigma [in Kildall.kildall.itera]
iter.step [in Kildall.kildall.itera]
iter.step_succs_same_length [in Kildall.kildall.itera]
iter.succs [in Kildall.kildall.itera]
iter.sup [in Kildall.kildall.itera]
iter.wfr [in Kildall.kildall.itera]

K

kildall_bytecode_verifier.step_equiv [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.succs_equiv [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.wfr [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.r_is_semilattice [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.eq_Sigma_dec [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.step_succs_same_length [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.sup [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.T [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.r [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.wi [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.step [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.succs [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.n [in Kildall.kildall.kildall_bv]
kildall_bytecode_verifier.Sigma [in Kildall.kildall.kildall_bv]
kildall_data_flow_analizer.step_equiv [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.succs_equiv [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.wfr [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.r_is_semilattice [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.eq_Sigma_dec [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.step_succs_same_length [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.sup [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.T [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.r [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.wi [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.step [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.succs [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.n [in Kildall.kildall.kildall_dfa]
kildall_data_flow_analizer.Sigma [in Kildall.kildall.kildall_dfa]
kildall.eq_Sigma_dec [in Kildall.kildall.kildall]
kildall.n [in Kildall.kildall.kildall]
kildall.r [in Kildall.kildall.kildall]
kildall.r_is_semilattice [in Kildall.kildall.kildall]
kildall.Sigma [in Kildall.kildall.kildall]
kildall.step [in Kildall.kildall.kildall]
kildall.step_equiv [in Kildall.kildall.kildall]
kildall.step_succs_same_length [in Kildall.kildall.kildall]
kildall.succs [in Kildall.kildall.kildall]
kildall.succs_equiv [in Kildall.kildall.kildall]
kildall.sup [in Kildall.kildall.kildall]
kildall.T [in Kildall.kildall.kildall]
kildall.wfr [in Kildall.kildall.kildall]
kildall.wi [in Kildall.kildall.kildall]

L

lists.A [in Kildall.lists.lists]

M

machine_shapes.Pattern_branch [in Kildall.inst.machine_shapes]
machine_shapes.Passed_Kildall [in Kildall.inst.machine_shapes]
machine_shapes.Passed_Kildall_Types [in Kildall.inst.machine_shapes]
machine_shapes.fwd_jmp [in Kildall.inst.machine_shapes]
machine_types.Passed_Kildall [in Kildall.inst.machine_types]
m_list.r [in Kildall.lists.m_list]
m_list.eq_A_dec [in Kildall.lists.m_list]
m_list.A [in Kildall.lists.m_list]
m_list.n [in Kildall.lists.m_list]

N

nat_bounded_list.n [in Kildall.lists.nat_bounded_list]

P

pred_list_convertion.eq_A_dec [in Kildall.lists.pred_list]
pred_list_convertion.Q [in Kildall.lists.pred_list]
pred_list_convertion.P [in Kildall.lists.pred_list]
pred_list_convertion.A [in Kildall.lists.pred_list]
pred_list_equivalence.A [in Kildall.lists.pred_list]
pred_list.eq_A_dec [in Kildall.lists.pred_list]
pred_list.P [in Kildall.lists.pred_list]
pred_list.A [in Kildall.lists.pred_list]
product_results.r [in Kildall.aux.product_results]
product_results.R [in Kildall.aux.product_results]
product_results.rb [in Kildall.aux.product_results]
product_results.ra [in Kildall.aux.product_results]
product_results.Beta [in Kildall.aux.product_results]
product_results.Alpha [in Kildall.aux.product_results]
propa_property2.r_is_semilattice [in Kildall.kildall.propa_property2]
propa_property2.eq_Sigma_dec [in Kildall.kildall.propa_property2]
propa_property2.step_succs_same_length [in Kildall.kildall.propa_property2]
propa_property2.sup [in Kildall.kildall.propa_property2]
propa_property2.r [in Kildall.kildall.propa_property2]
propa_property2.step [in Kildall.kildall.propa_property2]
propa_property2.succs [in Kildall.kildall.propa_property2]
propa_property2.n [in Kildall.kildall.propa_property2]
propa_property2.Sigma [in Kildall.kildall.propa_property2]
propa_property.r_is_semilattice [in Kildall.kildall.propa_property]
propa_property.eq_Sigma_dec [in Kildall.kildall.propa_property]
propa_property.step_succs_same_length [in Kildall.kildall.propa_property]
propa_property.sup [in Kildall.kildall.propa_property]
propa_property.r [in Kildall.kildall.propa_property]
propa_property.step [in Kildall.kildall.propa_property]
propa_property.succs [in Kildall.kildall.propa_property]
propa_property.n [in Kildall.kildall.propa_property]
propa_property.Sigma [in Kildall.kildall.propa_property]
propa.eq_Sigma_dec [in Kildall.kildall.propa]
propa.r [in Kildall.kildall.propa]
propa.r_is_semilattice [in Kildall.kildall.propa]
propa.Sigma [in Kildall.kildall.propa]
propa.sup [in Kildall.kildall.propa]
propa.wfr [in Kildall.kildall.propa]

R

relations.Alpha [in Kildall.aux.relations]
relations.r [in Kildall.aux.relations]
relations.sup [in Kildall.aux.relations]

S

semilattices.Alpha [in Kildall.aux.semilattices]
semilattices.r [in Kildall.aux.semilattices]
semilattices.sup [in Kildall.aux.semilattices]

T

tree.eq_L_dec [in Kildall.aux.tree]
tree.eq_N_dec [in Kildall.aux.tree]
tree.L [in Kildall.aux.tree]
tree.N [in Kildall.aux.tree]

V

Vector_results.sup [in Kildall.lists.vector_results]
Vector_results.r [in Kildall.lists.vector_results]
Vector_results.A [in Kildall.lists.vector_results]
Vector.A [in Kildall.lists.vector]

W

wf_list.R_wf [in Kildall.lists.well_founded]
wf_list.ra [in Kildall.lists.well_founded]
wf_list.A [in Kildall.lists.well_founded]

Library Index

A

D

dfa

F

fresh_variables

I

instructions
inst_shapes
inst_types
itera
iteraterme
itera_eq
itera_property

K

kildall
kildall_bv
kildall_dfa

L

lists

M

machine
machine_types
machine_shapes
m_list

N

nat_bounded_list

P

pred_list
product_results
propa
propa_property
propa_property2

R

S

semilattices
substitutions

T

V

vector
vector_results

W

Lemma Index

A

AccSl [in Kildall.inst.inst_types]
AccSSE [in Kildall.inst.inst_shapes]
AccTop_T [in Kildall.inst.inst_types]
AccTop_S [in Kildall.inst.inst_shapes]
acc_ssw [in Kildall.kildall.iteraterme]
alt_monostep_aux2 [in Kildall.lists.m_list]
alt_monostep_aux1 [in Kildall.lists.m_list]
antisymmetric_vector_pointwise [in Kildall.lists.vector_results]
apply_elem_pattern [in Kildall.inst.substitutions]
apply_elem_commut [in Kildall.inst.substitutions]
apply_applied [in Kildall.inst.substitutions]
apply_elem_in_subst [in Kildall.inst.substitutions]
apply_elem_var_not_in_unchanged [in Kildall.inst.substitutions]
apply_substitution_concat [in Kildall.inst.substitutions]
apply_substitution_cons [in Kildall.inst.substitutions]
apply_cons [in Kildall.inst.substitutions]
apply_to_forest [in Kildall.inst.substitutions]
apply_elem_to_forest [in Kildall.inst.substitutions]
apply_unchanged [in Kildall.inst.substitutions]
apply_elem_forest_unchanged [in Kildall.inst.substitutions]
apply_elem_unchanged [in Kildall.inst.substitutions]
app_list_typing [in Kildall.inst.typing]
args_to_tree_typing [in Kildall.inst.typing]
asc_vector_pointwise [in Kildall.lists.well_founded]
aug_wl [in Kildall.kildall.kildall]
aux [in Kildall.kildall.kildall]
aux_init_vars_length [in Kildall.inst.substitutions]
aux2 [in Kildall.kildall.kildall]

B

belong_list_to_pred_list [in Kildall.lists.pred_list]
belong_pred_list_to_list [in Kildall.lists.pred_list]
belong_and_snd [in Kildall.lists.m_list]
belong_and_fst [in Kildall.lists.m_list]
Bot_T_bot [in Kildall.inst.inst_types]
Bot_S_bot [in Kildall.inst.inst_shapes]

C

combaux1 [in Kildall.lists.m_list]
combaux2 [in Kildall.lists.m_list]
commutative_replace [in Kildall.lists.vector_results]
compose_map [in Kildall.lists.lists]
concat_map [in Kildall.lists.lists]
concat_In [in Kildall.lists.lists]
concat_length [in Kildall.lists.lists]
cons_eq [in Kildall.lists.lists]
cons_list_typing [in Kildall.inst.typing]
contrap [in Kildall.kildall.kildall_dfa]

D

dec_belong [in Kildall.lists.vector_results]
dep_r_Top_T_2 [in Kildall.inst.inst_types]
dep_r_Bot_T_2 [in Kildall.inst.inst_types]
dep_r_Top_T_1 [in Kildall.inst.inst_types]
dep_r_Bot_T_1 [in Kildall.inst.inst_types]
dep_r_Top_2 [in Kildall.inst.inst_shapes]
dep_r_Bot_2 [in Kildall.inst.inst_shapes]
dep_r_Top_1 [in Kildall.inst.inst_shapes]
dep_r_Bot_1 [in Kildall.inst.inst_shapes]
dfa_is_bv [in Kildall.kildall.dfa]
does_not_belong_is_not_element [in Kildall.lists.vector_results]

E

element_at_unsafe_some [in Kildall.lists.vector_results]
element_at_unsafe_none [in Kildall.lists.vector_results]
element_at_to_unsafe [in Kildall.lists.vector_results]
element_at_unsafe_to_safe [in Kildall.lists.vector_results]
element_at_constant_list [in Kildall.lists.vector_results]
element_at_0_is_head [in Kildall.lists.vector_results]
element_at_belong [in Kildall.lists.vector_results]
element_at_irrel [in Kildall.lists.vector_results]
element_at_in_replaced' [in Kildall.lists.vector_results]
element_at_in_replaced [in Kildall.lists.vector_results]
element_at_list_map' [in Kildall.lists.lists]
element_at_list_map [in Kildall.lists.lists]
element_at_list_rev [in Kildall.lists.lists]
element_at_list_concat' [in Kildall.lists.lists]
element_at_list_concat [in Kildall.lists.lists]
element_at_list_in [in Kildall.lists.lists]
element_at_list_none [in Kildall.lists.lists]
element_at_list_some [in Kildall.lists.lists]
element_at_init_subst [in Kildall.inst.substitutions]
element_at_init_vars [in Kildall.inst.substitutions]
element_at_list_typing [in Kildall.inst.typing]
empty [in Kildall.lists.vector]
empty_dep [in Kildall.lists.vector]
eq_dec_to_list_eq_dec [in Kildall.lists.vector_results]
eq_Sigma_dec [in Kildall.inst.inst_types]
eq_list_name_dec [in Kildall.inst.inst_types]
eq_tree_dec [in Kildall.aux.tree]
eq_configuration_nil_dec [in Kildall.inst.machine_types]
eq_Sigma_S_dec [in Kildall.inst.inst_shapes]
eq_Substitution_dec [in Kildall.inst.substitutions]
eq_list_Expression_dec [in Kildall.inst.substitutions]
eq_Expression_dec [in Kildall.inst.substitutions]
eq_Name_dec [in Kildall.inst.substitutions]
eq_prod_dec [in Kildall.lists.m_list]
execution_length [in Kildall.inst.machine_types]

F

fold_inc [in Kildall.aux.tree]
fold_dom [in Kildall.aux.tree]
fold_bool_or_true [in Kildall.lists.lists]
fold_bool_or_false [in Kildall.lists.lists]
fold_bool_or_first_true [in Kildall.lists.lists]
fold_bool_and_true [in Kildall.lists.lists]
fold_bool_and_false [in Kildall.lists.lists]
fold_bool_and_first_false [in Kildall.lists.lists]
forall_element_to_vector_pointwise [in Kildall.lists.vector_results]
f_is_lub [in Kildall.inst.inst_types]

G

get_some_in_functions [in Kildall.inst.instructions]

H

Hvars_Kildall_Shapes [in Kildall.inst.fresh_variables]
Hvars_Shapes [in Kildall.inst.fresh_variables]
Hvars_Sp_Bot [in Kildall.inst.fresh_variables]
Hvars_Sp_Top [in Kildall.inst.fresh_variables]
Hvars_Bot_S [in Kildall.inst.fresh_variables]
Hvars_Top_S [in Kildall.inst.fresh_variables]
Hvars_replace_Bot [in Kildall.inst.fresh_variables]
Hvars_replace_Top [in Kildall.inst.fresh_variables]
hyp_belong_convert [in Kildall.lists.pred_list]

I

idempotent_replace [in Kildall.lists.vector_results]
idempotent_lub [in Kildall.aux.semilattices]
immediate_subtree_size [in Kildall.aux.tree]
inc_w_propa_w [in Kildall.kildall.propa]
inc_propa_w_propa_replace_ss_w [in Kildall.kildall.propa_property]
init_stack_shaping [in Kildall.inst.substitutions]
init_subst_apply [in Kildall.inst.substitutions]
init_subst_member [in Kildall.inst.substitutions]
init_vars_length [in Kildall.inst.substitutions]
In_mapped [in Kildall.lists.lists]
In_rev [in Kildall.lists.lists]
In_concat [in Kildall.lists.lists]
In_fresh [in Kildall.inst.substitutions]
In_fresh_not_var_in [in Kildall.inst.substitutions]
in_snd_in_snd_combine [in Kildall.lists.m_list]
in_snd_combine_in_snd [in Kildall.lists.m_list]
in_fst_in_fst_combine [in Kildall.lists.m_list]
in_fst_combine_in_fst [in Kildall.lists.m_list]
is_not_element_does_not_belong [in Kildall.lists.vector_results]
is_stable_list_irrel [in Kildall.kildall.kildall]
is_stable_irrel [in Kildall.kildall.kildall]
is_stable_stable [in Kildall.kildall.kildall_dfa]
iteraterme [in Kildall.kildall.iteraterme]
itera_eq [in Kildall.kildall.itera_eq]
itera_shapes_Hvars [in Kildall.inst.fresh_variables]
itera_shapes_cons [in Kildall.inst.fresh_variables]
itera_shapes_nil [in Kildall.inst.fresh_variables]
iter_lub [in Kildall.kildall.itera_property]
iter_decrease [in Kildall.kildall.itera_property]
iter_preserves_stable [in Kildall.kildall.itera_property]

K

Kildall_Shapes_0 [in Kildall.inst.machine_shapes]
Kildall_is_bytecode_verifier [in Kildall.kildall.kildall_bv]
Kildall_Is_Bytecode_Verifier [in Kildall.inst.inst_types]
Kildall_Types_0 [in Kildall.inst.machine_types]
Kildall_Shape_Is_Bytecode_Verifier [in Kildall.inst.inst_shapes]

L

lexicographic_wf_step [in Kildall.lists.well_founded]
list_concat_nil [in Kildall.lists.lists]
list_tail [in Kildall.lists.lists]
list_concat_cons [in Kildall.lists.lists]
list_typing_length [in Kildall.inst.typing]
list_from_pred_convertion [in Kildall.lists.pred_list]
list_to_pred_list_belong [in Kildall.lists.pred_list]
list_to_pred_list_length [in Kildall.lists.pred_list]
list_to_pred_list_to_list [in Kildall.lists.pred_list]
list_to_pred_list_convert_hyp [in Kildall.lists.pred_list]
list_pointwise_to_m_list_pointwise [in Kildall.lists.m_list]
lt_not_ge [in Kildall.aux.aux_arith]
lt_S_neq_lt [in Kildall.aux.aux_arith]
lub_refl [in Kildall.aux.semilattices]
lub_r_sup2 [in Kildall.aux.semilattices]
lub_r_sup [in Kildall.aux.semilattices]
lub_circ [in Kildall.aux.semilattices]

M

make_substitution_simpl_in_branch_then_elem [in Kildall.inst.substitutions]
make_substitution_invariant [in Kildall.inst.substitutions]
make_substitution_apply [in Kildall.inst.substitutions]
make_substitution_vars [in Kildall.inst.substitutions]
make_substitution_some [in Kildall.inst.substitutions]
map_rev_commut [in Kildall.lists.lists]
map_to_elements [in Kildall.lists.lists]
map_length [in Kildall.lists.lists]
map_unchanged_elements [in Kildall.lists.lists]
map_id [in Kildall.lists.lists]
map_apply_to_element [in Kildall.inst.substitutions]
map_apply_substitution_concat [in Kildall.inst.substitutions]
map_apply_substitution_cons [in Kildall.inst.substitutions]
monotone_Step [in Kildall.inst.inst_types]
monotone_lub [in Kildall.aux.semilattices]
monotone_step_imp_kildall_dfa [in Kildall.kildall.kildall_dfa]
monotone_Step_S [in Kildall.inst.inst_shapes]
m_list_inc_refl [in Kildall.lists.m_list]
m_list_inc_trans [in Kildall.lists.m_list]
m_list_inc_equiv [in Kildall.lists.m_list]
m_list_convert_belong [in Kildall.lists.m_list]
m_list_belong_convert [in Kildall.lists.m_list]
m_list_equiv_combine [in Kildall.lists.m_list]
m_list_get_second_element [in Kildall.lists.m_list]
m_list_get_first_element [in Kildall.lists.m_list]
m_list_belong_fst_dec [in Kildall.lists.m_list]
m_list_inc_2 [in Kildall.inst.fresh_variables]
m_list_inc_1 [in Kildall.inst.fresh_variables]

N

neq_replace [in Kildall.lists.vector_results]
neq_n_Sn [in Kildall.aux.aux_arith]
nonempty_progress' [in Kildall.inst.machine_types]
nonempty_progress [in Kildall.inst.machine_types]
Non_empty_Hd [in Kildall.lists.vector]
non_empty [in Kildall.lists.vector]
non_empty_dep [in Kildall.lists.vector]
not_lt_S [in Kildall.aux.aux_arith]
not_S_le [in Kildall.aux.aux_arith]
not_pred_lt_S_lt [in Kildall.aux.aux_arith]
not_var_in_tree_value [in Kildall.inst.substitutions]
no_change_at_p_not_in_succs [in Kildall.kildall.propa_property2]
no_change_at_p_not_in_w [in Kildall.kildall.propa_property]
no_loop_forest [in Kildall.aux.tree]
no_loop_tree [in Kildall.aux.tree]

O

order_subtree [in Kildall.aux.tree]
overwrite_replace [in Kildall.lists.vector_results]

P

pred_list_convert_belong [in Kildall.lists.pred_list]
pred_list_belong_convert [in Kildall.lists.pred_list]
pred_list_convert_length [in Kildall.lists.pred_list]
pred_list_convert_equiv [in Kildall.lists.pred_list]
pred_list_equiv_belong [in Kildall.lists.pred_list]
pred_list_split_equiv [in Kildall.lists.pred_list]
pred_list_equiv_split [in Kildall.lists.pred_list]
pred_list_equiv_sym [in Kildall.lists.pred_list]
pred_list_equiv_trans [in Kildall.lists.pred_list]
pred_list_equiv_refl [in Kildall.lists.pred_list]
pred_list_add_already_there_added [in Kildall.lists.pred_list]
pred_list_belong_added [in Kildall.lists.pred_list]
pred_list_add_already_there [in Kildall.lists.pred_list]
pred_list_belong_rem [in Kildall.lists.pred_list]
pred_list_belong_add [in Kildall.lists.pred_list]
pred_list_get_witness [in Kildall.lists.pred_list]
pred_list_belong_dec [in Kildall.lists.pred_list]
pred_list_belong_remove [in Kildall.lists.pred_list]
pred_list_to_list_belong [in Kildall.lists.pred_list]
pred_list_to_list_length [in Kildall.lists.pred_list]
prod_eq [in Kildall.kildall.propa_property2]
prod_eq [in Kildall.kildall.propa_property]
propa_lub [in Kildall.kildall.propa_property2]
propa_decrease [in Kildall.kildall.propa_property2]
propa_case [in Kildall.kildall.propa]
propa_replace_commut [in Kildall.kildall.propa_property]
propa_nondep_lexprod [in Kildall.kildall.propa_property]
propa_shapes_hvars [in Kildall.inst.fresh_variables]
push_list_is_app_rev [in Kildall.lists.lists]

R

ra_replace [in Kildall.kildall.propa]
really_fresh_alt [in Kildall.inst.fresh_variables]
Really_fresh [in Kildall.inst.fresh_variables]
reduction_keeps_wellshaped [in Kildall.inst.machine_shapes]
reduction_length [in Kildall.inst.machine_types]
reduction_progress [in Kildall.inst.machine_types]
reduction_keeps_welltyped [in Kildall.inst.machine_types]
reduction_keeps_wellformed [in Kildall.inst.machine]
reduction_to_execution [in Kildall.inst.machine]
reduction_determinism [in Kildall.inst.machine]
red_branch_else_keeps_welltyped [in Kildall.inst.machine_types]
red_branch_then_keeps_welltyped [in Kildall.inst.machine_types]
red_build_keeps_welltyped [in Kildall.inst.machine_types]
red_call_keeps_welltyped [in Kildall.inst.machine_types]
red_load_keeps_welltyped [in Kildall.inst.machine_types]
red_return_keeps_welltyped [in Kildall.inst.machine_types]
red_branch_else_keeps_wellformed [in Kildall.inst.machine]
red_branch_then_keeps_wellformed [in Kildall.inst.machine]
red_build_keeps_wellformed [in Kildall.inst.machine]
red_call_keeps_wellformed [in Kildall.inst.machine]
red_load_keeps_wellformed [in Kildall.inst.machine]
red_return_keeps_wellformed [in Kildall.inst.machine]
reflexive_vector_pointwise [in Kildall.lists.vector_results]
refl_dep_r [in Kildall.inst.inst_types]
refl_dep_r [in Kildall.inst.inst_shapes]
remove_compat [in Kildall.lists.m_list]
reverse_apply [in Kildall.inst.substitutions]
rev_map [in Kildall.lists.lists]
rev_length [in Kildall.lists.lists]
rev_lin_is_rev [in Kildall.lists.lists]
rev_list_typing [in Kildall.inst.typing]
R_to_r [in Kildall.aux.product_results]
r_is_semilattice [in Kildall.inst.inst_types]
r_is_order [in Kildall.inst.inst_types]
r_propa_ss_ts [in Kildall.kildall.propa_property2]
r_ss_propa_ss [in Kildall.kildall.propa_property]
r_S_is_semilattice [in Kildall.inst.inst_shapes]
r_S_is_order [in Kildall.inst.inst_shapes]

S

SI_vector_pointwise_or_eq_imp_vector_pointwise [in Kildall.lists.vector_results]
sl_to_list_sl [in Kildall.lists.vector_results]
sl_lub_to_list_sl_lub [in Kildall.lists.vector_results]
sl_order_to_list_sl_order [in Kildall.lists.vector_results]
split_vector_pointwise [in Kildall.lists.vector_results]
split_k_elements_none [in Kildall.lists.lists]
split_k_elements_some [in Kildall.lists.lists]
split_k_elements_length [in Kildall.lists.lists]
split_k_elements_ok [in Kildall.lists.lists]
split_vector [in Kildall.lists.vector]
Sss_init_Hvars [in Kildall.inst.fresh_variables]
stable_imp_Wti [in Kildall.inst.inst_types]
stable_equality [in Kildall.kildall.propa_property2]
stable_p_by_propa [in Kildall.kildall.propa_property]
stable_imp_Wshi [in Kildall.inst.inst_shapes]
Step_Succs_same_length [in Kildall.inst.inst_types]
Step_Succs_aux_same_length [in Kildall.inst.inst_types]
Step_equiv [in Kildall.inst.inst_types]
Step_S_Succs_same_length [in Kildall.inst.inst_shapes]
Step_S_Succs_aux_same_length [in Kildall.inst.inst_shapes]
Step_S_equiv [in Kildall.inst.inst_shapes]
strict_subtree_is_subtree_neq [in Kildall.aux.tree]
strict_subtree_size [in Kildall.aux.tree]
strongest_r_R [in Kildall.aux.product_results]
subst_unchanged [in Kildall.inst.substitutions]
subst_length [in Kildall.inst.substitutions]
subtree_size [in Kildall.aux.tree]
sub_pattern [in Kildall.inst.substitutions]
sub_list_typing_left [in Kildall.inst.typing]
sub_list_typing_right [in Kildall.inst.typing]
Succs_equiv [in Kildall.inst.instructions]
Succs_aux_equiv [in Kildall.inst.instructions]
Succs_better_bound [in Kildall.inst.instructions]
sup_iter_m_r [in Kildall.kildall.propa_property]
sup_iter_stable [in Kildall.kildall.propa_property]
sup_iter_r_in [in Kildall.kildall.propa_property]
sup_iter_r_arg [in Kildall.kildall.propa_property]
sup_iter_r [in Kildall.kildall.propa_property]
sup_S_is_lub [in Kildall.inst.inst_shapes]

T

tail_neq [in Kildall.lists.lists]
tail_length [in Kildall.lists.m_list]
Theorem_iter [in Kildall.kildall.itera_property]
top_free_dominates_args_implies_top_free_kildall [in Kildall.kildall.kildall_bv]
top_free_to_wi [in Kildall.kildall.kildall_bv]
Top_T_top [in Kildall.inst.inst_types]
Top_S_top [in Kildall.inst.inst_shapes]
transition [in Kildall.kildall.itera_property]
transitive_SI_vector_pointwise [in Kildall.lists.vector_results]
transitive_vector_pointwise [in Kildall.lists.vector_results]
tree_rec [in Kildall.aux.tree]
tree_ind [in Kildall.aux.tree]
tree_rec_aux [in Kildall.aux.tree]
tree_ind_aux [in Kildall.aux.tree]
tree_typing_args_length [in Kildall.inst.typing]
tree_to_args_typing [in Kildall.inst.typing]
T_free [in Kildall.kildall.dfa]

U

up_wl [in Kildall.kildall.kildall]

V

var_in_apply_elem_tree_aux2 [in Kildall.inst.substitutions]
var_in_apply_elem_tree_aux [in Kildall.inst.substitutions]
var_not_in_subst_unchanged [in Kildall.inst.substitutions]
var_not_in_subst_elem_unchanged [in Kildall.inst.substitutions]
var_not_in_subst_not_in_apply [in Kildall.inst.substitutions]
var_not_in_subst_not_in_apply_elem [in Kildall.inst.substitutions]
var_not_in_subst_elem [in Kildall.inst.substitutions]
vector_pointwise_imp_SI_vector_pointwise_or_eq [in Kildall.lists.vector_results]
vector_pointwise_to_element [in Kildall.lists.vector_results]
vector_pointwise_replace [in Kildall.lists.vector_results]
vector_pointwise_to_lexicographic_inv [in Kildall.lists.well_founded]

W

wellformed_execution [in Kildall.inst.machine]
wellformed_init_configuration [in Kildall.inst.machine]
wellformed_epsilon [in Kildall.inst.machine]
wellshaped_execution [in Kildall.inst.machine_shapes]
wellshaped_init_configuration [in Kildall.inst.machine_shapes]
welltyped_execution [in Kildall.inst.machine_types]
welltyped_init_configuration [in Kildall.inst.machine_types]
wfr [in Kildall.inst.inst_types]
wfr_S [in Kildall.inst.inst_shapes]
wf_nondep_lexprod [in Kildall.aux.product_results]
wf_R_to_r [in Kildall.aux.product_results]
wf_dep_nodep_lexprod [in Kildall.aux.product_results]
wf_lexicographic [in Kildall.lists.well_founded]
wf_lexicographic_step [in Kildall.lists.well_founded]
wf_lexicographic0 [in Kildall.lists.well_founded]
wf_lt_dep_length [in Kildall.kildall.iteraterme]
work_list_irrel_inc [in Kildall.kildall.kildall]
work_list_not_stable [in Kildall.kildall.kildall_dfa]
Wshi_Kildall [in Kildall.inst.machine_shapes]
Wshi_and_stable_agree [in Kildall.inst.inst_shapes]
Wshi_imp_stable [in Kildall.inst.inst_shapes]
Wti_and_stable_agree [in Kildall.inst.inst_types]
Wti_imp_stable [in Kildall.inst.inst_types]
Wti_Kildall [in Kildall.inst.machine_types]

Constructor Index

B

Bot_T [in Kildall.inst.inst_types]
Bot_S [in Kildall.inst.inst_shapes]

C

config_wrap_wt_list [in Kildall.inst.machine_types]
config_wrap_result [in Kildall.inst.machine_types]
config_wrap_error [in Kildall.inst.machine_types]
config_runtime [in Kildall.inst.machine]
config_stopped [in Kildall.inst.machine]
config_is_result [in Kildall.inst.machine]

E

execution_step [in Kildall.inst.machine]
execution_init [in Kildall.inst.machine]

I

i_branch [in Kildall.inst.instructions]
i_build [in Kildall.inst.instructions]
i_call [in Kildall.inst.instructions]
i_load [in Kildall.inst.instructions]
i_stop [in Kildall.inst.instructions]
i_return [in Kildall.inst.instructions]

L

Leaf [in Kildall.aux.tree]
lexicographic_intro2 [in Kildall.lists.well_founded]
lexicographic_intro1 [in Kildall.lists.well_founded]
lexprod_eq [in Kildall.aux.relations]
lexprod_inf [in Kildall.aux.relations]
le_cons [in Kildall.lists.vector]
le_nil [in Kildall.lists.vector]
list_pointwise_cons [in Kildall.lists.m_list]
list_pointwise_nil [in Kildall.lists.m_list]

M

mkconstr [in Kildall.inst.instructions]
mkframe [in Kildall.inst.instructions]
mkfunction [in Kildall.inst.instructions]
mksubst [in Kildall.inst.substitutions]
m_cons_inc [in Kildall.lists.m_list]
m_equiv_inc [in Kildall.lists.m_list]
m_list_pointwise_cons [in Kildall.lists.m_list]
m_list_pointwise_nil [in Kildall.lists.m_list]

N

Node [in Kildall.aux.tree]

P

pred_pointwise_cons [in Kildall.lists.pred_list]
pred_pointwise_nil [in Kildall.lists.pred_list]
pred_cons [in Kildall.lists.pred_list]
pred_nil [in Kildall.lists.pred_list]

R

red_branch_else [in Kildall.inst.machine]
red_branch_then [in Kildall.inst.machine]
red_build [in Kildall.inst.machine]
red_call [in Kildall.inst.machine]
red_load [in Kildall.inst.machine]
red_stop [in Kildall.inst.machine]
red_return [in Kildall.inst.machine]

S

Shapes [in Kildall.inst.inst_shapes]
strict_subtree_cons [in Kildall.aux.tree]
subtree_cons [in Kildall.aux.tree]
subtree_refl [in Kildall.aux.tree]
symbol [in Kildall.inst.substitutions]

T

Top_T [in Kildall.inst.inst_types]
Top_S [in Kildall.inst.inst_shapes]
tree_list_typing_cons [in Kildall.inst.typing]
tree_list_typing_nil [in Kildall.inst.typing]
Types [in Kildall.inst.inst_types]

V

vector_cons [in Kildall.lists.vector]
vector_nil [in Kildall.lists.vector]

W

wellshaped_conf [in Kildall.inst.machine_shapes]
welltyped_conf [in Kildall.inst.machine_types]

X

x [in Kildall.inst.substitutions]

Axiom Index

C

constructors [in Kildall.inst.machine]

E

eq_name_dec [in Kildall.inst.instructions]

F

functions [in Kildall.inst.machine]

L

lrs_functions [in Kildall.inst.machine]

N

name [in Kildall.inst.instructions]
nonvoidfcn [in Kildall.inst.machine]

Inductive Index

C

config_wrap [in Kildall.inst.machine_types]
config_error [in Kildall.inst.machine]
config_result [in Kildall.inst.machine]

E

execution [in Kildall.inst.machine]

I

instruction [in Kildall.inst.instructions]

L

lexicographic [in Kildall.lists.well_founded]
list_pointwise [in Kildall.lists.m_list]

M

m_list_inc [in Kildall.lists.m_list]
m_list_pointwise [in Kildall.lists.m_list]

N

Name [in Kildall.inst.substitutions]
nondep_lexprod [in Kildall.aux.relations]

P

pred_pointwise [in Kildall.lists.pred_list]
pred_list [in Kildall.lists.pred_list]

R

reduction [in Kildall.inst.machine]

S

Sigma [in Kildall.inst.inst_types]
Sigma_S [in Kildall.inst.inst_shapes]
strict_subtree [in Kildall.aux.tree]
subtree [in Kildall.aux.tree]

T

tree [in Kildall.aux.tree]
tree_list_typing [in Kildall.inst.typing]

V

vector [in Kildall.lists.vector]
vector_pointwise [in Kildall.lists.vector]

W

wellshaped_configuration [in Kildall.inst.machine_shapes]
welltyped_configuration [in Kildall.inst.machine_types]

Projection Index

C

cons_ret [in Kildall.inst.instructions]
cons_args [in Kildall.inst.instructions]
cons_name [in Kildall.inst.instructions]

F

fcn_bytecode [in Kildall.inst.instructions]
fcn_size [in Kildall.inst.instructions]
fcn_ret [in Kildall.inst.instructions]
fcn_args [in Kildall.inst.instructions]
fcn_name [in Kildall.inst.instructions]
frm_args [in Kildall.inst.instructions]
frm_stack [in Kildall.inst.instructions]
frm_pc [in Kildall.inst.instructions]
frm_fun [in Kildall.inst.instructions]

S

subst_expr [in Kildall.inst.substitutions]

X

xi [in Kildall.inst.substitutions]
xj [in Kildall.inst.substitutions]

Section Index

A

asc_list [in Kildall.lists.well_founded]
aux_arith [in Kildall.aux.aux_arith]

D

Data_flow_analysis [in Kildall.kildall.dfa]

F

fold_bool [in Kildall.lists.lists]
fresh_variables [in Kildall.inst.fresh_variables]

I

instructions [in Kildall.inst.instructions]
inst_types [in Kildall.inst.inst_types]
inst_shapes [in Kildall.inst.inst_shapes]
iter [in Kildall.kildall.itera]
iteraterme [in Kildall.kildall.iteraterme]
itera_eq [in Kildall.kildall.itera_eq]
itera_property [in Kildall.kildall.itera_property]

K

kildall [in Kildall.kildall.kildall]
kildall_bytecode_verifier [in Kildall.kildall.kildall_bv]
kildall_data_flow_analizer [in Kildall.kildall.kildall_dfa]

L

lists [in Kildall.lists.lists]

M

machine [in Kildall.inst.machine]
machine_shapes [in Kildall.inst.machine_shapes]
machine_types [in Kildall.inst.machine_types]
m_list [in Kildall.lists.m_list]

N

nat_bounded_list [in Kildall.lists.nat_bounded_list]

P

pred_list_convertion [in Kildall.lists.pred_list]
pred_list_equivalence [in Kildall.lists.pred_list]
pred_list [in Kildall.lists.pred_list]
product_results [in Kildall.aux.product_results]
propa [in Kildall.kildall.propa]
propa_property2 [in Kildall.kildall.propa_property2]
propa_property [in Kildall.kildall.propa_property]

R

relations [in Kildall.aux.relations]

S

semilattices [in Kildall.aux.semilattices]
substitutions [in Kildall.inst.substitutions]

T

tree [in Kildall.aux.tree]
typing [in Kildall.inst.typing]

V

Vector [in Kildall.lists.vector]
Vector_results [in Kildall.lists.vector_results]

W

wf_list [in Kildall.lists.well_founded]

Abbreviation Index

A

Acc_ssw [in Kildall.kildall.itera_property]

B

bc [in Kildall.inst.inst_types]
bc [in Kildall.inst.inst_shapes]

C

configuration [in Kildall.inst.machine_shapes]
configuration [in Kildall.inst.instructions]
configuration [in Kildall.inst.machine_types]
configuration [in Kildall.inst.machine]
configuration [in Kildall.inst.fresh_variables]

E

eq_value_dec [in Kildall.inst.instructions]
Expression [in Kildall.inst.machine_shapes]
Expression [in Kildall.inst.inst_shapes]
Expression [in Kildall.inst.substitutions]
Expression [in Kildall.inst.fresh_variables]

F

forest [in Kildall.aux.tree]
Frm [in Kildall.inst.machine_shapes]
Frm [in Kildall.inst.machine_types]
Frm [in Kildall.inst.fresh_variables]

G

Get_constr [in Kildall.inst.machine_shapes]
Get_function [in Kildall.inst.machine_shapes]
Get_constr [in Kildall.inst.inst_types]
Get_function [in Kildall.inst.inst_types]
Get_constr [in Kildall.inst.machine_types]
Get_function [in Kildall.inst.machine_types]
Get_constr [in Kildall.inst.inst_shapes]
Get_function [in Kildall.inst.inst_shapes]
Get_function [in Kildall.inst.substitutions]
Get_constr [in Kildall.inst.typing]
Get_constr [in Kildall.inst.machine]
Get_function [in Kildall.inst.machine]
Get_constr [in Kildall.inst.fresh_variables]
Get_function [in Kildall.inst.fresh_variables]

I

Instruction [in Kildall.inst.inst_types]
Instruction [in Kildall.inst.inst_shapes]
IS_bytecode_verifier [in Kildall.kildall.kildall_bv]
IS_data_flow_analyser [in Kildall.kildall.kildall_bv]
IS_data_flow_analyser [in Kildall.kildall.kildall_dfa]
Itera [in Kildall.kildall.itera_eq]
Itera [in Kildall.kildall.kildall]
Itera [in Kildall.kildall.itera_property]
Iteraterme [in Kildall.kildall.itera]
Itera_eq [in Kildall.kildall.itera_property]

K

KIldall [in Kildall.kildall.kildall_bv]
KIldall [in Kildall.kildall.kildall_dfa]

M

MonotoneStep [in Kildall.kildall.kildall_bv]
MonotoneStep [in Kildall.kildall.kildall_dfa]

N

n [in Kildall.inst.inst_types]
n [in Kildall.inst.inst_shapes]

P

Propa [in Kildall.kildall.itera_eq]
Propa [in Kildall.kildall.propa_property2]
Propa [in Kildall.kildall.propa_property]
Propa [in Kildall.kildall.itera_property]
Propa [in Kildall.kildall.iteraterme]
Propa_nondep_lexprod [in Kildall.kildall.itera_property]

R

ra [in Kildall.kildall.propa_property2]
ra [in Kildall.kildall.propa]
ra [in Kildall.kildall.propa_property]
ra [in Kildall.kildall.itera_property]
ra [in Kildall.kildall.iteraterme]
Rt [in Kildall.inst.inst_types]

S

Stable [in Kildall.kildall.dfa]
Stables [in Kildall.kildall.dfa]
Step' [in Kildall.kildall.itera_eq]
Step' [in Kildall.kildall.kildall_bv]
Step' [in Kildall.kildall.propa_property2]
Step' [in Kildall.kildall.itera]
Step' [in Kildall.kildall.kildall]
Step' [in Kildall.kildall.itera_property]
Step' [in Kildall.kildall.kildall_dfa]
Step' [in Kildall.kildall.iteraterme]
Substitution [in Kildall.inst.machine_shapes]
Substitution [in Kildall.inst.inst_shapes]
Substitution [in Kildall.inst.substitutions]
Substitution [in Kildall.inst.fresh_variables]
sup_iter [in Kildall.kildall.propa_property2]

V

value [in Kildall.inst.substitutions]

W

Wi_and_stable_agree [in Kildall.kildall.kildall_bv]

Definition Index

A

apply [in Kildall.inst.substitutions]
apply_elem_tree [in Kildall.inst.substitutions]
ascending_chain [in Kildall.aux.relations]

B

belong_element_vector [in Kildall.lists.vector]
binop [in Kildall.aux.relations]

C

combine [in Kildall.lists.m_list]
compose [in Kildall.kildall.iteraterme]
constant_list [in Kildall.lists.vector]

D

dfa_type [in Kildall.kildall.dfa]

E

element_at_list [in Kildall.lists.lists]
element_at_unsafe [in Kildall.lists.vector]
element_at [in Kildall.lists.vector]
eq_list [in Kildall.lists.vector]

F

f [in Kildall.inst.inst_types]
fl [in Kildall.kildall.iteraterme]
fold_left2 [in Kildall.inst.typing]
fonctionnal_reduction [in Kildall.inst.machine_types]
frames_args_length [in Kildall.inst.machine_types]
fresh [in Kildall.inst.substitutions]

G

get_constr_by_name [in Kildall.inst.instructions]
get_function_by_name [in Kildall.inst.instructions]

H

hd' [in Kildall.lists.vector]
head [in Kildall.lists.vector]
head' [in Kildall.lists.vector]
Hvars [in Kildall.inst.machine_shapes]
Hvars [in Kildall.inst.fresh_variables]

I

init_subst [in Kildall.inst.substitutions]
init_vars [in Kildall.inst.substitutions]
Init_configuration [in Kildall.inst.machine]
inv [in Kildall.aux.relations]
Invariant [in Kildall.inst.machine]
Is_bytecode_verifier [in Kildall.kildall.dfa]
Is_data_flow_analyser [in Kildall.kildall.dfa]
is_top_element [in Kildall.kildall.dfa]
is_stable [in Kildall.kildall.kildall]
itera [in Kildall.kildall.itera]
itera_shapes [in Kildall.inst.fresh_variables]

K

Kildall [in Kildall.kildall.kildall]
Kildall_Shapes [in Kildall.inst.machine_shapes]
Kildall_types [in Kildall.inst.inst_types]
Kildall_Types [in Kildall.inst.machine_types]
Kildall_shapes [in Kildall.inst.inst_shapes]
Kildall_Shapes [in Kildall.inst.fresh_variables]

L

last_return_or_stop [in Kildall.inst.instructions]
le_lt_Sn_m [in Kildall.kildall.kildall]
list_to_pred_list [in Kildall.lists.pred_list]
lt_nb_length [in Kildall.lists.nat_bounded_list]
lt_pred_length [in Kildall.lists.pred_list]
lt_m_length [in Kildall.lists.m_list]
lub [in Kildall.aux.relations]

M

make_substitution [in Kildall.inst.substitutions]
Map2 [in Kildall.lists.vector]
map2 [in Kildall.lists.vector]
monotonestep [in Kildall.kildall.propa_property2]
m_list_belong_snd [in Kildall.lists.m_list]
m_list_belong_fst [in Kildall.lists.m_list]
m_list_equiv [in Kildall.lists.m_list]
m_length [in Kildall.lists.m_list]
m_list_remove [in Kildall.lists.m_list]
m_list_get_witness [in Kildall.lists.m_list]
m_list_belong_dec [in Kildall.lists.m_list]
m_list_belong [in Kildall.lists.m_list]
m_list_add_element [in Kildall.lists.m_list]
m_cons [in Kildall.lists.m_list]
m_nil [in Kildall.lists.m_list]
m_list [in Kildall.lists.m_list]

N

nb_list_convert_belong [in Kildall.lists.nat_bounded_list]
nb_list_belong_convert [in Kildall.lists.nat_bounded_list]
nb_list_convert_length [in Kildall.lists.nat_bounded_list]
nb_list_convert_equiv [in Kildall.lists.nat_bounded_list]
nb_list_convert [in Kildall.lists.nat_bounded_list]
nb_list_equiv [in Kildall.lists.nat_bounded_list]
nb_length [in Kildall.lists.nat_bounded_list]
nb_list_remove [in Kildall.lists.nat_bounded_list]
nb_list_belong_added [in Kildall.lists.nat_bounded_list]
nb_list_add_already_there_added [in Kildall.lists.nat_bounded_list]
nb_list_add_already_there [in Kildall.lists.nat_bounded_list]
nb_list_belong_rem [in Kildall.lists.nat_bounded_list]
nb_list_belong_add [in Kildall.lists.nat_bounded_list]
nb_list_get_witness [in Kildall.lists.nat_bounded_list]
nb_list_belong_dec [in Kildall.lists.nat_bounded_list]
nb_list_belong [in Kildall.lists.nat_bounded_list]
nb_list_add_element [in Kildall.lists.nat_bounded_list]
nb_cons [in Kildall.lists.nat_bounded_list]
nb_nil [in Kildall.lists.nat_bounded_list]
nb_list [in Kildall.lists.nat_bounded_list]
nodep_prod_of_dep [in Kildall.aux.product_results]

P

P [in Kildall.lists.nat_bounded_list]
pred_list_convert [in Kildall.lists.pred_list]
pred_list_equiv [in Kildall.lists.pred_list]
pred_list_to_list [in Kildall.lists.pred_list]
pred_length [in Kildall.lists.pred_list]
pred_list_remove [in Kildall.lists.pred_list]
pred_list_belong [in Kildall.lists.pred_list]
pred_list_add_element [in Kildall.lists.pred_list]
propagate [in Kildall.kildall.propa]
propagate_shapes [in Kildall.inst.fresh_variables]
push_list [in Kildall.lists.lists]

Q

Q [in Kildall.lists.m_list]

R

r [in Kildall.inst.inst_types]
rb [in Kildall.kildall.propa_property]
rev_lin [in Kildall.lists.lists]
r_S [in Kildall.inst.inst_shapes]

S

semilattice [in Kildall.aux.semilattices]
SI_vector_pointwise [in Kildall.lists.vector]
split_k_elements [in Kildall.lists.lists]
Sss_init [in Kildall.inst.machine_shapes]
Sss_init [in Kildall.inst.fresh_variables]
ss_init [in Kildall.inst.machine_shapes]
ss_init [in Kildall.inst.machine_types]
ss_init [in Kildall.inst.fresh_variables]
stable [in Kildall.kildall.itera]
stables [in Kildall.kildall.itera]
stack_shaping [in Kildall.inst.substitutions]
stack_typing [in Kildall.inst.typing]
Step [in Kildall.inst.inst_types]
Step_S [in Kildall.inst.inst_shapes]
Step_S' [in Kildall.inst.fresh_variables]
step' [in Kildall.kildall.propa_property]
strict [in Kildall.aux.relations]
Succs [in Kildall.inst.instructions]
Succs_aux [in Kildall.inst.instructions]
sup_iter [in Kildall.kildall.propa_property]
sup_S [in Kildall.inst.inst_shapes]

T

tail [in Kildall.lists.vector]
tree_size [in Kildall.aux.tree]
tree_name_to_tree_Name [in Kildall.inst.substitutions]
tree_is_pattern [in Kildall.inst.substitutions]
tree_is_pattern_bool [in Kildall.inst.substitutions]
tree_typing [in Kildall.inst.typing]

V

value [in Kildall.inst.instructions]
var_in_subst_elem [in Kildall.inst.substitutions]
var_not_in_tree [in Kildall.inst.substitutions]
var_in_tree_bool [in Kildall.inst.substitutions]
vector_map [in Kildall.lists.vector]
vector_replace [in Kildall.lists.vector]
Vector_pointwise [in Kildall.lists.vector]

W

wellformed_configuration [in Kildall.inst.machine]
wellshaped_plus_frame [in Kildall.inst.machine_shapes]
welltyped_frame [in Kildall.inst.machine_types]
welltyping [in Kildall.kildall.dfa]
wi_and_stable_agree [in Kildall.kildall.dfa]
work_list [in Kildall.kildall.kildall]
Wshi [in Kildall.inst.inst_shapes]
Wti [in Kildall.inst.inst_types]

Record Index

C

constr [in Kildall.inst.instructions]

F

frame [in Kildall.inst.instructions]
function [in Kildall.inst.instructions]

S

subst_elem [in Kildall.inst.substitutions]

Global Index

J

Y

Z

_

(958 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

(23 entries)

Variable Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(171 entries)

Library Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(32 entries)

Lemma Index

J

Q

X

Y

Z

_

other

(366 entries)

Constructor Index

A

D

F

G

H

J

K

O

Q

U

Y

Z

_

other

(60 entries)

Axiom Index

A

B

D

G

H

I

J

K

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Inductive Index

A

B

D

F

G

H

J

K

O

Q

U

X

Y

Z

_

other

(24 entries)

Projection Index

A

B

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

Y

Z

_

other

(15 entries)

Section Index

B

C

E

G

H

J

O

Q

U

X

Y

Z

_

other

(36 entries)

Abbreviation Index

D

H

J

L

O

Q

T

U

X

Y

Z

_

other

(76 entries)

Definition Index

J

O

U

X

Y

Z

_

other

(145 entries)

Record Index

A

B

D

E

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)