| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (809 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 | _ | other | (16 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (457 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 | _ | other | (6 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
A
absurd [lemma, in GC.safety.sweepnogrey]accessible [definition, in GC.reachable.reachable]
accnotfree [library]
acc_imp_notfree_gcend [lemma, in GC.safety.accnotfree]
acc_imp_notfree_gcfree1 [lemma, in GC.safety.accnotfree]
acc_imp_notfree_gcfree [lemma, in GC.safety.accnotfree]
acc_imp_notfree_gcstop [lemma, in GC.safety.accnotfree]
acc_imp_notfree_marknode [lemma, in GC.safety.accnotfree]
acc_imp_notfree_gccall [lemma, in GC.safety.accnotfree]
acc_imp_notfree_alloc [lemma, in GC.safety.accnotfree]
acc_imp_notfree_removeedge [lemma, in GC.safety.accnotfree]
acc_imp_notfree_addedge [lemma, in GC.safety.accnotfree]
acc_imp_notfree_init [lemma, in GC.safety.accnotfree]
acc_imp_notfree [definition, in GC.gc.gc]
acc_imp_notfree_step [lemma, in GC.safety.safety]
add [definition, in GC.gc.gc]
addedge_notacces_t [lemma, in GC.liveness.notfree_notacc]
add_grey [lemma, in GC.mesure.grey_card]
add_idem_or_init [lemma, in GC.liveness.notacc_init]
add_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
add_ex_mesure [lemma, in GC.mesure.mesure]
add_mesure [lemma, in GC.mesure.mesure]
add_to_node [constructor, in GC.gc.gc]
add_edge [inductive, in GC.gc.gc]
add_white [lemma, in GC.mesure.white_card]
add_black [lemma, in GC.mesure.black_card]
add_white_nogrey [lemma, in GC.lemma_step.lemma_add]
add_notfrees_notfreet [lemma, in GC.lemma_step.lemma_add]
add_blacks_blackt [lemma, in GC.lemma_step.lemma_add]
add_notgreyt_notgreys [lemma, in GC.lemma_step.lemma_add]
add_ancestor_col [lemma, in GC.lemma_step.lemma_add]
add_ancestor [lemma, in GC.lemma_step.lemma_add]
add_notaccess_notaccest [lemma, in GC.lemma_step.lemma_add]
add_accest_access [lemma, in GC.lemma_step.lemma_add]
add_nowhite [lemma, in GC.lemma_step.lemma_add]
add_nogrey [lemma, in GC.lemma_step.lemma_add]
add_notacc_white [lemma, in GC.lemma_step.lemma_add]
add_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
add_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
ae [constructor, in GC.gc.gc]
al [constructor, in GC.gc.gc]
alloc [inductive, in GC.gc.gc]
alloc_grey [lemma, in GC.mesure.grey_card]
alloc_idem_or_init [lemma, in GC.liveness.notacc_init]
alloc_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
alloc_ancestor_col [lemma, in GC.lemma_step.lemma_alloc]
alloc_ancestor [lemma, in GC.lemma_step.lemma_alloc]
alloc_nowhite [lemma, in GC.lemma_step.lemma_alloc]
alloc_nogrey [lemma, in GC.lemma_step.lemma_alloc]
alloc_whites_whitet [lemma, in GC.lemma_step.lemma_alloc]
alloc_notwhites_notwhitet [lemma, in GC.lemma_step.lemma_alloc]
alloc_notgreys_notgreyt [lemma, in GC.lemma_step.lemma_alloc]
alloc_greys_greyt [lemma, in GC.lemma_step.lemma_alloc]
alloc_notgreyt_notgreys [lemma, in GC.lemma_step.lemma_alloc]
alloc_accest_access [lemma, in GC.lemma_step.lemma_alloc]
alloc_blacks_blackt [lemma, in GC.lemma_step.lemma_alloc]
alloc_ex_mesure [lemma, in GC.mesure.mesure]
alloc_mesure [lemma, in GC.mesure.mesure]
alloc_add_free_to_rt [constructor, in GC.gc.gc]
alloc_white [lemma, in GC.mesure.white_card]
alloc_black [lemma, in GC.mesure.black_card]
alloc_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
alloc_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
alloc_notacces_t [lemma, in GC.liveness.notfree_notacc]
always [inductive, in GC.logique.LTL]
always_fairstep [lemma, in GC.liveness.fairstr]
always_exist_fairstep [lemma, in GC.liveness.fairstr]
always_and_inv_g_w_b [lemma, in GC.liveness.liveness]
always_unless [lemma, in GC.logique.LTL]
always_and_and [lemma, in GC.logique.LTL]
always_and_bis [lemma, in GC.logique.LTL]
always_and [lemma, in GC.logique.LTL]
always_implies_always_state [lemma, in GC.logique.LTL]
always_always_implies_always [lemma, in GC.logique.LTL]
always_imp_always [lemma, in GC.logique.LTL]
always_fairstr [lemma, in GC.logique.LTL]
always_trace [lemma, in GC.logique.LTL]
always_always_bis [lemma, in GC.logique.LTL]
always_always [lemma, in GC.logique.LTL]
always_implies_always_stream [lemma, in GC.logique.LTL]
always_implies_always [lemma, in GC.logique.LTL]
always_P [lemma, in GC.logique.LTL]
always_one_step_leads_to [lemma, in GC.logique.LTL]
always_on_run [lemma, in GC.logique.LTL]
always_nogrey_accn_imp_blackn [lemma, in GC.safety.safety]
always_invariant_safety_and [lemma, in GC.safety.safety]
always_inv_safety [lemma, in GC.safety.safety]
always_sweep_no_grey [lemma, in GC.safety.safety]
always_eventually_white_until_zero_trace [lemma, in GC.liveness.until_zero]
always_eventually_grey_until_zero_trace [lemma, in GC.liveness.until_zero]
always_mesure [lemma, in GC.mesure.safe_card]
always_gwb [lemma, in GC.mesure.safe_card]
always_card_grey [lemma, in GC.mesure.safe_card]
always_card_white [lemma, in GC.mesure.safe_card]
always_card_black [lemma, in GC.mesure.safe_card]
always_notfree_notacces_unless_isfree [lemma, in GC.liveness.notfree_notacc]
and [definition, in GC.logique.LTL]
and_inv [definition, in GC.liveness.liveness]
and_always_state [lemma, in GC.logique.LTL]
and_always [lemma, in GC.logique.LTL]
and_state [definition, in GC.logique.LTL]
and_exist [lemma, in GC.liveness.until_zero]
B
black [constructor, in GC.gc.parameters]black_grey_node [lemma, in GC.safety.noedgeblacktowhite]
black_grey_node [lemma, in GC.safety.rtgreyorblack]
black_card [section, in GC.mesure.black_card]
black_card [library]
C
call_gc_fair [lemma, in GC.liveness.fairstr]call_exist_grey_fair [lemma, in GC.liveness.fairstr]
call_exist_grey [constructor, in GC.gc.gc]
call_gc [constructor, in GC.gc.gc]
Card [abbreviation, in GC.card.card_facts]
card [inductive, in GC.card.card]
Card [abbreviation, in GC.mesure.grey_card]
Card [abbreviation, in GC.mesure.parameters_card]
Card [abbreviation, in GC.mesure.mesure]
Card [abbreviation, in GC.mesure.white_card]
Card [abbreviation, in GC.mesure.black_card]
card [library]
cardinal [section, in GC.card.card]
cardinal.A [variable, in GC.card.card]
cardinal.B [variable, in GC.card.card]
cardinal.P [variable, in GC.card.card]
card_facts.C [variable, in GC.card.card_facts]
card_facts.B [variable, in GC.card.card_facts]
card_facts.A [variable, in GC.card.card_facts]
card_facts [section, in GC.card.card_facts]
card_rem [lemma, in GC.card.card]
card_inv [lemma, in GC.card.card]
card_S [constructor, in GC.card.card]
card_0 [constructor, in GC.card.card]
card_grey_marknode [lemma, in GC.mesure.grey_card]
card_sons [inductive, in GC.mesure.parameters_card]
card_color [definition, in GC.mesure.parameters_card]
card_grey_rt [lemma, in GC.liveness.liveness]
card_white_marknode [lemma, in GC.mesure.white_card]
card_facts [library]
cases_marknode [lemma, in GC.gc.gc]
color [inductive, in GC.gc.parameters]
color_node [lemma, in GC.lemma_step.lemma_step]
conj_inv [definition, in GC.mesure.safe_card]
cons_str [constructor, in GC.logique.LTL]
control [inductive, in GC.gc.parameters]
CS [constructor, in GC.mesure.parameters_card]
ctl [projection, in GC.gc.parameters]
c_state [constructor, in GC.gc.parameters]
c_fstep [constructor, in GC.logique.LTL]
C_always [constructor, in GC.logique.LTL]
c_pos_trans [constructor, in GC.logique.LTL]
C_trans [constructor, in GC.logique.LTL]
D
def_equiv [lemma, in GC.liveness.liveness]dif [lemma, in GC.card.card]
dif2 [lemma, in GC.card.card]
E
enabled [inductive, in GC.logique.LTL]eqnm_eqSnSm [lemma, in GC.lib_arith.lib_S_pred]
equivalent_def [lemma, in GC.liveness.notacc_white_ancestor]
equiv_def2 [lemma, in GC.liveness.notacc_black_nogrey]
equiv_def [lemma, in GC.liveness.notacc_black_nogrey]
eq_dec_set [axiom, in GC.card.card_facts]
eq_dec_set [axiom, in GC.card.card]
eq_dec_color [lemma, in GC.gc.parameters]
eq_dec_node [axiom, in GC.gc.parameters]
Eventually [inductive, in GC.logique.LTL]
eventually_until [lemma, in GC.logique.LTL]
eventually_implies_eventually [lemma, in GC.logique.LTL]
Eventually_permanently [definition, in GC.logique.LTL]
eventually_white_until_zero [lemma, in GC.liveness.until_zero]
eventually_white_until_zero_trace [lemma, in GC.liveness.until_zero]
eventually_grey_until_zero [lemma, in GC.liveness.until_zero]
eventually_grey_until_zero_trace [lemma, in GC.liveness.until_zero]
eventually_measure_until_zero_on_run [lemma, in GC.liveness.until_zero]
eventually_measure_until_zero_trace_bis [lemma, in GC.liveness.until_zero]
eventually_measure_until_zero [lemma, in GC.liveness.until_zero]
eventually_measure_until_zero_trace [lemma, in GC.liveness.until_zero]
ev_t [constructor, in GC.logique.LTL]
ev_h [constructor, in GC.logique.LTL]
exist_updated_N [lemma, in GC.card.card_facts]
exist_updated_M [lemma, in GC.card.card_facts]
exist_updated [lemma, in GC.card.card]
exist_updated_heap [lemma, in GC.mesure.parameters_card]
exist_or_none [axiom, in GC.liveness.fairstr]
exist_update_color [lemma, in GC.liveness.fairstr]
exist_update_init_color [lemma, in GC.liveness.fairstr]
exist_grey_node [lemma, in GC.liveness.fairstr]
ex_gcend_grey [lemma, in GC.mesure.grey_card]
ex_gcfree1_grey [lemma, in GC.mesure.grey_card]
ex_gcfree_grey [lemma, in GC.mesure.grey_card]
ex_gcstop_grey [lemma, in GC.mesure.grey_card]
ex_marknode_grey [lemma, in GC.mesure.grey_card]
ex_gccall_grey [lemma, in GC.mesure.grey_card]
ex_alloc_grey [lemma, in GC.mesure.grey_card]
ex_remove_grey [lemma, in GC.mesure.grey_card]
ex_add_grey [lemma, in GC.mesure.grey_card]
ex_init_grey [lemma, in GC.mesure.grey_card]
ex_gcend_white [lemma, in GC.mesure.white_card]
ex_gcfree1_white [lemma, in GC.mesure.white_card]
ex_gcfree_white [lemma, in GC.mesure.white_card]
ex_gcstop_white [lemma, in GC.mesure.white_card]
ex_marknode_white [lemma, in GC.mesure.white_card]
ex_gccall_white [lemma, in GC.mesure.white_card]
ex_alloc_white [lemma, in GC.mesure.white_card]
ex_remove_white [lemma, in GC.mesure.white_card]
ex_add_white [lemma, in GC.mesure.white_card]
ex_init_white [lemma, in GC.mesure.white_card]
ex_gcend_black [lemma, in GC.mesure.black_card]
ex_gcfree1_black [lemma, in GC.mesure.black_card]
ex_gcfree_black [lemma, in GC.mesure.black_card]
ex_gcstop_black [lemma, in GC.mesure.black_card]
ex_marknode_black [lemma, in GC.mesure.black_card]
ex_gccall_black [lemma, in GC.mesure.black_card]
ex_alloc_black [lemma, in GC.mesure.black_card]
ex_remove_black [lemma, in GC.mesure.black_card]
ex_add_black [lemma, in GC.mesure.black_card]
ex_init_black [lemma, in GC.mesure.black_card]
F
fair [definition, in GC.gc.gc]fairness [definition, in GC.logique.LTL]
fairness_lt [lemma, in GC.liveness.until_zero]
fairness_decrease [lemma, in GC.liveness.until_zero]
fairstep_implies_gc_call [lemma, in GC.liveness.notacc_init]
fairstep_implies_initcol [lemma, in GC.liveness.notacc_init]
Fairstr [abbreviation, in GC.liveness.fairstr]
fairstr [section, in GC.liveness.fairstr]
Fairstr [abbreviation, in GC.liveness.notacc_init]
fairstr [definition, in GC.logique.LTL]
Fairstr [abbreviation, in GC.liveness.until_zero]
fairstr [library]
fairstr_eventually_tl [lemma, in GC.liveness.fairstr]
fairstr_eventually [lemma, in GC.liveness.fairstr]
Fair_step [abbreviation, in GC.liveness.fairstr]
Fair_step [abbreviation, in GC.liveness.notacc_init]
fair_step [inductive, in GC.logique.LTL]
Fair_step [abbreviation, in GC.liveness.until_zero]
followed_until [lemma, in GC.logique.LTL]
free [constructor, in GC.gc.parameters]
free_no_grey_but_white [constructor, in GC.gc.gc]
free_white_node [lemma, in GC.safety.rtgreyorblack]
free_or_notfree_notacc_nogrey [definition, in GC.liveness.notfree_notacc]
free1_white_fair [lemma, in GC.liveness.fairstr]
free1_white [constructor, in GC.gc.gc]
G
gc [library]gcc [constructor, in GC.gc.gc]
gccall_notaccess_notaccest [lemma, in GC.lemma_step.lemma_call]
gccall_idem_or_init [lemma, in GC.liveness.notacc_init]
gccall_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
gccall_ex_mesure [lemma, in GC.mesure.mesure]
gccall_mesure [lemma, in GC.mesure.mesure]
gccall_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
gccall_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
gccall_notacces_t [lemma, in GC.liveness.notfree_notacc]
gce [constructor, in GC.gc.gc]
gcend [constructor, in GC.gc.gc]
gcend_grey [lemma, in GC.mesure.grey_card]
gcend_idem_or_init [lemma, in GC.liveness.notacc_init]
gcend_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
gcend_ex_mesure [lemma, in GC.mesure.mesure]
gcend_mesure [lemma, in GC.mesure.mesure]
gcend_nowhite [lemma, in GC.lemma_step.lemma_end]
gcend_nogrey [lemma, in GC.lemma_step.lemma_end]
gcend_white [lemma, in GC.lemma_step.lemma_end]
gcend_notfrees_notfreet [lemma, in GC.lemma_step.lemma_end]
gcend_blacks_blackt [lemma, in GC.lemma_step.lemma_end]
gcend_notgreyt_notgreys [lemma, in GC.lemma_step.lemma_end]
gcend_notaccess_notaccest [lemma, in GC.lemma_step.lemma_end]
gcend_accest_access [lemma, in GC.lemma_step.lemma_end]
gcend_ancestor_col [lemma, in GC.lemma_step.lemma_end]
gcend_white [lemma, in GC.mesure.white_card]
gcend_black [lemma, in GC.mesure.black_card]
gcend_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
gcend_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
gcend_notacces_t [lemma, in GC.liveness.notfree_notacc]
gcf [constructor, in GC.gc.gc]
gcfr [constructor, in GC.gc.gc]
gcfree_grey [lemma, in GC.mesure.grey_card]
gcfree_fair [lemma, in GC.liveness.fairstr]
gcfree_idem_or_init [lemma, in GC.liveness.notacc_init]
gcfree_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
gcfree_ex_mesure [lemma, in GC.mesure.mesure]
gcfree_mesure [lemma, in GC.mesure.mesure]
gcfree_white [lemma, in GC.mesure.white_card]
gcfree_black [lemma, in GC.mesure.black_card]
gcfree_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
gcfree_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
gcfree_greys_greyt [lemma, in GC.lemma_step.lemma_free]
gcfree_notgreys_notgreyt [lemma, in GC.lemma_step.lemma_free]
gcfree_notaccess_notaccest [lemma, in GC.lemma_step.lemma_free]
gcfree_accest_access [lemma, in GC.lemma_step.lemma_free]
gcfree_notblacks_notblackt [lemma, in GC.lemma_step.lemma_free]
gcfree_blacks_blackt [lemma, in GC.lemma_step.lemma_free]
gcfree_nogrey [lemma, in GC.lemma_step.lemma_free]
gcfree_nowhite [lemma, in GC.lemma_step.lemma_free]
gcfree_notacces_t [lemma, in GC.liveness.notfree_notacc]
gcfree1_grey [lemma, in GC.mesure.grey_card]
gcfree1_idem_or_init [lemma, in GC.liveness.notacc_init]
gcfree1_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
gcfree1_ex_mesure [lemma, in GC.mesure.mesure]
gcfree1_mesure [lemma, in GC.mesure.mesure]
gcfree1_notgreys_notgreyt [lemma, in GC.lemma_step.lemma_free1]
gcfree1_greys_greyt [lemma, in GC.lemma_step.lemma_free1]
gcfree1_notblacks_notblackt [lemma, in GC.lemma_step.lemma_free1]
gcfree1_blacks_blackt [lemma, in GC.lemma_step.lemma_free1]
gcfree1_notaccess_notaccest [lemma, in GC.lemma_step.lemma_free1]
gcfree1_accest_access [lemma, in GC.lemma_step.lemma_free1]
gcfree1_nogrey [lemma, in GC.lemma_step.lemma_free1]
gcfree1_nowhite [lemma, in GC.lemma_step.lemma_free1]
gcfree1_white [lemma, in GC.mesure.white_card]
gcfree1_black [lemma, in GC.mesure.black_card]
gcfree1_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
gcfree1_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
gcfree1_notacces_t [lemma, in GC.liveness.notfree_notacc]
gcs [constructor, in GC.gc.gc]
gcstop [constructor, in GC.gc.gc]
gcstop_grey [lemma, in GC.mesure.grey_card]
gcstop_idem_or_init [lemma, in GC.liveness.notacc_init]
gcstop_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
gcstop_nowhite [lemma, in GC.lemma_step.lemma_stop]
gcstop_nogrey [lemma, in GC.lemma_step.lemma_stop]
gcstop_white [lemma, in GC.lemma_step.lemma_stop]
gcstop_notfrees_notfreet [lemma, in GC.lemma_step.lemma_stop]
gcstop_notgreyt_notgreys [lemma, in GC.lemma_step.lemma_stop]
gcstop_blacks_blackt [lemma, in GC.lemma_step.lemma_stop]
gcstop_ancestor_col [lemma, in GC.lemma_step.lemma_stop]
gcstop_notaccess_notaccest [lemma, in GC.lemma_step.lemma_stop]
gcstop_accest_access [lemma, in GC.lemma_step.lemma_stop]
gcstop_ex_mesure [lemma, in GC.mesure.mesure]
gcstop_mesure [lemma, in GC.mesure.mesure]
gcstop_white [lemma, in GC.mesure.white_card]
gcstop_black [lemma, in GC.mesure.black_card]
gcstop_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
gcstop_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
gcstop_notacces_t [lemma, in GC.liveness.notfree_notacc]
gc_end [inductive, in GC.gc.gc]
gc_free1 [inductive, in GC.gc.gc]
gc_free [inductive, in GC.gc.gc]
gc_stop [inductive, in GC.gc.gc]
gc_call [inductive, in GC.gc.gc]
grey [constructor, in GC.gc.parameters]
greynode_notfrees_notfreet [lemma, in GC.lemma_step.lemma_mark]
greynode_card_white [lemma, in GC.mesure.grey_card]
greynode_card_white [lemma, in GC.mesure.white_card]
greynode_black [lemma, in GC.mesure.black_card]
grey_white [lemma, in GC.lemma_step.lemma_mark]
grey_ancestor_col [lemma, in GC.lemma_step.lemma_mark]
grey_card [section, in GC.mesure.grey_card]
grey_sons [constructor, in GC.mesure.parameters_card]
grey_white_sons [inductive, in GC.mesure.parameters_card]
grey_node [constructor, in GC.gc.gc]
grey_node_case [inductive, in GC.gc.gc]
grey_card [library]
g_w_b [definition, in GC.mesure.safe_card]
H
head_str [definition, in GC.logique.LTL]heap [definition, in GC.gc.parameters]
hp [projection, in GC.gc.parameters]
I
implies [definition, in GC.logique.LTL]implies_inf_often [lemma, in GC.logique.LTL]
implies_safety_prop [lemma, in GC.safety.safety]
imp1 [lemma, in GC.safety.noedgeblacktowhite]
imp2 [lemma, in GC.safety.noedgeblacktowhite]
include_card_bis [lemma, in GC.card.card_facts]
include_card [lemma, in GC.card.card_facts]
ind [lemma, in GC.lemma_step.lemma_step]
induct [lemma, in GC.logique.LTL]
infinitely_fairstep [lemma, in GC.liveness.fairstr]
infinitely_often [definition, in GC.logique.LTL]
initcolor_imp_noblack [lemma, in GC.safety.noedgeblacktowhite]
initcolor_notfrees_notfreet [lemma, in GC.lemma_step.lemma_step]
initcol_grey [lemma, in GC.mesure.grey_card]
initcol_white [lemma, in GC.mesure.white_card]
initcol_black [lemma, in GC.mesure.black_card]
init_grey [lemma, in GC.mesure.grey_card]
init_implies_whiteorfree [lemma, in GC.liveness.notacc_init]
init_ex_mesure [lemma, in GC.mesure.mesure]
init_mesure [lemma, in GC.mesure.mesure]
init_state [definition, in GC.gc.gc]
init_marking [definition, in GC.gc.gc]
init_no_greys_but_white [constructor, in GC.gc.gc]
init_color [definition, in GC.gc.gc]
init_white [lemma, in GC.mesure.white_card]
init_invariant_safe [lemma, in GC.safety.safety]
init_inv_conj_mes [lemma, in GC.mesure.safe_card]
init_inv_conj [lemma, in GC.mesure.safe_card]
init_conj_inv [lemma, in GC.mesure.safe_card]
init_black [lemma, in GC.mesure.black_card]
invariant [definition, in GC.logique.LTL]
Invariant [abbreviation, in GC.safety.safety]
Invariant [abbreviation, in GC.mesure.safe_card]
invariant_safety_and [definition, in GC.safety.safety]
invariant_safe [lemma, in GC.safety.safety]
invariant_safety [definition, in GC.safety.safety]
invariant_inv_conj_mes [lemma, in GC.mesure.safe_card]
invariant_inv_conj [lemma, in GC.mesure.safe_card]
invariant_conj_inv [lemma, in GC.mesure.safe_card]
invariant1 [section, in GC.safety.rtgreyorblack]
invariant2 [section, in GC.safety.sweepnogrey]
invariant3 [section, in GC.safety.noedgeblacktowhite]
invariant4 [section, in GC.safety.accnotfree]
invariant5 [section, in GC.safety.nogreyaccnblackn]
inv_clos [lemma, in GC.logique.LTL]
inv_implies_inf_often [lemma, in GC.logique.LTL]
inv_safety_prop [lemma, in GC.safety.safety]
inv_invariant_safety [lemma, in GC.safety.safety]
inv_conj_mes [definition, in GC.mesure.safe_card]
inv_conj [definition, in GC.mesure.safe_card]
inv_black_card [lemma, in GC.mesure.safe_card]
is_true [lemma, in GC.mesure.parameters_card]
is_white [lemma, in GC.mesure.parameters_card]
is_always_followed [definition, in GC.logique.LTL]
is_followed [definition, in GC.logique.LTL]
is_free [definition, in GC.liveness.notfree_notacc]
L
label [inductive, in GC.gc.gc]label_end [constructor, in GC.gc.gc]
label_free1 [constructor, in GC.gc.gc]
label_free [constructor, in GC.gc.gc]
label_stop [constructor, in GC.gc.gc]
label_mark [constructor, in GC.gc.gc]
label_call [constructor, in GC.gc.gc]
label_alloc [constructor, in GC.gc.gc]
label_rem [constructor, in GC.gc.gc]
label_add [constructor, in GC.gc.gc]
leadsto_tx_l_or [lemma, in GC.logique.LTL]
leads_to_via [definition, in GC.logique.LTL]
leads_to [definition, in GC.logique.LTL]
lemma_mark [section, in GC.lemma_step.lemma_mark]
lemma_call [section, in GC.lemma_step.lemma_call]
lemma_stop [section, in GC.lemma_step.lemma_stop]
lemma_alloc [section, in GC.lemma_step.lemma_alloc]
lemma_free1 [section, in GC.lemma_step.lemma_free1]
lemma_end [section, in GC.lemma_step.lemma_end]
lemma_step [section, in GC.lemma_step.lemma_step]
lemma_add [section, in GC.lemma_step.lemma_add]
lemma_free [section, in GC.lemma_step.lemma_free]
lemma_remove [section, in GC.lemma_step.lemma_remove]
lemma_step [library]
lemma_alloc [library]
lemma_remove [library]
lemma_free1 [library]
lemma_stop [library]
lemma_free [library]
lemma_call [library]
lemma_end [library]
lemma_add [library]
lemma_mark [library]
lemme_arith [section, in GC.lib_arith.lemme_arith]
lemme_arith [library]
le_measure [lemma, in GC.liveness.until_zero]
lib_S_pred [section, in GC.lib_arith.lib_S_pred]
lib_minus [section, in GC.lib_arith.lib_minus]
lib_plus [section, in GC.lib_arith.lib_plus]
lib_plus [library]
lib_S_pred [library]
lib_minus [library]
liveness [lemma, in GC.liveness.liveness]
liveness [section, in GC.liveness.liveness]
liveness [library]
LTL [section, in GC.logique.LTL]
LTL [library]
LTL.fair [variable, in GC.logique.LTL]
LTL.init_state [variable, in GC.logique.LTL]
LTL.label [variable, in GC.logique.LTL]
LTL.state [variable, in GC.logique.LTL]
LTL.transition [variable, in GC.logique.LTL]
ltv_equiv_ltv [lemma, in GC.logique.LTL]
M
mar [constructor, in GC.gc.gc]mark [constructor, in GC.gc.parameters]
marking [definition, in GC.gc.parameters]
marking_add [definition, in GC.gc.gc]
marknode_notaccess_notaccest [lemma, in GC.lemma_step.lemma_mark]
marknode_accest_access [lemma, in GC.lemma_step.lemma_mark]
marknode_notfrees_notfreet [lemma, in GC.lemma_step.lemma_mark]
marknode_fair [lemma, in GC.liveness.fairstr]
marknode_idem_or_init [lemma, in GC.liveness.notacc_init]
marknode_ex_mesure [lemma, in GC.mesure.mesure]
marknode_mesure [lemma, in GC.mesure.mesure]
marknode_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
marknode_notacces_t [lemma, in GC.liveness.notfree_notacc]
mark_white [lemma, in GC.lemma_step.lemma_mark]
mark_ancestor_col [lemma, in GC.lemma_step.lemma_mark]
mark_ancestor [lemma, in GC.lemma_step.lemma_mark]
mark_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
mark_node [inductive, in GC.gc.gc]
mark_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
measure [definition, in GC.liveness.until_zero]
measureO_whiteO [lemma, in GC.liveness.until_zero]
measureO_greyO [lemma, in GC.liveness.until_zero]
measure_unicity [lemma, in GC.mesure.unicite_mes]
measure_until_zero_on_run [lemma, in GC.liveness.until_zero]
measure_until_zero [lemma, in GC.liveness.until_zero]
measure_trivial_bis [lemma, in GC.liveness.until_zero]
measure_trivial [lemma, in GC.liveness.until_zero]
mesur [constructor, in GC.mesure.mesure]
mesure [inductive, in GC.mesure.mesure]
mesure [section, in GC.mesure.mesure]
mesure [library]
minus_pred [lemma, in GC.lib_arith.lib_minus]
mk [projection, in GC.gc.parameters]
mn_exist_grey [constructor, in GC.gc.gc]
mutate [constructor, in GC.gc.parameters]
N
next [definition, in GC.logique.LTL]node [axiom, in GC.gc.parameters]
noedgeblacktowhite [library]
nogreyaccnblackn [library]
nogrey_accn_imp_blackn [definition, in GC.gc.gc]
nogrey_accn_imp_blackn_step [lemma, in GC.safety.safety]
nogrey_accn_imp_blackn_gcend [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcfree1 [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcfree [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcstop [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_marknode [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gccall [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_alloc [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_removeedge [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_addedge [lemma, in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_init [lemma, in GC.safety.nogreyaccnblackn]
none [constructor, in GC.logique.LTL]
none_or_one_step [inductive, in GC.logique.LTL]
none_or_one_decrease [lemma, in GC.liveness.until_zero]
None_or_one_step [abbreviation, in GC.liveness.until_zero]
notacc_white_init_formula [definition, in GC.liveness.notacc_init]
notacc_black_nomeasure_formula [definition, in GC.liveness.notacc_init]
notacc_white_init [definition, in GC.liveness.notacc_init]
notacc_black_nomeasure [definition, in GC.liveness.notacc_init]
notacc_init [section, in GC.liveness.notacc_init]
notacc_white_nogrey_formula [definition, in GC.liveness.notacc_white_nogrey]
notacc_white_nogrey_or_free [definition, in GC.liveness.notacc_white_nogrey]
notacc_white_nogrey [definition, in GC.liveness.notacc_white_nogrey]
notacc_white_nogrey [section, in GC.liveness.notacc_white_nogrey]
notacc_black_nomeasure_formula [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_formula [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_nowhite_formula [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_exwhite_formula [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_exwhite [definition, in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey [section, in GC.liveness.notacc_black_nogrey]
notacc_white_nogrey_eventually_free [lemma, in GC.liveness.notacc_white_ancestor]
notacc_white_reach_formula [definition, in GC.liveness.notacc_white_ancestor]
notacc_white_exgrey_reach_formula [definition, in GC.liveness.notacc_white_ancestor]
notacc_white_reach [definition, in GC.liveness.notacc_white_ancestor]
notacc_white_exgrey_reach [definition, in GC.liveness.notacc_white_ancestor]
notacc_white_ancestor [section, in GC.liveness.notacc_white_ancestor]
notacc_init [library]
notacc_white_nogrey [library]
notacc_white_ancestor [library]
notacc_black_nogrey [library]
noteqmar_noteqnod [lemma, in GC.gc.parameters]
notfree [definition, in GC.liveness.notfree_notacc]
notfree_notacces_unless_isfree [lemma, in GC.liveness.notfree_notacc]
notfree_notacces [definition, in GC.liveness.notfree_notacc]
notfree_notacc [section, in GC.liveness.notfree_notacc]
notfree_notacc [library]
not_true_and_white [lemma, in GC.mesure.parameters_card]
no_grey_but_white_fair [lemma, in GC.liveness.fairstr]
no_edge_black_to_white_bis [definition, in GC.gc.gc]
no_edge_black_to_white [definition, in GC.gc.gc]
no_edge_black_to_white_gcend [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree1 [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree_bis [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcstop [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_marknode [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gccall [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_alloc [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_removeedge [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_addedge [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_init [lemma, in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_inv [lemma, in GC.safety.safety]
no_edge_black_to_white_step [lemma, in GC.safety.safety]
null_measure_grey_white [lemma, in GC.liveness.notacc_init]
O
once_equiv_once [lemma, in GC.logique.LTL]once_eventually [lemma, in GC.logique.LTL]
once_until [definition, in GC.logique.LTL]
once_always [definition, in GC.logique.LTL]
once_until_zero [lemma, in GC.liveness.until_zero]
Once_always [abbreviation, in GC.liveness.until_zero]
one [constructor, in GC.logique.LTL]
one_step_leads_to [lemma, in GC.logique.LTL]
P
parameters [section, in GC.gc.parameters]parameters [library]
parameters_card [section, in GC.mesure.parameters_card]
parameters_card [library]
plus_pred [lemma, in GC.lib_arith.lib_plus]
plus_O_O [lemma, in GC.lib_arith.lib_plus]
plus_O [lemma, in GC.lib_arith.lib_plus]
plus_S_pred [lemma, in GC.lib_arith.lib_plus]
positive_measure [definition, in GC.liveness.until_zero]
pred_S [lemma, in GC.lib_arith.lib_S_pred]
pred_S_minus [lemma, in GC.lib_arith.lib_minus]
pred_plus_minus [lemma, in GC.lib_arith.lib_plus]
pred_plus_S [lemma, in GC.lib_arith.lib_plus]
prop_dec2 [definition, in GC.card.card_facts]
prop_dec [definition, in GC.card.card_facts]
R
re [constructor, in GC.gc.gc]Reachable [abbreviation, in GC.lemma_step.lemma_mark]
Reachable [abbreviation, in GC.lemma_step.lemma_stop]
Reachable [abbreviation, in GC.lemma_step.lemma_alloc]
Reachable [abbreviation, in GC.lemma_step.lemma_end]
Reachable [abbreviation, in GC.lemma_step.lemma_add]
Reachable [abbreviation, in GC.liveness.notacc_white_ancestor]
reachable [inductive, in GC.reachable.reachable]
reachable [section, in GC.reachable.reachable]
Reachable [abbreviation, in GC.lemma_step.lemma_remove]
reachable [library]
reachable_edge [constructor, in GC.reachable.reachable]
reachable_init [constructor, in GC.reachable.reachable]
reachable.h [variable, in GC.reachable.reachable]
reachable.N [variable, in GC.reachable.reachable]
reachable.root [variable, in GC.reachable.reachable]
reach_true_reach [lemma, in GC.reachable.reachable]
reach_notacc [lemma, in GC.reachable.reachable]
reach_acc [lemma, in GC.reachable.reachable]
remove [definition, in GC.gc.gc]
removeedge_notacces_t [lemma, in GC.liveness.notfree_notacc]
remove_grey [lemma, in GC.mesure.grey_card]
remove_idem_or_init [lemma, in GC.liveness.notacc_init]
remove_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
remove_ex_mesure [lemma, in GC.mesure.mesure]
remove_mesure [lemma, in GC.mesure.mesure]
remove_to_node [constructor, in GC.gc.gc]
remove_edge [inductive, in GC.gc.gc]
remove_white [lemma, in GC.mesure.white_card]
remove_black [lemma, in GC.mesure.black_card]
remove_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
remove_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
remove_ancestor_col [lemma, in GC.lemma_step.lemma_remove]
remove_ancestor [lemma, in GC.lemma_step.lemma_remove]
remove_nowhite [lemma, in GC.lemma_step.lemma_remove]
remove_nogrey [lemma, in GC.lemma_step.lemma_remove]
remove_white [lemma, in GC.lemma_step.lemma_remove]
remove_notaccess_notaccest [lemma, in GC.lemma_step.lemma_remove]
remove_notgreyt_notgreys [lemma, in GC.lemma_step.lemma_remove]
remove_blacks_blackt [lemma, in GC.lemma_step.lemma_remove]
remove_notfrees_notfreet [lemma, in GC.lemma_step.lemma_remove]
remove_accest_access [lemma, in GC.lemma_step.lemma_remove]
rt [axiom, in GC.gc.parameters]
rtgreyorblack [library]
rt_grey_or_black [definition, in GC.gc.gc]
rt_grey_or_black_inv [lemma, in GC.safety.safety]
rt_grey_or_black_step [lemma, in GC.safety.safety]
rt_grey_or_black_gcend [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_gcfree1 [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_gcfree [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_gcstop [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_marknode [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_gccall [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_alloc [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_removeedge [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_addedge [lemma, in GC.safety.rtgreyorblack]
rt_grey_or_black_init [lemma, in GC.safety.rtgreyorblack]
Run [abbreviation, in GC.liveness.fairstr]
Run [abbreviation, in GC.liveness.liveness]
run [definition, in GC.logique.LTL]
Run [abbreviation, in GC.safety.safety]
Run [abbreviation, in GC.liveness.until_zero]
Run [abbreviation, in GC.mesure.safe_card]
run_fairstr_always [lemma, in GC.liveness.liveness]
S
Safe [abbreviation, in GC.liveness.fairstr]Safe [abbreviation, in GC.liveness.liveness]
safe [definition, in GC.logique.LTL]
Safe [abbreviation, in GC.safety.safety]
Safe [abbreviation, in GC.mesure.safe_card]
safeP_safeQ_stream [lemma, in GC.logique.LTL]
safeP_safeQ [lemma, in GC.logique.LTL]
safety [lemma, in GC.logique.LTL]
safety [section, in GC.safety.safety]
safety [library]
safety_prop_safe [lemma, in GC.safety.safety]
safety_prop [definition, in GC.safety.safety]
safe_inv_gwb_mesure [lemma, in GC.liveness.liveness]
safe_inv_and_gwb [lemma, in GC.liveness.liveness]
safe_and_state [lemma, in GC.logique.LTL]
safe_and [lemma, in GC.logique.LTL]
safe_sweep_no_greys [lemma, in GC.safety.safety]
safe_mesure [lemma, in GC.mesure.safe_card]
safe_inv_conj_mes [lemma, in GC.mesure.safe_card]
safe_gwb [lemma, in GC.mesure.safe_card]
safe_card_grey [lemma, in GC.mesure.safe_card]
safe_inv_conj [lemma, in GC.mesure.safe_card]
safe_card_white [lemma, in GC.mesure.safe_card]
safe_conj_inv [lemma, in GC.mesure.safe_card]
safe_card_black [lemma, in GC.mesure.safe_card]
safe_card [section, in GC.mesure.safe_card]
safe_card [library]
specification [section, in GC.gc.gc]
state [record, in GC.gc.parameters]
State_formula [abbreviation, in GC.logique.well_founded]
State_formula [abbreviation, in GC.gc.gc]
state_formula [definition, in GC.logique.LTL]
State_formula [abbreviation, in GC.safety.safety]
State_formula [abbreviation, in GC.liveness.until_zero]
State_formula [abbreviation, in GC.mesure.safe_card]
State_formula [abbreviation, in GC.liveness.notfree_notacc]
state2stream_formula [definition, in GC.logique.LTL]
Step [abbreviation, in GC.liveness.notacc_init]
Step [abbreviation, in GC.liveness.notacc_white_nogrey]
step [inductive, in GC.logique.LTL]
Step [abbreviation, in GC.safety.safety]
Step [abbreviation, in GC.liveness.until_zero]
Step [abbreviation, in GC.mesure.safe_card]
Step [abbreviation, in GC.liveness.notacc_black_nogrey]
Step [abbreviation, in GC.liveness.notacc_white_ancestor]
Step [abbreviation, in GC.liveness.notfree_notacc]
step_initcolor [lemma, in GC.liveness.notacc_init]
step_idem_or_init [lemma, in GC.liveness.notacc_init]
step_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
step_decrease [lemma, in GC.liveness.until_zero]
step_ex_mesure [lemma, in GC.mesure.safe_card]
step_mesure [lemma, in GC.mesure.safe_card]
step_grey_card [lemma, in GC.mesure.safe_card]
step_white_card [lemma, in GC.mesure.safe_card]
step_black_card [lemma, in GC.mesure.safe_card]
step_notacc_black_nogrey [lemma, in GC.liveness.notacc_black_nogrey]
step_notacc_white_reach [lemma, in GC.liveness.notacc_white_ancestor]
step_notacces_t [lemma, in GC.liveness.notfree_notacc]
Stream [abbreviation, in GC.logique.well_founded]
Stream [abbreviation, in GC.liveness.fairstr]
Stream [abbreviation, in GC.liveness.notacc_init]
Stream [abbreviation, in GC.liveness.notacc_white_nogrey]
Stream [abbreviation, in GC.liveness.liveness]
stream [inductive, in GC.logique.LTL]
Stream [abbreviation, in GC.safety.safety]
Stream [abbreviation, in GC.liveness.until_zero]
Stream [abbreviation, in GC.mesure.safe_card]
Stream [abbreviation, in GC.liveness.notacc_black_nogrey]
Stream [abbreviation, in GC.liveness.notacc_white_ancestor]
Stream [abbreviation, in GC.liveness.notfree_notacc]
Stream_formula [abbreviation, in GC.liveness.notacc_init]
Stream_formula [abbreviation, in GC.liveness.notacc_white_nogrey]
Stream_formula [abbreviation, in GC.liveness.liveness]
stream_formula [definition, in GC.logique.LTL]
Stream_formula [abbreviation, in GC.safety.safety]
Stream_formula [abbreviation, in GC.mesure.safe_card]
Stream_formula [abbreviation, in GC.liveness.notacc_black_nogrey]
Stream_formula [abbreviation, in GC.liveness.notacc_white_ancestor]
Stream_formula [abbreviation, in GC.liveness.notfree_notacc]
Strong_fairstr [abbreviation, in GC.liveness.notacc_init]
Strong_fairstr [abbreviation, in GC.liveness.liveness]
strong_fairstr_implies_fairstr [lemma, in GC.logique.LTL]
strong_fairstr [definition, in GC.logique.LTL]
sweep [constructor, in GC.gc.parameters]
sweepnogrey [library]
sweep_no_greys [definition, in GC.gc.gc]
sweep_no_greys_inv [lemma, in GC.safety.safety]
sweep_no_greys_step [lemma, in GC.safety.safety]
sweep_no_greys_gcend [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_gcfree1 [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_gcfree [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_gcstop [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_marknode [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_gccall [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_alloc [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_removeedge [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_addedge [lemma, in GC.safety.sweepnogrey]
sweep_no_greys_init [lemma, in GC.safety.sweepnogrey]
S_pred [lemma, in GC.lib_arith.lib_S_pred]
T
tl_str [definition, in GC.logique.LTL]Trace [abbreviation, in GC.liveness.notacc_init]
Trace [abbreviation, in GC.liveness.notacc_white_nogrey]
Trace [abbreviation, in GC.liveness.liveness]
trace [definition, in GC.logique.LTL]
Trace [abbreviation, in GC.liveness.until_zero]
Trace [abbreviation, in GC.liveness.notacc_black_nogrey]
Trace [abbreviation, in GC.liveness.notacc_white_ancestor]
Trace [abbreviation, in GC.liveness.notfree_notacc]
transition [inductive, in GC.gc.gc]
trivial [lemma, in GC.lemma_step.lemma_step]
trivial_unicity_bis [lemma, in GC.liveness.until_zero]
trivial_unicity [lemma, in GC.liveness.until_zero]
U
unicite_mesure [section, in GC.mesure.unicite_mes]unicite_mes [library]
unicity_card [lemma, in GC.card.card]
unless [inductive, in GC.logique.LTL]
unless_t [constructor, in GC.logique.LTL]
unless_h [constructor, in GC.logique.LTL]
until [inductive, in GC.logique.LTL]
until_no_measure_init [lemma, in GC.liveness.notacc_init]
until_idem_or_free [lemma, in GC.liveness.notacc_white_nogrey]
until_eventually [lemma, in GC.logique.LTL]
until_implies_until [lemma, in GC.logique.LTL]
until_trans [lemma, in GC.logique.LTL]
until_or [lemma, in GC.logique.LTL]
until_implies_until_state [lemma, in GC.logique.LTL]
until_implies_until_stream [lemma, in GC.logique.LTL]
until_t [constructor, in GC.logique.LTL]
until_h [constructor, in GC.logique.LTL]
until_zero [lemma, in GC.liveness.until_zero]
until_zero [section, in GC.liveness.until_zero]
until_no_measure [lemma, in GC.liveness.notacc_black_nogrey]
until_no_white [lemma, in GC.liveness.notacc_black_nogrey]
until_no_grey_without_reach [lemma, in GC.liveness.notacc_white_ancestor]
until_no_grey [lemma, in GC.liveness.notacc_white_ancestor]
until_free_or_nogrey [lemma, in GC.liveness.notfree_notacc]
until_zero [library]
update [definition, in GC.card.card]
updatecolor_blacks_blackt [lemma, in GC.lemma_step.lemma_free]
update_N [definition, in GC.card.card_facts]
update_M [definition, in GC.card.card_facts]
update_heap [definition, in GC.mesure.parameters_card]
update_init_color [definition, in GC.liveness.fairstr]
update_color_marknode [definition, in GC.liveness.fairstr]
update_color [definition, in GC.gc.gc]
W
well_founded.state [variable, in GC.logique.well_founded]well_founded.Alpha [variable, in GC.logique.well_founded]
well_founded [section, in GC.logique.well_founded]
well_founded [library]
wf_leadsto_rule [lemma, in GC.logique.well_founded]
wf_leadsto [lemma, in GC.logique.well_founded]
Wf_leadsto_rule [abbreviation, in GC.liveness.until_zero]
white [constructor, in GC.gc.parameters]
white_notacc_nogrey_until_eventually_free [lemma, in GC.liveness.notacc_white_nogrey]
white_card [section, in GC.mesure.white_card]
white_card [library]
Variable Index
C
cardinal.A [in GC.card.card]cardinal.B [in GC.card.card]
cardinal.P [in GC.card.card]
card_facts.C [in GC.card.card_facts]
card_facts.B [in GC.card.card_facts]
card_facts.A [in GC.card.card_facts]
L
LTL.fair [in GC.logique.LTL]LTL.init_state [in GC.logique.LTL]
LTL.label [in GC.logique.LTL]
LTL.state [in GC.logique.LTL]
LTL.transition [in GC.logique.LTL]
R
reachable.h [in GC.reachable.reachable]reachable.N [in GC.reachable.reachable]
reachable.root [in GC.reachable.reachable]
W
well_founded.state [in GC.logique.well_founded]well_founded.Alpha [in GC.logique.well_founded]
Library Index
A
accnotfreeB
black_cardC
cardcard_facts
F
fairstrG
gcgrey_card
L
lemma_steplemma_alloc
lemma_remove
lemma_free1
lemma_stop
lemma_free
lemma_call
lemma_end
lemma_add
lemma_mark
lemme_arith
lib_plus
lib_S_pred
lib_minus
liveness
LTL
M
mesureN
noedgeblacktowhitenogreyaccnblackn
notacc_init
notacc_white_nogrey
notacc_white_ancestor
notacc_black_nogrey
notfree_notacc
P
parametersparameters_card
R
reachablertgreyorblack
S
safetysafe_card
sweepnogrey
U
unicite_mesuntil_zero
W
well_foundedwhite_card
Lemma Index
A
absurd [in GC.safety.sweepnogrey]acc_imp_notfree_gcend [in GC.safety.accnotfree]
acc_imp_notfree_gcfree1 [in GC.safety.accnotfree]
acc_imp_notfree_gcfree [in GC.safety.accnotfree]
acc_imp_notfree_gcstop [in GC.safety.accnotfree]
acc_imp_notfree_marknode [in GC.safety.accnotfree]
acc_imp_notfree_gccall [in GC.safety.accnotfree]
acc_imp_notfree_alloc [in GC.safety.accnotfree]
acc_imp_notfree_removeedge [in GC.safety.accnotfree]
acc_imp_notfree_addedge [in GC.safety.accnotfree]
acc_imp_notfree_init [in GC.safety.accnotfree]
acc_imp_notfree_step [in GC.safety.safety]
addedge_notacces_t [in GC.liveness.notfree_notacc]
add_grey [in GC.mesure.grey_card]
add_idem_or_init [in GC.liveness.notacc_init]
add_idem_or_free [in GC.liveness.notacc_white_nogrey]
add_ex_mesure [in GC.mesure.mesure]
add_mesure [in GC.mesure.mesure]
add_white [in GC.mesure.white_card]
add_black [in GC.mesure.black_card]
add_white_nogrey [in GC.lemma_step.lemma_add]
add_notfrees_notfreet [in GC.lemma_step.lemma_add]
add_blacks_blackt [in GC.lemma_step.lemma_add]
add_notgreyt_notgreys [in GC.lemma_step.lemma_add]
add_ancestor_col [in GC.lemma_step.lemma_add]
add_ancestor [in GC.lemma_step.lemma_add]
add_notaccess_notaccest [in GC.lemma_step.lemma_add]
add_accest_access [in GC.lemma_step.lemma_add]
add_nowhite [in GC.lemma_step.lemma_add]
add_nogrey [in GC.lemma_step.lemma_add]
add_notacc_white [in GC.lemma_step.lemma_add]
add_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
add_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
alloc_grey [in GC.mesure.grey_card]
alloc_idem_or_init [in GC.liveness.notacc_init]
alloc_idem_or_free [in GC.liveness.notacc_white_nogrey]
alloc_ancestor_col [in GC.lemma_step.lemma_alloc]
alloc_ancestor [in GC.lemma_step.lemma_alloc]
alloc_nowhite [in GC.lemma_step.lemma_alloc]
alloc_nogrey [in GC.lemma_step.lemma_alloc]
alloc_whites_whitet [in GC.lemma_step.lemma_alloc]
alloc_notwhites_notwhitet [in GC.lemma_step.lemma_alloc]
alloc_notgreys_notgreyt [in GC.lemma_step.lemma_alloc]
alloc_greys_greyt [in GC.lemma_step.lemma_alloc]
alloc_notgreyt_notgreys [in GC.lemma_step.lemma_alloc]
alloc_accest_access [in GC.lemma_step.lemma_alloc]
alloc_blacks_blackt [in GC.lemma_step.lemma_alloc]
alloc_ex_mesure [in GC.mesure.mesure]
alloc_mesure [in GC.mesure.mesure]
alloc_white [in GC.mesure.white_card]
alloc_black [in GC.mesure.black_card]
alloc_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
alloc_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
alloc_notacces_t [in GC.liveness.notfree_notacc]
always_fairstep [in GC.liveness.fairstr]
always_exist_fairstep [in GC.liveness.fairstr]
always_and_inv_g_w_b [in GC.liveness.liveness]
always_unless [in GC.logique.LTL]
always_and_and [in GC.logique.LTL]
always_and_bis [in GC.logique.LTL]
always_and [in GC.logique.LTL]
always_implies_always_state [in GC.logique.LTL]
always_always_implies_always [in GC.logique.LTL]
always_imp_always [in GC.logique.LTL]
always_fairstr [in GC.logique.LTL]
always_trace [in GC.logique.LTL]
always_always_bis [in GC.logique.LTL]
always_always [in GC.logique.LTL]
always_implies_always_stream [in GC.logique.LTL]
always_implies_always [in GC.logique.LTL]
always_P [in GC.logique.LTL]
always_one_step_leads_to [in GC.logique.LTL]
always_on_run [in GC.logique.LTL]
always_nogrey_accn_imp_blackn [in GC.safety.safety]
always_invariant_safety_and [in GC.safety.safety]
always_inv_safety [in GC.safety.safety]
always_sweep_no_grey [in GC.safety.safety]
always_eventually_white_until_zero_trace [in GC.liveness.until_zero]
always_eventually_grey_until_zero_trace [in GC.liveness.until_zero]
always_mesure [in GC.mesure.safe_card]
always_gwb [in GC.mesure.safe_card]
always_card_grey [in GC.mesure.safe_card]
always_card_white [in GC.mesure.safe_card]
always_card_black [in GC.mesure.safe_card]
always_notfree_notacces_unless_isfree [in GC.liveness.notfree_notacc]
and_always_state [in GC.logique.LTL]
and_always [in GC.logique.LTL]
and_exist [in GC.liveness.until_zero]
B
black_grey_node [in GC.safety.noedgeblacktowhite]black_grey_node [in GC.safety.rtgreyorblack]
C
call_gc_fair [in GC.liveness.fairstr]call_exist_grey_fair [in GC.liveness.fairstr]
card_rem [in GC.card.card]
card_inv [in GC.card.card]
card_grey_marknode [in GC.mesure.grey_card]
card_grey_rt [in GC.liveness.liveness]
card_white_marknode [in GC.mesure.white_card]
cases_marknode [in GC.gc.gc]
color_node [in GC.lemma_step.lemma_step]
D
def_equiv [in GC.liveness.liveness]dif [in GC.card.card]
dif2 [in GC.card.card]
E
eqnm_eqSnSm [in GC.lib_arith.lib_S_pred]equivalent_def [in GC.liveness.notacc_white_ancestor]
equiv_def2 [in GC.liveness.notacc_black_nogrey]
equiv_def [in GC.liveness.notacc_black_nogrey]
eq_dec_color [in GC.gc.parameters]
eventually_until [in GC.logique.LTL]
eventually_implies_eventually [in GC.logique.LTL]
eventually_white_until_zero [in GC.liveness.until_zero]
eventually_white_until_zero_trace [in GC.liveness.until_zero]
eventually_grey_until_zero [in GC.liveness.until_zero]
eventually_grey_until_zero_trace [in GC.liveness.until_zero]
eventually_measure_until_zero_on_run [in GC.liveness.until_zero]
eventually_measure_until_zero_trace_bis [in GC.liveness.until_zero]
eventually_measure_until_zero [in GC.liveness.until_zero]
eventually_measure_until_zero_trace [in GC.liveness.until_zero]
exist_updated_N [in GC.card.card_facts]
exist_updated_M [in GC.card.card_facts]
exist_updated [in GC.card.card]
exist_updated_heap [in GC.mesure.parameters_card]
exist_update_color [in GC.liveness.fairstr]
exist_update_init_color [in GC.liveness.fairstr]
exist_grey_node [in GC.liveness.fairstr]
ex_gcend_grey [in GC.mesure.grey_card]
ex_gcfree1_grey [in GC.mesure.grey_card]
ex_gcfree_grey [in GC.mesure.grey_card]
ex_gcstop_grey [in GC.mesure.grey_card]
ex_marknode_grey [in GC.mesure.grey_card]
ex_gccall_grey [in GC.mesure.grey_card]
ex_alloc_grey [in GC.mesure.grey_card]
ex_remove_grey [in GC.mesure.grey_card]
ex_add_grey [in GC.mesure.grey_card]
ex_init_grey [in GC.mesure.grey_card]
ex_gcend_white [in GC.mesure.white_card]
ex_gcfree1_white [in GC.mesure.white_card]
ex_gcfree_white [in GC.mesure.white_card]
ex_gcstop_white [in GC.mesure.white_card]
ex_marknode_white [in GC.mesure.white_card]
ex_gccall_white [in GC.mesure.white_card]
ex_alloc_white [in GC.mesure.white_card]
ex_remove_white [in GC.mesure.white_card]
ex_add_white [in GC.mesure.white_card]
ex_init_white [in GC.mesure.white_card]
ex_gcend_black [in GC.mesure.black_card]
ex_gcfree1_black [in GC.mesure.black_card]
ex_gcfree_black [in GC.mesure.black_card]
ex_gcstop_black [in GC.mesure.black_card]
ex_marknode_black [in GC.mesure.black_card]
ex_gccall_black [in GC.mesure.black_card]
ex_alloc_black [in GC.mesure.black_card]
ex_remove_black [in GC.mesure.black_card]
ex_add_black [in GC.mesure.black_card]
ex_init_black [in GC.mesure.black_card]
F
fairness_lt [in GC.liveness.until_zero]fairness_decrease [in GC.liveness.until_zero]
fairstep_implies_gc_call [in GC.liveness.notacc_init]
fairstep_implies_initcol [in GC.liveness.notacc_init]
fairstr_eventually_tl [in GC.liveness.fairstr]
fairstr_eventually [in GC.liveness.fairstr]
followed_until [in GC.logique.LTL]
free_white_node [in GC.safety.rtgreyorblack]
free1_white_fair [in GC.liveness.fairstr]
G
gccall_notaccess_notaccest [in GC.lemma_step.lemma_call]gccall_idem_or_init [in GC.liveness.notacc_init]
gccall_idem_or_free [in GC.liveness.notacc_white_nogrey]
gccall_ex_mesure [in GC.mesure.mesure]
gccall_mesure [in GC.mesure.mesure]
gccall_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
gccall_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
gccall_notacces_t [in GC.liveness.notfree_notacc]
gcend_grey [in GC.mesure.grey_card]
gcend_idem_or_init [in GC.liveness.notacc_init]
gcend_idem_or_free [in GC.liveness.notacc_white_nogrey]
gcend_ex_mesure [in GC.mesure.mesure]
gcend_mesure [in GC.mesure.mesure]
gcend_nowhite [in GC.lemma_step.lemma_end]
gcend_nogrey [in GC.lemma_step.lemma_end]
gcend_white [in GC.lemma_step.lemma_end]
gcend_notfrees_notfreet [in GC.lemma_step.lemma_end]
gcend_blacks_blackt [in GC.lemma_step.lemma_end]
gcend_notgreyt_notgreys [in GC.lemma_step.lemma_end]
gcend_notaccess_notaccest [in GC.lemma_step.lemma_end]
gcend_accest_access [in GC.lemma_step.lemma_end]
gcend_ancestor_col [in GC.lemma_step.lemma_end]
gcend_white [in GC.mesure.white_card]
gcend_black [in GC.mesure.black_card]
gcend_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
gcend_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
gcend_notacces_t [in GC.liveness.notfree_notacc]
gcfree_grey [in GC.mesure.grey_card]
gcfree_fair [in GC.liveness.fairstr]
gcfree_idem_or_init [in GC.liveness.notacc_init]
gcfree_idem_or_free [in GC.liveness.notacc_white_nogrey]
gcfree_ex_mesure [in GC.mesure.mesure]
gcfree_mesure [in GC.mesure.mesure]
gcfree_white [in GC.mesure.white_card]
gcfree_black [in GC.mesure.black_card]
gcfree_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
gcfree_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
gcfree_greys_greyt [in GC.lemma_step.lemma_free]
gcfree_notgreys_notgreyt [in GC.lemma_step.lemma_free]
gcfree_notaccess_notaccest [in GC.lemma_step.lemma_free]
gcfree_accest_access [in GC.lemma_step.lemma_free]
gcfree_notblacks_notblackt [in GC.lemma_step.lemma_free]
gcfree_blacks_blackt [in GC.lemma_step.lemma_free]
gcfree_nogrey [in GC.lemma_step.lemma_free]
gcfree_nowhite [in GC.lemma_step.lemma_free]
gcfree_notacces_t [in GC.liveness.notfree_notacc]
gcfree1_grey [in GC.mesure.grey_card]
gcfree1_idem_or_init [in GC.liveness.notacc_init]
gcfree1_idem_or_free [in GC.liveness.notacc_white_nogrey]
gcfree1_ex_mesure [in GC.mesure.mesure]
gcfree1_mesure [in GC.mesure.mesure]
gcfree1_notgreys_notgreyt [in GC.lemma_step.lemma_free1]
gcfree1_greys_greyt [in GC.lemma_step.lemma_free1]
gcfree1_notblacks_notblackt [in GC.lemma_step.lemma_free1]
gcfree1_blacks_blackt [in GC.lemma_step.lemma_free1]
gcfree1_notaccess_notaccest [in GC.lemma_step.lemma_free1]
gcfree1_accest_access [in GC.lemma_step.lemma_free1]
gcfree1_nogrey [in GC.lemma_step.lemma_free1]
gcfree1_nowhite [in GC.lemma_step.lemma_free1]
gcfree1_white [in GC.mesure.white_card]
gcfree1_black [in GC.mesure.black_card]
gcfree1_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
gcfree1_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
gcfree1_notacces_t [in GC.liveness.notfree_notacc]
gcstop_grey [in GC.mesure.grey_card]
gcstop_idem_or_init [in GC.liveness.notacc_init]
gcstop_idem_or_free [in GC.liveness.notacc_white_nogrey]
gcstop_nowhite [in GC.lemma_step.lemma_stop]
gcstop_nogrey [in GC.lemma_step.lemma_stop]
gcstop_white [in GC.lemma_step.lemma_stop]
gcstop_notfrees_notfreet [in GC.lemma_step.lemma_stop]
gcstop_notgreyt_notgreys [in GC.lemma_step.lemma_stop]
gcstop_blacks_blackt [in GC.lemma_step.lemma_stop]
gcstop_ancestor_col [in GC.lemma_step.lemma_stop]
gcstop_notaccess_notaccest [in GC.lemma_step.lemma_stop]
gcstop_accest_access [in GC.lemma_step.lemma_stop]
gcstop_ex_mesure [in GC.mesure.mesure]
gcstop_mesure [in GC.mesure.mesure]
gcstop_white [in GC.mesure.white_card]
gcstop_black [in GC.mesure.black_card]
gcstop_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
gcstop_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
gcstop_notacces_t [in GC.liveness.notfree_notacc]
greynode_notfrees_notfreet [in GC.lemma_step.lemma_mark]
greynode_card_white [in GC.mesure.grey_card]
greynode_card_white [in GC.mesure.white_card]
greynode_black [in GC.mesure.black_card]
grey_white [in GC.lemma_step.lemma_mark]
grey_ancestor_col [in GC.lemma_step.lemma_mark]
I
implies_inf_often [in GC.logique.LTL]implies_safety_prop [in GC.safety.safety]
imp1 [in GC.safety.noedgeblacktowhite]
imp2 [in GC.safety.noedgeblacktowhite]
include_card_bis [in GC.card.card_facts]
include_card [in GC.card.card_facts]
ind [in GC.lemma_step.lemma_step]
induct [in GC.logique.LTL]
infinitely_fairstep [in GC.liveness.fairstr]
initcolor_imp_noblack [in GC.safety.noedgeblacktowhite]
initcolor_notfrees_notfreet [in GC.lemma_step.lemma_step]
initcol_grey [in GC.mesure.grey_card]
initcol_white [in GC.mesure.white_card]
initcol_black [in GC.mesure.black_card]
init_grey [in GC.mesure.grey_card]
init_implies_whiteorfree [in GC.liveness.notacc_init]
init_ex_mesure [in GC.mesure.mesure]
init_mesure [in GC.mesure.mesure]
init_white [in GC.mesure.white_card]
init_invariant_safe [in GC.safety.safety]
init_inv_conj_mes [in GC.mesure.safe_card]
init_inv_conj [in GC.mesure.safe_card]
init_conj_inv [in GC.mesure.safe_card]
init_black [in GC.mesure.black_card]
invariant_safe [in GC.safety.safety]
invariant_inv_conj_mes [in GC.mesure.safe_card]
invariant_inv_conj [in GC.mesure.safe_card]
invariant_conj_inv [in GC.mesure.safe_card]
inv_clos [in GC.logique.LTL]
inv_implies_inf_often [in GC.logique.LTL]
inv_safety_prop [in GC.safety.safety]
inv_invariant_safety [in GC.safety.safety]
inv_black_card [in GC.mesure.safe_card]
is_true [in GC.mesure.parameters_card]
is_white [in GC.mesure.parameters_card]
L
leadsto_tx_l_or [in GC.logique.LTL]le_measure [in GC.liveness.until_zero]
liveness [in GC.liveness.liveness]
ltv_equiv_ltv [in GC.logique.LTL]
M
marknode_notaccess_notaccest [in GC.lemma_step.lemma_mark]marknode_accest_access [in GC.lemma_step.lemma_mark]
marknode_notfrees_notfreet [in GC.lemma_step.lemma_mark]
marknode_fair [in GC.liveness.fairstr]
marknode_idem_or_init [in GC.liveness.notacc_init]
marknode_ex_mesure [in GC.mesure.mesure]
marknode_mesure [in GC.mesure.mesure]
marknode_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
marknode_notacces_t [in GC.liveness.notfree_notacc]
mark_white [in GC.lemma_step.lemma_mark]
mark_ancestor_col [in GC.lemma_step.lemma_mark]
mark_ancestor [in GC.lemma_step.lemma_mark]
mark_idem_or_free [in GC.liveness.notacc_white_nogrey]
mark_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
measureO_whiteO [in GC.liveness.until_zero]
measureO_greyO [in GC.liveness.until_zero]
measure_unicity [in GC.mesure.unicite_mes]
measure_until_zero_on_run [in GC.liveness.until_zero]
measure_until_zero [in GC.liveness.until_zero]
measure_trivial_bis [in GC.liveness.until_zero]
measure_trivial [in GC.liveness.until_zero]
minus_pred [in GC.lib_arith.lib_minus]
N
nogrey_accn_imp_blackn_step [in GC.safety.safety]nogrey_accn_imp_blackn_gcend [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcfree1 [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcfree [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gcstop [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_marknode [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_gccall [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_alloc [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_removeedge [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_addedge [in GC.safety.nogreyaccnblackn]
nogrey_accn_imp_blackn_init [in GC.safety.nogreyaccnblackn]
none_or_one_decrease [in GC.liveness.until_zero]
notacc_white_nogrey_eventually_free [in GC.liveness.notacc_white_ancestor]
noteqmar_noteqnod [in GC.gc.parameters]
notfree_notacces_unless_isfree [in GC.liveness.notfree_notacc]
not_true_and_white [in GC.mesure.parameters_card]
no_grey_but_white_fair [in GC.liveness.fairstr]
no_edge_black_to_white_gcend [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree1 [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree_bis [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcfree [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gcstop [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_marknode [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_gccall [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_alloc [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_removeedge [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_addedge [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_init [in GC.safety.noedgeblacktowhite]
no_edge_black_to_white_inv [in GC.safety.safety]
no_edge_black_to_white_step [in GC.safety.safety]
null_measure_grey_white [in GC.liveness.notacc_init]
O
once_equiv_once [in GC.logique.LTL]once_eventually [in GC.logique.LTL]
once_until_zero [in GC.liveness.until_zero]
one_step_leads_to [in GC.logique.LTL]
P
plus_pred [in GC.lib_arith.lib_plus]plus_O_O [in GC.lib_arith.lib_plus]
plus_O [in GC.lib_arith.lib_plus]
plus_S_pred [in GC.lib_arith.lib_plus]
pred_S [in GC.lib_arith.lib_S_pred]
pred_S_minus [in GC.lib_arith.lib_minus]
pred_plus_minus [in GC.lib_arith.lib_plus]
pred_plus_S [in GC.lib_arith.lib_plus]
R
reach_true_reach [in GC.reachable.reachable]reach_notacc [in GC.reachable.reachable]
reach_acc [in GC.reachable.reachable]
removeedge_notacces_t [in GC.liveness.notfree_notacc]
remove_grey [in GC.mesure.grey_card]
remove_idem_or_init [in GC.liveness.notacc_init]
remove_idem_or_free [in GC.liveness.notacc_white_nogrey]
remove_ex_mesure [in GC.mesure.mesure]
remove_mesure [in GC.mesure.mesure]
remove_white [in GC.mesure.white_card]
remove_black [in GC.mesure.black_card]
remove_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
remove_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
remove_ancestor_col [in GC.lemma_step.lemma_remove]
remove_ancestor [in GC.lemma_step.lemma_remove]
remove_nowhite [in GC.lemma_step.lemma_remove]
remove_nogrey [in GC.lemma_step.lemma_remove]
remove_white [in GC.lemma_step.lemma_remove]
remove_notaccess_notaccest [in GC.lemma_step.lemma_remove]
remove_notgreyt_notgreys [in GC.lemma_step.lemma_remove]
remove_blacks_blackt [in GC.lemma_step.lemma_remove]
remove_notfrees_notfreet [in GC.lemma_step.lemma_remove]
remove_accest_access [in GC.lemma_step.lemma_remove]
rt_grey_or_black_inv [in GC.safety.safety]
rt_grey_or_black_step [in GC.safety.safety]
rt_grey_or_black_gcend [in GC.safety.rtgreyorblack]
rt_grey_or_black_gcfree1 [in GC.safety.rtgreyorblack]
rt_grey_or_black_gcfree [in GC.safety.rtgreyorblack]
rt_grey_or_black_gcstop [in GC.safety.rtgreyorblack]
rt_grey_or_black_marknode [in GC.safety.rtgreyorblack]
rt_grey_or_black_gccall [in GC.safety.rtgreyorblack]
rt_grey_or_black_alloc [in GC.safety.rtgreyorblack]
rt_grey_or_black_removeedge [in GC.safety.rtgreyorblack]
rt_grey_or_black_addedge [in GC.safety.rtgreyorblack]
rt_grey_or_black_init [in GC.safety.rtgreyorblack]
run_fairstr_always [in GC.liveness.liveness]
S
safeP_safeQ_stream [in GC.logique.LTL]safeP_safeQ [in GC.logique.LTL]
safety [in GC.logique.LTL]
safety_prop_safe [in GC.safety.safety]
safe_inv_gwb_mesure [in GC.liveness.liveness]
safe_inv_and_gwb [in GC.liveness.liveness]
safe_and_state [in GC.logique.LTL]
safe_and [in GC.logique.LTL]
safe_sweep_no_greys [in GC.safety.safety]
safe_mesure [in GC.mesure.safe_card]
safe_inv_conj_mes [in GC.mesure.safe_card]
safe_gwb [in GC.mesure.safe_card]
safe_card_grey [in GC.mesure.safe_card]
safe_inv_conj [in GC.mesure.safe_card]
safe_card_white [in GC.mesure.safe_card]
safe_conj_inv [in GC.mesure.safe_card]
safe_card_black [in GC.mesure.safe_card]
step_initcolor [in GC.liveness.notacc_init]
step_idem_or_init [in GC.liveness.notacc_init]
step_idem_or_free [in GC.liveness.notacc_white_nogrey]
step_decrease [in GC.liveness.until_zero]
step_ex_mesure [in GC.mesure.safe_card]
step_mesure [in GC.mesure.safe_card]
step_grey_card [in GC.mesure.safe_card]
step_white_card [in GC.mesure.safe_card]
step_black_card [in GC.mesure.safe_card]
step_notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
step_notacc_white_reach [in GC.liveness.notacc_white_ancestor]
step_notacces_t [in GC.liveness.notfree_notacc]
strong_fairstr_implies_fairstr [in GC.logique.LTL]
sweep_no_greys_inv [in GC.safety.safety]
sweep_no_greys_step [in GC.safety.safety]
sweep_no_greys_gcend [in GC.safety.sweepnogrey]
sweep_no_greys_gcfree1 [in GC.safety.sweepnogrey]
sweep_no_greys_gcfree [in GC.safety.sweepnogrey]
sweep_no_greys_gcstop [in GC.safety.sweepnogrey]
sweep_no_greys_marknode [in GC.safety.sweepnogrey]
sweep_no_greys_gccall [in GC.safety.sweepnogrey]
sweep_no_greys_alloc [in GC.safety.sweepnogrey]
sweep_no_greys_removeedge [in GC.safety.sweepnogrey]
sweep_no_greys_addedge [in GC.safety.sweepnogrey]
sweep_no_greys_init [in GC.safety.sweepnogrey]
S_pred [in GC.lib_arith.lib_S_pred]
T
trivial [in GC.lemma_step.lemma_step]trivial_unicity_bis [in GC.liveness.until_zero]
trivial_unicity [in GC.liveness.until_zero]
U
unicity_card [in GC.card.card]until_no_measure_init [in GC.liveness.notacc_init]
until_idem_or_free [in GC.liveness.notacc_white_nogrey]
until_eventually [in GC.logique.LTL]
until_implies_until [in GC.logique.LTL]
until_trans [in GC.logique.LTL]
until_or [in GC.logique.LTL]
until_implies_until_state [in GC.logique.LTL]
until_implies_until_stream [in GC.logique.LTL]
until_zero [in GC.liveness.until_zero]
until_no_measure [in GC.liveness.notacc_black_nogrey]
until_no_white [in GC.liveness.notacc_black_nogrey]
until_no_grey_without_reach [in GC.liveness.notacc_white_ancestor]
until_no_grey [in GC.liveness.notacc_white_ancestor]
until_free_or_nogrey [in GC.liveness.notfree_notacc]
updatecolor_blacks_blackt [in GC.lemma_step.lemma_free]
W
wf_leadsto_rule [in GC.logique.well_founded]wf_leadsto [in GC.logique.well_founded]
white_notacc_nogrey_until_eventually_free [in GC.liveness.notacc_white_nogrey]
Axiom Index
E
eq_dec_set [in GC.card.card_facts]eq_dec_set [in GC.card.card]
eq_dec_node [in GC.gc.parameters]
exist_or_none [in GC.liveness.fairstr]
N
node [in GC.gc.parameters]R
rt [in GC.gc.parameters]Constructor Index
A
add_to_node [in GC.gc.gc]ae [in GC.gc.gc]
al [in GC.gc.gc]
alloc_add_free_to_rt [in GC.gc.gc]
B
black [in GC.gc.parameters]C
call_exist_grey [in GC.gc.gc]call_gc [in GC.gc.gc]
card_S [in GC.card.card]
card_0 [in GC.card.card]
cons_str [in GC.logique.LTL]
CS [in GC.mesure.parameters_card]
c_state [in GC.gc.parameters]
c_fstep [in GC.logique.LTL]
C_always [in GC.logique.LTL]
c_pos_trans [in GC.logique.LTL]
C_trans [in GC.logique.LTL]
E
ev_t [in GC.logique.LTL]ev_h [in GC.logique.LTL]
F
free [in GC.gc.parameters]free_no_grey_but_white [in GC.gc.gc]
free1_white [in GC.gc.gc]
G
gcc [in GC.gc.gc]gce [in GC.gc.gc]
gcend [in GC.gc.gc]
gcf [in GC.gc.gc]
gcfr [in GC.gc.gc]
gcs [in GC.gc.gc]
gcstop [in GC.gc.gc]
grey [in GC.gc.parameters]
grey_sons [in GC.mesure.parameters_card]
grey_node [in GC.gc.gc]
I
init_no_greys_but_white [in GC.gc.gc]L
label_end [in GC.gc.gc]label_free1 [in GC.gc.gc]
label_free [in GC.gc.gc]
label_stop [in GC.gc.gc]
label_mark [in GC.gc.gc]
label_call [in GC.gc.gc]
label_alloc [in GC.gc.gc]
label_rem [in GC.gc.gc]
label_add [in GC.gc.gc]
M
mar [in GC.gc.gc]mark [in GC.gc.parameters]
mesur [in GC.mesure.mesure]
mn_exist_grey [in GC.gc.gc]
mutate [in GC.gc.parameters]
N
none [in GC.logique.LTL]O
one [in GC.logique.LTL]R
re [in GC.gc.gc]reachable_edge [in GC.reachable.reachable]
reachable_init [in GC.reachable.reachable]
remove_to_node [in GC.gc.gc]
S
sweep [in GC.gc.parameters]U
unless_t [in GC.logique.LTL]unless_h [in GC.logique.LTL]
until_t [in GC.logique.LTL]
until_h [in GC.logique.LTL]
W
white [in GC.gc.parameters]Inductive Index
A
add_edge [in GC.gc.gc]alloc [in GC.gc.gc]
always [in GC.logique.LTL]
C
card [in GC.card.card]card_sons [in GC.mesure.parameters_card]
color [in GC.gc.parameters]
control [in GC.gc.parameters]
E
enabled [in GC.logique.LTL]Eventually [in GC.logique.LTL]
F
fair_step [in GC.logique.LTL]G
gc_end [in GC.gc.gc]gc_free1 [in GC.gc.gc]
gc_free [in GC.gc.gc]
gc_stop [in GC.gc.gc]
gc_call [in GC.gc.gc]
grey_white_sons [in GC.mesure.parameters_card]
grey_node_case [in GC.gc.gc]
L
label [in GC.gc.gc]M
mark_node [in GC.gc.gc]mesure [in GC.mesure.mesure]
N
none_or_one_step [in GC.logique.LTL]R
reachable [in GC.reachable.reachable]remove_edge [in GC.gc.gc]
S
step [in GC.logique.LTL]stream [in GC.logique.LTL]
T
transition [in GC.gc.gc]U
unless [in GC.logique.LTL]until [in GC.logique.LTL]
Projection Index
C
ctl [in GC.gc.parameters]H
hp [in GC.gc.parameters]M
mk [in GC.gc.parameters]Section Index
B
black_card [in GC.mesure.black_card]C
cardinal [in GC.card.card]card_facts [in GC.card.card_facts]
F
fairstr [in GC.liveness.fairstr]G
grey_card [in GC.mesure.grey_card]I
invariant1 [in GC.safety.rtgreyorblack]invariant2 [in GC.safety.sweepnogrey]
invariant3 [in GC.safety.noedgeblacktowhite]
invariant4 [in GC.safety.accnotfree]
invariant5 [in GC.safety.nogreyaccnblackn]
L
lemma_mark [in GC.lemma_step.lemma_mark]lemma_call [in GC.lemma_step.lemma_call]
lemma_stop [in GC.lemma_step.lemma_stop]
lemma_alloc [in GC.lemma_step.lemma_alloc]
lemma_free1 [in GC.lemma_step.lemma_free1]
lemma_end [in GC.lemma_step.lemma_end]
lemma_step [in GC.lemma_step.lemma_step]
lemma_add [in GC.lemma_step.lemma_add]
lemma_free [in GC.lemma_step.lemma_free]
lemma_remove [in GC.lemma_step.lemma_remove]
lemme_arith [in GC.lib_arith.lemme_arith]
lib_S_pred [in GC.lib_arith.lib_S_pred]
lib_minus [in GC.lib_arith.lib_minus]
lib_plus [in GC.lib_arith.lib_plus]
liveness [in GC.liveness.liveness]
LTL [in GC.logique.LTL]
M
mesure [in GC.mesure.mesure]N
notacc_init [in GC.liveness.notacc_init]notacc_white_nogrey [in GC.liveness.notacc_white_nogrey]
notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
notacc_white_ancestor [in GC.liveness.notacc_white_ancestor]
notfree_notacc [in GC.liveness.notfree_notacc]
P
parameters [in GC.gc.parameters]parameters_card [in GC.mesure.parameters_card]
R
reachable [in GC.reachable.reachable]S
safety [in GC.safety.safety]safe_card [in GC.mesure.safe_card]
specification [in GC.gc.gc]
U
unicite_mesure [in GC.mesure.unicite_mes]until_zero [in GC.liveness.until_zero]
W
well_founded [in GC.logique.well_founded]white_card [in GC.mesure.white_card]
Abbreviation Index
C
Card [in GC.card.card_facts]Card [in GC.mesure.grey_card]
Card [in GC.mesure.parameters_card]
Card [in GC.mesure.mesure]
Card [in GC.mesure.white_card]
Card [in GC.mesure.black_card]
F
Fairstr [in GC.liveness.fairstr]Fairstr [in GC.liveness.notacc_init]
Fairstr [in GC.liveness.until_zero]
Fair_step [in GC.liveness.fairstr]
Fair_step [in GC.liveness.notacc_init]
Fair_step [in GC.liveness.until_zero]
I
Invariant [in GC.safety.safety]Invariant [in GC.mesure.safe_card]
N
None_or_one_step [in GC.liveness.until_zero]O
Once_always [in GC.liveness.until_zero]R
Reachable [in GC.lemma_step.lemma_mark]Reachable [in GC.lemma_step.lemma_stop]
Reachable [in GC.lemma_step.lemma_alloc]
Reachable [in GC.lemma_step.lemma_end]
Reachable [in GC.lemma_step.lemma_add]
Reachable [in GC.liveness.notacc_white_ancestor]
Reachable [in GC.lemma_step.lemma_remove]
Run [in GC.liveness.fairstr]
Run [in GC.liveness.liveness]
Run [in GC.safety.safety]
Run [in GC.liveness.until_zero]
Run [in GC.mesure.safe_card]
S
Safe [in GC.liveness.fairstr]Safe [in GC.liveness.liveness]
Safe [in GC.safety.safety]
Safe [in GC.mesure.safe_card]
State_formula [in GC.logique.well_founded]
State_formula [in GC.gc.gc]
State_formula [in GC.safety.safety]
State_formula [in GC.liveness.until_zero]
State_formula [in GC.mesure.safe_card]
State_formula [in GC.liveness.notfree_notacc]
Step [in GC.liveness.notacc_init]
Step [in GC.liveness.notacc_white_nogrey]
Step [in GC.safety.safety]
Step [in GC.liveness.until_zero]
Step [in GC.mesure.safe_card]
Step [in GC.liveness.notacc_black_nogrey]
Step [in GC.liveness.notacc_white_ancestor]
Step [in GC.liveness.notfree_notacc]
Stream [in GC.logique.well_founded]
Stream [in GC.liveness.fairstr]
Stream [in GC.liveness.notacc_init]
Stream [in GC.liveness.notacc_white_nogrey]
Stream [in GC.liveness.liveness]
Stream [in GC.safety.safety]
Stream [in GC.liveness.until_zero]
Stream [in GC.mesure.safe_card]
Stream [in GC.liveness.notacc_black_nogrey]
Stream [in GC.liveness.notacc_white_ancestor]
Stream [in GC.liveness.notfree_notacc]
Stream_formula [in GC.liveness.notacc_init]
Stream_formula [in GC.liveness.notacc_white_nogrey]
Stream_formula [in GC.liveness.liveness]
Stream_formula [in GC.safety.safety]
Stream_formula [in GC.mesure.safe_card]
Stream_formula [in GC.liveness.notacc_black_nogrey]
Stream_formula [in GC.liveness.notacc_white_ancestor]
Stream_formula [in GC.liveness.notfree_notacc]
Strong_fairstr [in GC.liveness.notacc_init]
Strong_fairstr [in GC.liveness.liveness]
T
Trace [in GC.liveness.notacc_init]Trace [in GC.liveness.notacc_white_nogrey]
Trace [in GC.liveness.liveness]
Trace [in GC.liveness.until_zero]
Trace [in GC.liveness.notacc_black_nogrey]
Trace [in GC.liveness.notacc_white_ancestor]
Trace [in GC.liveness.notfree_notacc]
W
Wf_leadsto_rule [in GC.liveness.until_zero]Definition Index
A
accessible [in GC.reachable.reachable]acc_imp_notfree [in GC.gc.gc]
add [in GC.gc.gc]
and [in GC.logique.LTL]
and_inv [in GC.liveness.liveness]
and_state [in GC.logique.LTL]
C
card_color [in GC.mesure.parameters_card]conj_inv [in GC.mesure.safe_card]
E
Eventually_permanently [in GC.logique.LTL]F
fair [in GC.gc.gc]fairness [in GC.logique.LTL]
fairstr [in GC.logique.LTL]
free_or_notfree_notacc_nogrey [in GC.liveness.notfree_notacc]
G
g_w_b [in GC.mesure.safe_card]H
head_str [in GC.logique.LTL]heap [in GC.gc.parameters]
I
implies [in GC.logique.LTL]infinitely_often [in GC.logique.LTL]
init_state [in GC.gc.gc]
init_marking [in GC.gc.gc]
init_color [in GC.gc.gc]
invariant [in GC.logique.LTL]
invariant_safety_and [in GC.safety.safety]
invariant_safety [in GC.safety.safety]
inv_conj_mes [in GC.mesure.safe_card]
inv_conj [in GC.mesure.safe_card]
is_always_followed [in GC.logique.LTL]
is_followed [in GC.logique.LTL]
is_free [in GC.liveness.notfree_notacc]
L
leads_to_via [in GC.logique.LTL]leads_to [in GC.logique.LTL]
M
marking [in GC.gc.parameters]marking_add [in GC.gc.gc]
measure [in GC.liveness.until_zero]
N
next [in GC.logique.LTL]nogrey_accn_imp_blackn [in GC.gc.gc]
notacc_white_init_formula [in GC.liveness.notacc_init]
notacc_black_nomeasure_formula [in GC.liveness.notacc_init]
notacc_white_init [in GC.liveness.notacc_init]
notacc_black_nomeasure [in GC.liveness.notacc_init]
notacc_white_nogrey_formula [in GC.liveness.notacc_white_nogrey]
notacc_white_nogrey_or_free [in GC.liveness.notacc_white_nogrey]
notacc_white_nogrey [in GC.liveness.notacc_white_nogrey]
notacc_black_nomeasure_formula [in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_formula [in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_nowhite_formula [in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_exwhite_formula [in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey [in GC.liveness.notacc_black_nogrey]
notacc_black_nogrey_exwhite [in GC.liveness.notacc_black_nogrey]
notacc_white_reach_formula [in GC.liveness.notacc_white_ancestor]
notacc_white_exgrey_reach_formula [in GC.liveness.notacc_white_ancestor]
notacc_white_reach [in GC.liveness.notacc_white_ancestor]
notacc_white_exgrey_reach [in GC.liveness.notacc_white_ancestor]
notfree [in GC.liveness.notfree_notacc]
notfree_notacces [in GC.liveness.notfree_notacc]
no_edge_black_to_white_bis [in GC.gc.gc]
no_edge_black_to_white [in GC.gc.gc]
O
once_until [in GC.logique.LTL]once_always [in GC.logique.LTL]
P
positive_measure [in GC.liveness.until_zero]prop_dec2 [in GC.card.card_facts]
prop_dec [in GC.card.card_facts]
R
remove [in GC.gc.gc]rt_grey_or_black [in GC.gc.gc]
run [in GC.logique.LTL]
S
safe [in GC.logique.LTL]safety_prop [in GC.safety.safety]
state_formula [in GC.logique.LTL]
state2stream_formula [in GC.logique.LTL]
stream_formula [in GC.logique.LTL]
strong_fairstr [in GC.logique.LTL]
sweep_no_greys [in GC.gc.gc]
T
tl_str [in GC.logique.LTL]trace [in GC.logique.LTL]
U
update [in GC.card.card]update_N [in GC.card.card_facts]
update_M [in GC.card.card_facts]
update_heap [in GC.mesure.parameters_card]
update_init_color [in GC.liveness.fairstr]
update_color_marknode [in GC.liveness.fairstr]
update_color [in GC.gc.gc]
Record Index
S
state [in GC.gc.parameters]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (809 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 | _ | other | (16 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (457 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 | _ | other | (6 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (42 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (75 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (81 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |