| 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 | (363 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 | (79 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (25 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 | (12 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 | (96 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 | (57 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 | (23 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 | (14 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 | (5 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 | (11 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 | (37 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 | (4 entries) |
Global Index
A
absSim [section, in LM.Refinements]absSim.assume_refine.top_down.C [variable, in LM.Refinements]
absSim.assume_refine.top_down.FN [variable, in LM.Refinements]
absSim.assume_refine.top_down [section, in LM.Refinements]
absSim.assume_refine.Correctness.H [variable, in LM.Refinements]
absSim.assume_refine.Correctness.x [variable, in LM.Refinements]
absSim.assume_refine.Correctness.a [variable, in LM.Refinements]
absSim.assume_refine.Correctness [section, in LM.Refinements]
absSim.assume_refine.refinement [variable, in LM.Refinements]
_ ≫ _ [notation, in LM.Refinements]
absSim.assume_refine.refines [variable, in LM.Refinements]
_ ▷τ _ [notation, in LM.Refinements]
absSim.assume_refine.X [variable, in LM.Refinements]
absSim.assume_refine.A [variable, in LM.Refinements]
absSim.assume_refine [section, in LM.Refinements]
_ ≫ _ [notation, in LM.Refinements]
absSim.refine_M.refines [variable, in LM.Refinements]
absSim.refine_M.B [variable, in LM.Refinements]
absSim.refine_M.A [variable, in LM.Refinements]
absSim.refine_M [section, in LM.Refinements]
_ ≫ _ [notation, in LM.Refinements]
absSim.refine_ARS.refines [variable, in LM.Refinements]
absSim.refine_ARS.A [variable, in LM.Refinements]
absSim.refine_ARS.X [variable, in LM.Refinements]
absSim.refine_ARS [section, in LM.Refinements]
abstraction [inductive, in LM.L]
any [definition, in LM.Refinements]
app [constructor, in LM.L]
appC [constructor, in LM.Codes]
appT [constructor, in LM.Programs]
ARS [record, in LM.Prelims]
ARS_R [projection, in LM.Prelims]
ARS_X [projection, in LM.Prelims]
B
beta_simulation [lemma, in LM.M_stack]beta_terminating [lemma, in LM.M_stack]
beta_functional [lemma, in LM.M_stack]
beta_simulation [lemma, in LM.M_clos]
bndApp [constructor, in LM.L]
bndlam [constructor, in LM.L]
bndvar [constructor, in LM.L]
boundC [inductive, in LM.Closures]
boundC_C [constructor, in LM.Closures]
boundL [inductive, in LM.L]
boundL_subst [lemma, in LM.Extra]
boundL_mono [lemma, in LM.Extra]
boundP [inductive, in LM.Programs]
boundP_substP [lemma, in LM.Closures]
boundP_mono [lemma, in LM.Closures]
boundP_app [constructor, in LM.Programs]
boundP_lam [constructor, in LM.Programs]
boundP_var [constructor, in LM.Programs]
boundP_ret [constructor, in LM.Programs]
bound_compile [lemma, in LM.Programs]
C
cbound_cons [lemma, in LM.M_clos]classical [definition, in LM.Prelims]
Clo [inductive, in LM.Closures]
closC [constructor, in LM.Closures]
closedL [definition, in LM.L]
closedP [definition, in LM.Programs]
closedSC [definition, in LM.M_clos]
closedSC_preserved [lemma, in LM.M_clos]
closed_stepL [lemma, in LM.Extra]
closed_subst [lemma, in LM.Extra]
closed_cases [lemma, in LM.Extra]
Closures [library]
clos_L_refinement [lemma, in LM.M_clos]
clos_stack_refinement [lemma, in LM.M_clos]
Code [projection, in LM.Codes]
code [record, in LM.Codes]
codeImpl [instance, in LM.Codes]
Codes [library]
Com [inductive, in LM.Codes]
compile_heap_L [lemma, in LM.M_heap]
compile_heap_clos [lemma, in LM.M_heap]
compile_stack_L [lemma, in LM.M_stack]
compile_clos_L [lemma, in LM.M_clos]
compile_clos_stack [lemma, in LM.M_clos]
composition [lemma, in LM.Refinements]
computable [definition, in LM.Prelims]
computable_classical [lemma, in LM.Prelims]
counterexample_closed_needed [lemma, in LM.Extra]
D
Dec [definition, in LM.Prelims]dec [definition, in LM.Prelims]
decompileArg_abstractions [lemma, in LM.M_stack]
decompileArg_step [lemma, in LM.M_stack]
decompileArg_inv [lemma, in LM.M_stack]
decompileTask_step [lemma, in LM.M_stack]
decompileTask_inv [lemma, in LM.M_stack]
decompile_lamT_inv [lemma, in LM.Programs]
decompile_append [lemma, in LM.Programs]
decompile_correct' [lemma, in LM.Programs]
downSim [lemma, in LM.Refinements]
E
evaluates [inductive, in LM.Prelims]evaluates_irred [lemma, in LM.Prelims]
evaluates_fun [lemma, in LM.Prelims]
evaluates_S [constructor, in LM.Prelims]
evaluates_B [constructor, in LM.Prelims]
evaluates_tau [lemma, in LM.Refinements]
evaluation_propagates [lemma, in LM.Refinements]
exactlyOneHolds [definition, in LM.Prelims]
Extra [library]
F
fetch_correct [lemma, in LM.Codes]fetch_correct' [lemma, in LM.Codes]
Forall_map [lemma, in LM.Prelims]
Forall2_impl [lemma, in LM.Prelims]
functional [definition, in LM.Prelims]
G
get [projection, in LM.Heaps]H
HA [projection, in LM.Heaps]heap [section, in LM.Heaps]
Heap [projection, in LM.Heaps]
heap [record, in LM.Heaps]
heapImpl [instance, in LM.Heaps]
Heaps [library]
heap_decomp.unlinEnv.H [variable, in LM.Extra]
heap_decomp.unlinEnv [section, in LM.Extra]
heap_decomp.unlinPro [section, in LM.Extra]
_ ≫HC _ [notation, in LM.Extra]
(≫HC) [notation, in LM.Extra]
_ ≫E_ _ _ [notation, in LM.Extra]
_ ≫C_ _ _ [notation, in LM.Extra]
(≫C_ _ ) [notation, in LM.Extra]
heap_decomp.C [variable, in LM.Extra]
heap_decomp.heapImpl [variable, in LM.Extra]
heap_decomp.codeImpl [variable, in LM.Extra]
heap_decomp [section, in LM.Extra]
heap_L_refinement [lemma, in LM.M_heap]
heap_clos_refinement [lemma, in LM.M_heap]
heap.C [variable, in LM.Heaps]
heap.codeImpl [variable, in LM.Heaps]
heap.heapImpl [variable, in LM.Heaps]
_ .[ _ , _ ] [notation, in LM.Heaps]
_ ≫C_ _ _ [notation, in LM.Heaps]
_ ≫C_ _ _ [notation, in LM.Heaps]
_ ≫C_ _ _ [notation, in LM.Heaps]
_ ≫E_ _ _ [notation, in LM.Heaps]
(≫C( _ ) ) [notation, in LM.Heaps]
HR1 [projection, in LM.Heaps]
HR2 [projection, in LM.Heaps]
I
inc [projection, in LM.Codes]isAbstraction [constructor, in LM.L]
L
L [library]label [inductive, in LM.Refinements]
lam [constructor, in LM.L]
lamC [constructor, in LM.Codes]
lamT [constructor, in LM.Programs]
Lin [section, in LM.M_heap]
Lin.C [variable, in LM.M_heap]
Lin.codeImpl [variable, in LM.M_heap]
Lin.heapImpl [variable, in LM.M_heap]
_ ≫HL _ [notation, in LM.M_heap]
_ ≫HC _ [notation, in LM.M_heap]
_ ≻H _ [notation, in LM.M_heap]
_ ≻H_ _ _ [notation, in LM.M_heap]
_ ≻H_ _ _ [notation, in LM.M_heap]
_ ≻H_ _ _ [notation, in LM.M_heap]
_ ≫E_ _ _ [notation, in LM.M_heap]
_ ≫C_ _ _ [notation, in LM.M_heap]
(≫C_ _ ) [notation, in LM.M_heap]
(≫HC) [notation, in LM.M_heap]
(≫HL) [notation, in LM.M_heap]
(≻H_ _ ) [notation, in LM.M_heap]
(≻H) [notation, in LM.M_heap]
lookup [definition, in LM.Heaps]
lookup_unlinedEnv [lemma, in LM.Heaps]
L_trichotomy [lemma, in LM.L]
M
Machine [record, in LM.Refinements]M_rel [projection, in LM.Refinements]
M_A [projection, in LM.Refinements]
M_stack [library]
M_clos [library]
M_heap [library]
N
nat_eq_dec [instance, in LM.Prelims]nat_le_dec [instance, in LM.Prelims]
noneHolds [definition, in LM.Prelims]
normalizes [definition, in LM.Prelims]
normalizes_terminates [lemma, in LM.Prelims]
nth_error_map [lemma, in LM.Prelims]
nth_error_Some_lt [lemma, in LM.Prelims]
nth_error_lt_Some [lemma, in LM.Prelims]
nth_error_unlinedEnv [lemma, in LM.Heaps]
O
one_downSim [lemma, in LM.Refinements]P
PA [projection, in LM.Codes]Prelims [library]
PrelimsTac [library]
Pro [inductive, in LM.Programs]
Programs [library]
put [projection, in LM.Heaps]
R
rcomp [definition, in LM.Prelims]redL [definition, in LM.L]
reducibility [lemma, in LM.M_clos]
reducible [definition, in LM.Prelims]
reducible_red [lemma, in LM.M_heap]
reducible_red [lemma, in LM.M_stack]
Refinements [library]
refinement_M [definition, in LM.Refinements]
refinement_ARS [definition, in LM.Refinements]
representsC [constructor, in LM.M_heap]
representsClos [inductive, in LM.Heaps]
representsClos_extend [lemma, in LM.Heaps]
representsClos_C [constructor, in LM.Heaps]
representsEnv [inductive, in LM.Heaps]
representsEnvCons [constructor, in LM.Heaps]
representsEnvNil [constructor, in LM.Heaps]
representsEnv_extend [lemma, in LM.Heaps]
representsEnv_functional [lemma, in LM.Heaps]
representsPro [inductive, in LM.Codes]
representsProApp [constructor, in LM.Codes]
representsProLam [constructor, in LM.Codes]
representsProRet [constructor, in LM.Codes]
representsProVar [constructor, in LM.Codes]
representsPro_functional [lemma, in LM.Codes]
repsCL [definition, in LM.M_clos]
repsCS [definition, in LM.M_clos]
repsCS_functional [lemma, in LM.M_clos]
repsHC [inductive, in LM.M_heap]
repsHL [definition, in LM.M_heap]
repsP [definition, in LM.Programs]
repsSL [definition, in LM.M_stack]
repsSL_computable [lemma, in LM.M_stack]
repsSL_functional [lemma, in LM.M_stack]
retC [constructor, in LM.Codes]
retT [constructor, in LM.Programs]
rightValue [lemma, in LM.Refinements]
S
size_induction [lemma, in LM.Prelims]stack_L_refinement [lemma, in LM.M_stack]
star [inductive, in LM.Extra]
starC [constructor, in LM.Extra]
starR [constructor, in LM.Extra]
state [definition, in LM.M_heap]
stateC [definition, in LM.M_clos]
stateS [definition, in LM.M_stack]
stateS_trichotomy [lemma, in LM.M_stack]
stepC [inductive, in LM.M_clos]
stepFunction [definition, in LM.Prelims]
stepH [inductive, in LM.M_heap]
stepL [inductive, in LM.L]
stepLApp [constructor, in LM.L]
stepLAppL [constructor, in LM.L]
stepLAppR [constructor, in LM.L]
stepLs [inductive, in LM.M_stack]
stepLs_decompileTask [lemma, in LM.M_stack]
stepLs_decomp [lemma, in LM.M_stack]
stepLs_singleton_inv [lemma, in LM.M_stack]
stepLs_there [constructor, in LM.M_stack]
stepL_computable [lemma, in LM.L]
stepL_funct [lemma, in LM.L]
stepL_here [constructor, in LM.M_stack]
stepS [inductive, in LM.M_stack]
stepS_functional [lemma, in LM.M_stack]
stepS_nil [constructor, in LM.M_stack]
stepS_pushVal [constructor, in LM.M_stack]
stepS_betaC [constructor, in LM.M_stack]
step_simulation [lemma, in LM.M_heap]
step_beta [constructor, in LM.M_heap]
step_pushVal [constructor, in LM.M_heap]
step_load [constructor, in LM.M_heap]
step_nil [constructor, in LM.M_heap]
step_betaC [constructor, in LM.M_clos]
step_pushVal [constructor, in LM.M_clos]
step_load [constructor, in LM.M_clos]
step_nil [constructor, in LM.M_clos]
stuck [inductive, in LM.L]
stuckL [constructor, in LM.L]
stuckLs [inductive, in LM.M_stack]
stuckLsHere [constructor, in LM.M_stack]
stuckLsThere [constructor, in LM.M_stack]
stuckR [constructor, in LM.L]
stuckVar [constructor, in LM.L]
stuck_normal [lemma, in LM.L]
stuck_not_closed [lemma, in LM.Extra]
stuck_decompileTask [lemma, in LM.M_stack]
stuck_decompile [lemma, in LM.M_stack]
subst [definition, in LM.L]
substP [definition, in LM.Programs]
substPl [definition, in LM.Closures]
substPl_cons [lemma, in LM.Closures]
substPl_nil [lemma, in LM.Closures]
substP_boundP [lemma, in LM.Closures]
substP_rep_subst' [lemma, in LM.Programs]
substP_rep_subst [lemma, in LM.M_stack]
subst_boundL_inv [lemma, in LM.Extra]
T
tau_eval [lemma, in LM.Refinements]tau_evaluates_evaluates [lemma, in LM.Refinements]
tau_simulation [lemma, in LM.M_stack]
tau_terminating [lemma, in LM.M_stack]
tau_functional [lemma, in LM.M_stack]
tau_simulation [lemma, in LM.M_clos]
term [inductive, in LM.L]
terminatesC [constructor, in LM.Prelims]
terminatesOn [inductive, in LM.Prelims]
terminates_normalizes [lemma, in LM.Prelims]
termination_propagates [lemma, in LM.Refinements]
term_eq_dec [instance, in LM.L]
translateC_boundP [lemma, in LM.Closures]
U
unlinClos [definition, in LM.Extra]unlinEnv [definition, in LM.Extra]
unlinEnv_fuel [lemma, in LM.Extra]
unlinEnv_mono [lemma, in LM.Extra]
unlinPro [definition, in LM.Extra]
unlinPro_fuel [lemma, in LM.Extra]
unlinPro_mono [lemma, in LM.Extra]
upSim [lemma, in LM.Refinements]
V
var [constructor, in LM.L]varC [constructor, in LM.Codes]
varT [constructor, in LM.Programs]
other
__ ≻L _ [notation, in LM.L]
_ ≻L _ [notation, in LM.L]
_ ≻L _ [notation, in LM.L]
_ ▷ _ [notation, in LM.Prelims]
_ ▷ _ [notation, in LM.Prelims]
_ ▷ _ [notation, in LM.Prelims]
_ ≻ _ [notation, in LM.Prelims]
_ ∈ _ [notation, in LM.Prelims]
_ .[ _ ] [notation, in LM.Prelims]
_
_ / _ [notation, in LM.Closures]
_ ≻β _ [notation, in LM.Refinements]
_ ≻τ _ [notation, in LM.Refinements]
_ ≫p_ _ _ [notation, in LM.Codes]
_ .[ _ , _ ] [notation, in LM.Heaps]
_
[notation, in LM.Programs] [notation, in LM.Programs] [in LM.Programs] [in LM.Programs]
_ ≫P _ [notation, in LM.Programs]
_ ≻Ls _ [notation, in LM.M_stack]
_ ≫SL _ [notation, in LM.M_stack]
_ ≻S _ [notation, in LM.M_stack]
_ ≻S_ _ _ [notation, in LM.M_stack]
_ ≻S_ _ _ [notation, in LM.M_stack]
_ ≻S_ _ _ [notation, in LM.M_stack]
_ ≫CL _ [notation, in LM.M_clos]
_ ≫CS _ [notation, in LM.M_clos]
_ ≻C _ [notation, in LM.M_clos]
_ ≻C_ _ _ [notation, in LM.M_clos]
_ ≻C_ _ _ [notation, in LM.M_clos]
_ ≻C_ _ _ [notation, in LM.M_clos]
eq_dec _ [notation, in LM.Prelims]
try _ := _ in _ [notation, in LM.Prelims]
# _ [notation, in LM.Codes]
(
(
(>>P) [notation, in LM.Programs]
(≫CL) [notation, in LM.M_clos]
(≫CS) [notation, in LM.M_clos]
(≫SL) [notation, in LM.M_stack]
(≻C_ _ ) [notation, in LM.M_clos]
(≻C) [notation, in LM.M_clos]
(≻L) [notation, in LM.L]
(≻S_ _ ) [notation, in LM.M_stack]
(≻S) [notation, in LM.M_stack]
(≻ _ ) [notation, in LM.Prelims]
(≻) [notation, in LM.Prelims]
(≻τ) [notation, in LM.Refinements]
(▷ _ ) [notation, in LM.Prelims]
(▷) [notation, in LM.Prelims]
(λ _ ) [notation, in LM.L]
| _ | [notation, in LM.Prelims]
β [constructor, in LM.Refinements]
γ [definition, in LM.Programs]
δC [definition, in LM.Closures]
τ [constructor, in LM.Refinements]
τβ_rel [definition, in LM.Refinements]
φ [projection, in LM.Codes]
ψ [definition, in LM.Codes]
Notation Index
A
_ ≫ _ [in LM.Refinements]
_ ▷τ _ [in LM.Refinements]
_ ≫ _ [in LM.Refinements]
_ ≫ _ [in LM.Refinements]
H
_ ≫HC _ [in LM.Extra]
(≫HC) [in LM.Extra]
_ ≫E_ _ _ [in LM.Extra]
_ ≫C_ _ _ [in LM.Extra]
(≫C_ _ ) [in LM.Extra]
_ .[ _ , _ ] [in LM.Heaps]
_ ≫C_ _ _ [in LM.Heaps]
_ ≫C_ _ _ [in LM.Heaps]
_ ≫C_ _ _ [in LM.Heaps]
_ ≫E_ _ _ [in LM.Heaps]
(≫C( _ ) ) [in LM.Heaps]
L
_ ≫HL _ [in LM.M_heap]
_ ≫HC _ [in LM.M_heap]
_ ≻H _ [in LM.M_heap]
_ ≻H_ _ _ [in LM.M_heap]
_ ≻H_ _ _ [in LM.M_heap]
_ ≻H_ _ _ [in LM.M_heap]
_ ≫E_ _ _ [in LM.M_heap]
_ ≫C_ _ _ [in LM.M_heap]
(≫C_ _ ) [in LM.M_heap]
(≫HC) [in LM.M_heap]
(≫HL) [in LM.M_heap]
(≻H_ _ ) [in LM.M_heap]
(≻H) [in LM.M_heap]
other
_
_ ≻L _ [in LM.L]
_ ≻L _ [in LM.L]
_ ≻L _ [in LM.L]
_ ▷ _ [in LM.Prelims]
_ ▷ _ [in LM.Prelims]
_ ▷ _ [in LM.Prelims]
_ ≻ _ [in LM.Prelims]
_ ∈ _ [in LM.Prelims]
_ .[ _ ] [in LM.Prelims]
_
_ / _ [in LM.Closures]
_ ≻β _ [in LM.Refinements]
_ ≻τ _ [in LM.Refinements]
_ ≫p_ _ _ [in LM.Codes]
_ .[ _ , _ ] [in LM.Heaps]
_
_ ≫P _ [in LM.Programs]
_ ≻Ls _ [in LM.M_stack]
_ ≫SL _ [in LM.M_stack]
_ ≻S _ [in LM.M_stack]
_ ≻S_ _ _ [in LM.M_stack]
_ ≻S_ _ _ [in LM.M_stack]
_ ≻S_ _ _ [in LM.M_stack]
_ ≫CL _ [in LM.M_clos]
_ ≫CS _ [in LM.M_clos]
_ ≻C _ [in LM.M_clos]
_ ≻C_ _ _ [in LM.M_clos]
_ ≻C_ _ _ [in LM.M_clos]
_ ≻C_ _ _ [in LM.M_clos]
eq_dec _ [in LM.Prelims]
try _ := _ in _ [in LM.Prelims]
# _ [in LM.Codes]
(
(
(>>P) [in LM.Programs]
(≫CL) [in LM.M_clos]
(≫CS) [in LM.M_clos]
(≫SL) [in LM.M_stack]
(≻C_ _ ) [in LM.M_clos]
(≻C) [in LM.M_clos]
(≻L) [in LM.L]
(≻S_ _ ) [in LM.M_stack]
(≻S) [in LM.M_stack]
(≻ _ ) [in LM.Prelims]
(≻) [in LM.Prelims]
(≻τ) [in LM.Refinements]
(▷ _ ) [in LM.Prelims]
(▷) [in LM.Prelims]
(λ _ ) [in LM.L]
| _ | [in LM.Prelims]
Variable Index
A
absSim.assume_refine.top_down.C [in LM.Refinements]
absSim.assume_refine.top_down.FN [in LM.Refinements]
absSim.assume_refine.Correctness.H [in LM.Refinements]
absSim.assume_refine.Correctness.x [in LM.Refinements]
absSim.assume_refine.Correctness.a [in LM.Refinements]
absSim.assume_refine.refinement [in LM.Refinements]
absSim.assume_refine.refines [in LM.Refinements]
absSim.assume_refine.X [in LM.Refinements]
absSim.assume_refine.A [in LM.Refinements]
absSim.refine_M.refines [in LM.Refinements]
absSim.refine_M.B [in LM.Refinements]
absSim.refine_M.A [in LM.Refinements]
absSim.refine_ARS.refines [in LM.Refinements]
absSim.refine_ARS.A [in LM.Refinements]
absSim.refine_ARS.X [in LM.Refinements]
H
heap_decomp.unlinEnv.H [in LM.Extra]
heap_decomp.C [in LM.Extra]
heap_decomp.heapImpl [in LM.Extra]
heap_decomp.codeImpl [in LM.Extra]
heap.C [in LM.Heaps]
heap.codeImpl [in LM.Heaps]
heap.heapImpl [in LM.Heaps]
L
Lin.C [in LM.M_heap]
Lin.codeImpl [in LM.M_heap]
Lin.heapImpl [in LM.M_heap]
Library Index
C
Closures
Codes
E
Extra
H
Heaps
L
L
M
M_stack
M_clos
M_heap
P
Prelims
PrelimsTac
Programs
R
Refinements
Lemma Index
B
beta_simulation [in LM.M_stack]
beta_terminating [in LM.M_stack]
beta_functional [in LM.M_stack]
beta_simulation [in LM.M_clos]
boundL_subst [in LM.Extra]
boundL_mono [in LM.Extra]
boundP_substP [in LM.Closures]
boundP_mono [in LM.Closures]
bound_compile [in LM.Programs]
C
cbound_cons [in LM.M_clos]
closedSC_preserved [in LM.M_clos]
closed_stepL [in LM.Extra]
closed_subst [in LM.Extra]
closed_cases [in LM.Extra]
clos_L_refinement [in LM.M_clos]
clos_stack_refinement [in LM.M_clos]
compile_heap_L [in LM.M_heap]
compile_heap_clos [in LM.M_heap]
compile_stack_L [in LM.M_stack]
compile_clos_L [in LM.M_clos]
compile_clos_stack [in LM.M_clos]
composition [in LM.Refinements]
computable_classical [in LM.Prelims]
counterexample_closed_needed [in LM.Extra]
D
decompileArg_abstractions [in LM.M_stack]
decompileArg_step [in LM.M_stack]
decompileArg_inv [in LM.M_stack]
decompileTask_step [in LM.M_stack]
decompileTask_inv [in LM.M_stack]
decompile_lamT_inv [in LM.Programs]
decompile_append [in LM.Programs]
decompile_correct' [in LM.Programs]
downSim [in LM.Refinements]
E
evaluates_irred [in LM.Prelims]
evaluates_fun [in LM.Prelims]
evaluates_tau [in LM.Refinements]
evaluation_propagates [in LM.Refinements]
F
fetch_correct [in LM.Codes]
fetch_correct' [in LM.Codes]
Forall_map [in LM.Prelims]
Forall2_impl [in LM.Prelims]
H
heap_L_refinement [in LM.M_heap]
heap_clos_refinement [in LM.M_heap]
L
lookup_unlinedEnv [in LM.Heaps]
L_trichotomy [in LM.L]
N
normalizes_terminates [in LM.Prelims]
nth_error_map [in LM.Prelims]
nth_error_Some_lt [in LM.Prelims]
nth_error_lt_Some [in LM.Prelims]
nth_error_unlinedEnv [in LM.Heaps]
O
one_downSim [in LM.Refinements]
R
reducibility [in LM.M_clos]
reducible_red [in LM.M_heap]
reducible_red [in LM.M_stack]
representsClos_extend [in LM.Heaps]
representsEnv_extend [in LM.Heaps]
representsEnv_functional [in LM.Heaps]
representsPro_functional [in LM.Codes]
repsCS_functional [in LM.M_clos]
repsSL_computable [in LM.M_stack]
repsSL_functional [in LM.M_stack]
rightValue [in LM.Refinements]
S
size_induction [in LM.Prelims]
stack_L_refinement [in LM.M_stack]
stateS_trichotomy [in LM.M_stack]
stepLs_decompileTask [in LM.M_stack]
stepLs_decomp [in LM.M_stack]
stepLs_singleton_inv [in LM.M_stack]
stepL_computable [in LM.L]
stepL_funct [in LM.L]
stepS_functional [in LM.M_stack]
step_simulation [in LM.M_heap]
stuck_normal [in LM.L]
stuck_not_closed [in LM.Extra]
stuck_decompileTask [in LM.M_stack]
stuck_decompile [in LM.M_stack]
substPl_cons [in LM.Closures]
substPl_nil [in LM.Closures]
substP_boundP [in LM.Closures]
substP_rep_subst' [in LM.Programs]
substP_rep_subst [in LM.M_stack]
subst_boundL_inv [in LM.Extra]
T
tau_eval [in LM.Refinements]
tau_evaluates_evaluates [in LM.Refinements]
tau_simulation [in LM.M_stack]
tau_terminating [in LM.M_stack]
tau_functional [in LM.M_stack]
tau_simulation [in LM.M_clos]
terminates_normalizes [in LM.Prelims]
termination_propagates [in LM.Refinements]
translateC_boundP [in LM.Closures]
U
unlinEnv_fuel [in LM.Extra]
unlinEnv_mono [in LM.Extra]
unlinPro_fuel [in LM.Extra]
unlinPro_mono [in LM.Extra]
upSim [in LM.Refinements]
Constructor Index
A
app [in LM.L]
appC [in LM.Codes]
appT [in LM.Programs]
B
bndApp [in LM.L]
bndlam [in LM.L]
bndvar [in LM.L]
boundC_C [in LM.Closures]
boundP_app [in LM.Programs]
boundP_lam [in LM.Programs]
boundP_var [in LM.Programs]
boundP_ret [in LM.Programs]
C
closC [in LM.Closures]
E
evaluates_S [in LM.Prelims]
evaluates_B [in LM.Prelims]
I
isAbstraction [in LM.L]
L
lam [in LM.L]
lamC [in LM.Codes]
lamT [in LM.Programs]
R
representsC [in LM.M_heap]
representsClos_C [in LM.Heaps]
representsEnvCons [in LM.Heaps]
representsEnvNil [in LM.Heaps]
representsProApp [in LM.Codes]
representsProLam [in LM.Codes]
representsProRet [in LM.Codes]
representsProVar [in LM.Codes]
retC [in LM.Codes]
retT [in LM.Programs]
S
starC [in LM.Extra]
starR [in LM.Extra]
stepLApp [in LM.L]
stepLAppL [in LM.L]
stepLAppR [in LM.L]
stepLs_there [in LM.M_stack]
stepL_here [in LM.M_stack]
stepS_nil [in LM.M_stack]
stepS_pushVal [in LM.M_stack]
stepS_betaC [in LM.M_stack]
step_beta [in LM.M_heap]
step_pushVal [in LM.M_heap]
step_load [in LM.M_heap]
step_nil [in LM.M_heap]
step_betaC [in LM.M_clos]
step_pushVal [in LM.M_clos]
step_load [in LM.M_clos]
step_nil [in LM.M_clos]
stuckL [in LM.L]
stuckLsHere [in LM.M_stack]
stuckLsThere [in LM.M_stack]
stuckR [in LM.L]
stuckVar [in LM.L]
T
terminatesC [in LM.Prelims]
V
var [in LM.L]
varC [in LM.Codes]
varT [in LM.Programs]
other
β [in LM.Refinements]
τ [in LM.Refinements]
Inductive Index
A
abstraction [in LM.L]
B
boundC [in LM.Closures]
boundL [in LM.L]
boundP [in LM.Programs]
C
Clo [in LM.Closures]
Com [in LM.Codes]
E
evaluates [in LM.Prelims]
L
label [in LM.Refinements]
P
Pro [in LM.Programs]
R
representsClos [in LM.Heaps]
representsEnv [in LM.Heaps]
representsPro [in LM.Codes]
repsHC [in LM.M_heap]
S
star [in LM.Extra]
stepC [in LM.M_clos]
stepH [in LM.M_heap]
stepL [in LM.L]
stepLs [in LM.M_stack]
stepS [in LM.M_stack]
stuck [in LM.L]
stuckLs [in LM.M_stack]
T
term [in LM.L]
terminatesOn [in LM.Prelims]
Projection Index
A
ARS_R [in LM.Prelims]
ARS_X [in LM.Prelims]
C
Code [in LM.Codes]
G
get [in LM.Heaps]
H
HA [in LM.Heaps]
Heap [in LM.Heaps]
HR1 [in LM.Heaps]
HR2 [in LM.Heaps]
I
inc [in LM.Codes]
M
M_rel [in LM.Refinements]
M_A [in LM.Refinements]
P
PA [in LM.Codes]
put [in LM.Heaps]
other
φ [in LM.Codes]
Instance Index
C
codeImpl [in LM.Codes]
H
heapImpl [in LM.Heaps]
N
nat_eq_dec [in LM.Prelims]
nat_le_dec [in LM.Prelims]
T
term_eq_dec [in LM.L]
Section Index
A
absSim [in LM.Refinements]
absSim.assume_refine.top_down [in LM.Refinements]
absSim.assume_refine.Correctness [in LM.Refinements]
absSim.assume_refine [in LM.Refinements]
absSim.refine_M [in LM.Refinements]
absSim.refine_ARS [in LM.Refinements]
H
heap [in LM.Heaps]
heap_decomp.unlinEnv [in LM.Extra]
heap_decomp.unlinPro [in LM.Extra]
heap_decomp [in LM.Extra]
L
Lin [in LM.M_heap]
Definition Index
A
any [in LM.Refinements]
C
classical [in LM.Prelims]
closedL [in LM.L]
closedP [in LM.Programs]
closedSC [in LM.M_clos]
computable [in LM.Prelims]
D
Dec [in LM.Prelims]
dec [in LM.Prelims]
E
exactlyOneHolds [in LM.Prelims]
F
functional [in LM.Prelims]
L
lookup [in LM.Heaps]
N
noneHolds [in LM.Prelims]
normalizes [in LM.Prelims]
R
rcomp [in LM.Prelims]
redL [in LM.L]
reducible [in LM.Prelims]
refinement_M [in LM.Refinements]
refinement_ARS [in LM.Refinements]
repsCL [in LM.M_clos]
repsCS [in LM.M_clos]
repsHL [in LM.M_heap]
repsP [in LM.Programs]
repsSL [in LM.M_stack]
S
state [in LM.M_heap]
stateC [in LM.M_clos]
stateS [in LM.M_stack]
stepFunction [in LM.Prelims]
subst [in LM.L]
substP [in LM.Programs]
substPl [in LM.Closures]
U
unlinClos [in LM.Extra]
unlinEnv [in LM.Extra]
unlinPro [in LM.Extra]
other
γ [in LM.Programs]
δC [in LM.Closures]
τβ_rel [in LM.Refinements]
ψ [in LM.Codes]
Record Index
A
ARS [in LM.Prelims]
C
code [in LM.Codes]
H
heap [in LM.Heaps]
M
Machine [in LM.Refinements]
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
(363 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
(79 entries)
Variable Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
_
other
(25 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
(12 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
(96 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
(57 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
(23 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
(14 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
(5 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
(11 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
(37 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
(4 entries)