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 _ (245 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 _ (78 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 _ (2 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 _ (73 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 _ (17 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 _ (64 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 _ (3 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6 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 _ (2 entries)

Global Index

A

aand [definition, in Sem]
Aassert [constructor, in Sem]
Aassign [constructor, in Sem]
acmd [inductive, in Sem]
aequal [definition, in Sem]
afalse [definition, in Sem]
agree [definition, in Sem]
agree_mon [lemma, in Sem]
agree_update_dead [lemma, in Sem]
agree_update_live [lemma, in Sem]
Aifthenelse [constructor, in Sem]
aimp [definition, in Sem]
alessthan [definition, in Sem]
aor [definition, in Sem]
aprog [definition, in Sem]
aprog_correct [lemma, in Sem]
Aseq [constructor, in Sem]
Askip [constructor, in Sem]
assertion [definition, in Sem]
atrue [definition, in Sem]
aupdate [definition, in Sem]
Awhile [constructor, in Sem]


B

Bequal [constructor, in Sem]
bind [definition, in Sem]
bind_mon [lemma, in Sem]
bind_Res_inversion [lemma, in Sem]
Bless [constructor, in Sem]
bool_expr [inductive, in Sem]
Bot [constructor, in Sem]


C

Cassign [constructor, in Sem]
Cifthenelse [constructor, in Sem]
cmd [inductive, in Sem]
code [definition, in Sem]
code_at [definition, in Sem]
code_at_app [lemma, in Sem]
compile_bool_expr [definition, in Sem]
compile_bool_expr_correct [lemma, in Sem]
compile_cmd [definition, in Sem]
compile_cmd_correct_diverging [lemma, in Sem]
compile_cmd_correct_terminating [lemma, in Sem]
compile_expr [definition, in Sem]
compile_expr_correct [lemma, in Sem]
compile_program [definition, in Sem]
compile_program_correct [lemma, in Sem]
Cseq [constructor, in Sem]
Cskip [constructor, in Sem]
Cwhile [constructor, in Sem]


D

dce [definition, in Sem]
dce_correct_diverging [lemma, in Sem]
dce_correct_terminating [lemma, in Sem]
denot [definition, in Sem]
denot_assign [lemma, in Sem]
denot_charact [lemma, in Sem]
denot_exec [lemma, in Sem]
denot_execinf [lemma, in Sem]
denot_if [lemma, in Sem]
denot_limit [lemma, in Sem]
denot_seq [lemma, in Sem]
denot_skip [lemma, in Sem]
denot_while [lemma, in Sem]
denot_while_least_fixed_point [lemma, in Sem]
diverges [definition, in Sem]
diverges_execinf [lemma, in Sem]
diverges_seq_inversion [lemma, in Sem]
diverges_star_inv [lemma, in Sem]
diverges_while_inversion [lemma, in Sem]
diverging_state [inductive, in Sem]
diverging_state_productive [lemma, in Sem]
div_state_intro [constructor, in Sem]


E

Eadd [constructor, in Sem]
Econst [constructor, in Sem]
eq_ident [definition, in Sem]
erase [definition, in Sem]
Esub [constructor, in Sem]
eval_bool_expr [definition, in Sem]
eval_bool_expr_agree [lemma, in Sem]
eval_expr [definition, in Sem]
eval_expr_agree [lemma, in Sem]
eval_expr_domain [lemma, in Sem]
Evar [constructor, in Sem]
exec [inductive, in Sem]
execinf [inductive, in Sem]
execinf_denot [lemma, in Sem]
execinf_diverges [lemma, in Sem]
execinf_if [constructor, in Sem]
execinf_interp [lemma, in Sem]
execinf_red_step [lemma, in Sem]
execinf_seq_left [constructor, in Sem]
execinf_seq_right [constructor, in Sem]
execinf_while_body [constructor, in Sem]
execinf_while_loop [constructor, in Sem]
exec_assign [constructor, in Sem]
exec_denot [lemma, in Sem]
exec_if [constructor, in Sem]
exec_interp [lemma, in Sem]
exec_interp_either [lemma, in Sem]
exec_seq [constructor, in Sem]
exec_skip [constructor, in Sem]
exec_terminates [lemma, in Sem]
exec_while_loop [constructor, in Sem]
exec_while_stop [constructor, in Sem]
expr [inductive, in Sem]
expr_add_pos [lemma, in Sem]


F

finally [inductive, in Sem]
finally_consequence [lemma, in Sem]
finally_done [constructor, in Sem]
finally_seq [lemma, in Sem]
finally_step [constructor, in Sem]
finally_while [lemma, in Sem]
finseq_unique [lemma, in Sequences]
FIXPOINT [section, in Sem]
fixpoint [definition, in Sem]
FIXPOINT.default [variable, in Sem]
FIXPOINT.F [variable, in Sem]
FIXPOINT.F_stable [variable, in Sem]
fixpoint_charact [lemma, in Sem]
fixpoint_upper_bound [lemma, in Sem]
fv_bool_expr [definition, in Sem]
fv_cmd [definition, in Sem]
fv_expr [definition, in Sem]


G

goes_wrong [definition, in Sem]


I

Iadd [constructor, in Sem]
Ibge [constructor, in Sem]
Ibne [constructor, in Sem]
Ibranch [constructor, in Sem]
Iconst [constructor, in Sem]
ident [definition, in Sem]
Ihalt [constructor, in Sem]
infseq [inductive, in Sequences]
infseq_alternate_characterization [lemma, in Sequences]
infseq_coinduction_principle [lemma, in Sequences]
infseq_coinduction_principle_2 [lemma, in Sequences]
infseq_finseq_excl [lemma, in Sequences]
infseq_or_finseq [lemma, in Sequences]
infseq_star_inv [lemma, in Sequences]
infseq_step [constructor, in Sequences]
initial_state [definition, in Sem]
instruction [inductive, in Sem]
interp [definition, in Sem]
interp_exec [lemma, in Sem]
interp_limit [lemma, in Sem]
interp_limit_dep [definition, in Sem]
interp_mon [lemma, in Sem]
interp_Res_stable [lemma, in Sem]
invariant [definition, in Sem]
irred [definition, in Sequences]
Isetvar [constructor, in Sem]
Isub [constructor, in Sem]
is_free [definition, in Sem]
iter [definition, in Sem]
Ivar [constructor, in Sem]


L

length [definition, in Sem]
length_app [lemma, in Sem]
length_cons [lemma, in Sem]
length_singleton [lemma, in Sem]
le_interp_denot [lemma, in Sem]
live [definition, in Sem]
live_upper_bound [lemma, in Sem]
live_while_charact [lemma, in Sem]


M

machine_state [definition, in Sem]
mach_diverges [definition, in Sem]
mach_goes_wrong [definition, in Sem]
mach_terminates [definition, in Sem]


N

niter [definition, in Sem]


P

plus [inductive, in Sequences]
plus_left [constructor, in Sequences]
plus_one [lemma, in Sequences]
plus_right [lemma, in Sequences]
postcondition [definition, in Sem]
precondition [definition, in Sem]
prog [definition, in Sem]
prog_init_state [definition, in Sem]


R

red [inductive, in Sem]
red_assign [constructor, in Sem]
red_deterministic [lemma, in Sem]
red_if_false [constructor, in Sem]
red_if_true [constructor, in Sem]
red_preserves_exec [lemma, in Sem]
red_seq_left [constructor, in Sem]
red_seq_skip [constructor, in Sem]
red_while_false [constructor, in Sem]
red_while_true [constructor, in Sem]
Res [constructor, in Sem]
result [inductive, in Sem]
res_le [definition, in Sem]


S

Sem [library]
sem_Triple [definition, in Sem]
sem_triple [definition, in Sem]
SEQUENCES [section, in Sequences]
Sequences [library]
SEQUENCES.A [variable, in Sequences]
SEQUENCES.R [variable, in Sequences]
SEQUENCES.R_determ [variable, in Sequences]
stack [definition, in Sem]
star [inductive, in Sequences]
star_one [lemma, in Sequences]
star_plus [lemma, in Sequences]
star_red_seq_left [lemma, in Sem]
star_refl [constructor, in Sequences]
star_star_inv [lemma, in Sequences]
star_step [constructor, in Sequences]
star_trans [lemma, in Sequences]
state [definition, in Sem]


T

terminates [definition, in Sem]
terminates_exec [lemma, in Sem]
test_prog [definition, in Sem]
transition [inductive, in Sem]
trans_add [constructor, in Sem]
trans_bge [constructor, in Sem]
trans_bne [constructor, in Sem]
trans_branch [constructor, in Sem]
trans_const [constructor, in Sem]
trans_setvar [constructor, in Sem]
trans_sub [constructor, in Sem]
trans_var [constructor, in Sem]
triple [inductive, in Sem]
Triple [inductive, in Sem]
triple_assign [constructor, in Sem]
Triple_assign [constructor, in Sem]
Triple_consequence [constructor, in Sem]
triple_consequence [constructor, in Sem]
Triple_correct [lemma, in Sem]
triple_correct [lemma, in Sem]
triple_if [constructor, in Sem]
Triple_if [constructor, in Sem]
triple_seq [constructor, in Sem]
Triple_seq [constructor, in Sem]
triple_skip [constructor, in Sem]
Triple_skip [constructor, in Sem]
triple_while [constructor, in Sem]
Triple_while [constructor, in Sem]
Triple_while_correct [lemma, in Sem]


U

update [definition, in Sem]


V

va [definition, in Sem]
vb [definition, in Sem]
vcg [definition, in Sem]
vcgen [definition, in Sem]
vcgen_correct [lemma, in Sem]
vcg_correct [lemma, in Sem]
vq [definition, in Sem]
vr [definition, in Sem]
VS [module, in Sem]
VSdecide [module, in Sem]
VSP [module, in Sem]


W

wp [definition, in Sem]



Lemma Index

A

agree_mon [in Sem]
agree_update_dead [in Sem]
agree_update_live [in Sem]
aprog_correct [in Sem]


B

bind_mon [in Sem]
bind_Res_inversion [in Sem]


C

code_at_app [in Sem]
compile_bool_expr_correct [in Sem]
compile_cmd_correct_diverging [in Sem]
compile_cmd_correct_terminating [in Sem]
compile_expr_correct [in Sem]
compile_program_correct [in Sem]


D

dce_correct_diverging [in Sem]
dce_correct_terminating [in Sem]
denot_assign [in Sem]
denot_charact [in Sem]
denot_exec [in Sem]
denot_execinf [in Sem]
denot_if [in Sem]
denot_limit [in Sem]
denot_seq [in Sem]
denot_skip [in Sem]
denot_while [in Sem]
denot_while_least_fixed_point [in Sem]
diverges_execinf [in Sem]
diverges_seq_inversion [in Sem]
diverges_star_inv [in Sem]
diverges_while_inversion [in Sem]
diverging_state_productive [in Sem]


E

eval_bool_expr_agree [in Sem]
eval_expr_agree [in Sem]
eval_expr_domain [in Sem]
execinf_denot [in Sem]
execinf_diverges [in Sem]
execinf_interp [in Sem]
execinf_red_step [in Sem]
exec_denot [in Sem]
exec_interp [in Sem]
exec_interp_either [in Sem]
exec_terminates [in Sem]
expr_add_pos [in Sem]


F

finally_consequence [in Sem]
finally_seq [in Sem]
finally_while [in Sem]
finseq_unique [in Sequences]
fixpoint_charact [in Sem]
fixpoint_upper_bound [in Sem]


I

infseq_alternate_characterization [in Sequences]
infseq_coinduction_principle [in Sequences]
infseq_coinduction_principle_2 [in Sequences]
infseq_finseq_excl [in Sequences]
infseq_or_finseq [in Sequences]
infseq_star_inv [in Sequences]
interp_exec [in Sem]
interp_limit [in Sem]
interp_mon [in Sem]
interp_Res_stable [in Sem]


L

length_app [in Sem]
length_cons [in Sem]
length_singleton [in Sem]
le_interp_denot [in Sem]
live_upper_bound [in Sem]
live_while_charact [in Sem]


P

plus_one [in Sequences]
plus_right [in Sequences]


R

red_deterministic [in Sem]
red_preserves_exec [in Sem]


S

star_one [in Sequences]
star_plus [in Sequences]
star_red_seq_left [in Sem]
star_star_inv [in Sequences]
star_trans [in Sequences]


T

terminates_exec [in Sem]
Triple_correct [in Sem]
triple_correct [in Sem]
Triple_while_correct [in Sem]


V

vcgen_correct [in Sem]
vcg_correct [in Sem]



Section Index

F

FIXPOINT [in Sem]


S

SEQUENCES [in Sequences]



Constructor Index

A

Aassert [in Sem]
Aassign [in Sem]
Aifthenelse [in Sem]
Aseq [in Sem]
Askip [in Sem]
Awhile [in Sem]


B

Bequal [in Sem]
Bless [in Sem]
Bot [in Sem]


C

Cassign [in Sem]
Cifthenelse [in Sem]
Cseq [in Sem]
Cskip [in Sem]
Cwhile [in Sem]


D

div_state_intro [in Sem]


E

Eadd [in Sem]
Econst [in Sem]
Esub [in Sem]
Evar [in Sem]
execinf_if [in Sem]
execinf_seq_left [in Sem]
execinf_seq_right [in Sem]
execinf_while_body [in Sem]
execinf_while_loop [in Sem]
exec_assign [in Sem]
exec_if [in Sem]
exec_seq [in Sem]
exec_skip [in Sem]
exec_while_loop [in Sem]
exec_while_stop [in Sem]


F

finally_done [in Sem]
finally_step [in Sem]


I

Iadd [in Sem]
Ibge [in Sem]
Ibne [in Sem]
Ibranch [in Sem]
Iconst [in Sem]
Ihalt [in Sem]
infseq_step [in Sequences]
Isetvar [in Sem]
Isub [in Sem]
Ivar [in Sem]


P

plus_left [in Sequences]


R

red_assign [in Sem]
red_if_false [in Sem]
red_if_true [in Sem]
red_seq_left [in Sem]
red_seq_skip [in Sem]
red_while_false [in Sem]
red_while_true [in Sem]
Res [in Sem]


S

star_refl [in Sequences]
star_step [in Sequences]


T

trans_add [in Sem]
trans_bge [in Sem]
trans_bne [in Sem]
trans_branch [in Sem]
trans_const [in Sem]
trans_setvar [in Sem]
trans_sub [in Sem]
trans_var [in Sem]
triple_assign [in Sem]
Triple_assign [in Sem]
Triple_consequence [in Sem]
triple_consequence [in Sem]
triple_if [in Sem]
Triple_if [in Sem]
triple_seq [in Sem]
Triple_seq [in Sem]
triple_skip [in Sem]
Triple_skip [in Sem]
triple_while [in Sem]
Triple_while [in Sem]



Inductive Index

A

acmd [in Sem]


B

bool_expr [in Sem]


C

cmd [in Sem]


D

diverging_state [in Sem]


E

exec [in Sem]
execinf [in Sem]
expr [in Sem]


F

finally [in Sem]


I

infseq [in Sequences]
instruction [in Sem]


P

plus [in Sequences]


R

red [in Sem]
result [in Sem]


S

star [in Sequences]


T

transition [in Sem]
triple [in Sem]
Triple [in Sem]



Definition Index

A

aand [in Sem]
aequal [in Sem]
afalse [in Sem]
agree [in Sem]
aimp [in Sem]
alessthan [in Sem]
aor [in Sem]
aprog [in Sem]
assertion [in Sem]
atrue [in Sem]
aupdate [in Sem]


B

bind [in Sem]


C

code [in Sem]
code_at [in Sem]
compile_bool_expr [in Sem]
compile_cmd [in Sem]
compile_expr [in Sem]
compile_program [in Sem]


D

dce [in Sem]
denot [in Sem]
diverges [in Sem]


E

eq_ident [in Sem]
erase [in Sem]
eval_bool_expr [in Sem]
eval_expr [in Sem]


F

fixpoint [in Sem]
fv_bool_expr [in Sem]
fv_cmd [in Sem]
fv_expr [in Sem]


G

goes_wrong [in Sem]


I

ident [in Sem]
initial_state [in Sem]
interp [in Sem]
interp_limit_dep [in Sem]
invariant [in Sem]
irred [in Sequences]
is_free [in Sem]
iter [in Sem]


L

length [in Sem]
live [in Sem]


M

machine_state [in Sem]
mach_diverges [in Sem]
mach_goes_wrong [in Sem]
mach_terminates [in Sem]


N

niter [in Sem]


P

postcondition [in Sem]
precondition [in Sem]
prog [in Sem]
prog_init_state [in Sem]


R

res_le [in Sem]


S

sem_Triple [in Sem]
sem_triple [in Sem]
stack [in Sem]
state [in Sem]


T

terminates [in Sem]
test_prog [in Sem]


U

update [in Sem]


V

va [in Sem]
vb [in Sem]
vcg [in Sem]
vcgen [in Sem]
vq [in Sem]
vr [in Sem]


W

wp [in Sem]



Module Index

V

VS [in Sem]
VSdecide [in Sem]
VSP [in Sem]



Variable Index

F

FIXPOINT.default [in Sem]
FIXPOINT.F [in Sem]
FIXPOINT.F_stable [in Sem]


S

SEQUENCES.A [in Sequences]
SEQUENCES.R [in Sequences]
SEQUENCES.R_determ [in Sequences]



Library Index

S

Sem
Sequences



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 _ (245 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 _ (78 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 _ (2 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 _ (73 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 _ (17 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 _ (64 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 _ (3 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6 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 _ (2 entries)

This page has been generated by coqdoc