Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (866 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (30 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (24 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (451 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (37 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (173 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries)

Global Index

A

ADP_after [constructor, in assert]
ADP_here [constructor, in assert]
ADS_assert [constructor, in assert]
ADS_while [constructor, in assert]
ADS_ifb_r [constructor, in assert]
ADS_ifb_l [constructor, in assert]
aeval [definition, in semantics3]
aexp [inductive, in prog]
affected_prog_In [lemma, in semantics3]
affected_prog [definition, in semantics3]
AIP_after [constructor, in data]
AIP_here [constructor, in data]
AIS_while [constructor, in data]
AIS_ifb_r [constructor, in data]
AIS_ifb_l [constructor, in data]
AIS_ass [constructor, in data]
alpha [constructor, in parser]
and_or_distr_l [lemma, in decidable]
ante_diff_emptyset_l [lemma, in set_relation]
ante_diff_In [lemma, in set_relation]
ante_diff [definition, in set_relation]
appears_in [definition, in set_relation]
app_prog_cons [lemma, in seq]
app_prog [definition, in prog]
app_prog_list_nil_r [lemma, in data]
app_prog_list_app_r [lemma, in data]
app_prog_list [definition, in data]
assert [library]
assert_depsR_prog_dec [lemma, in assert]
assert_depsR_prog_stable [lemma, in assert]
assert_depsR_prog_label_inR_prog [lemma, in assert]
assert_depsR_stmt_mutual_ind [definition, in assert]
assert_depsR_prog_mutual_ind [definition, in assert]
assert_depsR_stmt [inductive, in assert]
assert_depsR_prog [inductive, in assert]
assert_depsR_prog_stable_app [lemma, in semantics3]
assert_depsR_prog_stable_cons [lemma, in semantics3]
assert_depsR_prog_stable_after [lemma, in semantics3]
ass_inR_prog_dec [lemma, in data]
ass_inR_stmt [inductive, in data]
ass_inR_prog [inductive, in data]
ass_inR_prog_seq [lemma, in set_deps]
ass_not_preserved_proj_equal_ok [lemma, in semantics3]
ass_not_preserved_mayread [lemma, in semantics3]
ass_not_inR_prog_is_flat_of [lemma, in semantics3]
ass_inR_prog_single [lemma, in semantics3]
ass_inR_prog_app [lemma, in semantics3]
ass_not_preserved_proj_equal [lemma, in semantics3]
aux5 [definition, in set_relation]
aux5_correct [lemma, in set_relation]
aux5_grow [lemma, in set_relation]
aux5_incl_res [lemma, in set_relation]
aux5_equation_S [lemma, in set_relation]
A_mult [constructor, in prog]
A_minus [constructor, in prog]
A_plus [constructor, in prog]
A_id [constructor, in prog]
A_num [constructor, in prog]


B

beval [definition, in semantics3]
bexp [inductive, in prog]
bignumber [definition, in parser]
build_symtable [definition, in parser]
B_and [constructor, in prog]
B_not [constructor, in prog]
B_le [constructor, in prog]
B_eq [constructor, in prog]
B_false [constructor, in prog]
B_true [constructor, in prog]


C

CDP_after [constructor, in control]
CDP_here [constructor, in control]
CDS_while_cond [constructor, in control]
CDS_while [constructor, in control]
CDS_ifb_cond_r [constructor, in control]
CDS_ifb_cond_l [constructor, in control]
CDS_ifb_r [constructor, in control]
CDS_ifb_l [constructor, in control]
chartype [inductive, in parser]
classifyChar [definition, in parser]
cons_prog_list_app [lemma, in data]
cons_prog_list_nil [lemma, in data]
cons_prog_list [definition, in data]
control [library]
control_depsR_prog_stable_app [lemma, in semantics3]
control_depsR_prog_stable_cons_reverse [lemma, in semantics3]
control_depsR_prog_stable_cons [lemma, in semantics3]
control_depsR_prog_stable_unrel [lemma, in semantics3]
control_depsR_prog_stable_quotient [lemma, in semantics3]
control_depsR_prog_quotient_include [lemma, in semantics3]
control_depsR_prog_stable [lemma, in control]
control_depsR_label_inR_prog [lemma, in control]
control_stmt_get_label [lemma, in control]
control_ifb [lemma, in control]
control_depsR_stmt_mutual_ind [definition, in control]
control_depsR_prog_mutual_ind [definition, in control]
control_depsR_stmt [inductive, in control]
control_depsR_prog [inductive, in control]


D

data [library]
data_deps_prog_correct [lemma, in data]
data_deps_prog [definition, in data]
data_depsR_prog_after [lemma, in data]
data_depsR_prog_here [lemma, in data]
data_depsR_prog_stable [lemma, in data]
data_depsR_label_inR_prog [lemma, in data]
data_depsR_prog [inductive, in data]
data_depsR_prog_stable_after [lemma, in semantics3]
data_depsR_prog_stable_unrel [lemma, in semantics3]
data_depsR_prog_unrel [lemma, in semantics3]
DDP_flat [constructor, in data]
decidable [library]
DecidableType [record, in set]
dec_is_decidable [lemma, in decidable]
definitions [section, in slice]
digit [constructor, in parser]
digit_of_nat [definition, in parser]
DS [section, in set]
DS_pair [instance, in set2]
DS_id [instance, in set_instance]
DS_label [instance, in set_instance]
DS_sequel_map [section, in set]
DS_sequel [section, in set]
DS_decide [projection, in set]


E

empty_set [definition, in set]
empty_state [definition, in semantics3]
enter [definition, in parser]
equivalence [section, in set]
equivalence_map [section, in set]
eq_id_dec [lemma, in prog]
expect [definition, in parser]


F

FDP_after [constructor, in data]
FDP_unrel [constructor, in data]
FDP_here [constructor, in data]
filter_length [lemma, in proj_vs_traj]
find_last_nil [lemma, in set_relation]
find_last_keeps_last [lemma, in set_relation]
find_last_keeps_head [lemma, in set_relation]
find_last_stays_sorted [lemma, in set_relation]
find_last_include [lemma, in set_relation]
find_last_decrease [lemma, in set_relation]
find_last [definition, in set_relation]
first [definition, in set_relation]
firstExpect [definition, in parser]
firstn_full [lemma, in set_relation]
firstn_incl [lemma, in set_relation]
first_true_if [lemma, in set_relation]
first_true [lemma, in set_relation]
first_false_forall [lemma, in set_relation]
first_false [lemma, in set_relation]
first_results [library]
flat_list_prog_single [lemma, in data]
flat_data_depsR_prog_decomposition [lemma, in data]
flat_data_depsR_prog_grow_m [lemma, in data]
flat_data_depsR_prog_unrel [lemma, in data]
flat_data_deps_prog_complete [lemma, in data]
flat_data_deps_prog_correct [lemma, in data]
flat_list_prog_correct [lemma, in data]
flat_list_stmt [definition, in data]
flat_list_prog [definition, in data]
flat_data_depsR_prog_grow_r [lemma, in data]
flat_data_depsR_prog_grow_l [lemma, in data]
flat_l_stmt_correct [lemma, in data]
flat_l_prog_correct [lemma, in data]
flat_l_stmt [definition, in data]
flat_l_prog [definition, in data]
flat_data_depsR_label_inR_prog [lemma, in data]
flat_data_depsR_prog [inductive, in data]
flat_l_prog_label [lemma, in semantics3]
flat_data_depsR_prog_app_unrel [lemma, in semantics3]
flat_data_depsR_prog_stable_prefix [lemma, in semantics3]
flat_data_depsR_prog_prefix [lemma, in semantics3]
flat_state_prog_proj_traj [lemma, in semantics3]
flat_data_depsR_prog_stable_unrel [lemma, in semantics3]
flat_data_depsR_prog_stable_after [lemma, in semantics3]
flat_data_depsR_prog_unrel [lemma, in semantics3]
flat_state_prog_prefix_is_flatR_of [lemma, in semantics3]
flat_state_prog_prefix [lemma, in semantics3]
flat_state_prog_traj_length [lemma, in semantics3]
flat_state_prog_is_flatR_of_if_terminating_no_error [lemma, in semantics3]
flat_state_prog_num_lab [lemma, in semantics3]
flat_state_prog_traj [lemma, in semantics3]
flat_state_prog_is_flatR [lemma, in semantics3]
flat_state_prog [definition, in semantics3]
forall_fun_ext [lemma, in set_relation]
forall_firstn [lemma, in set_relation]
forall_sorted_firstn [lemma, in set_relation]
forall_sorted [lemma, in set_relation]
forall_filter [lemma, in proj_vs_traj]


G

getLabel [definition, in set_relation]


H

hdrel_firstn [lemma, in set_relation]
hdrel_fun_ext [lemma, in set_relation]


I

IBFOP_cons [constructor, in set_deps]
IBFOP_nil [constructor, in set_deps]
IBFOS_assert [constructor, in set_deps]
IBFOS_while_end [constructor, in set_deps]
IBFOS_while_loop [constructor, in set_deps]
IBFOS_ifb_r [constructor, in set_deps]
IBFOS_ifb_l [constructor, in set_deps]
IBFOS_ass [constructor, in set_deps]
IBFOS_skip [constructor, in set_deps]
Id [constructor, in prog]
id [inductive, in prog]
id [section, in set_prog]
id_inR_bexp [inductive, in prog]
id_inR_aexp [inductive, in prog]
id_inR_ref_prog_stmt_inR_prog [lemma, in data]
id_inR_ref_prog [inductive, in data]
id_in_ref_correct [lemma, in data]
id_in_ref [definition, in data]
id_in_bexp_correct [lemma, in data]
id_in_bexp [definition, in data]
id_in_aexp_correct [lemma, in data]
id_in_aexp [definition, in data]
id_inR_ref [inductive, in data]
id_not_in_mayread_prog_update [lemma, in semantics3]
ifb_not_preserved_stable_not_preserved_r [lemma, in semantics3]
ifb_not_preserved_stable_not_preserved_l [lemma, in semantics3]
IFOP_cons [constructor, in data]
IFOP_nil [constructor, in data]
IFOS_assert [constructor, in data]
IFOS_while_end [constructor, in data]
IFOS_while_loop [constructor, in data]
IFOS_ifb_r [constructor, in data]
IFOS_ifb_l [constructor, in data]
IFOS_ass [constructor, in data]
IFOS_skip [constructor, in data]
IFP_cons [constructor, in data]
IFP_nil [constructor, in data]
IFS_assert [constructor, in data]
IFS_ass [constructor, in data]
IFS_skip [constructor, in data]
IIA_mult_r [constructor, in prog]
IIA_mult_l [constructor, in prog]
IIA_minus_r [constructor, in prog]
IIA_minus_l [constructor, in prog]
IIA_plus_r [constructor, in prog]
IIA_plus_l [constructor, in prog]
IIA_id [constructor, in prog]
IIB_and_r [constructor, in prog]
IIB_and_l [constructor, in prog]
IIB_not [constructor, in prog]
IIB_le_r [constructor, in prog]
IIB_le_l [constructor, in prog]
IIB_eq_r [constructor, in prog]
IIB_eq_l [constructor, in prog]
IIR_after [constructor, in data]
IIR_here [constructor, in data]
IIR_assert [constructor, in data]
IIR_while [constructor, in data]
IIR_ifb [constructor, in data]
IIR_ass [constructor, in data]
include [inductive, in set_relation]
include_forall [lemma, in set_relation]
include_incl [lemma, in set_relation]
include_appears_in [lemma, in set_relation]
include_nil_l [lemma, in set_relation]
include_trans [lemma, in set_relation]
include_refl [lemma, in set_relation]
include_after [constructor, in set_relation]
include_here [constructor, in set_relation]
include_nil [constructor, in set_relation]
include_rt [lemma, in control]
index_proj_bounded [lemma, in first_results]
index_proj [definition, in first_results]
inverse [definition, in set_relation]
inverse_r [lemma, in set_relation]
in_flat_list_prog_seq [lemma, in data]
in_app_prog_list [lemma, in data]
in_cons_prog_list [lemma, in data]
IQP_stmt [constructor, in quotient]
IQP_remove [constructor, in quotient]
IQP_nil [constructor, in quotient]
IQS_assert [constructor, in quotient]
IQS_while [constructor, in quotient]
IQS_ifb [constructor, in quotient]
IQS_ass [constructor, in quotient]
IQS_skip [constructor, in quotient]
isAlpha [definition, in parser]
isDigit [definition, in parser]
isLowerAlpha [definition, in parser]
isParenthese [definition, in parser]
isWhite [definition, in parser]
is_quotientR_prog_single [lemma, in quotient]
is_quotientR_in_seq [lemma, in quotient]
is_quotientR_trans [lemma, in quotient]
is_quotientR_antisym [lemma, in quotient]
is_quotientR_prog_same_num [lemma, in quotient]
is_quotientR_stmt_num_lab [lemma, in quotient]
is_quotientR_prog_num_lab [lemma, in quotient]
is_quotientR_refl [lemma, in quotient]
is_quotientR_stmt_mutual_ind [definition, in quotient]
is_quotientR_prog_mutual_ind [definition, in quotient]
is_quotientR_stmt [inductive, in quotient]
is_quotientR_prog [inductive, in quotient]
Is_true_eq_true_iff [lemma, in set_relation]
is_flatR_of_prog_intro [lemma, in data]
is_flatR_of_prog_self [lemma, in data]
is_flatR_of_prog_is_flatR [lemma, in data]
is_flatR_prog_app [lemma, in data]
is_quotientR_prog_nil_r [lemma, in data]
is_flatR_of_prog_cut [lemma, in data]
is_quotientR_prog_is_flatR [lemma, in data]
is_flatR_prog_single [lemma, in data]
is_flatR_stmt_mutual_ind [definition, in data]
is_flatR_prog_mutual_ind [definition, in data]
is_flatR_stmt [inductive, in data]
is_flatR_prog [inductive, in data]
is_flatR_of_prog_single [lemma, in data]
is_flatR_of_prog_label [lemma, in data]
is_flatR_of_stmt_mutual_ind [definition, in data]
is_flatR_of_prog_mutual_ind [definition, in data]
is_flatR_of_stmt [inductive, in data]
is_flatR_of_prog [inductive, in data]
is_flatR_of_prog_set_data_incl [lemma, in set_deps]
is_flatR_stmt_maydef [lemma, in set_deps]
is_flatR_stmt_mayread [lemma, in set_deps]
is_flatR_stmt_mustdef [lemma, in set_deps]
is_flatR_prog_mustdef [lemma, in set_deps]
is_flatR_of_prog_mayread_incl [lemma, in set_deps]
is_flatR_of_prog_maydef_incl [lemma, in set_deps]
is_flatR_of_prog_mustdef_incl [lemma, in set_deps]
is_flatR_prog_app_reverse [lemma, in set_deps]
is_flatR_prog_is_flatR_of_same [lemma, in set_deps]
is_bounded_flatR_of_prog_is_flatR_of [lemma, in set_deps]
is_bounded_flatR_of_stmt_mutual_ind [definition, in set_deps]
is_bounded_flatR_of_prog_mutual_ind [definition, in set_deps]
is_bounded_flatR_of_stmt [inductive, in set_deps]
is_bounded_flatR_of_prog [inductive, in set_deps]
is_flatR_stmt_num_lab [lemma, in semantics3]
is_flatR_prog_unrel [lemma, in semantics3]
is_flatR_prog_no_control [lemma, in semantics3]
is_flatR_prog_proj_traj_keep_L_prefix [lemma, in semantics3]
is_flatR_prog_num_lab_not_reached [lemma, in semantics3]
is_flatR_prog_traj_length [lemma, in semantics3]
is_flatR_of_prog_one_step [lemma, in semantics3]


K

keep_L_prog_involutive_quotient [lemma, in semantics3]
keep_L_stmt_quotient [lemma, in semantics3]
keep_L_prog_flat_reverse [lemma, in semantics3]
keep_L_prog_app_bis_reverse [lemma, in semantics3]
keep_L_prog_app_reverse [lemma, in semantics3]
keep_L_prog_cons_reverse [lemma, in semantics3]
keep_L_prog_flat [lemma, in semantics3]
keep_L_prog_nil_flat_nil [lemma, in semantics3]
keep_L_prog_app [lemma, in semantics3]
keep_L_prog_label [lemma, in control]
keep_L_prog_quotient [lemma, in control]
keep_L_stmt [definition, in control]
keep_L_prog [definition, in control]


L

label [definition, in prog]
label [section, in set_prog]
label [library]
label_inR_prog_iff_in_set_of_labels [lemma, in set_prog]
label_inR_prog_seq [lemma, in label]
label_first_label_inR_prog [lemma, in label]
label_first_inR_prog [inductive, in label]
label_inR_prog_dec [lemma, in label]
label_in_prog_correct [lemma, in label]
label_inR_stmt_mutual_ind [definition, in label]
label_inR_prog_mutual_ind [definition, in label]
label_inR_stmt [inductive, in label]
label_inR_prog [inductive, in label]
label_in_prog_iff_in_list_of_labels [lemma, in label]
label_in_app [lemma, in label]
label_in [definition, in label]
label_in_stmt [definition, in label]
label_in_prog [definition, in label]
label_first_inR_prog_quotient_include [lemma, in semantics3]
last [library]
last_state_map [lemma, in last_state]
last_state_is_map [lemma, in last_state]
last_f_not_empty_In [lemma, in last_state]
last_state_cons_change_default [lemma, in last_state]
last_state_not_empty [lemma, in last_state]
last_state_not_default [lemma, in last_state]
last_state_app_not_nil [lemma, in last_state]
last_last_cons_not_nil [lemma, in last_state]
last_state [definition, in last_state]
last_f_map [lemma, in last_f]
last_f_is_map [lemma, in last_f]
last_f_not_empty_In [lemma, in last_f]
last_f_cons_change_default [lemma, in last_f]
last_f_not_empty [lemma, in last_f]
last_f_not_default [lemma, in last_f]
last_f_app_not_nil [lemma, in last_f]
last_f_cons_not_nil [lemma, in last_f]
last_f [definition, in last_f]
last_filter [lemma, in last]
last_firstn [lemma, in last]
last_map [lemma, in last]
last_not_empty_In [lemma, in last]
last_cons_change_default [lemma, in last]
last_not_empty [lemma, in last]
last_not_default [lemma, in last]
last_app_not_nil [lemma, in last]
last_cons_not_nil [lemma, in last]
last_last_f [lemma, in last]
last_state [library]
last_f [library]
LFP_after [constructor, in label]
LFP_here [constructor, in label]
LIP_after [constructor, in label]
LIP_here [constructor, in label]
list_of_labels_stmt [definition, in label]
list_of_labels_prog [definition, in label]
list_of_string [definition, in parser]
LIS_assert [constructor, in label]
LIS_while_body [constructor, in label]
LIS_while_cond [constructor, in label]
LIS_ifb_r [constructor, in label]
LIS_ifb_l [constructor, in label]
LIS_ifb_cond [constructor, in label]
LIS_ass [constructor, in label]
LIS_skip [constructor, in label]


M

many [definition, in parser]
many_helper [definition, in parser]
maydef_prog_single [lemma, in set_deps]
maydef_flat [lemma, in set_deps]
maydef_prog_seq [lemma, in set_deps]
maydef_stmt_equation [lemma, in set_deps]
maydef_prog_equation [lemma, in set_deps]
maydef_stmt [definition, in set_deps]
maydef_prog [definition, in set_deps]
mayread_prog_single [lemma, in set_deps]
mayread_flat [lemma, in set_deps]
mayread_prog_seq [lemma, in set_deps]
mayread_stmt_equation [lemma, in set_deps]
mayread_prog_equation [lemma, in set_deps]
mayread_stmt [definition, in set_deps]
mayread_prog [definition, in set_deps]
mayread_prog_keep_L_affected [lemma, in semantics3]
mustdef_prog_single [lemma, in set_deps]
mustdef_prog_exists_maydef [lemma, in set_deps]
mustdef_prog_not_flat [lemma, in set_deps]
mustdef_prog_seq [lemma, in set_deps]
mustdef_stmt_equation [lemma, in set_deps]
mustdef_prog_equation [lemma, in set_deps]
mustdef_stmt [definition, in set_deps]
mustdef_prog [definition, in set_deps]
mustdef_prog_quotient [lemma, in semantics3]


N

negb_filter_list [lemma, in data]
NoneE [constructor, in parser]
not_id_inR_bexp_update_same_beval [lemma, in semantics3]
not_id_inR_aexp_update_same_aeval [lemma, in semantics3]
not_or_iff [lemma, in decidable]
not_and_iff [lemma, in decidable]
no_repeat_bound [lemma, in set_relation]
no_repeat_bound_aux [lemma, in set_relation]
nth_not_default [lemma, in set_relation]
num_lab_stmt_lt [lemma, in label]
num_lab_app [lemma, in label]
num_lab_stmt [definition, in label]
num_lab_prog [definition, in label]


O

optionE [inductive, in parser]
option_proj [definition, in proj_vs_traj]
other [constructor, in parser]
others [section, in set2]


P

pair [section, in set2]
pair_proj [definition, in proj_vs_traj]
parenthese [constructor, in parser]
parse [definition, in parser]
parseAExp [definition, in parser]
parseAtomicExp [definition, in parser]
parseBExp [definition, in parser]
parseConjunctionExp [definition, in parser]
parseIdentifier [definition, in parser]
parseLabel [definition, in parser]
parseNumber [definition, in parser]
parsePrimaryExp [definition, in parser]
parseProductExp [definition, in parser]
parseProg [definition, in parser]
parser [definition, in parser]
parser [library]
parseSequencedCommand [definition, in parser]
parseSimpleCommand [definition, in parser]
parseSumExp [definition, in parser]
parse_finished [definition, in parser]
partial_state_proj [definition, in semantics3]
partial_traj [definition, in semantics3]
partial_state_eps [definition, in semantics3]
partial_state [definition, in semantics3]
power [definition, in parser]
PP_after [constructor, in prefix]
PP_nil [constructor, in prefix]
prefix [inductive, in prefix]
prefix [library]
prefix_prog_intro [lemma, in prefix]
prefix_prog_app [lemma, in prefix]
prefix_prog_single [lemma, in prefix]
prefix_prog_trans [lemma, in prefix]
prefix_prog_irrefl [lemma, in prefix]
prefix_prog_refl [lemma, in prefix]
prefix_prog [inductive, in prefix]
prefix_single [lemma, in prefix]
prefix_length [lemma, in prefix]
prefix_trans [lemma, in prefix]
prefix_irrefl [lemma, in prefix]
prefix_refl [lemma, in prefix]
prefix_include [lemma, in slice]
prefix_prog_traj2 [lemma, in semantics3]
prefix_saturate [lemma, in semantics3]
prefix_prog_traj [lemma, in semantics3]
prefix_prog_app_same [lemma, in semantics3]
prod [section, in set2]
prog [inductive, in prog]
prog [library]
ProgWithDep [record, in slice]
prog_mutual_rect [definition, in prog]
prog_mutual_ind [definition, in prog]
proj_equal [lemma, in first_results]
proj_equal_bis [lemma, in first_results]
proj_prefix [lemma, in first_results]
proj_traj_prog_none_in [lemma, in slice]
proj_traj_print_prog [definition, in parser]
proj_traj_print [definition, in parser]
proj_traj_prog_three_cases [lemma, in semantics3]
proj_state_update_not_in_L_fun [lemma, in semantics3]
proj_traj_prog_app [lemma, in semantics3]
proj_traj_prog_length [lemma, in semantics3]
proj_traj_prog_prefix [lemma, in semantics3]
proj_traj_prog [definition, in semantics3]
proj_state_eps [definition, in semantics3]
proj_state [definition, in semantics3]
proj_traj_prog_last_set_incl [lemma, in proj_vs_traj]
proj_traj_prog_not_none_set_incl [lemma, in proj_vs_traj]
proj_traj_prog_length_set_incl [lemma, in proj_vs_traj]
proj_traj_prog_map_set_incl [lemma, in proj_vs_traj]
proj_traj_prog_last [lemma, in proj_vs_traj]
proj_traj_prog_not_none [lemma, in proj_vs_traj]
proj_traj_prog_shorter [lemma, in proj_vs_traj]
proj_traj_prog_map [lemma, in proj_vs_traj]
proj_traj_prog_shorter [lemma, in proj_vs_traj]
proj_vs_traj [library]
PR_after [constructor, in prefix]
PR_nil [constructor, in prefix]
PWD_cda [instance, in slice]
PWD_correct [projection, in slice]
PWD_rl [projection, in slice]
PWD_stable [projection, in slice]
PWD_control [projection, in slice]
P_cons [constructor, in prog]
P_nil [constructor, in prog]


Q

quotient [library]


R

relation [section, in set_relation]
relation_set_rel_clos_stable2 [lemma, in set_relation]
relation_set_rel_clos_stable [lemma, in set_relation]
relation_set_rel_clos [lemma, in set_relation]
remove_cycles_nil [lemma, in set_relation]
remove_cycles_stays_sorted [lemma, in set_relation]
remove_cycles_keeps_last [lemma, in set_relation]
remove_cycles_keeps_head [lemma, in set_relation]
remove_cycles_no_repeat [lemma, in set_relation]
remove_cycles_include [lemma, in set_relation]
repeat [inductive, in set_relation]
repeat_include [lemma, in set_relation]
repeat_after [constructor, in set_relation]
repeat_here [constructor, in set_relation]


S

semantics3 [library]
seq [library]
seq_nil_r [lemma, in seq]
seq_nil_l [lemma, in seq]
seq_assoc [lemma, in seq]
set [definition, in set]
set [library]
set_prod_In [lemma, in set2]
set_prod [definition, in set2]
set_rel_clos_refl_trans_inverse_stable2 [lemma, in set_relation]
set_incl_emptyset_l [lemma, in set_relation]
set_rel_clos_relation_stable_iff2 [lemma, in set_relation]
set_rel_clos_relation2 [lemma, in set_relation]
set_refl_trans_inverse_stable [lemma, in set_relation]
set_refl_trans_inverse_correct [lemma, in set_relation]
set_refl_trans_inverse [definition, in set_relation]
set_refl_trans_inverse_aux_correct [lemma, in set_relation]
set_refl_trans_inverse_aux [definition, in set_relation]
set_rel_power_incl [lemma, in set_relation]
set_rel_clos_refl_trans_inverse_stable [lemma, in set_relation]
set_rel_clos_relation_stable_iff [lemma, in set_relation]
set_rel_clos_relation_iff [lemma, in set_relation]
set_rel_carrier_stable [lemma, in set_relation]
set_rel_carrier [lemma, in set_relation]
set_rel_clos_power [lemma, in set_relation]
set_rel_clos_power_aux [lemma, in set_relation]
set_rel_power_size [lemma, in set_relation]
set_rel_add_power [lemma, in set_relation]
set_rel_power_add [lemma, in set_relation]
set_rel_power_size_aux [lemma, in set_relation]
set_list_too_long [lemma, in set_relation]
set_list_rel_power [lemma, in set_relation]
set_rel_power_list [lemma, in set_relation]
set_rel_power_clos_le [lemma, in set_relation]
set_rel_clos_relation [lemma, in set_relation]
set_rel_clos_relation_aux [lemma, in set_relation]
set_rel_power_clos [lemma, in set_relation]
set_inverse_singleton [lemma, in set_relation]
set_inverse_r [lemma, in set_relation]
set_inverse [definition, in set_relation]
set_rel_clos_refl_trans [definition, in set_relation]
set_rel_clos_refl_trans_aux [definition, in set_relation]
set_rel_power [definition, in set_relation]
set_stable [definition, in set_relation]
set_same_In_iff [lemma, in set]
set_same_trans [lemma, in set]
set_same_sym [lemma, in set]
set_same_refl [lemma, in set]
set_diff_In [lemma, in set]
set_diff_union_distr_l [lemma, in set]
set_diff_union_distr_r [lemma, in set]
set_diff_empty [lemma, in set]
set_diff_union [lemma, in set]
set_diff_same [lemma, in set]
set_diff_emptyset_r [lemma, in set]
set_diff_emptyset_l [lemma, in set]
set_incl_union [lemma, in set]
set_diff_incl [lemma, in set]
set_same_bound_1_singleton [lemma, in set]
set_singleton_In [lemma, in set]
set_test_empty_complete [lemma, in set]
set_test_empty_correct [lemma, in set]
set_same_union_add_singleton [lemma, in set]
set_inter_same [lemma, in set]
set_incl_inter [lemma, in set]
set_inter_incl [lemma, in set]
set_inter_comm [lemma, in set]
set_union_comm [lemma, in set]
set_union_assoc [lemma, in set]
set_inter_In [lemma, in set]
set_union_In [lemma, in set]
set_inter_union_distr_l [lemma, in set]
set_same_union_empty_r [lemma, in set]
set_same_union_empty_l [lemma, in set]
set_inter_mem_singleton [lemma, in set]
set_inter_not_mem_empty [lemma, in set]
set_incl_trans [lemma, in set]
set_incl_refl [lemma, in set]
set_singleton [definition, in set]
set_same [definition, in set]
set_incl [definition, in set]
set_map_In [lemma, in set]
set_map [definition, in set]
set_size_In_remove [lemma, in set]
set_size_In_remove [lemma, in set]
set_size_not_In_remove [lemma, in set]
set_size_not_In_remove [lemma, in set]
set_size_not_In_remove_aux [lemma, in set]
set_size_ge_1_In [lemma, in set]
set_size_1_singleton [lemma, in set]
set_remove_not_In [lemma, in set]
set_size_0_empty [lemma, in set]
set_size_le_set_bound [lemma, in set]
set_bound_1_singleton [lemma, in set]
set_bound_0_empty [lemma, in set]
set_filter_In [lemma, in set]
set_empty_not_In [lemma, in set]
set_not_empty_In [lemma, in set]
set_remove_decrease [lemma, in set]
set_size_bound [definition, in set]
set_filter [definition, in set]
set_test_empty [definition, in set]
set_remove [definition, in set]
set_diff_trivial [lemma, in set]
set_diff_elim2 [lemma, in set]
set_diff_elim1 [lemma, in set]
set_diff_intro [lemma, in set]
set_inter_elim [lemma, in set]
set_inter_elim2 [lemma, in set]
set_inter_elim1 [lemma, in set]
set_inter_intro [lemma, in set]
set_union_emptyR [lemma, in set]
set_union_emptyL [lemma, in set]
set_union_elim [lemma, in set]
set_union_intro [lemma, in set]
set_union_intro2 [lemma, in set]
set_union_intro1 [lemma, in set]
set_add_not_empty [lemma, in set]
set_add_elim2 [lemma, in set]
set_add_elim [lemma, in set]
set_add_intro [lemma, in set]
set_add_intro2 [lemma, in set]
set_add_intro1 [lemma, in set]
set_mem_complete_iff [lemma, in set]
set_mem_correct_iff [lemma, in set]
set_mem_complete2 [lemma, in set]
set_mem_complete1 [lemma, in set]
set_mem_correct2 [lemma, in set]
set_mem_correct1 [lemma, in set]
set_mem_ind2 [lemma, in set]
set_mem_ind [lemma, in set]
set_In_dec [lemma, in set]
set_In [definition, in set]
set_diff [definition, in set]
set_union [definition, in set]
set_inter [definition, in set]
set_mem [definition, in set]
set_add [definition, in set]
set_assert_prog_correct [lemma, in assert]
set_assert_stmt [definition, in assert]
set_assert_prog [definition, in assert]
set_of_id_stmt [definition, in set_prog]
set_of_id_prog [definition, in set_prog]
set_of_id_bexp_correct [lemma, in set_prog]
set_of_id_aexp_correct [lemma, in set_prog]
set_of_id_bexp [definition, in set_prog]
set_of_id_aexp [definition, in set_prog]
set_of_labels_prog_seq [lemma, in set_prog]
set_of_labels_stmt [definition, in set_prog]
set_of_labels_prog [definition, in set_prog]
set_slice_stable [lemma, in slice]
set_slice_include [lemma, in slice]
set_slice_correct [lemma, in slice]
set_slice [definition, in slice]
set_data_prog_correct [lemma, in set_deps]
set_data_prog_seq [lemma, in set_deps]
set_data_stmt_equation [lemma, in set_deps]
set_data_prog_equation [lemma, in set_deps]
set_data_stmt [definition, in set_deps]
set_data_prog [definition, in set_deps]
set_def [definition, in set_deps]
set_ref [definition, in set_deps]
set_of_labels_prog_empty_nil [lemma, in semantics3]
set_control_prog_correct [lemma, in control]
set_control_stmt [definition, in control]
set_control_prog [definition, in control]
set_label_first_prog_correct [lemma, in control]
set_label_first_prog [definition, in control]
set_stable_clos [lemma, in control]
set_prog [library]
set_relation [library]
set_deps [library]
set_instance [library]
set2 [library]
set2_inner_fst_diff_lr [lemma, in set2]
set2_inner_fst_union_distr_r [lemma, in set2]
set2_inner_fst_union_distr_l [lemma, in set2]
set2_inner_fst_emptyset_l [lemma, in set2]
set2_inner_fst_In [lemma, in set2]
set2_inner_fst [definition, in set2]
set2_diff_fst_twice [lemma, in set2]
set2_diff_fst_emptyset_r [lemma, in set2]
set2_diff_fst_emptyset_l [lemma, in set2]
set2_diff_fst_inter_distr_r [lemma, in set2]
set2_diff_fst_inter_distr_l [lemma, in set2]
set2_diff_fst_union_distr_r [lemma, in set2]
set2_diff_fst_union_distr_l [lemma, in set2]
set2_diff_snd_In [lemma, in set2]
set2_diff_fst_In [lemma, in set2]
set2_diff_snd [definition, in set2]
set2_diff_fst [definition, in set2]
set2_inter_snd_In [lemma, in set2]
set2_inter_fst_In [lemma, in set2]
set2_inter_snd [definition, in set2]
set2_inter_fst [definition, in set2]
sflib [library]
SIAI_ass [constructor, in data]
SIA_ass [constructor, in data]
SIP_after [constructor, in data]
SIP_here [constructor, in data]
slice [definition, in slice]
slice [library]
slice_error_classical [lemma, in slice]
slice_error [lemma, in slice]
slice_no_error [lemma, in slice]
slice_no_error_ste [lemma, in slice]
slice_proj_equal [lemma, in slice]
slice_proj_prefix [lemma, in slice]
slice_label [lemma, in slice]
slice_quotient [lemma, in slice]
SomeE [constructor, in parser]
sorted_firstn [lemma, in set_relation]
sorted_fun_ext [lemma, in set_relation]
sorted_combine [lemma, in set_relation]
stable_inclusion_stable [lemma, in semantics3]
state [definition, in semantics3]
state_eps [definition, in semantics3]
stmt [inductive, in prog]
stmt_mutual_rect [definition, in prog]
stmt_mutual_ind [definition, in prog]
stmt_inR_prog [inductive, in data]
stmt_is_ass_id_correct [lemma, in data]
stmt_is_ass_id [definition, in data]
stmt_is_assR_id_dec [lemma, in data]
stmt_is_assR_dec [lemma, in data]
stmt_is_assR_id [inductive, in data]
stmt_is_assR [inductive, in data]
stmt_get_label_in_stmt [lemma, in label]
stmt_get_label [definition, in label]
stmt_get_label_is_quotientR_stmt [lemma, in semantics3]
stmt_is_assR_id_in [lemma, in semantics3]
string_of_stmt [definition, in parser]
string_of_prog [definition, in parser]
string_of_stmt_aux [definition, in parser]
string_of_prog_aux' [definition, in parser]
string_of_prog_aux [definition, in parser]
string_of_bexp [definition, in parser]
string_of_aexp [definition, in parser]
string_of_id [definition, in parser]
string_of_nat [definition, in parser]
string_of_list [definition, in parser]
S_assert [constructor, in prog]
S_while [constructor, in prog]
S_if [constructor, in prog]
S_ass [constructor, in prog]
S_skip [constructor, in prog]


T

test [section, in set_relation]
theorems [section, in set]
token [definition, in parser]
tokenize [definition, in parser]
tokenize_helper [definition, in parser]
traj [definition, in semantics3]
traj_print_prog [definition, in parser]
traj_print [definition, in parser]
traj_prog_none_end [lemma, in semantics3]
traj_prog_not_none_iff [lemma, in semantics3]
traj_prog_not_none [lemma, in semantics3]
traj_prog_is_flatR_of [lemma, in semantics3]
traj_prog_three_cases [lemma, in semantics3]
traj_prog_app_last_none [lemma, in semantics3]
traj_prog_app_saturate [lemma, in semantics3]
traj_prog_app [lemma, in semantics3]
traj_prog_length_not_reached [lemma, in semantics3]
traj_prog_less_than_length [lemma, in semantics3]
traj_prog_prefix [lemma, in semantics3]
traj_prog_length [lemma, in semantics3]
traj_prog [definition, in semantics3]
traj_prog_label_in [lemma, in proj_vs_traj]
trans_control_depsR_label_inR_prog [lemma, in control]


U

unfold_while_prog_is_flatR [lemma, in data]
unfold_while_stmt [definition, in data]
unfold_while_prog [definition, in data]
update [definition, in semantics3]
update_permute_fun [lemma, in semantics3]
update_shadow_fun [lemma, in semantics3]
update_permute [lemma, in semantics3]
update_same [lemma, in semantics3]
update_shadow [lemma, in semantics3]
update_neq [lemma, in semantics3]
update_eq [lemma, in semantics3]


W

while_not_preserved_stable_not_preserved [lemma, in semantics3]
white [constructor, in parser]


other

_ +;+ _ [notation, in prog]
_ ;; _ [notation, in prog]
_ ::= _ << _ >> [notation, in prog]
_ ⊆ _ [notation, in set]
_ \subseteq _ [notation, in set]
_ ≡ _ [notation, in set]
_ \equiv _ [notation, in set]
_ ⊕ _ [notation, in set]
_ \oplus _ [notation, in set]
_ ∈? _ [notation, in set]
_ \in? _ [notation, in set]
_ ∈ _ [notation, in set]
_ \in _ [notation, in set]
_ \ _ [notation, in set]
_ ∩ _ [notation, in set]
_ \cap _ [notation, in set]
_ ∪ _ [notation, in set]
_ \cup _ [notation, in set]
ASSERT << _ >> _ =>> _ [notation, in prog]
DO ( _ , _ ) <-- _ ; _ OR _ [notation, in parser]
DO ( _ , _ ) <== _ ; _ [notation, in parser]
IFB << _ >> _ THEN _ ELSE _ FI [notation, in prog]
SKIP << _ >> [notation, in prog]
WHILE << _ >> _ DO _ END [notation, in prog]
\emptyset [notation, in set]
\sin _ [notation, in set]
{{ _ ; .. ; _ }} [notation, in prog]
{{ }} [notation, in prog]
∅ [notation, in set]
〈 _ 〉 [notation, in set]


Notation Index

other

_ +;+ _ [in prog]
_ ;; _ [in prog]
_ ::= _ << _ >> [in prog]
_ ⊆ _ [in set]
_ \subseteq _ [in set]
_ ≡ _ [in set]
_ \equiv _ [in set]
_ ⊕ _ [in set]
_ \oplus _ [in set]
_ ∈? _ [in set]
_ \in? _ [in set]
_ ∈ _ [in set]
_ \in _ [in set]
_ \ _ [in set]
_ ∩ _ [in set]
_ \cap _ [in set]
_ ∪ _ [in set]
_ \cup _ [in set]
ASSERT << _ >> _ =>> _ [in prog]
DO ( _ , _ ) <-- _ ; _ OR _ [in parser]
DO ( _ , _ ) <== _ ; _ [in parser]
IFB << _ >> _ THEN _ ELSE _ FI [in prog]
SKIP << _ >> [in prog]
WHILE << _ >> _ DO _ END [in prog]
\emptyset [in set]
\sin _ [in set]
{{ _ ; .. ; _ }} [in prog]
{{ }} [in prog]
∅ [in set]
〈 _ 〉 [in set]


Library Index

A

assert


C

control


D

data
decidable


F

first_results


L

label
last
last_state
last_f


P

parser
prefix
prog
proj_vs_traj


Q

quotient


S

semantics3
seq
set
set_prog
set_relation
set_deps
set_instance
set2
sflib
slice


Lemma Index

A

affected_prog_In [in semantics3]
and_or_distr_l [in decidable]
ante_diff_emptyset_l [in set_relation]
ante_diff_In [in set_relation]
app_prog_cons [in seq]
app_prog_list_nil_r [in data]
app_prog_list_app_r [in data]
assert_depsR_prog_dec [in assert]
assert_depsR_prog_stable [in assert]
assert_depsR_prog_label_inR_prog [in assert]
assert_depsR_prog_stable_app [in semantics3]
assert_depsR_prog_stable_cons [in semantics3]
assert_depsR_prog_stable_after [in semantics3]
ass_inR_prog_dec [in data]
ass_inR_prog_seq [in set_deps]
ass_not_preserved_proj_equal_ok [in semantics3]
ass_not_preserved_mayread [in semantics3]
ass_not_inR_prog_is_flat_of [in semantics3]
ass_inR_prog_single [in semantics3]
ass_inR_prog_app [in semantics3]
ass_not_preserved_proj_equal [in semantics3]
aux5_correct [in set_relation]
aux5_grow [in set_relation]
aux5_incl_res [in set_relation]
aux5_equation_S [in set_relation]


C

cons_prog_list_app [in data]
cons_prog_list_nil [in data]
control_depsR_prog_stable_app [in semantics3]
control_depsR_prog_stable_cons_reverse [in semantics3]
control_depsR_prog_stable_cons [in semantics3]
control_depsR_prog_stable_unrel [in semantics3]
control_depsR_prog_stable_quotient [in semantics3]
control_depsR_prog_quotient_include [in semantics3]
control_depsR_prog_stable [in control]
control_depsR_label_inR_prog [in control]
control_stmt_get_label [in control]
control_ifb [in control]


D

data_deps_prog_correct [in data]
data_depsR_prog_after [in data]
data_depsR_prog_here [in data]
data_depsR_prog_stable [in data]
data_depsR_label_inR_prog [in data]
data_depsR_prog_stable_after [in semantics3]
data_depsR_prog_stable_unrel [in semantics3]
data_depsR_prog_unrel [in semantics3]
dec_is_decidable [in decidable]


E

eq_id_dec [in prog]


F

filter_length [in proj_vs_traj]
find_last_nil [in set_relation]
find_last_keeps_last [in set_relation]
find_last_keeps_head [in set_relation]
find_last_stays_sorted [in set_relation]
find_last_include [in set_relation]
find_last_decrease [in set_relation]
firstn_full [in set_relation]
firstn_incl [in set_relation]
first_true_if [in set_relation]
first_true [in set_relation]
first_false_forall [in set_relation]
first_false [in set_relation]
flat_list_prog_single [in data]
flat_data_depsR_prog_decomposition [in data]
flat_data_depsR_prog_grow_m [in data]
flat_data_depsR_prog_unrel [in data]
flat_data_deps_prog_complete [in data]
flat_data_deps_prog_correct [in data]
flat_list_prog_correct [in data]
flat_data_depsR_prog_grow_r [in data]
flat_data_depsR_prog_grow_l [in data]
flat_l_stmt_correct [in data]
flat_l_prog_correct [in data]
flat_data_depsR_label_inR_prog [in data]
flat_l_prog_label [in semantics3]
flat_data_depsR_prog_app_unrel [in semantics3]
flat_data_depsR_prog_stable_prefix [in semantics3]
flat_data_depsR_prog_prefix [in semantics3]
flat_state_prog_proj_traj [in semantics3]
flat_data_depsR_prog_stable_unrel [in semantics3]
flat_data_depsR_prog_stable_after [in semantics3]
flat_data_depsR_prog_unrel [in semantics3]
flat_state_prog_prefix_is_flatR_of [in semantics3]
flat_state_prog_prefix [in semantics3]
flat_state_prog_traj_length [in semantics3]
flat_state_prog_is_flatR_of_if_terminating_no_error [in semantics3]
flat_state_prog_num_lab [in semantics3]
flat_state_prog_traj [in semantics3]
flat_state_prog_is_flatR [in semantics3]
forall_fun_ext [in set_relation]
forall_firstn [in set_relation]
forall_sorted_firstn [in set_relation]
forall_sorted [in set_relation]
forall_filter [in proj_vs_traj]


H

hdrel_firstn [in set_relation]
hdrel_fun_ext [in set_relation]


I

id_inR_ref_prog_stmt_inR_prog [in data]
id_in_ref_correct [in data]
id_in_bexp_correct [in data]
id_in_aexp_correct [in data]
id_not_in_mayread_prog_update [in semantics3]
ifb_not_preserved_stable_not_preserved_r [in semantics3]
ifb_not_preserved_stable_not_preserved_l [in semantics3]
include_forall [in set_relation]
include_incl [in set_relation]
include_appears_in [in set_relation]
include_nil_l [in set_relation]
include_trans [in set_relation]
include_refl [in set_relation]
include_rt [in control]
index_proj_bounded [in first_results]
inverse_r [in set_relation]
in_flat_list_prog_seq [in data]
in_app_prog_list [in data]
in_cons_prog_list [in data]
is_quotientR_prog_single [in quotient]
is_quotientR_in_seq [in quotient]
is_quotientR_trans [in quotient]
is_quotientR_antisym [in quotient]
is_quotientR_prog_same_num [in quotient]
is_quotientR_stmt_num_lab [in quotient]
is_quotientR_prog_num_lab [in quotient]
is_quotientR_refl [in quotient]
Is_true_eq_true_iff [in set_relation]
is_flatR_of_prog_intro [in data]
is_flatR_of_prog_self [in data]
is_flatR_of_prog_is_flatR [in data]
is_flatR_prog_app [in data]
is_quotientR_prog_nil_r [in data]
is_flatR_of_prog_cut [in data]
is_quotientR_prog_is_flatR [in data]
is_flatR_prog_single [in data]
is_flatR_of_prog_single [in data]
is_flatR_of_prog_label [in data]
is_flatR_of_prog_set_data_incl [in set_deps]
is_flatR_stmt_maydef [in set_deps]
is_flatR_stmt_mayread [in set_deps]
is_flatR_stmt_mustdef [in set_deps]
is_flatR_prog_mustdef [in set_deps]
is_flatR_of_prog_mayread_incl [in set_deps]
is_flatR_of_prog_maydef_incl [in set_deps]
is_flatR_of_prog_mustdef_incl [in set_deps]
is_flatR_prog_app_reverse [in set_deps]
is_flatR_prog_is_flatR_of_same [in set_deps]
is_bounded_flatR_of_prog_is_flatR_of [in set_deps]
is_flatR_stmt_num_lab [in semantics3]
is_flatR_prog_unrel [in semantics3]
is_flatR_prog_no_control [in semantics3]
is_flatR_prog_proj_traj_keep_L_prefix [in semantics3]
is_flatR_prog_num_lab_not_reached [in semantics3]
is_flatR_prog_traj_length [in semantics3]
is_flatR_of_prog_one_step [in semantics3]


K

keep_L_prog_involutive_quotient [in semantics3]
keep_L_stmt_quotient [in semantics3]
keep_L_prog_flat_reverse [in semantics3]
keep_L_prog_app_bis_reverse [in semantics3]
keep_L_prog_app_reverse [in semantics3]
keep_L_prog_cons_reverse [in semantics3]
keep_L_prog_flat [in semantics3]
keep_L_prog_nil_flat_nil [in semantics3]
keep_L_prog_app [in semantics3]
keep_L_prog_label [in control]
keep_L_prog_quotient [in control]


L

label_inR_prog_iff_in_set_of_labels [in set_prog]
label_inR_prog_seq [in label]
label_first_label_inR_prog [in label]
label_inR_prog_dec [in label]
label_in_prog_correct [in label]
label_in_prog_iff_in_list_of_labels [in label]
label_in_app [in label]
label_first_inR_prog_quotient_include [in semantics3]
last_state_map [in last_state]
last_state_is_map [in last_state]
last_f_not_empty_In [in last_state]
last_state_cons_change_default [in last_state]
last_state_not_empty [in last_state]
last_state_not_default [in last_state]
last_state_app_not_nil [in last_state]
last_last_cons_not_nil [in last_state]
last_f_map [in last_f]
last_f_is_map [in last_f]
last_f_not_empty_In [in last_f]
last_f_cons_change_default [in last_f]
last_f_not_empty [in last_f]
last_f_not_default [in last_f]
last_f_app_not_nil [in last_f]
last_f_cons_not_nil [in last_f]
last_filter [in last]
last_firstn [in last]
last_map [in last]
last_not_empty_In [in last]
last_cons_change_default [in last]
last_not_empty [in last]
last_not_default [in last]
last_app_not_nil [in last]
last_cons_not_nil [in last]
last_last_f [in last]


M

maydef_prog_single [in set_deps]
maydef_flat [in set_deps]
maydef_prog_seq [in set_deps]
maydef_stmt_equation [in set_deps]
maydef_prog_equation [in set_deps]
mayread_prog_single [in set_deps]
mayread_flat [in set_deps]
mayread_prog_seq [in set_deps]
mayread_stmt_equation [in set_deps]
mayread_prog_equation [in set_deps]
mayread_prog_keep_L_affected [in semantics3]
mustdef_prog_single [in set_deps]
mustdef_prog_exists_maydef [in set_deps]
mustdef_prog_not_flat [in set_deps]
mustdef_prog_seq [in set_deps]
mustdef_stmt_equation [in set_deps]
mustdef_prog_equation [in set_deps]
mustdef_prog_quotient [in semantics3]


N

negb_filter_list [in data]
not_id_inR_bexp_update_same_beval [in semantics3]
not_id_inR_aexp_update_same_aeval [in semantics3]
not_or_iff [in decidable]
not_and_iff [in decidable]
no_repeat_bound [in set_relation]
no_repeat_bound_aux [in set_relation]
nth_not_default [in set_relation]
num_lab_stmt_lt [in label]
num_lab_app [in label]


P

prefix_prog_intro [in prefix]
prefix_prog_app [in prefix]
prefix_prog_single [in prefix]
prefix_prog_trans [in prefix]
prefix_prog_irrefl [in prefix]
prefix_prog_refl [in prefix]
prefix_single [in prefix]
prefix_length [in prefix]
prefix_trans [in prefix]
prefix_irrefl [in prefix]
prefix_refl [in prefix]
prefix_include [in slice]
prefix_prog_traj2 [in semantics3]
prefix_saturate [in semantics3]
prefix_prog_traj [in semantics3]
prefix_prog_app_same [in semantics3]
proj_equal [in first_results]
proj_equal_bis [in first_results]
proj_prefix [in first_results]
proj_traj_prog_none_in [in slice]
proj_traj_prog_three_cases [in semantics3]
proj_state_update_not_in_L_fun [in semantics3]
proj_traj_prog_app [in semantics3]
proj_traj_prog_length [in semantics3]
proj_traj_prog_prefix [in semantics3]
proj_traj_prog_last_set_incl [in proj_vs_traj]
proj_traj_prog_not_none_set_incl [in proj_vs_traj]
proj_traj_prog_length_set_incl [in proj_vs_traj]
proj_traj_prog_map_set_incl [in proj_vs_traj]
proj_traj_prog_last [in proj_vs_traj]
proj_traj_prog_not_none [in proj_vs_traj]
proj_traj_prog_shorter [in proj_vs_traj]
proj_traj_prog_map [in proj_vs_traj]
proj_traj_prog_shorter [in proj_vs_traj]


R

relation_set_rel_clos_stable2 [in set_relation]
relation_set_rel_clos_stable [in set_relation]
relation_set_rel_clos [in set_relation]
remove_cycles_nil [in set_relation]
remove_cycles_stays_sorted [in set_relation]
remove_cycles_keeps_last [in set_relation]
remove_cycles_keeps_head [in set_relation]
remove_cycles_no_repeat [in set_relation]
remove_cycles_include [in set_relation]
repeat_include [in set_relation]


S

seq_nil_r [in seq]
seq_nil_l [in seq]
seq_assoc [in seq]
set_prod_In [in set2]
set_rel_clos_refl_trans_inverse_stable2 [in set_relation]
set_incl_emptyset_l [in set_relation]
set_rel_clos_relation_stable_iff2 [in set_relation]
set_rel_clos_relation2 [in set_relation]
set_refl_trans_inverse_stable [in set_relation]
set_refl_trans_inverse_correct [in set_relation]
set_refl_trans_inverse_aux_correct [in set_relation]
set_rel_power_incl [in set_relation]
set_rel_clos_refl_trans_inverse_stable [in set_relation]
set_rel_clos_relation_stable_iff [in set_relation]
set_rel_clos_relation_iff [in set_relation]
set_rel_carrier_stable [in set_relation]
set_rel_carrier [in set_relation]
set_rel_clos_power [in set_relation]
set_rel_clos_power_aux [in set_relation]
set_rel_power_size [in set_relation]
set_rel_add_power [in set_relation]
set_rel_power_add [in set_relation]
set_rel_power_size_aux [in set_relation]
set_list_too_long [in set_relation]
set_list_rel_power [in set_relation]
set_rel_power_list [in set_relation]
set_rel_power_clos_le [in set_relation]
set_rel_clos_relation [in set_relation]
set_rel_clos_relation_aux [in set_relation]
set_rel_power_clos [in set_relation]
set_inverse_singleton [in set_relation]
set_inverse_r [in set_relation]
set_same_In_iff [in set]
set_same_trans [in set]
set_same_sym [in set]
set_same_refl [in set]
set_diff_In [in set]
set_diff_union_distr_l [in set]
set_diff_union_distr_r [in set]
set_diff_empty [in set]
set_diff_union [in set]
set_diff_same [in set]
set_diff_emptyset_r [in set]
set_diff_emptyset_l [in set]
set_incl_union [in set]
set_diff_incl [in set]
set_same_bound_1_singleton [in set]
set_singleton_In [in set]
set_test_empty_complete [in set]
set_test_empty_correct [in set]
set_same_union_add_singleton [in set]
set_inter_same [in set]
set_incl_inter [in set]
set_inter_incl [in set]
set_inter_comm [in set]
set_union_comm [in set]
set_union_assoc [in set]
set_inter_In [in set]
set_union_In [in set]
set_inter_union_distr_l [in set]
set_same_union_empty_r [in set]
set_same_union_empty_l [in set]
set_inter_mem_singleton [in set]
set_inter_not_mem_empty [in set]
set_incl_trans [in set]
set_incl_refl [in set]
set_map_In [in set]
set_size_In_remove [in set]
set_size_In_remove [in set]
set_size_not_In_remove [in set]
set_size_not_In_remove [in set]
set_size_not_In_remove_aux [in set]
set_size_ge_1_In [in set]
set_size_1_singleton [in set]
set_remove_not_In [in set]
set_size_0_empty [in set]
set_size_le_set_bound [in set]
set_bound_1_singleton [in set]
set_bound_0_empty [in set]
set_filter_In [in set]
set_empty_not_In [in set]
set_not_empty_In [in set]
set_remove_decrease [in set]
set_diff_trivial [in set]
set_diff_elim2 [in set]
set_diff_elim1 [in set]
set_diff_intro [in set]
set_inter_elim [in set]
set_inter_elim2 [in set]
set_inter_elim1 [in set]
set_inter_intro [in set]
set_union_emptyR [in set]
set_union_emptyL [in set]
set_union_elim [in set]
set_union_intro [in set]
set_union_intro2 [in set]
set_union_intro1 [in set]
set_add_not_empty [in set]
set_add_elim2 [in set]
set_add_elim [in set]
set_add_intro [in set]
set_add_intro2 [in set]
set_add_intro1 [in set]
set_mem_complete_iff [in set]
set_mem_correct_iff [in set]
set_mem_complete2 [in set]
set_mem_complete1 [in set]
set_mem_correct2 [in set]
set_mem_correct1 [in set]
set_mem_ind2 [in set]
set_mem_ind [in set]
set_In_dec [in set]
set_assert_prog_correct [in assert]
set_of_id_bexp_correct [in set_prog]
set_of_id_aexp_correct [in set_prog]
set_of_labels_prog_seq [in set_prog]
set_slice_stable [in slice]
set_slice_include [in slice]
set_slice_correct [in slice]
set_data_prog_correct [in set_deps]
set_data_prog_seq [in set_deps]
set_data_stmt_equation [in set_deps]
set_data_prog_equation [in set_deps]
set_of_labels_prog_empty_nil [in semantics3]
set_control_prog_correct [in control]
set_label_first_prog_correct [in control]
set_stable_clos [in control]
set2_inner_fst_diff_lr [in set2]
set2_inner_fst_union_distr_r [in set2]
set2_inner_fst_union_distr_l [in set2]
set2_inner_fst_emptyset_l [in set2]
set2_inner_fst_In [in set2]
set2_diff_fst_twice [in set2]
set2_diff_fst_emptyset_r [in set2]
set2_diff_fst_emptyset_l [in set2]
set2_diff_fst_inter_distr_r [in set2]
set2_diff_fst_inter_distr_l [in set2]
set2_diff_fst_union_distr_r [in set2]
set2_diff_fst_union_distr_l [in set2]
set2_diff_snd_In [in set2]
set2_diff_fst_In [in set2]
set2_inter_snd_In [in set2]
set2_inter_fst_In [in set2]
slice_error_classical [in slice]
slice_error [in slice]
slice_no_error [in slice]
slice_no_error_ste [in slice]
slice_proj_equal [in slice]
slice_proj_prefix [in slice]
slice_label [in slice]
slice_quotient [in slice]
sorted_firstn [in set_relation]
sorted_fun_ext [in set_relation]
sorted_combine [in set_relation]
stable_inclusion_stable [in semantics3]
stmt_is_ass_id_correct [in data]
stmt_is_assR_id_dec [in data]
stmt_is_assR_dec [in data]
stmt_get_label_in_stmt [in label]
stmt_get_label_is_quotientR_stmt [in semantics3]
stmt_is_assR_id_in [in semantics3]


T

traj_prog_none_end [in semantics3]
traj_prog_not_none_iff [in semantics3]
traj_prog_not_none [in semantics3]
traj_prog_is_flatR_of [in semantics3]
traj_prog_three_cases [in semantics3]
traj_prog_app_last_none [in semantics3]
traj_prog_app_saturate [in semantics3]
traj_prog_app [in semantics3]
traj_prog_length_not_reached [in semantics3]
traj_prog_less_than_length [in semantics3]
traj_prog_prefix [in semantics3]
traj_prog_length [in semantics3]
traj_prog_label_in [in proj_vs_traj]
trans_control_depsR_label_inR_prog [in control]


U

unfold_while_prog_is_flatR [in data]
update_permute_fun [in semantics3]
update_shadow_fun [in semantics3]
update_permute [in semantics3]
update_same [in semantics3]
update_shadow [in semantics3]
update_neq [in semantics3]
update_eq [in semantics3]


W

while_not_preserved_stable_not_preserved [in semantics3]


Constructor Index

A

ADP_after [in assert]
ADP_here [in assert]
ADS_assert [in assert]
ADS_while [in assert]
ADS_ifb_r [in assert]
ADS_ifb_l [in assert]
AIP_after [in data]
AIP_here [in data]
AIS_while [in data]
AIS_ifb_r [in data]
AIS_ifb_l [in data]
AIS_ass [in data]
alpha [in parser]
A_mult [in prog]
A_minus [in prog]
A_plus [in prog]
A_id [in prog]
A_num [in prog]


B

B_and [in prog]
B_not [in prog]
B_le [in prog]
B_eq [in prog]
B_false [in prog]
B_true [in prog]


C

CDP_after [in control]
CDP_here [in control]
CDS_while_cond [in control]
CDS_while [in control]
CDS_ifb_cond_r [in control]
CDS_ifb_cond_l [in control]
CDS_ifb_r [in control]
CDS_ifb_l [in control]


D

DDP_flat [in data]
digit [in parser]


F

FDP_after [in data]
FDP_unrel [in data]
FDP_here [in data]


I

IBFOP_cons [in set_deps]
IBFOP_nil [in set_deps]
IBFOS_assert [in set_deps]
IBFOS_while_end [in set_deps]
IBFOS_while_loop [in set_deps]
IBFOS_ifb_r [in set_deps]
IBFOS_ifb_l [in set_deps]
IBFOS_ass [in set_deps]
IBFOS_skip [in set_deps]
Id [in prog]
IFOP_cons [in data]
IFOP_nil [in data]
IFOS_assert [in data]
IFOS_while_end [in data]
IFOS_while_loop [in data]
IFOS_ifb_r [in data]
IFOS_ifb_l [in data]
IFOS_ass [in data]
IFOS_skip [in data]
IFP_cons [in data]
IFP_nil [in data]
IFS_assert [in data]
IFS_ass [in data]
IFS_skip [in data]
IIA_mult_r [in prog]
IIA_mult_l [in prog]
IIA_minus_r [in prog]
IIA_minus_l [in prog]
IIA_plus_r [in prog]
IIA_plus_l [in prog]
IIA_id [in prog]
IIB_and_r [in prog]
IIB_and_l [in prog]
IIB_not [in prog]
IIB_le_r [in prog]
IIB_le_l [in prog]
IIB_eq_r [in prog]
IIB_eq_l [in prog]
IIR_after [in data]
IIR_here [in data]
IIR_assert [in data]
IIR_while [in data]
IIR_ifb [in data]
IIR_ass [in data]
include_after [in set_relation]
include_here [in set_relation]
include_nil [in set_relation]
IQP_stmt [in quotient]
IQP_remove [in quotient]
IQP_nil [in quotient]
IQS_assert [in quotient]
IQS_while [in quotient]
IQS_ifb [in quotient]
IQS_ass [in quotient]
IQS_skip [in quotient]


L

LFP_after [in label]
LFP_here [in label]
LIP_after [in label]
LIP_here [in label]
LIS_assert [in label]
LIS_while_body [in label]
LIS_while_cond [in label]
LIS_ifb_r [in label]
LIS_ifb_l [in label]
LIS_ifb_cond [in label]
LIS_ass [in label]
LIS_skip [in label]


N

NoneE [in parser]


O

other [in parser]


P

parenthese [in parser]
PP_after [in prefix]
PP_nil [in prefix]
PR_after [in prefix]
PR_nil [in prefix]
P_cons [in prog]
P_nil [in prog]


R

repeat_after [in set_relation]
repeat_here [in set_relation]


S

SIAI_ass [in data]
SIA_ass [in data]
SIP_after [in data]
SIP_here [in data]
SomeE [in parser]
S_assert [in prog]
S_while [in prog]
S_if [in prog]
S_ass [in prog]
S_skip [in prog]


W

white [in parser]


Inductive Index

A

aexp [in prog]
assert_depsR_stmt [in assert]
assert_depsR_prog [in assert]
ass_inR_stmt [in data]
ass_inR_prog [in data]


B

bexp [in prog]


C

chartype [in parser]
control_depsR_stmt [in control]
control_depsR_prog [in control]


D

data_depsR_prog [in data]


F

flat_data_depsR_prog [in data]


I

id [in prog]
id_inR_bexp [in prog]
id_inR_aexp [in prog]
id_inR_ref_prog [in data]
id_inR_ref [in data]
include [in set_relation]
is_quotientR_stmt [in quotient]
is_quotientR_prog [in quotient]
is_flatR_stmt [in data]
is_flatR_prog [in data]
is_flatR_of_stmt [in data]
is_flatR_of_prog [in data]
is_bounded_flatR_of_stmt [in set_deps]
is_bounded_flatR_of_prog [in set_deps]


L

label_first_inR_prog [in label]
label_inR_stmt [in label]
label_inR_prog [in label]


O

optionE [in parser]


P

prefix [in prefix]
prefix_prog [in prefix]
prog [in prog]


R

repeat [in set_relation]


S

stmt [in prog]
stmt_inR_prog [in data]
stmt_is_assR_id [in data]
stmt_is_assR [in data]


Projection Index

D

DS_decide [in set]


P

PWD_correct [in slice]
PWD_rl [in slice]
PWD_stable [in slice]
PWD_control [in slice]


Section Index

D

definitions [in slice]
DS [in set]
DS_sequel_map [in set]
DS_sequel [in set]


E

equivalence [in set]
equivalence_map [in set]


I

id [in set_prog]


L

label [in set_prog]


O

others [in set2]


P

pair [in set2]
prod [in set2]


R

relation [in set_relation]


T

test [in set_relation]
theorems [in set]


Instance Index

D

DS_pair [in set2]
DS_id [in set_instance]
DS_label [in set_instance]


P

PWD_cda [in slice]


Definition Index

A

aeval [in semantics3]
affected_prog [in semantics3]
ante_diff [in set_relation]
appears_in [in set_relation]
app_prog [in prog]
app_prog_list [in data]
assert_depsR_stmt_mutual_ind [in assert]
assert_depsR_prog_mutual_ind [in assert]
aux5 [in set_relation]


B

beval [in semantics3]
bignumber [in parser]
build_symtable [in parser]


C

classifyChar [in parser]
cons_prog_list [in data]
control_depsR_stmt_mutual_ind [in control]
control_depsR_prog_mutual_ind [in control]


D

data_deps_prog [in data]
digit_of_nat [in parser]


E

empty_set [in set]
empty_state [in semantics3]
enter [in parser]
expect [in parser]


F

find_last [in set_relation]
first [in set_relation]
firstExpect [in parser]
flat_list_stmt [in data]
flat_list_prog [in data]
flat_l_stmt [in data]
flat_l_prog [in data]
flat_state_prog [in semantics3]


G

getLabel [in set_relation]


I

id_in_ref [in data]
id_in_bexp [in data]
id_in_aexp [in data]
index_proj [in first_results]
inverse [in set_relation]
isAlpha [in parser]
isDigit [in parser]
isLowerAlpha [in parser]
isParenthese [in parser]
isWhite [in parser]
is_quotientR_stmt_mutual_ind [in quotient]
is_quotientR_prog_mutual_ind [in quotient]
is_flatR_stmt_mutual_ind [in data]
is_flatR_prog_mutual_ind [in data]
is_flatR_of_stmt_mutual_ind [in data]
is_flatR_of_prog_mutual_ind [in data]
is_bounded_flatR_of_stmt_mutual_ind [in set_deps]
is_bounded_flatR_of_prog_mutual_ind [in set_deps]


K

keep_L_stmt [in control]
keep_L_prog [in control]


L

label [in prog]
label_inR_stmt_mutual_ind [in label]
label_inR_prog_mutual_ind [in label]
label_in [in label]
label_in_stmt [in label]
label_in_prog [in label]
last_state [in last_state]
last_f [in last_f]
list_of_labels_stmt [in label]
list_of_labels_prog [in label]
list_of_string [in parser]


M

many [in parser]
many_helper [in parser]
maydef_stmt [in set_deps]
maydef_prog [in set_deps]
mayread_stmt [in set_deps]
mayread_prog [in set_deps]
mustdef_stmt [in set_deps]
mustdef_prog [in set_deps]


N

num_lab_stmt [in label]
num_lab_prog [in label]


O

option_proj [in proj_vs_traj]


P

pair_proj [in proj_vs_traj]
parse [in parser]
parseAExp [in parser]
parseAtomicExp [in parser]
parseBExp [in parser]
parseConjunctionExp [in parser]
parseIdentifier [in parser]
parseLabel [in parser]
parseNumber [in parser]
parsePrimaryExp [in parser]
parseProductExp [in parser]
parseProg [in parser]
parser [in parser]
parseSequencedCommand [in parser]
parseSimpleCommand [in parser]
parseSumExp [in parser]
parse_finished [in parser]
partial_state_proj [in semantics3]
partial_traj [in semantics3]
partial_state_eps [in semantics3]
partial_state [in semantics3]
power [in parser]
prog_mutual_rect [in prog]
prog_mutual_ind [in prog]
proj_traj_print_prog [in parser]
proj_traj_print [in parser]
proj_traj_prog [in semantics3]
proj_state_eps [in semantics3]
proj_state [in semantics3]


S

set [in set]
set_prod [in set2]
set_refl_trans_inverse [in set_relation]
set_refl_trans_inverse_aux [in set_relation]
set_inverse [in set_relation]
set_rel_clos_refl_trans [in set_relation]
set_rel_clos_refl_trans_aux [in set_relation]
set_rel_power [in set_relation]
set_stable [in set_relation]
set_singleton [in set]
set_same [in set]
set_incl [in set]
set_map [in set]
set_size_bound [in set]
set_filter [in set]
set_test_empty [in set]
set_remove [in set]
set_In [in set]
set_diff [in set]
set_union [in set]
set_inter [in set]
set_mem [in set]
set_add [in set]
set_assert_stmt [in assert]
set_assert_prog [in assert]
set_of_id_stmt [in set_prog]
set_of_id_prog [in set_prog]
set_of_id_bexp [in set_prog]
set_of_id_aexp [in set_prog]
set_of_labels_stmt [in set_prog]
set_of_labels_prog [in set_prog]
set_slice [in slice]
set_data_stmt [in set_deps]
set_data_prog [in set_deps]
set_def [in set_deps]
set_ref [in set_deps]
set_control_stmt [in control]
set_control_prog [in control]
set_label_first_prog [in control]
set2_inner_fst [in set2]
set2_diff_snd [in set2]
set2_diff_fst [in set2]
set2_inter_snd [in set2]
set2_inter_fst [in set2]
slice [in slice]
state [in semantics3]
state_eps [in semantics3]
stmt_mutual_rect [in prog]
stmt_mutual_ind [in prog]
stmt_is_ass_id [in data]
stmt_get_label [in label]
string_of_stmt [in parser]
string_of_prog [in parser]
string_of_stmt_aux [in parser]
string_of_prog_aux' [in parser]
string_of_prog_aux [in parser]
string_of_bexp [in parser]
string_of_aexp [in parser]
string_of_id [in parser]
string_of_nat [in parser]
string_of_list [in parser]


T

token [in parser]
tokenize [in parser]
tokenize_helper [in parser]
traj [in semantics3]
traj_print_prog [in parser]
traj_print [in parser]
traj_prog [in semantics3]


U

unfold_while_stmt [in data]
unfold_while_prog [in data]
update [in semantics3]


Record Index

D

DecidableType [in set]


P

ProgWithDep [in slice]


Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (866 entries)
Notation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (30 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (24 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (451 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (37 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (5 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (4 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (173 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2 entries)
This page has been generated by coqdoc