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]

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]

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]

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]

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]

goes_wrong [definition, in Sem]

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]

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]

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

niter [definition, in Sem]

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]

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]

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]

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]

update [definition, in Sem]

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]