| 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 | (911 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 | (20 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 | (56 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 | (30 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 | (238 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 | (189 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 | (3 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 | (71 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 | (56 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 | (241 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 | (7 entries) |
Global Index
A
a [constructor, in OracleLanguages.Paper]AbstractEquiv [library]
abstractequiv_example' [definition, in OracleLanguages.Paper]
abstractequiv_example [definition, in OracleLanguages.Paper]
abstract_equiv_or_1 [lemma, in OracleLanguages.Paper]
abstract_equiv_or [definition, in OracleLanguages.Paper]
B
b [constructor, in OracleLanguages.Paper]BigStep [library]
bind [definition, in OracleLanguages.Common]
C
c [constructor, in OracleLanguages.Paper]CCons [constructor, in OracleLanguages.Common]
CConsConverges [constructor, in OracleLanguages.ReductionTrace]
CConsCrashes [constructor, in OracleLanguages.ReductionTrace]
Common [library]
compose_trace_relations_externally [definition, in OracleLanguages.ReductionTracesRelation]
configuration [definition, in OracleLanguages.ProgrammingLanguage]
configuration_eq [definition, in OracleLanguages.ProgrammingLanguage]
coplist [inductive, in OracleLanguages.Common]
CoplistInHead [constructor, in OracleLanguages.Common]
CoplistInSingle [constructor, in OracleLanguages.Common]
CoplistInTail [constructor, in OracleLanguages.Common]
coplist_in [inductive, in OracleLanguages.Common]
coplist_id_force_eq [lemma, in OracleLanguages.Common]
coplist_id_force [definition, in OracleLanguages.Common]
CoreRHL [module, in OracleLanguages.Paper]
CoreRHL [library]
CoreRHLSC [library]
correlation_trace_from [definition, in OracleLanguages.OracleLanguage]
correlation_relation [definition, in OracleLanguages.OracleLanguage]
count [constructor, in OracleLanguages.Paper]
CrashFix [library]
CrashFixWhile [library]
crashfixwhile_or_1 [lemma, in OracleLanguages.Paper]
crashfixwhile_or [definition, in OracleLanguages.Paper]
crashfix_or_1 [lemma, in OracleLanguages.Paper]
crashfix_or [definition, in OracleLanguages.Paper]
crashfix_example' [definition, in OracleLanguages.Paper]
crashfix_example [definition, in OracleLanguages.Paper]
crash_proof [definition, in OracleLanguages.Paper]
crash_fix [definition, in OracleLanguages.Paper]
CSingle [constructor, in OracleLanguages.Common]
D
d [constructor, in OracleLanguages.Paper]difference [projection, in OracleLanguages.DifferenceLanguage]
DifferenceLanguage [library]
difference_language [record, in OracleLanguages.DifferenceLanguage]
DisjointStates [library]
E
ex₁ [definition, in OracleLanguages.Paper]ex₁_γ_correlation_1 [definition, in OracleLanguages.Paper]
ex₁_γ_correlation [definition, in OracleLanguages.Paper]
ex₁_as_id_oracle_step [definition, in OracleLanguages.Paper]
ex₁_as_id_oracle_projections [definition, in OracleLanguages.Paper]
ex₁_as_id_oracle [definition, in OracleLanguages.Paper]
ex₁_trace_converges [definition, in OracleLanguages.Paper]
ex₁_trace_actually_trace [definition, in OracleLanguages.Paper]
ex₁_trace [definition, in OracleLanguages.Paper]
ex₁_final_state_is_final [definition, in OracleLanguages.Paper]
ex₁_final_state [definition, in OracleLanguages.Paper]
ex₁_initial_state [definition, in OracleLanguages.Paper]
ex₁_genv [definition, in OracleLanguages.Paper]
ex₁_initial_configuration [definition, in OracleLanguages.Paper]
ex₂ [definition, in OracleLanguages.Paper]
ex₂_refl [definition, in OracleLanguages.Paper]
F
FinallyConverges [constructor, in OracleLanguages.ReductionTrace]FinallyCrashes [constructor, in OracleLanguages.ReductionTrace]
first [definition, in OracleLanguages.Common]
G
gamma_correlated [inductive, in OracleLanguages.ReductionTracesRelation]genv_eq_dec [projection, in OracleLanguages.ProgrammingLanguage]
genv_eq_trans [projection, in OracleLanguages.ProgrammingLanguage]
genv_eq_sym [projection, in OracleLanguages.ProgrammingLanguage]
genv_eq_refl [projection, in OracleLanguages.ProgrammingLanguage]
genv_eq [projection, in OracleLanguages.ProgrammingLanguage]
genv_type [projection, in OracleLanguages.ProgrammingLanguage]
H
Hoare [library]I
Identity [library]identity_oracle [definition, in OracleLanguages.Oracles.Identity]
identity_oracle [definition, in OracleLanguages.Paper]
id_step_completeness [lemma, in OracleLanguages.Paper]
id_step_soundness [lemma, in OracleLanguages.Paper]
id_step [definition, in OracleLanguages.Paper]
IgnoreFirstSN [constructor, in OracleLanguages.ReductionTrace]
Imp [module, in OracleLanguages.Imp.SmallStep]
Imp [module, in OracleLanguages.Imp.Syntax]
Imp [module, in OracleLanguages.Paper]
ImpBigStep [module, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_div_implies_small_div [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_cont_div_implies_small_div [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_div_implies_small_div_helper' [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_implies_small_helper [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_div_implies_small_div_helper [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_determinist [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_cont_div [inductive, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_cont [inductive, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_implies_small [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_div [inductive, in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step [inductive, in OracleLanguages.Imp.BigStep]
ImpBigStep.Diverges [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.Halted [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while₂ [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while₁ [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_else_inf [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_then_inf [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq₂ [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq₁ [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_assert_true [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while_end [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while_iter [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_else [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_then [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_assign [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.j_skip [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.OneBigStep [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.OneBigStep' [constructor, in OracleLanguages.Imp.BigStep]
ImpBigStep.seq_assoc [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.small_equiv_big [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.small_implies_big [lemma, in OracleLanguages.Imp.BigStep]
ImpBigStep.small_implies_big_helper [lemma, in OracleLanguages.Imp.BigStep]
_ ⊢ _ ⇒ ∞ [notation, in OracleLanguages.Imp.BigStep]
_ ⊢ _ ⇓ _ [notation, in OracleLanguages.Imp.BigStep]
ImpDifferenceLanguage [module, in OracleLanguages.Paper]
ImpDifferenceLanguage [library]
ImpHoare [module, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion [definition, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_implies_trans [lemma, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_implies_refl [lemma, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_implies [definition, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_of_bexp [definition, in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_subst [definition, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareAssert [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareAssign [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareITE [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSeq [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSkip [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSub [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.HoareWhile [constructor, in OracleLanguages.Imp.Hoare]
ImpHoare.hoare_soundness [lemma, in OracleLanguages.Imp.Hoare]
ImpHoare.hoare_proof [inductive, in OracleLanguages.Imp.Hoare]
_ ⇒ _ [notation, in OracleLanguages.Imp.Hoare]
_ [ _ ↦ _ ] [notation, in OracleLanguages.Imp.Hoare]
ImpOracleHelpers [module, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.CmdMod [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.cmd_mod [inductive, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.ContMod [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.cont_mod [inductive, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.GenericStep [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.generic_step_bicrash [lemma, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.generic_step_bistep [lemma, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.Id [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.LeafMod [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.left_mod [definition, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.local_identity [definition, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.RecMod [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.right_mod [definition, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.SpecialCmdStep [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.SpecialContStep [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_special_cont_step_inv [lemma, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_special_cmd_step_inv [lemma, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper [definition, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_id [definition, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_res [inductive, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.StuckStep [constructor, in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage [module, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.finite_small_step_exec_nsteps [lemma, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.finite_small_step_exec [inductive, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.genv_eq_dec [lemma, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.Halted [constructor, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.imp_language [definition, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.infinite_small_step_exec [inductive, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.InfStep [constructor, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.nsteps_compose [lemma, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.nsteps_imp_app_1 [lemma, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.SmallStep [module, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.state_final_no_step [lemma, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.Step [constructor, in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.υ [definition, in OracleLanguages.Imp.Lang]
Imp.AND [constructor, in OracleLanguages.Imp.Syntax]
Imp.Assert [constructor, in OracleLanguages.Imp.Syntax]
Imp.Assign [constructor, in OracleLanguages.Imp.Syntax]
Imp.beq_state [definition, in OracleLanguages.Imp.SmallStep]
Imp.beq_cmd_false_iff [lemma, in OracleLanguages.Imp.Syntax]
Imp.beq_cmd_true_iff [lemma, in OracleLanguages.Imp.Syntax]
Imp.beq_cmd_reflx [lemma, in OracleLanguages.Imp.Syntax]
Imp.beq_cmd [definition, in OracleLanguages.Imp.Syntax]
Imp.beq_bexp [definition, in OracleLanguages.Imp.Syntax]
Imp.beq_exp_reflx [lemma, in OracleLanguages.Imp.Syntax]
Imp.beq_exp [definition, in OracleLanguages.Imp.Syntax]
Imp.bexp [inductive, in OracleLanguages.Imp.Syntax]
Imp.bexp_eq_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.cmd [inductive, in OracleLanguages.Imp.Syntax]
Imp.cmd_eq_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.cont [definition, in OracleLanguages.Imp.SmallStep]
Imp.Div [constructor, in OracleLanguages.Imp.Syntax]
Imp.EQ [constructor, in OracleLanguages.Imp.Syntax]
Imp.EQB [constructor, in OracleLanguages.Imp.Syntax]
Imp.eval_bexp [definition, in OracleLanguages.Imp.Syntax]
Imp.eval_exp [definition, in OracleLanguages.Imp.Syntax]
Imp.exp [inductive, in OracleLanguages.Imp.Syntax]
Imp.exp_eq_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.False [constructor, in OracleLanguages.Imp.Syntax]
Imp.finite_small_step_exec [inductive, in OracleLanguages.Imp.SmallStep]
Imp.Halted [constructor, in OracleLanguages.Imp.SmallStep]
Imp.infinite_small_step_exec [inductive, in OracleLanguages.Imp.SmallStep]
Imp.InfStep [constructor, in OracleLanguages.Imp.SmallStep]
Imp.Int [constructor, in OracleLanguages.Imp.Syntax]
Imp.In_var_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.In_var [definition, in OracleLanguages.Imp.Syntax]
Imp.In_bexp_div_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.In_bexp_var_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.In_bexp_div [definition, in OracleLanguages.Imp.Syntax]
Imp.In_bexp_var [definition, in OracleLanguages.Imp.Syntax]
Imp.In_exp_div_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.In_exp_var_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.In_exp_div [definition, in OracleLanguages.Imp.Syntax]
Imp.In_exp_var [definition, in OracleLanguages.Imp.Syntax]
Imp.ITE [constructor, in OracleLanguages.Imp.Syntax]
Imp.LE [constructor, in OracleLanguages.Imp.Syntax]
Imp.LT [constructor, in OracleLanguages.Imp.Syntax]
Imp.M [module, in OracleLanguages.Imp.Syntax]
Imp.MFacts [module, in OracleLanguages.Imp.Syntax]
Imp.Modulo [constructor, in OracleLanguages.Imp.Syntax]
Imp.MProps [module, in OracleLanguages.Imp.Syntax]
Imp.Mult [constructor, in OracleLanguages.Imp.Syntax]
Imp.NOT [constructor, in OracleLanguages.Imp.Syntax]
Imp.Notations [module, in OracleLanguages.Imp.Syntax]
WHILE _ DO _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
IF _ THEN _ ELSE _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
{ _ ; _ ; .. ; _ } (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ ← _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
¬ _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ && _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ || _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ ≤ _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ < _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ == _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ % _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ * _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ / _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ - _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
_ + _ (ast_scope) [notation, in OracleLanguages.Imp.Syntax]
Imp.OR [constructor, in OracleLanguages.Imp.Syntax]
Imp.Seq [constructor, in OracleLanguages.Imp.Syntax]
Imp.Skip [constructor, in OracleLanguages.Imp.Syntax]
Imp.state [definition, in OracleLanguages.Imp.SmallStep]
Imp.state_final_eq [lemma, in OracleLanguages.Imp.SmallStep]
Imp.state_final [definition, in OracleLanguages.Imp.SmallStep]
Imp.state_eq_trans [lemma, in OracleLanguages.Imp.SmallStep]
Imp.state_eq_refl [lemma, in OracleLanguages.Imp.SmallStep]
Imp.state_eq_sym [lemma, in OracleLanguages.Imp.SmallStep]
Imp.state_eq_dec [lemma, in OracleLanguages.Imp.SmallStep]
Imp.state_eq [definition, in OracleLanguages.Imp.SmallStep]
Imp.Step [constructor, in OracleLanguages.Imp.SmallStep]
Imp.step [definition, in OracleLanguages.Imp.SmallStep]
Imp.step_eq' [lemma, in OracleLanguages.Imp.SmallStep]
Imp.step_eq [lemma, in OracleLanguages.Imp.SmallStep]
Imp.step_app [lemma, in OracleLanguages.Imp.SmallStep]
Imp.store [definition, in OracleLanguages.Imp.Syntax]
Imp.store_equal_eval_bexp [lemma, in OracleLanguages.Imp.Syntax]
Imp.store_equal_eval_exp [lemma, in OracleLanguages.Imp.Syntax]
Imp.store_Equal_dec [lemma, in OracleLanguages.Imp.Syntax]
Imp.store_equal_true_iff [lemma, in OracleLanguages.Imp.Syntax]
Imp.store_equal [definition, in OracleLanguages.Imp.Syntax]
Imp.Sub [constructor, in OracleLanguages.Imp.Syntax]
Imp.Sum [constructor, in OracleLanguages.Imp.Syntax]
Imp.Syntax [module, in OracleLanguages.Imp.SmallStep]
Imp.True [constructor, in OracleLanguages.Imp.Syntax]
Imp.Var [constructor, in OracleLanguages.Imp.Syntax]
Imp.varid [definition, in OracleLanguages.Imp.Syntax]
Imp.While [constructor, in OracleLanguages.Imp.Syntax]
included_subtrace [inductive, in OracleLanguages.ReductionTrace]
initial_configuration [definition, in OracleLanguages.ProgrammingLanguage]
initial_state [projection, in OracleLanguages.ProgrammingLanguage]
interpret [projection, in OracleLanguages.DifferenceLanguage]
invariant [projection, in OracleLanguages.OracleLanguage]
invariant_1 [projection, in OracleLanguages.OracleLanguage]
L
L [axiom, in OracleLanguages.Oracles.Identity]Lang [library]
language [record, in OracleLanguages.ProgrammingLanguage]
left_trace [definition, in OracleLanguages.OracleLanguage]
left_genv [projection, in OracleLanguages.OracleLanguage]
left_state [projection, in OracleLanguages.OracleLanguage]
L₁ [axiom, in OracleLanguages.Oracles.UniversalOracle]
L₂ [axiom, in OracleLanguages.Oracles.UniversalOracle]
M
Make [module, in OracleLanguages.Imp.BigStep]Make [module, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make [module, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make [module, in OracleLanguages.Imp.Oracles.ValueChange]
Make [module, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make [module, in OracleLanguages.Imp.DisjointStates]
Make [module, in OracleLanguages.Imp.Hoare]
Make [module, in OracleLanguages.Imp.Lang]
Make [module, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make [module, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make [module, in OracleLanguages.Imp.RHL]
Make [module, in OracleLanguages.Imp.Oracles.SwapAssign]
Make [module, in OracleLanguages.Imp.Oracles.CrashFix]
Make [module, in OracleLanguages.Imp.Oracles.OracleHelpers]
Make [module, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make [module, in OracleLanguages.Imp.Oracles.SwapBranches]
Make [module, in OracleLanguages.Imp.Oracles.CoreRHL]
Make [module, in OracleLanguages.Imp.Oracles.Renaming]
Make.AbstractEquiv [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.abstract_equiv_oracle [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.apply_cmd_mod_id [lemma, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.apply_cmd_mod [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.apply_cmd_mod_id [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.apply_cmd_mod [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.apply_cmd_mod_id [lemma, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.apply_cmd_mod [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.apply_cmd_mod_id [lemma, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.apply_cmd_mod [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.assign_indep [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.assign_indep' [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.BigStep [module, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.BigStep [module, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.BigStep [module, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.bijection [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.bijective [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.body [projection, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.bound [projection, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.close_skip_skip [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.close_assign [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.close_skip_skip [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.cmd_mod_from_imp_ctx [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.cmd_cont [constructor, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.Compare [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Compose [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.condition [projection, in OracleLanguages.Imp.Oracles.CrashFix]
Make.cont_classified_2 [lemma, in OracleLanguages.Imp.DisjointStates]
Make.cont_classified_1 [lemma, in OracleLanguages.Imp.DisjointStates]
Make.cont_classified [definition, in OracleLanguages.Imp.DisjointStates]
Make.cont_mod_inv [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.CoreAssert [constructor, in OracleLanguages.Imp.RHL]
Make.CoreAssertLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreAssertRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreAssign [constructor, in OracleLanguages.Imp.RHL]
Make.CoreAssignLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreAssignRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreITE [constructor, in OracleLanguages.Imp.RHL]
Make.CoreITELeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreITERight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreRHLSC [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CoreSCAssert [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCAssertLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCAssertRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCAssign [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCAssignLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCAssignRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCITE [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCITELeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCITERight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSelfComp [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSeq [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSeqSkipLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSeqSkipRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSkip [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCSub [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSCWhile [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSeq [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSeqSkipLeft [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSeqSkipRight [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSkip [constructor, in OracleLanguages.Imp.RHL]
Make.CoreSub [constructor, in OracleLanguages.Imp.RHL]
Make.CoreWhile [constructor, in OracleLanguages.Imp.RHL]
Make.core_rhl_sc_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.core_rhl_oracle [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.core_rhl_sc_proof [inductive, in OracleLanguages.Imp.RHL]
Make.core_rhl_proof [inductive, in OracleLanguages.Imp.RHL]
Make.core_rhl_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.core_rhl_oracle [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.CrashFix [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CrashFixWhile [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CrashFixWhile [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.crashfixwhile_oracle [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crashfix_oracle [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make.crash_avoided_1 [projection, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crash_bound [projection, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crash_avoided_1 [projection, in OracleLanguages.Imp.Oracles.CrashFix]
Make.crash_bound [projection, in OracleLanguages.Imp.Oracles.CrashFix]
Make.CtxHole [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxIfElse [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxIfThen [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxSeqL [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxSeqR [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxWhile [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.c_right [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.c_left [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.c_else [projection, in OracleLanguages.Imp.Oracles.CrashFix]
Make.c_then [projection, in OracleLanguages.Imp.Oracles.CrashFix]
Make.DisjointStates [module, in OracleLanguages.Imp.RHL]
Make.disjoint_union_eval_bexp_same [lemma, in OracleLanguages.Imp.DisjointStates]
Make.disjoint_union_eval_exp_same [lemma, in OracleLanguages.Imp.DisjointStates]
Make.disjoint_eval_bexp [lemma, in OracleLanguages.Imp.DisjointStates]
Make.disjoint_eval_exp [lemma, in OracleLanguages.Imp.DisjointStates]
Make.disjoint_states_sym [lemma, in OracleLanguages.Imp.DisjointStates]
Make.disjoint_states [definition, in OracleLanguages.Imp.DisjointStates]
Make.either [inductive, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.empty_cont_mod [constructor, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.equal_store_is_union [lemma, in OracleLanguages.Imp.DisjointStates]
Make.eval_exp_add_neq' [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.eval_exp_add_neq [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.expression [projection, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.ExtraUnfoldLeft [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.ExtraUnfoldRight [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.extra_unfold_right_inv [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.extra_unfold_left_inv [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.FixCrash [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.FoldSeq [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.fold_seq [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.genv [projection, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Hoare [module, in OracleLanguages.Imp.RHL]
Make.HoareProof [constructor, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.HoareProof [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProof [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.HoareProofL [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProofL [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.HoareProofR [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProofR [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.hoare_close_skip_skip [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.hoare_close_skip [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.imp [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.imp_difference_language [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.imp_ctx [inductive, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.interpret_difference [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.interpret_primitive_difference [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.In_var_cont [definition, in OracleLanguages.Imp.DisjointStates]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.CrashFix]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.km_invariant [inductive, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.leaf_mod_of_cmds [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.leaf_mod_of_cmds [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.Left [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_fun_spec_2 [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_fun_spec_1 [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_equiv_right [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_fun [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.map_swap_add_neq [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.MinimalAssert [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalAssign [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalITE [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalSeq [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalSkip [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalSub [constructor, in OracleLanguages.Imp.RHL]
Make.MinimalWhile [constructor, in OracleLanguages.Imp.RHL]
Make.minimal_rhl_soundness [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.minimal_rhl_oracle [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.minimal_rhl_proof [inductive, in OracleLanguages.Imp.RHL]
Make.mod [inductive, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.mod [record, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod [inductive, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.mod [record, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod [inductive, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.mod [inductive, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.modif [record, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_special' [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_special [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_while [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_ite [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_seq [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_id [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_invariant [inductive, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_special [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_while [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_ite [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_seq [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_id [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_invariant [inductive, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_special [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_while [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_ite [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_seq [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_id [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_invariant [inductive, in OracleLanguages.Imp.Oracles.CrashFix]
Make.Negate [constructor, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.no_crash [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.no_crash [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.no_crash [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.Optimize [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.oracle [record, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.OracleHelpers [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.oracle_from_primitive_diff [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.oracle_step [definition, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.OT [projection, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.perform_n_steps [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.perform_n_steps [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.perform_n_m_steps [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.primitive_difference [inductive, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.proof_terms_match_cons [constructor, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match_nil [constructor, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match [inductive, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_consistent_1 [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_consistent [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_term [inductive, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match_cons_r' [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_l' [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_r [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_l [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_nil [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match [inductive, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_consistent_1 [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_consistent [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_term [inductive, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_r [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_cons_l [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_cons [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_nil [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match [inductive, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_consistent_1 [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_consistent [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_term [inductive, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.Refactor [constructor, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.Refactor [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RefactorCommonBranchRemainder [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RefactorCommonBranchRemainder [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.refactor_common_branch_trailer_oracle [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.refactor_common_trailer [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.rename_store_comm_add [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_Equal [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_eval_bexp [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_eval_exp [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_store_preserves_values [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_store [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_store_helper [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_cont [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_cmd [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_bexp [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_exp [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.Renaming [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Renaming [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.renaming_oracle [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make.RHL [module, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.RHL [module, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.RHL [module, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.RHLProof [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Right [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.right_fun_spec_2 [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.right_fun_spec_1 [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.right_fun [projection, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.same_control_store_add_stable' [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_add_stable [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_exp_crash [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_eval_bexp [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_eval_exp [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_cont [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_assert [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_assign [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_While [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_ITE [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_seq [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_skip [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_cmd [inductive, in OracleLanguages.Imp.Oracles.ValueChange]
Make.SeqAssoc [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SeqAssoc [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.seqassoc_oracle [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.SingleHoareProofL [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.SingleHoareProofR [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.State [constructor, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.State [constructor, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.State [constructor, in OracleLanguages.Imp.Oracles.ValueChange]
Make.State [constructor, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.state [projection, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.State [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.State [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.State [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.State [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.State [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.State [constructor, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.State [constructor, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.State [constructor, in OracleLanguages.Imp.Oracles.Renaming]
Make.state_final_nocrash [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.state_final_nocrash [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.state_final_nocrash [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make.step_disjoint_union_states [lemma, in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states_union_same_crashes [lemma, in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states_union [lemma, in OracleLanguages.Imp.DisjointStates]
Make.step_2_disjoint_states [lemma, in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states [lemma, in OracleLanguages.Imp.DisjointStates]
Make.store_classified [definition, in OracleLanguages.Imp.DisjointStates]
Make.store_is_union_add [lemma, in OracleLanguages.Imp.DisjointStates]
Make.store_is_union_sym [lemma, in OracleLanguages.Imp.DisjointStates]
Make.store_is_union [definition, in OracleLanguages.Imp.DisjointStates]
Make.Stuck [constructor, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.Stuck [constructor, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.Stuck [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.StuckLeft [constructor, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.StuckLeft [constructor, in OracleLanguages.Imp.Oracles.CrashFix]
Make.Superpose [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Swap [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.SwapAssign [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapAssign [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.swapassign_oracle [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.SwapBranches [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapBranches [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.swapbranches_oracle [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.SwapCont [constructor, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.swap_assignments [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make.syntactic_un_negate [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.syntactic_negate [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.t [inductive, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.UnfoldSeq [constructor, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.unfold_seq [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.UnNegate [constructor, in OracleLanguages.Imp.Oracles.SwapBranches]
Make.ValueChange [constructor, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.ValueChange [module, in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.valuechange_oracle [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._step [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._step_helper [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._state [inductive, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._genv [definition, in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_invariant [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_invariant [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_no_crash [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_no_crash [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_right [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_left [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._split_hoare_seq_1 [lemma, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._split_hoare_seq [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._state [inductive, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._genv [definition, in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.ValueChange]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._step [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._state [inductive, in OracleLanguages.Imp.Oracles.ValueChange]
Make._genv [definition, in OracleLanguages.Imp.Oracles.ValueChange]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._step [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._state [inductive, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._genv [definition, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._step [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._state [inductive, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._genv [definition, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._step [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._state [inductive, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._genv [definition, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._step [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._state [inductive, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._genv [definition, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.SwapAssign]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.CrashFix]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.CrashFix]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.CrashFix]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make._step [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make._state [inductive, in OracleLanguages.Imp.Oracles.CrashFix]
Make._genv [definition, in OracleLanguages.Imp.Oracles.CrashFix]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.CrashFix]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._step [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._state [inductive, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._genv [definition, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._step [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._state [inductive, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._genv [definition, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._cont_mod [inductive, in OracleLanguages.Imp.Oracles.SwapBranches]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper_right [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper_left [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._state [inductive, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._genv [definition, in OracleLanguages.Imp.Oracles.CoreRHL]
Make._prediction_completeness [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make._prediction_soundness [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make._invariant_1 [lemma, in OracleLanguages.Imp.Oracles.Renaming]
Make._invariant [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make._right_state [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make._left_state [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make._step [definition, in OracleLanguages.Imp.Oracles.Renaming]
Make._state [inductive, in OracleLanguages.Imp.Oracles.Renaming]
Make._genv [definition, in OracleLanguages.Imp.Oracles.Renaming]
map [definition, in OracleLanguages.Common]
MinimalRHL [module, in OracleLanguages.Paper]
MinimalRHL [library]
N
n [constructor, in OracleLanguages.Paper]napply [definition, in OracleLanguages.Common]
napply_napply'_0_iff [lemma, in OracleLanguages.Common]
napply_napply'_Sn_iff [lemma, in OracleLanguages.Common]
napply' [definition, in OracleLanguages.Common]
napply'_lt_id [lemma, in OracleLanguages.Common]
napply'_prefix [lemma, in OracleLanguages.Common]
napply'_1 [lemma, in OracleLanguages.Common]
next [definition, in OracleLanguages.Common]
nsteps [definition, in OracleLanguages.ProgrammingLanguage]
nsteps_split_helper [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_plus_2 [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_plus_1' [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_plus_1 [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_plus_0 [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_eq [lemma, in OracleLanguages.ProgrammingLanguage]
nsteps_skipn [lemma, in OracleLanguages.ReductionTrace]
nsteps_crashing_trace [inductive, in OracleLanguages.ReductionTrace]
nsteps_converging_trace [inductive, in OracleLanguages.ReductionTrace]
nsteps_helper_1 [lemma, in OracleLanguages.Paper]
nsteps_helper [definition, in OracleLanguages.Paper]
nsteps' [definition, in OracleLanguages.ProgrammingLanguage]
O
opt_state_eq_trans [lemma, in OracleLanguages.ProgrammingLanguage]opt_state_eq_sym [lemma, in OracleLanguages.ProgrammingLanguage]
opt_state_eq_refl [lemma, in OracleLanguages.ProgrammingLanguage]
opt_state_eq_Some_r__state_eq [lemma, in OracleLanguages.ProgrammingLanguage]
opt_state_eq_dec [lemma, in OracleLanguages.ProgrammingLanguage]
opt_state_eq [definition, in OracleLanguages.ProgrammingLanguage]
OracleHelpers [library]
OracleLanguage [library]
OracleStepEquality [constructor, in OracleLanguages.OracleLanguage]
OracleStuckEquality [constructor, in OracleLanguages.OracleLanguage]
oracle_nsteps_termination'' [lemma, in OracleLanguages.OracleLanguage]
oracle_nsteps_termination [lemma, in OracleLanguages.OracleLanguage]
oracle_nsteps_right [lemma, in OracleLanguages.OracleLanguage]
oracle_nsteps_left [lemma, in OracleLanguages.OracleLanguage]
oracle_nsteps' [definition, in OracleLanguages.OracleLanguage]
oracle_nsteps [definition, in OracleLanguages.OracleLanguage]
oracle_eq_trans [lemma, in OracleLanguages.OracleLanguage]
oracle_eq_sym [lemma, in OracleLanguages.OracleLanguage]
oracle_eq_refl [lemma, in OracleLanguages.OracleLanguage]
oracle_eq [inductive, in OracleLanguages.OracleLanguage]
oracle_gamma_correlated [lemma, in OracleLanguages.OracleLanguage]
oracle_relates_configurations_of_programs [lemma, in OracleLanguages.OracleLanguage]
oracle_correlation_relation [definition, in OracleLanguages.OracleLanguage]
oracle_step [projection, in OracleLanguages.OracleLanguage]
oracle_genv [projection, in OracleLanguages.OracleLanguage]
oracle_state [projection, in OracleLanguages.OracleLanguage]
oracle_language [record, in OracleLanguages.OracleLanguage]
P
Paper [library]pow [constructor, in OracleLanguages.Paper]
prediction_completeness [projection, in OracleLanguages.OracleLanguage]
prediction_soundness [projection, in OracleLanguages.OracleLanguage]
prog [projection, in OracleLanguages.ProgrammingLanguage]
ProgrammingLanguage [library]
program_trace [definition, in OracleLanguages.ReductionTrace]
P₀ [definition, in OracleLanguages.Paper]
P₀_crashes [lemma, in OracleLanguages.Paper]
P₀_loop_crashes [lemma, in OracleLanguages.Paper]
P₁ [definition, in OracleLanguages.Paper]
P₁_loop_body_crashes [lemma, in OracleLanguages.Paper]
P₁_loop_body [definition, in OracleLanguages.Paper]
P₁_loop_ctx [definition, in OracleLanguages.Paper]
P₂ [definition, in OracleLanguages.Paper]
P₂_does_not_crash [lemma, in OracleLanguages.Paper]
P₂_loop_does_not_crash [lemma, in OracleLanguages.Paper]
R
ReductionTrace [library]ReductionTracesRelation [library]
RefactorCommonBranchRemainder [library]
renaming [definition, in OracleLanguages.Paper]
Renaming [library]
renaming_ex₁_1 [definition, in OracleLanguages.Paper]
renaming_ex₁ [definition, in OracleLanguages.Paper]
ret [definition, in OracleLanguages.Common]
return_type [projection, in OracleLanguages.ProgrammingLanguage]
RHL [library]
right_trace [definition, in OracleLanguages.OracleLanguage]
right_genv [projection, in OracleLanguages.OracleLanguage]
right_state [projection, in OracleLanguages.OracleLanguage]
S
s [constructor, in OracleLanguages.Paper]SameFirst [constructor, in OracleLanguages.ReductionTrace]
SeqAssoc [library]
skipn [definition, in OracleLanguages.Common]
SmallStep [library]
sound_program_difference [definition, in OracleLanguages.DifferenceLanguage]
state [projection, in OracleLanguages.ProgrammingLanguage]
state_eq__opt_state_eq [lemma, in OracleLanguages.ProgrammingLanguage]
state_final_eq [projection, in OracleLanguages.ProgrammingLanguage]
state_eq_dec [projection, in OracleLanguages.ProgrammingLanguage]
state_eq_trans [projection, in OracleLanguages.ProgrammingLanguage]
state_eq_sym [projection, in OracleLanguages.ProgrammingLanguage]
state_eq_refl [projection, in OracleLanguages.ProgrammingLanguage]
state_eq [projection, in OracleLanguages.ProgrammingLanguage]
state_final_no_step [projection, in OracleLanguages.ProgrammingLanguage]
state_final [projection, in OracleLanguages.ProgrammingLanguage]
step [projection, in OracleLanguages.ProgrammingLanguage]
StepCorrelated [constructor, in OracleLanguages.ReductionTracesRelation]
step_eq' [projection, in OracleLanguages.ProgrammingLanguage]
step_eq [projection, in OracleLanguages.ProgrammingLanguage]
Stutter [constructor, in OracleLanguages.ReductionTrace]
SwapAssign [library]
SwapBranches [library]
swap_ite_or_1 [lemma, in OracleLanguages.Paper]
swap_ite_or [definition, in OracleLanguages.Paper]
swap_ite_example' [definition, in OracleLanguages.Paper]
swap_ite_example [definition, in OracleLanguages.Paper]
swap_assign_or_1 [lemma, in OracleLanguages.Paper]
swap_assign_or [definition, in OracleLanguages.Paper]
swap_example' [definition, in OracleLanguages.Paper]
swap_example [definition, in OracleLanguages.Paper]
Syntax [library]
T
take [definition, in OracleLanguages.Common]TerminatedCorrelated [constructor, in OracleLanguages.ReductionTracesRelation]
terminates [definition, in OracleLanguages.ProgrammingLanguage]
TFinal [constructor, in OracleLanguages.ReductionTrace]
trace [inductive, in OracleLanguages.ReductionTrace]
traceFrom [definition, in OracleLanguages.ReductionTrace]
traceFrom_trace [lemma, in OracleLanguages.ReductionTrace]
trace_relation [definition, in OracleLanguages.ReductionTracesRelation]
trace_trace' [lemma, in OracleLanguages.ReductionTrace]
trace_first [lemma, in OracleLanguages.ReductionTrace]
trace' [definition, in OracleLanguages.ReductionTrace]
TStep [constructor, in OracleLanguages.ReductionTrace]
U
UniversalOracle [library]universal_oracle [definition, in OracleLanguages.Oracles.UniversalOracle]
V
ValueChange [library]valuechange_or_1 [lemma, in OracleLanguages.Paper]
valuechange_or [definition, in OracleLanguages.Paper]
valuechange_example' [definition, in OracleLanguages.Paper]
valuechange_example [definition, in OracleLanguages.Paper]
Var [module, in OracleLanguages.Paper]
varid [inductive, in OracleLanguages.Paper]
varid_eq_dec [lemma, in OracleLanguages.Paper]
Var_as_DT [module, in OracleLanguages.Paper]
Var.eq_dec [definition, in OracleLanguages.Paper]
Var.t [definition, in OracleLanguages.Paper]
X
x [constructor, in OracleLanguages.Paper]Y
y [constructor, in OracleLanguages.Paper]Z
z [constructor, in OracleLanguages.Paper]_
_prediction_completeness [lemma, in OracleLanguages.Oracles.UniversalOracle]_prediction_soundness [lemma, in OracleLanguages.Oracles.UniversalOracle]
_step [definition, in OracleLanguages.Oracles.UniversalOracle]
_genv [definition, in OracleLanguages.Oracles.UniversalOracle]
_state [definition, in OracleLanguages.Oracles.UniversalOracle]
_prediction_completeness [lemma, in OracleLanguages.Oracles.Identity]
_prediction_soundness [lemma, in OracleLanguages.Oracles.Identity]
_state [definition, in OracleLanguages.Oracles.Identity]
other
_ >>= _ [notation, in OracleLanguages.Common]γ_from_oracle [definition, in OracleLanguages.OracleLanguage]
δ [definition, in OracleLanguages.Paper]
δ_sound [lemma, in OracleLanguages.Paper]
φ [definition, in OracleLanguages.Paper]
φ' [definition, in OracleLanguages.Paper]
Notation Index
I
_ ⊢ _ ⇒ ∞ [in OracleLanguages.Imp.BigStep]_ ⊢ _ ⇓ _ [in OracleLanguages.Imp.BigStep]
_ ⇒ _ [in OracleLanguages.Imp.Hoare]
_ [ _ ↦ _ ] [in OracleLanguages.Imp.Hoare]
WHILE _ DO _ (ast_scope) [in OracleLanguages.Imp.Syntax]
IF _ THEN _ ELSE _ (ast_scope) [in OracleLanguages.Imp.Syntax]
{ _ ; _ ; .. ; _ } (ast_scope) [in OracleLanguages.Imp.Syntax]
_ ← _ (ast_scope) [in OracleLanguages.Imp.Syntax]
¬ _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ && _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ || _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ ≤ _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ < _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ == _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ % _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ * _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ / _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ - _ (ast_scope) [in OracleLanguages.Imp.Syntax]
_ + _ (ast_scope) [in OracleLanguages.Imp.Syntax]
other
_ >>= _ [in OracleLanguages.Common]Module Index
C
CoreRHL [in OracleLanguages.Paper]I
Imp [in OracleLanguages.Imp.SmallStep]Imp [in OracleLanguages.Imp.Syntax]
Imp [in OracleLanguages.Paper]
ImpBigStep [in OracleLanguages.Imp.BigStep]
ImpDifferenceLanguage [in OracleLanguages.Paper]
ImpHoare [in OracleLanguages.Imp.Hoare]
ImpOracleHelpers [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.SmallStep [in OracleLanguages.Imp.Lang]
Imp.M [in OracleLanguages.Imp.Syntax]
Imp.MFacts [in OracleLanguages.Imp.Syntax]
Imp.MProps [in OracleLanguages.Imp.Syntax]
Imp.Notations [in OracleLanguages.Imp.Syntax]
Imp.Syntax [in OracleLanguages.Imp.SmallStep]
M
Make [in OracleLanguages.Imp.BigStep]Make [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make [in OracleLanguages.Imp.Oracles.ValueChange]
Make [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make [in OracleLanguages.Imp.DisjointStates]
Make [in OracleLanguages.Imp.Hoare]
Make [in OracleLanguages.Imp.Lang]
Make [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make [in OracleLanguages.Imp.RHL]
Make [in OracleLanguages.Imp.Oracles.SwapAssign]
Make [in OracleLanguages.Imp.Oracles.CrashFix]
Make [in OracleLanguages.Imp.Oracles.OracleHelpers]
Make [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make [in OracleLanguages.Imp.Oracles.SwapBranches]
Make [in OracleLanguages.Imp.Oracles.CoreRHL]
Make [in OracleLanguages.Imp.Oracles.Renaming]
Make.AbstractEquiv [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.BigStep [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.BigStep [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.BigStep [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.CoreRHLSC [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CrashFix [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CrashFixWhile [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.DisjointStates [in OracleLanguages.Imp.RHL]
Make.Hoare [in OracleLanguages.Imp.RHL]
Make.OracleHelpers [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RefactorCommonBranchRemainder [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Renaming [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RHL [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.RHL [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.RHL [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.SeqAssoc [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapAssign [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapBranches [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.ValueChange [in OracleLanguages.Imp.ImpDifferenceLanguage]
MinimalRHL [in OracleLanguages.Paper]
V
Var [in OracleLanguages.Paper]Var_as_DT [in OracleLanguages.Paper]
Library Index
A
AbstractEquivB
BigStepC
CommonCoreRHL
CoreRHLSC
CrashFix
CrashFixWhile
D
DifferenceLanguageDisjointStates
H
HoareI
IdentityImpDifferenceLanguage
L
LangM
MinimalRHLO
OracleHelpersOracleLanguage
P
PaperProgrammingLanguage
R
ReductionTraceReductionTracesRelation
RefactorCommonBranchRemainder
Renaming
RHL
S
SeqAssocSmallStep
SwapAssign
SwapBranches
Syntax
U
UniversalOracleV
ValueChangeConstructor Index
A
a [in OracleLanguages.Paper]B
b [in OracleLanguages.Paper]C
c [in OracleLanguages.Paper]CCons [in OracleLanguages.Common]
CConsConverges [in OracleLanguages.ReductionTrace]
CConsCrashes [in OracleLanguages.ReductionTrace]
CoplistInHead [in OracleLanguages.Common]
CoplistInSingle [in OracleLanguages.Common]
CoplistInTail [in OracleLanguages.Common]
count [in OracleLanguages.Paper]
CSingle [in OracleLanguages.Common]
D
d [in OracleLanguages.Paper]F
FinallyConverges [in OracleLanguages.ReductionTrace]FinallyCrashes [in OracleLanguages.ReductionTrace]
I
IgnoreFirstSN [in OracleLanguages.ReductionTrace]ImpBigStep.Diverges [in OracleLanguages.Imp.BigStep]
ImpBigStep.Halted [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while₂ [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while₁ [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_else_inf [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_then_inf [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq₂ [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq₁ [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_assert_true [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while_end [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_while_iter [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_else [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_if_then [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_assign [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_seq [in OracleLanguages.Imp.BigStep]
ImpBigStep.j_skip [in OracleLanguages.Imp.BigStep]
ImpBigStep.OneBigStep [in OracleLanguages.Imp.BigStep]
ImpBigStep.OneBigStep' [in OracleLanguages.Imp.BigStep]
ImpHoare.HoareAssert [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareAssign [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareITE [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSeq [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSkip [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareSub [in OracleLanguages.Imp.Hoare]
ImpHoare.HoareWhile [in OracleLanguages.Imp.Hoare]
ImpOracleHelpers.CmdMod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.ContMod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.GenericStep [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.Id [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.LeafMod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.RecMod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.SpecialCmdStep [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.SpecialContStep [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.StuckStep [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage.Halted [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.InfStep [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.Step [in OracleLanguages.Imp.Lang]
Imp.AND [in OracleLanguages.Imp.Syntax]
Imp.Assert [in OracleLanguages.Imp.Syntax]
Imp.Assign [in OracleLanguages.Imp.Syntax]
Imp.Div [in OracleLanguages.Imp.Syntax]
Imp.EQ [in OracleLanguages.Imp.Syntax]
Imp.EQB [in OracleLanguages.Imp.Syntax]
Imp.False [in OracleLanguages.Imp.Syntax]
Imp.Halted [in OracleLanguages.Imp.SmallStep]
Imp.InfStep [in OracleLanguages.Imp.SmallStep]
Imp.Int [in OracleLanguages.Imp.Syntax]
Imp.ITE [in OracleLanguages.Imp.Syntax]
Imp.LE [in OracleLanguages.Imp.Syntax]
Imp.LT [in OracleLanguages.Imp.Syntax]
Imp.Modulo [in OracleLanguages.Imp.Syntax]
Imp.Mult [in OracleLanguages.Imp.Syntax]
Imp.NOT [in OracleLanguages.Imp.Syntax]
Imp.OR [in OracleLanguages.Imp.Syntax]
Imp.Seq [in OracleLanguages.Imp.Syntax]
Imp.Skip [in OracleLanguages.Imp.Syntax]
Imp.Step [in OracleLanguages.Imp.SmallStep]
Imp.Sub [in OracleLanguages.Imp.Syntax]
Imp.Sum [in OracleLanguages.Imp.Syntax]
Imp.True [in OracleLanguages.Imp.Syntax]
Imp.Var [in OracleLanguages.Imp.Syntax]
Imp.While [in OracleLanguages.Imp.Syntax]
M
Make.close_assign [in OracleLanguages.Imp.Oracles.ValueChange]Make.cmd_cont [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.CrashFix]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.cmd_cont [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.Compare [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Compose [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.cont_mod_inv [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.CoreAssert [in OracleLanguages.Imp.RHL]
Make.CoreAssertLeft [in OracleLanguages.Imp.RHL]
Make.CoreAssertRight [in OracleLanguages.Imp.RHL]
Make.CoreAssign [in OracleLanguages.Imp.RHL]
Make.CoreAssignLeft [in OracleLanguages.Imp.RHL]
Make.CoreAssignRight [in OracleLanguages.Imp.RHL]
Make.CoreITE [in OracleLanguages.Imp.RHL]
Make.CoreITELeft [in OracleLanguages.Imp.RHL]
Make.CoreITERight [in OracleLanguages.Imp.RHL]
Make.CoreSCAssert [in OracleLanguages.Imp.RHL]
Make.CoreSCAssertLeft [in OracleLanguages.Imp.RHL]
Make.CoreSCAssertRight [in OracleLanguages.Imp.RHL]
Make.CoreSCAssign [in OracleLanguages.Imp.RHL]
Make.CoreSCAssignLeft [in OracleLanguages.Imp.RHL]
Make.CoreSCAssignRight [in OracleLanguages.Imp.RHL]
Make.CoreSCITE [in OracleLanguages.Imp.RHL]
Make.CoreSCITELeft [in OracleLanguages.Imp.RHL]
Make.CoreSCITERight [in OracleLanguages.Imp.RHL]
Make.CoreSCSelfComp [in OracleLanguages.Imp.RHL]
Make.CoreSCSeq [in OracleLanguages.Imp.RHL]
Make.CoreSCSeqSkipLeft [in OracleLanguages.Imp.RHL]
Make.CoreSCSeqSkipRight [in OracleLanguages.Imp.RHL]
Make.CoreSCSkip [in OracleLanguages.Imp.RHL]
Make.CoreSCSub [in OracleLanguages.Imp.RHL]
Make.CoreSCWhile [in OracleLanguages.Imp.RHL]
Make.CoreSeq [in OracleLanguages.Imp.RHL]
Make.CoreSeqSkipLeft [in OracleLanguages.Imp.RHL]
Make.CoreSeqSkipRight [in OracleLanguages.Imp.RHL]
Make.CoreSkip [in OracleLanguages.Imp.RHL]
Make.CoreSub [in OracleLanguages.Imp.RHL]
Make.CoreWhile [in OracleLanguages.Imp.RHL]
Make.CrashFixWhile [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxHole [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxIfElse [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxIfThen [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxSeqL [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxSeqR [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.CtxWhile [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.CrashFix]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.empty_cont_mod [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.ExtraUnfoldLeft [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.ExtraUnfoldRight [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.extra_unfold_right_inv [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.extra_unfold_left_inv [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.FixCrash [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.FoldSeq [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.HoareProof [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.HoareProof [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProof [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.HoareProofL [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProofL [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.HoareProofR [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.HoareProofR [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.Left [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.MinimalAssert [in OracleLanguages.Imp.RHL]
Make.MinimalAssign [in OracleLanguages.Imp.RHL]
Make.MinimalITE [in OracleLanguages.Imp.RHL]
Make.MinimalSeq [in OracleLanguages.Imp.RHL]
Make.MinimalSkip [in OracleLanguages.Imp.RHL]
Make.MinimalSub [in OracleLanguages.Imp.RHL]
Make.MinimalWhile [in OracleLanguages.Imp.RHL]
Make.mod_special' [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_special [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_while [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_ite [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_rec_seq [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_id [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_special [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_while [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_ite [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_rec_seq [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_id [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_special [in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_while [in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_ite [in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_rec_seq [in OracleLanguages.Imp.Oracles.CrashFix]
Make.mod_id [in OracleLanguages.Imp.Oracles.CrashFix]
Make.Negate [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.Optimize [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.proof_terms_match_cons [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match_nil [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match_cons_r' [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_l' [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_r [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_l [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_nil [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match_cons_r [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_cons_l [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_cons [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_match_nil [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.Refactor [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.Refactor [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RefactorCommonBranchRemainder [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Renaming [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.RHLProof [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Right [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.same_assert [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_assign [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_While [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_ITE [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_seq [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_skip [in OracleLanguages.Imp.Oracles.ValueChange]
Make.SeqAssoc [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SingleHoareProofL [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.SingleHoareProofR [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.State [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.State [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.State [in OracleLanguages.Imp.Oracles.ValueChange]
Make.State [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.State [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.State [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.State [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.State [in OracleLanguages.Imp.Oracles.CrashFix]
Make.State [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.State [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.State [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.State [in OracleLanguages.Imp.Oracles.Renaming]
Make.Stuck [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.Stuck [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.Stuck [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.StuckLeft [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.StuckLeft [in OracleLanguages.Imp.Oracles.CrashFix]
Make.Superpose [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.Swap [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.SwapAssign [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapBranches [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.SwapCont [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.UnfoldSeq [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.UnNegate [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.ValueChange [in OracleLanguages.Imp.ImpDifferenceLanguage]
N
n [in OracleLanguages.Paper]O
OracleStepEquality [in OracleLanguages.OracleLanguage]OracleStuckEquality [in OracleLanguages.OracleLanguage]
P
pow [in OracleLanguages.Paper]S
s [in OracleLanguages.Paper]SameFirst [in OracleLanguages.ReductionTrace]
StepCorrelated [in OracleLanguages.ReductionTracesRelation]
Stutter [in OracleLanguages.ReductionTrace]
T
TerminatedCorrelated [in OracleLanguages.ReductionTracesRelation]TFinal [in OracleLanguages.ReductionTrace]
TStep [in OracleLanguages.ReductionTrace]
X
x [in OracleLanguages.Paper]Y
y [in OracleLanguages.Paper]Z
z [in OracleLanguages.Paper]Lemma Index
A
abstract_equiv_or_1 [in OracleLanguages.Paper]C
coplist_id_force_eq [in OracleLanguages.Common]crashfixwhile_or_1 [in OracleLanguages.Paper]
crashfix_or_1 [in OracleLanguages.Paper]
I
id_step_completeness [in OracleLanguages.Paper]id_step_soundness [in OracleLanguages.Paper]
ImpBigStep.big_div_implies_small_div [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_cont_div_implies_small_div [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_div_implies_small_div_helper' [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_implies_small_helper [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_div_implies_small_div_helper [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_determinist [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_implies_small [in OracleLanguages.Imp.BigStep]
ImpBigStep.seq_assoc [in OracleLanguages.Imp.BigStep]
ImpBigStep.small_equiv_big [in OracleLanguages.Imp.BigStep]
ImpBigStep.small_implies_big [in OracleLanguages.Imp.BigStep]
ImpBigStep.small_implies_big_helper [in OracleLanguages.Imp.BigStep]
ImpHoare.assertion_implies_trans [in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_implies_refl [in OracleLanguages.Imp.Hoare]
ImpHoare.hoare_soundness [in OracleLanguages.Imp.Hoare]
ImpOracleHelpers.generic_step_bicrash [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.generic_step_bistep [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_special_cont_step_inv [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_special_cmd_step_inv [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage.finite_small_step_exec_nsteps [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.genv_eq_dec [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.nsteps_compose [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.nsteps_imp_app_1 [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.state_final_no_step [in OracleLanguages.Imp.Lang]
Imp.beq_cmd_false_iff [in OracleLanguages.Imp.Syntax]
Imp.beq_cmd_true_iff [in OracleLanguages.Imp.Syntax]
Imp.beq_cmd_reflx [in OracleLanguages.Imp.Syntax]
Imp.beq_exp_reflx [in OracleLanguages.Imp.Syntax]
Imp.bexp_eq_dec [in OracleLanguages.Imp.Syntax]
Imp.cmd_eq_dec [in OracleLanguages.Imp.Syntax]
Imp.exp_eq_dec [in OracleLanguages.Imp.Syntax]
Imp.In_var_dec [in OracleLanguages.Imp.Syntax]
Imp.In_bexp_div_dec [in OracleLanguages.Imp.Syntax]
Imp.In_bexp_var_dec [in OracleLanguages.Imp.Syntax]
Imp.In_exp_div_dec [in OracleLanguages.Imp.Syntax]
Imp.In_exp_var_dec [in OracleLanguages.Imp.Syntax]
Imp.state_final_eq [in OracleLanguages.Imp.SmallStep]
Imp.state_eq_trans [in OracleLanguages.Imp.SmallStep]
Imp.state_eq_refl [in OracleLanguages.Imp.SmallStep]
Imp.state_eq_sym [in OracleLanguages.Imp.SmallStep]
Imp.state_eq_dec [in OracleLanguages.Imp.SmallStep]
Imp.step_eq' [in OracleLanguages.Imp.SmallStep]
Imp.step_eq [in OracleLanguages.Imp.SmallStep]
Imp.step_app [in OracleLanguages.Imp.SmallStep]
Imp.store_equal_eval_bexp [in OracleLanguages.Imp.Syntax]
Imp.store_equal_eval_exp [in OracleLanguages.Imp.Syntax]
Imp.store_Equal_dec [in OracleLanguages.Imp.Syntax]
Imp.store_equal_true_iff [in OracleLanguages.Imp.Syntax]
M
Make.apply_cmd_mod_id [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]Make.apply_cmd_mod_id [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.apply_cmd_mod_id [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.apply_cmd_mod_id [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.close_skip_skip [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.close_skip_skip [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.cont_classified_2 [in OracleLanguages.Imp.DisjointStates]
Make.cont_classified_1 [in OracleLanguages.Imp.DisjointStates]
Make.core_rhl_sc_soundness [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.core_rhl_soundness [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.disjoint_union_eval_bexp_same [in OracleLanguages.Imp.DisjointStates]
Make.disjoint_union_eval_exp_same [in OracleLanguages.Imp.DisjointStates]
Make.disjoint_eval_bexp [in OracleLanguages.Imp.DisjointStates]
Make.disjoint_eval_exp [in OracleLanguages.Imp.DisjointStates]
Make.disjoint_states_sym [in OracleLanguages.Imp.DisjointStates]
Make.equal_store_is_union [in OracleLanguages.Imp.DisjointStates]
Make.eval_exp_add_neq' [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.eval_exp_add_neq [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.hoare_close_skip_skip [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.hoare_close_skip [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.map_swap_add_neq [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.minimal_rhl_soundness [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.no_crash [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.no_crash [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.no_crash [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_terms_consistent_1 [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_consistent_1 [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_consistent_1 [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.rename_store_comm_add [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_Equal [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_eval_bexp [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_eval_exp [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_store_preserves_values [in OracleLanguages.Imp.Oracles.Renaming]
Make.same_control_store_add_stable' [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_add_stable [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_exp_crash [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_eval_bexp [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_store_eval_exp [in OracleLanguages.Imp.Oracles.ValueChange]
Make.state_final_nocrash [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.state_final_nocrash [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.state_final_nocrash [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.step_disjoint_union_states [in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states_union_same_crashes [in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states_union [in OracleLanguages.Imp.DisjointStates]
Make.step_2_disjoint_states [in OracleLanguages.Imp.DisjointStates]
Make.step_disjoint_states [in OracleLanguages.Imp.DisjointStates]
Make.store_is_union_add [in OracleLanguages.Imp.DisjointStates]
Make.store_is_union_sym [in OracleLanguages.Imp.DisjointStates]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_invariant [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_invariant [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_no_crash [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right_soundness [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_no_crash [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left_soundness [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._split_hoare_seq_1 [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.ValueChange]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.ValueChange]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.ValueChange]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.CrashFix]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.CrashFix]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.CrashFix]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._prediction_completeness [in OracleLanguages.Imp.Oracles.Renaming]
Make._prediction_soundness [in OracleLanguages.Imp.Oracles.Renaming]
Make._invariant_1 [in OracleLanguages.Imp.Oracles.Renaming]
N
napply_napply'_0_iff [in OracleLanguages.Common]napply_napply'_Sn_iff [in OracleLanguages.Common]
napply'_lt_id [in OracleLanguages.Common]
napply'_prefix [in OracleLanguages.Common]
napply'_1 [in OracleLanguages.Common]
nsteps_split_helper [in OracleLanguages.ProgrammingLanguage]
nsteps_plus_2 [in OracleLanguages.ProgrammingLanguage]
nsteps_plus_1' [in OracleLanguages.ProgrammingLanguage]
nsteps_plus_1 [in OracleLanguages.ProgrammingLanguage]
nsteps_plus_0 [in OracleLanguages.ProgrammingLanguage]
nsteps_eq [in OracleLanguages.ProgrammingLanguage]
nsteps_skipn [in OracleLanguages.ReductionTrace]
nsteps_helper_1 [in OracleLanguages.Paper]
O
opt_state_eq_trans [in OracleLanguages.ProgrammingLanguage]opt_state_eq_sym [in OracleLanguages.ProgrammingLanguage]
opt_state_eq_refl [in OracleLanguages.ProgrammingLanguage]
opt_state_eq_Some_r__state_eq [in OracleLanguages.ProgrammingLanguage]
opt_state_eq_dec [in OracleLanguages.ProgrammingLanguage]
oracle_nsteps_termination'' [in OracleLanguages.OracleLanguage]
oracle_nsteps_termination [in OracleLanguages.OracleLanguage]
oracle_nsteps_right [in OracleLanguages.OracleLanguage]
oracle_nsteps_left [in OracleLanguages.OracleLanguage]
oracle_eq_trans [in OracleLanguages.OracleLanguage]
oracle_eq_sym [in OracleLanguages.OracleLanguage]
oracle_eq_refl [in OracleLanguages.OracleLanguage]
oracle_gamma_correlated [in OracleLanguages.OracleLanguage]
oracle_relates_configurations_of_programs [in OracleLanguages.OracleLanguage]
P
P₀_crashes [in OracleLanguages.Paper]P₀_loop_crashes [in OracleLanguages.Paper]
P₁_loop_body_crashes [in OracleLanguages.Paper]
P₂_does_not_crash [in OracleLanguages.Paper]
P₂_loop_does_not_crash [in OracleLanguages.Paper]
S
state_eq__opt_state_eq [in OracleLanguages.ProgrammingLanguage]swap_ite_or_1 [in OracleLanguages.Paper]
swap_assign_or_1 [in OracleLanguages.Paper]
T
traceFrom_trace [in OracleLanguages.ReductionTrace]trace_trace' [in OracleLanguages.ReductionTrace]
trace_first [in OracleLanguages.ReductionTrace]
V
valuechange_or_1 [in OracleLanguages.Paper]varid_eq_dec [in OracleLanguages.Paper]
_
_prediction_completeness [in OracleLanguages.Oracles.UniversalOracle]_prediction_soundness [in OracleLanguages.Oracles.UniversalOracle]
_prediction_completeness [in OracleLanguages.Oracles.Identity]
_prediction_soundness [in OracleLanguages.Oracles.Identity]
other
δ_sound [in OracleLanguages.Paper]Axiom Index
L
L [in OracleLanguages.Oracles.Identity]L₁ [in OracleLanguages.Oracles.UniversalOracle]
L₂ [in OracleLanguages.Oracles.UniversalOracle]
Inductive Index
C
coplist [in OracleLanguages.Common]coplist_in [in OracleLanguages.Common]
G
gamma_correlated [in OracleLanguages.ReductionTracesRelation]I
ImpBigStep.big_step_cont_div [in OracleLanguages.Imp.BigStep]ImpBigStep.big_step_cont [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step_div [in OracleLanguages.Imp.BigStep]
ImpBigStep.big_step [in OracleLanguages.Imp.BigStep]
ImpHoare.hoare_proof [in OracleLanguages.Imp.Hoare]
ImpOracleHelpers.cmd_mod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.cont_mod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_res [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage.finite_small_step_exec [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.infinite_small_step_exec [in OracleLanguages.Imp.Lang]
Imp.bexp [in OracleLanguages.Imp.Syntax]
Imp.cmd [in OracleLanguages.Imp.Syntax]
Imp.exp [in OracleLanguages.Imp.Syntax]
Imp.finite_small_step_exec [in OracleLanguages.Imp.SmallStep]
Imp.infinite_small_step_exec [in OracleLanguages.Imp.SmallStep]
included_subtrace [in OracleLanguages.ReductionTrace]
M
Make.core_rhl_sc_proof [in OracleLanguages.Imp.RHL]Make.core_rhl_proof [in OracleLanguages.Imp.RHL]
Make.either [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.imp_ctx [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.km_invariant [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.km_invariant [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.km_invariant [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.km_invariant [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.km_invariant [in OracleLanguages.Imp.Oracles.CrashFix]
Make.km_invariant [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.km_invariant [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.minimal_rhl_proof [in OracleLanguages.Imp.RHL]
Make.mod [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.mod [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.mod [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.mod [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.mod_invariant [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.mod_invariant [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.mod_invariant [in OracleLanguages.Imp.Oracles.CrashFix]
Make.primitive_difference [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.proof_terms_match [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_term [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_match [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_term [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_match [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.proof_term [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.same_control_cmd [in OracleLanguages.Imp.Oracles.ValueChange]
Make.t [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make._state [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._state [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._state [in OracleLanguages.Imp.Oracles.ValueChange]
Make._state [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._cont_mod [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._state [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._cont_mod [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._state [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._cont_mod [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._state [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._cont_mod [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._state [in OracleLanguages.Imp.Oracles.CrashFix]
Make._cont_mod [in OracleLanguages.Imp.Oracles.CrashFix]
Make._state [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._cont_mod [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._state [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._cont_mod [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._state [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._state [in OracleLanguages.Imp.Oracles.Renaming]
N
nsteps_crashing_trace [in OracleLanguages.ReductionTrace]nsteps_converging_trace [in OracleLanguages.ReductionTrace]
O
oracle_eq [in OracleLanguages.OracleLanguage]T
trace [in OracleLanguages.ReductionTrace]V
varid [in OracleLanguages.Paper]Projection Index
D
difference [in OracleLanguages.DifferenceLanguage]G
genv_eq_dec [in OracleLanguages.ProgrammingLanguage]genv_eq_trans [in OracleLanguages.ProgrammingLanguage]
genv_eq_sym [in OracleLanguages.ProgrammingLanguage]
genv_eq_refl [in OracleLanguages.ProgrammingLanguage]
genv_eq [in OracleLanguages.ProgrammingLanguage]
genv_type [in OracleLanguages.ProgrammingLanguage]
I
initial_state [in OracleLanguages.ProgrammingLanguage]interpret [in OracleLanguages.DifferenceLanguage]
invariant [in OracleLanguages.OracleLanguage]
invariant_1 [in OracleLanguages.OracleLanguage]
L
left_genv [in OracleLanguages.OracleLanguage]left_state [in OracleLanguages.OracleLanguage]
M
Make.body [in OracleLanguages.Imp.Oracles.CrashFixWhile]Make.bound [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.condition [in OracleLanguages.Imp.Oracles.CrashFix]
Make.crash_avoided_1 [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crash_bound [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crash_avoided_1 [in OracleLanguages.Imp.Oracles.CrashFix]
Make.crash_bound [in OracleLanguages.Imp.Oracles.CrashFix]
Make.c_right [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.c_left [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.c_else [in OracleLanguages.Imp.Oracles.CrashFix]
Make.c_then [in OracleLanguages.Imp.Oracles.CrashFix]
Make.expression [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.genv [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.left_fun_spec_2 [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_fun_spec_1 [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_equiv_right [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.left_fun [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.OT [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.right_fun_spec_2 [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.right_fun_spec_1 [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.right_fun [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make.state [in OracleLanguages.Imp.ImpDifferenceLanguage]
O
oracle_step [in OracleLanguages.OracleLanguage]oracle_genv [in OracleLanguages.OracleLanguage]
oracle_state [in OracleLanguages.OracleLanguage]
P
prediction_completeness [in OracleLanguages.OracleLanguage]prediction_soundness [in OracleLanguages.OracleLanguage]
prog [in OracleLanguages.ProgrammingLanguage]
R
return_type [in OracleLanguages.ProgrammingLanguage]right_genv [in OracleLanguages.OracleLanguage]
right_state [in OracleLanguages.OracleLanguage]
S
state [in OracleLanguages.ProgrammingLanguage]state_final_eq [in OracleLanguages.ProgrammingLanguage]
state_eq_dec [in OracleLanguages.ProgrammingLanguage]
state_eq_trans [in OracleLanguages.ProgrammingLanguage]
state_eq_sym [in OracleLanguages.ProgrammingLanguage]
state_eq_refl [in OracleLanguages.ProgrammingLanguage]
state_eq [in OracleLanguages.ProgrammingLanguage]
state_final_no_step [in OracleLanguages.ProgrammingLanguage]
state_final [in OracleLanguages.ProgrammingLanguage]
step [in OracleLanguages.ProgrammingLanguage]
step_eq' [in OracleLanguages.ProgrammingLanguage]
step_eq [in OracleLanguages.ProgrammingLanguage]
Definition Index
A
abstractequiv_example' [in OracleLanguages.Paper]abstractequiv_example [in OracleLanguages.Paper]
abstract_equiv_or [in OracleLanguages.Paper]
B
bind [in OracleLanguages.Common]C
compose_trace_relations_externally [in OracleLanguages.ReductionTracesRelation]configuration [in OracleLanguages.ProgrammingLanguage]
configuration_eq [in OracleLanguages.ProgrammingLanguage]
coplist_id_force [in OracleLanguages.Common]
correlation_trace_from [in OracleLanguages.OracleLanguage]
correlation_relation [in OracleLanguages.OracleLanguage]
crashfixwhile_or [in OracleLanguages.Paper]
crashfix_or [in OracleLanguages.Paper]
crashfix_example' [in OracleLanguages.Paper]
crashfix_example [in OracleLanguages.Paper]
crash_proof [in OracleLanguages.Paper]
crash_fix [in OracleLanguages.Paper]
E
ex₁ [in OracleLanguages.Paper]ex₁_γ_correlation_1 [in OracleLanguages.Paper]
ex₁_γ_correlation [in OracleLanguages.Paper]
ex₁_as_id_oracle_step [in OracleLanguages.Paper]
ex₁_as_id_oracle_projections [in OracleLanguages.Paper]
ex₁_as_id_oracle [in OracleLanguages.Paper]
ex₁_trace_converges [in OracleLanguages.Paper]
ex₁_trace_actually_trace [in OracleLanguages.Paper]
ex₁_trace [in OracleLanguages.Paper]
ex₁_final_state_is_final [in OracleLanguages.Paper]
ex₁_final_state [in OracleLanguages.Paper]
ex₁_initial_state [in OracleLanguages.Paper]
ex₁_genv [in OracleLanguages.Paper]
ex₁_initial_configuration [in OracleLanguages.Paper]
ex₂ [in OracleLanguages.Paper]
ex₂_refl [in OracleLanguages.Paper]
F
first [in OracleLanguages.Common]I
identity_oracle [in OracleLanguages.Oracles.Identity]identity_oracle [in OracleLanguages.Paper]
id_step [in OracleLanguages.Paper]
ImpHoare.assertion [in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_implies [in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_of_bexp [in OracleLanguages.Imp.Hoare]
ImpHoare.assertion_subst [in OracleLanguages.Imp.Hoare]
ImpOracleHelpers.left_mod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.local_identity [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.right_mod [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpOracleHelpers.step_helper_id [in OracleLanguages.Imp.Oracles.OracleHelpers]
ImpProgrammingLanguage.imp_language [in OracleLanguages.Imp.Lang]
ImpProgrammingLanguage.υ [in OracleLanguages.Imp.Lang]
Imp.beq_state [in OracleLanguages.Imp.SmallStep]
Imp.beq_cmd [in OracleLanguages.Imp.Syntax]
Imp.beq_bexp [in OracleLanguages.Imp.Syntax]
Imp.beq_exp [in OracleLanguages.Imp.Syntax]
Imp.cont [in OracleLanguages.Imp.SmallStep]
Imp.eval_bexp [in OracleLanguages.Imp.Syntax]
Imp.eval_exp [in OracleLanguages.Imp.Syntax]
Imp.In_var [in OracleLanguages.Imp.Syntax]
Imp.In_bexp_div [in OracleLanguages.Imp.Syntax]
Imp.In_bexp_var [in OracleLanguages.Imp.Syntax]
Imp.In_exp_div [in OracleLanguages.Imp.Syntax]
Imp.In_exp_var [in OracleLanguages.Imp.Syntax]
Imp.state [in OracleLanguages.Imp.SmallStep]
Imp.state_final [in OracleLanguages.Imp.SmallStep]
Imp.state_eq [in OracleLanguages.Imp.SmallStep]
Imp.step [in OracleLanguages.Imp.SmallStep]
Imp.store [in OracleLanguages.Imp.Syntax]
Imp.store_equal [in OracleLanguages.Imp.Syntax]
Imp.varid [in OracleLanguages.Imp.Syntax]
initial_configuration [in OracleLanguages.ProgrammingLanguage]
L
left_trace [in OracleLanguages.OracleLanguage]M
Make.abstract_equiv_oracle [in OracleLanguages.Imp.Oracles.AbstractEquiv]Make.apply_cmd_mod [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.apply_cmd_mod [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.apply_cmd_mod [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.apply_cmd_mod [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.assign_indep [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.assign_indep' [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.bijection [in OracleLanguages.Imp.Oracles.Renaming]
Make.bijective [in OracleLanguages.Imp.Oracles.Renaming]
Make.cmd_mod_from_imp_ctx [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.cont_classified [in OracleLanguages.Imp.DisjointStates]
Make.core_rhl_oracle [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.core_rhl_oracle [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.crashfixwhile_oracle [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.crashfix_oracle [in OracleLanguages.Imp.Oracles.CrashFix]
Make.disjoint_states [in OracleLanguages.Imp.DisjointStates]
Make.fold_seq [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.imp [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.imp_difference_language [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.interpret_difference [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.interpret_primitive_difference [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.In_var_cont [in OracleLanguages.Imp.DisjointStates]
Make.leaf_mod_of_cmds [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.leaf_mod_of_cmds [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.minimal_rhl_oracle [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.oracle_from_primitive_diff [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.oracle_step [in OracleLanguages.Imp.ImpDifferenceLanguage]
Make.perform_n_steps [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.perform_n_steps [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.perform_n_m_steps [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.proof_terms_consistent [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make.proof_terms_consistent [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make.proof_terms_consistent [in OracleLanguages.Imp.Oracles.CoreRHL]
Make.refactor_common_branch_trailer_oracle [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.refactor_common_trailer [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make.rename_store [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_store_helper [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_cont [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_cmd [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_bexp [in OracleLanguages.Imp.Oracles.Renaming]
Make.rename_exp [in OracleLanguages.Imp.Oracles.Renaming]
Make.renaming_oracle [in OracleLanguages.Imp.Oracles.Renaming]
Make.same_control_store [in OracleLanguages.Imp.Oracles.ValueChange]
Make.same_control_cont [in OracleLanguages.Imp.Oracles.ValueChange]
Make.seqassoc_oracle [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.store_classified [in OracleLanguages.Imp.DisjointStates]
Make.store_is_union [in OracleLanguages.Imp.DisjointStates]
Make.swapassign_oracle [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.swapbranches_oracle [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.swap_assignments [in OracleLanguages.Imp.Oracles.SwapAssign]
Make.syntactic_un_negate [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.syntactic_negate [in OracleLanguages.Imp.Oracles.SwapBranches]
Make.unfold_seq [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make.valuechange_oracle [in OracleLanguages.Imp.Oracles.ValueChange]
Make._right_state [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._left_state [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._step [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._step_helper [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._invariant [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._genv [in OracleLanguages.Imp.Oracles.MinimalRHL]
Make._right_state [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._left_state [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_right [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_left [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_right [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._step_helper_single_left [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._split_hoare_seq [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._invariant [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._genv [in OracleLanguages.Imp.Oracles.CoreRHLSC]
Make._invariant [in OracleLanguages.Imp.Oracles.ValueChange]
Make._right_state [in OracleLanguages.Imp.Oracles.ValueChange]
Make._left_state [in OracleLanguages.Imp.Oracles.ValueChange]
Make._step [in OracleLanguages.Imp.Oracles.ValueChange]
Make._genv [in OracleLanguages.Imp.Oracles.ValueChange]
Make._invariant [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._right_state [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._left_state [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._step [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._genv [in OracleLanguages.Imp.Oracles.RefactorCommonBranchRemainder]
Make._invariant [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._right_state [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._left_state [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._step [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._genv [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make._invariant [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._right_state [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._left_state [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._step [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._genv [in OracleLanguages.Imp.Oracles.AbstractEquiv]
Make._invariant [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._right_state [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._left_state [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._step [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._genv [in OracleLanguages.Imp.Oracles.SwapAssign]
Make._invariant [in OracleLanguages.Imp.Oracles.CrashFix]
Make._right_state [in OracleLanguages.Imp.Oracles.CrashFix]
Make._left_state [in OracleLanguages.Imp.Oracles.CrashFix]
Make._step [in OracleLanguages.Imp.Oracles.CrashFix]
Make._genv [in OracleLanguages.Imp.Oracles.CrashFix]
Make._invariant [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._right_state [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._left_state [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._step [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._genv [in OracleLanguages.Imp.Oracles.SeqAssoc]
Make._invariant [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._right_state [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._left_state [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._step [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._genv [in OracleLanguages.Imp.Oracles.SwapBranches]
Make._right_state [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._left_state [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper_right [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper_left [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._step_helper [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._invariant [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._genv [in OracleLanguages.Imp.Oracles.CoreRHL]
Make._invariant [in OracleLanguages.Imp.Oracles.Renaming]
Make._right_state [in OracleLanguages.Imp.Oracles.Renaming]
Make._left_state [in OracleLanguages.Imp.Oracles.Renaming]
Make._step [in OracleLanguages.Imp.Oracles.Renaming]
Make._genv [in OracleLanguages.Imp.Oracles.Renaming]
map [in OracleLanguages.Common]
N
napply [in OracleLanguages.Common]napply' [in OracleLanguages.Common]
next [in OracleLanguages.Common]
nsteps [in OracleLanguages.ProgrammingLanguage]
nsteps_helper [in OracleLanguages.Paper]
nsteps' [in OracleLanguages.ProgrammingLanguage]
O
opt_state_eq [in OracleLanguages.ProgrammingLanguage]oracle_nsteps' [in OracleLanguages.OracleLanguage]
oracle_nsteps [in OracleLanguages.OracleLanguage]
oracle_correlation_relation [in OracleLanguages.OracleLanguage]
P
program_trace [in OracleLanguages.ReductionTrace]P₀ [in OracleLanguages.Paper]
P₁ [in OracleLanguages.Paper]
P₁_loop_body [in OracleLanguages.Paper]
P₁_loop_ctx [in OracleLanguages.Paper]
P₂ [in OracleLanguages.Paper]
R
renaming [in OracleLanguages.Paper]renaming_ex₁_1 [in OracleLanguages.Paper]
renaming_ex₁ [in OracleLanguages.Paper]
ret [in OracleLanguages.Common]
right_trace [in OracleLanguages.OracleLanguage]
S
skipn [in OracleLanguages.Common]sound_program_difference [in OracleLanguages.DifferenceLanguage]
swap_ite_or [in OracleLanguages.Paper]
swap_ite_example' [in OracleLanguages.Paper]
swap_ite_example [in OracleLanguages.Paper]
swap_assign_or [in OracleLanguages.Paper]
swap_example' [in OracleLanguages.Paper]
swap_example [in OracleLanguages.Paper]
T
take [in OracleLanguages.Common]terminates [in OracleLanguages.ProgrammingLanguage]
traceFrom [in OracleLanguages.ReductionTrace]
trace_relation [in OracleLanguages.ReductionTracesRelation]
trace' [in OracleLanguages.ReductionTrace]
U
universal_oracle [in OracleLanguages.Oracles.UniversalOracle]V
valuechange_or [in OracleLanguages.Paper]valuechange_example' [in OracleLanguages.Paper]
valuechange_example [in OracleLanguages.Paper]
Var.eq_dec [in OracleLanguages.Paper]
Var.t [in OracleLanguages.Paper]
_
_step [in OracleLanguages.Oracles.UniversalOracle]_genv [in OracleLanguages.Oracles.UniversalOracle]
_state [in OracleLanguages.Oracles.UniversalOracle]
_state [in OracleLanguages.Oracles.Identity]
other
γ_from_oracle [in OracleLanguages.OracleLanguage]δ [in OracleLanguages.Paper]
φ [in OracleLanguages.Paper]
φ' [in OracleLanguages.Paper]
Record Index
D
difference_language [in OracleLanguages.DifferenceLanguage]L
language [in OracleLanguages.ProgrammingLanguage]M
Make.mod [in OracleLanguages.Imp.Oracles.AbstractEquiv]Make.mod [in OracleLanguages.Imp.Oracles.CrashFix]
Make.modif [in OracleLanguages.Imp.Oracles.CrashFixWhile]
Make.oracle [in OracleLanguages.Imp.ImpDifferenceLanguage]
O
oracle_language [in OracleLanguages.OracleLanguage]| 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 | (911 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 | (20 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 | (56 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 | (30 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 | (238 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 | (189 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 | (3 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 | (71 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 | (56 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 | (241 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 | (7 entries) |
This page has been generated by coqdoc