| 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 |
_ |
(860 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(34 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 |
_ |
(386 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 |
_ |
(106 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 |
_ |
(66 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 |
_ |
(222 entries) |
| Module 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 |
_ |
(32 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 |
_ |
(14 entries) |
Global Index
A
acc_property [axiom, in Lattice]
acc_property [definition, in FiniteSetLat]
acc_property [definition, in FiniteSetLat]
acc_property [lemma, in BoolLat]
acc_property [lemma, in ArrayLat]
acc_property' [lemma, in ArrayLat]
add_set [definition, in FiniteSetLat]
add_set_eq [lemma, in FiniteSetLat]
add_set_monotone [lemma, in FiniteSetLat]
AllConstr [inductive, in analysis2]
AllLattice [library]
analyse [lemma, in extract]
AnalyseResult [inductive, in extract]
analysis [library]
analysis2 [library]
apply [definition, in FiniteSetLat]
apply [definition, in ArrayLat]
applyFunc [definition, in ArrayLat]
apply_bottom [lemma, in ArrayLat]
apply_build_const_TabTree_is_bot [lemma, in TabTree]
apply_build_const_TabTree_is_const [lemma, in TabTree]
apply_eq [lemma, in ArrayLat]
apply_eq_word [lemma, in ArrayLat]
apply_functree [definition, in ArrayLat]
apply_inter_tree [lemma, in ArrayLat]
apply_is_bottom [lemma, in ArrayLat]
apply_join_tree [lemma, in ArrayLat]
apply_modify1 [lemma, in ArrayLat]
apply_modify1' [lemma, in ArrayLat]
apply_modify2 [lemma, in ArrayLat]
apply_modify2' [lemma, in ArrayLat]
apply_modify_set1 [lemma, in FiniteSetLat]
apply_modify_set2 [lemma, in FiniteSetLat]
apply_modify_set_tree [lemma, in TabTree]
apply_modify_set_tree1 [lemma, in TabTree]
apply_modify_tree1 [lemma, in TabTree]
apply_modify_tree2 [lemma, in TabTree]
apply_monotone [lemma, in ArrayLat]
apply_prop_prefix [lemma, in analysis]
apply_prop_tr [lemma, in analysis]
apply_set [definition, in FiniteSetLat]
apply_set_in [lemma, in FiniteSetLat]
apply_set_tree [definition, in TabTree]
apply_set_tree1 [lemma, in TabTree]
apply_subst1 [lemma, in ArrayLat]
apply_subst1' [lemma, in ArrayLat]
apply_subst2 [lemma, in ArrayLat]
apply_subst2' [lemma, in ArrayLat]
apply_subst_leaf1 [lemma, in TabTree]
apply_subst_leaf2 [lemma, in TabTree]
apply_subst_tree1 [lemma, in TabTree]
apply_subst_tree2 [lemma, in TabTree]
apply_tree [definition, in TabTree]
apply_tree [definition, in ArrayLat]
apply_tree_bot [lemma, in ArrayLat]
app_dec [lemma, in analysis]
ArrayLat [library]
ArrayLattice [module, in ArrayLat]
arraylength [constructor, in syntax]
arrayload [constructor, in syntax]
ArrayPoset [module, in ArrayLat]
ArraySetLattice [module, in FiniteSetLat]
arraystore [constructor, in syntax]
B
BC_correctness [lemma, in analysis]
BC_correctness_lemma [lemma, in analysis]
big_bound1 [lemma, in analysis2]
big_bound2 [lemma, in analysis2]
BoolLat [library]
BoolLattice [module, in BoolLat]
BoolPoset [module, in BoolLat]
bool_order [inductive, in BoolLat]
bottom [axiom, in Lattice]
bottom [definition, in FiniteSetLat]
bottom [definition, in FiniteSetLat]
bottom [definition, in BoolLat]
bottom [definition, in ArrayLat]
bottom_cardinal_tree [lemma, in FiniteSetLat]
bottom_is_a_bottom [lemma, in ArrayLat]
bottom_is_a_bottom [lemma, in BoolLat]
bottom_is_a_bottom [axiom, in Lattice]
bottom_is_a_bottom [definition, in FiniteSetLat]
bottom_is_a_bottom [definition, in FiniteSetLat]
bounded_calls [lemma, in analysis2]
bounded_news [lemma, in analysis2]
build_const_TabTree_rec [definition, in TabTree]
C
call [inductive, in analysis2]
call_exist [lemma, in analysis2]
call_is_nb_invoke [lemma, in analysis2]
call_jump1 [lemma, in analysis2]
call_0 [constructor, in analysis2]
call_1 [constructor, in analysis2]
call_2 [constructor, in analysis2]
cardinal [definition, in FiniteSetLat]
cardinal_max [lemma, in FiniteSetLat]
cardinal_monotone [lemma, in FiniteSetLat]
cardinal_tree [definition, in FiniteSetLat]
cardinal_tree_bottom [lemma, in FiniteSetLat]
cardinal_tree_eq [lemma, in FiniteSetLat]
cardinal_tree_inf_pow2 [lemma, in FiniteSetLat]
cardinal_tree_monotone [lemma, in FiniteSetLat]
cardinal_0_in_set [lemma, in FiniteSetLat]
CardMax [definition, in FiniteSetLat]
Class [inductive, in syntax]
ClassName [definition, in syntax]
ClassType [constructor, in syntax]
collect [definition, in collect]
collect [library]
collectBC1 [definition, in extract]
collectBC2 [definition, in extract]
collectedMB_monotones [lemma, in extract]
collectedPred_monotones [lemma, in extract]
collected_BC_monotones [lemma, in extract]
collected_monotones [lemma, in extract]
collected_monotones_BC2 [lemma, in extract]
collected_MutRec_monotones [lemma, in extract]
collectM [definition, in collect]
collectMB [definition, in extract]
collectMutRec [definition, in extract]
collectPred [definition, in extract]
collectRec [definition, in extract]
ComponentType [inductive, in syntax]
conc_tr [inductive, in analysis]
conc_tr0 [constructor, in analysis]
conc_tr1 [constructor, in analysis]
conc_tr_currentState [lemma, in analysis]
Constraint [inductive, in extract]
ConstraintBC [inductive, in extract]
ConstraintMB [inductive, in extract]
ConstraintMutRec [inductive, in extract]
ConstraintPred [inductive, in extract]
ConstrBC [inductive, in analysis]
ConstrMB [inductive, in extract]
ConstrMutRec [definition, in analysis]
ConstrPred [inductive, in analysis]
ConstrRec [inductive, in analysis]
count_new [definition, in analysis2]
count_new_m [definition, in analysis2]
count_new_m_eq [lemma, in analysis2]
count_new_m_eq0 [lemma, in analysis2]
count_new_m_eq0_pc [lemma, in analysis2]
count_new_m_eq_pc [lemma, in analysis2]
count_new_m_eq_word [lemma, in analysis2]
count_new_m_pc [definition, in analysis2]
count_new_m_pc0 [lemma, in analysis2]
count_new_m_pc_case [lemma, in analysis2]
count_new_m_pc_eq [lemma, in analysis2]
count_new_m_pc_is_new [lemma, in analysis2]
count_new_m_pc_le1 [lemma, in analysis2]
count_new_m__0or1 [lemma, in analysis2]
currentState_in_trace [lemma, in analysis]
C1 [constructor, in extract]
C2 [constructor, in extract]
C4 [constructor, in extract]
C5 [constructor, in extract]
C6 [constructor, in extract]
C7 [constructor, in extract]
D
definedFields [definition, in syntax]
definedFields_eq_word [lemma, in syntax]
E
elim_in_set_add_set [lemma, in FiniteSetLat]
empty [definition, in FiniteSetLat]
eq [definition, in ArrayLat]
eq [definition, in BoolLat]
eq [axiom, in Poset]
eq [axiom, in Poset]
eq' [inductive, in ArrayLat]
eq'_dec [lemma, in ArrayLat]
eq'_sym [lemma, in ArrayLat]
eq'_to_Feq [lemma, in ArrayLat]
eq'_trans [lemma, in ArrayLat]
eq_dec [definition, in FiniteSetLat]
eq_dec [lemma, in BoolLat]
eq_dec [lemma, in ArrayLat]
eq_dec [definition, in FiniteSetLat]
eq_dec [axiom, in Lattice]
eq_funcTree' [inductive, in ArrayLat]
eq_funcTree'_none [constructor, in ArrayLat]
eq_funcTree'_some [constructor, in ArrayLat]
eq_order_order [lemma, in Lattice]
eq_refl [lemma, in BoolLat]
eq_refl [axiom, in Poset]
eq_refl [lemma, in ArrayLat]
eq_refl [axiom, in Poset]
eq_sumlist [lemma, in SumList]
eq_sumlist' [lemma, in analysis2]
eq_sym [lemma, in BoolLat]
eq_sym [axiom, in Poset]
eq_sym [lemma, in ArrayLat]
eq_sym [axiom, in Poset]
eq_trans [lemma, in BoolLat]
eq_trans [axiom, in Poset]
eq_trans [axiom, in Poset]
eq_trans [lemma, in ArrayLat]
eq_trans' [lemma, in ArrayLat]
eq_word [definition, in PosInf]
eq_word_dec [lemma, in PosInf]
eq_word_def' [lemma, in PosInf]
eq_word_refl [lemma, in PosInf]
eq_word_sym [lemma, in PosInf]
eq_word_trans [lemma, in PosInf]
exP [definition, in PosInf]
extract [library]
F
F [definition, in extract]
factorize [definition, in SumList]
factorize_distinct [lemma, in SumList]
false_order [constructor, in BoolLat]
Fbottom [definition, in ArrayLat]
Feq [definition, in ArrayLat]
Feq_bot_dec [definition, in ArrayLat]
Feq_dec [definition, in ArrayLat]
Field [inductive, in syntax]
FieldName [definition, in syntax]
fieldNum [constructor, in syntax]
fieldRef [constructor, in syntax]
Field_dec [definition, in syntax]
filterM [definition, in analysis2]
filterM_distinct [lemma, in analysis2]
FiniteSetLat [library]
FiniteSetLattice [module, in FiniteSetLat]
Finter [definition, in ArrayLat]
fix_implies_fix_iter [lemma, in Lattice]
Fjoin [definition, in ArrayLat]
Forder [definition, in ArrayLat]
Forder_dec [definition, in ArrayLat]
Forder_to_order' [lemma, in ArrayLat]
funcTree [inductive, in ArrayLat]
funcTree' [definition, in ArrayLat]
F_BC [definition, in extract]
F_BC_monotone [lemma, in extract]
f_in_listf_prop1 [lemma, in Lattice]
f_in_listf_prop2 [lemma, in Lattice]
f_in_listf_prop3 [lemma, in Lattice]
F_MB [definition, in extract]
F_MB_monotone [lemma, in extract]
F_monotone [lemma, in extract]
F_MutRec [definition, in extract]
F_MutRec_monotone [lemma, in extract]
F_Pred [definition, in extract]
F_Pred_monotone [lemma, in extract]
G
gammaBC [definition, in analysis]
gammaMutRec [definition, in analysis]
gammaPred [definition, in analysis]
gammaRec [definition, in analysis]
gammaRec_prefix [lemma, in analysis2]
genMB [definition, in extract]
genMB_respect_eq [lemma, in extract]
genM_methods_rec [definition, in collect]
genPred [definition, in extract]
genPred_respect_eq [lemma, in extract]
gen_cBC1 [definition, in extract]
gen_cBC2 [definition, in extract]
gen_cBC2_respect_eq [lemma, in extract]
gen_cMutRec [definition, in extract]
gen_constr [definition, in extract]
gen_constr_respect_eq [lemma, in extract]
gen_instructions [definition, in collect]
gen_instructions_rec [lemma, in collect]
gen_methods_rec [definition, in collect]
getfield [constructor, in syntax]
goto [constructor, in syntax]
H
height_inf [inductive, in ArrayLat]
height_inf_modify [lemma, in ArrayLat]
height_inf_modify_set [lemma, in FiniteSetLat]
height_pos [definition, in FiniteSetLat]
I
I [inductive, in extract]
IBC [inductive, in extract]
If [constructor, in syntax]
ifix_implies_ifix_iter [lemma, in Lattice]
implem [definition, in syntax]
implem_rec [definition, in syntax]
IMutRec [inductive, in extract]
inf_leaf [constructor, in ArrayLat]
inf_log [inductive, in PosInf]
inf_logM [lemma, in collect]
inf_log_dec [lemma, in PosInf]
inf_log_dec [lemma, in TabTree]
inf_log_height [lemma, in FiniteSetLat]
inf_log_le [lemma, in FiniteSetLat]
inf_log_le [lemma, in PosInf]
inf_log_prop1 [lemma, in collect]
inf_log_prop2 [lemma, in collect]
inf_log_trans [lemma, in TabTree]
inf_log_trans' [lemma, in TabTree]
inf_log_xH [constructor, in PosInf]
inf_log_xI [constructor, in PosInf]
inf_log_xO [constructor, in PosInf]
inf_node [constructor, in ArrayLat]
insere [definition, in SumList]
insereM [definition, in analysis2]
insereM_distinct [lemma, in analysis2]
insere_in_multiset [definition, in SumList]
insere_in_multiset_distincts [lemma, in SumList]
insere_word [definition, in analysis2]
insere_word_distinct [lemma, in analysis2]
insere_word_sumlist [lemma, in analysis2]
Instruction [inductive, in syntax]
instructionAt [definition, in syntax]
instructionAt_eq_word [lemma, in syntax]
instructionAt_in_methods [lemma, in syntax]
integer [definition, in syntax]
inter [definition, in BoolLat]
inter [definition, in FiniteSetLat]
inter [axiom, in Lattice]
inter [definition, in FiniteSetLat]
inter [definition, in ArrayLat]
inter_bool [definition, in BoolLat]
inter_bound1 [lemma, in BoolLat]
inter_bound1 [definition, in FiniteSetLat]
inter_bound1 [definition, in FiniteSetLat]
inter_bound1 [axiom, in Lattice]
inter_bound1 [lemma, in ArrayLat]
inter_bound2 [definition, in FiniteSetLat]
inter_bound2 [definition, in FiniteSetLat]
inter_bound2 [axiom, in Lattice]
inter_bound2 [lemma, in BoolLat]
inter_bound2 [lemma, in ArrayLat]
inter_greater_bound [lemma, in BoolLat]
inter_greater_bound [axiom, in Lattice]
inter_greater_bound [lemma, in ArrayLat]
inter_greater_bound [definition, in FiniteSetLat]
inter_greater_bound [definition, in FiniteSetLat]
inter_tree [definition, in ArrayLat]
inter_tree_height_inf [lemma, in ArrayLat]
invariant_invoke_prefix_tr [lemma, in analysis]
invokevirtual [constructor, in syntax]
invoke_invariant_return [lemma, in analysis]
invoke_list [definition, in analysis2]
invoke_list_eq_word [lemma, in analysis2]
invoke_list_rec [definition, in analysis2]
invoke_must_change_sf [lemma, in analysis]
in_call [lemma, in analysis2]
in_call_cutrent_meth [lemma, in analysis2]
in_call_invoke [lemma, in analysis2]
in_collectM_elim [lemma, in collect]
in_collectM_intro [lemma, in collect]
in_collect_elim [lemma, in collect]
in_collect_intro [lemma, in collect]
in_definedFields [lemma, in syntax]
in_factorize [lemma, in SumList]
in_factorize2 [lemma, in SumList]
in_factorize3 [lemma, in analysis2]
in_factorize_in_Rec [lemma, in analysis2]
in_filterM [lemma, in analysis2]
in_filterM2 [lemma, in analysis2]
in_genM_methods_rec_elim [lemma, in collect]
in_genM_methods_rec_intro [lemma, in collect]
in_gen_instructions_elim [lemma, in collect]
in_gen_instructions_intro [lemma, in collect]
in_gen_instructions_rec_elim [lemma, in collect]
in_gen_instructions_rec_intro [lemma, in collect]
in_gen_methods_rec_elim [lemma, in collect]
in_gen_methods_rec_intro [lemma, in collect]
in_inf_log [lemma, in TabTree]
in_insere [lemma, in SumList]
in_insereM1 [lemma, in analysis2]
in_insereM2 [lemma, in analysis2]
in_insereM3 [lemma, in analysis2]
in_insere2 [lemma, in SumList]
in_insere_in_multiset [lemma, in SumList]
in_insere_in_multiset2 [lemma, in SumList]
in_insere_in_multiset_eq [lemma, in SumList]
in_insere_simpl [lemma, in SumList]
in_insere_word [lemma, in analysis2]
in_insere_word2 [lemma, in analysis2]
in_insere_word3 [lemma, in analysis2]
in_l [lemma, in analysis2]
in_list2multiset [lemma, in SumList]
in_list2multiset_factorize [lemma, in SumList]
in_list2multiset_invoke [lemma, in analysis2]
in_map_inv [lemma, in extract]
in_m_distinct [lemma, in SumList]
in_pc_new_is_new [lemma, in analysis2]
in_rev [lemma, in Lattice]
in_set [definition, in FiniteSetLat]
in_set_add_set1 [lemma, in FiniteSetLat]
in_set_add_set2 [lemma, in FiniteSetLat]
in_set_eq' [lemma, in FiniteSetLat]
in_set_eq_word [lemma, in FiniteSetLat]
in_set_eq_word' [lemma, in FiniteSetLat]
in_set_implem_rec [lemma, in syntax]
in_set_monotone [lemma, in FiniteSetLat]
in_set_singleton [lemma, in FiniteSetLat]
in_set_singleton' [lemma, in FiniteSetLat]
in_set_singleton1 [lemma, in FiniteSetLat]
in_set_singleton2 [lemma, in FiniteSetLat]
in_set_top [lemma, in FiniteSetLat]
in_singleton [lemma, in FiniteSetLat]
in_trace [inductive, in analysis]
in_trace0 [constructor, in analysis]
in_trace1 [constructor, in analysis]
in_trace2 [constructor, in analysis]
in_trace_conc [lemma, in analysis]
in_trace_conc_tr_r [lemma, in analysis]
in_trace_prefix [lemma, in analysis]
is_bottom [inductive, in ArrayLat]
is_bottom2_eq' [lemma, in ArrayLat]
is_bottom_apply [lemma, in ArrayLat]
is_bottom_dec [lemma, in ArrayLat]
is_bottom_eq' [lemma, in ArrayLat]
is_invoke_in_invoke_list [lemma, in analysis2]
is_new_in_new_list [lemma, in analysis2]
iter [definition, in Lattice]
iter_assoc [lemma, in Lattice]
iter_bottom_is_lfp [lemma, in Lattice]
iter_bottom_is_lifp [lemma, in Lattice]
iter_def [lemma, in Lattice]
iter_fix [definition, in Lattice]
Iter_fix [module, in Lattice]
iter_listf [definition, in Lattice]
iter_listf_is_monotone [lemma, in Lattice]
iter_monotone [lemma, in Lattice]
iter_stabilize_implies_lfp [lemma, in Lattice]
iter_stabilize_implies_lifp [lemma, in Lattice]
iter_until_fix_f [definition, in Lattice]
I_MB [inductive, in extract]
I_Pred [inductive, in extract]
J
join [definition, in FiniteSetLat]
join [definition, in FiniteSetLat]
join [definition, in BoolLat]
join [definition, in ArrayLat]
join [axiom, in Lattice]
joinB [definition, in analysis]
join4 [lemma, in Lattice]
join_bool [definition, in BoolLat]
join_bottom1 [lemma, in Lattice]
join_bottom2 [lemma, in Lattice]
join_bound1 [axiom, in Lattice]
join_bound1 [lemma, in ArrayLat]
join_bound1 [lemma, in BoolLat]
join_bound1 [definition, in FiniteSetLat]
join_bound1 [definition, in FiniteSetLat]
join_bound2 [lemma, in BoolLat]
join_bound2 [axiom, in Lattice]
join_bound2 [definition, in FiniteSetLat]
join_bound2 [lemma, in ArrayLat]
join_bound2 [definition, in FiniteSetLat]
join_eq1 [lemma, in Lattice]
join_eq2 [lemma, in Lattice]
join_least_bound [lemma, in ArrayLat]
join_least_bound [lemma, in BoolLat]
join_least_bound [definition, in FiniteSetLat]
join_least_bound [definition, in FiniteSetLat]
join_least_bound [axiom, in Lattice]
join_list [definition, in Lattice]
join_list_greater [lemma, in Lattice]
join_list_least_greater [lemma, in Lattice]
join_sym [lemma, in Lattice]
join_tree [definition, in ArrayLat]
join_tree_height_inf [lemma, in ArrayLat]
L
L [module, in FiniteSetLat]
Lattice [module, in Lattice]
Lattice [library]
Lattice_prop [module, in Lattice]
leaf [constructor, in TabTree]
leaf [definition, in FiniteSetLat]
left [definition, in analysis2]
left [definition, in analysis2]
left [definition, in SumList]
left [definition, in SumList]
left [definition, in analysis2]
left [definition, in analysis2]
length_list2multiset_le_invoke [lemma, in analysis2]
lfp [definition, in Lattice]
LFP [module, in extract]
LFPMB [module, in extract]
LFPPred [module, in extract]
LFP_BC [module, in extract]
lfp_is_lfp [lemma, in Lattice]
lfp_is_lifp [lemma, in Lattice]
lfp_list [definition, in Lattice]
lfp_list_is_lifp [lemma, in Lattice]
LFP_MutRec [module, in extract]
list2multiset [definition, in SumList]
list2multiset_distinct [lemma, in SumList]
list_order [inductive, in Lattice]
list_order_cons [constructor, in Lattice]
list_order_join_list [lemma, in Lattice]
list_order_nil [constructor, in Lattice]
load [constructor, in syntax]
log_inf_log_positive [lemma, in TabTree]
log_positive [definition, in TabTree]
lt_n_op [inductive, in FiniteSetLat]
lt_n_op_none [constructor, in FiniteSetLat]
lt_n_op_some [constructor, in FiniteSetLat]
lt_n_op_trans [lemma, in FiniteSetLat]
M
M [module, in FiniteSetLat]
majoration1 [lemma, in analysis2]
majoration2 [lemma, in analysis2]
majoration3 [lemma, in analysis2]
majoration4 [lemma, in analysis2]
map_app [lemma, in extract]
max_inf_log_trans [lemma, in TabTree]
max_invoke_list [definition, in analysis2]
max_invoke_list_bound [lemma, in analysis2]
max_invoke_list_rec [definition, in analysis2]
max_invoke_list_rec_bound1 [lemma, in analysis2]
max_invoke_list_rec_bound2 [lemma, in analysis2]
max_log_list [definition, in TabTree]
max_new_list [definition, in analysis2]
max_new_list_bound [lemma, in analysis2]
max_new_list_rec [definition, in analysis2]
max_new_list_rec_bound1 [lemma, in analysis2]
max_new_list_rec_bound2 [lemma, in analysis2]
may_call [definition, in analysis2]
may_call_eq_word [lemma, in analysis2]
MBC [module, in analysis]
Method [inductive, in syntax]
MethodID [definition, in syntax]
methodLookup [definition, in syntax]
methodLookup_in_implem [lemma, in syntax]
methodLookup_some [lemma, in syntax]
methodLookup_some_in [lemma, in syntax]
MethodName [definition, in syntax]
MethodName_dec [definition, in syntax]
Methods_all_distinct [inductive, in syntax]
Methods_all_distinct_cons [constructor, in syntax]
Methods_all_distinct_nil [constructor, in syntax]
MMB [module, in extract]
MMutRec [module, in analysis]
modify [definition, in ArrayLat]
modify [definition, in FiniteSetLat]
modifyFunc [definition, in ArrayLat]
modify_monotone [lemma, in ArrayLat]
modify_set [definition, in FiniteSetLat]
modify_set_tree [definition, in TabTree]
modify_tree [definition, in TabTree]
modify_tree [definition, in ArrayLat]
Mon [inductive, in extract]
monotone [definition, in Lattice]
Mon_BC [inductive, in extract]
Mon_C1 [constructor, in extract]
Mon_C2 [constructor, in extract]
Mon_C4 [constructor, in extract]
Mon_C5 [constructor, in extract]
Mon_C6 [constructor, in extract]
Mon_C7 [constructor, in extract]
Mon_MB [inductive, in extract]
Mon_MutRec [inductive, in extract]
Mon_Pred [inductive, in extract]
MPred [module, in analysis]
MPred' [module, in analysis]
MProp [module, in ArrayLat]
MRec [module, in analysis]
MutRec_correctness [lemma, in analysis]
MutRec_correctness_lemma [lemma, in analysis]
m2_pc_in_tr [inductive, in analysis]
m2_pc_in_tr0 [constructor, in analysis]
m2_pc_in_tr1 [constructor, in analysis]
m2_pc_in_tr_conc [lemma, in analysis]
m2_pc_in_tr_eq_word1 [lemma, in analysis]
m_disticts_in_sf [inductive, in analysis]
m_disticts_in_sf_cons [constructor, in analysis]
m_disticts_in_sf_nil [constructor, in analysis]
M_distinct [inductive, in analysis2]
m_distincts [inductive, in SumList]
m_distincts0 [constructor, in SumList]
m_distincts1 [constructor, in SumList]
m_distincts_insere [lemma, in SumList]
m_distincts_length_bounded [lemma, in analysis2]
M_distinct0 [constructor, in analysis2]
M_distinct1 [constructor, in analysis2]
M_distinct_permute_sumlist [lemma, in analysis2]
m_in_sf_dec [lemma, in analysis]
m_in_sf_eq_word [lemma, in analysis]
m_in_sf_In [lemma, in analysis]
m_in_sf_incl [lemma, in analysis]
m_in_tr [inductive, in analysis]
m_in_tr0 [constructor, in analysis]
m_in_tr1 [constructor, in analysis]
m_in_tr_st [lemma, in analysis]
m_pc_in_current_tr [constructor, in analysis]
m_pc_in_current_tr1 [constructor, in analysis]
m_pc_in_current_tr2 [constructor, in analysis]
m_pc_in_current_tr3 [constructor, in analysis]
m_pc_in_current_tr4 [constructor, in analysis]
m_pc_in_current_tr5 [constructor, in analysis]
m_pc_in_sf_rest [inductive, in analysis]
m_pc_in_sf_rest0 [constructor, in analysis]
m_pc_in_sf_rest1 [constructor, in analysis]
m_pc_in_sf_rest_incl [lemma, in analysis]
m_pc_not_in [lemma, in SumList]
N
nameMethod_invariant [lemma, in analysis]
nat2pos [definition, in syntax]
nb_instruction_prefix [lemma, in analysis]
nb_invoke [inductive, in analysis]
nb_invoke0 [constructor, in analysis]
nb_invoke2 [constructor, in analysis]
nb_invoke4 [constructor, in analysis]
nb_invoke_exist [lemma, in analysis2]
nb_invoke_nb_new_m [lemma, in analysis2]
nb_invoke_pred [lemma, in analysis2]
nb_m_pc [inductive, in SumList]
nb_m_pc0 [constructor, in SumList]
nb_m_pc1 [constructor, in SumList]
nb_m_pc2 [constructor, in SumList]
nb_m_pc_bounded [lemma, in analysis2]
nb_m_pc_eq [lemma, in SumList]
nb_m_pc_in_current_tr [inductive, in analysis]
nb_m_pc_in_current_tr_not0 [lemma, in analysis]
nb_m_pc_in_list [lemma, in SumList]
nb_new [definition, in analysis2]
nb_new_m [definition, in analysis2]
nb_new_m_eq_word [lemma, in analysis2]
nb_new_m_pc [definition, in analysis2]
nb_new_m_pc0 [lemma, in analysis2]
nb_new_m_pc_eq [lemma, in analysis2]
nb_new_m_pc_eq0_or_new [lemma, in analysis2]
nb_new_m_sumlist [lemma, in analysis2]
nb_new_sumlist [lemma, in analysis2]
new_a [constructor, in syntax]
new_list [definition, in analysis2]
new_list_eq_word [lemma, in analysis2]
new_list_rec [definition, in analysis2]
new_o [constructor, in syntax]
nextAddress [definition, in syntax]
nextAddress_eq_word [lemma, in syntax]
nil [definition, in SumList]
nil [definition, in SumList]
nil [definition, in SumList]
nil [definition, in syntax]
nil [definition, in SumList]
nil [definition, in analysis2]
nil [definition, in analysis2]
nil [definition, in syntax]
nil [definition, in SumList]
nil [definition, in syntax]
nil [definition, in analysis2]
nil [definition, in analysis2]
nil [definition, in analysis2]
nil [definition, in syntax]
nil [definition, in analysis2]
nil [definition, in analysis2]
nil [definition, in collect]
nil [definition, in collect]
node [constructor, in TabTree]
nop [constructor, in syntax]
not_empty [definition, in extract]
not_empty_monotone [lemma, in extract]
not_single_tr [inductive, in analysis]
not_single_tr0 [constructor, in analysis]
nth_invoke_list [lemma, in analysis2]
nth_new_list [lemma, in analysis2]
nth_positive [definition, in syntax]
NumericType [constructor, in syntax]
numop [constructor, in syntax]
O
O [definition, in TabTree]
O [definition, in PosInf]
Operator [inductive, in syntax]
OpMult [constructor, in syntax]
OpPlus [constructor, in syntax]
order [axiom, in Poset]
order [definition, in ArrayLat]
order [axiom, in Poset]
order [definition, in BoolLat]
orderB [definition, in analysis]
order' [inductive, in ArrayLat]
order'_antisym [lemma, in ArrayLat]
order'_is_bottom [lemma, in ArrayLat]
order'_is_bottom2 [lemma, in ArrayLat]
order'_trans [lemma, in ArrayLat]
order2eq_dec [lemma, in Lattice]
order_add_set [lemma, in FiniteSetLat]
order_antisym [axiom, in Poset]
order_antisym [lemma, in BoolLat]
order_antisym [axiom, in Poset]
order_antisym [lemma, in ArrayLat]
order_dec [lemma, in ArrayLat]
order_dec [axiom, in Lattice]
order_dec [lemma, in BoolLat]
order_dec [definition, in FiniteSetLat]
order_dec [definition, in FiniteSetLat]
order_eq_order [lemma, in Lattice]
order_funcTree' [inductive, in ArrayLat]
order_funcTree'_none [constructor, in ArrayLat]
order_funcTree'_some [constructor, in ArrayLat]
order_refl [lemma, in ArrayLat]
order_refl [lemma, in BoolLat]
order_refl [axiom, in Poset]
order_refl [axiom, in Poset]
order_subst [lemma, in ArrayLat]
order_trans [lemma, in ArrayLat]
order_trans [lemma, in BoolLat]
order_trans [axiom, in Poset]
order_trans [axiom, in Poset]
order_trans' [lemma, in ArrayLat]
P
pc_distincts [inductive, in SumList]
pc_distincts0 [constructor, in SumList]
pc_distincts1 [constructor, in SumList]
pc_distincts_length_bounded [lemma, in analysis2]
pc_in_current_tr [inductive, in analysis]
pc_in_current_tr_conc [lemma, in analysis]
pc_in_current_tr_current [constructor, in analysis]
pc_in_current_tr_eq_word [lemma, in analysis]
pc_in_current_tr_eq_word' [lemma, in analysis]
pc_in_current_tr_in_trace [lemma, in analysis]
pc_in_current_tr_next [constructor, in analysis]
pc_in_rest_tr [inductive, in analysis]
pc_in_rest_tr_def [constructor, in analysis]
pc_new [definition, in analysis2]
pc_new_bounded_by_nrw_list [lemma, in analysis2]
pc_new_distinct [lemma, in analysis2]
physical_eq [axiom, in PosInf]
pop [constructor, in syntax]
Pos [module, in FiniteSetLat]
Pos [module, in ArrayLat]
Pos [module, in Lattice]
Pos [module, in BoolLat]
Pos [module, in FiniteSetLat]
Poset [module, in Poset]
Poset [library]
PosetSet [module, in Poset]
posInf [definition, in PosInf]
PosInf [library]
positive_dec [lemma, in PosInf]
positive_dec [lemma, in TabTree]
postfix_F_to_I [lemma, in extract]
postfix_F_to_I_BC1 [lemma, in extract]
postfix_F_to_I_MB [lemma, in extract]
postfix_F_to_I_MutRec [lemma, in extract]
postfix_F_to_I_Pred [lemma, in extract]
Pos_dec [module, in Lattice]
pow2 [definition, in FiniteSetLat]
pow2_le1 [lemma, in FiniteSetLat]
Pred_correctness [lemma, in analysis]
Pred_correctness_lemma [lemma, in analysis]
prefix_conc_tr [lemma, in analysis]
prefix_tr [inductive, in analysis]
prefix_tr0 [constructor, in analysis]
prefix_tr1 [constructor, in analysis]
prefix_tr_strict [inductive, in analysis]
prefix_tr_strict0 [constructor, in analysis]
progCount [definition, in syntax]
Program [inductive, in syntax]
properties [module, in Lattice]
prop_on_collect [lemma, in collect]
prop_on_collectM [lemma, in collect]
prop_prefix_tr [inductive, in analysis]
prop_prefix_tr0 [constructor, in analysis]
prop_prefix_tr1 [constructor, in analysis]
push [constructor, in syntax]
push2 [constructor, in syntax]
putfield [constructor, in syntax]
R
R [definition, in ArrayLat]
Rec_correctness [lemma, in analysis]
Rec_correctness_lemma [lemma, in analysis]
remove_begin_invoke [lemma, in analysis]
remove_exec [inductive, in analysis]
remove_exec_continue [constructor, in analysis]
remove_exec_exists [lemma, in analysis]
remove_exec_first [constructor, in analysis]
remove_exec_found [constructor, in analysis]
remove_exec_prefix [lemma, in analysis]
remove_exec_prefix' [lemma, in analysis]
remove_SemCol [lemma, in analysis]
return_invariant [lemma, in analysis]
return_v [constructor, in syntax]
R'_acc [lemma, in ArrayLat]
R_acc [lemma, in ArrayLat]
S
searchClass [definition, in syntax]
searchClass_eq_word [lemma, in syntax]
searchClass_in_class [lemma, in syntax]
searchClass_in_class_nameClass [lemma, in syntax]
searchClass_none [lemma, in analysis]
searchClass_rec [definition, in syntax]
searchClass_rec_in_l [lemma, in syntax]
searchClass_rec_in_l_classname [lemma, in syntax]
searchField [definition, in syntax]
searchField_rec [definition, in syntax]
searchMethod [definition, in syntax]
searchMethod_eq_some [lemma, in syntax]
searchMethod_eq_word [lemma, in analysis2]
searchMethod_rec [definition, in syntax]
searchMethod_rec_eq_word [lemma, in syntax]
searchMethod_some [lemma, in syntax]
searchMethod_some_in [lemma, in syntax]
searchWithMethodID [definition, in syntax]
seq_call [inductive, in analysis]
seq_call_dec [lemma, in analysis]
seq_call_def [constructor, in analysis]
seq_call_eq_word [lemma, in analysis]
set [axiom, in Poset]
set [definition, in ArrayLat]
set [axiom, in Poset]
set [definition, in BoolLat]
set2list [definition, in FiniteSetLat]
set2list_rec [definition, in FiniteSetLat]
sf_rest [inductive, in analysis]
sf_rest0 [constructor, in analysis]
singleton [definition, in FiniteSetLat]
solveBC [lemma, in extract]
solveMB [lemma, in extract]
solveMutRec [lemma, in extract]
solvePred [lemma, in extract]
solveRec [lemma, in extract]
store [constructor, in syntax]
subst [definition, in ArrayLat]
subst [definition, in FiniteSetLat]
substFunc [definition, in ArrayLat]
subst_eq [lemma, in ArrayLat]
subst_leaf [definition, in TabTree]
subst_monotone [lemma, in ArrayLat]
subst_tree [definition, in TabTree]
succ_word [definition, in PosInf]
succ_word_eq_word [lemma, in PosInf]
succ_word_n [definition, in PosInf]
sumlist [definition, in SumList]
SumList [library]
sumlist0 [lemma, in analysis2]
sumlist_bound [lemma, in SumList]
sumlist_bound2 [lemma, in SumList]
sumlist_factorize [lemma, in SumList]
sumlist_final [lemma, in SumList]
sumlist_list2multiset [lemma, in SumList]
syntax [library]
T
TabTree [library]
top [axiom, in Lattice]
top [definition, in BoolLat]
top [definition, in FiniteSetLat]
top [definition, in FiniteSetLat]
top [definition, in ArrayLat]
topF [definition, in ArrayLat]
topF_is_top [lemma, in ArrayLat]
top_is_top [lemma, in ArrayLat]
top_is_top [lemma, in BoolLat]
top_is_top [definition, in FiniteSetLat]
top_is_top [definition, in FiniteSetLat]
top_is_top [axiom, in Lattice]
Trace_init [definition, in analysis2]
Trace_init [definition, in analysis2]
Trace_init [definition, in analysis2]
Trace_init [definition, in analysis2]
tree [inductive, in TabTree]
true_order [constructor, in BoolLat]
tr_rest [inductive, in analysis]
tr_rest0 [constructor, in analysis]
typeOfField [inductive, in syntax]
U
update [definition, in extract]
V
valid_method_invariant [lemma, in analysis2]
Var [definition, in syntax]
Var_dec [definition, in syntax]
verif_all_collected_BC1 [lemma, in extract]
verif_all_collected_BC2 [lemma, in extract]
verif_all_collected_MB [lemma, in extract]
verif_all_collected_MutRec [lemma, in extract]
verif_all_collected_Pred [lemma, in extract]
verif_all_collected_Rec [lemma, in extract]
verif_all_gen_constr_BC1 [lemma, in extract]
verif_all_gen_constr_BC2 [lemma, in extract]
verif_all_gen_constr_MB [lemma, in extract]
verif_all_gen_constr_MutRec [lemma, in extract]
verif_all_gen_constr_Pred [lemma, in extract]
verif_all_gen_constr_Rec [lemma, in extract]
W
Word [definition, in PosInf]
WordSize [definition, in PosInf]
word2pos [definition, in PosInf]
word_distincts [inductive, in analysis2]
word_distincts0 [constructor, in analysis2]
word_distincts1 [constructor, in analysis2]
word_distincts_length_bounded [lemma, in analysis2]
Word_1 [definition, in PosInf]
X
xH [definition, in FiniteSetLat]
Axiom Index
A
acc_property [in Lattice]
B
bottom [in Lattice]
bottom_is_a_bottom [in Lattice]
E
eq [in Poset]
eq [in Poset]
eq_dec [in Lattice]
eq_refl [in Poset]
eq_refl [in Poset]
eq_sym [in Poset]
eq_sym [in Poset]
eq_trans [in Poset]
eq_trans [in Poset]
I
inter [in Lattice]
inter_bound1 [in Lattice]
inter_bound2 [in Lattice]
inter_greater_bound [in Lattice]
J
join [in Lattice]
join_bound1 [in Lattice]
join_bound2 [in Lattice]
join_least_bound [in Lattice]
O
order [in Poset]
order [in Poset]
order_antisym [in Poset]
order_antisym [in Poset]
order_dec [in Lattice]
order_refl [in Poset]
order_refl [in Poset]
order_trans [in Poset]
order_trans [in Poset]
P
physical_eq [in PosInf]
S
set [in Poset]
set [in Poset]
T
top [in Lattice]
top_is_top [in Lattice]
Lemma Index
A
acc_property [in BoolLat]
acc_property [in ArrayLat]
acc_property' [in ArrayLat]
add_set_eq [in FiniteSetLat]
add_set_monotone [in FiniteSetLat]
analyse [in extract]
apply_bottom [in ArrayLat]
apply_build_const_TabTree_is_bot [in TabTree]
apply_build_const_TabTree_is_const [in TabTree]
apply_eq [in ArrayLat]
apply_eq_word [in ArrayLat]
apply_inter_tree [in ArrayLat]
apply_is_bottom [in ArrayLat]
apply_join_tree [in ArrayLat]
apply_modify1 [in ArrayLat]
apply_modify1' [in ArrayLat]
apply_modify2 [in ArrayLat]
apply_modify2' [in ArrayLat]
apply_modify_set1 [in FiniteSetLat]
apply_modify_set2 [in FiniteSetLat]
apply_modify_set_tree [in TabTree]
apply_modify_set_tree1 [in TabTree]
apply_modify_tree1 [in TabTree]
apply_modify_tree2 [in TabTree]
apply_monotone [in ArrayLat]
apply_prop_prefix [in analysis]
apply_prop_tr [in analysis]
apply_set_in [in FiniteSetLat]
apply_set_tree1 [in TabTree]
apply_subst1 [in ArrayLat]
apply_subst1' [in ArrayLat]
apply_subst2 [in ArrayLat]
apply_subst2' [in ArrayLat]
apply_subst_leaf1 [in TabTree]
apply_subst_leaf2 [in TabTree]
apply_subst_tree1 [in TabTree]
apply_subst_tree2 [in TabTree]
apply_tree_bot [in ArrayLat]
app_dec [in analysis]
B
BC_correctness [in analysis]
BC_correctness_lemma [in analysis]
big_bound1 [in analysis2]
big_bound2 [in analysis2]
bottom_cardinal_tree [in FiniteSetLat]
bottom_is_a_bottom [in ArrayLat]
bottom_is_a_bottom [in BoolLat]
bounded_calls [in analysis2]
bounded_news [in analysis2]
C
call_exist [in analysis2]
call_is_nb_invoke [in analysis2]
call_jump1 [in analysis2]
cardinal_max [in FiniteSetLat]
cardinal_monotone [in FiniteSetLat]
cardinal_tree_bottom [in FiniteSetLat]
cardinal_tree_eq [in FiniteSetLat]
cardinal_tree_inf_pow2 [in FiniteSetLat]
cardinal_tree_monotone [in FiniteSetLat]
cardinal_0_in_set [in FiniteSetLat]
collectedMB_monotones [in extract]
collectedPred_monotones [in extract]
collected_BC_monotones [in extract]
collected_monotones [in extract]
collected_monotones_BC2 [in extract]
collected_MutRec_monotones [in extract]
conc_tr_currentState [in analysis]
count_new_m_eq [in analysis2]
count_new_m_eq0 [in analysis2]
count_new_m_eq0_pc [in analysis2]
count_new_m_eq_pc [in analysis2]
count_new_m_eq_word [in analysis2]
count_new_m_pc0 [in analysis2]
count_new_m_pc_case [in analysis2]
count_new_m_pc_eq [in analysis2]
count_new_m_pc_is_new [in analysis2]
count_new_m_pc_le1 [in analysis2]
count_new_m__0or1 [in analysis2]
currentState_in_trace [in analysis]
D
definedFields_eq_word [in syntax]
E
elim_in_set_add_set [in FiniteSetLat]
eq'_dec [in ArrayLat]
eq'_sym [in ArrayLat]
eq'_to_Feq [in ArrayLat]
eq'_trans [in ArrayLat]
eq_dec [in BoolLat]
eq_dec [in ArrayLat]
eq_order_order [in Lattice]
eq_refl [in BoolLat]
eq_refl [in ArrayLat]
eq_sumlist [in SumList]
eq_sumlist' [in analysis2]
eq_sym [in BoolLat]
eq_sym [in ArrayLat]
eq_trans [in BoolLat]
eq_trans [in ArrayLat]
eq_trans' [in ArrayLat]
eq_word_dec [in PosInf]
eq_word_def' [in PosInf]
eq_word_refl [in PosInf]
eq_word_sym [in PosInf]
eq_word_trans [in PosInf]
F
factorize_distinct [in SumList]
filterM_distinct [in analysis2]
fix_implies_fix_iter [in Lattice]
Forder_to_order' [in ArrayLat]
F_BC_monotone [in extract]
f_in_listf_prop1 [in Lattice]
f_in_listf_prop2 [in Lattice]
f_in_listf_prop3 [in Lattice]
F_MB_monotone [in extract]
F_monotone [in extract]
F_MutRec_monotone [in extract]
F_Pred_monotone [in extract]
G
gammaRec_prefix [in analysis2]
genMB_respect_eq [in extract]
genPred_respect_eq [in extract]
gen_cBC2_respect_eq [in extract]
gen_constr_respect_eq [in extract]
gen_instructions_rec [in collect]
H
height_inf_modify [in ArrayLat]
height_inf_modify_set [in FiniteSetLat]
I
ifix_implies_ifix_iter [in Lattice]
inf_logM [in collect]
inf_log_dec [in PosInf]
inf_log_dec [in TabTree]
inf_log_height [in FiniteSetLat]
inf_log_le [in FiniteSetLat]
inf_log_le [in PosInf]
inf_log_prop1 [in collect]
inf_log_prop2 [in collect]
inf_log_trans [in TabTree]
inf_log_trans' [in TabTree]
insereM_distinct [in analysis2]
insere_in_multiset_distincts [in SumList]
insere_word_distinct [in analysis2]
insere_word_sumlist [in analysis2]
instructionAt_eq_word [in syntax]
instructionAt_in_methods [in syntax]
inter_bound1 [in BoolLat]
inter_bound1 [in ArrayLat]
inter_bound2 [in BoolLat]
inter_bound2 [in ArrayLat]
inter_greater_bound [in BoolLat]
inter_greater_bound [in ArrayLat]
inter_tree_height_inf [in ArrayLat]
invariant_invoke_prefix_tr [in analysis]
invoke_invariant_return [in analysis]
invoke_list_eq_word [in analysis2]
invoke_must_change_sf [in analysis]
in_call [in analysis2]
in_call_cutrent_meth [in analysis2]
in_call_invoke [in analysis2]
in_collectM_elim [in collect]
in_collectM_intro [in collect]
in_collect_elim [in collect]
in_collect_intro [in collect]
in_definedFields [in syntax]
in_factorize [in SumList]
in_factorize2 [in SumList]
in_factorize3 [in analysis2]
in_factorize_in_Rec [in analysis2]
in_filterM [in analysis2]
in_filterM2 [in analysis2]
in_genM_methods_rec_elim [in collect]
in_genM_methods_rec_intro [in collect]
in_gen_instructions_elim [in collect]
in_gen_instructions_intro [in collect]
in_gen_instructions_rec_elim [in collect]
in_gen_instructions_rec_intro [in collect]
in_gen_methods_rec_elim [in collect]
in_gen_methods_rec_intro [in collect]
in_inf_log [in TabTree]
in_insere [in SumList]
in_insereM1 [in analysis2]
in_insereM2 [in analysis2]
in_insereM3 [in analysis2]
in_insere2 [in SumList]
in_insere_in_multiset [in SumList]
in_insere_in_multiset2 [in SumList]
in_insere_in_multiset_eq [in SumList]
in_insere_simpl [in SumList]
in_insere_word [in analysis2]
in_insere_word2 [in analysis2]
in_insere_word3 [in analysis2]
in_l [in analysis2]
in_list2multiset [in SumList]
in_list2multiset_factorize [in SumList]
in_list2multiset_invoke [in analysis2]
in_map_inv [in extract]
in_m_distinct [in SumList]
in_pc_new_is_new [in analysis2]
in_rev [in Lattice]
in_set_add_set1 [in FiniteSetLat]
in_set_add_set2 [in FiniteSetLat]
in_set_eq' [in FiniteSetLat]
in_set_eq_word [in FiniteSetLat]
in_set_eq_word' [in FiniteSetLat]
in_set_implem_rec [in syntax]
in_set_monotone [in FiniteSetLat]
in_set_singleton [in FiniteSetLat]
in_set_singleton' [in FiniteSetLat]
in_set_singleton1 [in FiniteSetLat]
in_set_singleton2 [in FiniteSetLat]
in_set_top [in FiniteSetLat]
in_singleton [in FiniteSetLat]
in_trace_conc [in analysis]
in_trace_conc_tr_r [in analysis]
in_trace_prefix [in analysis]
is_bottom2_eq' [in ArrayLat]
is_bottom_apply [in ArrayLat]
is_bottom_dec [in ArrayLat]
is_bottom_eq' [in ArrayLat]
is_invoke_in_invoke_list [in analysis2]
is_new_in_new_list [in analysis2]
iter_assoc [in Lattice]
iter_bottom_is_lfp [in Lattice]
iter_bottom_is_lifp [in Lattice]
iter_def [in Lattice]
iter_listf_is_monotone [in Lattice]
iter_monotone [in Lattice]
iter_stabilize_implies_lfp [in Lattice]
iter_stabilize_implies_lifp [in Lattice]
J
join4 [in Lattice]
join_bottom1 [in Lattice]
join_bottom2 [in Lattice]
join_bound1 [in ArrayLat]
join_bound1 [in BoolLat]
join_bound2 [in BoolLat]
join_bound2 [in ArrayLat]
join_eq1 [in Lattice]
join_eq2 [in Lattice]
join_least_bound [in ArrayLat]
join_least_bound [in BoolLat]
join_list_greater [in Lattice]
join_list_least_greater [in Lattice]
join_sym [in Lattice]
join_tree_height_inf [in ArrayLat]
L
length_list2multiset_le_invoke [in analysis2]
lfp_is_lfp [in Lattice]
lfp_is_lifp [in Lattice]
lfp_list_is_lifp [in Lattice]
list2multiset_distinct [in SumList]
list_order_join_list [in Lattice]
log_inf_log_positive [in TabTree]
lt_n_op_trans [in FiniteSetLat]
M
majoration1 [in analysis2]
majoration2 [in analysis2]
majoration3 [in analysis2]
majoration4 [in analysis2]
map_app [in extract]
max_inf_log_trans [in TabTree]
max_invoke_list_bound [in analysis2]
max_invoke_list_rec_bound1 [in analysis2]
max_invoke_list_rec_bound2 [in analysis2]
max_new_list_bound [in analysis2]
max_new_list_rec_bound1 [in analysis2]
max_new_list_rec_bound2 [in analysis2]
may_call_eq_word [in analysis2]
methodLookup_in_implem [in syntax]
methodLookup_some [in syntax]
methodLookup_some_in [in syntax]
modify_monotone [in ArrayLat]
MutRec_correctness [in analysis]
MutRec_correctness_lemma [in analysis]
m2_pc_in_tr_conc [in analysis]
m2_pc_in_tr_eq_word1 [in analysis]
m_distincts_insere [in SumList]
m_distincts_length_bounded [in analysis2]
M_distinct_permute_sumlist [in analysis2]
m_in_sf_dec [in analysis]
m_in_sf_eq_word [in analysis]
m_in_sf_In [in analysis]
m_in_sf_incl [in analysis]
m_in_tr_st [in analysis]
m_pc_in_sf_rest_incl [in analysis]
m_pc_not_in [in SumList]
N
nameMethod_invariant [in analysis]
nb_instruction_prefix [in analysis]
nb_invoke_exist [in analysis2]
nb_invoke_nb_new_m [in analysis2]
nb_invoke_pred [in analysis2]
nb_m_pc_bounded [in analysis2]
nb_m_pc_eq [in SumList]
nb_m_pc_in_current_tr_not0 [in analysis]
nb_m_pc_in_list [in SumList]
nb_new_m_eq_word [in analysis2]
nb_new_m_pc0 [in analysis2]
nb_new_m_pc_eq [in analysis2]
nb_new_m_pc_eq0_or_new [in analysis2]
nb_new_m_sumlist [in analysis2]
nb_new_sumlist [in analysis2]
new_list_eq_word [in analysis2]
nextAddress_eq_word [in syntax]
not_empty_monotone [in extract]
nth_invoke_list [in analysis2]
nth_new_list [in analysis2]
O
order'_antisym [in ArrayLat]
order'_is_bottom [in ArrayLat]
order'_is_bottom2 [in ArrayLat]
order'_trans [in ArrayLat]
order2eq_dec [in Lattice]
order_add_set [in FiniteSetLat]
order_antisym [in BoolLat]
order_antisym [in ArrayLat]
order_dec [in ArrayLat]
order_dec [in BoolLat]
order_eq_order [in Lattice]
order_refl [in ArrayLat]
order_refl [in BoolLat]
order_subst [in ArrayLat]
order_trans [in ArrayLat]
order_trans [in BoolLat]
order_trans' [in ArrayLat]
P
pc_distincts_length_bounded [in analysis2]
pc_in_current_tr_conc [in analysis]
pc_in_current_tr_eq_word [in analysis]
pc_in_current_tr_eq_word' [in analysis]
pc_in_current_tr_in_trace [in analysis]
pc_new_bounded_by_nrw_list [in analysis2]
pc_new_distinct [in analysis2]
positive_dec [in PosInf]
positive_dec [in TabTree]
postfix_F_to_I [in extract]
postfix_F_to_I_BC1 [in extract]
postfix_F_to_I_MB [in extract]
postfix_F_to_I_MutRec [in extract]
postfix_F_to_I_Pred [in extract]
pow2_le1 [in FiniteSetLat]
Pred_correctness [in analysis]
Pred_correctness_lemma [in analysis]
prefix_conc_tr [in analysis]
prop_on_collect [in collect]
prop_on_collectM [in collect]
R
Rec_correctness [in analysis]
Rec_correctness_lemma [in analysis]
remove_begin_invoke [in analysis]
remove_exec_exists [in analysis]
remove_exec_prefix [in analysis]
remove_exec_prefix' [in analysis]
remove_SemCol [in analysis]
return_invariant [in analysis]
R'_acc [in ArrayLat]
R_acc [in ArrayLat]
S
searchClass_eq_word [in syntax]
searchClass_in_class [in syntax]
searchClass_in_class_nameClass [in syntax]
searchClass_none [in analysis]
searchClass_rec_in_l [in syntax]
searchClass_rec_in_l_classname [in syntax]
searchMethod_eq_some [in syntax]
searchMethod_eq_word [in analysis2]
searchMethod_rec_eq_word [in syntax]
searchMethod_some [in syntax]
searchMethod_some_in [in syntax]
seq_call_dec [in analysis]
seq_call_eq_word [in analysis]
solveBC [in extract]
solveMB [in extract]
solveMutRec [in extract]
solvePred [in extract]
solveRec [in extract]
subst_eq [in ArrayLat]
subst_monotone [in ArrayLat]
succ_word_eq_word [in PosInf]
sumlist0 [in analysis2]
sumlist_bound [in SumList]
sumlist_bound2 [in SumList]
sumlist_factorize [in SumList]
sumlist_final [in SumList]
sumlist_list2multiset [in SumList]
T
topF_is_top [in ArrayLat]
top_is_top [in ArrayLat]
top_is_top [in BoolLat]
V
valid_method_invariant [in analysis2]
verif_all_collected_BC1 [in extract]
verif_all_collected_BC2 [in extract]
verif_all_collected_MB [in extract]
verif_all_collected_MutRec [in extract]
verif_all_collected_Pred [in extract]
verif_all_collected_Rec [in extract]
verif_all_gen_constr_BC1 [in extract]
verif_all_gen_constr_BC2 [in extract]
verif_all_gen_constr_MB [in extract]
verif_all_gen_constr_MutRec [in extract]
verif_all_gen_constr_Pred [in extract]
verif_all_gen_constr_Rec [in extract]
W
word_distincts_length_bounded [in analysis2]
Constructor Index
A
arraylength [in syntax]
arrayload [in syntax]
arraystore [in syntax]
C
call_0 [in analysis2]
call_1 [in analysis2]
call_2 [in analysis2]
ClassType [in syntax]
conc_tr0 [in analysis]
conc_tr1 [in analysis]
C1 [in extract]
C2 [in extract]
C4 [in extract]
C5 [in extract]
C6 [in extract]
C7 [in extract]
E
eq_funcTree'_none [in ArrayLat]
eq_funcTree'_some [in ArrayLat]
F
false_order [in BoolLat]
fieldNum [in syntax]
fieldRef [in syntax]
G
getfield [in syntax]
goto [in syntax]
I
If [in syntax]
inf_leaf [in ArrayLat]
inf_log_xH [in PosInf]
inf_log_xI [in PosInf]
inf_log_xO [in PosInf]
inf_node [in ArrayLat]
invokevirtual [in syntax]
in_trace0 [in analysis]
in_trace1 [in analysis]
in_trace2 [in analysis]
L
leaf [in TabTree]
list_order_cons [in Lattice]
list_order_nil [in Lattice]
load [in syntax]
lt_n_op_none [in FiniteSetLat]
lt_n_op_some [in FiniteSetLat]
M
Methods_all_distinct_cons [in syntax]
Methods_all_distinct_nil [in syntax]
Mon_C1 [in extract]
Mon_C2 [in extract]
Mon_C4 [in extract]
Mon_C5 [in extract]
Mon_C6 [in extract]
Mon_C7 [in extract]
m2_pc_in_tr0 [in analysis]
m2_pc_in_tr1 [in analysis]
m_disticts_in_sf_cons [in analysis]
m_disticts_in_sf_nil [in analysis]
m_distincts0 [in SumList]
m_distincts1 [in SumList]
M_distinct0 [in analysis2]
M_distinct1 [in analysis2]
m_in_tr0 [in analysis]
m_in_tr1 [in analysis]
m_pc_in_current_tr [in analysis]
m_pc_in_current_tr1 [in analysis]
m_pc_in_current_tr2 [in analysis]
m_pc_in_current_tr3 [in analysis]
m_pc_in_current_tr4 [in analysis]
m_pc_in_current_tr5 [in analysis]
m_pc_in_sf_rest0 [in analysis]
m_pc_in_sf_rest1 [in analysis]
N
nb_invoke0 [in analysis]
nb_invoke2 [in analysis]
nb_invoke4 [in analysis]
nb_m_pc0 [in SumList]
nb_m_pc1 [in SumList]
nb_m_pc2 [in SumList]
new_a [in syntax]
new_o [in syntax]
node [in TabTree]
nop [in syntax]
not_single_tr0 [in analysis]
NumericType [in syntax]
numop [in syntax]
O
OpMult [in syntax]
OpPlus [in syntax]
order_funcTree'_none [in ArrayLat]
order_funcTree'_some [in ArrayLat]
P
pc_distincts0 [in SumList]
pc_distincts1 [in SumList]
pc_in_current_tr_current [in analysis]
pc_in_current_tr_next [in analysis]
pc_in_rest_tr_def [in analysis]
pop [in syntax]
prefix_tr0 [in analysis]
prefix_tr1 [in analysis]
prefix_tr_strict0 [in analysis]
prop_prefix_tr0 [in analysis]
prop_prefix_tr1 [in analysis]
push [in syntax]
push2 [in syntax]
putfield [in syntax]
R
remove_exec_continue [in analysis]
remove_exec_first [in analysis]
remove_exec_found [in analysis]
return_v [in syntax]
S
seq_call_def [in analysis]
sf_rest0 [in analysis]
store [in syntax]
T
true_order [in BoolLat]
tr_rest0 [in analysis]
W
word_distincts0 [in analysis2]
word_distincts1 [in analysis2]
Inductive Index
A
AllConstr [in analysis2]
AnalyseResult [in extract]
B
bool_order [in BoolLat]
C
call [in analysis2]
Class [in syntax]
ComponentType [in syntax]
conc_tr [in analysis]
Constraint [in extract]
ConstraintBC [in extract]
ConstraintMB [in extract]
ConstraintMutRec [in extract]
ConstraintPred [in extract]
ConstrBC [in analysis]
ConstrMB [in extract]
ConstrPred [in analysis]
ConstrRec [in analysis]
E
eq' [in ArrayLat]
eq_funcTree' [in ArrayLat]
F
Field [in syntax]
funcTree [in ArrayLat]
H
height_inf [in ArrayLat]
I
I [in extract]
IBC [in extract]
IMutRec [in extract]
inf_log [in PosInf]
Instruction [in syntax]
in_trace [in analysis]
is_bottom [in ArrayLat]
I_MB [in extract]
I_Pred [in extract]
L
list_order [in Lattice]
lt_n_op [in FiniteSetLat]
M
Method [in syntax]
Methods_all_distinct [in syntax]
Mon [in extract]
Mon_BC [in extract]
Mon_MB [in extract]
Mon_MutRec [in extract]
Mon_Pred [in extract]
m2_pc_in_tr [in analysis]
m_disticts_in_sf [in analysis]
M_distinct [in analysis2]
m_distincts [in SumList]
m_in_tr [in analysis]
m_pc_in_sf_rest [in analysis]
N
nb_invoke [in analysis]
nb_m_pc [in SumList]
nb_m_pc_in_current_tr [in analysis]
not_single_tr [in analysis]
O
Operator [in syntax]
order' [in ArrayLat]
order_funcTree' [in ArrayLat]
P
pc_distincts [in SumList]
pc_in_current_tr [in analysis]
pc_in_rest_tr [in analysis]
prefix_tr [in analysis]
prefix_tr_strict [in analysis]
Program [in syntax]
prop_prefix_tr [in analysis]
R
remove_exec [in analysis]
S
seq_call [in analysis]
sf_rest [in analysis]
T
tree [in TabTree]
tr_rest [in analysis]
typeOfField [in syntax]
W
word_distincts [in analysis2]
Definition Index
A
acc_property [in FiniteSetLat]
acc_property [in FiniteSetLat]
add_set [in FiniteSetLat]
apply [in FiniteSetLat]
apply [in ArrayLat]
applyFunc [in ArrayLat]
apply_functree [in ArrayLat]
apply_set [in FiniteSetLat]
apply_set_tree [in TabTree]
apply_tree [in TabTree]
apply_tree [in ArrayLat]
B
bottom [in FiniteSetLat]
bottom [in FiniteSetLat]
bottom [in BoolLat]
bottom [in ArrayLat]
bottom_is_a_bottom [in FiniteSetLat]
bottom_is_a_bottom [in FiniteSetLat]
build_const_TabTree_rec [in TabTree]
C
cardinal [in FiniteSetLat]
cardinal_tree [in FiniteSetLat]
CardMax [in FiniteSetLat]
ClassName [in syntax]
collect [in collect]
collectBC1 [in extract]
collectBC2 [in extract]
collectM [in collect]
collectMB [in extract]
collectMutRec [in extract]
collectPred [in extract]
collectRec [in extract]
ConstrMutRec [in analysis]
count_new [in analysis2]
count_new_m [in analysis2]
count_new_m_pc [in analysis2]
D
definedFields [in syntax]
E
empty [in FiniteSetLat]
eq [in ArrayLat]
eq [in BoolLat]
eq_dec [in FiniteSetLat]
eq_dec [in FiniteSetLat]
eq_word [in PosInf]
exP [in PosInf]
F
F [in extract]
factorize [in SumList]
Fbottom [in ArrayLat]
Feq [in ArrayLat]
Feq_bot_dec [in ArrayLat]
Feq_dec [in ArrayLat]
FieldName [in syntax]
Field_dec [in syntax]
filterM [in analysis2]
Finter [in ArrayLat]
Fjoin [in ArrayLat]
Forder [in ArrayLat]
Forder_dec [in ArrayLat]
funcTree' [in ArrayLat]
F_BC [in extract]
F_MB [in extract]
F_MutRec [in extract]
F_Pred [in extract]
G
gammaBC [in analysis]
gammaMutRec [in analysis]
gammaPred [in analysis]
gammaRec [in analysis]
genMB [in extract]
genM_methods_rec [in collect]
genPred [in extract]
gen_cBC1 [in extract]
gen_cBC2 [in extract]
gen_cMutRec [in extract]
gen_constr [in extract]
gen_instructions [in collect]
gen_methods_rec [in collect]
H
height_pos [in FiniteSetLat]
I
implem [in syntax]
implem_rec [in syntax]
insere [in SumList]
insereM [in analysis2]
insere_in_multiset [in SumList]
insere_word [in analysis2]
instructionAt [in syntax]
integer [in syntax]
inter [in BoolLat]
inter [in FiniteSetLat]
inter [in FiniteSetLat]
inter [in ArrayLat]
inter_bool [in BoolLat]
inter_bound1 [in FiniteSetLat]
inter_bound1 [in FiniteSetLat]
inter_bound2 [in FiniteSetLat]
inter_bound2 [in FiniteSetLat]
inter_greater_bound [in FiniteSetLat]
inter_greater_bound [in FiniteSetLat]
inter_tree [in ArrayLat]
invoke_list [in analysis2]
invoke_list_rec [in analysis2]
in_set [in FiniteSetLat]
iter [in Lattice]
iter_fix [in Lattice]
iter_listf [in Lattice]
iter_until_fix_f [in Lattice]
J
join [in FiniteSetLat]
join [in FiniteSetLat]
join [in BoolLat]
join [in ArrayLat]
joinB [in analysis]
join_bool [in BoolLat]
join_bound1 [in FiniteSetLat]
join_bound1 [in FiniteSetLat]
join_bound2 [in FiniteSetLat]
join_bound2 [in FiniteSetLat]
join_least_bound [in FiniteSetLat]
join_least_bound [in FiniteSetLat]
join_list [in Lattice]
join_tree [in ArrayLat]
L
leaf [in FiniteSetLat]
left [in analysis2]
left [in analysis2]
left [in SumList]
left [in SumList]
left [in analysis2]
left [in analysis2]
lfp [in Lattice]
lfp_list [in Lattice]
list2multiset [in SumList]
log_positive [in TabTree]
M
max_invoke_list [in analysis2]
max_invoke_list_rec [in analysis2]
max_log_list [in TabTree]
max_new_list [in analysis2]
max_new_list_rec [in analysis2]
may_call [in analysis2]
MethodID [in syntax]
methodLookup [in syntax]
MethodName [in syntax]
MethodName_dec [in syntax]
modify [in ArrayLat]
modify [in FiniteSetLat]
modifyFunc [in ArrayLat]
modify_set [in FiniteSetLat]
modify_set_tree [in TabTree]
modify_tree [in TabTree]
modify_tree [in ArrayLat]
monotone [in Lattice]
N
nat2pos [in syntax]
nb_new [in analysis2]
nb_new_m [in analysis2]
nb_new_m_pc [in analysis2]
new_list [in analysis2]
new_list_rec [in analysis2]
nextAddress [in syntax]
nil [in SumList]
nil [in SumList]
nil [in SumList]
nil [in syntax]
nil [in SumList]
nil [in analysis2]
nil [in analysis2]
nil [in syntax]
nil [in SumList]
nil [in syntax]
nil [in analysis2]
nil [in analysis2]
nil [in analysis2]
nil [in syntax]
nil [in analysis2]
nil [in analysis2]
nil [in collect]
nil [in collect]
not_empty [in extract]
nth_positive [in syntax]
O
O [in TabTree]
O [in PosInf]
order [in ArrayLat]
order [in BoolLat]
orderB [in analysis]
order_dec [in FiniteSetLat]
order_dec [in FiniteSetLat]
P
pc_new [in analysis2]
posInf [in PosInf]
pow2 [in FiniteSetLat]
progCount [in syntax]
R
R [in ArrayLat]
S
searchClass [in syntax]
searchClass_rec [in syntax]
searchField [in syntax]
searchField_rec [in syntax]
searchMethod [in syntax]
searchMethod_rec [in syntax]
searchWithMethodID [in syntax]
set [in ArrayLat]
set [in BoolLat]
set2list [in FiniteSetLat]
set2list_rec [in FiniteSetLat]
singleton [in FiniteSetLat]
subst [in ArrayLat]
subst [in FiniteSetLat]
substFunc [in ArrayLat]
subst_leaf [in TabTree]
subst_tree [in TabTree]
succ_word [in PosInf]
succ_word_n [in PosInf]
sumlist [in SumList]
T
top [in BoolLat]
top [in FiniteSetLat]
top [in FiniteSetLat]
top [in ArrayLat]
topF [in ArrayLat]
top_is_top [in FiniteSetLat]
top_is_top [in FiniteSetLat]
Trace_init [in analysis2]
Trace_init [in analysis2]
Trace_init [in analysis2]
Trace_init [in analysis2]
U
update [in extract]
V
Var [in syntax]
Var_dec [in syntax]
W
Word [in PosInf]
WordSize [in PosInf]
word2pos [in PosInf]
Word_1 [in PosInf]
X
xH [in FiniteSetLat]
Module Index
A
ArrayLattice [in ArrayLat]
ArrayPoset [in ArrayLat]
ArraySetLattice [in FiniteSetLat]
B
BoolLattice [in BoolLat]
BoolPoset [in BoolLat]
F
FiniteSetLattice [in FiniteSetLat]
I
Iter_fix [in Lattice]
L
L [in FiniteSetLat]
Lattice [in Lattice]
Lattice_prop [in Lattice]
LFP [in extract]
LFPMB [in extract]
LFPPred [in extract]
LFP_BC [in extract]
LFP_MutRec [in extract]
M
M [in FiniteSetLat]
MBC [in analysis]
MMB [in extract]
MMutRec [in analysis]
MPred [in analysis]
MPred' [in analysis]
MProp [in ArrayLat]
MRec [in analysis]
P
Pos [in FiniteSetLat]
Pos [in ArrayLat]
Pos [in Lattice]
Pos [in BoolLat]
Pos [in FiniteSetLat]
Poset [in Poset]
PosetSet [in Poset]
Pos_dec [in Lattice]
properties [in Lattice]
Library Index
A
AllLattice
analysis
analysis2
ArrayLat
B
BoolLat
C
collect
E
extract
F
FiniteSetLat
L
Lattice
P
Poset
PosInf
S
SumList
syntax
T
TabTree
| 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 |
_ |
(860 entries) |
| Axiom Index |
A |
B |
C |
D |
E |
F |
G |
H |
I |
J |
K |
L |
M |
N |
O |
P |
Q |
R |
S |
T |
U |
V |
W |
X |
Y |
Z |
_ |
(34 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 |
_ |
(386 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 |
_ |
(106 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 |
_ |
(66 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 |
_ |
(222 entries) |
| Module 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 |
_ |
(32 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 |
_ |
(14 entries) |
This page has been generated by coqdoc