| 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 | (1421 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 | (91 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 | (3 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 | (40 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 | (470 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 | (290 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 | (20 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 | (61 entries) |
| Instance 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 | (132 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (39 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 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 | (237 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 | (16 entries) |
Global Index
A
add_modal_fupd_wbwp [instance, in WBLogic.program_logic.weakestpre]adequacy [library]
adequacy [library]
adequacy [library]
Alloc [abbreviation, in WBLogic.heap_lang_trace.notation]
alloc_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
alloc_hist [lemma, in WBLogic.heap_lang_trace.trace_resources]
App_typed [constructor, in WBLogic.F_mu_ref.typing]
AsRecV [record, in WBLogic.heap_lang_trace.class_instances]
AsRecV [inductive, in WBLogic.heap_lang_trace.class_instances]
AsRecV_recv [definition, in WBLogic.heap_lang_trace.class_instances]
as_recv [projection, in WBLogic.heap_lang_trace.class_instances]
as_recv [constructor, in WBLogic.heap_lang_trace.class_instances]
as_val_val [instance, in WBLogic.heap_lang_trace.class_instances]
atomic [section, in WBLogic.heap_lang_trace.class_instances]
Autosubst_Lemmas [section, in WBLogic.F_mu_ref.base]
awkN [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
awkward [section, in WBLogic.heap_lang_examples.awkward]
awkward [definition, in WBLogic.heap_lang_examples.awkward]
awkward [library]
awkward_self_apply_returns_one [lemma, in WBLogic.heap_lang_examples.awkward]
awkward_self_apply [definition, in WBLogic.heap_lang_examples.awkward]
B
base [library]basic_soundness [lemma, in WBLogic.F_mu_ref.binary.soundness]
beta_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
binary_fundamental [lemma, in WBLogic.F_mu_ref.binary.fundamental]
binary_soundness [lemma, in WBLogic.F_mu_ref.binary.soundness]
BinOp_typed [constructor, in WBLogic.F_mu_ref.typing]
binop_res_type [definition, in WBLogic.F_mu_ref.typing]
binop_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
bin_log_related_under_typed_ctx [lemma, in WBLogic.F_mu_ref.binary.context_refinement]
bin_log_related_under_typed_ctx [section, in WBLogic.F_mu_ref.binary.context_refinement]
bin_log_related_store [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_load [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_alloc [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unfold [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_fold [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unpack [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_pack [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_tapp [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_tlam [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_app [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_seq [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_letin [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_lam [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_rec [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_nat_binop [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_if [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_case [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_injr [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_injl [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_snd [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_fst [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_pair [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_bool [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_nat [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unit [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_var [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_alt [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_val_rel_bin_expr_rel [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_expr_rel_bind [lemma, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related [definition, in WBLogic.F_mu_ref.binary.fundamental]
bin_log_def [section, in WBLogic.F_mu_ref.binary.fundamental]
Bool_typed [constructor, in WBLogic.F_mu_ref.typing]
C
call_fact_across [definition, in WBLogic.heap_lang_trace_examples.very_awkward]call_twice_return_one_very_awkward_refinement [lemma, in WBLogic.F_mu_ref.binary.examples.very_awkward]
call_twice_return_one_typed [lemma, in WBLogic.F_mu_ref.binary.examples.very_awkward]
call_twice_return_one [definition, in WBLogic.F_mu_ref.binary.examples.very_awkward]
call_fact_across [definition, in WBLogic.heap_lang_examples.very_awkward]
CAS [abbreviation, in WBLogic.heap_lang_trace.notation]
Case_typed [constructor, in WBLogic.F_mu_ref.typing]
cfg [section, in WBLogic.F_mu_ref.binary.rules]
cfgSG [record, in WBLogic.F_mu_ref.binary.rules]
cfgUR [definition, in WBLogic.F_mu_ref.binary.rules]
cfg_name [projection, in WBLogic.F_mu_ref.binary.rules]
cfg_inG [projection, in WBLogic.F_mu_ref.binary.rules]
class_instances [library]
closed_context_weakening [lemma, in WBLogic.F_mu_ref.typing]
cmpxchg_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
context_weakening [lemma, in WBLogic.F_mu_ref.typing]
context_gen_weakening [lemma, in WBLogic.F_mu_ref.typing]
context_refinement [library]
conversions [section, in WBLogic.F_mu_ref.binary.rules]
ctx [definition, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_lookup [definition, in WBLogic.F_mu_ref.binary.logrel]
ctx_refines [definition, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_sind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_rec [definition, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_ind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_rect [definition, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_StoreR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_StoreL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Load [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Alloc [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_TApp [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_TLam [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Unfold [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Fold [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfM [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_BinOpR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_BinOpL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseM [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_InjR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_InjL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Snd [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Fst [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_PairR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_PairL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_AppR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_AppL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Rec [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item [inductive, in WBLogic.F_mu_ref.binary.context_refinement]
D
D [abbreviation, in WBLogic.F_mu_ref.binary.logrel]D [abbreviation, in WBLogic.F_mu_ref.unary.fundamental]
D [abbreviation, in WBLogic.F_mu_ref.unary.logrel]
D [abbreviation, in WBLogic.F_mu_ref.binary.fundamental]
D [abbreviation, in WBLogic.F_mu_ref.binary.fundamental]
definitions [section, in WBLogic.heap_lang_trace.primitive_laws]
definitionsS [section, in WBLogic.F_mu_ref.binary.rules]
derived_laws [library]
derived_laws [library]
do_step_pure [lemma, in WBLogic.F_mu_ref.binary.rules]
E
elim_acc_wbwp_nonatomic [instance, in WBLogic.program_logic.weakestpre]elim_acc_wbwp_atomic [instance, in WBLogic.program_logic.weakestpre]
elim_modal_fupd_wbwp_atomic [instance, in WBLogic.program_logic.weakestpre]
elim_modal_fupd_wbwp [instance, in WBLogic.program_logic.weakestpre]
elim_modal_bupd_wbwp [instance, in WBLogic.program_logic.weakestpre]
emit_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
empty_state [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
env_subst_lookup [lemma, in WBLogic.F_mu_ref.typing]
env_subst [definition, in WBLogic.F_mu_ref.typing]
env_lookup [definition, in WBLogic.F_mu_ref.unary.logrel]
eventO [definition, in WBLogic.heap_lang_trace.trace_resources]
F
faa_atomic [instance, in WBLogic.heap_lang_trace.class_instances]fact [definition, in WBLogic.F_mu_ref.binary.examples.fact]
fact [library]
factorial [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
factorial [definition, in WBLogic.heap_lang_examples.very_awkward]
factV [definition, in WBLogic.F_mu_ref.binary.examples.fact]
fact_ctx_equiv [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_fact_refinement [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_fact_acc_refinement [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_equiv [section, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_typed [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_subst [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_unfold [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_accV [definition, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc [definition, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_unfold [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_subst [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_typed [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body [definition, in WBLogic.F_mu_ref.binary.examples.fact]
fact_unfold [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fact_typed [lemma, in WBLogic.F_mu_ref.binary.examples.fact]
fill_ctx [definition, in WBLogic.F_mu_ref.binary.context_refinement]
fill_ctx_item [definition, in WBLogic.F_mu_ref.binary.context_refinement]
fixpoint_interp_rec1_eq [lemma, in WBLogic.F_mu_ref.binary.logrel]
fixpoint_interp_rec1_eq [lemma, in WBLogic.F_mu_ref.unary.logrel]
fork_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
frame_wbwp [instance, in WBLogic.program_logic.weakestpre]
free_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
fresh_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
Fst_typed [constructor, in WBLogic.F_mu_ref.typing]
fst_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
fundamental [lemma, in WBLogic.F_mu_ref.unary.fundamental]
fundamental [section, in WBLogic.F_mu_ref.binary.fundamental]
fundamental [library]
fundamental [library]
fupd_wbwp [lemma, in WBLogic.program_logic.weakestpre]
F_mu_ref_lang [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref_ectx_lang [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref_ectxi_lang [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.exprO [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.valO [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.stateO [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.lang_mixin [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_head_stuck [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.alloc_fresh [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item_no_val_inj [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.head_ctx_step_val [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_stuck [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item_inj [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item_val [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.of_val_inj [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.of_to_val [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.to_of_val [lemma, in WBLogic.F_mu_ref.lang]
F_mu_ref.head_step_sind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.head_step_ind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.StoreS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LoadS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.AllocS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.TBeta [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Unfold_Fold [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.IfTrue [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.IfFalse [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseRS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseLS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.SndS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.FstS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.SeqBetaS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LetInBetaS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LamBetaS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BetaS [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.head_step [inductive, in WBLogic.F_mu_ref.lang]
F_mu_ref.state [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_sind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_rec [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_ind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_rect [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.StoreRCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.StoreLCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LoadCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.AllocCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.UnfoldCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.FoldCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.IfCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjRCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjLCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.SndCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.FstCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpRCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpLCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.PairRCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.PairLCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackInCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.PackCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.TAppCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.SeqCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LetInCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.AppRCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.AppLCtx [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item [inductive, in WBLogic.F_mu_ref.lang]
F_mu_ref.to_val [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.of_val [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_inh [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_dec_eq [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_eval [definition, in WBLogic.F_mu_ref.lang]
#nv _ [notation, in WBLogic.F_mu_ref.lang]
#♭v _ [notation, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_sind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_rec [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_ind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.val_rect [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.LocV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.FoldV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjRV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjLV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.PairV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BoolV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.NatV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.UnitV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.PackV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.TLamV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LamV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.RecV [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.val [inductive, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_dec_eq [instance, in WBLogic.F_mu_ref.lang]
#n _ [notation, in WBLogic.F_mu_ref.lang]
#♭ _ [notation, in WBLogic.F_mu_ref.lang]
F_mu_ref.SubstLemmas_expr [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.Subst_expr [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.Rename_expr [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.Ids_expr [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_sind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_rec [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_ind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_rect [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.Store [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Load [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Alloc [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Loc [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackIn [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Pack [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.TApp [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.TLam [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Unfold [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Fold [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Case [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjR [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.InjL [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Snd [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Fst [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Pair [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.If [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOp [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Bool [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Nat [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Unit [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Seq [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.LetIn [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Lam [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.App [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Rec [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Var [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.expr [inductive, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_dec_eq [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_sind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_rec [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_ind [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_rect [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref.Lt [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Le [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Eq [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Mult [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Sub [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.Add [constructor, in WBLogic.F_mu_ref.lang]
F_mu_ref.binop [inductive, in WBLogic.F_mu_ref.lang]
F_mu_ref.loc_dec_eq [instance, in WBLogic.F_mu_ref.lang]
F_mu_ref.loc [definition, in WBLogic.F_mu_ref.lang]
F_mu_ref [module, in WBLogic.F_mu_ref.lang]
G
ghost_stacks [section, in WBLogic.program_logic.ghost_stacks]ghost_id [definition, in WBLogic.program_logic.ghost_stacks]
ghost_stacks [library]
gmap_of_trace_valid [lemma, in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace_hist_valid_prefix [lemma, in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace_dom [lemma, in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace_snoc [lemma, in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace [definition, in WBLogic.heap_lang_trace.trace_resources]
gpop [definition, in WBLogic.program_logic.ghost_stacks]
gpop_gpush [lemma, in WBLogic.program_logic.ghost_stacks]
gpush [definition, in WBLogic.program_logic.ghost_stacks]
gsingleton [definition, in WBLogic.program_logic.ghost_stacks]
gstack [definition, in WBLogic.program_logic.ghost_stacks]
gstackO [definition, in WBLogic.program_logic.ghost_stacks]
gstacks [definition, in WBLogic.program_logic.ghost_stacks]
gstacksGpre [record, in WBLogic.program_logic.ghost_stacks]
gstacksGpre_ing [projection, in WBLogic.program_logic.ghost_stacks]
gstacksGpre_dom_ing [projection, in WBLogic.program_logic.ghost_stacks]
gstacksIG [record, in WBLogic.program_logic.ghost_stacks]
gstacks_init [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_except_included [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_out_swap [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_put_back [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_take_out [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_agree [lemma, in WBLogic.program_logic.ghost_stacks]
gstacks_except_Timeless [instance, in WBLogic.program_logic.ghost_stacks]
gstacks_except [definition, in WBLogic.program_logic.ghost_stacks]
gstacks_subΣ_inG [instance, in WBLogic.program_logic.ghost_stacks]
gstacks_name [projection, in WBLogic.program_logic.ghost_stacks]
gstacks_ing [projection, in WBLogic.program_logic.ghost_stacks]
gstacks_dom_ing [projection, in WBLogic.program_logic.ghost_stacks]
gstacksΣ [definition, in WBLogic.program_logic.ghost_stacks]
gstackUR [definition, in WBLogic.program_logic.ghost_stacks]
gstack_alloc [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_full_is_out [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_full_in [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_frag_not_out_agree [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_frag_in [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_exists_in [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_full_exists [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_frag_exists [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_pop [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_push [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_full_unique [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_frag_unique [lemma, in WBLogic.program_logic.ghost_stacks]
gstack_exists_Persistent [instance, in WBLogic.program_logic.ghost_stacks]
gstack_exists_Timeless [instance, in WBLogic.program_logic.ghost_stacks]
gstack_full_Timeless [instance, in WBLogic.program_logic.ghost_stacks]
gstack_frag_Timeless [instance, in WBLogic.program_logic.ghost_stacks]
gstack_exists [definition, in WBLogic.program_logic.ghost_stacks]
gstack_full [definition, in WBLogic.program_logic.ghost_stacks]
gstack_frag [definition, in WBLogic.program_logic.ghost_stacks]
gtop [definition, in WBLogic.program_logic.ghost_stacks]
gtop_inv [lemma, in WBLogic.program_logic.ghost_stacks]
gtop_gsingleton [lemma, in WBLogic.program_logic.ghost_stacks]
gtop_gpush [lemma, in WBLogic.program_logic.ghost_stacks]
H
head_step_to_val [lemma, in WBLogic.heap_lang_trace.lang]heap [section, in WBLogic.heap_lang.proofmode]
heap [section, in WBLogic.heap_lang_trace.proofmode]
heap [section, in WBLogic.heap_lang_trace.proofmode]
heapIG [record, in WBLogic.F_mu_ref.wp_rules]
heapIG_irisG [instance, in WBLogic.F_mu_ref.wp_rules]
heapI_gstacksIG [projection, in WBLogic.F_mu_ref.wp_rules]
heapI_gen_heapG [projection, in WBLogic.F_mu_ref.wp_rules]
heapI_invG [projection, in WBLogic.F_mu_ref.wp_rules]
heapS_mapsto_timeless [instance, in WBLogic.F_mu_ref.binary.rules]
heapS_mapsto [definition, in WBLogic.F_mu_ref.binary.rules]
heapUR [definition, in WBLogic.F_mu_ref.binary.rules]
heap_array_to_seq_mapsto [lemma, in WBLogic.heap_lang_trace.primitive_laws]
heap_array_to_seq_meta [lemma, in WBLogic.heap_lang_trace.primitive_laws]
heap_singleton_included [lemma, in WBLogic.F_mu_ref.binary.rules]
heap_lang [definition, in WBLogic.heap_lang_trace.lang]
heap_ectx_lang [definition, in WBLogic.heap_lang_trace.lang]
heap_ectxi_lang [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.heap_lang_mixin [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.new_proph_id_fresh [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.alloc_fresh [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item_no_val_inj [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.head_ctx_step_val [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.val_head_stuck [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item_val [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item_inj [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.head_step_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.head_step_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.FreshS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.EmitS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.NewProphS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ForkS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FaaS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.XchgS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.StoreS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LoadS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FreeS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CaseRS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CaseLS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.SndS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FstS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.IfFalseS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.IfTrueS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.UnOpS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.BetaS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjRS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjLS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.PairS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.RecS [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.head_step [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.tags [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.state_init_heap_singleton [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.state_init_heap [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_map_disjoint [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_lookup [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_singleton [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.state_upd_used_proph_id [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.state_add_event [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.state_upd_heap [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_loc [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_bool [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_int [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_eval [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.subst' [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.subst [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.FreshCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.EmitCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveMCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FaaRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FaaLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgMCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.XchgRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.XchgLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.StoreRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.StoreLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LoadCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FreeCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CaseCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.SndCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FstCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.PairRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.PairLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.IfCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.UnOpCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AppRCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AppLCtx [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.exprO [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.valO [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.locO [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.stateO [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_inhabited [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.val_inhabited [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.state_inhabited [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.val_countable [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_countable [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_countable [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_finite [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_countable [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.val_eq_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_eq_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eq_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_eq_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_eq_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.of_val_inj [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.of_to_val [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.to_of_val [lemma, in WBLogic.heap_lang_trace.lang]
heap_lang.used_proph_id [projection, in WBLogic.heap_lang_trace.lang]
heap_lang.trace [projection, in WBLogic.heap_lang_trace.lang]
heap_lang.heap [projection, in WBLogic.heap_lang_trace.lang]
heap_lang.state [record, in WBLogic.heap_lang_trace.lang]
heap_lang.vals_compare_safe [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.val_is_unboxed_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.lit_is_unboxed_dec [instance, in WBLogic.heap_lang_trace.lang]
heap_lang.val_is_unboxed [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.lit_is_unboxed [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.to_val [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.of_val [abbreviation, in WBLogic.heap_lang_trace.lang]
heap_lang.observation [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.val_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.val_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.val_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.val_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.expr_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.InjRV [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjLV [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.PairV [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.RecV [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitV [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.val [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.Fresh [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Emit [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Resolve [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.NewProph [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Fork [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.FAA [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Xchg [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchg [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Store [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Load [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Free [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AllocN [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Case [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjR [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.InjL [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Snd [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Fst [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Pair [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.If [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.BinOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.UnOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.App [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Rec [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Var [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.Val [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.expr [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.OffsetOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.EqOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LtOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LeOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ShiftROp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.ShiftLOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.XorOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.OrOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.AndOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.RemOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.QuotOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.MultOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.MinusOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.PlusOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.MinusUnOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.NegOp [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.un_op [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_sind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_rec [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_ind [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_rect [definition, in WBLogic.heap_lang_trace.lang]
heap_lang.LitProphecy [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitTag [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitLoc [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitPoison [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitUnit [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitBool [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.LitInt [constructor, in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit [inductive, in WBLogic.heap_lang_trace.lang]
heap_lang.proph_id [definition, in WBLogic.heap_lang_trace.lang]
heap_lang [module, in WBLogic.heap_lang_trace.lang]
heapΣ [definition, in WBLogic.heap_lang_trace.adequacy]
heapΣ [definition, in WBLogic.heap_lang.adequacy]
hist [definition, in WBLogic.heap_lang_trace.trace_resources]
hist_trace_is_prefix [lemma, in WBLogic.heap_lang_trace.trace_resources]
hist_persistent [instance, in WBLogic.heap_lang_trace.trace_resources]
I
Ids_type [instance, in WBLogic.F_mu_ref.typing]If_typed [constructor, in WBLogic.F_mu_ref.typing]
if_false_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
if_true_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
inG_soundness_binaryΣ [instance, in WBLogic.F_mu_ref.binary.soundness]
InjL_typed [constructor, in WBLogic.F_mu_ref.typing]
injl_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
InjR_typed [constructor, in WBLogic.F_mu_ref.typing]
injr_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
interp [definition, in WBLogic.F_mu_ref.binary.logrel]
interp [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_expr_change_type [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_ren [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_cons [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_nil [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_Some_l [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_length [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_subst [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_subst_up [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_weaken [lemma, in WBLogic.F_mu_ref.binary.logrel]
interp_env_persistent [instance, in WBLogic.F_mu_ref.binary.logrel]
interp_env_base_persistent [instance, in WBLogic.F_mu_ref.binary.logrel]
interp_env [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_ref [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_ref_inv [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_rec [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_rec1_contractive [instance, in WBLogic.F_mu_ref.binary.logrel]
interp_rec1 [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_exist [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_forall [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_arrow [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_sum [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_prod [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_bool [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_nat [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_unit [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_expr_proper [instance, in WBLogic.F_mu_ref.binary.logrel]
interp_expr_ne [instance, in WBLogic.F_mu_ref.binary.logrel]
interp_expr [definition, in WBLogic.F_mu_ref.binary.logrel]
interp_env_ren [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_env_cons [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_env_nil [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_env_Some_l [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_env_length [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_subst [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_subst_up [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_weaken [lemma, in WBLogic.F_mu_ref.unary.logrel]
interp_env_persistent [instance, in WBLogic.F_mu_ref.unary.logrel]
interp_env_base_persistent [instance, in WBLogic.F_mu_ref.unary.logrel]
interp_expr [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_env [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_ref [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_ref_inv [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_rec [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_rec1_contractive [instance, in WBLogic.F_mu_ref.unary.logrel]
interp_rec1 [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_exist [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_forall [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_arrow [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_sum [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_prod [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_bool [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_nat [definition, in WBLogic.F_mu_ref.unary.logrel]
interp_unit [definition, in WBLogic.F_mu_ref.unary.logrel]
into_val_val [instance, in WBLogic.heap_lang_trace.class_instances]
inv_mapsto_acc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_acc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_acc_strong [lemma, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_inv [lemma, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_proper [instance, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_proper [instance, in WBLogic.heap_lang_trace.primitive_laws]
inv_heap_inv [abbreviation, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto [definition, in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own [definition, in WBLogic.heap_lang_trace.primitive_laws]
irreducible_resolve [lemma, in WBLogic.heap_lang_trace.lang]
is_atomic_correct [instance, in WBLogic.F_mu_ref.lang]
is_atomic [definition, in WBLogic.F_mu_ref.lang]
is_except_0_wbwp [instance, in WBLogic.program_logic.weakestpre]
iter_up [lemma, in WBLogic.F_mu_ref.base]
L
Lam [abbreviation, in WBLogic.heap_lang_trace.notation]LamV [abbreviation, in WBLogic.heap_lang_trace.notation]
Lam_typed [constructor, in WBLogic.F_mu_ref.typing]
lang [library]
lang [library]
lang_rules [section, in WBLogic.F_mu_ref.wp_rules]
Let [abbreviation, in WBLogic.heap_lang_trace.notation]
LetCtx [abbreviation, in WBLogic.heap_lang_trace.notation]
LetIn_typed [constructor, in WBLogic.F_mu_ref.typing]
lifting [section, in WBLogic.program_logic.lifting]
lifting [section, in WBLogic.heap_lang_trace.derived_laws]
lifting [section, in WBLogic.heap_lang_trace.primitive_laws]
lifting [section, in WBLogic.heap_lang.primitive_laws]
lifting [section, in WBLogic.heap_lang.derived_laws]
lifting [library]
load_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
logN [definition, in WBLogic.F_mu_ref.binary.logrel]
logN [definition, in WBLogic.F_mu_ref.unary.logrel]
logrel [section, in WBLogic.F_mu_ref.binary.logrel]
logrel [section, in WBLogic.F_mu_ref.unary.logrel]
logrel [library]
logrel [library]
⟦ _ ⟧* [notation, in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧ [notation, in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧* [notation, in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ [notation, in WBLogic.F_mu_ref.unary.logrel]
log_typed [definition, in WBLogic.F_mu_ref.unary.fundamental]
lookup_to_heap_None [lemma, in WBLogic.F_mu_ref.binary.rules]
M
make_inv_mapsto [lemma, in WBLogic.heap_lang_trace.primitive_laws]make_STS [lemma, in WBLogic.program_logic.lib.sts]
mapstoS_valid_2 [lemma, in WBLogic.F_mu_ref.binary.rules]
mapstoS_valid [lemma, in WBLogic.F_mu_ref.binary.rules]
mapstoS_combine [lemma, in WBLogic.F_mu_ref.binary.rules]
mapstoS_agree [lemma, in WBLogic.F_mu_ref.binary.rules]
mapsto_persist [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_ne [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_frac_ne [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_combine [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_agree [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_valid_2 [lemma, in WBLogic.heap_lang_trace.primitive_laws]
mapsto_valid [lemma, in WBLogic.heap_lang_trace.primitive_laws]
Match [abbreviation, in WBLogic.heap_lang_trace.notation]
module_invariance [lemma, in WBLogic.heap_lang_trace.adequacy]
N
Nat_typed [constructor, in WBLogic.F_mu_ref.typing]new_pending [lemma, in WBLogic.oneshot]
new_proph_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
NONE [abbreviation, in WBLogic.heap_lang_trace.notation]
NONEV [abbreviation, in WBLogic.heap_lang_trace.notation]
notation [library]
nsteps_inv_r [lemma, in WBLogic.F_mu_ref.binary.rules]
O
oneshot [library]oneshotG [record, in WBLogic.oneshot]
oneshotR [definition, in WBLogic.oneshot]
oneshot_inG [projection, in WBLogic.oneshot]
oneshotΣ [definition, in WBLogic.oneshot]
P
Pack_typed [constructor, in WBLogic.F_mu_ref.typing]Pair_typed [constructor, in WBLogic.F_mu_ref.typing]
pair_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
pending [definition, in WBLogic.oneshot]
persistent_pred_ext [lemma, in WBLogic.persistent_pred]
persistent_pred_car_proper [instance, in WBLogic.persistent_pred]
persistent_pred_car_ne [instance, in WBLogic.persistent_pred]
persistent_pred_cofe [instance, in WBLogic.persistent_pred]
persistent_predO [definition, in WBLogic.persistent_pred]
persistent_pred_ofe_mixin [definition, in WBLogic.persistent_pred]
persistent_pred_dist [instance, in WBLogic.persistent_pred]
persistent_pred_equiv [instance, in WBLogic.persistent_pred]
persistent_pred [record, in WBLogic.persistent_pred]
persistent_pred [section, in WBLogic.persistent_pred]
persistent_pred [library]
pers_pred_persistent [projection, in WBLogic.persistent_pred]
pers_pred_car [projection, in WBLogic.persistent_pred]
prefix_snoc_inv [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
primitive_laws [library]
primitive_laws [library]
prim_step_to_val_is_head_step [lemma, in WBLogic.heap_lang_trace.lang]
pri_rel_po [projection, in WBLogic.program_logic.lib.sts]
pri_rel [projection, in WBLogic.program_logic.lib.sts]
proofmode [library]
proofmode [library]
proofmode_classes [section, in WBLogic.program_logic.weakestpre]
pub_pri_incl [projection, in WBLogic.program_logic.lib.sts]
pub_rel_po [projection, in WBLogic.program_logic.lib.sts]
pub_rel [projection, in WBLogic.program_logic.lib.sts]
pure_case_inr [instance, in WBLogic.heap_lang_trace.class_instances]
pure_case_inl [instance, in WBLogic.heap_lang_trace.class_instances]
pure_snd [instance, in WBLogic.heap_lang_trace.class_instances]
pure_fst [instance, in WBLogic.heap_lang_trace.class_instances]
pure_if_false [instance, in WBLogic.heap_lang_trace.class_instances]
pure_if_true [instance, in WBLogic.heap_lang_trace.class_instances]
pure_eqop [instance, in WBLogic.heap_lang_trace.class_instances]
pure_binop [instance, in WBLogic.heap_lang_trace.class_instances]
pure_unop [instance, in WBLogic.heap_lang_trace.class_instances]
pure_beta [instance, in WBLogic.heap_lang_trace.class_instances]
pure_injrc [instance, in WBLogic.heap_lang_trace.class_instances]
pure_injlc [instance, in WBLogic.heap_lang_trace.class_instances]
pure_pairc [instance, in WBLogic.heap_lang_trace.class_instances]
pure_recc [instance, in WBLogic.heap_lang_trace.class_instances]
pure_exec [section, in WBLogic.heap_lang_trace.class_instances]
pure_case_inr [instance, in WBLogic.F_mu_ref.wp_rules]
pure_case_inl [instance, in WBLogic.F_mu_ref.wp_rules]
pure_snd [instance, in WBLogic.F_mu_ref.wp_rules]
pure_fst [instance, in WBLogic.F_mu_ref.wp_rules]
pure_fold [instance, in WBLogic.F_mu_ref.wp_rules]
pure_pack [instance, in WBLogic.F_mu_ref.wp_rules]
pure_tlam [instance, in WBLogic.F_mu_ref.wp_rules]
pure_seq [instance, in WBLogic.F_mu_ref.wp_rules]
pure_LetIn [instance, in WBLogic.F_mu_ref.wp_rules]
pure_lam [instance, in WBLogic.F_mu_ref.wp_rules]
pure_rec [instance, in WBLogic.F_mu_ref.wp_rules]
R
Rec_typed [constructor, in WBLogic.F_mu_ref.typing]rec_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
related_public_states [lemma, in WBLogic.program_logic.lib.sts]
related_public_trans [lemma, in WBLogic.program_logic.lib.sts]
related_private_public [lemma, in WBLogic.program_logic.lib.sts]
related_private [definition, in WBLogic.program_logic.lib.sts]
related_public [definition, in WBLogic.program_logic.lib.sts]
Rename_type [instance, in WBLogic.F_mu_ref.typing]
ResolveProph [abbreviation, in WBLogic.heap_lang_trace.notation]
resolve_reducible [lemma, in WBLogic.heap_lang_trace.primitive_laws]
resolve_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
rules [library]
S
sem_typed_store [lemma, in WBLogic.F_mu_ref.unary.fundamental]sem_typed_load [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_alloc [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unfold [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_fold [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unpack [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_pack [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_tapp [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_tlam [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_app [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_seq [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_letin [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_lam [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_rec [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_if [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_case [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_injr [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_injl [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_snd [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_fst [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_pair [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_nat_binop [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_bool [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_nat [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unit [lemma, in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_var [lemma, in WBLogic.F_mu_ref.unary.fundamental]
Seq [abbreviation, in WBLogic.heap_lang_trace.notation]
SeqCtx [abbreviation, in WBLogic.heap_lang_trace.notation]
sequential_trace_alt_iff [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_of_sequential [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_prefix [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_with_opened_nil [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_app [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_open_front [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_sequential [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_call_middle [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_call [lemma, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_trace_alt [definition, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_sind [definition, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_ind [definition, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_app [constructor, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_wrap [constructor, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_nil [constructor, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace [inductive, in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_trace [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_sind [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_ind [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_close [constructor, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_open [constructor, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_nil [constructor, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened [inductive, in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_trace_alt [library]
Seq_typed [constructor, in WBLogic.F_mu_ref.typing]
shoot [lemma, in WBLogic.oneshot]
shot [definition, in WBLogic.oneshot]
shot_not_pending [lemma, in WBLogic.oneshot]
Skip [abbreviation, in WBLogic.heap_lang_trace.notation]
Snd_typed [constructor, in WBLogic.F_mu_ref.typing]
snd_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
SOME [abbreviation, in WBLogic.heap_lang_trace.notation]
SOMEV [abbreviation, in WBLogic.heap_lang_trace.notation]
soundness [lemma, in WBLogic.F_mu_ref.unary.soundness]
soundness [library]
soundness [library]
soundness_unary_preG_reg [projection, in WBLogic.F_mu_ref.unary.soundness]
soundness_unary_preG_heap [projection, in WBLogic.F_mu_ref.unary.soundness]
soundness_unary_preG_iris [projection, in WBLogic.F_mu_ref.unary.soundness]
soundness_unary_preG [record, in WBLogic.F_mu_ref.unary.soundness]
soundness_binaryΣ [definition, in WBLogic.F_mu_ref.binary.soundness]
Spec [section, in WBLogic.heap_lang_trace_examples.very_awkward]
specN [definition, in WBLogic.F_mu_ref.binary.rules]
spec_ctx_persistent [instance, in WBLogic.F_mu_ref.binary.rules]
spec_ctx [definition, in WBLogic.F_mu_ref.binary.rules]
spec_inv [definition, in WBLogic.F_mu_ref.binary.rules]
state_of [definition, in WBLogic.program_logic.lib.sts]
state_inh [projection, in WBLogic.program_logic.lib.sts]
steps [section, in WBLogic.heap_lang_trace.primitive_laws]
steps_lb_le [lemma, in WBLogic.heap_lang_trace.primitive_laws]
steps_auth_update_S [lemma, in WBLogic.heap_lang_trace.primitive_laws]
steps_auth_update [lemma, in WBLogic.heap_lang_trace.primitive_laws]
steps_lb_get [lemma, in WBLogic.heap_lang_trace.primitive_laws]
steps_lb_valid [lemma, in WBLogic.heap_lang_trace.primitive_laws]
steps_lb [definition, in WBLogic.heap_lang_trace.primitive_laws]
steps_auth [definition, in WBLogic.heap_lang_trace.primitive_laws]
step_resolve [lemma, in WBLogic.heap_lang_trace.primitive_laws]
step_nat_binop [lemma, in WBLogic.F_mu_ref.binary.rules]
step_if_true [lemma, in WBLogic.F_mu_ref.binary.rules]
step_if_false [lemma, in WBLogic.F_mu_ref.binary.rules]
step_case_inr [lemma, in WBLogic.F_mu_ref.binary.rules]
step_case_inl [lemma, in WBLogic.F_mu_ref.binary.rules]
step_snd [lemma, in WBLogic.F_mu_ref.binary.rules]
step_fst [lemma, in WBLogic.F_mu_ref.binary.rules]
step_pack [lemma, in WBLogic.F_mu_ref.binary.rules]
step_fold [lemma, in WBLogic.F_mu_ref.binary.rules]
step_tlam [lemma, in WBLogic.F_mu_ref.binary.rules]
step_seq [lemma, in WBLogic.F_mu_ref.binary.rules]
step_letin [lemma, in WBLogic.F_mu_ref.binary.rules]
step_lam [lemma, in WBLogic.F_mu_ref.binary.rules]
step_rec [lemma, in WBLogic.F_mu_ref.binary.rules]
step_store [lemma, in WBLogic.F_mu_ref.binary.rules]
step_load [lemma, in WBLogic.F_mu_ref.binary.rules]
step_alloc [lemma, in WBLogic.F_mu_ref.binary.rules]
step_pure' [lemma, in WBLogic.F_mu_ref.binary.rules]
step_insert_no_fork [lemma, in WBLogic.F_mu_ref.binary.rules]
step_insert [lemma, in WBLogic.F_mu_ref.binary.rules]
store_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
STS [section, in WBLogic.program_logic.lib.sts]
STS [record, in WBLogic.program_logic.lib.sts]
sts [library]
STSUR [definition, in WBLogic.program_logic.lib.sts]
sts_make_undo_private_trans [lemma, in WBLogic.program_logic.lib.sts]
sts_make_private_trans [lemma, in WBLogic.program_logic.lib.sts]
sts_make_public_trans [lemma, in WBLogic.program_logic.lib.sts]
sts_configs_pub_related [lemma, in WBLogic.program_logic.lib.sts]
sts_configs_update_frag [lemma, in WBLogic.program_logic.lib.sts]
STS_inv [definition, in WBLogic.program_logic.lib.sts]
sts_config_full [definition, in WBLogic.program_logic.lib.sts]
sts_config_frag [definition, in WBLogic.program_logic.lib.sts]
STS_inv_name [definition, in WBLogic.program_logic.lib.sts]
sts_config [definition, in WBLogic.program_logic.lib.sts]
STS_state [projection, in WBLogic.program_logic.lib.sts]
STSΣ [definition, in WBLogic.program_logic.lib.sts]
subG_oneshotΣ [instance, in WBLogic.oneshot]
subG_heapGpreS [instance, in WBLogic.heap_lang_trace.adequacy]
subG_heapGpreS [instance, in WBLogic.heap_lang.adequacy]
subG_tracePreG [instance, in WBLogic.heap_lang_trace.trace_resources]
subG_STSΣ_ing [instance, in WBLogic.program_logic.lib.sts]
SubstLemmas_typer [instance, in WBLogic.F_mu_ref.typing]
Subst_type [instance, in WBLogic.F_mu_ref.typing]
T
tactics [library]tac_wbwp_faa [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_cmpxchg_suc [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_cmpxchg_fail [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_cmpxchg [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_xchg [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_store [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_load [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_free [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_alloc [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_allocN [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_bind [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_value [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_value_nofupd [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_pure_credit [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_pure [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_expr_eval [lemma, in WBLogic.heap_lang.proofmode]
tac_wbwp_faa [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_xchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_store [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_load [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_free [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_alloc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_bind [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_value [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_value_nofupd [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_pure_credit [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_pure [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_expr_eval [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_faa [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_faa [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_xchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_xchg [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_store [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_store [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_load [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_load [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_free [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_free [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_alloc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_alloc [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_bind [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_bind [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_value [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_value [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_value_nofupd [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_value_nofupd [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_pure_credit [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_pure [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_pure [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_twp_expr_eval [lemma, in WBLogic.heap_lang_trace.proofmode]
tac_wp_expr_eval [lemma, in WBLogic.heap_lang_trace.proofmode]
TAlloc [constructor, in WBLogic.F_mu_ref.typing]
TApp_typed [constructor, in WBLogic.F_mu_ref.typing]
TArrow [constructor, in WBLogic.F_mu_ref.typing]
TBool [constructor, in WBLogic.F_mu_ref.typing]
TExist [constructor, in WBLogic.F_mu_ref.typing]
TFold [constructor, in WBLogic.F_mu_ref.typing]
TForall [constructor, in WBLogic.F_mu_ref.typing]
TLam_typed [constructor, in WBLogic.F_mu_ref.typing]
TLoad [constructor, in WBLogic.F_mu_ref.typing]
TNat [constructor, in WBLogic.F_mu_ref.typing]
to_heap_insert [lemma, in WBLogic.F_mu_ref.binary.rules]
to_heap [section, in WBLogic.F_mu_ref.binary.rules]
to_tpool_snoc [lemma, in WBLogic.F_mu_ref.binary.rules]
to_tpool_insert' [lemma, in WBLogic.F_mu_ref.binary.rules]
to_tpool_insert [lemma, in WBLogic.F_mu_ref.binary.rules]
to_tpool_valid [lemma, in WBLogic.F_mu_ref.binary.rules]
to_heap [definition, in WBLogic.F_mu_ref.binary.rules]
to_tpool [definition, in WBLogic.F_mu_ref.binary.rules]
to_tpool_go [definition, in WBLogic.F_mu_ref.binary.rules]
to_val_fill_some [lemma, in WBLogic.heap_lang_trace.lang]
TPCTX_cons [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TPCTX_nil [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TPCTX_Alloc [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
tpoolUR [definition, in WBLogic.F_mu_ref.binary.rules]
tpool_singleton_included' [lemma, in WBLogic.F_mu_ref.binary.rules]
tpool_singleton_included [lemma, in WBLogic.F_mu_ref.binary.rules]
tpool_lookup_Some [lemma, in WBLogic.F_mu_ref.binary.rules]
tpool_lookup [lemma, in WBLogic.F_mu_ref.binary.rules]
tpool_mapsto [definition, in WBLogic.F_mu_ref.binary.rules]
TProd [constructor, in WBLogic.F_mu_ref.typing]
TP_CTX_StoreR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_StoreL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Load [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_TApp [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_TLam [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Unfold [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Fold [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_BinOpR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_BinOpL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfM [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseM [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_InjR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_InjL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Snd [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Fst [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_PairR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_PairL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_AppR [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_AppL [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Rec [constructor, in WBLogic.F_mu_ref.binary.context_refinement]
Trace [section, in WBLogic.heap_lang_trace_examples.very_awkward]
traceGS [record, in WBLogic.heap_lang_trace.trace_resources]
traceO [definition, in WBLogic.heap_lang_trace.trace_resources]
trace_auth_init [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_is_inv [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_add_event [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_half_frag_agree [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_agree [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_auth_half_frag_agree [lemma, in WBLogic.heap_lang_trace.trace_resources]
trace_inv [definition, in WBLogic.heap_lang_trace.trace_resources]
trace_is [definition, in WBLogic.heap_lang_trace.trace_resources]
trace_half_frag [definition, in WBLogic.heap_lang_trace.trace_resources]
trace_auth [definition, in WBLogic.heap_lang_trace.trace_resources]
trace_preG_inG [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_hist_preG_inG [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_preG [record, in WBLogic.heap_lang_trace.trace_resources]
trace_name [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_inG [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_hist_name [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_hist_inG [projection, in WBLogic.heap_lang_trace.trace_resources]
trace_resources [library]
traceΣ [definition, in WBLogic.heap_lang_trace.trace_resources]
TRec [constructor, in WBLogic.F_mu_ref.typing]
Tref [constructor, in WBLogic.F_mu_ref.typing]
TStore [constructor, in WBLogic.F_mu_ref.typing]
TSum [constructor, in WBLogic.F_mu_ref.typing]
TUnfold [constructor, in WBLogic.F_mu_ref.typing]
TUnit [constructor, in WBLogic.F_mu_ref.typing]
TVar [constructor, in WBLogic.F_mu_ref.typing]
twp_faa [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_xchg [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_store [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_load [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_free [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_alloc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_allocN_seq [lemma, in WBLogic.heap_lang_trace.primitive_laws]
twp_fork [lemma, in WBLogic.heap_lang_trace.primitive_laws]
type [inductive, in WBLogic.F_mu_ref.typing]
typed [inductive, in WBLogic.F_mu_ref.typing]
typed_n_closed [lemma, in WBLogic.F_mu_ref.typing]
typed_sind [definition, in WBLogic.F_mu_ref.typing]
typed_ind [definition, in WBLogic.F_mu_ref.typing]
typed_interp [section, in WBLogic.F_mu_ref.unary.fundamental]
typed_ctx_n_closed [lemma, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_typed [lemma, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_sind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_ind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx [inductive, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_typed [lemma, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_sind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_ind [definition, in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item [inductive, in WBLogic.F_mu_ref.binary.context_refinement]
type_sind [definition, in WBLogic.F_mu_ref.typing]
type_rec [definition, in WBLogic.F_mu_ref.typing]
type_ind [definition, in WBLogic.F_mu_ref.typing]
type_rect [definition, in WBLogic.F_mu_ref.typing]
type_soundness [lemma, in WBLogic.F_mu_ref.unary.soundness]
typing [library]
U
Unit_typed [constructor, in WBLogic.F_mu_ref.typing]unop_atomic [instance, in WBLogic.heap_lang_trace.class_instances]
UnpackIn_typed [constructor, in WBLogic.F_mu_ref.typing]
V
vae_sts [definition, in WBLogic.heap_lang_examples.sts.very_awkward]varO [definition, in WBLogic.F_mu_ref.base]
Var_typed [constructor, in WBLogic.F_mu_ref.typing]
very_awkward_self_apply_safe [lemma, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_self_apply_sem_typed [lemma, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_sem_typed [lemma, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward [section, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_self_apply [definition, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_typed [lemma, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward [definition, in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_self_apply_returns_one [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward [section, in WBLogic.heap_lang_trace_examples.very_awkward]
very_akward_call_fact_across [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward_self_apply [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
very_awk_spec [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward_call_twice_return_one_ctx_equiv [lemma, in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_call_twice_return_one_refinement [lemma, in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward [section, in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_typed [lemma, in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward [definition, in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_self_apply_returns_one [lemma, in WBLogic.heap_lang_examples.very_awkward]
very_awkward [section, in WBLogic.heap_lang_examples.very_awkward]
very_akward_call_fact_across [definition, in WBLogic.heap_lang_examples.very_awkward]
very_awkward_self_apply [definition, in WBLogic.heap_lang_examples.very_awkward]
very_awkward [definition, in WBLogic.heap_lang_examples.very_awkward]
very_awkward_self_apply_returns_one [lemma, in WBLogic.heap_lang_examples.sts.very_awkward]
very_awkward [section, in WBLogic.heap_lang_examples.sts.very_awkward]
very_awkward_self_apply [definition, in WBLogic.heap_lang_examples.sts.very_awkward]
very_awkward [definition, in WBLogic.heap_lang_examples.sts.very_awkward]
very_awkward [library]
very_awkward [library]
very_awkward [library]
very_awkward [library]
very_awkward [library]
W
wbheapGpreS [record, in WBLogic.heap_lang_trace.adequacy]wbheapGpreS [record, in WBLogic.heap_lang.adequacy]
wbheapGpreS_trace [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_gstacks [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_proph [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_inv_heap [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_heap [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_iris [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_gstacks [projection, in WBLogic.heap_lang.adequacy]
wbheapGpreS_proph [projection, in WBLogic.heap_lang.adequacy]
wbheapGpreS_inv_heap [projection, in WBLogic.heap_lang.adequacy]
wbheapGpreS_heap [projection, in WBLogic.heap_lang.adequacy]
wbheapGpreS_iris [projection, in WBLogic.heap_lang.adequacy]
wbheapGS [record, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS [record, in WBLogic.heap_lang.primitive_laws]
wbheapGS_traceGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_gstacksGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_step_cnt [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_step_name [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_proph_mapGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_inv_heapGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_gen_heapGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_invGS [projection, in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_heapGS [instance, in WBLogic.heap_lang.primitive_laws]
wbheapGS_gstacksGS [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_cnt [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_name [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_proph_mapGS [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_inv_heapGS [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_gen_heapGS [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_invGS [projection, in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_cnt [projection, in WBLogic.heap_lang_trace.adequacy]
wbheapGS_step_cnt [projection, in WBLogic.heap_lang.adequacy]
wbheapG_irisG [instance, in WBLogic.heap_lang_trace.primitive_laws]
wbheap_invariance [definition, in WBLogic.heap_lang_trace.adequacy]
wbheap_adequacy [definition, in WBLogic.heap_lang_trace.adequacy]
wbheap_adequacy [definition, in WBLogic.heap_lang.adequacy]
wbwp [definition, in WBLogic.program_logic.weakestpre]
wbwp_invariance [lemma, in WBLogic.program_logic.adequacy]
wbwp_adequacy [lemma, in WBLogic.program_logic.adequacy]
wbwp_strong_adequacy [lemma, in WBLogic.program_logic.adequacy]
wbwp_pure_step_later [lemma, in WBLogic.program_logic.lifting]
wbwp_pure_step_fupd [lemma, in WBLogic.program_logic.lifting]
wbwp_resolve_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve_proph [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_faa_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_faa_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_fail_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_fail_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_suc_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_suc_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_xchg_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_xchg_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_store_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_store_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_load_offset_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_load_offset [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_allocN_vec [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_allocN [lemma, in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_fresh [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_emit [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_new_proph [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_faa [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_xchg [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_store [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_load [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_free [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_alloc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_allocN_seq [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_rec_löb [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_step_fupdN_lb [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_lb_update [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_lb_init [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wbwp_resolve [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_new_proph [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_faa [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_cmpxchg_suc [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_cmpxchg_fail [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_xchg [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_store [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_load [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_free [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_alloc [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_allocN_seq [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_step_fupdN_lb [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_lb_update [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_lb_init [lemma, in WBLogic.heap_lang.primitive_laws]
wbwp_very_akward_call_fact_across_returns_one [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_akward_call_fact_across [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_awkward_self_apply [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_awkward [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_awkward_self_apply [lemma, in WBLogic.heap_lang_examples.awkward]
wbwp_awkward [lemma, in WBLogic.heap_lang_examples.awkward]
wbwp_very_akward_call_fact_across_returns_one [lemma, in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_akward_call_fact_across [lemma, in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_awkward_self_apply [lemma, in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_awkward [lemma, in WBLogic.heap_lang_examples.very_awkward]
wbwp_wand_r [lemma, in WBLogic.program_logic.weakestpre]
wbwp_wand_l [lemma, in WBLogic.program_logic.weakestpre]
wbwp_wand [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_step_r' [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_step_l' [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_step_r [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_step_l [lemma, in WBLogic.program_logic.weakestpre]
wbwp_step_fupd [lemma, in WBLogic.program_logic.weakestpre]
wbwp_step_fupdN [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_r [lemma, in WBLogic.program_logic.weakestpre]
wbwp_frame_l [lemma, in WBLogic.program_logic.weakestpre]
wbwp_value [lemma, in WBLogic.program_logic.weakestpre]
wbwp_value' [lemma, in WBLogic.program_logic.weakestpre]
wbwp_value_fupd [lemma, in WBLogic.program_logic.weakestpre]
wbwp_flip_mono' [instance, in WBLogic.program_logic.weakestpre]
wbwp_mono' [instance, in WBLogic.program_logic.weakestpre]
wbwp_mono [lemma, in WBLogic.program_logic.weakestpre]
wbwp_bind [lemma, in WBLogic.program_logic.weakestpre]
wbwp_step_fupdN_strong [lemma, in WBLogic.program_logic.weakestpre]
wbwp_credit_access [lemma, in WBLogic.program_logic.weakestpre]
wbwp_fupd [lemma, in WBLogic.program_logic.weakestpre]
wbwp_make_gstack [lemma, in WBLogic.program_logic.weakestpre]
wbwp_mend [lemma, in WBLogic.program_logic.weakestpre]
wbwp_get_gstack_full [lemma, in WBLogic.program_logic.weakestpre]
wbwp_strong_mono [lemma, in WBLogic.program_logic.weakestpre]
wbwp_value_fupd' [lemma, in WBLogic.program_logic.weakestpre]
wbwp_contractive [instance, in WBLogic.program_logic.weakestpre]
wbwp_proper [instance, in WBLogic.program_logic.weakestpre]
wbwp_ne [instance, in WBLogic.program_logic.weakestpre]
wbwp_store [lemma, in WBLogic.F_mu_ref.wp_rules]
wbwp_load [lemma, in WBLogic.F_mu_ref.wp_rules]
wbwp_alloc [lemma, in WBLogic.F_mu_ref.wp_rules]
wbwp_resolve_cmpxchg_fail [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_resolve_cmpxchg_suc [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_resolve_proph [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_faa_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_faa_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_fail_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_fail_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_suc_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_suc_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_xchg_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_xchg_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_store_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_store_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_load_offset_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_load_offset [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_allocN_vec [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_allocN [lemma, in WBLogic.heap_lang.derived_laws]
wbwp_sts_mend [lemma, in WBLogic.program_logic.lib.sts]
wbwp_sts_get_state [lemma, in WBLogic.program_logic.lib.sts]
wbwp_very_awkward_self_apply [lemma, in WBLogic.heap_lang_examples.sts.very_awkward]
wbwp_very_awkward [lemma, in WBLogic.heap_lang_examples.sts.very_awkward]
wb_mask_mono [lemma, in WBLogic.program_logic.weakestpre]
weakestpre [library]
wp [section, in WBLogic.program_logic.weakestpre]
wp_resolve [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_new_proph [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_faa [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_cmpxchg_suc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_cmpxchg_fail [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_xchg [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_store [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_load [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_free [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_alloc [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_allocN_seq [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_fork [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_fresh [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_emit [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_rec_löb [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_step_fupdN_lb [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_lb_update [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_lb_init [lemma, in WBLogic.heap_lang_trace.primitive_laws]
wp_rec_löb [lemma, in WBLogic.heap_lang.primitive_laws]
wp_call_fact_across [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wp_factorial [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
wp_call_fact_across [lemma, in WBLogic.heap_lang_examples.very_awkward]
wp_factorial [lemma, in WBLogic.heap_lang_examples.very_awkward]
wp_frame_wand [lemma, in WBLogic.program_logic.weakestpre]
wp_wbwp [lemma, in WBLogic.program_logic.weakestpre]
wp_atomic [lemma, in WBLogic.program_logic.weakestpre]
wp_nat_binop [instance, in WBLogic.F_mu_ref.wp_rules]
wp_if_false [instance, in WBLogic.F_mu_ref.wp_rules]
wp_if_true [instance, in WBLogic.F_mu_ref.wp_rules]
wp_store [lemma, in WBLogic.F_mu_ref.wp_rules]
wp_load [lemma, in WBLogic.F_mu_ref.wp_rules]
wp_alloc [lemma, in WBLogic.F_mu_ref.wp_rules]
wp_rules [library]
Wrap [module, in WBLogic.heap_lang_trace_examples.very_awkward]
wrap_very_awk_correct [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
Wrap.correct [lemma, in WBLogic.heap_lang_trace_examples.very_awkward]
Wrap.S [section, in WBLogic.heap_lang_trace_examples.very_awkward]
Wrap.very_awk_instrumented [definition, in WBLogic.heap_lang_trace_examples.very_awkward]
X
xchg_atomic [instance, in WBLogic.heap_lang_trace.class_instances]other
_ ↦_ _ _ (bi_scope) [notation, in WBLogic.heap_lang_trace.primitive_laws]_ ↦_ _ □ (bi_scope) [notation, in WBLogic.heap_lang_trace.primitive_laws]
_ ↦ _ _ (bi_scope) [notation, in WBLogic.heap_lang_trace.primitive_laws]
_ ⤇ _ (bi_scope) [notation, in WBLogic.F_mu_ref.binary.rules]
_ ↦ₛ _ (bi_scope) [notation, in WBLogic.F_mu_ref.binary.rules]
_ ↦ₛ{ _ } _ (bi_scope) [notation, in WBLogic.F_mu_ref.binary.rules]
{WB{{ _ } } } _ {{{ RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ _ .. _ , RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @< _ >{{ _ , _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ {{ _ , _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @ _ {{ _ , _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @ _ ; _ {{ _ , _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @< _ >{{ _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ {{ _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @ _ {{ _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
WBWP _ @ _ ; _ {{ _ } } (bi_scope) [notation, in WBLogic.program_logic.weakestpre]
_ ↦ᵢ _ (bi_scope) [notation, in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ{# _ } _ (bi_scope) [notation, in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ□ _ (bi_scope) [notation, in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ{ _ } _ (bi_scope) [notation, in WBLogic.F_mu_ref.wp_rules]
resolve_proph: _ to: _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
match: _ with SOME _ => _ | NONE => _ end (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
match: _ with NONE => _ | SOME _ => _ end (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ || _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ && _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ;; _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
let: _ := _ in _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
λ: _ _ .. _ , _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
λ: _ , _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
rec: _ _ _ .. _ := _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
if: _ then _ else _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
rec: _ _ := _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ <- _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
~ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ≠ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ = _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ < _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ≤ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ≫ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ≪ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ `rem` _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ `quot` _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ * _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ - _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ +ₗ _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ + _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
- _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
ref _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
! _ (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
match: _ with InjR _ => _ | InjL _ => _ end (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
match: _ with InjL _ => _ | InjR _ => _ end (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
( _ , _ , .. , _ ) (expr_scope) [notation, in WBLogic.heap_lang_trace.notation]
{WB{{ _ } } } _ {{{ RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ > {{{ RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [notation, in WBLogic.program_logic.weakestpre]
λ: _ _ .. _ , _ (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
λ: _ , _ (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
rec: _ _ _ .. _ := _ (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
rec: _ _ := _ (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
() (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
( _ , _ , .. , _ ) (val_scope) [notation, in WBLogic.heap_lang_trace.notation]
_ ⊢ₜ _ : _ [notation, in WBLogic.F_mu_ref.typing]
_ ⊨ _ : _ [notation, in WBLogic.F_mu_ref.unary.fundamental]
_ ⊨ _ ≤ctx≤ _ : _ [notation, in WBLogic.F_mu_ref.binary.context_refinement]
_ ⊨ _ ≤log≤ _ : _ [notation, in WBLogic.F_mu_ref.binary.fundamental]
# _ [notation, in WBLogic.heap_lang_trace.notation]
⟦ _ ⟧* [notation, in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧ₑ [notation, in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧ [notation, in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧* [notation, in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ₑ [notation, in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ [notation, in WBLogic.F_mu_ref.unary.logrel]
Notation Index
F
#nv _ [in WBLogic.F_mu_ref.lang]#♭v _ [in WBLogic.F_mu_ref.lang]
#n _ [in WBLogic.F_mu_ref.lang]
#♭ _ [in WBLogic.F_mu_ref.lang]
L
⟦ _ ⟧* [in WBLogic.F_mu_ref.binary.logrel]⟦ _ ⟧ [in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧* [in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ [in WBLogic.F_mu_ref.unary.logrel]
other
_ ↦_ _ _ (bi_scope) [in WBLogic.heap_lang_trace.primitive_laws]_ ↦_ _ □ (bi_scope) [in WBLogic.heap_lang_trace.primitive_laws]
_ ↦ _ _ (bi_scope) [in WBLogic.heap_lang_trace.primitive_laws]
_ ⤇ _ (bi_scope) [in WBLogic.F_mu_ref.binary.rules]
_ ↦ₛ _ (bi_scope) [in WBLogic.F_mu_ref.binary.rules]
_ ↦ₛ{ _ } _ (bi_scope) [in WBLogic.F_mu_ref.binary.rules]
{WB{{ _ } } } _ {{{ RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ _ .. _ , RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ _ .. _ , RET _ ; _ } } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @< _ >{{ _ , _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ {{ _ , _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @ _ {{ _ , _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @ _ ; _ {{ _ , _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @< _ >{{ _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ {{ _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @ _ {{ _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
WBWP _ @ _ ; _ {{ _ } } (bi_scope) [in WBLogic.program_logic.weakestpre]
_ ↦ᵢ _ (bi_scope) [in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ{# _ } _ (bi_scope) [in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ□ _ (bi_scope) [in WBLogic.F_mu_ref.wp_rules]
_ ↦ᵢ{ _ } _ (bi_scope) [in WBLogic.F_mu_ref.wp_rules]
resolve_proph: _ to: _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
match: _ with SOME _ => _ | NONE => _ end (expr_scope) [in WBLogic.heap_lang_trace.notation]
match: _ with NONE => _ | SOME _ => _ end (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ || _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ && _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ ;; _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
let: _ := _ in _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
λ: _ _ .. _ , _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
λ: _ , _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
rec: _ _ _ .. _ := _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
if: _ then _ else _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
rec: _ _ := _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ <- _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
~ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ ≠ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ = _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ < _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ ≤ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ ≫ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ ≪ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ `rem` _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ `quot` _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ * _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ - _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ +ₗ _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
_ + _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
- _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
ref _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
! _ (expr_scope) [in WBLogic.heap_lang_trace.notation]
match: _ with InjR _ => _ | InjL _ => _ end (expr_scope) [in WBLogic.heap_lang_trace.notation]
match: _ with InjL _ => _ | InjR _ => _ end (expr_scope) [in WBLogic.heap_lang_trace.notation]
( _ , _ , .. , _ ) (expr_scope) [in WBLogic.heap_lang_trace.notation]
{WB{{ _ } } } _ {{{ RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ > {{{ RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @< _ >{{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
{WB{{ _ } } } _ @ _ ; _ {{{ _ .. _ , RET _ ; _ } } } (stdpp_scope) [in WBLogic.program_logic.weakestpre]
λ: _ _ .. _ , _ (val_scope) [in WBLogic.heap_lang_trace.notation]
λ: _ , _ (val_scope) [in WBLogic.heap_lang_trace.notation]
rec: _ _ _ .. _ := _ (val_scope) [in WBLogic.heap_lang_trace.notation]
rec: _ _ := _ (val_scope) [in WBLogic.heap_lang_trace.notation]
() (val_scope) [in WBLogic.heap_lang_trace.notation]
( _ , _ , .. , _ ) (val_scope) [in WBLogic.heap_lang_trace.notation]
_ ⊢ₜ _ : _ [in WBLogic.F_mu_ref.typing]
_ ⊨ _ : _ [in WBLogic.F_mu_ref.unary.fundamental]
_ ⊨ _ ≤ctx≤ _ : _ [in WBLogic.F_mu_ref.binary.context_refinement]
_ ⊨ _ ≤log≤ _ : _ [in WBLogic.F_mu_ref.binary.fundamental]
# _ [in WBLogic.heap_lang_trace.notation]
⟦ _ ⟧* [in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧ₑ [in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧ [in WBLogic.F_mu_ref.binary.logrel]
⟦ _ ⟧* [in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ₑ [in WBLogic.F_mu_ref.unary.logrel]
⟦ _ ⟧ [in WBLogic.F_mu_ref.unary.logrel]
Module Index
F
F_mu_ref [in WBLogic.F_mu_ref.lang]H
heap_lang [in WBLogic.heap_lang_trace.lang]W
Wrap [in WBLogic.heap_lang_trace_examples.very_awkward]Library Index
A
adequacyadequacy
adequacy
awkward
B
baseC
class_instancescontext_refinement
D
derived_lawsderived_laws
F
factfundamental
fundamental
G
ghost_stacksL
langlang
lifting
logrel
logrel
N
notationO
oneshotP
persistent_predprimitive_laws
primitive_laws
proofmode
proofmode
R
rulesS
sequential_trace_altsoundness
soundness
sts
T
tacticstrace_resources
typing
V
very_awkwardvery_awkward
very_awkward
very_awkward
very_awkward
W
weakestprewp_rules
Lemma Index
A
alloc_hist [in WBLogic.heap_lang_trace.trace_resources]awkward_self_apply_returns_one [in WBLogic.heap_lang_examples.awkward]
B
basic_soundness [in WBLogic.F_mu_ref.binary.soundness]binary_fundamental [in WBLogic.F_mu_ref.binary.fundamental]
binary_soundness [in WBLogic.F_mu_ref.binary.soundness]
bin_log_related_under_typed_ctx [in WBLogic.F_mu_ref.binary.context_refinement]
bin_log_related_store [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_load [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_alloc [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unfold [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_fold [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unpack [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_pack [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_tapp [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_tlam [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_app [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_seq [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_letin [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_lam [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_rec [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_nat_binop [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_if [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_case [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_injr [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_injl [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_snd [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_fst [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_pair [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_bool [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_nat [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_unit [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_var [in WBLogic.F_mu_ref.binary.fundamental]
bin_log_related_alt [in WBLogic.F_mu_ref.binary.fundamental]
bin_val_rel_bin_expr_rel [in WBLogic.F_mu_ref.binary.fundamental]
bin_expr_rel_bind [in WBLogic.F_mu_ref.binary.fundamental]
C
call_twice_return_one_very_awkward_refinement [in WBLogic.F_mu_ref.binary.examples.very_awkward]call_twice_return_one_typed [in WBLogic.F_mu_ref.binary.examples.very_awkward]
closed_context_weakening [in WBLogic.F_mu_ref.typing]
context_weakening [in WBLogic.F_mu_ref.typing]
context_gen_weakening [in WBLogic.F_mu_ref.typing]
D
do_step_pure [in WBLogic.F_mu_ref.binary.rules]E
env_subst_lookup [in WBLogic.F_mu_ref.typing]F
fact_ctx_equiv [in WBLogic.F_mu_ref.binary.examples.fact]fact_acc_fact_refinement [in WBLogic.F_mu_ref.binary.examples.fact]
fact_fact_acc_refinement [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_typed [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_subst [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_unfold [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_unfold [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_subst [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body_typed [in WBLogic.F_mu_ref.binary.examples.fact]
fact_unfold [in WBLogic.F_mu_ref.binary.examples.fact]
fact_typed [in WBLogic.F_mu_ref.binary.examples.fact]
fixpoint_interp_rec1_eq [in WBLogic.F_mu_ref.binary.logrel]
fixpoint_interp_rec1_eq [in WBLogic.F_mu_ref.unary.logrel]
fundamental [in WBLogic.F_mu_ref.unary.fundamental]
fupd_wbwp [in WBLogic.program_logic.weakestpre]
F_mu_ref.lang_mixin [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_head_stuck [in WBLogic.F_mu_ref.lang]
F_mu_ref.alloc_fresh [in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item_no_val_inj [in WBLogic.F_mu_ref.lang]
F_mu_ref.head_ctx_step_val [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_stuck [in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item_val [in WBLogic.F_mu_ref.lang]
F_mu_ref.of_to_val [in WBLogic.F_mu_ref.lang]
F_mu_ref.to_of_val [in WBLogic.F_mu_ref.lang]
G
gmap_of_trace_valid [in WBLogic.heap_lang_trace.trace_resources]gmap_of_trace_hist_valid_prefix [in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace_dom [in WBLogic.heap_lang_trace.trace_resources]
gmap_of_trace_snoc [in WBLogic.heap_lang_trace.trace_resources]
gpop_gpush [in WBLogic.program_logic.ghost_stacks]
gstacks_init [in WBLogic.program_logic.ghost_stacks]
gstacks_except_included [in WBLogic.program_logic.ghost_stacks]
gstacks_out_swap [in WBLogic.program_logic.ghost_stacks]
gstacks_put_back [in WBLogic.program_logic.ghost_stacks]
gstacks_take_out [in WBLogic.program_logic.ghost_stacks]
gstacks_agree [in WBLogic.program_logic.ghost_stacks]
gstack_alloc [in WBLogic.program_logic.ghost_stacks]
gstack_full_is_out [in WBLogic.program_logic.ghost_stacks]
gstack_full_in [in WBLogic.program_logic.ghost_stacks]
gstack_frag_not_out_agree [in WBLogic.program_logic.ghost_stacks]
gstack_frag_in [in WBLogic.program_logic.ghost_stacks]
gstack_exists_in [in WBLogic.program_logic.ghost_stacks]
gstack_full_exists [in WBLogic.program_logic.ghost_stacks]
gstack_frag_exists [in WBLogic.program_logic.ghost_stacks]
gstack_pop [in WBLogic.program_logic.ghost_stacks]
gstack_push [in WBLogic.program_logic.ghost_stacks]
gstack_full_unique [in WBLogic.program_logic.ghost_stacks]
gstack_frag_unique [in WBLogic.program_logic.ghost_stacks]
gtop_inv [in WBLogic.program_logic.ghost_stacks]
gtop_gsingleton [in WBLogic.program_logic.ghost_stacks]
gtop_gpush [in WBLogic.program_logic.ghost_stacks]
H
head_step_to_val [in WBLogic.heap_lang_trace.lang]heap_array_to_seq_mapsto [in WBLogic.heap_lang_trace.primitive_laws]
heap_array_to_seq_meta [in WBLogic.heap_lang_trace.primitive_laws]
heap_singleton_included [in WBLogic.F_mu_ref.binary.rules]
heap_lang.heap_lang_mixin [in WBLogic.heap_lang_trace.lang]
heap_lang.new_proph_id_fresh [in WBLogic.heap_lang_trace.lang]
heap_lang.alloc_fresh [in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item_no_val_inj [in WBLogic.heap_lang_trace.lang]
heap_lang.head_ctx_step_val [in WBLogic.heap_lang_trace.lang]
heap_lang.val_head_stuck [in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item_val [in WBLogic.heap_lang_trace.lang]
heap_lang.state_init_heap_singleton [in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_map_disjoint [in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_lookup [in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array_singleton [in WBLogic.heap_lang_trace.lang]
heap_lang.of_to_val [in WBLogic.heap_lang_trace.lang]
heap_lang.to_of_val [in WBLogic.heap_lang_trace.lang]
hist_trace_is_prefix [in WBLogic.heap_lang_trace.trace_resources]
I
interp_expr_change_type [in WBLogic.F_mu_ref.binary.logrel]interp_env_ren [in WBLogic.F_mu_ref.binary.logrel]
interp_env_cons [in WBLogic.F_mu_ref.binary.logrel]
interp_env_nil [in WBLogic.F_mu_ref.binary.logrel]
interp_env_Some_l [in WBLogic.F_mu_ref.binary.logrel]
interp_env_length [in WBLogic.F_mu_ref.binary.logrel]
interp_subst [in WBLogic.F_mu_ref.binary.logrel]
interp_subst_up [in WBLogic.F_mu_ref.binary.logrel]
interp_weaken [in WBLogic.F_mu_ref.binary.logrel]
interp_env_ren [in WBLogic.F_mu_ref.unary.logrel]
interp_env_cons [in WBLogic.F_mu_ref.unary.logrel]
interp_env_nil [in WBLogic.F_mu_ref.unary.logrel]
interp_env_Some_l [in WBLogic.F_mu_ref.unary.logrel]
interp_env_length [in WBLogic.F_mu_ref.unary.logrel]
interp_subst [in WBLogic.F_mu_ref.unary.logrel]
interp_subst_up [in WBLogic.F_mu_ref.unary.logrel]
interp_weaken [in WBLogic.F_mu_ref.unary.logrel]
inv_mapsto_acc [in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_acc [in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_acc_strong [in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_inv [in WBLogic.heap_lang_trace.primitive_laws]
irreducible_resolve [in WBLogic.heap_lang_trace.lang]
iter_up [in WBLogic.F_mu_ref.base]
L
lookup_to_heap_None [in WBLogic.F_mu_ref.binary.rules]M
make_inv_mapsto [in WBLogic.heap_lang_trace.primitive_laws]make_STS [in WBLogic.program_logic.lib.sts]
mapstoS_valid_2 [in WBLogic.F_mu_ref.binary.rules]
mapstoS_valid [in WBLogic.F_mu_ref.binary.rules]
mapstoS_combine [in WBLogic.F_mu_ref.binary.rules]
mapstoS_agree [in WBLogic.F_mu_ref.binary.rules]
mapsto_persist [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_ne [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_frac_ne [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_combine [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_agree [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_valid_2 [in WBLogic.heap_lang_trace.primitive_laws]
mapsto_valid [in WBLogic.heap_lang_trace.primitive_laws]
module_invariance [in WBLogic.heap_lang_trace.adequacy]
N
new_pending [in WBLogic.oneshot]nsteps_inv_r [in WBLogic.F_mu_ref.binary.rules]
P
persistent_pred_ext [in WBLogic.persistent_pred]prefix_snoc_inv [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
prim_step_to_val_is_head_step [in WBLogic.heap_lang_trace.lang]
R
related_public_states [in WBLogic.program_logic.lib.sts]related_public_trans [in WBLogic.program_logic.lib.sts]
related_private_public [in WBLogic.program_logic.lib.sts]
resolve_reducible [in WBLogic.heap_lang_trace.primitive_laws]
S
sem_typed_store [in WBLogic.F_mu_ref.unary.fundamental]sem_typed_load [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_alloc [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unfold [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_fold [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unpack [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_pack [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_tapp [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_tlam [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_app [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_seq [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_letin [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_lam [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_rec [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_if [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_case [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_injr [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_injl [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_snd [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_fst [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_pair [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_nat_binop [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_bool [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_nat [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_unit [in WBLogic.F_mu_ref.unary.fundamental]
sem_typed_var [in WBLogic.F_mu_ref.unary.fundamental]
sequential_trace_alt_iff [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_of_sequential [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_prefix [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_with_opened_nil [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_app [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_open_front [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_sequential [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_call_middle [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_call [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
shoot [in WBLogic.oneshot]
shot_not_pending [in WBLogic.oneshot]
soundness [in WBLogic.F_mu_ref.unary.soundness]
steps_lb_le [in WBLogic.heap_lang_trace.primitive_laws]
steps_auth_update_S [in WBLogic.heap_lang_trace.primitive_laws]
steps_auth_update [in WBLogic.heap_lang_trace.primitive_laws]
steps_lb_get [in WBLogic.heap_lang_trace.primitive_laws]
steps_lb_valid [in WBLogic.heap_lang_trace.primitive_laws]
step_resolve [in WBLogic.heap_lang_trace.primitive_laws]
step_nat_binop [in WBLogic.F_mu_ref.binary.rules]
step_if_true [in WBLogic.F_mu_ref.binary.rules]
step_if_false [in WBLogic.F_mu_ref.binary.rules]
step_case_inr [in WBLogic.F_mu_ref.binary.rules]
step_case_inl [in WBLogic.F_mu_ref.binary.rules]
step_snd [in WBLogic.F_mu_ref.binary.rules]
step_fst [in WBLogic.F_mu_ref.binary.rules]
step_pack [in WBLogic.F_mu_ref.binary.rules]
step_fold [in WBLogic.F_mu_ref.binary.rules]
step_tlam [in WBLogic.F_mu_ref.binary.rules]
step_seq [in WBLogic.F_mu_ref.binary.rules]
step_letin [in WBLogic.F_mu_ref.binary.rules]
step_lam [in WBLogic.F_mu_ref.binary.rules]
step_rec [in WBLogic.F_mu_ref.binary.rules]
step_store [in WBLogic.F_mu_ref.binary.rules]
step_load [in WBLogic.F_mu_ref.binary.rules]
step_alloc [in WBLogic.F_mu_ref.binary.rules]
step_pure' [in WBLogic.F_mu_ref.binary.rules]
step_insert_no_fork [in WBLogic.F_mu_ref.binary.rules]
step_insert [in WBLogic.F_mu_ref.binary.rules]
sts_make_undo_private_trans [in WBLogic.program_logic.lib.sts]
sts_make_private_trans [in WBLogic.program_logic.lib.sts]
sts_make_public_trans [in WBLogic.program_logic.lib.sts]
sts_configs_pub_related [in WBLogic.program_logic.lib.sts]
sts_configs_update_frag [in WBLogic.program_logic.lib.sts]
T
tac_wbwp_faa [in WBLogic.heap_lang.proofmode]tac_wbwp_cmpxchg_suc [in WBLogic.heap_lang.proofmode]
tac_wbwp_cmpxchg_fail [in WBLogic.heap_lang.proofmode]
tac_wbwp_cmpxchg [in WBLogic.heap_lang.proofmode]
tac_wbwp_xchg [in WBLogic.heap_lang.proofmode]
tac_wbwp_store [in WBLogic.heap_lang.proofmode]
tac_wbwp_load [in WBLogic.heap_lang.proofmode]
tac_wbwp_free [in WBLogic.heap_lang.proofmode]
tac_wbwp_alloc [in WBLogic.heap_lang.proofmode]
tac_wbwp_allocN [in WBLogic.heap_lang.proofmode]
tac_wbwp_bind [in WBLogic.heap_lang.proofmode]
tac_wbwp_value [in WBLogic.heap_lang.proofmode]
tac_wbwp_value_nofupd [in WBLogic.heap_lang.proofmode]
tac_wbwp_pure_credit [in WBLogic.heap_lang.proofmode]
tac_wbwp_pure [in WBLogic.heap_lang.proofmode]
tac_wbwp_expr_eval [in WBLogic.heap_lang.proofmode]
tac_wbwp_faa [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg_suc [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg_fail [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_cmpxchg [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_xchg [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_store [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_load [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_free [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_alloc [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_bind [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_value [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_value_nofupd [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_pure_credit [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_pure [in WBLogic.heap_lang_trace.proofmode]
tac_wbwp_expr_eval [in WBLogic.heap_lang_trace.proofmode]
tac_twp_faa [in WBLogic.heap_lang_trace.proofmode]
tac_wp_faa [in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg_suc [in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg_suc [in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg_fail [in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg_fail [in WBLogic.heap_lang_trace.proofmode]
tac_twp_cmpxchg [in WBLogic.heap_lang_trace.proofmode]
tac_wp_cmpxchg [in WBLogic.heap_lang_trace.proofmode]
tac_twp_xchg [in WBLogic.heap_lang_trace.proofmode]
tac_wp_xchg [in WBLogic.heap_lang_trace.proofmode]
tac_twp_store [in WBLogic.heap_lang_trace.proofmode]
tac_wp_store [in WBLogic.heap_lang_trace.proofmode]
tac_twp_load [in WBLogic.heap_lang_trace.proofmode]
tac_wp_load [in WBLogic.heap_lang_trace.proofmode]
tac_twp_free [in WBLogic.heap_lang_trace.proofmode]
tac_wp_free [in WBLogic.heap_lang_trace.proofmode]
tac_twp_alloc [in WBLogic.heap_lang_trace.proofmode]
tac_wp_alloc [in WBLogic.heap_lang_trace.proofmode]
tac_twp_bind [in WBLogic.heap_lang_trace.proofmode]
tac_wp_bind [in WBLogic.heap_lang_trace.proofmode]
tac_twp_value [in WBLogic.heap_lang_trace.proofmode]
tac_wp_value [in WBLogic.heap_lang_trace.proofmode]
tac_twp_value_nofupd [in WBLogic.heap_lang_trace.proofmode]
tac_wp_value_nofupd [in WBLogic.heap_lang_trace.proofmode]
tac_wp_pure_credit [in WBLogic.heap_lang_trace.proofmode]
tac_twp_pure [in WBLogic.heap_lang_trace.proofmode]
tac_wp_pure [in WBLogic.heap_lang_trace.proofmode]
tac_twp_expr_eval [in WBLogic.heap_lang_trace.proofmode]
tac_wp_expr_eval [in WBLogic.heap_lang_trace.proofmode]
to_heap_insert [in WBLogic.F_mu_ref.binary.rules]
to_tpool_snoc [in WBLogic.F_mu_ref.binary.rules]
to_tpool_insert' [in WBLogic.F_mu_ref.binary.rules]
to_tpool_insert [in WBLogic.F_mu_ref.binary.rules]
to_tpool_valid [in WBLogic.F_mu_ref.binary.rules]
to_val_fill_some [in WBLogic.heap_lang_trace.lang]
tpool_singleton_included' [in WBLogic.F_mu_ref.binary.rules]
tpool_singleton_included [in WBLogic.F_mu_ref.binary.rules]
tpool_lookup_Some [in WBLogic.F_mu_ref.binary.rules]
tpool_lookup [in WBLogic.F_mu_ref.binary.rules]
trace_auth_init [in WBLogic.heap_lang_trace.trace_resources]
trace_is_inv [in WBLogic.heap_lang_trace.trace_resources]
trace_add_event [in WBLogic.heap_lang_trace.trace_resources]
trace_half_frag_agree [in WBLogic.heap_lang_trace.trace_resources]
trace_agree [in WBLogic.heap_lang_trace.trace_resources]
trace_auth_half_frag_agree [in WBLogic.heap_lang_trace.trace_resources]
twp_faa [in WBLogic.heap_lang_trace.primitive_laws]
twp_cmpxchg_suc [in WBLogic.heap_lang_trace.primitive_laws]
twp_cmpxchg_fail [in WBLogic.heap_lang_trace.primitive_laws]
twp_xchg [in WBLogic.heap_lang_trace.primitive_laws]
twp_store [in WBLogic.heap_lang_trace.primitive_laws]
twp_load [in WBLogic.heap_lang_trace.primitive_laws]
twp_free [in WBLogic.heap_lang_trace.primitive_laws]
twp_alloc [in WBLogic.heap_lang_trace.primitive_laws]
twp_allocN_seq [in WBLogic.heap_lang_trace.primitive_laws]
twp_fork [in WBLogic.heap_lang_trace.primitive_laws]
typed_n_closed [in WBLogic.F_mu_ref.typing]
typed_ctx_n_closed [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_typed [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_typed [in WBLogic.F_mu_ref.binary.context_refinement]
type_soundness [in WBLogic.F_mu_ref.unary.soundness]
V
very_awkward_self_apply_safe [in WBLogic.F_mu_ref.unary.examples.very_awkward]very_awkward_self_apply_sem_typed [in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_sem_typed [in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_typed [in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward_self_apply_returns_one [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward_call_twice_return_one_ctx_equiv [in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_call_twice_return_one_refinement [in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_typed [in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward_self_apply_returns_one [in WBLogic.heap_lang_examples.very_awkward]
very_awkward_self_apply_returns_one [in WBLogic.heap_lang_examples.sts.very_awkward]
W
wbwp_invariance [in WBLogic.program_logic.adequacy]wbwp_adequacy [in WBLogic.program_logic.adequacy]
wbwp_strong_adequacy [in WBLogic.program_logic.adequacy]
wbwp_pure_step_later [in WBLogic.program_logic.lifting]
wbwp_pure_step_fupd [in WBLogic.program_logic.lifting]
wbwp_resolve_cmpxchg_fail [in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve_cmpxchg_suc [in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve_proph [in WBLogic.heap_lang_trace.derived_laws]
wbwp_faa_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_faa_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_fail_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_fail_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_suc_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_cmpxchg_suc_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_xchg_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_xchg_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_store_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_store_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_load_offset_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_load_offset [in WBLogic.heap_lang_trace.derived_laws]
wbwp_allocN_vec [in WBLogic.heap_lang_trace.derived_laws]
wbwp_allocN [in WBLogic.heap_lang_trace.derived_laws]
wbwp_resolve [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_fresh [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_emit [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_new_proph [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_faa [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_cmpxchg_suc [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_cmpxchg_fail [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_xchg [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_store [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_load [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_free [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_alloc [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_allocN_seq [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_rec_löb [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_step_fupdN_lb [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_lb_update [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_lb_init [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_resolve [in WBLogic.heap_lang.primitive_laws]
wbwp_new_proph [in WBLogic.heap_lang.primitive_laws]
wbwp_faa [in WBLogic.heap_lang.primitive_laws]
wbwp_cmpxchg_suc [in WBLogic.heap_lang.primitive_laws]
wbwp_cmpxchg_fail [in WBLogic.heap_lang.primitive_laws]
wbwp_xchg [in WBLogic.heap_lang.primitive_laws]
wbwp_store [in WBLogic.heap_lang.primitive_laws]
wbwp_load [in WBLogic.heap_lang.primitive_laws]
wbwp_free [in WBLogic.heap_lang.primitive_laws]
wbwp_alloc [in WBLogic.heap_lang.primitive_laws]
wbwp_allocN_seq [in WBLogic.heap_lang.primitive_laws]
wbwp_step_fupdN_lb [in WBLogic.heap_lang.primitive_laws]
wbwp_lb_update [in WBLogic.heap_lang.primitive_laws]
wbwp_lb_init [in WBLogic.heap_lang.primitive_laws]
wbwp_very_akward_call_fact_across_returns_one [in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_akward_call_fact_across [in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_awkward_self_apply [in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_very_awkward [in WBLogic.heap_lang_trace_examples.very_awkward]
wbwp_awkward_self_apply [in WBLogic.heap_lang_examples.awkward]
wbwp_awkward [in WBLogic.heap_lang_examples.awkward]
wbwp_very_akward_call_fact_across_returns_one [in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_akward_call_fact_across [in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_awkward_self_apply [in WBLogic.heap_lang_examples.very_awkward]
wbwp_very_awkward [in WBLogic.heap_lang_examples.very_awkward]
wbwp_wand_r [in WBLogic.program_logic.weakestpre]
wbwp_wand_l [in WBLogic.program_logic.weakestpre]
wbwp_wand [in WBLogic.program_logic.weakestpre]
wbwp_frame_step_r' [in WBLogic.program_logic.weakestpre]
wbwp_frame_step_l' [in WBLogic.program_logic.weakestpre]
wbwp_frame_step_r [in WBLogic.program_logic.weakestpre]
wbwp_frame_step_l [in WBLogic.program_logic.weakestpre]
wbwp_step_fupd [in WBLogic.program_logic.weakestpre]
wbwp_step_fupdN [in WBLogic.program_logic.weakestpre]
wbwp_frame_r [in WBLogic.program_logic.weakestpre]
wbwp_frame_l [in WBLogic.program_logic.weakestpre]
wbwp_value [in WBLogic.program_logic.weakestpre]
wbwp_value' [in WBLogic.program_logic.weakestpre]
wbwp_value_fupd [in WBLogic.program_logic.weakestpre]
wbwp_mono [in WBLogic.program_logic.weakestpre]
wbwp_bind [in WBLogic.program_logic.weakestpre]
wbwp_step_fupdN_strong [in WBLogic.program_logic.weakestpre]
wbwp_credit_access [in WBLogic.program_logic.weakestpre]
wbwp_fupd [in WBLogic.program_logic.weakestpre]
wbwp_make_gstack [in WBLogic.program_logic.weakestpre]
wbwp_mend [in WBLogic.program_logic.weakestpre]
wbwp_get_gstack_full [in WBLogic.program_logic.weakestpre]
wbwp_strong_mono [in WBLogic.program_logic.weakestpre]
wbwp_value_fupd' [in WBLogic.program_logic.weakestpre]
wbwp_store [in WBLogic.F_mu_ref.wp_rules]
wbwp_load [in WBLogic.F_mu_ref.wp_rules]
wbwp_alloc [in WBLogic.F_mu_ref.wp_rules]
wbwp_resolve_cmpxchg_fail [in WBLogic.heap_lang.derived_laws]
wbwp_resolve_cmpxchg_suc [in WBLogic.heap_lang.derived_laws]
wbwp_resolve_proph [in WBLogic.heap_lang.derived_laws]
wbwp_faa_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_faa_offset [in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_fail_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_fail_offset [in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_suc_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_cmpxchg_suc_offset [in WBLogic.heap_lang.derived_laws]
wbwp_xchg_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_xchg_offset [in WBLogic.heap_lang.derived_laws]
wbwp_store_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_store_offset [in WBLogic.heap_lang.derived_laws]
wbwp_load_offset_vec [in WBLogic.heap_lang.derived_laws]
wbwp_load_offset [in WBLogic.heap_lang.derived_laws]
wbwp_allocN_vec [in WBLogic.heap_lang.derived_laws]
wbwp_allocN [in WBLogic.heap_lang.derived_laws]
wbwp_sts_mend [in WBLogic.program_logic.lib.sts]
wbwp_sts_get_state [in WBLogic.program_logic.lib.sts]
wbwp_very_awkward_self_apply [in WBLogic.heap_lang_examples.sts.very_awkward]
wbwp_very_awkward [in WBLogic.heap_lang_examples.sts.very_awkward]
wb_mask_mono [in WBLogic.program_logic.weakestpre]
wp_resolve [in WBLogic.heap_lang_trace.primitive_laws]
wp_new_proph [in WBLogic.heap_lang_trace.primitive_laws]
wp_faa [in WBLogic.heap_lang_trace.primitive_laws]
wp_cmpxchg_suc [in WBLogic.heap_lang_trace.primitive_laws]
wp_cmpxchg_fail [in WBLogic.heap_lang_trace.primitive_laws]
wp_xchg [in WBLogic.heap_lang_trace.primitive_laws]
wp_store [in WBLogic.heap_lang_trace.primitive_laws]
wp_load [in WBLogic.heap_lang_trace.primitive_laws]
wp_free [in WBLogic.heap_lang_trace.primitive_laws]
wp_alloc [in WBLogic.heap_lang_trace.primitive_laws]
wp_allocN_seq [in WBLogic.heap_lang_trace.primitive_laws]
wp_fork [in WBLogic.heap_lang_trace.primitive_laws]
wp_fresh [in WBLogic.heap_lang_trace.primitive_laws]
wp_emit [in WBLogic.heap_lang_trace.primitive_laws]
wp_rec_löb [in WBLogic.heap_lang_trace.primitive_laws]
wp_step_fupdN_lb [in WBLogic.heap_lang_trace.primitive_laws]
wp_lb_update [in WBLogic.heap_lang_trace.primitive_laws]
wp_lb_init [in WBLogic.heap_lang_trace.primitive_laws]
wp_rec_löb [in WBLogic.heap_lang.primitive_laws]
wp_call_fact_across [in WBLogic.heap_lang_trace_examples.very_awkward]
wp_factorial [in WBLogic.heap_lang_trace_examples.very_awkward]
wp_call_fact_across [in WBLogic.heap_lang_examples.very_awkward]
wp_factorial [in WBLogic.heap_lang_examples.very_awkward]
wp_frame_wand [in WBLogic.program_logic.weakestpre]
wp_wbwp [in WBLogic.program_logic.weakestpre]
wp_atomic [in WBLogic.program_logic.weakestpre]
wp_store [in WBLogic.F_mu_ref.wp_rules]
wp_load [in WBLogic.F_mu_ref.wp_rules]
wp_alloc [in WBLogic.F_mu_ref.wp_rules]
wrap_very_awk_correct [in WBLogic.heap_lang_trace_examples.very_awkward]
Wrap.correct [in WBLogic.heap_lang_trace_examples.very_awkward]
Constructor Index
A
App_typed [in WBLogic.F_mu_ref.typing]as_recv [in WBLogic.heap_lang_trace.class_instances]
B
BinOp_typed [in WBLogic.F_mu_ref.typing]Bool_typed [in WBLogic.F_mu_ref.typing]
C
Case_typed [in WBLogic.F_mu_ref.typing]CTX_StoreR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_StoreL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Load [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Alloc [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_TApp [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_TLam [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Unfold [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Fold [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfM [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_IfL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_BinOpR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_BinOpL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseM [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_CaseL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_InjR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_InjL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Snd [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Fst [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_PairR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_PairL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_AppR [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_AppL [in WBLogic.F_mu_ref.binary.context_refinement]
CTX_Rec [in WBLogic.F_mu_ref.binary.context_refinement]
F
Fst_typed [in WBLogic.F_mu_ref.typing]F_mu_ref.StoreS [in WBLogic.F_mu_ref.lang]
F_mu_ref.LoadS [in WBLogic.F_mu_ref.lang]
F_mu_ref.AllocS [in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackS [in WBLogic.F_mu_ref.lang]
F_mu_ref.TBeta [in WBLogic.F_mu_ref.lang]
F_mu_ref.Unfold_Fold [in WBLogic.F_mu_ref.lang]
F_mu_ref.IfTrue [in WBLogic.F_mu_ref.lang]
F_mu_ref.IfFalse [in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpS [in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseRS [in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseLS [in WBLogic.F_mu_ref.lang]
F_mu_ref.SndS [in WBLogic.F_mu_ref.lang]
F_mu_ref.FstS [in WBLogic.F_mu_ref.lang]
F_mu_ref.SeqBetaS [in WBLogic.F_mu_ref.lang]
F_mu_ref.LetInBetaS [in WBLogic.F_mu_ref.lang]
F_mu_ref.LamBetaS [in WBLogic.F_mu_ref.lang]
F_mu_ref.BetaS [in WBLogic.F_mu_ref.lang]
F_mu_ref.StoreRCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.StoreLCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.LoadCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.AllocCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.UnfoldCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.FoldCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.IfCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.CaseCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjRCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjLCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.SndCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.FstCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpRCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOpLCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.PairRCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.PairLCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackInCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.PackCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.TAppCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.SeqCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.LetInCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.AppRCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.AppLCtx [in WBLogic.F_mu_ref.lang]
F_mu_ref.LocV [in WBLogic.F_mu_ref.lang]
F_mu_ref.FoldV [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjRV [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjLV [in WBLogic.F_mu_ref.lang]
F_mu_ref.PairV [in WBLogic.F_mu_ref.lang]
F_mu_ref.BoolV [in WBLogic.F_mu_ref.lang]
F_mu_ref.NatV [in WBLogic.F_mu_ref.lang]
F_mu_ref.UnitV [in WBLogic.F_mu_ref.lang]
F_mu_ref.PackV [in WBLogic.F_mu_ref.lang]
F_mu_ref.TLamV [in WBLogic.F_mu_ref.lang]
F_mu_ref.LamV [in WBLogic.F_mu_ref.lang]
F_mu_ref.RecV [in WBLogic.F_mu_ref.lang]
F_mu_ref.Store [in WBLogic.F_mu_ref.lang]
F_mu_ref.Load [in WBLogic.F_mu_ref.lang]
F_mu_ref.Alloc [in WBLogic.F_mu_ref.lang]
F_mu_ref.Loc [in WBLogic.F_mu_ref.lang]
F_mu_ref.UnpackIn [in WBLogic.F_mu_ref.lang]
F_mu_ref.Pack [in WBLogic.F_mu_ref.lang]
F_mu_ref.TApp [in WBLogic.F_mu_ref.lang]
F_mu_ref.TLam [in WBLogic.F_mu_ref.lang]
F_mu_ref.Unfold [in WBLogic.F_mu_ref.lang]
F_mu_ref.Fold [in WBLogic.F_mu_ref.lang]
F_mu_ref.Case [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjR [in WBLogic.F_mu_ref.lang]
F_mu_ref.InjL [in WBLogic.F_mu_ref.lang]
F_mu_ref.Snd [in WBLogic.F_mu_ref.lang]
F_mu_ref.Fst [in WBLogic.F_mu_ref.lang]
F_mu_ref.Pair [in WBLogic.F_mu_ref.lang]
F_mu_ref.If [in WBLogic.F_mu_ref.lang]
F_mu_ref.BinOp [in WBLogic.F_mu_ref.lang]
F_mu_ref.Bool [in WBLogic.F_mu_ref.lang]
F_mu_ref.Nat [in WBLogic.F_mu_ref.lang]
F_mu_ref.Unit [in WBLogic.F_mu_ref.lang]
F_mu_ref.Seq [in WBLogic.F_mu_ref.lang]
F_mu_ref.LetIn [in WBLogic.F_mu_ref.lang]
F_mu_ref.Lam [in WBLogic.F_mu_ref.lang]
F_mu_ref.App [in WBLogic.F_mu_ref.lang]
F_mu_ref.Rec [in WBLogic.F_mu_ref.lang]
F_mu_ref.Var [in WBLogic.F_mu_ref.lang]
F_mu_ref.Lt [in WBLogic.F_mu_ref.lang]
F_mu_ref.Le [in WBLogic.F_mu_ref.lang]
F_mu_ref.Eq [in WBLogic.F_mu_ref.lang]
F_mu_ref.Mult [in WBLogic.F_mu_ref.lang]
F_mu_ref.Sub [in WBLogic.F_mu_ref.lang]
F_mu_ref.Add [in WBLogic.F_mu_ref.lang]
H
heap_lang.FreshS [in WBLogic.heap_lang_trace.lang]heap_lang.EmitS [in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveS [in WBLogic.heap_lang_trace.lang]
heap_lang.NewProphS [in WBLogic.heap_lang_trace.lang]
heap_lang.ForkS [in WBLogic.heap_lang_trace.lang]
heap_lang.FaaS [in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgS [in WBLogic.heap_lang_trace.lang]
heap_lang.XchgS [in WBLogic.heap_lang_trace.lang]
heap_lang.StoreS [in WBLogic.heap_lang_trace.lang]
heap_lang.LoadS [in WBLogic.heap_lang_trace.lang]
heap_lang.FreeS [in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNS [in WBLogic.heap_lang_trace.lang]
heap_lang.CaseRS [in WBLogic.heap_lang_trace.lang]
heap_lang.CaseLS [in WBLogic.heap_lang_trace.lang]
heap_lang.SndS [in WBLogic.heap_lang_trace.lang]
heap_lang.FstS [in WBLogic.heap_lang_trace.lang]
heap_lang.IfFalseS [in WBLogic.heap_lang_trace.lang]
heap_lang.IfTrueS [in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpS [in WBLogic.heap_lang_trace.lang]
heap_lang.UnOpS [in WBLogic.heap_lang_trace.lang]
heap_lang.BetaS [in WBLogic.heap_lang_trace.lang]
heap_lang.InjRS [in WBLogic.heap_lang_trace.lang]
heap_lang.InjLS [in WBLogic.heap_lang_trace.lang]
heap_lang.PairS [in WBLogic.heap_lang_trace.lang]
heap_lang.RecS [in WBLogic.heap_lang_trace.lang]
heap_lang.FreshCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.EmitCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveMCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.ResolveLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.FaaRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.FaaLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgMCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchgLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.XchgRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.XchgLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.StoreRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.StoreLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.LoadCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.FreeCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.AllocNLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.CaseCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.InjRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.InjLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.SndCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.FstCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.PairRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.PairLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.IfCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.BinOpLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.UnOpCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.AppRCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.AppLCtx [in WBLogic.heap_lang_trace.lang]
heap_lang.InjRV [in WBLogic.heap_lang_trace.lang]
heap_lang.InjLV [in WBLogic.heap_lang_trace.lang]
heap_lang.PairV [in WBLogic.heap_lang_trace.lang]
heap_lang.RecV [in WBLogic.heap_lang_trace.lang]
heap_lang.LitV [in WBLogic.heap_lang_trace.lang]
heap_lang.Fresh [in WBLogic.heap_lang_trace.lang]
heap_lang.Emit [in WBLogic.heap_lang_trace.lang]
heap_lang.Resolve [in WBLogic.heap_lang_trace.lang]
heap_lang.NewProph [in WBLogic.heap_lang_trace.lang]
heap_lang.Fork [in WBLogic.heap_lang_trace.lang]
heap_lang.FAA [in WBLogic.heap_lang_trace.lang]
heap_lang.Xchg [in WBLogic.heap_lang_trace.lang]
heap_lang.CmpXchg [in WBLogic.heap_lang_trace.lang]
heap_lang.Store [in WBLogic.heap_lang_trace.lang]
heap_lang.Load [in WBLogic.heap_lang_trace.lang]
heap_lang.Free [in WBLogic.heap_lang_trace.lang]
heap_lang.AllocN [in WBLogic.heap_lang_trace.lang]
heap_lang.Case [in WBLogic.heap_lang_trace.lang]
heap_lang.InjR [in WBLogic.heap_lang_trace.lang]
heap_lang.InjL [in WBLogic.heap_lang_trace.lang]
heap_lang.Snd [in WBLogic.heap_lang_trace.lang]
heap_lang.Fst [in WBLogic.heap_lang_trace.lang]
heap_lang.Pair [in WBLogic.heap_lang_trace.lang]
heap_lang.If [in WBLogic.heap_lang_trace.lang]
heap_lang.BinOp [in WBLogic.heap_lang_trace.lang]
heap_lang.UnOp [in WBLogic.heap_lang_trace.lang]
heap_lang.App [in WBLogic.heap_lang_trace.lang]
heap_lang.Rec [in WBLogic.heap_lang_trace.lang]
heap_lang.Var [in WBLogic.heap_lang_trace.lang]
heap_lang.Val [in WBLogic.heap_lang_trace.lang]
heap_lang.OffsetOp [in WBLogic.heap_lang_trace.lang]
heap_lang.EqOp [in WBLogic.heap_lang_trace.lang]
heap_lang.LtOp [in WBLogic.heap_lang_trace.lang]
heap_lang.LeOp [in WBLogic.heap_lang_trace.lang]
heap_lang.ShiftROp [in WBLogic.heap_lang_trace.lang]
heap_lang.ShiftLOp [in WBLogic.heap_lang_trace.lang]
heap_lang.XorOp [in WBLogic.heap_lang_trace.lang]
heap_lang.OrOp [in WBLogic.heap_lang_trace.lang]
heap_lang.AndOp [in WBLogic.heap_lang_trace.lang]
heap_lang.RemOp [in WBLogic.heap_lang_trace.lang]
heap_lang.QuotOp [in WBLogic.heap_lang_trace.lang]
heap_lang.MultOp [in WBLogic.heap_lang_trace.lang]
heap_lang.MinusOp [in WBLogic.heap_lang_trace.lang]
heap_lang.PlusOp [in WBLogic.heap_lang_trace.lang]
heap_lang.MinusUnOp [in WBLogic.heap_lang_trace.lang]
heap_lang.NegOp [in WBLogic.heap_lang_trace.lang]
heap_lang.LitProphecy [in WBLogic.heap_lang_trace.lang]
heap_lang.LitTag [in WBLogic.heap_lang_trace.lang]
heap_lang.LitLoc [in WBLogic.heap_lang_trace.lang]
heap_lang.LitPoison [in WBLogic.heap_lang_trace.lang]
heap_lang.LitUnit [in WBLogic.heap_lang_trace.lang]
heap_lang.LitBool [in WBLogic.heap_lang_trace.lang]
heap_lang.LitInt [in WBLogic.heap_lang_trace.lang]
I
If_typed [in WBLogic.F_mu_ref.typing]InjL_typed [in WBLogic.F_mu_ref.typing]
InjR_typed [in WBLogic.F_mu_ref.typing]
L
Lam_typed [in WBLogic.F_mu_ref.typing]LetIn_typed [in WBLogic.F_mu_ref.typing]
N
Nat_typed [in WBLogic.F_mu_ref.typing]P
Pack_typed [in WBLogic.F_mu_ref.typing]Pair_typed [in WBLogic.F_mu_ref.typing]
R
Rec_typed [in WBLogic.F_mu_ref.typing]S
sequential_full_trace_app [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]sequential_full_trace_wrap [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_nil [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_with_opened_close [in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_open [in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_nil [in WBLogic.heap_lang_trace_examples.very_awkward]
Seq_typed [in WBLogic.F_mu_ref.typing]
Snd_typed [in WBLogic.F_mu_ref.typing]
T
TAlloc [in WBLogic.F_mu_ref.typing]TApp_typed [in WBLogic.F_mu_ref.typing]
TArrow [in WBLogic.F_mu_ref.typing]
TBool [in WBLogic.F_mu_ref.typing]
TExist [in WBLogic.F_mu_ref.typing]
TFold [in WBLogic.F_mu_ref.typing]
TForall [in WBLogic.F_mu_ref.typing]
TLam_typed [in WBLogic.F_mu_ref.typing]
TLoad [in WBLogic.F_mu_ref.typing]
TNat [in WBLogic.F_mu_ref.typing]
TPCTX_cons [in WBLogic.F_mu_ref.binary.context_refinement]
TPCTX_nil [in WBLogic.F_mu_ref.binary.context_refinement]
TPCTX_Alloc [in WBLogic.F_mu_ref.binary.context_refinement]
TProd [in WBLogic.F_mu_ref.typing]
TP_CTX_StoreR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_StoreL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Load [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_TApp [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_TLam [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Unfold [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Fold [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_BinOpR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_BinOpL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfM [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_IfL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseM [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_CaseL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_InjR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_InjL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Snd [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Fst [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_PairR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_PairL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_AppR [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_AppL [in WBLogic.F_mu_ref.binary.context_refinement]
TP_CTX_Rec [in WBLogic.F_mu_ref.binary.context_refinement]
TRec [in WBLogic.F_mu_ref.typing]
Tref [in WBLogic.F_mu_ref.typing]
TStore [in WBLogic.F_mu_ref.typing]
TSum [in WBLogic.F_mu_ref.typing]
TUnfold [in WBLogic.F_mu_ref.typing]
TUnit [in WBLogic.F_mu_ref.typing]
TVar [in WBLogic.F_mu_ref.typing]
U
Unit_typed [in WBLogic.F_mu_ref.typing]UnpackIn_typed [in WBLogic.F_mu_ref.typing]
V
Var_typed [in WBLogic.F_mu_ref.typing]Inductive Index
A
AsRecV [in WBLogic.heap_lang_trace.class_instances]C
ctx_item [in WBLogic.F_mu_ref.binary.context_refinement]F
F_mu_ref.head_step [in WBLogic.F_mu_ref.lang]F_mu_ref.ectx_item [in WBLogic.F_mu_ref.lang]
F_mu_ref.val [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop [in WBLogic.F_mu_ref.lang]
H
heap_lang.head_step [in WBLogic.heap_lang_trace.lang]heap_lang.ectx_item [in WBLogic.heap_lang_trace.lang]
heap_lang.val [in WBLogic.heap_lang_trace.lang]
heap_lang.expr [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit [in WBLogic.heap_lang_trace.lang]
S
sequential_full_trace [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]sequential_with_opened [in WBLogic.heap_lang_trace_examples.very_awkward]
T
type [in WBLogic.F_mu_ref.typing]typed [in WBLogic.F_mu_ref.typing]
typed_ctx [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item [in WBLogic.F_mu_ref.binary.context_refinement]
Projection Index
A
as_recv [in WBLogic.heap_lang_trace.class_instances]C
cfg_name [in WBLogic.F_mu_ref.binary.rules]cfg_inG [in WBLogic.F_mu_ref.binary.rules]
G
gstacksGpre_ing [in WBLogic.program_logic.ghost_stacks]gstacksGpre_dom_ing [in WBLogic.program_logic.ghost_stacks]
gstacks_name [in WBLogic.program_logic.ghost_stacks]
gstacks_ing [in WBLogic.program_logic.ghost_stacks]
gstacks_dom_ing [in WBLogic.program_logic.ghost_stacks]
H
heapI_gstacksIG [in WBLogic.F_mu_ref.wp_rules]heapI_gen_heapG [in WBLogic.F_mu_ref.wp_rules]
heapI_invG [in WBLogic.F_mu_ref.wp_rules]
heap_lang.used_proph_id [in WBLogic.heap_lang_trace.lang]
heap_lang.trace [in WBLogic.heap_lang_trace.lang]
heap_lang.heap [in WBLogic.heap_lang_trace.lang]
O
oneshot_inG [in WBLogic.oneshot]P
pers_pred_persistent [in WBLogic.persistent_pred]pers_pred_car [in WBLogic.persistent_pred]
pri_rel_po [in WBLogic.program_logic.lib.sts]
pri_rel [in WBLogic.program_logic.lib.sts]
pub_pri_incl [in WBLogic.program_logic.lib.sts]
pub_rel_po [in WBLogic.program_logic.lib.sts]
pub_rel [in WBLogic.program_logic.lib.sts]
S
soundness_unary_preG_reg [in WBLogic.F_mu_ref.unary.soundness]soundness_unary_preG_heap [in WBLogic.F_mu_ref.unary.soundness]
soundness_unary_preG_iris [in WBLogic.F_mu_ref.unary.soundness]
state_inh [in WBLogic.program_logic.lib.sts]
STS_state [in WBLogic.program_logic.lib.sts]
T
trace_preG_inG [in WBLogic.heap_lang_trace.trace_resources]trace_hist_preG_inG [in WBLogic.heap_lang_trace.trace_resources]
trace_name [in WBLogic.heap_lang_trace.trace_resources]
trace_inG [in WBLogic.heap_lang_trace.trace_resources]
trace_hist_name [in WBLogic.heap_lang_trace.trace_resources]
trace_hist_inG [in WBLogic.heap_lang_trace.trace_resources]
W
wbheapGpreS_trace [in WBLogic.heap_lang_trace.adequacy]wbheapGpreS_gstacks [in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_proph [in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_inv_heap [in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_heap [in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_iris [in WBLogic.heap_lang_trace.adequacy]
wbheapGpreS_gstacks [in WBLogic.heap_lang.adequacy]
wbheapGpreS_proph [in WBLogic.heap_lang.adequacy]
wbheapGpreS_inv_heap [in WBLogic.heap_lang.adequacy]
wbheapGpreS_heap [in WBLogic.heap_lang.adequacy]
wbheapGpreS_iris [in WBLogic.heap_lang.adequacy]
wbheapGS_traceGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_gstacksGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_step_cnt [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_step_name [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_proph_mapGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_inv_heapGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_gen_heapGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_invGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS_gstacksGS [in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_cnt [in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_name [in WBLogic.heap_lang.primitive_laws]
wbheapGS_proph_mapGS [in WBLogic.heap_lang.primitive_laws]
wbheapGS_inv_heapGS [in WBLogic.heap_lang.primitive_laws]
wbheapGS_gen_heapGS [in WBLogic.heap_lang.primitive_laws]
wbheapGS_invGS [in WBLogic.heap_lang.primitive_laws]
wbheapGS_step_cnt [in WBLogic.heap_lang_trace.adequacy]
wbheapGS_step_cnt [in WBLogic.heap_lang.adequacy]
Instance Index
A
add_modal_fupd_wbwp [in WBLogic.program_logic.weakestpre]alloc_atomic [in WBLogic.heap_lang_trace.class_instances]
as_val_val [in WBLogic.heap_lang_trace.class_instances]
B
beta_atomic [in WBLogic.heap_lang_trace.class_instances]binop_atomic [in WBLogic.heap_lang_trace.class_instances]
C
cmpxchg_atomic [in WBLogic.heap_lang_trace.class_instances]E
elim_acc_wbwp_nonatomic [in WBLogic.program_logic.weakestpre]elim_acc_wbwp_atomic [in WBLogic.program_logic.weakestpre]
elim_modal_fupd_wbwp_atomic [in WBLogic.program_logic.weakestpre]
elim_modal_fupd_wbwp [in WBLogic.program_logic.weakestpre]
elim_modal_bupd_wbwp [in WBLogic.program_logic.weakestpre]
emit_atomic [in WBLogic.heap_lang_trace.class_instances]
F
faa_atomic [in WBLogic.heap_lang_trace.class_instances]fork_atomic [in WBLogic.heap_lang_trace.class_instances]
frame_wbwp [in WBLogic.program_logic.weakestpre]
free_atomic [in WBLogic.heap_lang_trace.class_instances]
fresh_atomic [in WBLogic.heap_lang_trace.class_instances]
fst_atomic [in WBLogic.heap_lang_trace.class_instances]
F_mu_ref.fill_item_inj [in WBLogic.F_mu_ref.lang]
F_mu_ref.of_val_inj [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_inh [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_dec_eq [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_dec_eq [in WBLogic.F_mu_ref.lang]
F_mu_ref.SubstLemmas_expr [in WBLogic.F_mu_ref.lang]
F_mu_ref.Subst_expr [in WBLogic.F_mu_ref.lang]
F_mu_ref.Rename_expr [in WBLogic.F_mu_ref.lang]
F_mu_ref.Ids_expr [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_dec_eq [in WBLogic.F_mu_ref.lang]
F_mu_ref.loc_dec_eq [in WBLogic.F_mu_ref.lang]
G
gstacks_except_Timeless [in WBLogic.program_logic.ghost_stacks]gstacks_subΣ_inG [in WBLogic.program_logic.ghost_stacks]
gstack_exists_Persistent [in WBLogic.program_logic.ghost_stacks]
gstack_exists_Timeless [in WBLogic.program_logic.ghost_stacks]
gstack_full_Timeless [in WBLogic.program_logic.ghost_stacks]
gstack_frag_Timeless [in WBLogic.program_logic.ghost_stacks]
H
heapIG_irisG [in WBLogic.F_mu_ref.wp_rules]heapS_mapsto_timeless [in WBLogic.F_mu_ref.binary.rules]
heap_lang.fill_item_inj [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_inhabited [in WBLogic.heap_lang_trace.lang]
heap_lang.val_inhabited [in WBLogic.heap_lang_trace.lang]
heap_lang.state_inhabited [in WBLogic.heap_lang_trace.lang]
heap_lang.val_countable [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_countable [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_countable [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_finite [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_countable [in WBLogic.heap_lang_trace.lang]
heap_lang.val_eq_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_eq_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eq_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_eq_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_eq_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.of_val_inj [in WBLogic.heap_lang_trace.lang]
heap_lang.val_is_unboxed_dec [in WBLogic.heap_lang_trace.lang]
heap_lang.lit_is_unboxed_dec [in WBLogic.heap_lang_trace.lang]
hist_persistent [in WBLogic.heap_lang_trace.trace_resources]
I
Ids_type [in WBLogic.F_mu_ref.typing]if_false_atomic [in WBLogic.heap_lang_trace.class_instances]
if_true_atomic [in WBLogic.heap_lang_trace.class_instances]
inG_soundness_binaryΣ [in WBLogic.F_mu_ref.binary.soundness]
injl_atomic [in WBLogic.heap_lang_trace.class_instances]
injr_atomic [in WBLogic.heap_lang_trace.class_instances]
interp_env_persistent [in WBLogic.F_mu_ref.binary.logrel]
interp_env_base_persistent [in WBLogic.F_mu_ref.binary.logrel]
interp_rec1_contractive [in WBLogic.F_mu_ref.binary.logrel]
interp_expr_proper [in WBLogic.F_mu_ref.binary.logrel]
interp_expr_ne [in WBLogic.F_mu_ref.binary.logrel]
interp_env_persistent [in WBLogic.F_mu_ref.unary.logrel]
interp_env_base_persistent [in WBLogic.F_mu_ref.unary.logrel]
interp_rec1_contractive [in WBLogic.F_mu_ref.unary.logrel]
into_val_val [in WBLogic.heap_lang_trace.class_instances]
inv_mapsto_proper [in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own_proper [in WBLogic.heap_lang_trace.primitive_laws]
is_atomic_correct [in WBLogic.F_mu_ref.lang]
is_except_0_wbwp [in WBLogic.program_logic.weakestpre]
L
load_atomic [in WBLogic.heap_lang_trace.class_instances]N
new_proph_atomic [in WBLogic.heap_lang_trace.class_instances]P
pair_atomic [in WBLogic.heap_lang_trace.class_instances]persistent_pred_car_proper [in WBLogic.persistent_pred]
persistent_pred_car_ne [in WBLogic.persistent_pred]
persistent_pred_cofe [in WBLogic.persistent_pred]
persistent_pred_dist [in WBLogic.persistent_pred]
persistent_pred_equiv [in WBLogic.persistent_pred]
pure_case_inr [in WBLogic.heap_lang_trace.class_instances]
pure_case_inl [in WBLogic.heap_lang_trace.class_instances]
pure_snd [in WBLogic.heap_lang_trace.class_instances]
pure_fst [in WBLogic.heap_lang_trace.class_instances]
pure_if_false [in WBLogic.heap_lang_trace.class_instances]
pure_if_true [in WBLogic.heap_lang_trace.class_instances]
pure_eqop [in WBLogic.heap_lang_trace.class_instances]
pure_binop [in WBLogic.heap_lang_trace.class_instances]
pure_unop [in WBLogic.heap_lang_trace.class_instances]
pure_beta [in WBLogic.heap_lang_trace.class_instances]
pure_injrc [in WBLogic.heap_lang_trace.class_instances]
pure_injlc [in WBLogic.heap_lang_trace.class_instances]
pure_pairc [in WBLogic.heap_lang_trace.class_instances]
pure_recc [in WBLogic.heap_lang_trace.class_instances]
pure_case_inr [in WBLogic.F_mu_ref.wp_rules]
pure_case_inl [in WBLogic.F_mu_ref.wp_rules]
pure_snd [in WBLogic.F_mu_ref.wp_rules]
pure_fst [in WBLogic.F_mu_ref.wp_rules]
pure_fold [in WBLogic.F_mu_ref.wp_rules]
pure_pack [in WBLogic.F_mu_ref.wp_rules]
pure_tlam [in WBLogic.F_mu_ref.wp_rules]
pure_seq [in WBLogic.F_mu_ref.wp_rules]
pure_LetIn [in WBLogic.F_mu_ref.wp_rules]
pure_lam [in WBLogic.F_mu_ref.wp_rules]
pure_rec [in WBLogic.F_mu_ref.wp_rules]
R
rec_atomic [in WBLogic.heap_lang_trace.class_instances]Rename_type [in WBLogic.F_mu_ref.typing]
resolve_atomic [in WBLogic.heap_lang_trace.class_instances]
S
snd_atomic [in WBLogic.heap_lang_trace.class_instances]spec_ctx_persistent [in WBLogic.F_mu_ref.binary.rules]
store_atomic [in WBLogic.heap_lang_trace.class_instances]
subG_oneshotΣ [in WBLogic.oneshot]
subG_heapGpreS [in WBLogic.heap_lang_trace.adequacy]
subG_heapGpreS [in WBLogic.heap_lang.adequacy]
subG_tracePreG [in WBLogic.heap_lang_trace.trace_resources]
subG_STSΣ_ing [in WBLogic.program_logic.lib.sts]
SubstLemmas_typer [in WBLogic.F_mu_ref.typing]
Subst_type [in WBLogic.F_mu_ref.typing]
U
unop_atomic [in WBLogic.heap_lang_trace.class_instances]W
wbheapGS_heapGS [in WBLogic.heap_lang.primitive_laws]wbheapG_irisG [in WBLogic.heap_lang_trace.primitive_laws]
wbwp_flip_mono' [in WBLogic.program_logic.weakestpre]
wbwp_mono' [in WBLogic.program_logic.weakestpre]
wbwp_contractive [in WBLogic.program_logic.weakestpre]
wbwp_proper [in WBLogic.program_logic.weakestpre]
wbwp_ne [in WBLogic.program_logic.weakestpre]
wp_nat_binop [in WBLogic.F_mu_ref.wp_rules]
wp_if_false [in WBLogic.F_mu_ref.wp_rules]
wp_if_true [in WBLogic.F_mu_ref.wp_rules]
X
xchg_atomic [in WBLogic.heap_lang_trace.class_instances]Section Index
A
atomic [in WBLogic.heap_lang_trace.class_instances]Autosubst_Lemmas [in WBLogic.F_mu_ref.base]
awkward [in WBLogic.heap_lang_examples.awkward]
B
bin_log_related_under_typed_ctx [in WBLogic.F_mu_ref.binary.context_refinement]bin_log_def [in WBLogic.F_mu_ref.binary.fundamental]
C
cfg [in WBLogic.F_mu_ref.binary.rules]conversions [in WBLogic.F_mu_ref.binary.rules]
D
definitions [in WBLogic.heap_lang_trace.primitive_laws]definitionsS [in WBLogic.F_mu_ref.binary.rules]
F
fact_equiv [in WBLogic.F_mu_ref.binary.examples.fact]fundamental [in WBLogic.F_mu_ref.binary.fundamental]
G
ghost_stacks [in WBLogic.program_logic.ghost_stacks]H
heap [in WBLogic.heap_lang.proofmode]heap [in WBLogic.heap_lang_trace.proofmode]
heap [in WBLogic.heap_lang_trace.proofmode]
L
lang_rules [in WBLogic.F_mu_ref.wp_rules]lifting [in WBLogic.program_logic.lifting]
lifting [in WBLogic.heap_lang_trace.derived_laws]
lifting [in WBLogic.heap_lang_trace.primitive_laws]
lifting [in WBLogic.heap_lang.primitive_laws]
lifting [in WBLogic.heap_lang.derived_laws]
logrel [in WBLogic.F_mu_ref.binary.logrel]
logrel [in WBLogic.F_mu_ref.unary.logrel]
P
persistent_pred [in WBLogic.persistent_pred]proofmode_classes [in WBLogic.program_logic.weakestpre]
pure_exec [in WBLogic.heap_lang_trace.class_instances]
S
Spec [in WBLogic.heap_lang_trace_examples.very_awkward]steps [in WBLogic.heap_lang_trace.primitive_laws]
STS [in WBLogic.program_logic.lib.sts]
T
to_heap [in WBLogic.F_mu_ref.binary.rules]Trace [in WBLogic.heap_lang_trace_examples.very_awkward]
typed_interp [in WBLogic.F_mu_ref.unary.fundamental]
V
very_awkward [in WBLogic.F_mu_ref.unary.examples.very_awkward]very_awkward [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward [in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_awkward [in WBLogic.heap_lang_examples.very_awkward]
very_awkward [in WBLogic.heap_lang_examples.sts.very_awkward]
W
wp [in WBLogic.program_logic.weakestpre]Wrap.S [in WBLogic.heap_lang_trace_examples.very_awkward]
Abbreviation Index
A
Alloc [in WBLogic.heap_lang_trace.notation]C
CAS [in WBLogic.heap_lang_trace.notation]D
D [in WBLogic.F_mu_ref.binary.logrel]D [in WBLogic.F_mu_ref.unary.fundamental]
D [in WBLogic.F_mu_ref.unary.logrel]
D [in WBLogic.F_mu_ref.binary.fundamental]
D [in WBLogic.F_mu_ref.binary.fundamental]
H
heap_lang.of_val [in WBLogic.heap_lang_trace.lang]I
inv_heap_inv [in WBLogic.heap_lang_trace.primitive_laws]L
Lam [in WBLogic.heap_lang_trace.notation]LamV [in WBLogic.heap_lang_trace.notation]
Let [in WBLogic.heap_lang_trace.notation]
LetCtx [in WBLogic.heap_lang_trace.notation]
M
Match [in WBLogic.heap_lang_trace.notation]N
NONE [in WBLogic.heap_lang_trace.notation]NONEV [in WBLogic.heap_lang_trace.notation]
R
ResolveProph [in WBLogic.heap_lang_trace.notation]S
Seq [in WBLogic.heap_lang_trace.notation]SeqCtx [in WBLogic.heap_lang_trace.notation]
Skip [in WBLogic.heap_lang_trace.notation]
SOME [in WBLogic.heap_lang_trace.notation]
SOMEV [in WBLogic.heap_lang_trace.notation]
Definition Index
A
AsRecV_recv [in WBLogic.heap_lang_trace.class_instances]awkN [in WBLogic.heap_lang_trace_examples.very_awkward]
awkward [in WBLogic.heap_lang_examples.awkward]
awkward_self_apply [in WBLogic.heap_lang_examples.awkward]
B
binop_res_type [in WBLogic.F_mu_ref.typing]bin_log_related [in WBLogic.F_mu_ref.binary.fundamental]
C
call_fact_across [in WBLogic.heap_lang_trace_examples.very_awkward]call_twice_return_one [in WBLogic.F_mu_ref.binary.examples.very_awkward]
call_fact_across [in WBLogic.heap_lang_examples.very_awkward]
cfgUR [in WBLogic.F_mu_ref.binary.rules]
ctx [in WBLogic.F_mu_ref.binary.context_refinement]
ctx_lookup [in WBLogic.F_mu_ref.binary.logrel]
ctx_refines [in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_sind [in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_rec [in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_ind [in WBLogic.F_mu_ref.binary.context_refinement]
ctx_item_rect [in WBLogic.F_mu_ref.binary.context_refinement]
E
empty_state [in WBLogic.heap_lang_trace_examples.very_awkward]env_subst [in WBLogic.F_mu_ref.typing]
env_lookup [in WBLogic.F_mu_ref.unary.logrel]
eventO [in WBLogic.heap_lang_trace.trace_resources]
F
fact [in WBLogic.F_mu_ref.binary.examples.fact]factorial [in WBLogic.heap_lang_trace_examples.very_awkward]
factorial [in WBLogic.heap_lang_examples.very_awkward]
factV [in WBLogic.F_mu_ref.binary.examples.fact]
fact_accV [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc [in WBLogic.F_mu_ref.binary.examples.fact]
fact_acc_body [in WBLogic.F_mu_ref.binary.examples.fact]
fill_ctx [in WBLogic.F_mu_ref.binary.context_refinement]
fill_ctx_item [in WBLogic.F_mu_ref.binary.context_refinement]
F_mu_ref_lang [in WBLogic.F_mu_ref.lang]
F_mu_ref_ectx_lang [in WBLogic.F_mu_ref.lang]
F_mu_ref_ectxi_lang [in WBLogic.F_mu_ref.lang]
F_mu_ref.exprO [in WBLogic.F_mu_ref.lang]
F_mu_ref.valO [in WBLogic.F_mu_ref.lang]
F_mu_ref.stateO [in WBLogic.F_mu_ref.lang]
F_mu_ref.head_step_sind [in WBLogic.F_mu_ref.lang]
F_mu_ref.head_step_ind [in WBLogic.F_mu_ref.lang]
F_mu_ref.state [in WBLogic.F_mu_ref.lang]
F_mu_ref.fill_item [in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_sind [in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_rec [in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_ind [in WBLogic.F_mu_ref.lang]
F_mu_ref.ectx_item_rect [in WBLogic.F_mu_ref.lang]
F_mu_ref.to_val [in WBLogic.F_mu_ref.lang]
F_mu_ref.of_val [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_eval [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_sind [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_rec [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_ind [in WBLogic.F_mu_ref.lang]
F_mu_ref.val_rect [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_sind [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_rec [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_ind [in WBLogic.F_mu_ref.lang]
F_mu_ref.expr_rect [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_sind [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_rec [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_ind [in WBLogic.F_mu_ref.lang]
F_mu_ref.binop_rect [in WBLogic.F_mu_ref.lang]
F_mu_ref.loc [in WBLogic.F_mu_ref.lang]
G
ghost_id [in WBLogic.program_logic.ghost_stacks]gmap_of_trace [in WBLogic.heap_lang_trace.trace_resources]
gpop [in WBLogic.program_logic.ghost_stacks]
gpush [in WBLogic.program_logic.ghost_stacks]
gsingleton [in WBLogic.program_logic.ghost_stacks]
gstack [in WBLogic.program_logic.ghost_stacks]
gstackO [in WBLogic.program_logic.ghost_stacks]
gstacks [in WBLogic.program_logic.ghost_stacks]
gstacks_except [in WBLogic.program_logic.ghost_stacks]
gstacksΣ [in WBLogic.program_logic.ghost_stacks]
gstackUR [in WBLogic.program_logic.ghost_stacks]
gstack_exists [in WBLogic.program_logic.ghost_stacks]
gstack_full [in WBLogic.program_logic.ghost_stacks]
gstack_frag [in WBLogic.program_logic.ghost_stacks]
gtop [in WBLogic.program_logic.ghost_stacks]
H
heapS_mapsto [in WBLogic.F_mu_ref.binary.rules]heapUR [in WBLogic.F_mu_ref.binary.rules]
heap_lang [in WBLogic.heap_lang_trace.lang]
heap_ectx_lang [in WBLogic.heap_lang_trace.lang]
heap_ectxi_lang [in WBLogic.heap_lang_trace.lang]
heap_lang.head_step_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.head_step_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.tags [in WBLogic.heap_lang_trace.lang]
heap_lang.state_init_heap [in WBLogic.heap_lang_trace.lang]
heap_lang.heap_array [in WBLogic.heap_lang_trace.lang]
heap_lang.state_upd_used_proph_id [in WBLogic.heap_lang_trace.lang]
heap_lang.state_add_event [in WBLogic.heap_lang_trace.lang]
heap_lang.state_upd_heap [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_loc [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_bool [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_eval_int [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_eval [in WBLogic.heap_lang_trace.lang]
heap_lang.subst' [in WBLogic.heap_lang_trace.lang]
heap_lang.subst [in WBLogic.heap_lang_trace.lang]
heap_lang.fill_item [in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.ectx_item_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.exprO [in WBLogic.heap_lang_trace.lang]
heap_lang.valO [in WBLogic.heap_lang_trace.lang]
heap_lang.locO [in WBLogic.heap_lang_trace.lang]
heap_lang.stateO [in WBLogic.heap_lang_trace.lang]
heap_lang.vals_compare_safe [in WBLogic.heap_lang_trace.lang]
heap_lang.val_is_unboxed [in WBLogic.heap_lang_trace.lang]
heap_lang.lit_is_unboxed [in WBLogic.heap_lang_trace.lang]
heap_lang.to_val [in WBLogic.heap_lang_trace.lang]
heap_lang.observation [in WBLogic.heap_lang_trace.lang]
heap_lang.val_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.val_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.val_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.val_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.expr_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.bin_op_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.un_op_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_sind [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_rec [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_ind [in WBLogic.heap_lang_trace.lang]
heap_lang.base_lit_rect [in WBLogic.heap_lang_trace.lang]
heap_lang.proph_id [in WBLogic.heap_lang_trace.lang]
heapΣ [in WBLogic.heap_lang_trace.adequacy]
heapΣ [in WBLogic.heap_lang.adequacy]
hist [in WBLogic.heap_lang_trace.trace_resources]
I
interp [in WBLogic.F_mu_ref.binary.logrel]interp [in WBLogic.F_mu_ref.unary.logrel]
interp_env [in WBLogic.F_mu_ref.binary.logrel]
interp_ref [in WBLogic.F_mu_ref.binary.logrel]
interp_ref_inv [in WBLogic.F_mu_ref.binary.logrel]
interp_rec [in WBLogic.F_mu_ref.binary.logrel]
interp_rec1 [in WBLogic.F_mu_ref.binary.logrel]
interp_exist [in WBLogic.F_mu_ref.binary.logrel]
interp_forall [in WBLogic.F_mu_ref.binary.logrel]
interp_arrow [in WBLogic.F_mu_ref.binary.logrel]
interp_sum [in WBLogic.F_mu_ref.binary.logrel]
interp_prod [in WBLogic.F_mu_ref.binary.logrel]
interp_bool [in WBLogic.F_mu_ref.binary.logrel]
interp_nat [in WBLogic.F_mu_ref.binary.logrel]
interp_unit [in WBLogic.F_mu_ref.binary.logrel]
interp_expr [in WBLogic.F_mu_ref.binary.logrel]
interp_expr [in WBLogic.F_mu_ref.unary.logrel]
interp_env [in WBLogic.F_mu_ref.unary.logrel]
interp_ref [in WBLogic.F_mu_ref.unary.logrel]
interp_ref_inv [in WBLogic.F_mu_ref.unary.logrel]
interp_rec [in WBLogic.F_mu_ref.unary.logrel]
interp_rec1 [in WBLogic.F_mu_ref.unary.logrel]
interp_exist [in WBLogic.F_mu_ref.unary.logrel]
interp_forall [in WBLogic.F_mu_ref.unary.logrel]
interp_arrow [in WBLogic.F_mu_ref.unary.logrel]
interp_sum [in WBLogic.F_mu_ref.unary.logrel]
interp_prod [in WBLogic.F_mu_ref.unary.logrel]
interp_bool [in WBLogic.F_mu_ref.unary.logrel]
interp_nat [in WBLogic.F_mu_ref.unary.logrel]
interp_unit [in WBLogic.F_mu_ref.unary.logrel]
inv_mapsto [in WBLogic.heap_lang_trace.primitive_laws]
inv_mapsto_own [in WBLogic.heap_lang_trace.primitive_laws]
is_atomic [in WBLogic.F_mu_ref.lang]
L
logN [in WBLogic.F_mu_ref.binary.logrel]logN [in WBLogic.F_mu_ref.unary.logrel]
log_typed [in WBLogic.F_mu_ref.unary.fundamental]
O
oneshotR [in WBLogic.oneshot]oneshotΣ [in WBLogic.oneshot]
P
pending [in WBLogic.oneshot]persistent_predO [in WBLogic.persistent_pred]
persistent_pred_ofe_mixin [in WBLogic.persistent_pred]
R
related_private [in WBLogic.program_logic.lib.sts]related_public [in WBLogic.program_logic.lib.sts]
S
sequential_trace_alt [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]sequential_full_trace_sind [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_full_trace_ind [in WBLogic.heap_lang_trace_examples.sequential_trace_alt]
sequential_trace [in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_sind [in WBLogic.heap_lang_trace_examples.very_awkward]
sequential_with_opened_ind [in WBLogic.heap_lang_trace_examples.very_awkward]
shot [in WBLogic.oneshot]
soundness_binaryΣ [in WBLogic.F_mu_ref.binary.soundness]
specN [in WBLogic.F_mu_ref.binary.rules]
spec_ctx [in WBLogic.F_mu_ref.binary.rules]
spec_inv [in WBLogic.F_mu_ref.binary.rules]
state_of [in WBLogic.program_logic.lib.sts]
steps_lb [in WBLogic.heap_lang_trace.primitive_laws]
steps_auth [in WBLogic.heap_lang_trace.primitive_laws]
STSUR [in WBLogic.program_logic.lib.sts]
STS_inv [in WBLogic.program_logic.lib.sts]
sts_config_full [in WBLogic.program_logic.lib.sts]
sts_config_frag [in WBLogic.program_logic.lib.sts]
STS_inv_name [in WBLogic.program_logic.lib.sts]
sts_config [in WBLogic.program_logic.lib.sts]
STSΣ [in WBLogic.program_logic.lib.sts]
T
to_heap [in WBLogic.F_mu_ref.binary.rules]to_tpool [in WBLogic.F_mu_ref.binary.rules]
to_tpool_go [in WBLogic.F_mu_ref.binary.rules]
tpoolUR [in WBLogic.F_mu_ref.binary.rules]
tpool_mapsto [in WBLogic.F_mu_ref.binary.rules]
traceO [in WBLogic.heap_lang_trace.trace_resources]
trace_inv [in WBLogic.heap_lang_trace.trace_resources]
trace_is [in WBLogic.heap_lang_trace.trace_resources]
trace_half_frag [in WBLogic.heap_lang_trace.trace_resources]
trace_auth [in WBLogic.heap_lang_trace.trace_resources]
traceΣ [in WBLogic.heap_lang_trace.trace_resources]
typed_sind [in WBLogic.F_mu_ref.typing]
typed_ind [in WBLogic.F_mu_ref.typing]
typed_ctx_sind [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_ind [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_sind [in WBLogic.F_mu_ref.binary.context_refinement]
typed_ctx_item_ind [in WBLogic.F_mu_ref.binary.context_refinement]
type_sind [in WBLogic.F_mu_ref.typing]
type_rec [in WBLogic.F_mu_ref.typing]
type_ind [in WBLogic.F_mu_ref.typing]
type_rect [in WBLogic.F_mu_ref.typing]
V
vae_sts [in WBLogic.heap_lang_examples.sts.very_awkward]varO [in WBLogic.F_mu_ref.base]
very_awkward_self_apply [in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_awkward [in WBLogic.F_mu_ref.unary.examples.very_awkward]
very_akward_call_fact_across [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward_self_apply [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awk_spec [in WBLogic.heap_lang_trace_examples.very_awkward]
very_awkward [in WBLogic.F_mu_ref.binary.examples.very_awkward]
very_akward_call_fact_across [in WBLogic.heap_lang_examples.very_awkward]
very_awkward_self_apply [in WBLogic.heap_lang_examples.very_awkward]
very_awkward [in WBLogic.heap_lang_examples.very_awkward]
very_awkward_self_apply [in WBLogic.heap_lang_examples.sts.very_awkward]
very_awkward [in WBLogic.heap_lang_examples.sts.very_awkward]
W
wbheap_invariance [in WBLogic.heap_lang_trace.adequacy]wbheap_adequacy [in WBLogic.heap_lang_trace.adequacy]
wbheap_adequacy [in WBLogic.heap_lang.adequacy]
wbwp [in WBLogic.program_logic.weakestpre]
Wrap.very_awk_instrumented [in WBLogic.heap_lang_trace_examples.very_awkward]
Record Index
A
AsRecV [in WBLogic.heap_lang_trace.class_instances]C
cfgSG [in WBLogic.F_mu_ref.binary.rules]G
gstacksGpre [in WBLogic.program_logic.ghost_stacks]gstacksIG [in WBLogic.program_logic.ghost_stacks]
H
heapIG [in WBLogic.F_mu_ref.wp_rules]heap_lang.state [in WBLogic.heap_lang_trace.lang]
O
oneshotG [in WBLogic.oneshot]P
persistent_pred [in WBLogic.persistent_pred]S
soundness_unary_preG [in WBLogic.F_mu_ref.unary.soundness]STS [in WBLogic.program_logic.lib.sts]
T
traceGS [in WBLogic.heap_lang_trace.trace_resources]trace_preG [in WBLogic.heap_lang_trace.trace_resources]
W
wbheapGpreS [in WBLogic.heap_lang_trace.adequacy]wbheapGpreS [in WBLogic.heap_lang.adequacy]
wbheapGS [in WBLogic.heap_lang_trace.primitive_laws]
wbheapGS [in WBLogic.heap_lang.primitive_laws]
| 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 | (1421 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 | (91 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 | (3 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 | (40 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 | (470 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 | (290 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 | (20 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 | (61 entries) |
| Instance 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 | (132 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (39 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 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 | (237 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 | (16 entries) |