| 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 | (307 entries) |
| Notation 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 | (4 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 | _ | other | (15 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 | (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 | _ | other | (107 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 | (78 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 | (18 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 | (83 entries) |
Global Index
B
bind [definition, in CoqDefs]bind [definition, in CorrelatingProgram]
C
CoqDefs [library]CorrelatingProgram [library]
correlating_program_sound [lemma, in CorrelatingProgram]
correlating_program [definition, in CorrelatingProgram]
CP [module, in CorrelatingProgram]
CPStr [module, in CorrelatingProgram]
CP.add_cpoints_conserves_semantics [lemma, in CorrelatingProgram]
CP.add_cpoints [definition, in CorrelatingProgram]
CP.bexp_classified [definition, in CorrelatingProgram]
CP.both_running [constructor, in CorrelatingProgram]
CP.both_stopped [constructor, in CorrelatingProgram]
CP.break_helper [lemma, in CorrelatingProgram]
CP.CI [definition, in CorrelatingProgram]
CP.CI_sound [lemma, in CorrelatingProgram]
CP.classification [inductive, in CorrelatingProgram]
CP.classification_fun [definition, in CorrelatingProgram]
CP.classified_cmdg_preserves_classified_stores [lemma, in CorrelatingProgram]
CP.ClsDiff [constructor, in CorrelatingProgram]
CP.ClsOrig [constructor, in CorrelatingProgram]
CP.cmda_classified [definition, in CorrelatingProgram]
CP.cmdg_classified [definition, in CorrelatingProgram]
CP.cmd_classified [definition, in CorrelatingProgram]
CP.cmd_subtree_while [constructor, in CorrelatingProgram]
CP.cmd_subtree_seq_right [constructor, in CorrelatingProgram]
CP.cmd_subtree_seq_left [constructor, in CorrelatingProgram]
CP.cmd_subtree_if_else [constructor, in CorrelatingProgram]
CP.cmd_subtree_if_then [constructor, in CorrelatingProgram]
CP.cmd_subtree_id [constructor, in CorrelatingProgram]
CP.cmd_subtree [inductive, in CorrelatingProgram]
CP.continue_helper [lemma, in CorrelatingProgram]
CP.correlating_program_sound [lemma, in CorrelatingProgram]
CP.correlating_program [definition, in CorrelatingProgram]
CP.cp [definition, in CorrelatingProgram]
CP.cp_equiv_proj [lemma, in CorrelatingProgram]
CP.cp_equiv_tgl [lemma, in CorrelatingProgram]
CP.cp_sound [lemma, in CorrelatingProgram]
CP.C_false_noop [lemma, in CorrelatingProgram]
CP.diffmap_classification [lemma, in CorrelatingProgram]
CP.diffmap_classified [definition, in CorrelatingProgram]
CP.diffmap_recursivity [lemma, in CorrelatingProgram]
CP.diff_subtree_while_del [constructor, in CorrelatingProgram]
CP.diff_subtree_while_add [constructor, in CorrelatingProgram]
CP.diff_subtree_del_else [constructor, in CorrelatingProgram]
CP.diff_subtree_del_if [constructor, in CorrelatingProgram]
CP.diff_subtree_add_else [constructor, in CorrelatingProgram]
CP.diff_subtree_add_if [constructor, in CorrelatingProgram]
CP.diff_subtree_while_mut [constructor, in CorrelatingProgram]
CP.diff_subtree_ifmut_else [constructor, in CorrelatingProgram]
CP.diff_subtree_ifmut_then [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_r [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_l [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_ins_r [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_ins_l [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_del_r [constructor, in CorrelatingProgram]
CP.diff_subtree_seq_del_l [constructor, in CorrelatingProgram]
CP.diff_subtree_id [constructor, in CorrelatingProgram]
CP.diff_subtree [inductive, in CorrelatingProgram]
CP.diff_completeness [lemma, in CorrelatingProgram]
CP.double_loop_translation_correct [lemma, in CorrelatingProgram]
CP.dummy_correlating_program_sound [lemma, in CorrelatingProgram]
CP.dummy_correlating_program [definition, in CorrelatingProgram]
CP.dummy_cp_equiv_proj [lemma, in CorrelatingProgram]
CP.dummy_cp_equiv_tgl [lemma, in CorrelatingProgram]
CP.dummy_cp [definition, in CorrelatingProgram]
CP.exp_classified [definition, in CorrelatingProgram]
CP.gstore_inclusion_preserves_disj [lemma, in CorrelatingProgram]
CP.gstore_inclusion_preserves_conj [lemma, in CorrelatingProgram]
CP.gstore_classified [definition, in CorrelatingProgram]
CP.gstore_included [definition, in CorrelatingProgram]
CP.guard_disj_helper [lemma, in CorrelatingProgram]
CP.guard_classified_succ [lemma, in CorrelatingProgram]
CP.guard_disj_classified [definition, in CorrelatingProgram]
CP.guard_conj_classified [definition, in CorrelatingProgram]
CP.guard_classified [definition, in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_3 [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_2 [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_1 [lemma, in CorrelatingProgram]
CP.guard_conservation_helper [lemma, in CorrelatingProgram]
CP.guard_conj_prop [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_false_app_2 [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_false_app_1 [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_true_app [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_true_app_inv [lemma, in CorrelatingProgram]
CP.guard_conj_evals_to_true_cons_inv [lemma, in CorrelatingProgram]
CP.is_simple_diff [definition, in CorrelatingProgram]
CP.join_stores_inclusion [lemma, in CorrelatingProgram]
CP.LangDefs [module, in CorrelatingProgram]
CP.left_stopped [constructor, in CorrelatingProgram]
CP.left_step_helper2 [lemma, in CorrelatingProgram]
CP.left_step_helper [lemma, in CorrelatingProgram]
CP.loop_continued [definition, in CorrelatingProgram]
CP.loop_broken [definition, in CorrelatingProgram]
CP.lval_classified [definition, in CorrelatingProgram]
CP.path_suffix_helper [lemma, in CorrelatingProgram]
CP.path_suffix_S0_S1_exclusive [lemma, in CorrelatingProgram]
CP.path_length [definition, in CorrelatingProgram]
CP.path_suffix_inv_S1 [lemma, in CorrelatingProgram]
CP.path_suffix_inv_S0 [lemma, in CorrelatingProgram]
CP.right_stopped [constructor, in CorrelatingProgram]
CP.right_step_helper2 [lemma, in CorrelatingProgram]
CP.right_step_helper [lemma, in CorrelatingProgram]
CP.simplify_diff_preserves_semantics [lemma, in CorrelatingProgram]
CP.simplify_yields_simple_diff [lemma, in CorrelatingProgram]
CP.simplify_diff [definition, in CorrelatingProgram]
CP.store_inclusion_preserves_bexp_eval [lemma, in CorrelatingProgram]
CP.store_inclusion_preserves_lval_eval [lemma, in CorrelatingProgram]
CP.store_inclusion_preserves_exp_eval [lemma, in CorrelatingProgram]
CP.store_included [definition, in CorrelatingProgram]
CP.store_classified [definition, in CorrelatingProgram]
CP.suffix_order_implies_length_order [lemma, in CorrelatingProgram]
CP.S0g_not_suffix_g [lemma, in CorrelatingProgram]
CP.S1g_not_suffix_g [lemma, in CorrelatingProgram]
CP.tagged_execution [lemma, in CorrelatingProgram]
CP.tagged_store_inclusion_sorta_trans [lemma, in CorrelatingProgram]
CP.tagged_store_inclusion_bexp_eval [lemma, in CorrelatingProgram]
CP.tagged_store_inclusion_lval_eval [lemma, in CorrelatingProgram]
CP.tagged_store_inclusion_exp_eval [lemma, in CorrelatingProgram]
CP.tagged_store_keys_tagged [lemma, in CorrelatingProgram]
CP.tag_diffmap_classification [lemma, in CorrelatingProgram]
CP.tag_cmd_classification [lemma, in CorrelatingProgram]
CP.tag_cmda_classification [lemma, in CorrelatingProgram]
CP.tag_bexp_classification [lemma, in CorrelatingProgram]
CP.tag_lval_classification [lemma, in CorrelatingProgram]
CP.tag_exp_classification [lemma, in CorrelatingProgram]
CP.tag_diffmap_proj_correct [lemma, in CorrelatingProgram]
CP.tag_diffmap [definition, in CorrelatingProgram]
CP.tag_cmd [definition, in CorrelatingProgram]
CP.tag_cmda [definition, in CorrelatingProgram]
CP.tag_bexp [definition, in CorrelatingProgram]
CP.tag_exp [definition, in CorrelatingProgram]
CP.tag_lval [definition, in CorrelatingProgram]
CP.toto_TODO3 [lemma, in CorrelatingProgram]
CP.toto_TODO2 [lemma, in CorrelatingProgram]
CP.toto_TODO [lemma, in CorrelatingProgram]
CP.to_gl_sound [lemma, in CorrelatingProgram]
CP.to_gl [definition, in CorrelatingProgram]
CP.translation_preserves_classification [lemma, in CorrelatingProgram]
CP.truc [lemma, in CorrelatingProgram]
CP.two_loops_equiv [lemma, in CorrelatingProgram]
CP.two_loops_implied [lemma, in CorrelatingProgram]
CP.two_loops [inductive, in CorrelatingProgram]
CP.t_injective_store_proj [lemma, in CorrelatingProgram]
CP.valid_classification_fun [definition, in CorrelatingProgram]
CP.VarMap [module, in CorrelatingProgram]
CP.VarMapFacts [module, in CorrelatingProgram]
CP.VarMapProps [module, in CorrelatingProgram]
D
dummy_correlating_program_sound [lemma, in CorrelatingProgram]dummy_correlating_program [definition, in CorrelatingProgram]
F
Forall_app [lemma, in CorrelatingProgram]L
Languages [module, in CoqDefs]Languages.acmd_g [inductive, in CoqDefs]
Languages.ArrayAccess [constructor, in CoqDefs]
Languages.ArrayValue [constructor, in CoqDefs]
Languages.Assign [constructor, in CoqDefs]
Languages.BAnd [constructor, in CoqDefs]
Languages.BEQ [constructor, in CoqDefs]
Languages.bexp [inductive, in CoqDefs]
Languages.BFalse [constructor, in CoqDefs]
Languages.BGE [constructor, in CoqDefs]
Languages.BGT [constructor, in CoqDefs]
Languages.big_step_g [inductive, in CoqDefs]
Languages.big_step [inductive, in CoqDefs]
Languages.BLE [constructor, in CoqDefs]
Languages.BLT [constructor, in CoqDefs]
Languages.BNEQ [constructor, in CoqDefs]
Languages.BNot [constructor, in CoqDefs]
Languages.BOr [constructor, in CoqDefs]
Languages.Break [constructor, in CoqDefs]
Languages.BTrue [constructor, in CoqDefs]
Languages.cmd [inductive, in CoqDefs]
Languages.cmda_beq [definition, in CoqDefs]
Languages.cmd_diff [inductive, in CoqDefs]
Languages.cmd_g [inductive, in CoqDefs]
Languages.cmd_a [inductive, in CoqDefs]
Languages.Continue [constructor, in CoqDefs]
Languages.CPoint [constructor, in CoqDefs]
Languages.cp_algorithm_sound [definition, in CoqDefs]
Languages.Diff [constructor, in CoqDefs]
Languages.Div [constructor, in CoqDefs]
Languages.eq_guard_dec [lemma, in CoqDefs]
Languages.exp [inductive, in CoqDefs]
Languages.exp_beq [definition, in CoqDefs]
Languages.exp_mut [definition, in CoqDefs]
Languages.GAAssign [constructor, in CoqDefs]
Languages.GAGAssign [constructor, in CoqDefs]
Languages.GAtomic [constructor, in CoqDefs]
Languages.GCPoint [constructor, in CoqDefs]
Languages.GSeq [constructor, in CoqDefs]
Languages.GSkip [constructor, in CoqDefs]
Languages.gstore [definition, in CoqDefs]
Languages.guard [inductive, in CoqDefs]
Languages.GuardMap [module, in CoqDefs]
Languages.GuardMapFacts [module, in CoqDefs]
Languages.GuardMapProps [module, in CoqDefs]
Languages.guard_disj_evals_to [definition, in CoqDefs]
Languages.guard_conj_evals_to [definition, in CoqDefs]
Languages.guard_disj [definition, in CoqDefs]
Languages.guard_conj [definition, in CoqDefs]
Languages.guard_as_DT.eq_dec [definition, in CoqDefs]
Languages.guard_as_DT.eq_trans [definition, in CoqDefs]
Languages.guard_as_DT.eq_sym [definition, in CoqDefs]
Languages.guard_as_DT.eq_refl [definition, in CoqDefs]
Languages.guard_as_DT.eq [definition, in CoqDefs]
Languages.guard_as_DT.t [definition, in CoqDefs]
Languages.guard_as_DT [module, in CoqDefs]
Languages.GWhile [constructor, in CoqDefs]
Languages.IfMut [constructor, in CoqDefs]
Languages.IfThenElse [constructor, in CoqDefs]
Languages.Int [constructor, in CoqDefs]
Languages.interp_guard_conj [definition, in CoqDefs]
Languages.interp_bexp [definition, in CoqDefs]
Languages.interp_exp [definition, in CoqDefs]
Languages.IntValue [constructor, in CoqDefs]
Languages.ITEAddElse [constructor, in CoqDefs]
Languages.ITEAddIf [constructor, in CoqDefs]
Languages.ITEDelElse [constructor, in CoqDefs]
Languages.ITEDelIf [constructor, in CoqDefs]
Languages.join_stores [definition, in CoqDefs]
Languages.j_gcpoint [constructor, in CoqDefs]
Languages.j_gwhile_true [constructor, in CoqDefs]
Languages.j_gwhile_false [constructor, in CoqDefs]
Languages.j_gseq [constructor, in CoqDefs]
Languages.j_gskip [constructor, in CoqDefs]
Languages.j_ggassign [constructor, in CoqDefs]
Languages.j_gassign [constructor, in CoqDefs]
Languages.j_gatomic_false [constructor, in CoqDefs]
Languages.j_continue [constructor, in CoqDefs]
Languages.j_break [constructor, in CoqDefs]
Languages.j_while_break [constructor, in CoqDefs]
Languages.j_seq_interrupt [constructor, in CoqDefs]
Languages.j_while_true [constructor, in CoqDefs]
Languages.j_while_false [constructor, in CoqDefs]
Languages.j_if_else [constructor, in CoqDefs]
Languages.j_if_then [constructor, in CoqDefs]
Languages.j_seq_normal [constructor, in CoqDefs]
Languages.j_skip [constructor, in CoqDefs]
Languages.j_assign [constructor, in CoqDefs]
Languages.Leaf [constructor, in CoqDefs]
Languages.LeafSubst [constructor, in CoqDefs]
Languages.Lval [constructor, in CoqDefs]
Languages.lvalue [inductive, in CoqDefs]
Languages.lvalue_beq [definition, in CoqDefs]
Languages.lvalue_mut [definition, in CoqDefs]
Languages.MBreak [constructor, in CoqDefs]
Languages.MContinue [constructor, in CoqDefs]
Languages.MNormal [constructor, in CoqDefs]
Languages.mode [inductive, in CoqDefs]
Languages.Mult [constructor, in CoqDefs]
Languages.my_nth_implies_nth [lemma, in CoqDefs]
Languages.my_nth [definition, in CoqDefs]
Languages.path [definition, in CoqDefs]
Languages.path_suffix [inductive, in CoqDefs]
Languages.read_lval [definition, in CoqDefs]
Languages.Seq [constructor, in CoqDefs]
Languages.SeqDelL [constructor, in CoqDefs]
Languages.SeqDelR [constructor, in CoqDefs]
Languages.SeqInsL [constructor, in CoqDefs]
Languages.SeqInsR [constructor, in CoqDefs]
Languages.SeqMut [constructor, in CoqDefs]
Languages.set_lval [definition, in CoqDefs]
Languages.Skip [constructor, in CoqDefs]
Languages.store [definition, in CoqDefs]
Languages.store_included_tagged [definition, in CoqDefs]
Languages.suffix_S1 [constructor, in CoqDefs]
Languages.suffix_S0 [constructor, in CoqDefs]
Languages.suffix_eq [constructor, in CoqDefs]
Languages.Sum [constructor, in CoqDefs]
Languages.S0 [constructor, in CoqDefs]
Languages.S1 [constructor, in CoqDefs]
Languages.tag_store [definition, in CoqDefs]
Languages.value [inductive, in CoqDefs]
Languages.Var [constructor, in CoqDefs]
Languages.var [definition, in CoqDefs]
Languages.VarMap [module, in CoqDefs]
Languages.VarMapFacts [module, in CoqDefs]
Languages.VarMapProps [module, in CoqDefs]
Languages.While [constructor, in CoqDefs]
Languages.WhileAdd [constructor, in CoqDefs]
Languages.WhileDel [constructor, in CoqDefs]
Languages.WhileMut [constructor, in CoqDefs]
Languages.z_to_nat [definition, in CoqDefs]
_ ; _ (ast_scope) [notation, in CoqDefs]
_ ; _ (gast_scope) [notation, in CoqDefs]
Languages.Π₀ [definition, in CoqDefs]
Languages.Π₁ [definition, in CoqDefs]
Languages.ε [constructor, in CoqDefs]
R
ret [definition, in CoqDefs]ret [definition, in CorrelatingProgram]
S
String_as_DT.eq_dec [definition, in CorrelatingProgram]String_as_DT.eq_trans [definition, in CorrelatingProgram]
String_as_DT.eq_sym [definition, in CorrelatingProgram]
String_as_DT.eq_refl [definition, in CorrelatingProgram]
String_as_DT.eq [definition, in CorrelatingProgram]
String_as_DT.t [definition, in CorrelatingProgram]
String_as_DT [module, in CorrelatingProgram]
str_t'_inj [lemma, in CorrelatingProgram]
str_t_inj [lemma, in CorrelatingProgram]
str_f_valid [lemma, in CorrelatingProgram]
str_f [definition, in CorrelatingProgram]
str_t' [definition, in CorrelatingProgram]
str_t [definition, in CorrelatingProgram]
T
tag_diff_prefix [definition, in CorrelatingProgram]tag_orig_prefix [definition, in CorrelatingProgram]
other
_ >>= _ [notation, in CoqDefs]_ >>= _ [notation, in CorrelatingProgram]
Notation Index
L
_ ; _ (ast_scope) [in CoqDefs]_ ; _ (gast_scope) [in CoqDefs]
other
_ >>= _ [in CoqDefs]_ >>= _ [in CorrelatingProgram]
Module Index
C
CP [in CorrelatingProgram]CPStr [in CorrelatingProgram]
CP.LangDefs [in CorrelatingProgram]
CP.VarMap [in CorrelatingProgram]
CP.VarMapFacts [in CorrelatingProgram]
CP.VarMapProps [in CorrelatingProgram]
L
Languages [in CoqDefs]Languages.GuardMap [in CoqDefs]
Languages.GuardMapFacts [in CoqDefs]
Languages.GuardMapProps [in CoqDefs]
Languages.guard_as_DT [in CoqDefs]
Languages.VarMap [in CoqDefs]
Languages.VarMapFacts [in CoqDefs]
Languages.VarMapProps [in CoqDefs]
S
String_as_DT [in CorrelatingProgram]Library Index
C
CoqDefsCorrelatingProgram
Constructor Index
C
CP.both_running [in CorrelatingProgram]CP.both_stopped [in CorrelatingProgram]
CP.ClsDiff [in CorrelatingProgram]
CP.ClsOrig [in CorrelatingProgram]
CP.cmd_subtree_while [in CorrelatingProgram]
CP.cmd_subtree_seq_right [in CorrelatingProgram]
CP.cmd_subtree_seq_left [in CorrelatingProgram]
CP.cmd_subtree_if_else [in CorrelatingProgram]
CP.cmd_subtree_if_then [in CorrelatingProgram]
CP.cmd_subtree_id [in CorrelatingProgram]
CP.diff_subtree_while_del [in CorrelatingProgram]
CP.diff_subtree_while_add [in CorrelatingProgram]
CP.diff_subtree_del_else [in CorrelatingProgram]
CP.diff_subtree_del_if [in CorrelatingProgram]
CP.diff_subtree_add_else [in CorrelatingProgram]
CP.diff_subtree_add_if [in CorrelatingProgram]
CP.diff_subtree_while_mut [in CorrelatingProgram]
CP.diff_subtree_ifmut_else [in CorrelatingProgram]
CP.diff_subtree_ifmut_then [in CorrelatingProgram]
CP.diff_subtree_seq_r [in CorrelatingProgram]
CP.diff_subtree_seq_l [in CorrelatingProgram]
CP.diff_subtree_seq_ins_r [in CorrelatingProgram]
CP.diff_subtree_seq_ins_l [in CorrelatingProgram]
CP.diff_subtree_seq_del_r [in CorrelatingProgram]
CP.diff_subtree_seq_del_l [in CorrelatingProgram]
CP.diff_subtree_id [in CorrelatingProgram]
CP.left_stopped [in CorrelatingProgram]
CP.right_stopped [in CorrelatingProgram]
L
Languages.ArrayAccess [in CoqDefs]Languages.ArrayValue [in CoqDefs]
Languages.Assign [in CoqDefs]
Languages.BAnd [in CoqDefs]
Languages.BEQ [in CoqDefs]
Languages.BFalse [in CoqDefs]
Languages.BGE [in CoqDefs]
Languages.BGT [in CoqDefs]
Languages.BLE [in CoqDefs]
Languages.BLT [in CoqDefs]
Languages.BNEQ [in CoqDefs]
Languages.BNot [in CoqDefs]
Languages.BOr [in CoqDefs]
Languages.Break [in CoqDefs]
Languages.BTrue [in CoqDefs]
Languages.Continue [in CoqDefs]
Languages.CPoint [in CoqDefs]
Languages.Diff [in CoqDefs]
Languages.Div [in CoqDefs]
Languages.GAAssign [in CoqDefs]
Languages.GAGAssign [in CoqDefs]
Languages.GAtomic [in CoqDefs]
Languages.GCPoint [in CoqDefs]
Languages.GSeq [in CoqDefs]
Languages.GSkip [in CoqDefs]
Languages.GWhile [in CoqDefs]
Languages.IfMut [in CoqDefs]
Languages.IfThenElse [in CoqDefs]
Languages.Int [in CoqDefs]
Languages.IntValue [in CoqDefs]
Languages.ITEAddElse [in CoqDefs]
Languages.ITEAddIf [in CoqDefs]
Languages.ITEDelElse [in CoqDefs]
Languages.ITEDelIf [in CoqDefs]
Languages.j_gcpoint [in CoqDefs]
Languages.j_gwhile_true [in CoqDefs]
Languages.j_gwhile_false [in CoqDefs]
Languages.j_gseq [in CoqDefs]
Languages.j_gskip [in CoqDefs]
Languages.j_ggassign [in CoqDefs]
Languages.j_gassign [in CoqDefs]
Languages.j_gatomic_false [in CoqDefs]
Languages.j_continue [in CoqDefs]
Languages.j_break [in CoqDefs]
Languages.j_while_break [in CoqDefs]
Languages.j_seq_interrupt [in CoqDefs]
Languages.j_while_true [in CoqDefs]
Languages.j_while_false [in CoqDefs]
Languages.j_if_else [in CoqDefs]
Languages.j_if_then [in CoqDefs]
Languages.j_seq_normal [in CoqDefs]
Languages.j_skip [in CoqDefs]
Languages.j_assign [in CoqDefs]
Languages.Leaf [in CoqDefs]
Languages.LeafSubst [in CoqDefs]
Languages.Lval [in CoqDefs]
Languages.MBreak [in CoqDefs]
Languages.MContinue [in CoqDefs]
Languages.MNormal [in CoqDefs]
Languages.Mult [in CoqDefs]
Languages.Seq [in CoqDefs]
Languages.SeqDelL [in CoqDefs]
Languages.SeqDelR [in CoqDefs]
Languages.SeqInsL [in CoqDefs]
Languages.SeqInsR [in CoqDefs]
Languages.SeqMut [in CoqDefs]
Languages.Skip [in CoqDefs]
Languages.suffix_S1 [in CoqDefs]
Languages.suffix_S0 [in CoqDefs]
Languages.suffix_eq [in CoqDefs]
Languages.Sum [in CoqDefs]
Languages.S0 [in CoqDefs]
Languages.S1 [in CoqDefs]
Languages.Var [in CoqDefs]
Languages.While [in CoqDefs]
Languages.WhileAdd [in CoqDefs]
Languages.WhileDel [in CoqDefs]
Languages.WhileMut [in CoqDefs]
Languages.ε [in CoqDefs]
Lemma Index
C
correlating_program_sound [in CorrelatingProgram]CP.add_cpoints_conserves_semantics [in CorrelatingProgram]
CP.break_helper [in CorrelatingProgram]
CP.CI_sound [in CorrelatingProgram]
CP.classified_cmdg_preserves_classified_stores [in CorrelatingProgram]
CP.continue_helper [in CorrelatingProgram]
CP.correlating_program_sound [in CorrelatingProgram]
CP.cp_equiv_proj [in CorrelatingProgram]
CP.cp_equiv_tgl [in CorrelatingProgram]
CP.cp_sound [in CorrelatingProgram]
CP.C_false_noop [in CorrelatingProgram]
CP.diffmap_classification [in CorrelatingProgram]
CP.diffmap_recursivity [in CorrelatingProgram]
CP.diff_completeness [in CorrelatingProgram]
CP.double_loop_translation_correct [in CorrelatingProgram]
CP.dummy_correlating_program_sound [in CorrelatingProgram]
CP.dummy_cp_equiv_proj [in CorrelatingProgram]
CP.dummy_cp_equiv_tgl [in CorrelatingProgram]
CP.gstore_inclusion_preserves_disj [in CorrelatingProgram]
CP.gstore_inclusion_preserves_conj [in CorrelatingProgram]
CP.guard_disj_helper [in CorrelatingProgram]
CP.guard_classified_succ [in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_3 [in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_2 [in CorrelatingProgram]
CP.guard_conj_evals_to_gstore_inclusion_1 [in CorrelatingProgram]
CP.guard_conservation_helper [in CorrelatingProgram]
CP.guard_conj_prop [in CorrelatingProgram]
CP.guard_conj_evals_to_false_app_2 [in CorrelatingProgram]
CP.guard_conj_evals_to_false_app_1 [in CorrelatingProgram]
CP.guard_conj_evals_to_true_app [in CorrelatingProgram]
CP.guard_conj_evals_to_true_app_inv [in CorrelatingProgram]
CP.guard_conj_evals_to_true_cons_inv [in CorrelatingProgram]
CP.join_stores_inclusion [in CorrelatingProgram]
CP.left_step_helper2 [in CorrelatingProgram]
CP.left_step_helper [in CorrelatingProgram]
CP.path_suffix_helper [in CorrelatingProgram]
CP.path_suffix_S0_S1_exclusive [in CorrelatingProgram]
CP.path_suffix_inv_S1 [in CorrelatingProgram]
CP.path_suffix_inv_S0 [in CorrelatingProgram]
CP.right_step_helper2 [in CorrelatingProgram]
CP.right_step_helper [in CorrelatingProgram]
CP.simplify_diff_preserves_semantics [in CorrelatingProgram]
CP.simplify_yields_simple_diff [in CorrelatingProgram]
CP.store_inclusion_preserves_bexp_eval [in CorrelatingProgram]
CP.store_inclusion_preserves_lval_eval [in CorrelatingProgram]
CP.store_inclusion_preserves_exp_eval [in CorrelatingProgram]
CP.suffix_order_implies_length_order [in CorrelatingProgram]
CP.S0g_not_suffix_g [in CorrelatingProgram]
CP.S1g_not_suffix_g [in CorrelatingProgram]
CP.tagged_execution [in CorrelatingProgram]
CP.tagged_store_inclusion_sorta_trans [in CorrelatingProgram]
CP.tagged_store_inclusion_bexp_eval [in CorrelatingProgram]
CP.tagged_store_inclusion_lval_eval [in CorrelatingProgram]
CP.tagged_store_inclusion_exp_eval [in CorrelatingProgram]
CP.tagged_store_keys_tagged [in CorrelatingProgram]
CP.tag_diffmap_classification [in CorrelatingProgram]
CP.tag_cmd_classification [in CorrelatingProgram]
CP.tag_cmda_classification [in CorrelatingProgram]
CP.tag_bexp_classification [in CorrelatingProgram]
CP.tag_lval_classification [in CorrelatingProgram]
CP.tag_exp_classification [in CorrelatingProgram]
CP.tag_diffmap_proj_correct [in CorrelatingProgram]
CP.toto_TODO3 [in CorrelatingProgram]
CP.toto_TODO2 [in CorrelatingProgram]
CP.toto_TODO [in CorrelatingProgram]
CP.to_gl_sound [in CorrelatingProgram]
CP.translation_preserves_classification [in CorrelatingProgram]
CP.truc [in CorrelatingProgram]
CP.two_loops_equiv [in CorrelatingProgram]
CP.two_loops_implied [in CorrelatingProgram]
CP.t_injective_store_proj [in CorrelatingProgram]
D
dummy_correlating_program_sound [in CorrelatingProgram]F
Forall_app [in CorrelatingProgram]L
Languages.eq_guard_dec [in CoqDefs]Languages.my_nth_implies_nth [in CoqDefs]
S
str_t'_inj [in CorrelatingProgram]str_t_inj [in CorrelatingProgram]
str_f_valid [in CorrelatingProgram]
Inductive Index
C
CP.classification [in CorrelatingProgram]CP.cmd_subtree [in CorrelatingProgram]
CP.diff_subtree [in CorrelatingProgram]
CP.two_loops [in CorrelatingProgram]
L
Languages.acmd_g [in CoqDefs]Languages.bexp [in CoqDefs]
Languages.big_step_g [in CoqDefs]
Languages.big_step [in CoqDefs]
Languages.cmd [in CoqDefs]
Languages.cmd_diff [in CoqDefs]
Languages.cmd_g [in CoqDefs]
Languages.cmd_a [in CoqDefs]
Languages.exp [in CoqDefs]
Languages.guard [in CoqDefs]
Languages.lvalue [in CoqDefs]
Languages.mode [in CoqDefs]
Languages.path_suffix [in CoqDefs]
Languages.value [in CoqDefs]
Definition Index
B
bind [in CoqDefs]bind [in CorrelatingProgram]
C
correlating_program [in CorrelatingProgram]CP.add_cpoints [in CorrelatingProgram]
CP.bexp_classified [in CorrelatingProgram]
CP.CI [in CorrelatingProgram]
CP.classification_fun [in CorrelatingProgram]
CP.cmda_classified [in CorrelatingProgram]
CP.cmdg_classified [in CorrelatingProgram]
CP.cmd_classified [in CorrelatingProgram]
CP.correlating_program [in CorrelatingProgram]
CP.cp [in CorrelatingProgram]
CP.diffmap_classified [in CorrelatingProgram]
CP.dummy_correlating_program [in CorrelatingProgram]
CP.dummy_cp [in CorrelatingProgram]
CP.exp_classified [in CorrelatingProgram]
CP.gstore_classified [in CorrelatingProgram]
CP.gstore_included [in CorrelatingProgram]
CP.guard_disj_classified [in CorrelatingProgram]
CP.guard_conj_classified [in CorrelatingProgram]
CP.guard_classified [in CorrelatingProgram]
CP.is_simple_diff [in CorrelatingProgram]
CP.loop_continued [in CorrelatingProgram]
CP.loop_broken [in CorrelatingProgram]
CP.lval_classified [in CorrelatingProgram]
CP.path_length [in CorrelatingProgram]
CP.simplify_diff [in CorrelatingProgram]
CP.store_included [in CorrelatingProgram]
CP.store_classified [in CorrelatingProgram]
CP.tag_diffmap [in CorrelatingProgram]
CP.tag_cmd [in CorrelatingProgram]
CP.tag_cmda [in CorrelatingProgram]
CP.tag_bexp [in CorrelatingProgram]
CP.tag_exp [in CorrelatingProgram]
CP.tag_lval [in CorrelatingProgram]
CP.to_gl [in CorrelatingProgram]
CP.valid_classification_fun [in CorrelatingProgram]
D
dummy_correlating_program [in CorrelatingProgram]L
Languages.cmda_beq [in CoqDefs]Languages.cp_algorithm_sound [in CoqDefs]
Languages.exp_beq [in CoqDefs]
Languages.exp_mut [in CoqDefs]
Languages.gstore [in CoqDefs]
Languages.guard_disj_evals_to [in CoqDefs]
Languages.guard_conj_evals_to [in CoqDefs]
Languages.guard_disj [in CoqDefs]
Languages.guard_conj [in CoqDefs]
Languages.guard_as_DT.eq_dec [in CoqDefs]
Languages.guard_as_DT.eq_trans [in CoqDefs]
Languages.guard_as_DT.eq_sym [in CoqDefs]
Languages.guard_as_DT.eq_refl [in CoqDefs]
Languages.guard_as_DT.eq [in CoqDefs]
Languages.guard_as_DT.t [in CoqDefs]
Languages.interp_guard_conj [in CoqDefs]
Languages.interp_bexp [in CoqDefs]
Languages.interp_exp [in CoqDefs]
Languages.join_stores [in CoqDefs]
Languages.lvalue_beq [in CoqDefs]
Languages.lvalue_mut [in CoqDefs]
Languages.my_nth [in CoqDefs]
Languages.path [in CoqDefs]
Languages.read_lval [in CoqDefs]
Languages.set_lval [in CoqDefs]
Languages.store [in CoqDefs]
Languages.store_included_tagged [in CoqDefs]
Languages.tag_store [in CoqDefs]
Languages.var [in CoqDefs]
Languages.z_to_nat [in CoqDefs]
Languages.Π₀ [in CoqDefs]
Languages.Π₁ [in CoqDefs]
R
ret [in CoqDefs]ret [in CorrelatingProgram]
S
String_as_DT.eq_dec [in CorrelatingProgram]String_as_DT.eq_trans [in CorrelatingProgram]
String_as_DT.eq_sym [in CorrelatingProgram]
String_as_DT.eq_refl [in CorrelatingProgram]
String_as_DT.eq [in CorrelatingProgram]
String_as_DT.t [in CorrelatingProgram]
str_f [in CorrelatingProgram]
str_t' [in CorrelatingProgram]
str_t [in CorrelatingProgram]
T
tag_diff_prefix [in CorrelatingProgram]tag_orig_prefix [in CorrelatingProgram]
| 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 | (307 entries) |
| Notation 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 | (4 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 | _ | other | (15 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 | (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 | _ | other | (107 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 | (78 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 | (18 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 | (83 entries) |
This page has been generated by coqdoc