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

SemSequences

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