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 _ (195 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (15 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 _ (114 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 _ (13 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 _ (6 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 _ (40 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 _ (6 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 _ (1 entry)

Global Index

A

alignof [axiom, in Memory]
alignof_div [axiom, in Memory]
alignof_pos [axiom, in Memory]


C

compat [axiom, in Memory]
compat_alignof [axiom, in Memory]
compat_dec [axiom, in Memory]
compat_sizeof [axiom, in Memory]
Concrete_Mem [module, in Memory]
Concrete_Mem.aligned_dec [lemma, in Memory]
Concrete_Mem.alloc [definition, in Memory]
Concrete_Mem.alloc_bounds_inv [lemma, in Memory]
Concrete_Mem.alloc_fresh_block [lemma, in Memory]
Concrete_Mem.alloc_fresh_block_2 [lemma, in Memory]
Concrete_Mem.alloc_not_valid_block [lemma, in Memory]
Concrete_Mem.alloc_result_bounds [lemma, in Memory]
Concrete_Mem.alloc_same_domain [lemma, in Memory]
Concrete_Mem.alloc_valid_block [lemma, in Memory]
Concrete_Mem.alloc_valid_pointer_inv [lemma, in Memory]
Concrete_Mem.block [definition, in Memory]
Concrete_Mem.check_cont [definition, in Memory]
Concrete_Mem.check_cont_charact [lemma, in Memory]
Concrete_Mem.check_cont_exten [lemma, in Memory]
Concrete_Mem.content [definition, in Memory]
Concrete_Mem.empty [definition, in Memory]
Concrete_Mem.eq_block [lemma, in Memory]
Concrete_Mem.free [definition, in Memory]
Concrete_Mem.free_bounds_inv [lemma, in Memory]
Concrete_Mem.free_fresh_block [lemma, in Memory]
Concrete_Mem.free_not_valid_block [lemma, in Memory]
Concrete_Mem.free_same_bounds [lemma, in Memory]
Concrete_Mem.free_valid_block [lemma, in Memory]
Concrete_Mem.free_valid_pointer_inv [lemma, in Memory]
Concrete_Mem.fresh_block [definition, in Memory]
Concrete_Mem.fresh_valid_block_exclusive [lemma, in Memory]
Concrete_Mem.load [definition, in Memory]
Concrete_Mem.load_alloc_other [lemma, in Memory]
Concrete_Mem.load_alloc_same [lemma, in Memory]
Concrete_Mem.load_contents [definition, in Memory]
Concrete_Mem.load_contents_exten [lemma, in Memory]
Concrete_Mem.load_contents_1 [lemma, in Memory]
Concrete_Mem.load_contents_2 [lemma, in Memory]
Concrete_Mem.load_contents_3 [lemma, in Memory]
Concrete_Mem.load_contents_4 [lemma, in Memory]
Concrete_Mem.load_free_other [lemma, in Memory]
Concrete_Mem.load_store_contents_disjoint [lemma, in Memory]
Concrete_Mem.load_store_contents_mismatch [lemma, in Memory]
Concrete_Mem.load_store_contents_overlap [lemma, in Memory]
Concrete_Mem.load_store_contents_same [lemma, in Memory]
Concrete_Mem.load_store_disjoint [lemma, in Memory]
Concrete_Mem.load_store_mismatch [lemma, in Memory]
Concrete_Mem.load_store_overlap [lemma, in Memory]
Concrete_Mem.load_store_same [lemma, in Memory]
Concrete_Mem.load_valid_block [lemma, in Memory]
Concrete_Mem.load_valid_pointer [lemma, in Memory]
Concrete_Mem.mem [definition, in Memory]
Concrete_Mem.mem_ [inductive, in Memory]
Concrete_Mem.nat_of_Z [definition, in Memory]
Concrete_Mem.nat_of_Z_eq [lemma, in Memory]
Concrete_Mem.same_domain [definition, in Memory]
Concrete_Mem.same_domain_same_nextblock [lemma, in Memory]
Concrete_Mem.set_cont [definition, in Memory]
Concrete_Mem.set_cont_inside [lemma, in Memory]
Concrete_Mem.set_cont_outside [lemma, in Memory]
Concrete_Mem.store [definition, in Memory]
Concrete_Mem.store_bounds_inv [lemma, in Memory]
Concrete_Mem.store_contents [definition, in Memory]
Concrete_Mem.store_contents_at [lemma, in Memory]
Concrete_Mem.store_contents_cont [lemma, in Memory]
Concrete_Mem.store_contents_outside [lemma, in Memory]
Concrete_Mem.store_fresh_block [lemma, in Memory]
Concrete_Mem.store_inversion [lemma, in Memory]
Concrete_Mem.store_valid_block [lemma, in Memory]
Concrete_Mem.store_valid_block_inv [lemma, in Memory]
Concrete_Mem.store_valid_pointer [lemma, in Memory]
Concrete_Mem.store_valid_pointer_inv [lemma, in Memory]
Concrete_Mem.valid_block [definition, in Memory]
Concrete_Mem.valid_block_dec [lemma, in Memory]
Concrete_Mem.valid_block_free [lemma, in Memory]
Concrete_Mem.valid_pointer [definition, in Memory]
Concrete_Mem.valid_pointer_compat [lemma, in Memory]
Concrete_Mem.valid_pointer_dec [lemma, in Memory]
Concrete_Mem.valid_pointer_load [lemma, in Memory]
Concrete_Mem.valid_pointer_store [lemma, in Memory]
convert [axiom, in Memory]


E

enough_free_memory [axiom, in Memory]


G

GEN_MEM [module, in Memory]
GEN_MEM.valid_pointer [definition, in Memory]
Gen_Mem_Facts [module, in Memory]
Gen_Mem_Facts.alloc_not_valid_block_2 [lemma, in Memory]
Gen_Mem_Facts.alloc_result_valid_pointer [lemma, in Memory]
Gen_Mem_Facts.alloc_valid_block_inv [lemma, in Memory]
Gen_Mem_Facts.alloc_valid_pointer_inv [lemma, in Memory]
Gen_Mem_Facts.free_valid_pointer_inv [lemma, in Memory]
Gen_Mem_Facts.loadv [definition, in Memory]
Gen_Mem_Facts.load_alloc_other_2 [lemma, in Memory]
Gen_Mem_Facts.storev [definition, in Memory]
Gen_Mem_Facts.store_valid_pointer_inv [lemma, in Memory]


M

max_alignment [axiom, in Memory]
Memory [library]
memtype [axiom, in Memory]


R

REF_GEN_MEM [module, in Memory]
REF_GEN_MEM.same_domain [definition, in Memory]
REF_GEN_MEM.valid_pointer [definition, in Memory]
Ref_Gen_Mem_Facts [module, in Memory]
Ref_Gen_Mem_Facts.free_not_valid_pointer [lemma, in Memory]
Ref_Gen_Mem_Facts.free_same_domain [lemma, in Memory]
Ref_Gen_Mem_Facts.load_alloc_same_2 [lemma, in Memory]
Ref_Gen_Mem_Facts.load_store_cases [inductive, in Memory]
Ref_Gen_Mem_Facts.load_store_characterization [lemma, in Memory]
Ref_Gen_Mem_Facts.load_store_classification [definition, in Memory]
Ref_Gen_Mem_Facts.load_store_mismatch_2 [lemma, in Memory]
Ref_Gen_Mem_Facts.load_store_overlap_2 [lemma, in Memory]
Ref_Gen_Mem_Facts.lsc_mismatch [constructor, in Memory]
Ref_Gen_Mem_Facts.lsc_other [constructor, in Memory]
Ref_Gen_Mem_Facts.lsc_overlap [constructor, in Memory]
Ref_Gen_Mem_Facts.lsc_similar [constructor, in Memory]
Ref_Gen_Mem_Facts.store_same_domain [lemma, in Memory]
Ref_Gen_Mem_Facts.store_valid_pointer_2 [lemma, in Memory]
Rel_Mem [module, in Memory]
Rel_Mem.alloc_extends [lemma, in Memory]
Rel_Mem.alloc_left_mapped_emb [lemma, in Memory]
Rel_Mem.alloc_left_mapped_inject [lemma, in Memory]
Rel_Mem.alloc_left_unmapped_emb [lemma, in Memory]
Rel_Mem.alloc_left_unmapped_inject [lemma, in Memory]
Rel_Mem.alloc_lessdef [lemma, in Memory]
Rel_Mem.alloc_list [definition, in Memory]
Rel_Mem.alloc_list_alloc_inject [lemma, in Memory]
Rel_Mem.alloc_list_left_inject [lemma, in Memory]
Rel_Mem.alloc_parallel_emb [lemma, in Memory]
Rel_Mem.alloc_right_emb [lemma, in Memory]
Rel_Mem.alloc_right_inject [lemma, in Memory]
Rel_Mem.delta [constructor, in Memory]
Rel_Mem.disjoint_req [inductive, in Memory]
Rel_Mem.disjoint_req_cons [constructor, in Memory]
Rel_Mem.disjoint_req_nil [constructor, in Memory]
Rel_Mem.embedding [definition, in Memory]
Rel_Mem.embedding_incr [definition, in Memory]
Rel_Mem.embedding_no_overlap [definition, in Memory]
Rel_Mem.embedding_no_overlap_free [lemma, in Memory]
Rel_Mem.embedding_no_overlap_free_list [lemma, in Memory]
Rel_Mem.emb_id [definition, in Memory]
Rel_Mem.extend_embedding [definition, in Memory]
Rel_Mem.extend_embedding_incr [lemma, in Memory]
Rel_Mem.free_extends [lemma, in Memory]
Rel_Mem.free_inject [lemma, in Memory]
Rel_Mem.free_left_emb [lemma, in Memory]
Rel_Mem.free_lessdef [lemma, in Memory]
Rel_Mem.free_list [definition, in Memory]
Rel_Mem.free_list_free_parallel_emb [lemma, in Memory]
Rel_Mem.free_list_left_emb [lemma, in Memory]
Rel_Mem.free_parallel_emb [lemma, in Memory]
Rel_Mem.free_right_emb [lemma, in Memory]
Rel_Mem.list_forall2 [inductive, in Memory]
Rel_Mem.list_forall2_cons [constructor, in Memory]
Rel_Mem.list_forall2_nil [constructor, in Memory]
Rel_Mem.loadv_inject [lemma, in Memory]
Rel_Mem.load_extends [lemma, in Memory]
Rel_Mem.load_inject [lemma, in Memory]
Rel_Mem.load_lessdef [lemma, in Memory]
Rel_Mem.mem_emb [definition, in Memory]
Rel_Mem.mem_extends [definition, in Memory]
Rel_Mem.mem_extends_refl [lemma, in Memory]
Rel_Mem.mem_extends_trans [lemma, in Memory]
Rel_Mem.mem_inject [inductive, in Memory]
Rel_Mem.mem_lessdef [definition, in Memory]
Rel_Mem.mem_lessdef_refl [lemma, in Memory]
Rel_Mem.mem_lessdef_trans [lemma, in Memory]
Rel_Mem.Some [constructor, in Memory]
Rel_Mem.Some [constructor, in Memory]
Rel_Mem.storev_inject [lemma, in Memory]
Rel_Mem.store_lessdef [lemma, in Memory]
Rel_Mem.store_mapped_emb [lemma, in Memory]
Rel_Mem.store_mapped_inject [lemma, in Memory]
Rel_Mem.store_outside_emb [lemma, in Memory]
Rel_Mem.store_outside_extends [lemma, in Memory]
Rel_Mem.store_unmapped_emb [lemma, in Memory]
Rel_Mem.store_unmapped_inject [lemma, in Memory]
Rel_Mem.store_within_extends [lemma, in Memory]
Rel_Mem.valid_pointer_emb [lemma, in Memory]
Rel_Mem.val_emb_id [definition, in Memory]
Rel_Mem.val_emb_lessdef [definition, in Memory]
Rel_Mem.val_lessdef [definition, in Memory]
Rel_Mem.wf_req [inductive, in Memory]
Rel_Mem.wf_req_cons [constructor, in Memory]
Rel_Mem.wf_req_nil [constructor, in Memory]


S

sizeof [axiom, in Memory]
sizeof_pos [axiom, in Memory]


U

update [definition, in Memory]
update_o [lemma, in Memory]
update_s [lemma, in Memory]


V

val [axiom, in Memory]
vundef [axiom, in Memory]


Z

zeq [definition, in Memory]
zle [definition, in Memory]
zlt [definition, in Memory]



Axiom Index

A

alignof [in Memory]
alignof_div [in Memory]
alignof_pos [in Memory]


C

compat [in Memory]
compat_alignof [in Memory]
compat_dec [in Memory]
compat_sizeof [in Memory]
convert [in Memory]


E

enough_free_memory [in Memory]


M

max_alignment [in Memory]
memtype [in Memory]


S

sizeof [in Memory]
sizeof_pos [in Memory]


V

val [in Memory]
vundef [in Memory]



Lemma Index

C

Concrete_Mem.aligned_dec [in Memory]
Concrete_Mem.alloc_bounds_inv [in Memory]
Concrete_Mem.alloc_fresh_block [in Memory]
Concrete_Mem.alloc_fresh_block_2 [in Memory]
Concrete_Mem.alloc_not_valid_block [in Memory]
Concrete_Mem.alloc_result_bounds [in Memory]
Concrete_Mem.alloc_same_domain [in Memory]
Concrete_Mem.alloc_valid_block [in Memory]
Concrete_Mem.alloc_valid_pointer_inv [in Memory]
Concrete_Mem.check_cont_charact [in Memory]
Concrete_Mem.check_cont_exten [in Memory]
Concrete_Mem.eq_block [in Memory]
Concrete_Mem.free_bounds_inv [in Memory]
Concrete_Mem.free_fresh_block [in Memory]
Concrete_Mem.free_not_valid_block [in Memory]
Concrete_Mem.free_same_bounds [in Memory]
Concrete_Mem.free_valid_block [in Memory]
Concrete_Mem.free_valid_pointer_inv [in Memory]
Concrete_Mem.fresh_valid_block_exclusive [in Memory]
Concrete_Mem.load_alloc_other [in Memory]
Concrete_Mem.load_alloc_same [in Memory]
Concrete_Mem.load_contents_exten [in Memory]
Concrete_Mem.load_contents_1 [in Memory]
Concrete_Mem.load_contents_2 [in Memory]
Concrete_Mem.load_contents_3 [in Memory]
Concrete_Mem.load_contents_4 [in Memory]
Concrete_Mem.load_free_other [in Memory]
Concrete_Mem.load_store_contents_disjoint [in Memory]
Concrete_Mem.load_store_contents_mismatch [in Memory]
Concrete_Mem.load_store_contents_overlap [in Memory]
Concrete_Mem.load_store_contents_same [in Memory]
Concrete_Mem.load_store_disjoint [in Memory]
Concrete_Mem.load_store_mismatch [in Memory]
Concrete_Mem.load_store_overlap [in Memory]
Concrete_Mem.load_store_same [in Memory]
Concrete_Mem.load_valid_block [in Memory]
Concrete_Mem.load_valid_pointer [in Memory]
Concrete_Mem.nat_of_Z_eq [in Memory]
Concrete_Mem.same_domain_same_nextblock [in Memory]
Concrete_Mem.set_cont_inside [in Memory]
Concrete_Mem.set_cont_outside [in Memory]
Concrete_Mem.store_bounds_inv [in Memory]
Concrete_Mem.store_contents_at [in Memory]
Concrete_Mem.store_contents_cont [in Memory]
Concrete_Mem.store_contents_outside [in Memory]
Concrete_Mem.store_fresh_block [in Memory]
Concrete_Mem.store_inversion [in Memory]
Concrete_Mem.store_valid_block [in Memory]
Concrete_Mem.store_valid_block_inv [in Memory]
Concrete_Mem.store_valid_pointer [in Memory]
Concrete_Mem.store_valid_pointer_inv [in Memory]
Concrete_Mem.valid_block_dec [in Memory]
Concrete_Mem.valid_block_free [in Memory]
Concrete_Mem.valid_pointer_compat [in Memory]
Concrete_Mem.valid_pointer_dec [in Memory]
Concrete_Mem.valid_pointer_load [in Memory]
Concrete_Mem.valid_pointer_store [in Memory]


G

Gen_Mem_Facts.alloc_not_valid_block_2 [in Memory]
Gen_Mem_Facts.alloc_result_valid_pointer [in Memory]
Gen_Mem_Facts.alloc_valid_block_inv [in Memory]
Gen_Mem_Facts.alloc_valid_pointer_inv [in Memory]
Gen_Mem_Facts.free_valid_pointer_inv [in Memory]
Gen_Mem_Facts.load_alloc_other_2 [in Memory]
Gen_Mem_Facts.store_valid_pointer_inv [in Memory]


R

Ref_Gen_Mem_Facts.free_not_valid_pointer [in Memory]
Ref_Gen_Mem_Facts.free_same_domain [in Memory]
Ref_Gen_Mem_Facts.load_alloc_same_2 [in Memory]
Ref_Gen_Mem_Facts.load_store_characterization [in Memory]
Ref_Gen_Mem_Facts.load_store_mismatch_2 [in Memory]
Ref_Gen_Mem_Facts.load_store_overlap_2 [in Memory]
Ref_Gen_Mem_Facts.store_same_domain [in Memory]
Ref_Gen_Mem_Facts.store_valid_pointer_2 [in Memory]
Rel_Mem.alloc_extends [in Memory]
Rel_Mem.alloc_left_mapped_emb [in Memory]
Rel_Mem.alloc_left_mapped_inject [in Memory]
Rel_Mem.alloc_left_unmapped_emb [in Memory]
Rel_Mem.alloc_left_unmapped_inject [in Memory]
Rel_Mem.alloc_lessdef [in Memory]
Rel_Mem.alloc_list_alloc_inject [in Memory]
Rel_Mem.alloc_list_left_inject [in Memory]
Rel_Mem.alloc_parallel_emb [in Memory]
Rel_Mem.alloc_right_emb [in Memory]
Rel_Mem.alloc_right_inject [in Memory]
Rel_Mem.embedding_no_overlap_free [in Memory]
Rel_Mem.embedding_no_overlap_free_list [in Memory]
Rel_Mem.extend_embedding_incr [in Memory]
Rel_Mem.free_extends [in Memory]
Rel_Mem.free_inject [in Memory]
Rel_Mem.free_left_emb [in Memory]
Rel_Mem.free_lessdef [in Memory]
Rel_Mem.free_list_free_parallel_emb [in Memory]
Rel_Mem.free_list_left_emb [in Memory]
Rel_Mem.free_parallel_emb [in Memory]
Rel_Mem.free_right_emb [in Memory]
Rel_Mem.loadv_inject [in Memory]
Rel_Mem.load_extends [in Memory]
Rel_Mem.load_inject [in Memory]
Rel_Mem.load_lessdef [in Memory]
Rel_Mem.mem_extends_refl [in Memory]
Rel_Mem.mem_extends_trans [in Memory]
Rel_Mem.mem_lessdef_refl [in Memory]
Rel_Mem.mem_lessdef_trans [in Memory]
Rel_Mem.storev_inject [in Memory]
Rel_Mem.store_lessdef [in Memory]
Rel_Mem.store_mapped_emb [in Memory]
Rel_Mem.store_mapped_inject [in Memory]
Rel_Mem.store_outside_emb [in Memory]
Rel_Mem.store_outside_extends [in Memory]
Rel_Mem.store_unmapped_emb [in Memory]
Rel_Mem.store_unmapped_inject [in Memory]
Rel_Mem.store_within_extends [in Memory]
Rel_Mem.valid_pointer_emb [in Memory]


U

update_o [in Memory]
update_s [in Memory]



Constructor Index

R

Ref_Gen_Mem_Facts.lsc_mismatch [in Memory]
Ref_Gen_Mem_Facts.lsc_other [in Memory]
Ref_Gen_Mem_Facts.lsc_overlap [in Memory]
Ref_Gen_Mem_Facts.lsc_similar [in Memory]
Rel_Mem.delta [in Memory]
Rel_Mem.disjoint_req_cons [in Memory]
Rel_Mem.disjoint_req_nil [in Memory]
Rel_Mem.list_forall2_cons [in Memory]
Rel_Mem.list_forall2_nil [in Memory]
Rel_Mem.Some [in Memory]
Rel_Mem.Some [in Memory]
Rel_Mem.wf_req_cons [in Memory]
Rel_Mem.wf_req_nil [in Memory]



Inductive Index

C

Concrete_Mem.mem_ [in Memory]


R

Ref_Gen_Mem_Facts.load_store_cases [in Memory]
Rel_Mem.disjoint_req [in Memory]
Rel_Mem.list_forall2 [in Memory]
Rel_Mem.mem_inject [in Memory]
Rel_Mem.wf_req [in Memory]



Definition Index

C

Concrete_Mem.alloc [in Memory]
Concrete_Mem.block [in Memory]
Concrete_Mem.check_cont [in Memory]
Concrete_Mem.content [in Memory]
Concrete_Mem.empty [in Memory]
Concrete_Mem.free [in Memory]
Concrete_Mem.fresh_block [in Memory]
Concrete_Mem.load [in Memory]
Concrete_Mem.load_contents [in Memory]
Concrete_Mem.mem [in Memory]
Concrete_Mem.nat_of_Z [in Memory]
Concrete_Mem.same_domain [in Memory]
Concrete_Mem.set_cont [in Memory]
Concrete_Mem.store [in Memory]
Concrete_Mem.store_contents [in Memory]
Concrete_Mem.valid_block [in Memory]
Concrete_Mem.valid_pointer [in Memory]


G

GEN_MEM.valid_pointer [in Memory]
Gen_Mem_Facts.loadv [in Memory]
Gen_Mem_Facts.storev [in Memory]


R

REF_GEN_MEM.same_domain [in Memory]
REF_GEN_MEM.valid_pointer [in Memory]
Ref_Gen_Mem_Facts.load_store_classification [in Memory]
Rel_Mem.alloc_list [in Memory]
Rel_Mem.embedding [in Memory]
Rel_Mem.embedding_incr [in Memory]
Rel_Mem.embedding_no_overlap [in Memory]
Rel_Mem.emb_id [in Memory]
Rel_Mem.extend_embedding [in Memory]
Rel_Mem.free_list [in Memory]
Rel_Mem.mem_emb [in Memory]
Rel_Mem.mem_extends [in Memory]
Rel_Mem.mem_lessdef [in Memory]
Rel_Mem.val_emb_id [in Memory]
Rel_Mem.val_emb_lessdef [in Memory]
Rel_Mem.val_lessdef [in Memory]


U

update [in Memory]


Z

zeq [in Memory]
zle [in Memory]
zlt [in Memory]



Module Index

C

Concrete_Mem [in Memory]


G

GEN_MEM [in Memory]
Gen_Mem_Facts [in Memory]


R

REF_GEN_MEM [in Memory]
Ref_Gen_Mem_Facts [in Memory]
Rel_Mem [in Memory]



Library Index

M

Memory



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 _ (195 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (15 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 _ (114 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 _ (13 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 _ (6 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 _ (40 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 _ (6 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 _ (1 entry)

This page has been generated by coqdoc