| 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 | (2070 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 | (72 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 | (22 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 | (312 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 | (28 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 | (711 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 | (97 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (80 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 | (16 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 | (137 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 | (24 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 | (69 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 | (436 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 | (64 entries) |
Global Index
A
AbsHeap [constructor, in LemmaOverloading.cancel2]AbsPts [constructor, in LemmaOverloading.cancel2]
abs_heap [record, in LemmaOverloading.cancel2]
abs_pts [record, in LemmaOverloading.cancel2]
AdmissibleClosure [section, in LemmaOverloading.domains]
AdmissibleClosure.T [variable, in LemmaOverloading.domains]
allC [lemma, in LemmaOverloading.stsep]
alloc [definition, in LemmaOverloading.stsep]
allocb [definition, in LemmaOverloading.stsep]
allocbP [lemma, in LemmaOverloading.stsep]
allocb_s [definition, in LemmaOverloading.stsep]
allocP [lemma, in LemmaOverloading.stsep]
alloc_s [definition, in LemmaOverloading.stsep]
all_tag [definition, in LemmaOverloading.auto]
andFp [lemma, in LemmaOverloading.rels]
andpF [lemma, in LemmaOverloading.rels]
andpT [lemma, in LemmaOverloading.rels]
andTp [lemma, in LemmaOverloading.rels]
And6 [constructor, in LemmaOverloading.prelude]
and6 [inductive, in LemmaOverloading.prelude]
and6P [lemma, in LemmaOverloading.prelude]
ans [inductive, in LemmaOverloading.stmod]
antiframe [lemma, in LemmaOverloading.stsep]
AppChain [section, in LemmaOverloading.domains]
AppChain.A [variable, in LemmaOverloading.domains]
AppChain.s [variable, in LemmaOverloading.domains]
AppChain.T [variable, in LemmaOverloading.domains]
Append [section, in LemmaOverloading.finmap]
Append.K [variable, in LemmaOverloading.finmap]
Append.V [variable, in LemmaOverloading.finmap]
app_cont [lemma, in LemmaOverloading.domains]
app_chain [definition, in LemmaOverloading.domains]
app_mono [lemma, in LemmaOverloading.domains]
assign [projection, in LemmaOverloading.auto]
ast [record, in LemmaOverloading.cancel]
Ast [constructor, in LemmaOverloading.cancel]
ast [projection, in LemmaOverloading.cancelCTC]
Ast [record, in LemmaOverloading.cancelCTC]
auto [lemma, in LemmaOverloading.auto]
auto [library]
B
BasePrograms [section, in LemmaOverloading.stmod]BasePrograms.A [variable, in LemmaOverloading.stmod]
BasePrograms.P [variable, in LemmaOverloading.stmod]
BasicProperties [section, in LemmaOverloading.domains]
BasicProperties [section, in LemmaOverloading.hprop]
BasicProperties.T [variable, in LemmaOverloading.domains]
bind [definition, in LemmaOverloading.stsep]
bindP [lemma, in LemmaOverloading.stsep]
bind_s [definition, in LemmaOverloading.stsep]
bla [lemma, in LemmaOverloading.xfindCTC]
blah [lemma, in LemmaOverloading.stlog]
blah2 [lemma, in LemmaOverloading.stlog]
BlockUpdate [section, in LemmaOverloading.heaps]
BlockUpdate.A [variable, in LemmaOverloading.heaps]
BndForm [constructor, in LemmaOverloading.stlogR]
bnd_gh1 [lemma, in LemmaOverloading.stlog]
bnd_gh [lemma, in LemmaOverloading.stlog]
bnd_throw [lemma, in LemmaOverloading.stlog]
bnd_dealloc [lemma, in LemmaOverloading.stlog]
bnd_allocb [lemma, in LemmaOverloading.stlog]
bnd_alloc [lemma, in LemmaOverloading.stlog]
bnd_write [lemma, in LemmaOverloading.stlog]
bnd_read [lemma, in LemmaOverloading.stlog]
bnd_ret [lemma, in LemmaOverloading.stlog]
bnd_do [lemma, in LemmaOverloading.stlog]
bnd_is_try [lemma, in LemmaOverloading.stlog]
bnd_deallocR [lemma, in LemmaOverloading.stlogCTC]
bnd_writeR [lemma, in LemmaOverloading.stlogCTC]
bnd_pivot [projection, in LemmaOverloading.stlogR]
bnd_form [record, in LemmaOverloading.stlogR]
bnd_gh1R [lemma, in LemmaOverloading.stlogR]
bnd_ghR [lemma, in LemmaOverloading.stlogR]
bnd_throwR [definition, in LemmaOverloading.stlogR]
bnd_deallocR [lemma, in LemmaOverloading.stlogR]
bnd_allocbR [definition, in LemmaOverloading.stlogR]
bnd_allocR [definition, in LemmaOverloading.stlogR]
bnd_writeR [lemma, in LemmaOverloading.stlogR]
bnd_readR [lemma, in LemmaOverloading.stlogR]
bnd_retR [definition, in LemmaOverloading.stlogR]
bnd_doR [lemma, in LemmaOverloading.stlogR]
bot_runs [lemma, in LemmaOverloading.stmod]
bound [lemma, in LemmaOverloading.stmod]
C
cancel [definition, in LemmaOverloading.terms]cancel [lemma, in LemmaOverloading.cancel2]
cancel [lemma, in LemmaOverloading.heaps]
cancel [library]
cancelCTC [library]
cancelD [abbreviation, in LemmaOverloading.cancelD]
cancelD [library]
cancelR [lemma, in LemmaOverloading.cancel]
cancelR [lemma, in LemmaOverloading.cancelCTC]
cancelT [lemma, in LemmaOverloading.heaps]
cancel_sound [lemma, in LemmaOverloading.terms]
cancel_sound' [lemma, in LemmaOverloading.terms]
cancel_ins [lemma, in LemmaOverloading.finmap]
cancel' [definition, in LemmaOverloading.terms]
cancel1 [lemma, in LemmaOverloading.cancel2]
cancel2 [lemma, in LemmaOverloading.cancel2]
cancel2 [library]
cexit1 [lemma, in LemmaOverloading.heaps]
cexit2 [lemma, in LemmaOverloading.heaps]
cexit3 [lemma, in LemmaOverloading.heaps]
chain [record, in LemmaOverloading.domains]
Chain [constructor, in LemmaOverloading.domains]
ChainCompose [section, in LemmaOverloading.domains]
ChainCompose.f1 [variable, in LemmaOverloading.domains]
ChainCompose.f2 [variable, in LemmaOverloading.domains]
ChainCompose.M1 [variable, in LemmaOverloading.domains]
ChainCompose.M2 [variable, in LemmaOverloading.domains]
ChainCompose.s [variable, in LemmaOverloading.domains]
ChainCompose.T1 [variable, in LemmaOverloading.domains]
ChainCompose.T2 [variable, in LemmaOverloading.domains]
ChainCompose.T3 [variable, in LemmaOverloading.domains]
ChainConst [section, in LemmaOverloading.domains]
ChainConst.T1 [variable, in LemmaOverloading.domains]
ChainConst.T2 [variable, in LemmaOverloading.domains]
ChainConst.y [variable, in LemmaOverloading.domains]
chainE [lemma, in LemmaOverloading.domains]
ChainId [section, in LemmaOverloading.domains]
ChainId.s [variable, in LemmaOverloading.domains]
ChainId.T [variable, in LemmaOverloading.domains]
Chains [section, in LemmaOverloading.domains]
Chains.T [variable, in LemmaOverloading.domains]
chain_clos_diag [lemma, in LemmaOverloading.domains]
chain_closI [lemma, in LemmaOverloading.domains]
chain_clos_mono [lemma, in LemmaOverloading.domains]
chain_clos_idemp [lemma, in LemmaOverloading.domains]
chain_closP [lemma, in LemmaOverloading.domains]
chain_clos_min [lemma, in LemmaOverloading.domains]
chain_clos_sub [lemma, in LemmaOverloading.domains]
chain_closure [definition, in LemmaOverloading.domains]
chain_closed [definition, in LemmaOverloading.domains]
chain_axiom [definition, in LemmaOverloading.domains]
check [record, in LemmaOverloading.noalias]
Check [constructor, in LemmaOverloading.noalias]
check [record, in LemmaOverloading.auto]
Check [constructor, in LemmaOverloading.auto]
check' [record, in LemmaOverloading.noalias]
Check' [constructor, in LemmaOverloading.noalias]
coerce [definition, in LemmaOverloading.prelude]
coerce2 [definition, in LemmaOverloading.prelude]
Coercions [section, in LemmaOverloading.prelude]
Coercions.T [variable, in LemmaOverloading.prelude]
Coercions2 [section, in LemmaOverloading.prelude]
Coercions2.T [variable, in LemmaOverloading.prelude]
coherent [definition, in LemmaOverloading.stmod]
compA [lemma, in LemmaOverloading.prelude]
compf1 [lemma, in LemmaOverloading.prelude]
comp_cont [lemma, in LemmaOverloading.domains]
comp_chainE [lemma, in LemmaOverloading.domains]
comp_mono [lemma, in LemmaOverloading.domains]
comp1f [lemma, in LemmaOverloading.prelude]
CondBool [section, in LemmaOverloading.stsep]
CondBool.A [variable, in LemmaOverloading.stsep]
CondBool.b [variable, in LemmaOverloading.stsep]
CondBool.s1 [variable, in LemmaOverloading.stsep]
CondBool.s2 [variable, in LemmaOverloading.stsep]
CondDecide [section, in LemmaOverloading.stsep]
CondDecide.A [variable, in LemmaOverloading.stsep]
CondDecide.b [variable, in LemmaOverloading.stsep]
CondDecide.p1 [variable, in LemmaOverloading.stsep]
CondDecide.p2 [variable, in LemmaOverloading.stsep]
CondDecide.s1 [variable, in LemmaOverloading.stsep]
CondDecide.s2 [variable, in LemmaOverloading.stsep]
CondNat [section, in LemmaOverloading.stsep]
CondNat.A [variable, in LemmaOverloading.stsep]
CondNat.n [variable, in LemmaOverloading.stsep]
CondNat.s1 [variable, in LemmaOverloading.stsep]
CondNat.s2 [variable, in LemmaOverloading.stsep]
CondOption [section, in LemmaOverloading.stsep]
CondOption.A [variable, in LemmaOverloading.stsep]
CondOption.B [variable, in LemmaOverloading.stsep]
CondOption.s1 [variable, in LemmaOverloading.stsep]
CondOption.s2 [variable, in LemmaOverloading.stsep]
CondOption.x [variable, in LemmaOverloading.stsep]
CondSeq [section, in LemmaOverloading.stsep]
CondSeq.A [variable, in LemmaOverloading.stsep]
CondSeq.B [variable, in LemmaOverloading.stsep]
CondSeq.s [variable, in LemmaOverloading.stsep]
CondSeq.s1 [variable, in LemmaOverloading.stsep]
CondSeq.s2 [variable, in LemmaOverloading.stsep]
congeqUh [lemma, in LemmaOverloading.heaps]
congUh [lemma, in LemmaOverloading.heaps]
conseq [definition, in LemmaOverloading.stsep]
conseq_refl [lemma, in LemmaOverloading.stsep]
conseq1 [abbreviation, in LemmaOverloading.stsep]
const_cont [lemma, in LemmaOverloading.domains]
const_chainE [lemma, in LemmaOverloading.domains]
const_chain [definition, in LemmaOverloading.domains]
const_chainP [lemma, in LemmaOverloading.domains]
const_mono [lemma, in LemmaOverloading.domains]
cont [abbreviation, in LemmaOverloading.stlog]
cont [abbreviation, in LemmaOverloading.stlogCTC]
cont [abbreviation, in LemmaOverloading.stlogR]
contE [lemma, in LemmaOverloading.domains]
Context [constructor, in LemmaOverloading.terms]
Continuity [section, in LemmaOverloading.domains]
Continuity.D1 [variable, in LemmaOverloading.domains]
Continuity.D2 [variable, in LemmaOverloading.domains]
Continuity.f [variable, in LemmaOverloading.domains]
continuous [definition, in LemmaOverloading.domains]
contV [lemma, in LemmaOverloading.prelude]
contVT [lemma, in LemmaOverloading.prelude]
cont_mono [lemma, in LemmaOverloading.domains]
countN_varfree [lemma, in LemmaOverloading.terms]
count0_hfree [lemma, in LemmaOverloading.terms]
count1_hfree [lemma, in LemmaOverloading.terms]
CPO [module, in LemmaOverloading.domains]
CPO.base [projection, in LemmaOverloading.domains]
CPO.class [definition, in LemmaOverloading.domains]
CPO.Class [constructor, in LemmaOverloading.domains]
CPO.ClassDef [section, in LemmaOverloading.domains]
CPO.ClassDef.cT [variable, in LemmaOverloading.domains]
CPO.ClassDef.T [variable, in LemmaOverloading.domains]
CPO.class_of [record, in LemmaOverloading.domains]
CPO.clone [definition, in LemmaOverloading.domains]
CPO.Exports [module, in LemmaOverloading.domains]
CPO.Exports.CPO [abbreviation, in LemmaOverloading.domains]
CPO.Exports.cpo [abbreviation, in LemmaOverloading.domains]
CPO.Exports.CPOMixin [abbreviation, in LemmaOverloading.domains]
CPO.Exports.Laws [section, in LemmaOverloading.domains]
CPO.Exports.Laws.D [variable, in LemmaOverloading.domains]
CPO.Exports.lim [abbreviation, in LemmaOverloading.domains]
CPO.Exports.limM [lemma, in LemmaOverloading.domains]
CPO.Exports.limP [lemma, in LemmaOverloading.domains]
[ cpo of _ ] (form_scope) [notation, in LemmaOverloading.domains]
[ cpo of _ for _ ] (form_scope) [notation, in LemmaOverloading.domains]
CPO.lim [definition, in LemmaOverloading.domains]
CPO.mixin [projection, in LemmaOverloading.domains]
CPO.Mixin [constructor, in LemmaOverloading.domains]
CPO.mixin_of [record, in LemmaOverloading.domains]
CPO.mx_lim [projection, in LemmaOverloading.domains]
CPO.pack [definition, in LemmaOverloading.domains]
CPO.Pack [constructor, in LemmaOverloading.domains]
CPO.poset [definition, in LemmaOverloading.domains]
CPO.RawMixin [section, in LemmaOverloading.domains]
CPO.sort [projection, in LemmaOverloading.domains]
CPO.type [record, in LemmaOverloading.domains]
ctx [record, in LemmaOverloading.terms]
D
DAppChain [section, in LemmaOverloading.domains]DAppChain.A [variable, in LemmaOverloading.domains]
DAppChain.s [variable, in LemmaOverloading.domains]
DAppChain.T [variable, in LemmaOverloading.domains]
dapp_cont [lemma, in LemmaOverloading.domains]
dapp_chain [definition, in LemmaOverloading.domains]
dapp_mono [lemma, in LemmaOverloading.domains]
dealloc [definition, in LemmaOverloading.stsep]
deallocP [lemma, in LemmaOverloading.stsep]
dealloc_s [definition, in LemmaOverloading.stsep]
Def [section, in LemmaOverloading.finmap]
def [definition, in LemmaOverloading.heaps]
Def [constructor, in LemmaOverloading.heaps]
default_tag [definition, in LemmaOverloading.cancelD]
defE [lemma, in LemmaOverloading.heaps]
defed [definition, in LemmaOverloading.stmod]
defF [lemma, in LemmaOverloading.heaps]
defFUn [lemma, in LemmaOverloading.heaps]
defPt [lemma, in LemmaOverloading.heaps]
defPtUn [lemma, in LemmaOverloading.heaps]
defPt_dom [lemma, in LemmaOverloading.heaps]
defPt_def [lemma, in LemmaOverloading.heaps]
defPt_null [lemma, in LemmaOverloading.heaps]
defR [lemma, in LemmaOverloading.terms]
defU [lemma, in LemmaOverloading.heaps]
defUn [lemma, in LemmaOverloading.heaps]
defUnF [lemma, in LemmaOverloading.heaps]
defUnhh [lemma, in LemmaOverloading.heaps]
defUnl [lemma, in LemmaOverloading.heaps]
defUnr [lemma, in LemmaOverloading.heaps]
defUn_spec [inductive, in LemmaOverloading.heaps]
def_runs [lemma, in LemmaOverloading.stmod]
def_strict [definition, in LemmaOverloading.stmod]
def_true [constructor, in LemmaOverloading.heaps]
def_false3 [constructor, in LemmaOverloading.heaps]
def_false2 [constructor, in LemmaOverloading.heaps]
def_false1 [constructor, in LemmaOverloading.heaps]
Def.K [variable, in LemmaOverloading.finmap]
Def.V [variable, in LemmaOverloading.finmap]
def0 [lemma, in LemmaOverloading.heaps]
def2 [definition, in LemmaOverloading.heaps]
dfunCPO [definition, in LemmaOverloading.domains]
DFunCPO [section, in LemmaOverloading.domains]
dfunCPOMixin [definition, in LemmaOverloading.domains]
DFunCPO.A [variable, in LemmaOverloading.domains]
DFunCPO.B [variable, in LemmaOverloading.domains]
dfunLattice [definition, in LemmaOverloading.domains]
DFunLattice [section, in LemmaOverloading.domains]
dfunLatticeMixin [definition, in LemmaOverloading.domains]
DFunLattice.A [variable, in LemmaOverloading.domains]
DFunLattice.B [variable, in LemmaOverloading.domains]
dfunPoset [definition, in LemmaOverloading.domains]
DFunPoset [section, in LemmaOverloading.domains]
dfunPosetMixin [definition, in LemmaOverloading.domains]
DFunPoset.A [variable, in LemmaOverloading.domains]
DFunPoset.B [variable, in LemmaOverloading.domains]
dfun_limM [lemma, in LemmaOverloading.domains]
dfun_limP [lemma, in LemmaOverloading.domains]
dfun_lim [definition, in LemmaOverloading.domains]
dfun_supM [lemma, in LemmaOverloading.domains]
dfun_supP [lemma, in LemmaOverloading.domains]
dfun_sup [definition, in LemmaOverloading.domains]
dfun_trans [lemma, in LemmaOverloading.domains]
dfun_asym [lemma, in LemmaOverloading.domains]
dfun_refl [lemma, in LemmaOverloading.domains]
dfun_botP [lemma, in LemmaOverloading.domains]
dfun_leq [definition, in LemmaOverloading.domains]
dfun_bot [definition, in LemmaOverloading.domains]
DiagChain [section, in LemmaOverloading.domains]
DiagChain.s [variable, in LemmaOverloading.domains]
DiagChain.T [variable, in LemmaOverloading.domains]
diag_cont [lemma, in LemmaOverloading.domains]
diag_chain [definition, in LemmaOverloading.domains]
diag_mono [lemma, in LemmaOverloading.domains]
disj [definition, in LemmaOverloading.finmap]
disjC [lemma, in LemmaOverloading.finmap]
DisjointUnion [section, in LemmaOverloading.finmap]
DisjointUnion.K [variable, in LemmaOverloading.finmap]
DisjointUnion.V [variable, in LemmaOverloading.finmap]
disjP [lemma, in LemmaOverloading.finmap]
disj_fcat [lemma, in LemmaOverloading.finmap]
disj_remE [lemma, in LemmaOverloading.finmap]
disj_rem [lemma, in LemmaOverloading.finmap]
disj_ins [lemma, in LemmaOverloading.finmap]
disj_nil [lemma, in LemmaOverloading.finmap]
disj_false [constructor, in LemmaOverloading.finmap]
disj_true [constructor, in LemmaOverloading.finmap]
disj_spec [inductive, in LemmaOverloading.finmap]
dom [definition, in LemmaOverloading.heaps]
domains [library]
domF [lemma, in LemmaOverloading.heaps]
domPt [lemma, in LemmaOverloading.heaps]
domPtUn [lemma, in LemmaOverloading.heaps]
domPtUnX [lemma, in LemmaOverloading.heaps]
domPtX [lemma, in LemmaOverloading.heaps]
domR [lemma, in LemmaOverloading.terms]
domU [lemma, in LemmaOverloading.heaps]
domUn [lemma, in LemmaOverloading.heaps]
dom_hfresh [lemma, in LemmaOverloading.heaps]
dom_lfresh [lemma, in LemmaOverloading.heaps]
dom_in_notin [lemma, in LemmaOverloading.heaps]
dom_notin_notin [lemma, in LemmaOverloading.heaps]
dom_fresh [lemma, in LemmaOverloading.heaps]
dom_look [lemma, in LemmaOverloading.heaps]
dom_free [lemma, in LemmaOverloading.heaps]
dom_def [lemma, in LemmaOverloading.heaps]
dom_null [lemma, in LemmaOverloading.heaps]
dom0 [lemma, in LemmaOverloading.heaps]
doP [lemma, in LemmaOverloading.stsep]
do' [definition, in LemmaOverloading.stsep]
dummy [projection, in LemmaOverloading.cancel2]
dyn [abbreviation, in LemmaOverloading.prelude]
Dyn [module, in LemmaOverloading.prelude]
dynamic [abbreviation, in LemmaOverloading.prelude]
dyneq_tag [definition, in LemmaOverloading.cancelD]
dyn_injT [lemma, in LemmaOverloading.prelude]
dyn_eta [lemma, in LemmaOverloading.prelude]
dyn_inj [lemma, in LemmaOverloading.prelude]
Dyn.dyn [constructor, in LemmaOverloading.prelude]
Dyn.dynamic [record, in LemmaOverloading.prelude]
Dyn.typ [projection, in LemmaOverloading.prelude]
Dyn.val [projection, in LemmaOverloading.prelude]
E
einterp [definition, in LemmaOverloading.terms]elem [inductive, in LemmaOverloading.terms]
elem_of [projection, in LemmaOverloading.xfind]
emp [definition, in LemmaOverloading.hprop]
empb [definition, in LemmaOverloading.heaps]
empbE [lemma, in LemmaOverloading.heaps]
empc [definition, in LemmaOverloading.terms]
empP [lemma, in LemmaOverloading.heaps]
empPt [lemma, in LemmaOverloading.heaps]
empty [definition, in LemmaOverloading.heaps]
empty_pf [lemma, in LemmaOverloading.cancel]
empty_tag [definition, in LemmaOverloading.cancel]
empty_hfree [lemma, in LemmaOverloading.terms]
empty_struct [instance, in LemmaOverloading.cancelCTC]
empU [lemma, in LemmaOverloading.heaps]
empUn [lemma, in LemmaOverloading.heaps]
emp_pick [lemma, in LemmaOverloading.heaps]
eqc [lemma, in LemmaOverloading.prelude]
eqc2 [lemma, in LemmaOverloading.prelude]
eqD [constructor, in LemmaOverloading.terms]
eqexn [definition, in LemmaOverloading.stmod]
eqexnP [lemma, in LemmaOverloading.stmod]
eqfun_trans [lemma, in LemmaOverloading.rels]
eqfun_sym [lemma, in LemmaOverloading.rels]
eqfun_refl [lemma, in LemmaOverloading.rels]
eqH [constructor, in LemmaOverloading.terms]
EqMem [definition, in LemmaOverloading.rels]
EqPred [definition, in LemmaOverloading.rels]
EqPredFun [definition, in LemmaOverloading.rels]
EqPredType [definition, in LemmaOverloading.rels]
EqPredType_trans [definition, in LemmaOverloading.rels]
EqPredType_trans' [lemma, in LemmaOverloading.rels]
EqPredType_sym [lemma, in LemmaOverloading.rels]
EqPredType_refl [lemma, in LemmaOverloading.rels]
EqSeq_Class [definition, in LemmaOverloading.rels]
EqSimplPred [definition, in LemmaOverloading.rels]
EqType [section, in LemmaOverloading.finmap]
EqType.K [variable, in LemmaOverloading.finmap]
EqType.V [variable, in LemmaOverloading.finmap]
Equate [constructor, in LemmaOverloading.auto]
equate_to [record, in LemmaOverloading.auto]
eqUh [lemma, in LemmaOverloading.heaps]
eqX [constructor, in LemmaOverloading.terms]
eq_ptrP [lemma, in LemmaOverloading.heaps]
eq_ptr [definition, in LemmaOverloading.heaps]
eta [lemma, in LemmaOverloading.prelude]
eval [definition, in LemmaOverloading.terms]
EvalAlloc [section, in LemmaOverloading.stlog]
EvalAlloc.A [variable, in LemmaOverloading.stlog]
EvalAlloc.B [variable, in LemmaOverloading.stlog]
EvalBlockAlloc [section, in LemmaOverloading.stlog]
EvalBlockAlloc.A [variable, in LemmaOverloading.stlog]
EvalBlockAlloc.B [variable, in LemmaOverloading.stlog]
EvalDealloc [section, in LemmaOverloading.stlog]
EvalDeallocR [section, in LemmaOverloading.stlogCTC]
EvalDeallocR [section, in LemmaOverloading.stlogR]
EvalDeallocR.A [variable, in LemmaOverloading.stlogCTC]
EvalDeallocR.A [variable, in LemmaOverloading.stlogR]
EvalDeallocR.B [variable, in LemmaOverloading.stlogCTC]
EvalDeallocR.B [variable, in LemmaOverloading.stlogR]
EvalDealloc.A [variable, in LemmaOverloading.stlog]
EvalDealloc.B [variable, in LemmaOverloading.stlog]
EvalDo [section, in LemmaOverloading.stlog]
EvalDoR [section, in LemmaOverloading.stlogCTC]
EvalDoR [section, in LemmaOverloading.stlogR]
EvalDoR.A [variable, in LemmaOverloading.stlogCTC]
EvalDoR.A [variable, in LemmaOverloading.stlogR]
EvalDoR.B [variable, in LemmaOverloading.stlogCTC]
EvalDoR.B [variable, in LemmaOverloading.stlogR]
EvalDo.A [variable, in LemmaOverloading.stlog]
EvalDo.B [variable, in LemmaOverloading.stlog]
EvalGhost [section, in LemmaOverloading.stlog]
EvalGhostR [section, in LemmaOverloading.stlogR]
EvalGhostR.A [variable, in LemmaOverloading.stlogR]
EvalGhostR.B [variable, in LemmaOverloading.stlogR]
EvalGhostR.C [variable, in LemmaOverloading.stlogR]
EvalGhostR.f [variable, in LemmaOverloading.stlogR]
EvalGhostR.i [variable, in LemmaOverloading.stlogR]
EvalGhostR.j [variable, in LemmaOverloading.stlogR]
EvalGhostR.P [variable, in LemmaOverloading.stlogR]
EvalGhostR.p [variable, in LemmaOverloading.stlogR]
EvalGhostR.q [variable, in LemmaOverloading.stlogR]
EvalGhostR.s1 [variable, in LemmaOverloading.stlogR]
EvalGhostR.s2 [variable, in LemmaOverloading.stlogR]
EvalGhostR.t [variable, in LemmaOverloading.stlogR]
EvalGhost.A [variable, in LemmaOverloading.stlog]
EvalGhost.B [variable, in LemmaOverloading.stlog]
EvalGhost.C [variable, in LemmaOverloading.stlog]
EvalGhost.i [variable, in LemmaOverloading.stlog]
EvalGhost.j [variable, in LemmaOverloading.stlog]
EvalGhost.P [variable, in LemmaOverloading.stlog]
EvalGhost.p [variable, in LemmaOverloading.stlog]
EvalGhost.q [variable, in LemmaOverloading.stlog]
EvalGhost.s1 [variable, in LemmaOverloading.stlog]
EvalGhost.s2 [variable, in LemmaOverloading.stlog]
EvalGhost.t [variable, in LemmaOverloading.stlog]
EvalRead [section, in LemmaOverloading.stlog]
EvalReadR [section, in LemmaOverloading.stlogR]
EvalReadR.A [variable, in LemmaOverloading.stlogR]
EvalReadR.B [variable, in LemmaOverloading.stlogR]
EvalRead.A [variable, in LemmaOverloading.stlog]
EvalRead.B [variable, in LemmaOverloading.stlog]
EvalReturn [section, in LemmaOverloading.stlog]
EvalReturn.A [variable, in LemmaOverloading.stlog]
EvalReturn.B [variable, in LemmaOverloading.stlog]
EvalThrow [section, in LemmaOverloading.stlog]
EvalThrow.A [variable, in LemmaOverloading.stlog]
EvalThrow.B [variable, in LemmaOverloading.stlog]
EvalWrite [section, in LemmaOverloading.stlog]
EvalWriteR [section, in LemmaOverloading.stlogCTC]
EvalWriteR [section, in LemmaOverloading.stlogR]
EvalWriteR.A [variable, in LemmaOverloading.stlogCTC]
EvalWriteR.A [variable, in LemmaOverloading.stlogR]
EvalWriteR.B [variable, in LemmaOverloading.stlogCTC]
EvalWriteR.B [variable, in LemmaOverloading.stlogR]
EvalWriteR.C [variable, in LemmaOverloading.stlogCTC]
EvalWriteR.C [variable, in LemmaOverloading.stlogR]
EvalWrite.A [variable, in LemmaOverloading.stlog]
EvalWrite.B [variable, in LemmaOverloading.stlog]
EvalWrite.C [variable, in LemmaOverloading.stlog]
eval_rcons [lemma, in LemmaOverloading.terms]
eval_cat [lemma, in LemmaOverloading.terms]
eval_cons [lemma, in LemmaOverloading.terms]
eval_fact [definition, in LemmaOverloading.terms]
exit1 [lemma, in LemmaOverloading.heaps]
exit2 [lemma, in LemmaOverloading.heaps]
exit3 [lemma, in LemmaOverloading.heaps]
exit4 [lemma, in LemmaOverloading.heaps]
Exn [constructor, in LemmaOverloading.stmod]
exn [inductive, in LemmaOverloading.stmod]
exnc [definition, in LemmaOverloading.noaliasCTC]
exnc [definition, in LemmaOverloading.noalias]
exnc [definition, in LemmaOverloading.noalias]
exnc [definition, in LemmaOverloading.noalias]
exnc [definition, in LemmaOverloading.noaliasBT]
exnc [definition, in LemmaOverloading.noaliasBT]
exn_to_nat [definition, in LemmaOverloading.stmod]
exn_from_nat [constructor, in LemmaOverloading.stmod]
ext [lemma, in LemmaOverloading.prelude]
extend_pf [lemma, in LemmaOverloading.xfind]
extend_tag [definition, in LemmaOverloading.xfind]
extend_struct [instance, in LemmaOverloading.xfindCTC]
ex_noalias2 [definition, in LemmaOverloading.noaliasCTC]
ex_noalias [definition, in LemmaOverloading.noaliasCTC]
ex_find2 [definition, in LemmaOverloading.noaliasCTC]
ex_find [definition, in LemmaOverloading.noaliasCTC]
ex_scan [definition, in LemmaOverloading.noaliasCTC]
ex_find2 [definition, in LemmaOverloading.noalias]
ex_find [definition, in LemmaOverloading.noalias]
ex_scan [definition, in LemmaOverloading.noalias]
ex_dealloc_bwd [definition, in LemmaOverloading.stlogCTC]
ex_fwd [definition, in LemmaOverloading.stlogCTC]
ex_bwd [definition, in LemmaOverloading.stlogCTC]
ex_val_do [definition, in LemmaOverloading.stlogCTC]
ex_fwd [definition, in LemmaOverloading.stlogR]
ex_bwd [definition, in LemmaOverloading.stlogR]
ex_val_do [definition, in LemmaOverloading.stlogR]
ex_read [definition, in LemmaOverloading.stlogR]
ex0 [definition, in LemmaOverloading.cancel]
ex1 [definition, in LemmaOverloading.cancel]
ex1 [definition, in LemmaOverloading.xfindCTC]
ex1 [definition, in LemmaOverloading.indom]
ex1 [definition, in LemmaOverloading.auto]
ex1 [definition, in LemmaOverloading.cancelCTC]
ex1 [definition, in LemmaOverloading.indomCTC]
ex1' [definition, in LemmaOverloading.cancel]
ex2 [definition, in LemmaOverloading.cancel]
ex2 [definition, in LemmaOverloading.indom]
ex2 [definition, in LemmaOverloading.auto]
ex2 [definition, in LemmaOverloading.cancelCTC]
ex2 [definition, in LemmaOverloading.indomCTC]
ex3 [definition, in LemmaOverloading.auto]
ex3 [definition, in LemmaOverloading.cancel2]
ex3 [definition, in LemmaOverloading.cancelD]
ex4 [definition, in LemmaOverloading.auto]
ex5 [definition, in LemmaOverloading.auto]
ex6 [definition, in LemmaOverloading.auto]
ex7 [definition, in LemmaOverloading.auto]
ex8 [definition, in LemmaOverloading.auto]
ex9 [definition, in LemmaOverloading.auto]
F
fact [inductive, in LemmaOverloading.terms]fcat [definition, in LemmaOverloading.finmap]
fcatA [lemma, in LemmaOverloading.finmap]
fcatAC [lemma, in LemmaOverloading.finmap]
fcatC [lemma, in LemmaOverloading.finmap]
fcatCA [lemma, in LemmaOverloading.finmap]
fcatKs [lemma, in LemmaOverloading.finmap]
fcatsK [lemma, in LemmaOverloading.finmap]
fcats0 [lemma, in LemmaOverloading.finmap]
fcat_srem [lemma, in LemmaOverloading.finmap]
fcat_rems [lemma, in LemmaOverloading.finmap]
fcat_sins [lemma, in LemmaOverloading.finmap]
fcat_inss [lemma, in LemmaOverloading.finmap]
fcat_nil' [lemma, in LemmaOverloading.finmap]
fcat_ins' [lemma, in LemmaOverloading.finmap]
fcat' [definition, in LemmaOverloading.finmap]
fcat0s [lemma, in LemmaOverloading.finmap]
feq [definition, in LemmaOverloading.finmap]
feqP [lemma, in LemmaOverloading.finmap]
fext [axiom, in LemmaOverloading.prelude]
ffound_struct1 [instance, in LemmaOverloading.stlogCTC]
find [record, in LemmaOverloading.indom]
find [record, in LemmaOverloading.auto]
Find [constructor, in LemmaOverloading.auto]
findme [lemma, in LemmaOverloading.xfind]
Find1 [record, in LemmaOverloading.stlogCTC]
find2E [lemma, in LemmaOverloading.noaliasCTC]
finMap [record, in LemmaOverloading.finmap]
FinMap [constructor, in LemmaOverloading.finmap]
finmap [library]
finMap_for [definition, in LemmaOverloading.finmap]
FinTypeOrd [section, in LemmaOverloading.ordtype]
FinTypeOrd.T [variable, in LemmaOverloading.ordtype]
fin_ordMixin [definition, in LemmaOverloading.ordtype]
Fix [definition, in LemmaOverloading.stsep]
fleft_struct1 [instance, in LemmaOverloading.stlogCTC]
fmap [abbreviation, in LemmaOverloading.finmap]
fmap [abbreviation, in LemmaOverloading.finmap]
fmap [abbreviation, in LemmaOverloading.finmap]
fmap [abbreviation, in LemmaOverloading.finmap]
fmap [abbreviation, in LemmaOverloading.finmap]
fmapE [lemma, in LemmaOverloading.finmap]
FMapInd [section, in LemmaOverloading.finmap]
FMapInd.K [variable, in LemmaOverloading.finmap]
FMapInd.V [variable, in LemmaOverloading.finmap]
fmapP [lemma, in LemmaOverloading.finmap]
fmap_ind2 [lemma, in LemmaOverloading.finmap]
fmap_ind' [lemma, in LemmaOverloading.finmap]
fnd [definition, in LemmaOverloading.finmap]
fnd_fcat [lemma, in LemmaOverloading.finmap]
fnd_supp_in [lemma, in LemmaOverloading.finmap]
fnd_supp [lemma, in LemmaOverloading.finmap]
fnd_ins [lemma, in LemmaOverloading.finmap]
fnd_rem [lemma, in LemmaOverloading.finmap]
fnd_empty [lemma, in LemmaOverloading.finmap]
Form [constructor, in LemmaOverloading.indom]
form [record, in LemmaOverloading.auto]
Form [constructor, in LemmaOverloading.auto]
form [record, in LemmaOverloading.cancelD]
Form [constructor, in LemmaOverloading.cancelD]
found [instance, in LemmaOverloading.indomCTC]
found_pf [lemma, in LemmaOverloading.xfind]
found_struct [instance, in LemmaOverloading.xfindCTC]
found_pf [lemma, in LemmaOverloading.indom]
found_right [instance, in LemmaOverloading.indomCTC]
found_left [instance, in LemmaOverloading.indomCTC]
found_struct [instance, in LemmaOverloading.stlogCTC]
found_pf [lemma, in LemmaOverloading.stlogR]
fprod [definition, in LemmaOverloading.prelude]
fr [definition, in LemmaOverloading.stsep]
frame [lemma, in LemmaOverloading.stsep]
frame0 [lemma, in LemmaOverloading.stsep]
frame1 [lemma, in LemmaOverloading.stsep]
free [definition, in LemmaOverloading.heaps]
freeF [lemma, in LemmaOverloading.heaps]
freePtUn [lemma, in LemmaOverloading.heaps]
freeR [lemma, in LemmaOverloading.terms]
freeU [lemma, in LemmaOverloading.heaps]
freeUn [lemma, in LemmaOverloading.heaps]
freeUnD [lemma, in LemmaOverloading.heaps]
freeUnl [lemma, in LemmaOverloading.heaps]
freeUnr [lemma, in LemmaOverloading.heaps]
free_nullP [lemma, in LemmaOverloading.heaps]
free0 [lemma, in LemmaOverloading.heaps]
fresh [definition, in LemmaOverloading.heaps]
fresh_null [lemma, in LemmaOverloading.heaps]
fright_struct1 [instance, in LemmaOverloading.stlogCTC]
fr_pre [lemma, in LemmaOverloading.stsep]
FunCPO [section, in LemmaOverloading.domains]
funCPOMixin [definition, in LemmaOverloading.domains]
FunCPO.A [variable, in LemmaOverloading.domains]
FunCPO.B [variable, in LemmaOverloading.domains]
FunLattice [section, in LemmaOverloading.domains]
funLatticeMixin [definition, in LemmaOverloading.domains]
FunLattice.A [variable, in LemmaOverloading.domains]
FunLattice.B [variable, in LemmaOverloading.domains]
FunPoset [section, in LemmaOverloading.domains]
funPosetMixin [definition, in LemmaOverloading.domains]
FunPoset.A [variable, in LemmaOverloading.domains]
FunPoset.B [variable, in LemmaOverloading.domains]
fun_limM [lemma, in LemmaOverloading.domains]
fun_limP [lemma, in LemmaOverloading.domains]
fun_lim [definition, in LemmaOverloading.domains]
fun_supM [lemma, in LemmaOverloading.domains]
fun_supP [lemma, in LemmaOverloading.domains]
fun_sup [definition, in LemmaOverloading.domains]
fun_trans [lemma, in LemmaOverloading.domains]
fun_asym [lemma, in LemmaOverloading.domains]
fun_refl [lemma, in LemmaOverloading.domains]
fun_botP [lemma, in LemmaOverloading.domains]
fun_leq [definition, in LemmaOverloading.domains]
fun_bot [definition, in LemmaOverloading.domains]
G
get_highs [definition, in LemmaOverloading.heaps]get_lows [definition, in LemmaOverloading.heaps]
gh [definition, in LemmaOverloading.stsep]
ghE [lemma, in LemmaOverloading.stsep]
Ghosts [section, in LemmaOverloading.stsep]
Ghosts.A [variable, in LemmaOverloading.stsep]
Ghosts.p [variable, in LemmaOverloading.stsep]
Ghosts.s [variable, in LemmaOverloading.stsep]
H
hasPx [lemma, in LemmaOverloading.prelude]HasSelect [section, in LemmaOverloading.prelude]
HasSelect.A [variable, in LemmaOverloading.prelude]
HasSelect.p [variable, in LemmaOverloading.prelude]
has_spec [definition, in LemmaOverloading.stmod]
has_false [constructor, in LemmaOverloading.prelude]
has_true [constructor, in LemmaOverloading.prelude]
has_spec [inductive, in LemmaOverloading.prelude]
hdom [definition, in LemmaOverloading.heaps]
hdomP [lemma, in LemmaOverloading.heaps]
heap [inductive, in LemmaOverloading.heaps]
heapE [lemma, in LemmaOverloading.heaps]
heapeq [record, in LemmaOverloading.cancel2]
HeapEq [constructor, in LemmaOverloading.cancel2]
HeapReflection [section, in LemmaOverloading.cancel]
heaps [library]
heap_of [projection, in LemmaOverloading.cancel]
heap_ctx [projection, in LemmaOverloading.terms]
heap_of [projection, in LemmaOverloading.indom]
heap_inv [definition, in LemmaOverloading.cancel2]
heap_h [projection, in LemmaOverloading.cancel2]
heap_etaP [lemma, in LemmaOverloading.heaps]
heap_eta [lemma, in LemmaOverloading.heaps]
heap_of [projection, in LemmaOverloading.stlogR]
heq1 [projection, in LemmaOverloading.stlogCTC]
hfree [definition, in LemmaOverloading.terms]
hfreeE [lemma, in LemmaOverloading.terms]
hfreeN [lemma, in LemmaOverloading.terms]
hfree_def [lemma, in LemmaOverloading.terms]
hfree_subdom' [lemma, in LemmaOverloading.terms]
hfree_subdom [lemma, in LemmaOverloading.terms]
hfresh [definition, in LemmaOverloading.heaps]
hfresh_null [lemma, in LemmaOverloading.heaps]
hfresh_high [lemma, in LemmaOverloading.heaps]
high [definition, in LemmaOverloading.heaps]
highPn [lemma, in LemmaOverloading.heaps]
highPtUn [lemma, in LemmaOverloading.heaps]
highPtUn2 [lemma, in LemmaOverloading.heaps]
high_lowD [lemma, in LemmaOverloading.heaps]
hlE [lemma, in LemmaOverloading.heaps]
hlook [definition, in LemmaOverloading.terms]
hprop [library]
hstep [definition, in LemmaOverloading.stlogR]
hstep_bnd [definition, in LemmaOverloading.stlogR]
I
iA [definition, in LemmaOverloading.prelude]ideal [record, in LemmaOverloading.domains]
Ideal [constructor, in LemmaOverloading.domains]
ideald [abbreviation, in LemmaOverloading.stmod]
IdealDef [section, in LemmaOverloading.domains]
IdealDef.T [variable, in LemmaOverloading.domains]
IdealLattice [section, in LemmaOverloading.domains]
idealLatticeMixin [definition, in LemmaOverloading.domains]
IdealLattice.P [variable, in LemmaOverloading.domains]
IdealLattice.T [variable, in LemmaOverloading.domains]
IdealPoset [section, in LemmaOverloading.domains]
idealPosetMixin [definition, in LemmaOverloading.domains]
IdealPoset.P [variable, in LemmaOverloading.domains]
IdealPoset.T [variable, in LemmaOverloading.domains]
ideal_supM [lemma, in LemmaOverloading.domains]
ideal_supP [lemma, in LemmaOverloading.domains]
ideal_sup [definition, in LemmaOverloading.domains]
ideal_supP' [lemma, in LemmaOverloading.domains]
ideal_sup' [definition, in LemmaOverloading.domains]
ideal_trans [lemma, in LemmaOverloading.domains]
ideal_asym [lemma, in LemmaOverloading.domains]
ideal_refl [lemma, in LemmaOverloading.domains]
ideal_botP [lemma, in LemmaOverloading.domains]
ideal_leq [definition, in LemmaOverloading.domains]
ideal_bot [definition, in LemmaOverloading.domains]
id_cont [lemma, in LemmaOverloading.domains]
id_chainE [lemma, in LemmaOverloading.domains]
id_mono [lemma, in LemmaOverloading.domains]
id_pf [projection, in LemmaOverloading.domains]
id_val [projection, in LemmaOverloading.domains]
If [definition, in LemmaOverloading.stsep]
ImageChain [section, in LemmaOverloading.domains]
ImageChain.f [variable, in LemmaOverloading.domains]
ImageChain.M [variable, in LemmaOverloading.domains]
ImageChain.s [variable, in LemmaOverloading.domains]
ImageChain.T1 [variable, in LemmaOverloading.domains]
ImageChain.T2 [variable, in LemmaOverloading.domains]
image_chain [definition, in LemmaOverloading.domains]
image_chainP [lemma, in LemmaOverloading.domains]
impC [lemma, in LemmaOverloading.stsep]
imp_tag [definition, in LemmaOverloading.auto]
index_of [projection, in LemmaOverloading.xfindCTC]
indom [lemma, in LemmaOverloading.indom]
indom [projection, in LemmaOverloading.indomCTC]
Indom [record, in LemmaOverloading.indomCTC]
indom [library]
indomCTC [library]
InE [definition, in LemmaOverloading.rels]
inf [definition, in LemmaOverloading.domains]
Infimum [section, in LemmaOverloading.domains]
Infimum.T [variable, in LemmaOverloading.domains]
infM [lemma, in LemmaOverloading.domains]
infP [lemma, in LemmaOverloading.domains]
injUh [lemma, in LemmaOverloading.heaps]
inj_sval [lemma, in LemmaOverloading.prelude]
inj_pair2 [definition, in LemmaOverloading.prelude]
InMem [definition, in LemmaOverloading.rels]
ins [definition, in LemmaOverloading.finmap]
insert [definition, in LemmaOverloading.llistR]
ins_ins [lemma, in LemmaOverloading.finmap]
ins_rem [lemma, in LemmaOverloading.finmap]
ins' [definition, in LemmaOverloading.finmap]
interp [definition, in LemmaOverloading.terms]
interp_subctx [lemma, in LemmaOverloading.terms]
interp_perm [lemma, in LemmaOverloading.terms]
interp_cat [lemma, in LemmaOverloading.terms]
interp_cons [lemma, in LemmaOverloading.terms]
invariant [definition, in LemmaOverloading.xfind]
invariant [definition, in LemmaOverloading.cancel]
invariant [definition, in LemmaOverloading.xfindCTC]
invariant [definition, in LemmaOverloading.indom]
invariant [definition, in LemmaOverloading.cancelCTC]
In_nil [lemma, in LemmaOverloading.rels]
In_cons [lemma, in LemmaOverloading.rels]
In_Simpl [lemma, in LemmaOverloading.rels]
in_split [lemma, in LemmaOverloading.perms]
irA [lemma, in LemmaOverloading.prelude]
irr [lemma, in LemmaOverloading.ordtype]
irr_ordf [lemma, in LemmaOverloading.ordtype]
irr_lex [lemma, in LemmaOverloading.ordtype]
irr_ltn_nat [lemma, in LemmaOverloading.ordtype]
isMem [definition, in LemmaOverloading.rels]
J
jmE [lemma, in LemmaOverloading.prelude]jmeq [definition, in LemmaOverloading.prelude]
jmeq_refl [lemma, in LemmaOverloading.prelude]
jmeq2 [definition, in LemmaOverloading.prelude]
jm2E [lemma, in LemmaOverloading.prelude]
K
key [abbreviation, in LemmaOverloading.finmap]key [definition, in LemmaOverloading.finmap]
Kleene [section, in LemmaOverloading.domains]
kleene_lfp_least [lemma, in LemmaOverloading.domains]
kleene_lfp_fixed [lemma, in LemmaOverloading.domains]
kleene_lfp [definition, in LemmaOverloading.domains]
Kleene.C [variable, in LemmaOverloading.domains]
Kleene.D [variable, in LemmaOverloading.domains]
Kleene.f [variable, in LemmaOverloading.domains]
L
last_ins' [lemma, in LemmaOverloading.finmap]last_inv [lemma, in LemmaOverloading.heaps]
Lat [section, in LemmaOverloading.domains]
latCPO [definition, in LemmaOverloading.domains]
latCPOMixin [definition, in LemmaOverloading.domains]
Lattice [module, in LemmaOverloading.domains]
LatticeCPO [section, in LemmaOverloading.domains]
LatticeCPO.A [variable, in LemmaOverloading.domains]
Lattice.base [projection, in LemmaOverloading.domains]
Lattice.class [definition, in LemmaOverloading.domains]
Lattice.Class [constructor, in LemmaOverloading.domains]
Lattice.ClassDef [section, in LemmaOverloading.domains]
Lattice.ClassDef.cT [variable, in LemmaOverloading.domains]
Lattice.ClassDef.T [variable, in LemmaOverloading.domains]
Lattice.class_of [record, in LemmaOverloading.domains]
Lattice.clone [definition, in LemmaOverloading.domains]
Lattice.Exports [module, in LemmaOverloading.domains]
Lattice.Exports.Lattice [abbreviation, in LemmaOverloading.domains]
Lattice.Exports.lattice [abbreviation, in LemmaOverloading.domains]
Lattice.Exports.LatticeMixin [abbreviation, in LemmaOverloading.domains]
Lattice.Exports.Laws [section, in LemmaOverloading.domains]
Lattice.Exports.Laws.T [variable, in LemmaOverloading.domains]
Lattice.Exports.sup [abbreviation, in LemmaOverloading.domains]
Lattice.Exports.supM [lemma, in LemmaOverloading.domains]
Lattice.Exports.supP [lemma, in LemmaOverloading.domains]
[ lattice of _ ] (form_scope) [notation, in LemmaOverloading.domains]
[ lattice of _ for _ ] (form_scope) [notation, in LemmaOverloading.domains]
Lattice.mixin [projection, in LemmaOverloading.domains]
Lattice.Mixin [constructor, in LemmaOverloading.domains]
Lattice.mixin_of [record, in LemmaOverloading.domains]
Lattice.mx_sup [projection, in LemmaOverloading.domains]
Lattice.pack [definition, in LemmaOverloading.domains]
Lattice.Pack [constructor, in LemmaOverloading.domains]
Lattice.poset [definition, in LemmaOverloading.domains]
Lattice.RawMixin [section, in LemmaOverloading.domains]
Lattice.RawMixin.T [variable, in LemmaOverloading.domains]
Lattice.sort [projection, in LemmaOverloading.domains]
Lattice.sup [definition, in LemmaOverloading.domains]
Lattice.type [record, in LemmaOverloading.domains]
lat_limM [lemma, in LemmaOverloading.domains]
lat_limP [lemma, in LemmaOverloading.domains]
lat_lim [definition, in LemmaOverloading.domains]
Lat.T [variable, in LemmaOverloading.domains]
Laws [section, in LemmaOverloading.finmap]
Laws.K [variable, in LemmaOverloading.finmap]
Laws.V [variable, in LemmaOverloading.finmap]
ldom [definition, in LemmaOverloading.heaps]
ldomK [lemma, in LemmaOverloading.heaps]
ldomP [lemma, in LemmaOverloading.heaps]
ldomUn [lemma, in LemmaOverloading.heaps]
left_pf [lemma, in LemmaOverloading.indom]
left_tag [definition, in LemmaOverloading.indom]
left_struct [instance, in LemmaOverloading.stlogCTC]
left_pf [lemma, in LemmaOverloading.stlogR]
left_tag [definition, in LemmaOverloading.stlogR]
Lemmas [section, in LemmaOverloading.ordtype]
Lemmas.T [variable, in LemmaOverloading.ordtype]
lex [definition, in LemmaOverloading.ordtype]
lfresh [definition, in LemmaOverloading.heaps]
lfresh_null [lemma, in LemmaOverloading.heaps]
lfresh_low [lemma, in LemmaOverloading.heaps]
lhE [lemma, in LemmaOverloading.heaps]
LiftChain [section, in LemmaOverloading.domains]
LiftChain.s [variable, in LemmaOverloading.domains]
LiftChain.T [variable, in LemmaOverloading.domains]
lift_chain [definition, in LemmaOverloading.domains]
lift_chainP [lemma, in LemmaOverloading.domains]
limE [lemma, in LemmaOverloading.domains]
lim_dappE [lemma, in LemmaOverloading.domains]
lim_appE [lemma, in LemmaOverloading.domains]
lim_liftE [lemma, in LemmaOverloading.domains]
lim_mono [lemma, in LemmaOverloading.domains]
ListMembership [section, in LemmaOverloading.rels]
ListMembership.T [variable, in LemmaOverloading.rels]
llist [abbreviation, in LemmaOverloading.llistR]
LList [section, in LemmaOverloading.llistR]
llist [definition, in LemmaOverloading.llistR]
llistR [library]
LList.T [variable, in LemmaOverloading.llistR]
locality [lemma, in LemmaOverloading.stsep]
lolli [definition, in LemmaOverloading.stsep]
look [definition, in LemmaOverloading.heaps]
lookF [lemma, in LemmaOverloading.heaps]
lookPtUn [lemma, in LemmaOverloading.heaps]
lookR [lemma, in LemmaOverloading.terms]
lookU [lemma, in LemmaOverloading.heaps]
lookUnl [lemma, in LemmaOverloading.heaps]
lookUnr [lemma, in LemmaOverloading.heaps]
low [definition, in LemmaOverloading.heaps]
loweq [definition, in LemmaOverloading.heaps]
loweqE [lemma, in LemmaOverloading.heaps]
loweqK [lemma, in LemmaOverloading.heaps]
loweqP [lemma, in LemmaOverloading.heaps]
lowPn [lemma, in LemmaOverloading.heaps]
lowPtUn [lemma, in LemmaOverloading.heaps]
lowUn [lemma, in LemmaOverloading.heaps]
low_trans [lemma, in LemmaOverloading.heaps]
low_sym [lemma, in LemmaOverloading.heaps]
low_refl [lemma, in LemmaOverloading.heaps]
lseg [definition, in LemmaOverloading.llistR]
lseg_case [lemma, in LemmaOverloading.llistR]
lseg_empty [lemma, in LemmaOverloading.llistR]
lseg_neq [lemma, in LemmaOverloading.llistR]
lseg_null [lemma, in LemmaOverloading.llistR]
lseg_add_last [lemma, in LemmaOverloading.llistR]
lseq [definition, in LemmaOverloading.llistR]
lseq_pos [lemma, in LemmaOverloading.llistR]
lseq_null [lemma, in LemmaOverloading.llistR]
ltn_ptr_total [lemma, in LemmaOverloading.heaps]
ltn_ptr_trans [lemma, in LemmaOverloading.heaps]
ltn_ptr_irr [lemma, in LemmaOverloading.heaps]
ltn_ptr [definition, in LemmaOverloading.heaps]
M
Match_seq [definition, in LemmaOverloading.stsep]Match_nat [definition, in LemmaOverloading.stsep]
Match_dec [definition, in LemmaOverloading.stsep]
Match_opt [definition, in LemmaOverloading.stsep]
Mem [definition, in LemmaOverloading.rels]
MemE [definition, in LemmaOverloading.rels]
MemProp [constructor, in LemmaOverloading.rels]
Mem_Seq1 [lemma, in LemmaOverloading.rels]
Mem_Seq [definition, in LemmaOverloading.rels]
Mem_Mem [lemma, in LemmaOverloading.rels]
Mem_Simpl [lemma, in LemmaOverloading.rels]
Mem_toPred [lemma, in LemmaOverloading.rels]
Mem_Pred [inductive, in LemmaOverloading.rels]
mkPredType [definition, in LemmaOverloading.rels]
Model [module, in LemmaOverloading.stmod]
model [projection, in LemmaOverloading.stmod]
modelE [lemma, in LemmaOverloading.stmod]
model_runs [lemma, in LemmaOverloading.stmod]
Model.alloc [definition, in LemmaOverloading.stmod]
Model.Allocation [section, in LemmaOverloading.stmod]
Model.Allocation.A [variable, in LemmaOverloading.stmod]
Model.Allocation.v [variable, in LemmaOverloading.stmod]
Model.allocb [definition, in LemmaOverloading.stmod]
Model.allocb_has_spec [lemma, in LemmaOverloading.stmod]
Model.allocb_dstrict [lemma, in LemmaOverloading.stmod]
Model.allocb_coherent [lemma, in LemmaOverloading.stmod]
Model.allocb_sp [definition, in LemmaOverloading.stmod]
Model.allocb_s [definition, in LemmaOverloading.stmod]
Model.alloc_has_spec [lemma, in LemmaOverloading.stmod]
Model.alloc_dstrict [lemma, in LemmaOverloading.stmod]
Model.alloc_coherent [lemma, in LemmaOverloading.stmod]
Model.alloc_sp [definition, in LemmaOverloading.stmod]
Model.alloc_s [definition, in LemmaOverloading.stmod]
Model.bind [definition, in LemmaOverloading.stmod]
Model.Bind [section, in LemmaOverloading.stmod]
Model.bind_has_spec [lemma, in LemmaOverloading.stmod]
Model.bind_dstrict [lemma, in LemmaOverloading.stmod]
Model.bind_coherent [lemma, in LemmaOverloading.stmod]
Model.bind_sp [definition, in LemmaOverloading.stmod]
Model.bind_s [definition, in LemmaOverloading.stmod]
Model.bind_post [definition, in LemmaOverloading.stmod]
Model.bind_pre [definition, in LemmaOverloading.stmod]
Model.Bind.A [variable, in LemmaOverloading.stmod]
Model.Bind.B [variable, in LemmaOverloading.stmod]
Model.Bind.e1 [variable, in LemmaOverloading.stmod]
Model.Bind.e2 [variable, in LemmaOverloading.stmod]
Model.Bind.s1 [variable, in LemmaOverloading.stmod]
Model.Bind.s2 [variable, in LemmaOverloading.stmod]
Model.BlockAllocation [section, in LemmaOverloading.stmod]
Model.BlockAllocation.A [variable, in LemmaOverloading.stmod]
Model.BlockAllocation.n [variable, in LemmaOverloading.stmod]
Model.BlockAllocation.v [variable, in LemmaOverloading.stmod]
Model.conseq [definition, in LemmaOverloading.stmod]
Model.Consequence [section, in LemmaOverloading.stmod]
Model.Consequence.A [variable, in LemmaOverloading.stmod]
Model.Consequence.e [variable, in LemmaOverloading.stmod]
Model.Consequence.pf [variable, in LemmaOverloading.stmod]
Model.Consequence.s1 [variable, in LemmaOverloading.stmod]
Model.Consequence.s2 [variable, in LemmaOverloading.stmod]
Model.conseq_refl [lemma, in LemmaOverloading.stmod]
Model.dealloc [definition, in LemmaOverloading.stmod]
Model.Deallocation [section, in LemmaOverloading.stmod]
Model.Deallocation.x [variable, in LemmaOverloading.stmod]
Model.dealloc_has_spec [lemma, in LemmaOverloading.stmod]
Model.dealloc_dstrict [lemma, in LemmaOverloading.stmod]
Model.dealloc_coherent [lemma, in LemmaOverloading.stmod]
Model.dealloc_sp [definition, in LemmaOverloading.stmod]
Model.dealloc_s [definition, in LemmaOverloading.stmod]
Model.Do [definition, in LemmaOverloading.stmod]
Model.do_has_spec [lemma, in LemmaOverloading.stmod]
Model.do_dstrict [lemma, in LemmaOverloading.stmod]
Model.do_coherent [lemma, in LemmaOverloading.stmod]
Model.do_sp [definition, in LemmaOverloading.stmod]
Model.ffix [definition, in LemmaOverloading.stmod]
Model.Fix [section, in LemmaOverloading.stmod]
Model.Fix.A [variable, in LemmaOverloading.stmod]
Model.Fix.B [variable, in LemmaOverloading.stmod]
Model.Fix.f [variable, in LemmaOverloading.stmod]
Model.Fix.s [variable, in LemmaOverloading.stmod]
Model.f' [definition, in LemmaOverloading.stmod]
Model.lat [abbreviation, in LemmaOverloading.stmod]
Model.read [definition, in LemmaOverloading.stmod]
Model.Read [section, in LemmaOverloading.stmod]
Model.read_has_spec [lemma, in LemmaOverloading.stmod]
Model.read_dstrict [lemma, in LemmaOverloading.stmod]
Model.read_coherent [lemma, in LemmaOverloading.stmod]
Model.read_sp [definition, in LemmaOverloading.stmod]
Model.read_s [definition, in LemmaOverloading.stmod]
Model.Read.A [variable, in LemmaOverloading.stmod]
Model.Read.x [variable, in LemmaOverloading.stmod]
Model.ret [definition, in LemmaOverloading.stmod]
Model.Return [section, in LemmaOverloading.stmod]
Model.Return.A [variable, in LemmaOverloading.stmod]
Model.Return.x [variable, in LemmaOverloading.stmod]
Model.ret_has_spec [lemma, in LemmaOverloading.stmod]
Model.ret_dstrict [lemma, in LemmaOverloading.stmod]
Model.ret_coherent [lemma, in LemmaOverloading.stmod]
Model.ret_sp [definition, in LemmaOverloading.stmod]
Model.ret_s [definition, in LemmaOverloading.stmod]
Model.throw [definition, in LemmaOverloading.stmod]
Model.Throw [section, in LemmaOverloading.stmod]
Model.throw_has_spec [lemma, in LemmaOverloading.stmod]
Model.throw_dstrict [lemma, in LemmaOverloading.stmod]
Model.throw_coherent [lemma, in LemmaOverloading.stmod]
Model.throw_sp [definition, in LemmaOverloading.stmod]
Model.throw_s [definition, in LemmaOverloading.stmod]
Model.Throw.A [variable, in LemmaOverloading.stmod]
Model.Throw.e [variable, in LemmaOverloading.stmod]
Model.tp [abbreviation, in LemmaOverloading.stmod]
Model.try [definition, in LemmaOverloading.stmod]
Model.Try [section, in LemmaOverloading.stmod]
Model.try_has_spec [lemma, in LemmaOverloading.stmod]
Model.try_dstrict [lemma, in LemmaOverloading.stmod]
Model.try_coherent [lemma, in LemmaOverloading.stmod]
Model.try_sp [definition, in LemmaOverloading.stmod]
Model.try_s [definition, in LemmaOverloading.stmod]
Model.try_post [definition, in LemmaOverloading.stmod]
Model.try_pre [definition, in LemmaOverloading.stmod]
Model.Try.A [variable, in LemmaOverloading.stmod]
Model.Try.B [variable, in LemmaOverloading.stmod]
Model.Try.e [variable, in LemmaOverloading.stmod]
Model.Try.e1 [variable, in LemmaOverloading.stmod]
Model.Try.e2 [variable, in LemmaOverloading.stmod]
Model.Try.s [variable, in LemmaOverloading.stmod]
Model.Try.s1 [variable, in LemmaOverloading.stmod]
Model.Try.s2 [variable, in LemmaOverloading.stmod]
Model.write [definition, in LemmaOverloading.stmod]
Model.Write [section, in LemmaOverloading.stmod]
Model.write_has_spec [lemma, in LemmaOverloading.stmod]
Model.write_dstrict [lemma, in LemmaOverloading.stmod]
Model.write_coherent [lemma, in LemmaOverloading.stmod]
Model.write_sp [definition, in LemmaOverloading.stmod]
Model.write_s [definition, in LemmaOverloading.stmod]
Model.Write.A [variable, in LemmaOverloading.stmod]
Model.Write.v [variable, in LemmaOverloading.stmod]
Model.Write.x [variable, in LemmaOverloading.stmod]
modnS [lemma, in LemmaOverloading.heaps]
monotone [definition, in LemmaOverloading.domains]
N
NatChain [section, in LemmaOverloading.domains]NatOrd [section, in LemmaOverloading.ordtype]
NatPoset [section, in LemmaOverloading.domains]
natPosetMixin [definition, in LemmaOverloading.domains]
nat_chain [definition, in LemmaOverloading.domains]
nat_chain_axiom [lemma, in LemmaOverloading.domains]
nat_trans [lemma, in LemmaOverloading.domains]
nat_asym [lemma, in LemmaOverloading.domains]
nat_refl [lemma, in LemmaOverloading.domains]
nat_botP [lemma, in LemmaOverloading.domains]
nat_ordMixin [definition, in LemmaOverloading.ordtype]
nat_ptr [definition, in LemmaOverloading.heaps]
nil [abbreviation, in LemmaOverloading.finmap]
nil [abbreviation, in LemmaOverloading.finmap]
nil [abbreviation, in LemmaOverloading.finmap]
nil [abbreviation, in LemmaOverloading.finmap]
nil [definition, in LemmaOverloading.finmap]
NoAlias [module, in LemmaOverloading.noalias]
noalias [lemma, in LemmaOverloading.heaps]
noalias [library]
noaliasBT [library]
noaliasCTC [library]
noaliasR [lemma, in LemmaOverloading.noaliasCTC]
noaliasR [lemma, in LemmaOverloading.noalias]
noaliasR [lemma, in LemmaOverloading.noaliasBT]
noaliasR_fwd3' [lemma, in LemmaOverloading.noalias]
noaliasR_fwd3 [lemma, in LemmaOverloading.noalias]
noaliasR_fwd' [abbreviation, in LemmaOverloading.noalias]
noaliasR_fwd_wrong1 [lemma, in LemmaOverloading.noalias]
noaliasR_fwd [abbreviation, in LemmaOverloading.noalias]
noaliasR_fwd1 [lemma, in LemmaOverloading.noalias]
noaliasR2 [lemma, in LemmaOverloading.noaliasBT]
NoAlias.Exports [module, in LemmaOverloading.noalias]
NoAlias.form [record, in LemmaOverloading.noalias]
NoAlias.Form [constructor, in LemmaOverloading.noalias]
NoAlias.NoAliasSection [section, in LemmaOverloading.noalias]
NoAlias.noalias_pf [lemma, in LemmaOverloading.noalias]
NoAlias.singleton [definition, in LemmaOverloading.noalias]
NoAlias.Tag [constructor, in LemmaOverloading.noalias]
NoAlias.tagged_ptr [record, in LemmaOverloading.noalias]
NoAlias.untag [projection, in LemmaOverloading.noalias]
NoAlias.y_of [projection, in LemmaOverloading.noalias]
NoAlias2 [module, in LemmaOverloading.noaliasBT]
NoAlias2.eq_of [projection, in LemmaOverloading.noaliasBT]
NoAlias2.Exports [module, in LemmaOverloading.noaliasBT]
NoAlias2.form [record, in LemmaOverloading.noaliasBT]
NoAlias2.Form [constructor, in LemmaOverloading.noaliasBT]
NoAlias2.NoAlias2Section [section, in LemmaOverloading.noaliasBT]
NoAlias2.start_pf [lemma, in LemmaOverloading.noaliasBT]
NoAlias2.Tag [constructor, in LemmaOverloading.noaliasBT]
NoAlias2.tagged_bool [record, in LemmaOverloading.noaliasBT]
NoAlias2.untag [projection, in LemmaOverloading.noaliasBT]
NoAlias3 [module, in LemmaOverloading.noaliasBT]
NoAlias3.Exports [module, in LemmaOverloading.noaliasBT]
NoAlias3.form [record, in LemmaOverloading.noaliasBT]
NoAlias3.Form [constructor, in LemmaOverloading.noaliasBT]
NoAlias3.noalias_pf [lemma, in LemmaOverloading.noaliasBT]
NoAlias3.NoAlias3Section [section, in LemmaOverloading.noaliasBT]
NoAlias3.y_of [projection, in LemmaOverloading.noaliasBT]
notin_filter [lemma, in LemmaOverloading.finmap]
notin_path [lemma, in LemmaOverloading.finmap]
nsym [lemma, in LemmaOverloading.ordtype]
null [definition, in LemmaOverloading.heaps]
NullLemmas [section, in LemmaOverloading.heaps]
NullLemmas.d [variable, in LemmaOverloading.heaps]
NullLemmas.f [variable, in LemmaOverloading.heaps]
NullLemmas.g [variable, in LemmaOverloading.heaps]
NullLemmas.x [variable, in LemmaOverloading.heaps]
O
onth [definition, in LemmaOverloading.prefix]onth_size [lemma, in LemmaOverloading.prefix]
opn [lemma, in LemmaOverloading.stlog]
Ops [section, in LemmaOverloading.finmap]
Ops.K [variable, in LemmaOverloading.finmap]
Ops.V [variable, in LemmaOverloading.finmap]
Ordered [module, in LemmaOverloading.ordtype]
Ordered.base [projection, in LemmaOverloading.ordtype]
Ordered.class [definition, in LemmaOverloading.ordtype]
Ordered.Class [constructor, in LemmaOverloading.ordtype]
Ordered.ClassDef [section, in LemmaOverloading.ordtype]
Ordered.ClassDef.cT [variable, in LemmaOverloading.ordtype]
Ordered.ClassDef.T [variable, in LemmaOverloading.ordtype]
Ordered.class_of [record, in LemmaOverloading.ordtype]
Ordered.clone [definition, in LemmaOverloading.ordtype]
Ordered.eqType [definition, in LemmaOverloading.ordtype]
Ordered.Exports [module, in LemmaOverloading.ordtype]
Ordered.Exports.ord [definition, in LemmaOverloading.ordtype]
Ordered.Exports.OrdMixin [abbreviation, in LemmaOverloading.ordtype]
Ordered.Exports.OrdType [abbreviation, in LemmaOverloading.ordtype]
Ordered.Exports.ordType [abbreviation, in LemmaOverloading.ordtype]
[ ordType of _ ] (form_scope) [notation, in LemmaOverloading.ordtype]
[ ordType of _ for _ ] (form_scope) [notation, in LemmaOverloading.ordtype]
Ordered.mixin [projection, in LemmaOverloading.ordtype]
Ordered.Mixin [constructor, in LemmaOverloading.ordtype]
Ordered.mixin_of [record, in LemmaOverloading.ordtype]
Ordered.ordering [projection, in LemmaOverloading.ordtype]
Ordered.pack [definition, in LemmaOverloading.ordtype]
Ordered.Pack [constructor, in LemmaOverloading.ordtype]
Ordered.RawMixin [section, in LemmaOverloading.ordtype]
Ordered.sort [projection, in LemmaOverloading.ordtype]
Ordered.type [record, in LemmaOverloading.ordtype]
ordf [definition, in LemmaOverloading.ordtype]
ordinal_ordMixin [definition, in LemmaOverloading.ordtype]
ordtype [library]
ord_path [lemma, in LemmaOverloading.finmap]
orFp [lemma, in LemmaOverloading.rels]
orL_tag [definition, in LemmaOverloading.auto]
orpF [lemma, in LemmaOverloading.rels]
orpT [lemma, in LemmaOverloading.rels]
orrA [lemma, in LemmaOverloading.rels]
orrAb [lemma, in LemmaOverloading.rels]
orrAC [lemma, in LemmaOverloading.rels]
orrC [lemma, in LemmaOverloading.rels]
orrCA [lemma, in LemmaOverloading.rels]
orrI [lemma, in LemmaOverloading.rels]
orR_tag [definition, in LemmaOverloading.auto]
orr0 [lemma, in LemmaOverloading.rels]
orTp [lemma, in LemmaOverloading.rels]
or0r [lemma, in LemmaOverloading.rels]
or5 [inductive, in LemmaOverloading.prelude]
or5P [lemma, in LemmaOverloading.prelude]
Or51 [constructor, in LemmaOverloading.prelude]
Or52 [constructor, in LemmaOverloading.prelude]
Or53 [constructor, in LemmaOverloading.prelude]
Or54 [constructor, in LemmaOverloading.prelude]
Or55 [constructor, in LemmaOverloading.prelude]
or6 [inductive, in LemmaOverloading.prelude]
or6P [lemma, in LemmaOverloading.prelude]
Or61 [constructor, in LemmaOverloading.prelude]
Or62 [constructor, in LemmaOverloading.prelude]
Or63 [constructor, in LemmaOverloading.prelude]
Or64 [constructor, in LemmaOverloading.prelude]
Or65 [constructor, in LemmaOverloading.prelude]
Or66 [constructor, in LemmaOverloading.prelude]
P
Pack [constructor, in LemmaOverloading.cancel2]PackHeap [constructor, in LemmaOverloading.cancel2]
pack_right [definition, in LemmaOverloading.cancel2]
pack_found [definition, in LemmaOverloading.cancel2]
pack_h [projection, in LemmaOverloading.cancel2]
pack_heap [record, in LemmaOverloading.cancel2]
pack01 [definition, in LemmaOverloading.cancel2]
pack02 [definition, in LemmaOverloading.cancel2]
pack03 [definition, in LemmaOverloading.cancel2]
pack04 [definition, in LemmaOverloading.cancel2]
pack05 [definition, in LemmaOverloading.cancel2]
pack06 [definition, in LemmaOverloading.cancel2]
pack07 [definition, in LemmaOverloading.cancel2]
pack08 [definition, in LemmaOverloading.cancel2]
pack09 [definition, in LemmaOverloading.cancel2]
pack10 [definition, in LemmaOverloading.cancel2]
PairCPO [section, in LemmaOverloading.domains]
pairCPOMixin [definition, in LemmaOverloading.domains]
PairCPO.A [variable, in LemmaOverloading.domains]
PairCPO.B [variable, in LemmaOverloading.domains]
PairLattice [section, in LemmaOverloading.domains]
pairLatticeMixin [definition, in LemmaOverloading.domains]
PairLattice.A [variable, in LemmaOverloading.domains]
PairLattice.B [variable, in LemmaOverloading.domains]
PairPoset [section, in LemmaOverloading.domains]
pairPosetMixin [definition, in LemmaOverloading.domains]
PairPoset.A [variable, in LemmaOverloading.domains]
PairPoset.B [variable, in LemmaOverloading.domains]
pair_limM [lemma, in LemmaOverloading.domains]
pair_limP [lemma, in LemmaOverloading.domains]
pair_lim [definition, in LemmaOverloading.domains]
pair_supM [lemma, in LemmaOverloading.domains]
pair_supP [lemma, in LemmaOverloading.domains]
pair_sup [definition, in LemmaOverloading.domains]
pair_trans [lemma, in LemmaOverloading.domains]
pair_asym [lemma, in LemmaOverloading.domains]
pair_refl [lemma, in LemmaOverloading.domains]
pair_botP [lemma, in LemmaOverloading.domains]
pair_leq [definition, in LemmaOverloading.domains]
pair_bot [definition, in LemmaOverloading.domains]
path_supp_ins_inv [lemma, in LemmaOverloading.finmap]
path_supp_ins [lemma, in LemmaOverloading.finmap]
path_supp_ord [lemma, in LemmaOverloading.finmap]
path_ins' [lemma, in LemmaOverloading.finmap]
path_filter [lemma, in LemmaOverloading.heaps]
path_last [lemma, in LemmaOverloading.heaps]
perm [inductive, in LemmaOverloading.perms]
perms [library]
Permutations [section, in LemmaOverloading.perms]
Permutations.A [variable, in LemmaOverloading.perms]
permutation_trans [constructor, in LemmaOverloading.perms]
permutation_swap [constructor, in LemmaOverloading.perms]
permutation_skip [constructor, in LemmaOverloading.perms]
permutation_nil [constructor, in LemmaOverloading.perms]
perm_catCA [lemma, in LemmaOverloading.perms]
perm_catAC [lemma, in LemmaOverloading.perms]
perm_cat2r [lemma, in LemmaOverloading.perms]
perm_cat2l [lemma, in LemmaOverloading.perms]
perm_cat_cons [lemma, in LemmaOverloading.perms]
perm_cons_cat_cons [lemma, in LemmaOverloading.perms]
perm_cons [lemma, in LemmaOverloading.perms]
perm_cat_consR [lemma, in LemmaOverloading.perms]
perm_ind2 [lemma, in LemmaOverloading.perms]
perm_cons_cat_consL [lemma, in LemmaOverloading.perms]
perm_cons_catAC [lemma, in LemmaOverloading.perms]
perm_cons_catCA [lemma, in LemmaOverloading.perms]
perm_catC [lemma, in LemmaOverloading.perms]
perm_cat_consL [lemma, in LemmaOverloading.perms]
perm_catL [lemma, in LemmaOverloading.perms]
perm_cat2rL [lemma, in LemmaOverloading.perms]
perm_cat2lL [lemma, in LemmaOverloading.perms]
perm_in [lemma, in LemmaOverloading.perms]
perm_trans [lemma, in LemmaOverloading.perms]
perm_sym [lemma, in LemmaOverloading.perms]
perm_refl [lemma, in LemmaOverloading.perms]
perm_nil [lemma, in LemmaOverloading.perms]
pext [axiom, in LemmaOverloading.prelude]
pfree [definition, in LemmaOverloading.terms]
pfreeE [lemma, in LemmaOverloading.terms]
pfreeN [lemma, in LemmaOverloading.terms]
pfree_def [lemma, in LemmaOverloading.terms]
pfree_subdom [lemma, in LemmaOverloading.terms]
pick [definition, in LemmaOverloading.heaps]
pickP [lemma, in LemmaOverloading.heaps]
pL [definition, in LemmaOverloading.prelude]
plook [definition, in LemmaOverloading.terms]
plook' [abbreviation, in LemmaOverloading.terms]
plus2 [definition, in LemmaOverloading.heaps]
Poset [module, in LemmaOverloading.domains]
Poset.bot [definition, in LemmaOverloading.domains]
Poset.class [definition, in LemmaOverloading.domains]
Poset.Class [constructor, in LemmaOverloading.domains]
Poset.ClassDef [section, in LemmaOverloading.domains]
Poset.ClassDef.cT [variable, in LemmaOverloading.domains]
Poset.ClassDef.T [variable, in LemmaOverloading.domains]
Poset.class_of [record, in LemmaOverloading.domains]
Poset.clone [definition, in LemmaOverloading.domains]
Poset.Exports [module, in LemmaOverloading.domains]
Poset.Exports.bot [abbreviation, in LemmaOverloading.domains]
Poset.Exports.botP [lemma, in LemmaOverloading.domains]
Poset.Exports.Laws [section, in LemmaOverloading.domains]
Poset.Exports.Laws.T [variable, in LemmaOverloading.domains]
Poset.Exports.Poset [abbreviation, in LemmaOverloading.domains]
Poset.Exports.poset [abbreviation, in LemmaOverloading.domains]
Poset.Exports.PosetMixin [abbreviation, in LemmaOverloading.domains]
Poset.Exports.poset_trans [lemma, in LemmaOverloading.domains]
Poset.Exports.poset_asym [lemma, in LemmaOverloading.domains]
Poset.Exports.poset_refl [lemma, in LemmaOverloading.domains]
[ poset of _ ] (form_scope) [notation, in LemmaOverloading.domains]
[ poset of _ for _ ] (form_scope) [notation, in LemmaOverloading.domains]
_ <== _ [notation, in LemmaOverloading.domains]
Poset.leq [definition, in LemmaOverloading.domains]
Poset.mixin [projection, in LemmaOverloading.domains]
Poset.Mixin [constructor, in LemmaOverloading.domains]
Poset.mixin_of [record, in LemmaOverloading.domains]
Poset.mx_bot [projection, in LemmaOverloading.domains]
Poset.mx_leq [projection, in LemmaOverloading.domains]
Poset.pack [definition, in LemmaOverloading.domains]
Poset.Pack [constructor, in LemmaOverloading.domains]
Poset.RawMixin [section, in LemmaOverloading.domains]
Poset.sort [projection, in LemmaOverloading.domains]
Poset.type [record, in LemmaOverloading.domains]
post [abbreviation, in LemmaOverloading.stmod]
pow [definition, in LemmaOverloading.domains]
pow_chain [definition, in LemmaOverloading.domains]
pow_mono [lemma, in LemmaOverloading.domains]
ppts [definition, in LemmaOverloading.hprop]
pR [definition, in LemmaOverloading.prelude]
pre [abbreviation, in LemmaOverloading.stmod]
pread [definition, in LemmaOverloading.terms]
pread' [abbreviation, in LemmaOverloading.terms]
Pred [definition, in LemmaOverloading.rels]
PredArgType [definition, in LemmaOverloading.rels]
PredC [definition, in LemmaOverloading.rels]
predCk [abbreviation, in LemmaOverloading.finmap]
predCk [definition, in LemmaOverloading.finmap]
PredCPO [section, in LemmaOverloading.domains]
predCPOMixin [definition, in LemmaOverloading.domains]
PredCPO.A [variable, in LemmaOverloading.domains]
PredD [definition, in LemmaOverloading.rels]
PredI [definition, in LemmaOverloading.rels]
Predicates [section, in LemmaOverloading.rels]
Predicates.T [variable, in LemmaOverloading.rels]
predk [abbreviation, in LemmaOverloading.finmap]
predk [definition, in LemmaOverloading.finmap]
predkN [lemma, in LemmaOverloading.finmap]
PredLattice [section, in LemmaOverloading.domains]
predLatticeMixin [definition, in LemmaOverloading.domains]
PredLattice.A [variable, in LemmaOverloading.domains]
PredPoset [section, in LemmaOverloading.domains]
predPosetMixin [definition, in LemmaOverloading.domains]
PredPoset.A [variable, in LemmaOverloading.domains]
PredT [definition, in LemmaOverloading.rels]
PredType [record, in LemmaOverloading.rels]
PredU [definition, in LemmaOverloading.rels]
pred_of [projection, in LemmaOverloading.domains]
Pred_Class [abbreviation, in LemmaOverloading.rels]
Pred_Sort [projection, in LemmaOverloading.rels]
Pred0 [definition, in LemmaOverloading.rels]
Pred1 [definition, in LemmaOverloading.rels]
prefix [definition, in LemmaOverloading.prefix]
Prefix [section, in LemmaOverloading.prefix]
prefix [library]
prefix_onth [lemma, in LemmaOverloading.prefix]
prefix_size [lemma, in LemmaOverloading.prefix]
prefix_cons' [lemma, in LemmaOverloading.prefix]
prefix_cons [lemma, in LemmaOverloading.prefix]
prefix_trans [lemma, in LemmaOverloading.prefix]
prefix_refl [lemma, in LemmaOverloading.prefix]
Prefix.A [variable, in LemmaOverloading.prefix]
Preim [definition, in LemmaOverloading.rels]
prelude [library]
ProdChain [section, in LemmaOverloading.domains]
ProdChain.f1 [variable, in LemmaOverloading.domains]
ProdChain.f2 [variable, in LemmaOverloading.domains]
ProdChain.M1 [variable, in LemmaOverloading.domains]
ProdChain.M2 [variable, in LemmaOverloading.domains]
ProdChain.s [variable, in LemmaOverloading.domains]
ProdChain.S1 [variable, in LemmaOverloading.domains]
ProdChain.S2 [variable, in LemmaOverloading.domains]
ProdChain.T1 [variable, in LemmaOverloading.domains]
ProdChain.T2 [variable, in LemmaOverloading.domains]
ProdOrd [section, in LemmaOverloading.ordtype]
ProdOrd.K [variable, in LemmaOverloading.ordtype]
ProdOrd.T [variable, in LemmaOverloading.ordtype]
prod_cont [lemma, in LemmaOverloading.domains]
prod_chain [definition, in LemmaOverloading.domains]
prod_mono [lemma, in LemmaOverloading.domains]
prod_ordMixin [definition, in LemmaOverloading.ordtype]
prog [definition, in LemmaOverloading.stmod]
ProjChain [section, in LemmaOverloading.domains]
ProjChain.s [variable, in LemmaOverloading.domains]
ProjChain.T1 [variable, in LemmaOverloading.domains]
ProjChain.T2 [variable, in LemmaOverloading.domains]
proj1_cont [lemma, in LemmaOverloading.domains]
proj1_prodE [lemma, in LemmaOverloading.domains]
proj1_diagE [lemma, in LemmaOverloading.domains]
proj1_chain [definition, in LemmaOverloading.domains]
proj1_mono [lemma, in LemmaOverloading.domains]
proj2_cont [lemma, in LemmaOverloading.domains]
proj2_prodE [lemma, in LemmaOverloading.domains]
proj2_diagE [lemma, in LemmaOverloading.domains]
proj2_chain [definition, in LemmaOverloading.domains]
proj2_mono [lemma, in LemmaOverloading.domains]
proof [projection, in LemmaOverloading.cancel2]
proof_irrelevance [lemma, in LemmaOverloading.prelude]
prop [projection, in LemmaOverloading.cancel2]
PropCPO [section, in LemmaOverloading.domains]
propCPOMixin [definition, in LemmaOverloading.domains]
PropLattice [section, in LemmaOverloading.domains]
propLatticeMixin [definition, in LemmaOverloading.domains]
PropPoset [section, in LemmaOverloading.domains]
propPosetMixin [definition, in LemmaOverloading.domains]
PropPredType [constructor, in LemmaOverloading.rels]
prop_limM [lemma, in LemmaOverloading.domains]
prop_limP [lemma, in LemmaOverloading.domains]
prop_lim [definition, in LemmaOverloading.domains]
prop_supM [lemma, in LemmaOverloading.domains]
prop_supP [lemma, in LemmaOverloading.domains]
prop_sup [definition, in LemmaOverloading.domains]
prop_trans [lemma, in LemmaOverloading.domains]
prop_asym [lemma, in LemmaOverloading.domains]
prop_refl [lemma, in LemmaOverloading.domains]
prop_botP [lemma, in LemmaOverloading.domains]
prop_leq [definition, in LemmaOverloading.domains]
prop_bot [definition, in LemmaOverloading.domains]
prop_of [projection, in LemmaOverloading.auto]
prop_of [projection, in LemmaOverloading.cancelD]
ptr [inductive, in LemmaOverloading.heaps]
ptrA [lemma, in LemmaOverloading.heaps]
ptrE [lemma, in LemmaOverloading.heaps]
ptreq [definition, in LemmaOverloading.terms]
ptrK [lemma, in LemmaOverloading.heaps]
ptrs [definition, in LemmaOverloading.terms]
ptrT [lemma, in LemmaOverloading.heaps]
ptr_has [lemma, in LemmaOverloading.terms]
ptr_ctx [projection, in LemmaOverloading.terms]
ptr_ordMixin [definition, in LemmaOverloading.heaps]
ptr_null [lemma, in LemmaOverloading.heaps]
ptr_offset [definition, in LemmaOverloading.heaps]
ptr_eqMixin [definition, in LemmaOverloading.heaps]
ptr_nat [constructor, in LemmaOverloading.heaps]
ptr0 [lemma, in LemmaOverloading.heaps]
Pts [constructor, in LemmaOverloading.terms]
pts [definition, in LemmaOverloading.heaps]
pts_pf [lemma, in LemmaOverloading.cancel]
pts_tag [definition, in LemmaOverloading.cancel]
pts_inv [definition, in LemmaOverloading.cancel2]
pts_h [projection, in LemmaOverloading.cancel2]
pts_struct [instance, in LemmaOverloading.cancelCTC]
pts_inj [lemma, in LemmaOverloading.heaps]
pts_injT [lemma, in LemmaOverloading.heaps]
pts_injP [lemma, in LemmaOverloading.heaps]
pull [definition, in LemmaOverloading.stlog]
puntag [projection, in LemmaOverloading.cancelD]
push [definition, in LemmaOverloading.stlog]
R
rA [definition, in LemmaOverloading.prelude]rAC [definition, in LemmaOverloading.prelude]
rACI [lemma, in LemmaOverloading.prelude]
rCA [definition, in LemmaOverloading.prelude]
rCAI [lemma, in LemmaOverloading.prelude]
read [definition, in LemmaOverloading.stsep]
readP [lemma, in LemmaOverloading.stsep]
read_s [definition, in LemmaOverloading.stsep]
recurse [definition, in LemmaOverloading.auto]
recurse_pf [lemma, in LemmaOverloading.xfind]
recurse_tag [definition, in LemmaOverloading.xfind]
recurse_struct [instance, in LemmaOverloading.xfindCTC]
ReflectConnectives [section, in LemmaOverloading.prelude]
ReflectConnectives.b1 [variable, in LemmaOverloading.prelude]
ReflectConnectives.b2 [variable, in LemmaOverloading.prelude]
ReflectConnectives.b3 [variable, in LemmaOverloading.prelude]
ReflectConnectives.b4 [variable, in LemmaOverloading.prelude]
ReflectConnectives.b5 [variable, in LemmaOverloading.prelude]
ReflectConnectives.b6 [variable, in LemmaOverloading.prelude]
refl_jmeq2 [lemma, in LemmaOverloading.prelude]
reindex [lemma, in LemmaOverloading.domains]
relax [definition, in LemmaOverloading.domains]
relaxP [lemma, in LemmaOverloading.domains]
RelLaws [section, in LemmaOverloading.rels]
RelLaws.T [variable, in LemmaOverloading.rels]
RelProperties [section, in LemmaOverloading.rels]
RelProperties.pT [variable, in LemmaOverloading.rels]
RelProperties.T [variable, in LemmaOverloading.rels]
rels [library]
rem [definition, in LemmaOverloading.finmap]
remove [definition, in LemmaOverloading.llistR]
rem_supp [lemma, in LemmaOverloading.finmap]
rem_ins [lemma, in LemmaOverloading.finmap]
rem_rem [lemma, in LemmaOverloading.finmap]
rem_empty [lemma, in LemmaOverloading.finmap]
Reorder [section, in LemmaOverloading.prelude]
Reorder.A [variable, in LemmaOverloading.prelude]
Reorder.B [variable, in LemmaOverloading.prelude]
Reorder.C [variable, in LemmaOverloading.prelude]
repack_Pred [definition, in LemmaOverloading.rels]
rest [projection, in LemmaOverloading.stlogCTC]
rest1 [projection, in LemmaOverloading.stlogCTC]
ret [definition, in LemmaOverloading.stsep]
retP [lemma, in LemmaOverloading.stsep]
ret_s [definition, in LemmaOverloading.stsep]
reverse [definition, in LemmaOverloading.llistR]
revT [definition, in LemmaOverloading.llistR]
riA [lemma, in LemmaOverloading.prelude]
right_pf [lemma, in LemmaOverloading.indom]
right_tag [definition, in LemmaOverloading.indom]
right_struct [instance, in LemmaOverloading.stlogCTC]
right_pf [lemma, in LemmaOverloading.stlogR]
right_tag [definition, in LemmaOverloading.stlogR]
runs_of [definition, in LemmaOverloading.stmod]
S
scan [projection, in LemmaOverloading.noaliasCTC]Scan [record, in LemmaOverloading.noaliasCTC]
Scan [module, in LemmaOverloading.noalias]
scanE [lemma, in LemmaOverloading.noaliasCTC]
scan_default [instance, in LemmaOverloading.noaliasCTC]
scan_ptr [instance, in LemmaOverloading.noaliasCTC]
scan_union [instance, in LemmaOverloading.noaliasCTC]
scan_axiom [definition, in LemmaOverloading.noaliasCTC]
scan_it [lemma, in LemmaOverloading.noalias]
Scan.axiom [definition, in LemmaOverloading.noalias]
Scan.default_pf [lemma, in LemmaOverloading.noalias]
Scan.default_tag [definition, in LemmaOverloading.noalias]
Scan.Exports [module, in LemmaOverloading.noalias]
Scan.form [record, in LemmaOverloading.noalias]
Scan.Form [constructor, in LemmaOverloading.noalias]
Scan.heap_of [projection, in LemmaOverloading.noalias]
Scan.ptr_pf [lemma, in LemmaOverloading.noalias]
Scan.ptr_tag [definition, in LemmaOverloading.noalias]
Scan.scanE [lemma, in LemmaOverloading.noalias]
Scan.ScanSection [section, in LemmaOverloading.noalias]
Scan.Tag [constructor, in LemmaOverloading.noalias]
Scan.tagged_heap [record, in LemmaOverloading.noalias]
Scan.union_pf [lemma, in LemmaOverloading.noalias]
Scan.untag [projection, in LemmaOverloading.noalias]
search [projection, in LemmaOverloading.noaliasCTC]
Search [record, in LemmaOverloading.noaliasCTC]
Search [module, in LemmaOverloading.noalias]
search_recurse [instance, in LemmaOverloading.noaliasCTC]
search_found [instance, in LemmaOverloading.noaliasCTC]
search_them [definition, in LemmaOverloading.noalias]
Search.axiom [definition, in LemmaOverloading.noalias]
Search.Exports [module, in LemmaOverloading.noalias]
Search.findE [lemma, in LemmaOverloading.noalias]
Search.form [record, in LemmaOverloading.noalias]
Search.Form [constructor, in LemmaOverloading.noalias]
Search.found_pf [lemma, in LemmaOverloading.noalias]
Search.recurse_pf [lemma, in LemmaOverloading.noalias]
Search.recurse_tag [definition, in LemmaOverloading.noalias]
Search.SearchSection [section, in LemmaOverloading.noalias]
Search.seq_of [projection, in LemmaOverloading.noalias]
Search.Tag [constructor, in LemmaOverloading.noalias]
Search.tagged_seq [record, in LemmaOverloading.noalias]
Search.untag [projection, in LemmaOverloading.noalias]
search2 [projection, in LemmaOverloading.noaliasCTC]
Search2 [record, in LemmaOverloading.noaliasCTC]
Search2 [module, in LemmaOverloading.noalias]
search2_foundz [instance, in LemmaOverloading.noaliasCTC]
search2_foundy [instance, in LemmaOverloading.noaliasCTC]
search2_foundx [instance, in LemmaOverloading.noaliasCTC]
search2_axiom [definition, in LemmaOverloading.noaliasCTC]
Search2.axiom [definition, in LemmaOverloading.noalias]
Search2.Exports [module, in LemmaOverloading.noalias]
Search2.find2E [lemma, in LemmaOverloading.noalias]
Search2.form [record, in LemmaOverloading.noalias]
Search2.Form [constructor, in LemmaOverloading.noalias]
Search2.foundx_pf [lemma, in LemmaOverloading.noalias]
Search2.foundy_pf [lemma, in LemmaOverloading.noalias]
Search2.foundy_tag [definition, in LemmaOverloading.noalias]
Search2.foundz_pf [lemma, in LemmaOverloading.noalias]
Search2.foundz_tag [definition, in LemmaOverloading.noalias]
Search2.Search2Section [section, in LemmaOverloading.noalias]
Search2.seq_of [projection, in LemmaOverloading.noalias]
Search2.Tag [constructor, in LemmaOverloading.noalias]
Search2.tagged_seq [record, in LemmaOverloading.noalias]
Search2.untag [projection, in LemmaOverloading.noalias]
SepAlloc [section, in LemmaOverloading.stsep]
SepAlloc.A [variable, in LemmaOverloading.stsep]
SepAlloc.v [variable, in LemmaOverloading.stsep]
SepBind [section, in LemmaOverloading.stsep]
SepBind.A [variable, in LemmaOverloading.stsep]
SepBind.B [variable, in LemmaOverloading.stsep]
SepBind.e1 [variable, in LemmaOverloading.stsep]
SepBind.e2 [variable, in LemmaOverloading.stsep]
SepBind.s1 [variable, in LemmaOverloading.stsep]
SepBind.s2 [variable, in LemmaOverloading.stsep]
SepBlockAlloc [section, in LemmaOverloading.stsep]
SepBlockAlloc.A [variable, in LemmaOverloading.stsep]
SepBlockAlloc.n [variable, in LemmaOverloading.stsep]
SepBlockAlloc.v [variable, in LemmaOverloading.stsep]
SepConseq [section, in LemmaOverloading.stsep]
SepConseq.A [variable, in LemmaOverloading.stsep]
SepConseq.e [variable, in LemmaOverloading.stsep]
SepConseq.pf [variable, in LemmaOverloading.stsep]
SepConseq.s1 [variable, in LemmaOverloading.stsep]
SepConseq.s2 [variable, in LemmaOverloading.stsep]
SepDealloc [section, in LemmaOverloading.stsep]
SepDealloc.x [variable, in LemmaOverloading.stsep]
SepFix [section, in LemmaOverloading.stsep]
SepFix.A [variable, in LemmaOverloading.stsep]
SepFix.B [variable, in LemmaOverloading.stsep]
SepFix.s [variable, in LemmaOverloading.stsep]
SepFrame [section, in LemmaOverloading.stsep]
SepFrame.A [variable, in LemmaOverloading.stsep]
SepFrame.s [variable, in LemmaOverloading.stsep]
SepRead [section, in LemmaOverloading.stsep]
SepRead.A [variable, in LemmaOverloading.stsep]
SepRead.x [variable, in LemmaOverloading.stsep]
SepReturn [section, in LemmaOverloading.stsep]
SepReturn.A [variable, in LemmaOverloading.stsep]
SepReturn.x [variable, in LemmaOverloading.stsep]
SepThrow [section, in LemmaOverloading.stsep]
SepThrow.A [variable, in LemmaOverloading.stsep]
SepThrow.e [variable, in LemmaOverloading.stsep]
SepTry [section, in LemmaOverloading.stsep]
SepTry.A [variable, in LemmaOverloading.stsep]
SepTry.B [variable, in LemmaOverloading.stsep]
SepTry.e [variable, in LemmaOverloading.stsep]
SepTry.e1 [variable, in LemmaOverloading.stsep]
SepTry.e2 [variable, in LemmaOverloading.stsep]
SepTry.s [variable, in LemmaOverloading.stsep]
SepTry.s1 [variable, in LemmaOverloading.stsep]
SepTry.s2 [variable, in LemmaOverloading.stsep]
SepWrite [section, in LemmaOverloading.stsep]
SepWrite.A [variable, in LemmaOverloading.stsep]
SepWrite.v [variable, in LemmaOverloading.stsep]
SepWrite.x [variable, in LemmaOverloading.stsep]
seqof_ins [lemma, in LemmaOverloading.finmap]
seq_of [projection, in LemmaOverloading.noaliasCTC]
seq_of [projection, in LemmaOverloading.xfindCTC]
seq_of [projection, in LemmaOverloading.finmap]
seq_of [projection, in LemmaOverloading.auto]
sexit1 [lemma, in LemmaOverloading.heaps]
sexit2 [lemma, in LemmaOverloading.heaps]
sexit3 [lemma, in LemmaOverloading.heaps]
sexit4 [lemma, in LemmaOverloading.heaps]
shape_rev [definition, in LemmaOverloading.llistR]
Simplifications [section, in LemmaOverloading.rels]
Simplifications.pT [variable, in LemmaOverloading.rels]
Simplifications.T [variable, in LemmaOverloading.rels]
simplify [lemma, in LemmaOverloading.cancelD]
SimplPred [definition, in LemmaOverloading.rels]
Simpl_PredE [lemma, in LemmaOverloading.rels]
Simpl_Pred [definition, in LemmaOverloading.rels]
single [definition, in LemmaOverloading.stmod]
singleP [lemma, in LemmaOverloading.stmod]
size_onth [lemma, in LemmaOverloading.prefix]
sorted_filter [lemma, in LemmaOverloading.finmap]
sorted_ins' [lemma, in LemmaOverloading.finmap]
sorted_nil [lemma, in LemmaOverloading.finmap]
spec [definition, in LemmaOverloading.stmod]
spec_runs [lemma, in LemmaOverloading.stmod]
ST [record, in LemmaOverloading.stmod]
star [definition, in LemmaOverloading.hprop]
starA [lemma, in LemmaOverloading.hprop]
starAC [lemma, in LemmaOverloading.hprop]
starC [lemma, in LemmaOverloading.hprop]
starCA [lemma, in LemmaOverloading.hprop]
starp0 [lemma, in LemmaOverloading.hprop]
star0p [lemma, in LemmaOverloading.hprop]
STDef [section, in LemmaOverloading.stmod]
STDef.A [variable, in LemmaOverloading.stmod]
STDef.s [variable, in LemmaOverloading.stmod]
stLatticeMixin [definition, in LemmaOverloading.stmod]
stlog [library]
stlogCTC [library]
stlogR [library]
stmod [library]
stPosetMixin [definition, in LemmaOverloading.stmod]
STprog [constructor, in LemmaOverloading.stmod]
stress [definition, in LemmaOverloading.cancel]
stress [definition, in LemmaOverloading.cancel2]
STsep [definition, in LemmaOverloading.stsep]
stsep [library]
st_supM [lemma, in LemmaOverloading.stmod]
st_supP [lemma, in LemmaOverloading.stmod]
st_sup [definition, in LemmaOverloading.stmod]
st_sup_has_spec [lemma, in LemmaOverloading.stmod]
st_sup_dstrict [lemma, in LemmaOverloading.stmod]
st_sup_coherent [lemma, in LemmaOverloading.stmod]
st_sup' [definition, in LemmaOverloading.stmod]
st_botP [lemma, in LemmaOverloading.stmod]
st_bot [definition, in LemmaOverloading.stmod]
st_bot_has_spec [lemma, in LemmaOverloading.stmod]
st_bot_dstrict [lemma, in LemmaOverloading.stmod]
st_bot_coherent [lemma, in LemmaOverloading.stmod]
st_bot' [definition, in LemmaOverloading.stmod]
st_trans [lemma, in LemmaOverloading.stmod]
st_asym [lemma, in LemmaOverloading.stmod]
st_refl [lemma, in LemmaOverloading.stmod]
st_leq [definition, in LemmaOverloading.stmod]
subCPO [definition, in LemmaOverloading.domains]
SubCPO [section, in LemmaOverloading.domains]
subCPOMixin [definition, in LemmaOverloading.domains]
SubCPO.C [variable, in LemmaOverloading.domains]
SubCPO.D [variable, in LemmaOverloading.domains]
SubCPO.s [variable, in LemmaOverloading.domains]
subctx [definition, in LemmaOverloading.terms]
subctx_trans [lemma, in LemmaOverloading.terms]
subctx_refl [lemma, in LemmaOverloading.terms]
subdom [definition, in LemmaOverloading.heaps]
subdomD [lemma, in LemmaOverloading.heaps]
subdomE [lemma, in LemmaOverloading.heaps]
subdomP [lemma, in LemmaOverloading.heaps]
subdomPE [lemma, in LemmaOverloading.heaps]
subdomQ [lemma, in LemmaOverloading.heaps]
subdomUE [lemma, in LemmaOverloading.heaps]
subdom_trans [lemma, in LemmaOverloading.heaps]
subdom_emp_inv [lemma, in LemmaOverloading.heaps]
subdom_emp [lemma, in LemmaOverloading.heaps]
subdom_refl [lemma, in LemmaOverloading.heaps]
subdom_def [lemma, in LemmaOverloading.heaps]
subheap [definition, in LemmaOverloading.heaps]
subheapE [lemma, in LemmaOverloading.heaps]
subheapUn [lemma, in LemmaOverloading.heaps]
subheapUnl [lemma, in LemmaOverloading.heaps]
subheapUnr [lemma, in LemmaOverloading.heaps]
subheap_id [lemma, in LemmaOverloading.heaps]
subheap_trans [lemma, in LemmaOverloading.heaps]
subheap_def [lemma, in LemmaOverloading.heaps]
subheap_refl [lemma, in LemmaOverloading.heaps]
subLattice [definition, in LemmaOverloading.domains]
SubLattice [section, in LemmaOverloading.domains]
subLatticeMixin [definition, in LemmaOverloading.domains]
SubLattice.C [variable, in LemmaOverloading.domains]
SubLattice.s [variable, in LemmaOverloading.domains]
SubLattice.T [variable, in LemmaOverloading.domains]
SubMem [definition, in LemmaOverloading.rels]
SubMemLaws [section, in LemmaOverloading.rels]
SubMemLaws.T [variable, in LemmaOverloading.rels]
subPoset [definition, in LemmaOverloading.domains]
SubPoset [section, in LemmaOverloading.domains]
subPosetMixin [definition, in LemmaOverloading.domains]
SubPoset.C [variable, in LemmaOverloading.domains]
SubPoset.s [variable, in LemmaOverloading.domains]
SubPoset.T [variable, in LemmaOverloading.domains]
SubPred [definition, in LemmaOverloading.rels]
SubPredFun [definition, in LemmaOverloading.rels]
SubPredType [definition, in LemmaOverloading.rels]
SubPredType_trans [definition, in LemmaOverloading.rels]
SubPredType_trans' [lemma, in LemmaOverloading.rels]
SubPredType_refl [lemma, in LemmaOverloading.rels]
subp_andr [lemma, in LemmaOverloading.rels]
subp_andl [lemma, in LemmaOverloading.rels]
subp_orr [lemma, in LemmaOverloading.rels]
subp_orl [lemma, in LemmaOverloading.rels]
subp_and [lemma, in LemmaOverloading.rels]
subp_or [lemma, in LemmaOverloading.rels]
subp_trans [lemma, in LemmaOverloading.rels]
subp_asym [lemma, in LemmaOverloading.rels]
subp_refl [lemma, in LemmaOverloading.rels]
SubSimplPred [definition, in LemmaOverloading.rels]
subtract [definition, in LemmaOverloading.heaps]
sub_limM [lemma, in LemmaOverloading.domains]
sub_limP [lemma, in LemmaOverloading.domains]
sub_lim [definition, in LemmaOverloading.domains]
sub_limX [lemma, in LemmaOverloading.domains]
sub_supM [lemma, in LemmaOverloading.domains]
sub_supP [lemma, in LemmaOverloading.domains]
sub_sup [definition, in LemmaOverloading.domains]
sub_supX [lemma, in LemmaOverloading.domains]
sub_sup' [definition, in LemmaOverloading.domains]
sub_trans [lemma, in LemmaOverloading.domains]
sub_asym [lemma, in LemmaOverloading.domains]
sub_refl [lemma, in LemmaOverloading.domains]
sub_botP [lemma, in LemmaOverloading.domains]
sub_leq [definition, in LemmaOverloading.domains]
sub_bot [definition, in LemmaOverloading.domains]
sub_orr [lemma, in LemmaOverloading.rels]
sub_orl [lemma, in LemmaOverloading.rels]
supdom [definition, in LemmaOverloading.heaps]
supdomeqUh [lemma, in LemmaOverloading.heaps]
supdomUh [lemma, in LemmaOverloading.heaps]
supE [lemma, in LemmaOverloading.domains]
supp [definition, in LemmaOverloading.finmap]
suppP [lemma, in LemmaOverloading.finmap]
supp_eq_ins [lemma, in LemmaOverloading.finmap]
supp_fcat [lemma, in LemmaOverloading.finmap]
supp_ins [lemma, in LemmaOverloading.finmap]
supp_rem [lemma, in LemmaOverloading.finmap]
supp_nilE [lemma, in LemmaOverloading.finmap]
supp_nil [lemma, in LemmaOverloading.finmap]
supp_spec_none [constructor, in LemmaOverloading.finmap]
supp_spec_some [constructor, in LemmaOverloading.finmap]
supp_spec [inductive, in LemmaOverloading.finmap]
sup_dappE [lemma, in LemmaOverloading.domains]
sup_appE [lemma, in LemmaOverloading.domains]
sup_clos_mono [lemma, in LemmaOverloading.domains]
sup_clos_idemp [lemma, in LemmaOverloading.domains]
sup_closP [lemma, in LemmaOverloading.domains]
sup_clos_min [lemma, in LemmaOverloading.domains]
sup_clos_sub [lemma, in LemmaOverloading.domains]
sup_mono [lemma, in LemmaOverloading.domains]
sup_closure [definition, in LemmaOverloading.domains]
sup_closed [definition, in LemmaOverloading.domains]
sup_defdef [lemma, in LemmaOverloading.heaps]
svalE [lemma, in LemmaOverloading.prelude]
sval_mono [lemma, in LemmaOverloading.domains]
swap [definition, in LemmaOverloading.prelude]
swapI [lemma, in LemmaOverloading.prelude]
swap_rAC [lemma, in LemmaOverloading.prelude]
swap_rCA [lemma, in LemmaOverloading.prelude]
swap_prod [lemma, in LemmaOverloading.prelude]
swp [lemma, in LemmaOverloading.stlog]
sym [lemma, in LemmaOverloading.prelude]
synheap [definition, in LemmaOverloading.terms]
T
Tag [constructor, in LemmaOverloading.cancel]Tag [constructor, in LemmaOverloading.indom]
Tag [constructor, in LemmaOverloading.auto]
Tag [constructor, in LemmaOverloading.cancelD]
Tag [constructor, in LemmaOverloading.stlogR]
tagged_heap [record, in LemmaOverloading.cancel]
tagged_heap [record, in LemmaOverloading.indom]
tagged_prop [record, in LemmaOverloading.auto]
tagged_seq [record, in LemmaOverloading.auto]
tagged_prop [record, in LemmaOverloading.cancelD]
tagged_heap [record, in LemmaOverloading.stlogR]
TagS [constructor, in LemmaOverloading.auto]
tarski_gfp_greatest [lemma, in LemmaOverloading.domains]
tarski_gfp_fixed [lemma, in LemmaOverloading.domains]
tarski_lfp_least [lemma, in LemmaOverloading.domains]
tarski_lfp_fixed [lemma, in LemmaOverloading.domains]
tarski_gfp [definition, in LemmaOverloading.domains]
tarski_lfp [definition, in LemmaOverloading.domains]
terms [library]
test [definition, in LemmaOverloading.xfind]
test [lemma, in LemmaOverloading.heaps]
this [definition, in LemmaOverloading.hprop]
throw [definition, in LemmaOverloading.stsep]
throwP [lemma, in LemmaOverloading.stsep]
throw_s [definition, in LemmaOverloading.stsep]
top [definition, in LemmaOverloading.hprop]
toPred [projection, in LemmaOverloading.rels]
toPredE [lemma, in LemmaOverloading.rels]
total [lemma, in LemmaOverloading.ordtype]
Totality [section, in LemmaOverloading.ordtype]
Totality.K [variable, in LemmaOverloading.ordtype]
totalP [lemma, in LemmaOverloading.ordtype]
total_ordf [lemma, in LemmaOverloading.ordtype]
total_lex [lemma, in LemmaOverloading.ordtype]
total_ltn_nat [lemma, in LemmaOverloading.ordtype]
total_spec_gt [constructor, in LemmaOverloading.ordtype]
total_spec_eq [constructor, in LemmaOverloading.ordtype]
total_spec_lt [constructor, in LemmaOverloading.ordtype]
total_spec [inductive, in LemmaOverloading.ordtype]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.domains]
tp [abbreviation, in LemmaOverloading.stsep]
trans [lemma, in LemmaOverloading.ordtype]
trans_ordf [lemma, in LemmaOverloading.ordtype]
trans_lex [lemma, in LemmaOverloading.ordtype]
trans_ltn_nat [lemma, in LemmaOverloading.ordtype]
trigger [record, in LemmaOverloading.cancel2]
triggered [definition, in LemmaOverloading.noalias]
try [definition, in LemmaOverloading.stsep]
TryForm [constructor, in LemmaOverloading.stlogR]
tryP [lemma, in LemmaOverloading.stsep]
try_gh1 [lemma, in LemmaOverloading.stlog]
try_gh [lemma, in LemmaOverloading.stlog]
try_throw [lemma, in LemmaOverloading.stlog]
try_dealloc [lemma, in LemmaOverloading.stlog]
try_allocb [lemma, in LemmaOverloading.stlog]
try_alloc [lemma, in LemmaOverloading.stlog]
try_write [lemma, in LemmaOverloading.stlog]
try_read [lemma, in LemmaOverloading.stlog]
try_ret [lemma, in LemmaOverloading.stlog]
try_do [lemma, in LemmaOverloading.stlog]
try_s [definition, in LemmaOverloading.stsep]
try_case_pf [lemma, in LemmaOverloading.stlogR]
try_pivot [projection, in LemmaOverloading.stlogR]
try_form [record, in LemmaOverloading.stlogR]
try_gh1R [lemma, in LemmaOverloading.stlogR]
try_ghR [lemma, in LemmaOverloading.stlogR]
try_throwR [definition, in LemmaOverloading.stlogR]
try_deallocR [lemma, in LemmaOverloading.stlogR]
try_allocbR [definition, in LemmaOverloading.stlogR]
try_allocR [definition, in LemmaOverloading.stlogR]
try_writeR [lemma, in LemmaOverloading.stlogR]
try_readR [lemma, in LemmaOverloading.stlogR]
try_retR [definition, in LemmaOverloading.stlogR]
try_doR [lemma, in LemmaOverloading.stlogR]
U
unA [lemma, in LemmaOverloading.heaps]unAC [lemma, in LemmaOverloading.heaps]
unA2 [lemma, in LemmaOverloading.heaps]
unC [lemma, in LemmaOverloading.heaps]
unCA [lemma, in LemmaOverloading.heaps]
unC2 [lemma, in LemmaOverloading.heaps]
Undef [constructor, in LemmaOverloading.heaps]
undefE [lemma, in LemmaOverloading.heaps]
unDl2 [lemma, in LemmaOverloading.heaps]
unDr2 [lemma, in LemmaOverloading.heaps]
unhKl [lemma, in LemmaOverloading.heaps]
unhKr [lemma, in LemmaOverloading.heaps]
unh0 [lemma, in LemmaOverloading.heaps]
unh02 [lemma, in LemmaOverloading.heaps]
union_pf [lemma, in LemmaOverloading.cancel]
union_struct [instance, in LemmaOverloading.cancelCTC]
union2 [definition, in LemmaOverloading.heaps]
unit_test [definition, in LemmaOverloading.xfind]
unit_test [definition, in LemmaOverloading.xfindCTC]
unKhl [lemma, in LemmaOverloading.heaps]
unKhl2 [lemma, in LemmaOverloading.heaps]
unKhr [lemma, in LemmaOverloading.heaps]
unKhr2 [lemma, in LemmaOverloading.heaps]
unpack [projection, in LemmaOverloading.cancel2]
untag [projection, in LemmaOverloading.cancel]
untag [projection, in LemmaOverloading.indom]
untag [projection, in LemmaOverloading.auto]
untag [projection, in LemmaOverloading.stlogR]
untags [projection, in LemmaOverloading.auto]
un_nullP [lemma, in LemmaOverloading.heaps]
un0E [lemma, in LemmaOverloading.heaps]
un0h [lemma, in LemmaOverloading.heaps]
un0h2 [lemma, in LemmaOverloading.heaps]
upd [definition, in LemmaOverloading.heaps]
Update [record, in LemmaOverloading.stlogCTC]
update [record, in LemmaOverloading.stlogR]
Update [constructor, in LemmaOverloading.stlogR]
updateE [lemma, in LemmaOverloading.stlogR]
update_axiom [definition, in LemmaOverloading.stlogR]
update1 [projection, in LemmaOverloading.stlogCTC]
update2 [projection, in LemmaOverloading.stlogCTC]
updF [lemma, in LemmaOverloading.heaps]
updi [definition, in LemmaOverloading.heaps]
updiD [lemma, in LemmaOverloading.heaps]
updimV [lemma, in LemmaOverloading.heaps]
updiP [lemma, in LemmaOverloading.heaps]
updiS [lemma, in LemmaOverloading.heaps]
updiVm [lemma, in LemmaOverloading.heaps]
updiVm' [lemma, in LemmaOverloading.heaps]
updi_iinv [lemma, in LemmaOverloading.heaps]
updi_inv [lemma, in LemmaOverloading.heaps]
updi_catI [lemma, in LemmaOverloading.heaps]
updi_cat [lemma, in LemmaOverloading.heaps]
updi_last [lemma, in LemmaOverloading.heaps]
updPtUn [lemma, in LemmaOverloading.heaps]
updU [lemma, in LemmaOverloading.heaps]
updUnl [lemma, in LemmaOverloading.heaps]
updUnr [lemma, in LemmaOverloading.heaps]
upd_inj [lemma, in LemmaOverloading.heaps]
upd_nullP [lemma, in LemmaOverloading.heaps]
V
Val [constructor, in LemmaOverloading.stmod]ValForm [constructor, in LemmaOverloading.stlogR]
valid [definition, in LemmaOverloading.terms]
valid_subctx [lemma, in LemmaOverloading.terms]
valid_cat [lemma, in LemmaOverloading.terms]
valid_heaps_cat [lemma, in LemmaOverloading.terms]
valid_ptrs_cat [lemma, in LemmaOverloading.terms]
valid_cons [lemma, in LemmaOverloading.terms]
valid_heaps [definition, in LemmaOverloading.terms]
valid_ptrs [definition, in LemmaOverloading.terms]
value [definition, in LemmaOverloading.finmap]
val_gh1 [lemma, in LemmaOverloading.stlog]
val_gh [lemma, in LemmaOverloading.stlog]
val_throw [lemma, in LemmaOverloading.stlog]
val_dealloc [lemma, in LemmaOverloading.stlog]
val_allocb [lemma, in LemmaOverloading.stlog]
val_alloc [lemma, in LemmaOverloading.stlog]
val_write [lemma, in LemmaOverloading.stlog]
val_read [lemma, in LemmaOverloading.stlog]
val_ret [lemma, in LemmaOverloading.stlog]
val_do [lemma, in LemmaOverloading.stlog]
val_doR [lemma, in LemmaOverloading.stlogCTC]
val_pivot [projection, in LemmaOverloading.stlogR]
val_form [record, in LemmaOverloading.stlogR]
val_gh1R [lemma, in LemmaOverloading.stlogR]
val_ghR [lemma, in LemmaOverloading.stlogR]
val_throwR [definition, in LemmaOverloading.stlogR]
val_deallocR [lemma, in LemmaOverloading.stlogR]
val_allocbR [definition, in LemmaOverloading.stlogR]
val_allocR [definition, in LemmaOverloading.stlogR]
val_writeR [lemma, in LemmaOverloading.stlogR]
val_readR [lemma, in LemmaOverloading.stlogR]
val_retR [definition, in LemmaOverloading.stlogR]
val_doR [lemma, in LemmaOverloading.stlogR]
Var [constructor, in LemmaOverloading.terms]
vareq [definition, in LemmaOverloading.terms]
vars [definition, in LemmaOverloading.terms]
vars_hfree [lemma, in LemmaOverloading.terms]
var_pf [lemma, in LemmaOverloading.cancel]
var_tag [definition, in LemmaOverloading.cancel]
var_has [lemma, in LemmaOverloading.terms]
var_tag [definition, in LemmaOverloading.auto]
var_struct [instance, in LemmaOverloading.cancelCTC]
verify [abbreviation, in LemmaOverloading.stsep]
verify' [definition, in LemmaOverloading.stsep]
W
without_notation [definition, in LemmaOverloading.noalias]write [definition, in LemmaOverloading.stsep]
writeP [lemma, in LemmaOverloading.stsep]
write_s [definition, in LemmaOverloading.stsep]
X
xfind [record, in LemmaOverloading.xfind]XFind [constructor, in LemmaOverloading.xfind]
XFind [section, in LemmaOverloading.xfind]
xfind [projection, in LemmaOverloading.xfindCTC]
XFind [record, in LemmaOverloading.xfindCTC]
xfind [library]
xfindCTC [library]
XFind.A [variable, in LemmaOverloading.xfind]
xPredC [abbreviation, in LemmaOverloading.rels]
xPredD [abbreviation, in LemmaOverloading.rels]
xPredI [abbreviation, in LemmaOverloading.rels]
xPredT [abbreviation, in LemmaOverloading.rels]
xPredU [abbreviation, in LemmaOverloading.rels]
xPred0 [abbreviation, in LemmaOverloading.rels]
xPred1 [abbreviation, in LemmaOverloading.rels]
xPreim [abbreviation, in LemmaOverloading.rels]
XTag [constructor, in LemmaOverloading.xfind]
xtagged [record, in LemmaOverloading.xfind]
xuntag [projection, in LemmaOverloading.xfind]
x_of [projection, in LemmaOverloading.auto]
Y
y_of' [projection, in LemmaOverloading.noalias]y_of [projection, in LemmaOverloading.noalias]
other
[ _ ^^ _ by _ ] (form_scope) [notation, in LemmaOverloading.domains][ PredType of _ ] (form_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ \In _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ \In _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ \In _ & _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ \In _ & _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ \In _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ \In _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Preim _ of _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ PredC _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ PredD _ & _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ PredU _ & _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ PredI _ & _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Mem _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ : _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ : _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
[ Pred : _ | _ ] (fun_scope) [notation, in LemmaOverloading.rels]
_ \Notin _ (rel_scope) [notation, in LemmaOverloading.rels]
_ \In _ (rel_scope) [notation, in LemmaOverloading.rels]
_ ~1> _ (rel_scope) [notation, in LemmaOverloading.rels]
_ <~1> _ (rel_scope) [notation, in LemmaOverloading.rels]
_ ~> _ (rel_scope) [notation, in LemmaOverloading.rels]
_ <~> _ (rel_scope) [notation, in LemmaOverloading.rels]
_ *p _ (rel_scope) [notation, in LemmaOverloading.rels]
_ +p _ (rel_scope) [notation, in LemmaOverloading.rels]
_ :--> _ (rel_scope) [notation, in LemmaOverloading.hprop]
_ # _ (rel_scope) [notation, in LemmaOverloading.hprop]
_ ===> _ (signature_scope) [notation, in LemmaOverloading.hprop]
_ ===> _ (signature_scope) [notation, in LemmaOverloading.prelude]
If _ then _ else _ (stsep_scope) [notation, in LemmaOverloading.stsep]
match_opt _ then _ else [ _ ] _ (stsep_scope) [notation, in LemmaOverloading.stsep]
match_opt _ then _ else [ _ ] _ (stsep_scope) [notation, in LemmaOverloading.stsep]
ttry _ then _ else _ (stsep_scope) [notation, in LemmaOverloading.stsep]
ttry _ then _ else [ _ ] _ (stsep_scope) [notation, in LemmaOverloading.stsep]
ttry _ then [ _ ] _ else _ (stsep_scope) [notation, in LemmaOverloading.stsep]
ttry _ then [ _ ] _ else [ _ ] _ (stsep_scope) [notation, in LemmaOverloading.stsep]
throw [ _ ] _ (stsep_scope) [notation, in LemmaOverloading.stsep]
_ ::= _ (stsep_scope) [notation, in LemmaOverloading.stsep]
! _ (stsep_scope) [notation, in LemmaOverloading.stsep]
_ ;; _ (stsep_scope) [notation, in LemmaOverloading.stsep]
_ <-- _ ; _ (stsep_scope) [notation, in LemmaOverloading.stsep]
_ --o _ (stsep_scope) [notation, in LemmaOverloading.stsep]
_ <=p _ (type_scope) [notation, in LemmaOverloading.rels]
_ =p _ (type_scope) [notation, in LemmaOverloading.rels]
{ :: _ } (type_scope) [notation, in LemmaOverloading.rels]
{ finMap _ } (type_scope) [notation, in LemmaOverloading.finmap]
[ \/ _ , _ , _ , _ , _ | _ ] (type_scope) [notation, in LemmaOverloading.prelude]
[ \/ _ , _ , _ , _ | _ ] (type_scope) [notation, in LemmaOverloading.prelude]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [notation, in LemmaOverloading.prelude]
_ \* _ [notation, in LemmaOverloading.prelude]
_ =jm _ [notation, in LemmaOverloading.prelude]
_ :++ _ [notation, in LemmaOverloading.heaps]
_ =~ _ [notation, in LemmaOverloading.heaps]
_ :-> _ [notation, in LemmaOverloading.heaps]
_ :- _ [notation, in LemmaOverloading.heaps]
_ :+ _ [notation, in LemmaOverloading.heaps]
_ .+ _ [notation, in LemmaOverloading.heaps]
Do _ [notation, in LemmaOverloading.stsep]
() [notation, in LemmaOverloading.noalias]
[ _ ] [notation, in LemmaOverloading.stsep]
[ fin_ordMixin of _ ] [notation, in LemmaOverloading.ordtype]
Notation Index
C
[ cpo of _ ] (form_scope) [in LemmaOverloading.domains][ cpo of _ for _ ] (form_scope) [in LemmaOverloading.domains]
L
[ lattice of _ ] (form_scope) [in LemmaOverloading.domains][ lattice of _ for _ ] (form_scope) [in LemmaOverloading.domains]
O
[ ordType of _ ] (form_scope) [in LemmaOverloading.ordtype][ ordType of _ for _ ] (form_scope) [in LemmaOverloading.ordtype]
P
[ poset of _ ] (form_scope) [in LemmaOverloading.domains][ poset of _ for _ ] (form_scope) [in LemmaOverloading.domains]
_ <== _ [in LemmaOverloading.domains]
other
[ _ ^^ _ by _ ] (form_scope) [in LemmaOverloading.domains][ PredType of _ ] (form_scope) [in LemmaOverloading.rels]
[ Pred _ _ \In _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ _ \In _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ _ \In _ & _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ _ \In _ & _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ \In _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ \In _ ] (fun_scope) [in LemmaOverloading.rels]
[ Preim _ of _ ] (fun_scope) [in LemmaOverloading.rels]
[ PredC _ ] (fun_scope) [in LemmaOverloading.rels]
[ PredD _ & _ ] (fun_scope) [in LemmaOverloading.rels]
[ PredU _ & _ ] (fun_scope) [in LemmaOverloading.rels]
[ PredI _ & _ ] (fun_scope) [in LemmaOverloading.rels]
[ Mem _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ _ : _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ : _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred _ | _ ] (fun_scope) [in LemmaOverloading.rels]
[ Pred : _ | _ ] (fun_scope) [in LemmaOverloading.rels]
_ \Notin _ (rel_scope) [in LemmaOverloading.rels]
_ \In _ (rel_scope) [in LemmaOverloading.rels]
_ ~1> _ (rel_scope) [in LemmaOverloading.rels]
_ <~1> _ (rel_scope) [in LemmaOverloading.rels]
_ ~> _ (rel_scope) [in LemmaOverloading.rels]
_ <~> _ (rel_scope) [in LemmaOverloading.rels]
_ *p _ (rel_scope) [in LemmaOverloading.rels]
_ +p _ (rel_scope) [in LemmaOverloading.rels]
_ :--> _ (rel_scope) [in LemmaOverloading.hprop]
_ # _ (rel_scope) [in LemmaOverloading.hprop]
_ ===> _ (signature_scope) [in LemmaOverloading.hprop]
_ ===> _ (signature_scope) [in LemmaOverloading.prelude]
If _ then _ else _ (stsep_scope) [in LemmaOverloading.stsep]
match_opt _ then _ else [ _ ] _ (stsep_scope) [in LemmaOverloading.stsep]
match_opt _ then _ else [ _ ] _ (stsep_scope) [in LemmaOverloading.stsep]
ttry _ then _ else _ (stsep_scope) [in LemmaOverloading.stsep]
ttry _ then _ else [ _ ] _ (stsep_scope) [in LemmaOverloading.stsep]
ttry _ then [ _ ] _ else _ (stsep_scope) [in LemmaOverloading.stsep]
ttry _ then [ _ ] _ else [ _ ] _ (stsep_scope) [in LemmaOverloading.stsep]
throw [ _ ] _ (stsep_scope) [in LemmaOverloading.stsep]
_ ::= _ (stsep_scope) [in LemmaOverloading.stsep]
! _ (stsep_scope) [in LemmaOverloading.stsep]
_ ;; _ (stsep_scope) [in LemmaOverloading.stsep]
_ <-- _ ; _ (stsep_scope) [in LemmaOverloading.stsep]
_ --o _ (stsep_scope) [in LemmaOverloading.stsep]
_ <=p _ (type_scope) [in LemmaOverloading.rels]
_ =p _ (type_scope) [in LemmaOverloading.rels]
{ :: _ } (type_scope) [in LemmaOverloading.rels]
{ finMap _ } (type_scope) [in LemmaOverloading.finmap]
[ \/ _ , _ , _ , _ , _ | _ ] (type_scope) [in LemmaOverloading.prelude]
[ \/ _ , _ , _ , _ | _ ] (type_scope) [in LemmaOverloading.prelude]
[ /\ _ , _ , _ , _ , _ & _ ] (type_scope) [in LemmaOverloading.prelude]
_ \* _ [in LemmaOverloading.prelude]
_ =jm _ [in LemmaOverloading.prelude]
_ :++ _ [in LemmaOverloading.heaps]
_ =~ _ [in LemmaOverloading.heaps]
_ :-> _ [in LemmaOverloading.heaps]
_ :- _ [in LemmaOverloading.heaps]
_ :+ _ [in LemmaOverloading.heaps]
_ .+ _ [in LemmaOverloading.heaps]
Do _ [in LemmaOverloading.stsep]
() [in LemmaOverloading.noalias]
[ _ ] [in LemmaOverloading.stsep]
[ fin_ordMixin of _ ] [in LemmaOverloading.ordtype]
Module Index
C
CPO [in LemmaOverloading.domains]CPO.Exports [in LemmaOverloading.domains]
D
Dyn [in LemmaOverloading.prelude]L
Lattice [in LemmaOverloading.domains]Lattice.Exports [in LemmaOverloading.domains]
M
Model [in LemmaOverloading.stmod]N
NoAlias [in LemmaOverloading.noalias]NoAlias.Exports [in LemmaOverloading.noalias]
NoAlias2 [in LemmaOverloading.noaliasBT]
NoAlias2.Exports [in LemmaOverloading.noaliasBT]
NoAlias3 [in LemmaOverloading.noaliasBT]
NoAlias3.Exports [in LemmaOverloading.noaliasBT]
O
Ordered [in LemmaOverloading.ordtype]Ordered.Exports [in LemmaOverloading.ordtype]
P
Poset [in LemmaOverloading.domains]Poset.Exports [in LemmaOverloading.domains]
S
Scan [in LemmaOverloading.noalias]Scan.Exports [in LemmaOverloading.noalias]
Search [in LemmaOverloading.noalias]
Search.Exports [in LemmaOverloading.noalias]
Search2 [in LemmaOverloading.noalias]
Search2.Exports [in LemmaOverloading.noalias]
Variable Index
A
AdmissibleClosure.T [in LemmaOverloading.domains]AppChain.A [in LemmaOverloading.domains]
AppChain.s [in LemmaOverloading.domains]
AppChain.T [in LemmaOverloading.domains]
Append.K [in LemmaOverloading.finmap]
Append.V [in LemmaOverloading.finmap]
B
BasePrograms.A [in LemmaOverloading.stmod]BasePrograms.P [in LemmaOverloading.stmod]
BasicProperties.T [in LemmaOverloading.domains]
BlockUpdate.A [in LemmaOverloading.heaps]
C
ChainCompose.f1 [in LemmaOverloading.domains]ChainCompose.f2 [in LemmaOverloading.domains]
ChainCompose.M1 [in LemmaOverloading.domains]
ChainCompose.M2 [in LemmaOverloading.domains]
ChainCompose.s [in LemmaOverloading.domains]
ChainCompose.T1 [in LemmaOverloading.domains]
ChainCompose.T2 [in LemmaOverloading.domains]
ChainCompose.T3 [in LemmaOverloading.domains]
ChainConst.T1 [in LemmaOverloading.domains]
ChainConst.T2 [in LemmaOverloading.domains]
ChainConst.y [in LemmaOverloading.domains]
ChainId.s [in LemmaOverloading.domains]
ChainId.T [in LemmaOverloading.domains]
Chains.T [in LemmaOverloading.domains]
Coercions.T [in LemmaOverloading.prelude]
Coercions2.T [in LemmaOverloading.prelude]
CondBool.A [in LemmaOverloading.stsep]
CondBool.b [in LemmaOverloading.stsep]
CondBool.s1 [in LemmaOverloading.stsep]
CondBool.s2 [in LemmaOverloading.stsep]
CondDecide.A [in LemmaOverloading.stsep]
CondDecide.b [in LemmaOverloading.stsep]
CondDecide.p1 [in LemmaOverloading.stsep]
CondDecide.p2 [in LemmaOverloading.stsep]
CondDecide.s1 [in LemmaOverloading.stsep]
CondDecide.s2 [in LemmaOverloading.stsep]
CondNat.A [in LemmaOverloading.stsep]
CondNat.n [in LemmaOverloading.stsep]
CondNat.s1 [in LemmaOverloading.stsep]
CondNat.s2 [in LemmaOverloading.stsep]
CondOption.A [in LemmaOverloading.stsep]
CondOption.B [in LemmaOverloading.stsep]
CondOption.s1 [in LemmaOverloading.stsep]
CondOption.s2 [in LemmaOverloading.stsep]
CondOption.x [in LemmaOverloading.stsep]
CondSeq.A [in LemmaOverloading.stsep]
CondSeq.B [in LemmaOverloading.stsep]
CondSeq.s [in LemmaOverloading.stsep]
CondSeq.s1 [in LemmaOverloading.stsep]
CondSeq.s2 [in LemmaOverloading.stsep]
Continuity.D1 [in LemmaOverloading.domains]
Continuity.D2 [in LemmaOverloading.domains]
Continuity.f [in LemmaOverloading.domains]
CPO.ClassDef.cT [in LemmaOverloading.domains]
CPO.ClassDef.T [in LemmaOverloading.domains]
CPO.Exports.Laws.D [in LemmaOverloading.domains]
D
DAppChain.A [in LemmaOverloading.domains]DAppChain.s [in LemmaOverloading.domains]
DAppChain.T [in LemmaOverloading.domains]
Def.K [in LemmaOverloading.finmap]
Def.V [in LemmaOverloading.finmap]
DFunCPO.A [in LemmaOverloading.domains]
DFunCPO.B [in LemmaOverloading.domains]
DFunLattice.A [in LemmaOverloading.domains]
DFunLattice.B [in LemmaOverloading.domains]
DFunPoset.A [in LemmaOverloading.domains]
DFunPoset.B [in LemmaOverloading.domains]
DiagChain.s [in LemmaOverloading.domains]
DiagChain.T [in LemmaOverloading.domains]
DisjointUnion.K [in LemmaOverloading.finmap]
DisjointUnion.V [in LemmaOverloading.finmap]
E
EqType.K [in LemmaOverloading.finmap]EqType.V [in LemmaOverloading.finmap]
EvalAlloc.A [in LemmaOverloading.stlog]
EvalAlloc.B [in LemmaOverloading.stlog]
EvalBlockAlloc.A [in LemmaOverloading.stlog]
EvalBlockAlloc.B [in LemmaOverloading.stlog]
EvalDeallocR.A [in LemmaOverloading.stlogCTC]
EvalDeallocR.A [in LemmaOverloading.stlogR]
EvalDeallocR.B [in LemmaOverloading.stlogCTC]
EvalDeallocR.B [in LemmaOverloading.stlogR]
EvalDealloc.A [in LemmaOverloading.stlog]
EvalDealloc.B [in LemmaOverloading.stlog]
EvalDoR.A [in LemmaOverloading.stlogCTC]
EvalDoR.A [in LemmaOverloading.stlogR]
EvalDoR.B [in LemmaOverloading.stlogCTC]
EvalDoR.B [in LemmaOverloading.stlogR]
EvalDo.A [in LemmaOverloading.stlog]
EvalDo.B [in LemmaOverloading.stlog]
EvalGhostR.A [in LemmaOverloading.stlogR]
EvalGhostR.B [in LemmaOverloading.stlogR]
EvalGhostR.C [in LemmaOverloading.stlogR]
EvalGhostR.f [in LemmaOverloading.stlogR]
EvalGhostR.i [in LemmaOverloading.stlogR]
EvalGhostR.j [in LemmaOverloading.stlogR]
EvalGhostR.P [in LemmaOverloading.stlogR]
EvalGhostR.p [in LemmaOverloading.stlogR]
EvalGhostR.q [in LemmaOverloading.stlogR]
EvalGhostR.s1 [in LemmaOverloading.stlogR]
EvalGhostR.s2 [in LemmaOverloading.stlogR]
EvalGhostR.t [in LemmaOverloading.stlogR]
EvalGhost.A [in LemmaOverloading.stlog]
EvalGhost.B [in LemmaOverloading.stlog]
EvalGhost.C [in LemmaOverloading.stlog]
EvalGhost.i [in LemmaOverloading.stlog]
EvalGhost.j [in LemmaOverloading.stlog]
EvalGhost.P [in LemmaOverloading.stlog]
EvalGhost.p [in LemmaOverloading.stlog]
EvalGhost.q [in LemmaOverloading.stlog]
EvalGhost.s1 [in LemmaOverloading.stlog]
EvalGhost.s2 [in LemmaOverloading.stlog]
EvalGhost.t [in LemmaOverloading.stlog]
EvalReadR.A [in LemmaOverloading.stlogR]
EvalReadR.B [in LemmaOverloading.stlogR]
EvalRead.A [in LemmaOverloading.stlog]
EvalRead.B [in LemmaOverloading.stlog]
EvalReturn.A [in LemmaOverloading.stlog]
EvalReturn.B [in LemmaOverloading.stlog]
EvalThrow.A [in LemmaOverloading.stlog]
EvalThrow.B [in LemmaOverloading.stlog]
EvalWriteR.A [in LemmaOverloading.stlogCTC]
EvalWriteR.A [in LemmaOverloading.stlogR]
EvalWriteR.B [in LemmaOverloading.stlogCTC]
EvalWriteR.B [in LemmaOverloading.stlogR]
EvalWriteR.C [in LemmaOverloading.stlogCTC]
EvalWriteR.C [in LemmaOverloading.stlogR]
EvalWrite.A [in LemmaOverloading.stlog]
EvalWrite.B [in LemmaOverloading.stlog]
EvalWrite.C [in LemmaOverloading.stlog]
F
FinTypeOrd.T [in LemmaOverloading.ordtype]FMapInd.K [in LemmaOverloading.finmap]
FMapInd.V [in LemmaOverloading.finmap]
FunCPO.A [in LemmaOverloading.domains]
FunCPO.B [in LemmaOverloading.domains]
FunLattice.A [in LemmaOverloading.domains]
FunLattice.B [in LemmaOverloading.domains]
FunPoset.A [in LemmaOverloading.domains]
FunPoset.B [in LemmaOverloading.domains]
G
Ghosts.A [in LemmaOverloading.stsep]Ghosts.p [in LemmaOverloading.stsep]
Ghosts.s [in LemmaOverloading.stsep]
H
HasSelect.A [in LemmaOverloading.prelude]HasSelect.p [in LemmaOverloading.prelude]
I
IdealDef.T [in LemmaOverloading.domains]IdealLattice.P [in LemmaOverloading.domains]
IdealLattice.T [in LemmaOverloading.domains]
IdealPoset.P [in LemmaOverloading.domains]
IdealPoset.T [in LemmaOverloading.domains]
ImageChain.f [in LemmaOverloading.domains]
ImageChain.M [in LemmaOverloading.domains]
ImageChain.s [in LemmaOverloading.domains]
ImageChain.T1 [in LemmaOverloading.domains]
ImageChain.T2 [in LemmaOverloading.domains]
Infimum.T [in LemmaOverloading.domains]
K
Kleene.C [in LemmaOverloading.domains]Kleene.D [in LemmaOverloading.domains]
Kleene.f [in LemmaOverloading.domains]
L
LatticeCPO.A [in LemmaOverloading.domains]Lattice.ClassDef.cT [in LemmaOverloading.domains]
Lattice.ClassDef.T [in LemmaOverloading.domains]
Lattice.Exports.Laws.T [in LemmaOverloading.domains]
Lattice.RawMixin.T [in LemmaOverloading.domains]
Lat.T [in LemmaOverloading.domains]
Laws.K [in LemmaOverloading.finmap]
Laws.V [in LemmaOverloading.finmap]
Lemmas.T [in LemmaOverloading.ordtype]
LiftChain.s [in LemmaOverloading.domains]
LiftChain.T [in LemmaOverloading.domains]
ListMembership.T [in LemmaOverloading.rels]
LList.T [in LemmaOverloading.llistR]
M
Model.Allocation.A [in LemmaOverloading.stmod]Model.Allocation.v [in LemmaOverloading.stmod]
Model.Bind.A [in LemmaOverloading.stmod]
Model.Bind.B [in LemmaOverloading.stmod]
Model.Bind.e1 [in LemmaOverloading.stmod]
Model.Bind.e2 [in LemmaOverloading.stmod]
Model.Bind.s1 [in LemmaOverloading.stmod]
Model.Bind.s2 [in LemmaOverloading.stmod]
Model.BlockAllocation.A [in LemmaOverloading.stmod]
Model.BlockAllocation.n [in LemmaOverloading.stmod]
Model.BlockAllocation.v [in LemmaOverloading.stmod]
Model.Consequence.A [in LemmaOverloading.stmod]
Model.Consequence.e [in LemmaOverloading.stmod]
Model.Consequence.pf [in LemmaOverloading.stmod]
Model.Consequence.s1 [in LemmaOverloading.stmod]
Model.Consequence.s2 [in LemmaOverloading.stmod]
Model.Deallocation.x [in LemmaOverloading.stmod]
Model.Fix.A [in LemmaOverloading.stmod]
Model.Fix.B [in LemmaOverloading.stmod]
Model.Fix.f [in LemmaOverloading.stmod]
Model.Fix.s [in LemmaOverloading.stmod]
Model.Read.A [in LemmaOverloading.stmod]
Model.Read.x [in LemmaOverloading.stmod]
Model.Return.A [in LemmaOverloading.stmod]
Model.Return.x [in LemmaOverloading.stmod]
Model.Throw.A [in LemmaOverloading.stmod]
Model.Throw.e [in LemmaOverloading.stmod]
Model.Try.A [in LemmaOverloading.stmod]
Model.Try.B [in LemmaOverloading.stmod]
Model.Try.e [in LemmaOverloading.stmod]
Model.Try.e1 [in LemmaOverloading.stmod]
Model.Try.e2 [in LemmaOverloading.stmod]
Model.Try.s [in LemmaOverloading.stmod]
Model.Try.s1 [in LemmaOverloading.stmod]
Model.Try.s2 [in LemmaOverloading.stmod]
Model.Write.A [in LemmaOverloading.stmod]
Model.Write.v [in LemmaOverloading.stmod]
Model.Write.x [in LemmaOverloading.stmod]
N
NullLemmas.d [in LemmaOverloading.heaps]NullLemmas.f [in LemmaOverloading.heaps]
NullLemmas.g [in LemmaOverloading.heaps]
NullLemmas.x [in LemmaOverloading.heaps]
O
Ops.K [in LemmaOverloading.finmap]Ops.V [in LemmaOverloading.finmap]
Ordered.ClassDef.cT [in LemmaOverloading.ordtype]
Ordered.ClassDef.T [in LemmaOverloading.ordtype]
P
PairCPO.A [in LemmaOverloading.domains]PairCPO.B [in LemmaOverloading.domains]
PairLattice.A [in LemmaOverloading.domains]
PairLattice.B [in LemmaOverloading.domains]
PairPoset.A [in LemmaOverloading.domains]
PairPoset.B [in LemmaOverloading.domains]
Permutations.A [in LemmaOverloading.perms]
Poset.ClassDef.cT [in LemmaOverloading.domains]
Poset.ClassDef.T [in LemmaOverloading.domains]
Poset.Exports.Laws.T [in LemmaOverloading.domains]
PredCPO.A [in LemmaOverloading.domains]
Predicates.T [in LemmaOverloading.rels]
PredLattice.A [in LemmaOverloading.domains]
PredPoset.A [in LemmaOverloading.domains]
Prefix.A [in LemmaOverloading.prefix]
ProdChain.f1 [in LemmaOverloading.domains]
ProdChain.f2 [in LemmaOverloading.domains]
ProdChain.M1 [in LemmaOverloading.domains]
ProdChain.M2 [in LemmaOverloading.domains]
ProdChain.s [in LemmaOverloading.domains]
ProdChain.S1 [in LemmaOverloading.domains]
ProdChain.S2 [in LemmaOverloading.domains]
ProdChain.T1 [in LemmaOverloading.domains]
ProdChain.T2 [in LemmaOverloading.domains]
ProdOrd.K [in LemmaOverloading.ordtype]
ProdOrd.T [in LemmaOverloading.ordtype]
ProjChain.s [in LemmaOverloading.domains]
ProjChain.T1 [in LemmaOverloading.domains]
ProjChain.T2 [in LemmaOverloading.domains]
R
ReflectConnectives.b1 [in LemmaOverloading.prelude]ReflectConnectives.b2 [in LemmaOverloading.prelude]
ReflectConnectives.b3 [in LemmaOverloading.prelude]
ReflectConnectives.b4 [in LemmaOverloading.prelude]
ReflectConnectives.b5 [in LemmaOverloading.prelude]
ReflectConnectives.b6 [in LemmaOverloading.prelude]
RelLaws.T [in LemmaOverloading.rels]
RelProperties.pT [in LemmaOverloading.rels]
RelProperties.T [in LemmaOverloading.rels]
Reorder.A [in LemmaOverloading.prelude]
Reorder.B [in LemmaOverloading.prelude]
Reorder.C [in LemmaOverloading.prelude]
S
SepAlloc.A [in LemmaOverloading.stsep]SepAlloc.v [in LemmaOverloading.stsep]
SepBind.A [in LemmaOverloading.stsep]
SepBind.B [in LemmaOverloading.stsep]
SepBind.e1 [in LemmaOverloading.stsep]
SepBind.e2 [in LemmaOverloading.stsep]
SepBind.s1 [in LemmaOverloading.stsep]
SepBind.s2 [in LemmaOverloading.stsep]
SepBlockAlloc.A [in LemmaOverloading.stsep]
SepBlockAlloc.n [in LemmaOverloading.stsep]
SepBlockAlloc.v [in LemmaOverloading.stsep]
SepConseq.A [in LemmaOverloading.stsep]
SepConseq.e [in LemmaOverloading.stsep]
SepConseq.pf [in LemmaOverloading.stsep]
SepConseq.s1 [in LemmaOverloading.stsep]
SepConseq.s2 [in LemmaOverloading.stsep]
SepDealloc.x [in LemmaOverloading.stsep]
SepFix.A [in LemmaOverloading.stsep]
SepFix.B [in LemmaOverloading.stsep]
SepFix.s [in LemmaOverloading.stsep]
SepFrame.A [in LemmaOverloading.stsep]
SepFrame.s [in LemmaOverloading.stsep]
SepRead.A [in LemmaOverloading.stsep]
SepRead.x [in LemmaOverloading.stsep]
SepReturn.A [in LemmaOverloading.stsep]
SepReturn.x [in LemmaOverloading.stsep]
SepThrow.A [in LemmaOverloading.stsep]
SepThrow.e [in LemmaOverloading.stsep]
SepTry.A [in LemmaOverloading.stsep]
SepTry.B [in LemmaOverloading.stsep]
SepTry.e [in LemmaOverloading.stsep]
SepTry.e1 [in LemmaOverloading.stsep]
SepTry.e2 [in LemmaOverloading.stsep]
SepTry.s [in LemmaOverloading.stsep]
SepTry.s1 [in LemmaOverloading.stsep]
SepTry.s2 [in LemmaOverloading.stsep]
SepWrite.A [in LemmaOverloading.stsep]
SepWrite.v [in LemmaOverloading.stsep]
SepWrite.x [in LemmaOverloading.stsep]
Simplifications.pT [in LemmaOverloading.rels]
Simplifications.T [in LemmaOverloading.rels]
STDef.A [in LemmaOverloading.stmod]
STDef.s [in LemmaOverloading.stmod]
SubCPO.C [in LemmaOverloading.domains]
SubCPO.D [in LemmaOverloading.domains]
SubCPO.s [in LemmaOverloading.domains]
SubLattice.C [in LemmaOverloading.domains]
SubLattice.s [in LemmaOverloading.domains]
SubLattice.T [in LemmaOverloading.domains]
SubMemLaws.T [in LemmaOverloading.rels]
SubPoset.C [in LemmaOverloading.domains]
SubPoset.s [in LemmaOverloading.domains]
SubPoset.T [in LemmaOverloading.domains]
T
Totality.K [in LemmaOverloading.ordtype]X
XFind.A [in LemmaOverloading.xfind]Library Index
A
autoC
cancelcancelCTC
cancelD
cancel2
D
domainsF
finmapH
heapshprop
I
indomindomCTC
L
llistRN
noaliasnoaliasBT
noaliasCTC
O
ordtypeP
permsprefix
prelude
R
relsS
stlogstlogCTC
stlogR
stmod
stsep
T
termsX
xfindxfindCTC
Lemma Index
A
allC [in LemmaOverloading.stsep]allocbP [in LemmaOverloading.stsep]
allocP [in LemmaOverloading.stsep]
andFp [in LemmaOverloading.rels]
andpF [in LemmaOverloading.rels]
andpT [in LemmaOverloading.rels]
andTp [in LemmaOverloading.rels]
and6P [in LemmaOverloading.prelude]
antiframe [in LemmaOverloading.stsep]
app_cont [in LemmaOverloading.domains]
app_mono [in LemmaOverloading.domains]
auto [in LemmaOverloading.auto]
B
bindP [in LemmaOverloading.stsep]bla [in LemmaOverloading.xfindCTC]
blah [in LemmaOverloading.stlog]
blah2 [in LemmaOverloading.stlog]
bnd_gh1 [in LemmaOverloading.stlog]
bnd_gh [in LemmaOverloading.stlog]
bnd_throw [in LemmaOverloading.stlog]
bnd_dealloc [in LemmaOverloading.stlog]
bnd_allocb [in LemmaOverloading.stlog]
bnd_alloc [in LemmaOverloading.stlog]
bnd_write [in LemmaOverloading.stlog]
bnd_read [in LemmaOverloading.stlog]
bnd_ret [in LemmaOverloading.stlog]
bnd_do [in LemmaOverloading.stlog]
bnd_is_try [in LemmaOverloading.stlog]
bnd_deallocR [in LemmaOverloading.stlogCTC]
bnd_writeR [in LemmaOverloading.stlogCTC]
bnd_gh1R [in LemmaOverloading.stlogR]
bnd_ghR [in LemmaOverloading.stlogR]
bnd_deallocR [in LemmaOverloading.stlogR]
bnd_writeR [in LemmaOverloading.stlogR]
bnd_readR [in LemmaOverloading.stlogR]
bnd_doR [in LemmaOverloading.stlogR]
bot_runs [in LemmaOverloading.stmod]
bound [in LemmaOverloading.stmod]
C
cancel [in LemmaOverloading.cancel2]cancel [in LemmaOverloading.heaps]
cancelR [in LemmaOverloading.cancel]
cancelR [in LemmaOverloading.cancelCTC]
cancelT [in LemmaOverloading.heaps]
cancel_sound [in LemmaOverloading.terms]
cancel_sound' [in LemmaOverloading.terms]
cancel_ins [in LemmaOverloading.finmap]
cancel1 [in LemmaOverloading.cancel2]
cancel2 [in LemmaOverloading.cancel2]
cexit1 [in LemmaOverloading.heaps]
cexit2 [in LemmaOverloading.heaps]
cexit3 [in LemmaOverloading.heaps]
chainE [in LemmaOverloading.domains]
chain_clos_diag [in LemmaOverloading.domains]
chain_closI [in LemmaOverloading.domains]
chain_clos_mono [in LemmaOverloading.domains]
chain_clos_idemp [in LemmaOverloading.domains]
chain_closP [in LemmaOverloading.domains]
chain_clos_min [in LemmaOverloading.domains]
chain_clos_sub [in LemmaOverloading.domains]
compA [in LemmaOverloading.prelude]
compf1 [in LemmaOverloading.prelude]
comp_cont [in LemmaOverloading.domains]
comp_chainE [in LemmaOverloading.domains]
comp_mono [in LemmaOverloading.domains]
comp1f [in LemmaOverloading.prelude]
congeqUh [in LemmaOverloading.heaps]
congUh [in LemmaOverloading.heaps]
conseq_refl [in LemmaOverloading.stsep]
const_cont [in LemmaOverloading.domains]
const_chainE [in LemmaOverloading.domains]
const_chainP [in LemmaOverloading.domains]
const_mono [in LemmaOverloading.domains]
contE [in LemmaOverloading.domains]
contV [in LemmaOverloading.prelude]
contVT [in LemmaOverloading.prelude]
cont_mono [in LemmaOverloading.domains]
countN_varfree [in LemmaOverloading.terms]
count0_hfree [in LemmaOverloading.terms]
count1_hfree [in LemmaOverloading.terms]
CPO.Exports.limM [in LemmaOverloading.domains]
CPO.Exports.limP [in LemmaOverloading.domains]
D
dapp_cont [in LemmaOverloading.domains]dapp_mono [in LemmaOverloading.domains]
deallocP [in LemmaOverloading.stsep]
defE [in LemmaOverloading.heaps]
defF [in LemmaOverloading.heaps]
defFUn [in LemmaOverloading.heaps]
defPt [in LemmaOverloading.heaps]
defPtUn [in LemmaOverloading.heaps]
defPt_dom [in LemmaOverloading.heaps]
defPt_def [in LemmaOverloading.heaps]
defPt_null [in LemmaOverloading.heaps]
defR [in LemmaOverloading.terms]
defU [in LemmaOverloading.heaps]
defUn [in LemmaOverloading.heaps]
defUnF [in LemmaOverloading.heaps]
defUnhh [in LemmaOverloading.heaps]
defUnl [in LemmaOverloading.heaps]
defUnr [in LemmaOverloading.heaps]
def_runs [in LemmaOverloading.stmod]
def0 [in LemmaOverloading.heaps]
dfun_limM [in LemmaOverloading.domains]
dfun_limP [in LemmaOverloading.domains]
dfun_supM [in LemmaOverloading.domains]
dfun_supP [in LemmaOverloading.domains]
dfun_trans [in LemmaOverloading.domains]
dfun_asym [in LemmaOverloading.domains]
dfun_refl [in LemmaOverloading.domains]
dfun_botP [in LemmaOverloading.domains]
diag_cont [in LemmaOverloading.domains]
diag_mono [in LemmaOverloading.domains]
disjC [in LemmaOverloading.finmap]
disjP [in LemmaOverloading.finmap]
disj_fcat [in LemmaOverloading.finmap]
disj_remE [in LemmaOverloading.finmap]
disj_rem [in LemmaOverloading.finmap]
disj_ins [in LemmaOverloading.finmap]
disj_nil [in LemmaOverloading.finmap]
domF [in LemmaOverloading.heaps]
domPt [in LemmaOverloading.heaps]
domPtUn [in LemmaOverloading.heaps]
domPtUnX [in LemmaOverloading.heaps]
domPtX [in LemmaOverloading.heaps]
domR [in LemmaOverloading.terms]
domU [in LemmaOverloading.heaps]
domUn [in LemmaOverloading.heaps]
dom_hfresh [in LemmaOverloading.heaps]
dom_lfresh [in LemmaOverloading.heaps]
dom_in_notin [in LemmaOverloading.heaps]
dom_notin_notin [in LemmaOverloading.heaps]
dom_fresh [in LemmaOverloading.heaps]
dom_look [in LemmaOverloading.heaps]
dom_free [in LemmaOverloading.heaps]
dom_def [in LemmaOverloading.heaps]
dom_null [in LemmaOverloading.heaps]
dom0 [in LemmaOverloading.heaps]
doP [in LemmaOverloading.stsep]
dyn_injT [in LemmaOverloading.prelude]
dyn_eta [in LemmaOverloading.prelude]
dyn_inj [in LemmaOverloading.prelude]
E
empbE [in LemmaOverloading.heaps]empP [in LemmaOverloading.heaps]
empPt [in LemmaOverloading.heaps]
empty_pf [in LemmaOverloading.cancel]
empty_hfree [in LemmaOverloading.terms]
empU [in LemmaOverloading.heaps]
empUn [in LemmaOverloading.heaps]
emp_pick [in LemmaOverloading.heaps]
eqc [in LemmaOverloading.prelude]
eqc2 [in LemmaOverloading.prelude]
eqexnP [in LemmaOverloading.stmod]
eqfun_trans [in LemmaOverloading.rels]
eqfun_sym [in LemmaOverloading.rels]
eqfun_refl [in LemmaOverloading.rels]
EqPredType_trans' [in LemmaOverloading.rels]
EqPredType_sym [in LemmaOverloading.rels]
EqPredType_refl [in LemmaOverloading.rels]
eqUh [in LemmaOverloading.heaps]
eq_ptrP [in LemmaOverloading.heaps]
eta [in LemmaOverloading.prelude]
eval_rcons [in LemmaOverloading.terms]
eval_cat [in LemmaOverloading.terms]
eval_cons [in LemmaOverloading.terms]
exit1 [in LemmaOverloading.heaps]
exit2 [in LemmaOverloading.heaps]
exit3 [in LemmaOverloading.heaps]
exit4 [in LemmaOverloading.heaps]
ext [in LemmaOverloading.prelude]
extend_pf [in LemmaOverloading.xfind]
F
fcatA [in LemmaOverloading.finmap]fcatAC [in LemmaOverloading.finmap]
fcatC [in LemmaOverloading.finmap]
fcatCA [in LemmaOverloading.finmap]
fcatKs [in LemmaOverloading.finmap]
fcatsK [in LemmaOverloading.finmap]
fcats0 [in LemmaOverloading.finmap]
fcat_srem [in LemmaOverloading.finmap]
fcat_rems [in LemmaOverloading.finmap]
fcat_sins [in LemmaOverloading.finmap]
fcat_inss [in LemmaOverloading.finmap]
fcat_nil' [in LemmaOverloading.finmap]
fcat_ins' [in LemmaOverloading.finmap]
fcat0s [in LemmaOverloading.finmap]
feqP [in LemmaOverloading.finmap]
findme [in LemmaOverloading.xfind]
find2E [in LemmaOverloading.noaliasCTC]
fmapE [in LemmaOverloading.finmap]
fmapP [in LemmaOverloading.finmap]
fmap_ind2 [in LemmaOverloading.finmap]
fmap_ind' [in LemmaOverloading.finmap]
fnd_fcat [in LemmaOverloading.finmap]
fnd_supp_in [in LemmaOverloading.finmap]
fnd_supp [in LemmaOverloading.finmap]
fnd_ins [in LemmaOverloading.finmap]
fnd_rem [in LemmaOverloading.finmap]
fnd_empty [in LemmaOverloading.finmap]
found_pf [in LemmaOverloading.xfind]
found_pf [in LemmaOverloading.indom]
found_pf [in LemmaOverloading.stlogR]
frame [in LemmaOverloading.stsep]
frame0 [in LemmaOverloading.stsep]
frame1 [in LemmaOverloading.stsep]
freeF [in LemmaOverloading.heaps]
freePtUn [in LemmaOverloading.heaps]
freeR [in LemmaOverloading.terms]
freeU [in LemmaOverloading.heaps]
freeUn [in LemmaOverloading.heaps]
freeUnD [in LemmaOverloading.heaps]
freeUnl [in LemmaOverloading.heaps]
freeUnr [in LemmaOverloading.heaps]
free_nullP [in LemmaOverloading.heaps]
free0 [in LemmaOverloading.heaps]
fresh_null [in LemmaOverloading.heaps]
fr_pre [in LemmaOverloading.stsep]
fun_limM [in LemmaOverloading.domains]
fun_limP [in LemmaOverloading.domains]
fun_supM [in LemmaOverloading.domains]
fun_supP [in LemmaOverloading.domains]
fun_trans [in LemmaOverloading.domains]
fun_asym [in LemmaOverloading.domains]
fun_refl [in LemmaOverloading.domains]
fun_botP [in LemmaOverloading.domains]
G
ghE [in LemmaOverloading.stsep]H
hasPx [in LemmaOverloading.prelude]hdomP [in LemmaOverloading.heaps]
heapE [in LemmaOverloading.heaps]
heap_etaP [in LemmaOverloading.heaps]
heap_eta [in LemmaOverloading.heaps]
hfreeE [in LemmaOverloading.terms]
hfreeN [in LemmaOverloading.terms]
hfree_def [in LemmaOverloading.terms]
hfree_subdom' [in LemmaOverloading.terms]
hfree_subdom [in LemmaOverloading.terms]
hfresh_null [in LemmaOverloading.heaps]
hfresh_high [in LemmaOverloading.heaps]
highPn [in LemmaOverloading.heaps]
highPtUn [in LemmaOverloading.heaps]
highPtUn2 [in LemmaOverloading.heaps]
high_lowD [in LemmaOverloading.heaps]
hlE [in LemmaOverloading.heaps]
I
ideal_supM [in LemmaOverloading.domains]ideal_supP [in LemmaOverloading.domains]
ideal_supP' [in LemmaOverloading.domains]
ideal_trans [in LemmaOverloading.domains]
ideal_asym [in LemmaOverloading.domains]
ideal_refl [in LemmaOverloading.domains]
ideal_botP [in LemmaOverloading.domains]
id_cont [in LemmaOverloading.domains]
id_chainE [in LemmaOverloading.domains]
id_mono [in LemmaOverloading.domains]
image_chainP [in LemmaOverloading.domains]
impC [in LemmaOverloading.stsep]
indom [in LemmaOverloading.indom]
infM [in LemmaOverloading.domains]
infP [in LemmaOverloading.domains]
injUh [in LemmaOverloading.heaps]
inj_sval [in LemmaOverloading.prelude]
ins_ins [in LemmaOverloading.finmap]
ins_rem [in LemmaOverloading.finmap]
interp_subctx [in LemmaOverloading.terms]
interp_perm [in LemmaOverloading.terms]
interp_cat [in LemmaOverloading.terms]
interp_cons [in LemmaOverloading.terms]
In_nil [in LemmaOverloading.rels]
In_cons [in LemmaOverloading.rels]
In_Simpl [in LemmaOverloading.rels]
in_split [in LemmaOverloading.perms]
irA [in LemmaOverloading.prelude]
irr [in LemmaOverloading.ordtype]
irr_ordf [in LemmaOverloading.ordtype]
irr_lex [in LemmaOverloading.ordtype]
irr_ltn_nat [in LemmaOverloading.ordtype]
J
jmE [in LemmaOverloading.prelude]jmeq_refl [in LemmaOverloading.prelude]
jm2E [in LemmaOverloading.prelude]
K
kleene_lfp_least [in LemmaOverloading.domains]kleene_lfp_fixed [in LemmaOverloading.domains]
L
last_ins' [in LemmaOverloading.finmap]last_inv [in LemmaOverloading.heaps]
Lattice.Exports.supM [in LemmaOverloading.domains]
Lattice.Exports.supP [in LemmaOverloading.domains]
lat_limM [in LemmaOverloading.domains]
lat_limP [in LemmaOverloading.domains]
ldomK [in LemmaOverloading.heaps]
ldomP [in LemmaOverloading.heaps]
ldomUn [in LemmaOverloading.heaps]
left_pf [in LemmaOverloading.indom]
left_pf [in LemmaOverloading.stlogR]
lfresh_null [in LemmaOverloading.heaps]
lfresh_low [in LemmaOverloading.heaps]
lhE [in LemmaOverloading.heaps]
lift_chainP [in LemmaOverloading.domains]
limE [in LemmaOverloading.domains]
lim_dappE [in LemmaOverloading.domains]
lim_appE [in LemmaOverloading.domains]
lim_liftE [in LemmaOverloading.domains]
lim_mono [in LemmaOverloading.domains]
locality [in LemmaOverloading.stsep]
lookF [in LemmaOverloading.heaps]
lookPtUn [in LemmaOverloading.heaps]
lookR [in LemmaOverloading.terms]
lookU [in LemmaOverloading.heaps]
lookUnl [in LemmaOverloading.heaps]
lookUnr [in LemmaOverloading.heaps]
loweqE [in LemmaOverloading.heaps]
loweqK [in LemmaOverloading.heaps]
loweqP [in LemmaOverloading.heaps]
lowPn [in LemmaOverloading.heaps]
lowPtUn [in LemmaOverloading.heaps]
lowUn [in LemmaOverloading.heaps]
low_trans [in LemmaOverloading.heaps]
low_sym [in LemmaOverloading.heaps]
low_refl [in LemmaOverloading.heaps]
lseg_case [in LemmaOverloading.llistR]
lseg_empty [in LemmaOverloading.llistR]
lseg_neq [in LemmaOverloading.llistR]
lseg_null [in LemmaOverloading.llistR]
lseg_add_last [in LemmaOverloading.llistR]
lseq_pos [in LemmaOverloading.llistR]
lseq_null [in LemmaOverloading.llistR]
ltn_ptr_total [in LemmaOverloading.heaps]
ltn_ptr_trans [in LemmaOverloading.heaps]
ltn_ptr_irr [in LemmaOverloading.heaps]
M
Mem_Seq1 [in LemmaOverloading.rels]Mem_Mem [in LemmaOverloading.rels]
Mem_Simpl [in LemmaOverloading.rels]
Mem_toPred [in LemmaOverloading.rels]
modelE [in LemmaOverloading.stmod]
model_runs [in LemmaOverloading.stmod]
Model.allocb_has_spec [in LemmaOverloading.stmod]
Model.allocb_dstrict [in LemmaOverloading.stmod]
Model.allocb_coherent [in LemmaOverloading.stmod]
Model.alloc_has_spec [in LemmaOverloading.stmod]
Model.alloc_dstrict [in LemmaOverloading.stmod]
Model.alloc_coherent [in LemmaOverloading.stmod]
Model.bind_has_spec [in LemmaOverloading.stmod]
Model.bind_dstrict [in LemmaOverloading.stmod]
Model.bind_coherent [in LemmaOverloading.stmod]
Model.conseq_refl [in LemmaOverloading.stmod]
Model.dealloc_has_spec [in LemmaOverloading.stmod]
Model.dealloc_dstrict [in LemmaOverloading.stmod]
Model.dealloc_coherent [in LemmaOverloading.stmod]
Model.do_has_spec [in LemmaOverloading.stmod]
Model.do_dstrict [in LemmaOverloading.stmod]
Model.do_coherent [in LemmaOverloading.stmod]
Model.read_has_spec [in LemmaOverloading.stmod]
Model.read_dstrict [in LemmaOverloading.stmod]
Model.read_coherent [in LemmaOverloading.stmod]
Model.ret_has_spec [in LemmaOverloading.stmod]
Model.ret_dstrict [in LemmaOverloading.stmod]
Model.ret_coherent [in LemmaOverloading.stmod]
Model.throw_has_spec [in LemmaOverloading.stmod]
Model.throw_dstrict [in LemmaOverloading.stmod]
Model.throw_coherent [in LemmaOverloading.stmod]
Model.try_has_spec [in LemmaOverloading.stmod]
Model.try_dstrict [in LemmaOverloading.stmod]
Model.try_coherent [in LemmaOverloading.stmod]
Model.write_has_spec [in LemmaOverloading.stmod]
Model.write_dstrict [in LemmaOverloading.stmod]
Model.write_coherent [in LemmaOverloading.stmod]
modnS [in LemmaOverloading.heaps]
N
nat_chain_axiom [in LemmaOverloading.domains]nat_trans [in LemmaOverloading.domains]
nat_asym [in LemmaOverloading.domains]
nat_refl [in LemmaOverloading.domains]
nat_botP [in LemmaOverloading.domains]
noalias [in LemmaOverloading.heaps]
noaliasR [in LemmaOverloading.noaliasCTC]
noaliasR [in LemmaOverloading.noalias]
noaliasR [in LemmaOverloading.noaliasBT]
noaliasR_fwd3' [in LemmaOverloading.noalias]
noaliasR_fwd3 [in LemmaOverloading.noalias]
noaliasR_fwd_wrong1 [in LemmaOverloading.noalias]
noaliasR_fwd1 [in LemmaOverloading.noalias]
noaliasR2 [in LemmaOverloading.noaliasBT]
NoAlias.noalias_pf [in LemmaOverloading.noalias]
NoAlias2.start_pf [in LemmaOverloading.noaliasBT]
NoAlias3.noalias_pf [in LemmaOverloading.noaliasBT]
notin_filter [in LemmaOverloading.finmap]
notin_path [in LemmaOverloading.finmap]
nsym [in LemmaOverloading.ordtype]
O
onth_size [in LemmaOverloading.prefix]opn [in LemmaOverloading.stlog]
ord_path [in LemmaOverloading.finmap]
orFp [in LemmaOverloading.rels]
orpF [in LemmaOverloading.rels]
orpT [in LemmaOverloading.rels]
orrA [in LemmaOverloading.rels]
orrAb [in LemmaOverloading.rels]
orrAC [in LemmaOverloading.rels]
orrC [in LemmaOverloading.rels]
orrCA [in LemmaOverloading.rels]
orrI [in LemmaOverloading.rels]
orr0 [in LemmaOverloading.rels]
orTp [in LemmaOverloading.rels]
or0r [in LemmaOverloading.rels]
or5P [in LemmaOverloading.prelude]
or6P [in LemmaOverloading.prelude]
P
pair_limM [in LemmaOverloading.domains]pair_limP [in LemmaOverloading.domains]
pair_supM [in LemmaOverloading.domains]
pair_supP [in LemmaOverloading.domains]
pair_trans [in LemmaOverloading.domains]
pair_asym [in LemmaOverloading.domains]
pair_refl [in LemmaOverloading.domains]
pair_botP [in LemmaOverloading.domains]
path_supp_ins_inv [in LemmaOverloading.finmap]
path_supp_ins [in LemmaOverloading.finmap]
path_supp_ord [in LemmaOverloading.finmap]
path_ins' [in LemmaOverloading.finmap]
path_filter [in LemmaOverloading.heaps]
path_last [in LemmaOverloading.heaps]
perm_catCA [in LemmaOverloading.perms]
perm_catAC [in LemmaOverloading.perms]
perm_cat2r [in LemmaOverloading.perms]
perm_cat2l [in LemmaOverloading.perms]
perm_cat_cons [in LemmaOverloading.perms]
perm_cons_cat_cons [in LemmaOverloading.perms]
perm_cons [in LemmaOverloading.perms]
perm_cat_consR [in LemmaOverloading.perms]
perm_ind2 [in LemmaOverloading.perms]
perm_cons_cat_consL [in LemmaOverloading.perms]
perm_cons_catAC [in LemmaOverloading.perms]
perm_cons_catCA [in LemmaOverloading.perms]
perm_catC [in LemmaOverloading.perms]
perm_cat_consL [in LemmaOverloading.perms]
perm_catL [in LemmaOverloading.perms]
perm_cat2rL [in LemmaOverloading.perms]
perm_cat2lL [in LemmaOverloading.perms]
perm_in [in LemmaOverloading.perms]
perm_trans [in LemmaOverloading.perms]
perm_sym [in LemmaOverloading.perms]
perm_refl [in LemmaOverloading.perms]
perm_nil [in LemmaOverloading.perms]
pfreeE [in LemmaOverloading.terms]
pfreeN [in LemmaOverloading.terms]
pfree_def [in LemmaOverloading.terms]
pfree_subdom [in LemmaOverloading.terms]
pickP [in LemmaOverloading.heaps]
Poset.Exports.botP [in LemmaOverloading.domains]
Poset.Exports.poset_trans [in LemmaOverloading.domains]
Poset.Exports.poset_asym [in LemmaOverloading.domains]
Poset.Exports.poset_refl [in LemmaOverloading.domains]
pow_mono [in LemmaOverloading.domains]
predkN [in LemmaOverloading.finmap]
prefix_onth [in LemmaOverloading.prefix]
prefix_size [in LemmaOverloading.prefix]
prefix_cons' [in LemmaOverloading.prefix]
prefix_cons [in LemmaOverloading.prefix]
prefix_trans [in LemmaOverloading.prefix]
prefix_refl [in LemmaOverloading.prefix]
prod_cont [in LemmaOverloading.domains]
prod_mono [in LemmaOverloading.domains]
proj1_cont [in LemmaOverloading.domains]
proj1_prodE [in LemmaOverloading.domains]
proj1_diagE [in LemmaOverloading.domains]
proj1_mono [in LemmaOverloading.domains]
proj2_cont [in LemmaOverloading.domains]
proj2_prodE [in LemmaOverloading.domains]
proj2_diagE [in LemmaOverloading.domains]
proj2_mono [in LemmaOverloading.domains]
proof_irrelevance [in LemmaOverloading.prelude]
prop_limM [in LemmaOverloading.domains]
prop_limP [in LemmaOverloading.domains]
prop_supM [in LemmaOverloading.domains]
prop_supP [in LemmaOverloading.domains]
prop_trans [in LemmaOverloading.domains]
prop_asym [in LemmaOverloading.domains]
prop_refl [in LemmaOverloading.domains]
prop_botP [in LemmaOverloading.domains]
ptrA [in LemmaOverloading.heaps]
ptrE [in LemmaOverloading.heaps]
ptrK [in LemmaOverloading.heaps]
ptrT [in LemmaOverloading.heaps]
ptr_has [in LemmaOverloading.terms]
ptr_null [in LemmaOverloading.heaps]
ptr0 [in LemmaOverloading.heaps]
pts_pf [in LemmaOverloading.cancel]
pts_inj [in LemmaOverloading.heaps]
pts_injT [in LemmaOverloading.heaps]
pts_injP [in LemmaOverloading.heaps]
R
rACI [in LemmaOverloading.prelude]rCAI [in LemmaOverloading.prelude]
readP [in LemmaOverloading.stsep]
recurse_pf [in LemmaOverloading.xfind]
refl_jmeq2 [in LemmaOverloading.prelude]
reindex [in LemmaOverloading.domains]
relaxP [in LemmaOverloading.domains]
rem_supp [in LemmaOverloading.finmap]
rem_ins [in LemmaOverloading.finmap]
rem_rem [in LemmaOverloading.finmap]
rem_empty [in LemmaOverloading.finmap]
retP [in LemmaOverloading.stsep]
riA [in LemmaOverloading.prelude]
right_pf [in LemmaOverloading.indom]
right_pf [in LemmaOverloading.stlogR]
S
scanE [in LemmaOverloading.noaliasCTC]scan_it [in LemmaOverloading.noalias]
Scan.default_pf [in LemmaOverloading.noalias]
Scan.ptr_pf [in LemmaOverloading.noalias]
Scan.scanE [in LemmaOverloading.noalias]
Scan.union_pf [in LemmaOverloading.noalias]
Search.findE [in LemmaOverloading.noalias]
Search.found_pf [in LemmaOverloading.noalias]
Search.recurse_pf [in LemmaOverloading.noalias]
Search2.find2E [in LemmaOverloading.noalias]
Search2.foundx_pf [in LemmaOverloading.noalias]
Search2.foundy_pf [in LemmaOverloading.noalias]
Search2.foundz_pf [in LemmaOverloading.noalias]
seqof_ins [in LemmaOverloading.finmap]
sexit1 [in LemmaOverloading.heaps]
sexit2 [in LemmaOverloading.heaps]
sexit3 [in LemmaOverloading.heaps]
sexit4 [in LemmaOverloading.heaps]
simplify [in LemmaOverloading.cancelD]
Simpl_PredE [in LemmaOverloading.rels]
singleP [in LemmaOverloading.stmod]
size_onth [in LemmaOverloading.prefix]
sorted_filter [in LemmaOverloading.finmap]
sorted_ins' [in LemmaOverloading.finmap]
sorted_nil [in LemmaOverloading.finmap]
spec_runs [in LemmaOverloading.stmod]
starA [in LemmaOverloading.hprop]
starAC [in LemmaOverloading.hprop]
starC [in LemmaOverloading.hprop]
starCA [in LemmaOverloading.hprop]
starp0 [in LemmaOverloading.hprop]
star0p [in LemmaOverloading.hprop]
st_supM [in LemmaOverloading.stmod]
st_supP [in LemmaOverloading.stmod]
st_sup_has_spec [in LemmaOverloading.stmod]
st_sup_dstrict [in LemmaOverloading.stmod]
st_sup_coherent [in LemmaOverloading.stmod]
st_botP [in LemmaOverloading.stmod]
st_bot_has_spec [in LemmaOverloading.stmod]
st_bot_dstrict [in LemmaOverloading.stmod]
st_bot_coherent [in LemmaOverloading.stmod]
st_trans [in LemmaOverloading.stmod]
st_asym [in LemmaOverloading.stmod]
st_refl [in LemmaOverloading.stmod]
subctx_trans [in LemmaOverloading.terms]
subctx_refl [in LemmaOverloading.terms]
subdomD [in LemmaOverloading.heaps]
subdomE [in LemmaOverloading.heaps]
subdomP [in LemmaOverloading.heaps]
subdomPE [in LemmaOverloading.heaps]
subdomQ [in LemmaOverloading.heaps]
subdomUE [in LemmaOverloading.heaps]
subdom_trans [in LemmaOverloading.heaps]
subdom_emp_inv [in LemmaOverloading.heaps]
subdom_emp [in LemmaOverloading.heaps]
subdom_refl [in LemmaOverloading.heaps]
subdom_def [in LemmaOverloading.heaps]
subheapE [in LemmaOverloading.heaps]
subheapUn [in LemmaOverloading.heaps]
subheapUnl [in LemmaOverloading.heaps]
subheapUnr [in LemmaOverloading.heaps]
subheap_id [in LemmaOverloading.heaps]
subheap_trans [in LemmaOverloading.heaps]
subheap_def [in LemmaOverloading.heaps]
subheap_refl [in LemmaOverloading.heaps]
SubPredType_trans' [in LemmaOverloading.rels]
SubPredType_refl [in LemmaOverloading.rels]
subp_andr [in LemmaOverloading.rels]
subp_andl [in LemmaOverloading.rels]
subp_orr [in LemmaOverloading.rels]
subp_orl [in LemmaOverloading.rels]
subp_and [in LemmaOverloading.rels]
subp_or [in LemmaOverloading.rels]
subp_trans [in LemmaOverloading.rels]
subp_asym [in LemmaOverloading.rels]
subp_refl [in LemmaOverloading.rels]
sub_limM [in LemmaOverloading.domains]
sub_limP [in LemmaOverloading.domains]
sub_limX [in LemmaOverloading.domains]
sub_supM [in LemmaOverloading.domains]
sub_supP [in LemmaOverloading.domains]
sub_supX [in LemmaOverloading.domains]
sub_trans [in LemmaOverloading.domains]
sub_asym [in LemmaOverloading.domains]
sub_refl [in LemmaOverloading.domains]
sub_botP [in LemmaOverloading.domains]
sub_orr [in LemmaOverloading.rels]
sub_orl [in LemmaOverloading.rels]
supdomeqUh [in LemmaOverloading.heaps]
supdomUh [in LemmaOverloading.heaps]
supE [in LemmaOverloading.domains]
suppP [in LemmaOverloading.finmap]
supp_eq_ins [in LemmaOverloading.finmap]
supp_fcat [in LemmaOverloading.finmap]
supp_ins [in LemmaOverloading.finmap]
supp_rem [in LemmaOverloading.finmap]
supp_nilE [in LemmaOverloading.finmap]
supp_nil [in LemmaOverloading.finmap]
sup_dappE [in LemmaOverloading.domains]
sup_appE [in LemmaOverloading.domains]
sup_clos_mono [in LemmaOverloading.domains]
sup_clos_idemp [in LemmaOverloading.domains]
sup_closP [in LemmaOverloading.domains]
sup_clos_min [in LemmaOverloading.domains]
sup_clos_sub [in LemmaOverloading.domains]
sup_mono [in LemmaOverloading.domains]
sup_defdef [in LemmaOverloading.heaps]
svalE [in LemmaOverloading.prelude]
sval_mono [in LemmaOverloading.domains]
swapI [in LemmaOverloading.prelude]
swap_rAC [in LemmaOverloading.prelude]
swap_rCA [in LemmaOverloading.prelude]
swap_prod [in LemmaOverloading.prelude]
swp [in LemmaOverloading.stlog]
sym [in LemmaOverloading.prelude]
T
tarski_gfp_greatest [in LemmaOverloading.domains]tarski_gfp_fixed [in LemmaOverloading.domains]
tarski_lfp_least [in LemmaOverloading.domains]
tarski_lfp_fixed [in LemmaOverloading.domains]
test [in LemmaOverloading.heaps]
throwP [in LemmaOverloading.stsep]
toPredE [in LemmaOverloading.rels]
total [in LemmaOverloading.ordtype]
totalP [in LemmaOverloading.ordtype]
total_ordf [in LemmaOverloading.ordtype]
total_lex [in LemmaOverloading.ordtype]
total_ltn_nat [in LemmaOverloading.ordtype]
trans [in LemmaOverloading.ordtype]
trans_ordf [in LemmaOverloading.ordtype]
trans_lex [in LemmaOverloading.ordtype]
trans_ltn_nat [in LemmaOverloading.ordtype]
tryP [in LemmaOverloading.stsep]
try_gh1 [in LemmaOverloading.stlog]
try_gh [in LemmaOverloading.stlog]
try_throw [in LemmaOverloading.stlog]
try_dealloc [in LemmaOverloading.stlog]
try_allocb [in LemmaOverloading.stlog]
try_alloc [in LemmaOverloading.stlog]
try_write [in LemmaOverloading.stlog]
try_read [in LemmaOverloading.stlog]
try_ret [in LemmaOverloading.stlog]
try_do [in LemmaOverloading.stlog]
try_case_pf [in LemmaOverloading.stlogR]
try_gh1R [in LemmaOverloading.stlogR]
try_ghR [in LemmaOverloading.stlogR]
try_deallocR [in LemmaOverloading.stlogR]
try_writeR [in LemmaOverloading.stlogR]
try_readR [in LemmaOverloading.stlogR]
try_doR [in LemmaOverloading.stlogR]
U
unA [in LemmaOverloading.heaps]unAC [in LemmaOverloading.heaps]
unA2 [in LemmaOverloading.heaps]
unC [in LemmaOverloading.heaps]
unCA [in LemmaOverloading.heaps]
unC2 [in LemmaOverloading.heaps]
undefE [in LemmaOverloading.heaps]
unDl2 [in LemmaOverloading.heaps]
unDr2 [in LemmaOverloading.heaps]
unhKl [in LemmaOverloading.heaps]
unhKr [in LemmaOverloading.heaps]
unh0 [in LemmaOverloading.heaps]
unh02 [in LemmaOverloading.heaps]
union_pf [in LemmaOverloading.cancel]
unKhl [in LemmaOverloading.heaps]
unKhl2 [in LemmaOverloading.heaps]
unKhr [in LemmaOverloading.heaps]
unKhr2 [in LemmaOverloading.heaps]
un_nullP [in LemmaOverloading.heaps]
un0E [in LemmaOverloading.heaps]
un0h [in LemmaOverloading.heaps]
un0h2 [in LemmaOverloading.heaps]
updateE [in LemmaOverloading.stlogR]
updF [in LemmaOverloading.heaps]
updiD [in LemmaOverloading.heaps]
updimV [in LemmaOverloading.heaps]
updiP [in LemmaOverloading.heaps]
updiS [in LemmaOverloading.heaps]
updiVm [in LemmaOverloading.heaps]
updiVm' [in LemmaOverloading.heaps]
updi_iinv [in LemmaOverloading.heaps]
updi_inv [in LemmaOverloading.heaps]
updi_catI [in LemmaOverloading.heaps]
updi_cat [in LemmaOverloading.heaps]
updi_last [in LemmaOverloading.heaps]
updPtUn [in LemmaOverloading.heaps]
updU [in LemmaOverloading.heaps]
updUnl [in LemmaOverloading.heaps]
updUnr [in LemmaOverloading.heaps]
upd_inj [in LemmaOverloading.heaps]
upd_nullP [in LemmaOverloading.heaps]
V
valid_subctx [in LemmaOverloading.terms]valid_cat [in LemmaOverloading.terms]
valid_heaps_cat [in LemmaOverloading.terms]
valid_ptrs_cat [in LemmaOverloading.terms]
valid_cons [in LemmaOverloading.terms]
val_gh1 [in LemmaOverloading.stlog]
val_gh [in LemmaOverloading.stlog]
val_throw [in LemmaOverloading.stlog]
val_dealloc [in LemmaOverloading.stlog]
val_allocb [in LemmaOverloading.stlog]
val_alloc [in LemmaOverloading.stlog]
val_write [in LemmaOverloading.stlog]
val_read [in LemmaOverloading.stlog]
val_ret [in LemmaOverloading.stlog]
val_do [in LemmaOverloading.stlog]
val_doR [in LemmaOverloading.stlogCTC]
val_gh1R [in LemmaOverloading.stlogR]
val_ghR [in LemmaOverloading.stlogR]
val_deallocR [in LemmaOverloading.stlogR]
val_writeR [in LemmaOverloading.stlogR]
val_readR [in LemmaOverloading.stlogR]
val_doR [in LemmaOverloading.stlogR]
vars_hfree [in LemmaOverloading.terms]
var_pf [in LemmaOverloading.cancel]
var_has [in LemmaOverloading.terms]
W
writeP [in LemmaOverloading.stsep]Constructor Index
A
AbsHeap [in LemmaOverloading.cancel2]AbsPts [in LemmaOverloading.cancel2]
And6 [in LemmaOverloading.prelude]
Ast [in LemmaOverloading.cancel]
B
BndForm [in LemmaOverloading.stlogR]C
Chain [in LemmaOverloading.domains]Check [in LemmaOverloading.noalias]
Check [in LemmaOverloading.auto]
Check' [in LemmaOverloading.noalias]
Context [in LemmaOverloading.terms]
CPO.Class [in LemmaOverloading.domains]
CPO.Mixin [in LemmaOverloading.domains]
CPO.Pack [in LemmaOverloading.domains]
D
Def [in LemmaOverloading.heaps]def_true [in LemmaOverloading.heaps]
def_false3 [in LemmaOverloading.heaps]
def_false2 [in LemmaOverloading.heaps]
def_false1 [in LemmaOverloading.heaps]
disj_false [in LemmaOverloading.finmap]
disj_true [in LemmaOverloading.finmap]
Dyn.dyn [in LemmaOverloading.prelude]
E
eqD [in LemmaOverloading.terms]eqH [in LemmaOverloading.terms]
Equate [in LemmaOverloading.auto]
eqX [in LemmaOverloading.terms]
Exn [in LemmaOverloading.stmod]
exn_from_nat [in LemmaOverloading.stmod]
F
Find [in LemmaOverloading.auto]FinMap [in LemmaOverloading.finmap]
Form [in LemmaOverloading.indom]
Form [in LemmaOverloading.auto]
Form [in LemmaOverloading.cancelD]
H
has_false [in LemmaOverloading.prelude]has_true [in LemmaOverloading.prelude]
HeapEq [in LemmaOverloading.cancel2]
I
Ideal [in LemmaOverloading.domains]L
Lattice.Class [in LemmaOverloading.domains]Lattice.Mixin [in LemmaOverloading.domains]
Lattice.Pack [in LemmaOverloading.domains]
M
MemProp [in LemmaOverloading.rels]N
NoAlias.Form [in LemmaOverloading.noalias]NoAlias.Tag [in LemmaOverloading.noalias]
NoAlias2.Form [in LemmaOverloading.noaliasBT]
NoAlias2.Tag [in LemmaOverloading.noaliasBT]
NoAlias3.Form [in LemmaOverloading.noaliasBT]
O
Ordered.Class [in LemmaOverloading.ordtype]Ordered.Mixin [in LemmaOverloading.ordtype]
Ordered.Pack [in LemmaOverloading.ordtype]
Or51 [in LemmaOverloading.prelude]
Or52 [in LemmaOverloading.prelude]
Or53 [in LemmaOverloading.prelude]
Or54 [in LemmaOverloading.prelude]
Or55 [in LemmaOverloading.prelude]
Or61 [in LemmaOverloading.prelude]
Or62 [in LemmaOverloading.prelude]
Or63 [in LemmaOverloading.prelude]
Or64 [in LemmaOverloading.prelude]
Or65 [in LemmaOverloading.prelude]
Or66 [in LemmaOverloading.prelude]
P
Pack [in LemmaOverloading.cancel2]PackHeap [in LemmaOverloading.cancel2]
permutation_trans [in LemmaOverloading.perms]
permutation_swap [in LemmaOverloading.perms]
permutation_skip [in LemmaOverloading.perms]
permutation_nil [in LemmaOverloading.perms]
Poset.Class [in LemmaOverloading.domains]
Poset.Mixin [in LemmaOverloading.domains]
Poset.Pack [in LemmaOverloading.domains]
PropPredType [in LemmaOverloading.rels]
ptr_nat [in LemmaOverloading.heaps]
Pts [in LemmaOverloading.terms]
S
Scan.Form [in LemmaOverloading.noalias]Scan.Tag [in LemmaOverloading.noalias]
Search.Form [in LemmaOverloading.noalias]
Search.Tag [in LemmaOverloading.noalias]
Search2.Form [in LemmaOverloading.noalias]
Search2.Tag [in LemmaOverloading.noalias]
STprog [in LemmaOverloading.stmod]
supp_spec_none [in LemmaOverloading.finmap]
supp_spec_some [in LemmaOverloading.finmap]
T
Tag [in LemmaOverloading.cancel]Tag [in LemmaOverloading.indom]
Tag [in LemmaOverloading.auto]
Tag [in LemmaOverloading.cancelD]
Tag [in LemmaOverloading.stlogR]
TagS [in LemmaOverloading.auto]
total_spec_gt [in LemmaOverloading.ordtype]
total_spec_eq [in LemmaOverloading.ordtype]
total_spec_lt [in LemmaOverloading.ordtype]
TryForm [in LemmaOverloading.stlogR]
U
Undef [in LemmaOverloading.heaps]Update [in LemmaOverloading.stlogR]
V
Val [in LemmaOverloading.stmod]ValForm [in LemmaOverloading.stlogR]
Var [in LemmaOverloading.terms]
X
XFind [in LemmaOverloading.xfind]XTag [in LemmaOverloading.xfind]
Axiom Index
F
fext [in LemmaOverloading.prelude]P
pext [in LemmaOverloading.prelude]Projection Index
A
assign [in LemmaOverloading.auto]ast [in LemmaOverloading.cancelCTC]
B
bnd_pivot [in LemmaOverloading.stlogR]C
CPO.base [in LemmaOverloading.domains]CPO.mixin [in LemmaOverloading.domains]
CPO.mx_lim [in LemmaOverloading.domains]
CPO.sort [in LemmaOverloading.domains]
D
dummy [in LemmaOverloading.cancel2]Dyn.typ [in LemmaOverloading.prelude]
Dyn.val [in LemmaOverloading.prelude]
E
elem_of [in LemmaOverloading.xfind]H
heap_of [in LemmaOverloading.cancel]heap_ctx [in LemmaOverloading.terms]
heap_of [in LemmaOverloading.indom]
heap_h [in LemmaOverloading.cancel2]
heap_of [in LemmaOverloading.stlogR]
heq1 [in LemmaOverloading.stlogCTC]
I
id_pf [in LemmaOverloading.domains]id_val [in LemmaOverloading.domains]
index_of [in LemmaOverloading.xfindCTC]
indom [in LemmaOverloading.indomCTC]
L
Lattice.base [in LemmaOverloading.domains]Lattice.mixin [in LemmaOverloading.domains]
Lattice.mx_sup [in LemmaOverloading.domains]
Lattice.sort [in LemmaOverloading.domains]
M
model [in LemmaOverloading.stmod]N
NoAlias.untag [in LemmaOverloading.noalias]NoAlias.y_of [in LemmaOverloading.noalias]
NoAlias2.eq_of [in LemmaOverloading.noaliasBT]
NoAlias2.untag [in LemmaOverloading.noaliasBT]
NoAlias3.y_of [in LemmaOverloading.noaliasBT]
O
Ordered.base [in LemmaOverloading.ordtype]Ordered.mixin [in LemmaOverloading.ordtype]
Ordered.ordering [in LemmaOverloading.ordtype]
Ordered.sort [in LemmaOverloading.ordtype]
P
pack_h [in LemmaOverloading.cancel2]Poset.mixin [in LemmaOverloading.domains]
Poset.mx_bot [in LemmaOverloading.domains]
Poset.mx_leq [in LemmaOverloading.domains]
Poset.sort [in LemmaOverloading.domains]
pred_of [in LemmaOverloading.domains]
Pred_Sort [in LemmaOverloading.rels]
proof [in LemmaOverloading.cancel2]
prop [in LemmaOverloading.cancel2]
prop_of [in LemmaOverloading.auto]
prop_of [in LemmaOverloading.cancelD]
ptr_ctx [in LemmaOverloading.terms]
pts_h [in LemmaOverloading.cancel2]
puntag [in LemmaOverloading.cancelD]
R
rest [in LemmaOverloading.stlogCTC]rest1 [in LemmaOverloading.stlogCTC]
S
scan [in LemmaOverloading.noaliasCTC]Scan.heap_of [in LemmaOverloading.noalias]
Scan.untag [in LemmaOverloading.noalias]
search [in LemmaOverloading.noaliasCTC]
Search.seq_of [in LemmaOverloading.noalias]
Search.untag [in LemmaOverloading.noalias]
search2 [in LemmaOverloading.noaliasCTC]
Search2.seq_of [in LemmaOverloading.noalias]
Search2.untag [in LemmaOverloading.noalias]
seq_of [in LemmaOverloading.noaliasCTC]
seq_of [in LemmaOverloading.xfindCTC]
seq_of [in LemmaOverloading.finmap]
seq_of [in LemmaOverloading.auto]
T
toPred [in LemmaOverloading.rels]try_pivot [in LemmaOverloading.stlogR]
U
unpack [in LemmaOverloading.cancel2]untag [in LemmaOverloading.cancel]
untag [in LemmaOverloading.indom]
untag [in LemmaOverloading.auto]
untag [in LemmaOverloading.stlogR]
untags [in LemmaOverloading.auto]
update1 [in LemmaOverloading.stlogCTC]
update2 [in LemmaOverloading.stlogCTC]
V
val_pivot [in LemmaOverloading.stlogR]X
xfind [in LemmaOverloading.xfindCTC]xuntag [in LemmaOverloading.xfind]
x_of [in LemmaOverloading.auto]
Y
y_of' [in LemmaOverloading.noalias]y_of [in LemmaOverloading.noalias]
Inductive Index
A
and6 [in LemmaOverloading.prelude]ans [in LemmaOverloading.stmod]
D
defUn_spec [in LemmaOverloading.heaps]disj_spec [in LemmaOverloading.finmap]
E
elem [in LemmaOverloading.terms]exn [in LemmaOverloading.stmod]
F
fact [in LemmaOverloading.terms]H
has_spec [in LemmaOverloading.prelude]heap [in LemmaOverloading.heaps]
M
Mem_Pred [in LemmaOverloading.rels]O
or5 [in LemmaOverloading.prelude]or6 [in LemmaOverloading.prelude]
P
perm [in LemmaOverloading.perms]ptr [in LemmaOverloading.heaps]
S
supp_spec [in LemmaOverloading.finmap]T
total_spec [in LemmaOverloading.ordtype]Section Index
A
AdmissibleClosure [in LemmaOverloading.domains]AppChain [in LemmaOverloading.domains]
Append [in LemmaOverloading.finmap]
B
BasePrograms [in LemmaOverloading.stmod]BasicProperties [in LemmaOverloading.domains]
BasicProperties [in LemmaOverloading.hprop]
BlockUpdate [in LemmaOverloading.heaps]
C
ChainCompose [in LemmaOverloading.domains]ChainConst [in LemmaOverloading.domains]
ChainId [in LemmaOverloading.domains]
Chains [in LemmaOverloading.domains]
Coercions [in LemmaOverloading.prelude]
Coercions2 [in LemmaOverloading.prelude]
CondBool [in LemmaOverloading.stsep]
CondDecide [in LemmaOverloading.stsep]
CondNat [in LemmaOverloading.stsep]
CondOption [in LemmaOverloading.stsep]
CondSeq [in LemmaOverloading.stsep]
Continuity [in LemmaOverloading.domains]
CPO.ClassDef [in LemmaOverloading.domains]
CPO.Exports.Laws [in LemmaOverloading.domains]
CPO.RawMixin [in LemmaOverloading.domains]
D
DAppChain [in LemmaOverloading.domains]Def [in LemmaOverloading.finmap]
DFunCPO [in LemmaOverloading.domains]
DFunLattice [in LemmaOverloading.domains]
DFunPoset [in LemmaOverloading.domains]
DiagChain [in LemmaOverloading.domains]
DisjointUnion [in LemmaOverloading.finmap]
E
EqType [in LemmaOverloading.finmap]EvalAlloc [in LemmaOverloading.stlog]
EvalBlockAlloc [in LemmaOverloading.stlog]
EvalDealloc [in LemmaOverloading.stlog]
EvalDeallocR [in LemmaOverloading.stlogCTC]
EvalDeallocR [in LemmaOverloading.stlogR]
EvalDo [in LemmaOverloading.stlog]
EvalDoR [in LemmaOverloading.stlogCTC]
EvalDoR [in LemmaOverloading.stlogR]
EvalGhost [in LemmaOverloading.stlog]
EvalGhostR [in LemmaOverloading.stlogR]
EvalRead [in LemmaOverloading.stlog]
EvalReadR [in LemmaOverloading.stlogR]
EvalReturn [in LemmaOverloading.stlog]
EvalThrow [in LemmaOverloading.stlog]
EvalWrite [in LemmaOverloading.stlog]
EvalWriteR [in LemmaOverloading.stlogCTC]
EvalWriteR [in LemmaOverloading.stlogR]
F
FinTypeOrd [in LemmaOverloading.ordtype]FMapInd [in LemmaOverloading.finmap]
FunCPO [in LemmaOverloading.domains]
FunLattice [in LemmaOverloading.domains]
FunPoset [in LemmaOverloading.domains]
G
Ghosts [in LemmaOverloading.stsep]H
HasSelect [in LemmaOverloading.prelude]HeapReflection [in LemmaOverloading.cancel]
I
IdealDef [in LemmaOverloading.domains]IdealLattice [in LemmaOverloading.domains]
IdealPoset [in LemmaOverloading.domains]
ImageChain [in LemmaOverloading.domains]
Infimum [in LemmaOverloading.domains]
K
Kleene [in LemmaOverloading.domains]L
Lat [in LemmaOverloading.domains]LatticeCPO [in LemmaOverloading.domains]
Lattice.ClassDef [in LemmaOverloading.domains]
Lattice.Exports.Laws [in LemmaOverloading.domains]
Lattice.RawMixin [in LemmaOverloading.domains]
Laws [in LemmaOverloading.finmap]
Lemmas [in LemmaOverloading.ordtype]
LiftChain [in LemmaOverloading.domains]
ListMembership [in LemmaOverloading.rels]
LList [in LemmaOverloading.llistR]
M
Model.Allocation [in LemmaOverloading.stmod]Model.Bind [in LemmaOverloading.stmod]
Model.BlockAllocation [in LemmaOverloading.stmod]
Model.Consequence [in LemmaOverloading.stmod]
Model.Deallocation [in LemmaOverloading.stmod]
Model.Fix [in LemmaOverloading.stmod]
Model.Read [in LemmaOverloading.stmod]
Model.Return [in LemmaOverloading.stmod]
Model.Throw [in LemmaOverloading.stmod]
Model.Try [in LemmaOverloading.stmod]
Model.Write [in LemmaOverloading.stmod]
N
NatChain [in LemmaOverloading.domains]NatOrd [in LemmaOverloading.ordtype]
NatPoset [in LemmaOverloading.domains]
NoAlias.NoAliasSection [in LemmaOverloading.noalias]
NoAlias2.NoAlias2Section [in LemmaOverloading.noaliasBT]
NoAlias3.NoAlias3Section [in LemmaOverloading.noaliasBT]
NullLemmas [in LemmaOverloading.heaps]
O
Ops [in LemmaOverloading.finmap]Ordered.ClassDef [in LemmaOverloading.ordtype]
Ordered.RawMixin [in LemmaOverloading.ordtype]
P
PairCPO [in LemmaOverloading.domains]PairLattice [in LemmaOverloading.domains]
PairPoset [in LemmaOverloading.domains]
Permutations [in LemmaOverloading.perms]
Poset.ClassDef [in LemmaOverloading.domains]
Poset.Exports.Laws [in LemmaOverloading.domains]
Poset.RawMixin [in LemmaOverloading.domains]
PredCPO [in LemmaOverloading.domains]
Predicates [in LemmaOverloading.rels]
PredLattice [in LemmaOverloading.domains]
PredPoset [in LemmaOverloading.domains]
Prefix [in LemmaOverloading.prefix]
ProdChain [in LemmaOverloading.domains]
ProdOrd [in LemmaOverloading.ordtype]
ProjChain [in LemmaOverloading.domains]
PropCPO [in LemmaOverloading.domains]
PropLattice [in LemmaOverloading.domains]
PropPoset [in LemmaOverloading.domains]
R
ReflectConnectives [in LemmaOverloading.prelude]RelLaws [in LemmaOverloading.rels]
RelProperties [in LemmaOverloading.rels]
Reorder [in LemmaOverloading.prelude]
S
Scan.ScanSection [in LemmaOverloading.noalias]Search.SearchSection [in LemmaOverloading.noalias]
Search2.Search2Section [in LemmaOverloading.noalias]
SepAlloc [in LemmaOverloading.stsep]
SepBind [in LemmaOverloading.stsep]
SepBlockAlloc [in LemmaOverloading.stsep]
SepConseq [in LemmaOverloading.stsep]
SepDealloc [in LemmaOverloading.stsep]
SepFix [in LemmaOverloading.stsep]
SepFrame [in LemmaOverloading.stsep]
SepRead [in LemmaOverloading.stsep]
SepReturn [in LemmaOverloading.stsep]
SepThrow [in LemmaOverloading.stsep]
SepTry [in LemmaOverloading.stsep]
SepWrite [in LemmaOverloading.stsep]
Simplifications [in LemmaOverloading.rels]
STDef [in LemmaOverloading.stmod]
SubCPO [in LemmaOverloading.domains]
SubLattice [in LemmaOverloading.domains]
SubMemLaws [in LemmaOverloading.rels]
SubPoset [in LemmaOverloading.domains]
T
Totality [in LemmaOverloading.ordtype]X
XFind [in LemmaOverloading.xfind]Instance Index
E
empty_struct [in LemmaOverloading.cancelCTC]extend_struct [in LemmaOverloading.xfindCTC]
F
ffound_struct1 [in LemmaOverloading.stlogCTC]fleft_struct1 [in LemmaOverloading.stlogCTC]
found [in LemmaOverloading.indomCTC]
found_struct [in LemmaOverloading.xfindCTC]
found_right [in LemmaOverloading.indomCTC]
found_left [in LemmaOverloading.indomCTC]
found_struct [in LemmaOverloading.stlogCTC]
fright_struct1 [in LemmaOverloading.stlogCTC]
L
left_struct [in LemmaOverloading.stlogCTC]P
pts_struct [in LemmaOverloading.cancelCTC]R
recurse_struct [in LemmaOverloading.xfindCTC]right_struct [in LemmaOverloading.stlogCTC]
S
scan_default [in LemmaOverloading.noaliasCTC]scan_ptr [in LemmaOverloading.noaliasCTC]
scan_union [in LemmaOverloading.noaliasCTC]
search_recurse [in LemmaOverloading.noaliasCTC]
search_found [in LemmaOverloading.noaliasCTC]
search2_foundz [in LemmaOverloading.noaliasCTC]
search2_foundy [in LemmaOverloading.noaliasCTC]
search2_foundx [in LemmaOverloading.noaliasCTC]
U
union_struct [in LemmaOverloading.cancelCTC]V
var_struct [in LemmaOverloading.cancelCTC]Abbreviation Index
C
cancelD [in LemmaOverloading.cancelD]conseq1 [in LemmaOverloading.stsep]
cont [in LemmaOverloading.stlog]
cont [in LemmaOverloading.stlogCTC]
cont [in LemmaOverloading.stlogR]
CPO.Exports.CPO [in LemmaOverloading.domains]
CPO.Exports.cpo [in LemmaOverloading.domains]
CPO.Exports.CPOMixin [in LemmaOverloading.domains]
CPO.Exports.lim [in LemmaOverloading.domains]
D
dyn [in LemmaOverloading.prelude]dynamic [in LemmaOverloading.prelude]
F
fmap [in LemmaOverloading.finmap]fmap [in LemmaOverloading.finmap]
fmap [in LemmaOverloading.finmap]
fmap [in LemmaOverloading.finmap]
fmap [in LemmaOverloading.finmap]
I
ideald [in LemmaOverloading.stmod]K
key [in LemmaOverloading.finmap]L
Lattice.Exports.Lattice [in LemmaOverloading.domains]Lattice.Exports.lattice [in LemmaOverloading.domains]
Lattice.Exports.LatticeMixin [in LemmaOverloading.domains]
Lattice.Exports.sup [in LemmaOverloading.domains]
llist [in LemmaOverloading.llistR]
M
Model.lat [in LemmaOverloading.stmod]Model.tp [in LemmaOverloading.stmod]
N
nil [in LemmaOverloading.finmap]nil [in LemmaOverloading.finmap]
nil [in LemmaOverloading.finmap]
nil [in LemmaOverloading.finmap]
noaliasR_fwd' [in LemmaOverloading.noalias]
noaliasR_fwd [in LemmaOverloading.noalias]
O
Ordered.Exports.OrdMixin [in LemmaOverloading.ordtype]Ordered.Exports.OrdType [in LemmaOverloading.ordtype]
Ordered.Exports.ordType [in LemmaOverloading.ordtype]
P
plook' [in LemmaOverloading.terms]Poset.Exports.bot [in LemmaOverloading.domains]
Poset.Exports.Poset [in LemmaOverloading.domains]
Poset.Exports.poset [in LemmaOverloading.domains]
Poset.Exports.PosetMixin [in LemmaOverloading.domains]
post [in LemmaOverloading.stmod]
pre [in LemmaOverloading.stmod]
pread' [in LemmaOverloading.terms]
predCk [in LemmaOverloading.finmap]
predk [in LemmaOverloading.finmap]
Pred_Class [in LemmaOverloading.rels]
T
tp [in LemmaOverloading.domains]tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.domains]
tp [in LemmaOverloading.stsep]
V
verify [in LemmaOverloading.stsep]X
xPredC [in LemmaOverloading.rels]xPredD [in LemmaOverloading.rels]
xPredI [in LemmaOverloading.rels]
xPredT [in LemmaOverloading.rels]
xPredU [in LemmaOverloading.rels]
xPred0 [in LemmaOverloading.rels]
xPred1 [in LemmaOverloading.rels]
xPreim [in LemmaOverloading.rels]
Definition Index
A
alloc [in LemmaOverloading.stsep]allocb [in LemmaOverloading.stsep]
allocb_s [in LemmaOverloading.stsep]
alloc_s [in LemmaOverloading.stsep]
all_tag [in LemmaOverloading.auto]
app_chain [in LemmaOverloading.domains]
B
bind [in LemmaOverloading.stsep]bind_s [in LemmaOverloading.stsep]
bnd_throwR [in LemmaOverloading.stlogR]
bnd_allocbR [in LemmaOverloading.stlogR]
bnd_allocR [in LemmaOverloading.stlogR]
bnd_retR [in LemmaOverloading.stlogR]
C
cancel [in LemmaOverloading.terms]cancel' [in LemmaOverloading.terms]
chain_closure [in LemmaOverloading.domains]
chain_closed [in LemmaOverloading.domains]
chain_axiom [in LemmaOverloading.domains]
coerce [in LemmaOverloading.prelude]
coerce2 [in LemmaOverloading.prelude]
coherent [in LemmaOverloading.stmod]
conseq [in LemmaOverloading.stsep]
const_chain [in LemmaOverloading.domains]
continuous [in LemmaOverloading.domains]
CPO.class [in LemmaOverloading.domains]
CPO.clone [in LemmaOverloading.domains]
CPO.lim [in LemmaOverloading.domains]
CPO.pack [in LemmaOverloading.domains]
CPO.poset [in LemmaOverloading.domains]
D
dapp_chain [in LemmaOverloading.domains]dealloc [in LemmaOverloading.stsep]
dealloc_s [in LemmaOverloading.stsep]
def [in LemmaOverloading.heaps]
default_tag [in LemmaOverloading.cancelD]
defed [in LemmaOverloading.stmod]
def_strict [in LemmaOverloading.stmod]
def2 [in LemmaOverloading.heaps]
dfunCPO [in LemmaOverloading.domains]
dfunCPOMixin [in LemmaOverloading.domains]
dfunLattice [in LemmaOverloading.domains]
dfunLatticeMixin [in LemmaOverloading.domains]
dfunPoset [in LemmaOverloading.domains]
dfunPosetMixin [in LemmaOverloading.domains]
dfun_lim [in LemmaOverloading.domains]
dfun_sup [in LemmaOverloading.domains]
dfun_leq [in LemmaOverloading.domains]
dfun_bot [in LemmaOverloading.domains]
diag_chain [in LemmaOverloading.domains]
disj [in LemmaOverloading.finmap]
dom [in LemmaOverloading.heaps]
do' [in LemmaOverloading.stsep]
dyneq_tag [in LemmaOverloading.cancelD]
E
einterp [in LemmaOverloading.terms]emp [in LemmaOverloading.hprop]
empb [in LemmaOverloading.heaps]
empc [in LemmaOverloading.terms]
empty [in LemmaOverloading.heaps]
empty_tag [in LemmaOverloading.cancel]
eqexn [in LemmaOverloading.stmod]
EqMem [in LemmaOverloading.rels]
EqPred [in LemmaOverloading.rels]
EqPredFun [in LemmaOverloading.rels]
EqPredType [in LemmaOverloading.rels]
EqPredType_trans [in LemmaOverloading.rels]
EqSeq_Class [in LemmaOverloading.rels]
EqSimplPred [in LemmaOverloading.rels]
eq_ptr [in LemmaOverloading.heaps]
eval [in LemmaOverloading.terms]
eval_fact [in LemmaOverloading.terms]
exnc [in LemmaOverloading.noaliasCTC]
exnc [in LemmaOverloading.noalias]
exnc [in LemmaOverloading.noalias]
exnc [in LemmaOverloading.noalias]
exnc [in LemmaOverloading.noaliasBT]
exnc [in LemmaOverloading.noaliasBT]
exn_to_nat [in LemmaOverloading.stmod]
extend_tag [in LemmaOverloading.xfind]
ex_noalias2 [in LemmaOverloading.noaliasCTC]
ex_noalias [in LemmaOverloading.noaliasCTC]
ex_find2 [in LemmaOverloading.noaliasCTC]
ex_find [in LemmaOverloading.noaliasCTC]
ex_scan [in LemmaOverloading.noaliasCTC]
ex_find2 [in LemmaOverloading.noalias]
ex_find [in LemmaOverloading.noalias]
ex_scan [in LemmaOverloading.noalias]
ex_dealloc_bwd [in LemmaOverloading.stlogCTC]
ex_fwd [in LemmaOverloading.stlogCTC]
ex_bwd [in LemmaOverloading.stlogCTC]
ex_val_do [in LemmaOverloading.stlogCTC]
ex_fwd [in LemmaOverloading.stlogR]
ex_bwd [in LemmaOverloading.stlogR]
ex_val_do [in LemmaOverloading.stlogR]
ex_read [in LemmaOverloading.stlogR]
ex0 [in LemmaOverloading.cancel]
ex1 [in LemmaOverloading.cancel]
ex1 [in LemmaOverloading.xfindCTC]
ex1 [in LemmaOverloading.indom]
ex1 [in LemmaOverloading.auto]
ex1 [in LemmaOverloading.cancelCTC]
ex1 [in LemmaOverloading.indomCTC]
ex1' [in LemmaOverloading.cancel]
ex2 [in LemmaOverloading.cancel]
ex2 [in LemmaOverloading.indom]
ex2 [in LemmaOverloading.auto]
ex2 [in LemmaOverloading.cancelCTC]
ex2 [in LemmaOverloading.indomCTC]
ex3 [in LemmaOverloading.auto]
ex3 [in LemmaOverloading.cancel2]
ex3 [in LemmaOverloading.cancelD]
ex4 [in LemmaOverloading.auto]
ex5 [in LemmaOverloading.auto]
ex6 [in LemmaOverloading.auto]
ex7 [in LemmaOverloading.auto]
ex8 [in LemmaOverloading.auto]
ex9 [in LemmaOverloading.auto]
F
fcat [in LemmaOverloading.finmap]fcat' [in LemmaOverloading.finmap]
feq [in LemmaOverloading.finmap]
finMap_for [in LemmaOverloading.finmap]
fin_ordMixin [in LemmaOverloading.ordtype]
Fix [in LemmaOverloading.stsep]
fnd [in LemmaOverloading.finmap]
fprod [in LemmaOverloading.prelude]
fr [in LemmaOverloading.stsep]
free [in LemmaOverloading.heaps]
fresh [in LemmaOverloading.heaps]
funCPOMixin [in LemmaOverloading.domains]
funLatticeMixin [in LemmaOverloading.domains]
funPosetMixin [in LemmaOverloading.domains]
fun_lim [in LemmaOverloading.domains]
fun_sup [in LemmaOverloading.domains]
fun_leq [in LemmaOverloading.domains]
fun_bot [in LemmaOverloading.domains]
G
get_highs [in LemmaOverloading.heaps]get_lows [in LemmaOverloading.heaps]
gh [in LemmaOverloading.stsep]
H
has_spec [in LemmaOverloading.stmod]hdom [in LemmaOverloading.heaps]
heap_inv [in LemmaOverloading.cancel2]
hfree [in LemmaOverloading.terms]
hfresh [in LemmaOverloading.heaps]
high [in LemmaOverloading.heaps]
hlook [in LemmaOverloading.terms]
hstep [in LemmaOverloading.stlogR]
hstep_bnd [in LemmaOverloading.stlogR]
I
iA [in LemmaOverloading.prelude]idealLatticeMixin [in LemmaOverloading.domains]
idealPosetMixin [in LemmaOverloading.domains]
ideal_sup [in LemmaOverloading.domains]
ideal_sup' [in LemmaOverloading.domains]
ideal_leq [in LemmaOverloading.domains]
ideal_bot [in LemmaOverloading.domains]
If [in LemmaOverloading.stsep]
image_chain [in LemmaOverloading.domains]
imp_tag [in LemmaOverloading.auto]
InE [in LemmaOverloading.rels]
inf [in LemmaOverloading.domains]
inj_pair2 [in LemmaOverloading.prelude]
InMem [in LemmaOverloading.rels]
ins [in LemmaOverloading.finmap]
insert [in LemmaOverloading.llistR]
ins' [in LemmaOverloading.finmap]
interp [in LemmaOverloading.terms]
invariant [in LemmaOverloading.xfind]
invariant [in LemmaOverloading.cancel]
invariant [in LemmaOverloading.xfindCTC]
invariant [in LemmaOverloading.indom]
invariant [in LemmaOverloading.cancelCTC]
isMem [in LemmaOverloading.rels]
J
jmeq [in LemmaOverloading.prelude]jmeq2 [in LemmaOverloading.prelude]
K
key [in LemmaOverloading.finmap]kleene_lfp [in LemmaOverloading.domains]
L
latCPO [in LemmaOverloading.domains]latCPOMixin [in LemmaOverloading.domains]
Lattice.class [in LemmaOverloading.domains]
Lattice.clone [in LemmaOverloading.domains]
Lattice.pack [in LemmaOverloading.domains]
Lattice.poset [in LemmaOverloading.domains]
Lattice.sup [in LemmaOverloading.domains]
lat_lim [in LemmaOverloading.domains]
ldom [in LemmaOverloading.heaps]
left_tag [in LemmaOverloading.indom]
left_tag [in LemmaOverloading.stlogR]
lex [in LemmaOverloading.ordtype]
lfresh [in LemmaOverloading.heaps]
lift_chain [in LemmaOverloading.domains]
llist [in LemmaOverloading.llistR]
lolli [in LemmaOverloading.stsep]
look [in LemmaOverloading.heaps]
low [in LemmaOverloading.heaps]
loweq [in LemmaOverloading.heaps]
lseg [in LemmaOverloading.llistR]
lseq [in LemmaOverloading.llistR]
ltn_ptr [in LemmaOverloading.heaps]
M
Match_seq [in LemmaOverloading.stsep]Match_nat [in LemmaOverloading.stsep]
Match_dec [in LemmaOverloading.stsep]
Match_opt [in LemmaOverloading.stsep]
Mem [in LemmaOverloading.rels]
MemE [in LemmaOverloading.rels]
Mem_Seq [in LemmaOverloading.rels]
mkPredType [in LemmaOverloading.rels]
Model.alloc [in LemmaOverloading.stmod]
Model.allocb [in LemmaOverloading.stmod]
Model.allocb_sp [in LemmaOverloading.stmod]
Model.allocb_s [in LemmaOverloading.stmod]
Model.alloc_sp [in LemmaOverloading.stmod]
Model.alloc_s [in LemmaOverloading.stmod]
Model.bind [in LemmaOverloading.stmod]
Model.bind_sp [in LemmaOverloading.stmod]
Model.bind_s [in LemmaOverloading.stmod]
Model.bind_post [in LemmaOverloading.stmod]
Model.bind_pre [in LemmaOverloading.stmod]
Model.conseq [in LemmaOverloading.stmod]
Model.dealloc [in LemmaOverloading.stmod]
Model.dealloc_sp [in LemmaOverloading.stmod]
Model.dealloc_s [in LemmaOverloading.stmod]
Model.Do [in LemmaOverloading.stmod]
Model.do_sp [in LemmaOverloading.stmod]
Model.ffix [in LemmaOverloading.stmod]
Model.f' [in LemmaOverloading.stmod]
Model.read [in LemmaOverloading.stmod]
Model.read_sp [in LemmaOverloading.stmod]
Model.read_s [in LemmaOverloading.stmod]
Model.ret [in LemmaOverloading.stmod]
Model.ret_sp [in LemmaOverloading.stmod]
Model.ret_s [in LemmaOverloading.stmod]
Model.throw [in LemmaOverloading.stmod]
Model.throw_sp [in LemmaOverloading.stmod]
Model.throw_s [in LemmaOverloading.stmod]
Model.try [in LemmaOverloading.stmod]
Model.try_sp [in LemmaOverloading.stmod]
Model.try_s [in LemmaOverloading.stmod]
Model.try_post [in LemmaOverloading.stmod]
Model.try_pre [in LemmaOverloading.stmod]
Model.write [in LemmaOverloading.stmod]
Model.write_sp [in LemmaOverloading.stmod]
Model.write_s [in LemmaOverloading.stmod]
monotone [in LemmaOverloading.domains]
N
natPosetMixin [in LemmaOverloading.domains]nat_chain [in LemmaOverloading.domains]
nat_ordMixin [in LemmaOverloading.ordtype]
nat_ptr [in LemmaOverloading.heaps]
nil [in LemmaOverloading.finmap]
NoAlias.singleton [in LemmaOverloading.noalias]
null [in LemmaOverloading.heaps]
O
onth [in LemmaOverloading.prefix]Ordered.class [in LemmaOverloading.ordtype]
Ordered.clone [in LemmaOverloading.ordtype]
Ordered.eqType [in LemmaOverloading.ordtype]
Ordered.Exports.ord [in LemmaOverloading.ordtype]
Ordered.pack [in LemmaOverloading.ordtype]
ordf [in LemmaOverloading.ordtype]
ordinal_ordMixin [in LemmaOverloading.ordtype]
orL_tag [in LemmaOverloading.auto]
orR_tag [in LemmaOverloading.auto]
P
pack_right [in LemmaOverloading.cancel2]pack_found [in LemmaOverloading.cancel2]
pack01 [in LemmaOverloading.cancel2]
pack02 [in LemmaOverloading.cancel2]
pack03 [in LemmaOverloading.cancel2]
pack04 [in LemmaOverloading.cancel2]
pack05 [in LemmaOverloading.cancel2]
pack06 [in LemmaOverloading.cancel2]
pack07 [in LemmaOverloading.cancel2]
pack08 [in LemmaOverloading.cancel2]
pack09 [in LemmaOverloading.cancel2]
pack10 [in LemmaOverloading.cancel2]
pairCPOMixin [in LemmaOverloading.domains]
pairLatticeMixin [in LemmaOverloading.domains]
pairPosetMixin [in LemmaOverloading.domains]
pair_lim [in LemmaOverloading.domains]
pair_sup [in LemmaOverloading.domains]
pair_leq [in LemmaOverloading.domains]
pair_bot [in LemmaOverloading.domains]
pfree [in LemmaOverloading.terms]
pick [in LemmaOverloading.heaps]
pL [in LemmaOverloading.prelude]
plook [in LemmaOverloading.terms]
plus2 [in LemmaOverloading.heaps]
Poset.bot [in LemmaOverloading.domains]
Poset.class [in LemmaOverloading.domains]
Poset.clone [in LemmaOverloading.domains]
Poset.leq [in LemmaOverloading.domains]
Poset.pack [in LemmaOverloading.domains]
pow [in LemmaOverloading.domains]
pow_chain [in LemmaOverloading.domains]
ppts [in LemmaOverloading.hprop]
pR [in LemmaOverloading.prelude]
pread [in LemmaOverloading.terms]
Pred [in LemmaOverloading.rels]
PredArgType [in LemmaOverloading.rels]
PredC [in LemmaOverloading.rels]
predCk [in LemmaOverloading.finmap]
predCPOMixin [in LemmaOverloading.domains]
PredD [in LemmaOverloading.rels]
PredI [in LemmaOverloading.rels]
predk [in LemmaOverloading.finmap]
predLatticeMixin [in LemmaOverloading.domains]
predPosetMixin [in LemmaOverloading.domains]
PredT [in LemmaOverloading.rels]
PredU [in LemmaOverloading.rels]
Pred0 [in LemmaOverloading.rels]
Pred1 [in LemmaOverloading.rels]
prefix [in LemmaOverloading.prefix]
Preim [in LemmaOverloading.rels]
prod_chain [in LemmaOverloading.domains]
prod_ordMixin [in LemmaOverloading.ordtype]
prog [in LemmaOverloading.stmod]
proj1_chain [in LemmaOverloading.domains]
proj2_chain [in LemmaOverloading.domains]
propCPOMixin [in LemmaOverloading.domains]
propLatticeMixin [in LemmaOverloading.domains]
propPosetMixin [in LemmaOverloading.domains]
prop_lim [in LemmaOverloading.domains]
prop_sup [in LemmaOverloading.domains]
prop_leq [in LemmaOverloading.domains]
prop_bot [in LemmaOverloading.domains]
ptreq [in LemmaOverloading.terms]
ptrs [in LemmaOverloading.terms]
ptr_ordMixin [in LemmaOverloading.heaps]
ptr_offset [in LemmaOverloading.heaps]
ptr_eqMixin [in LemmaOverloading.heaps]
pts [in LemmaOverloading.heaps]
pts_tag [in LemmaOverloading.cancel]
pts_inv [in LemmaOverloading.cancel2]
pull [in LemmaOverloading.stlog]
push [in LemmaOverloading.stlog]
R
rA [in LemmaOverloading.prelude]rAC [in LemmaOverloading.prelude]
rCA [in LemmaOverloading.prelude]
read [in LemmaOverloading.stsep]
read_s [in LemmaOverloading.stsep]
recurse [in LemmaOverloading.auto]
recurse_tag [in LemmaOverloading.xfind]
relax [in LemmaOverloading.domains]
rem [in LemmaOverloading.finmap]
remove [in LemmaOverloading.llistR]
repack_Pred [in LemmaOverloading.rels]
ret [in LemmaOverloading.stsep]
ret_s [in LemmaOverloading.stsep]
reverse [in LemmaOverloading.llistR]
revT [in LemmaOverloading.llistR]
right_tag [in LemmaOverloading.indom]
right_tag [in LemmaOverloading.stlogR]
runs_of [in LemmaOverloading.stmod]
S
scan_axiom [in LemmaOverloading.noaliasCTC]Scan.axiom [in LemmaOverloading.noalias]
Scan.default_tag [in LemmaOverloading.noalias]
Scan.ptr_tag [in LemmaOverloading.noalias]
search_them [in LemmaOverloading.noalias]
Search.axiom [in LemmaOverloading.noalias]
Search.recurse_tag [in LemmaOverloading.noalias]
search2_axiom [in LemmaOverloading.noaliasCTC]
Search2.axiom [in LemmaOverloading.noalias]
Search2.foundy_tag [in LemmaOverloading.noalias]
Search2.foundz_tag [in LemmaOverloading.noalias]
shape_rev [in LemmaOverloading.llistR]
SimplPred [in LemmaOverloading.rels]
Simpl_Pred [in LemmaOverloading.rels]
single [in LemmaOverloading.stmod]
spec [in LemmaOverloading.stmod]
star [in LemmaOverloading.hprop]
stLatticeMixin [in LemmaOverloading.stmod]
stPosetMixin [in LemmaOverloading.stmod]
stress [in LemmaOverloading.cancel]
stress [in LemmaOverloading.cancel2]
STsep [in LemmaOverloading.stsep]
st_sup [in LemmaOverloading.stmod]
st_sup' [in LemmaOverloading.stmod]
st_bot [in LemmaOverloading.stmod]
st_bot' [in LemmaOverloading.stmod]
st_leq [in LemmaOverloading.stmod]
subCPO [in LemmaOverloading.domains]
subCPOMixin [in LemmaOverloading.domains]
subctx [in LemmaOverloading.terms]
subdom [in LemmaOverloading.heaps]
subheap [in LemmaOverloading.heaps]
subLattice [in LemmaOverloading.domains]
subLatticeMixin [in LemmaOverloading.domains]
SubMem [in LemmaOverloading.rels]
subPoset [in LemmaOverloading.domains]
subPosetMixin [in LemmaOverloading.domains]
SubPred [in LemmaOverloading.rels]
SubPredFun [in LemmaOverloading.rels]
SubPredType [in LemmaOverloading.rels]
SubPredType_trans [in LemmaOverloading.rels]
SubSimplPred [in LemmaOverloading.rels]
subtract [in LemmaOverloading.heaps]
sub_lim [in LemmaOverloading.domains]
sub_sup [in LemmaOverloading.domains]
sub_sup' [in LemmaOverloading.domains]
sub_leq [in LemmaOverloading.domains]
sub_bot [in LemmaOverloading.domains]
supdom [in LemmaOverloading.heaps]
supp [in LemmaOverloading.finmap]
sup_closure [in LemmaOverloading.domains]
sup_closed [in LemmaOverloading.domains]
swap [in LemmaOverloading.prelude]
synheap [in LemmaOverloading.terms]
T
tarski_gfp [in LemmaOverloading.domains]tarski_lfp [in LemmaOverloading.domains]
test [in LemmaOverloading.xfind]
this [in LemmaOverloading.hprop]
throw [in LemmaOverloading.stsep]
throw_s [in LemmaOverloading.stsep]
top [in LemmaOverloading.hprop]
triggered [in LemmaOverloading.noalias]
try [in LemmaOverloading.stsep]
try_s [in LemmaOverloading.stsep]
try_throwR [in LemmaOverloading.stlogR]
try_allocbR [in LemmaOverloading.stlogR]
try_allocR [in LemmaOverloading.stlogR]
try_retR [in LemmaOverloading.stlogR]
U
union2 [in LemmaOverloading.heaps]unit_test [in LemmaOverloading.xfind]
unit_test [in LemmaOverloading.xfindCTC]
upd [in LemmaOverloading.heaps]
update_axiom [in LemmaOverloading.stlogR]
updi [in LemmaOverloading.heaps]
V
valid [in LemmaOverloading.terms]valid_heaps [in LemmaOverloading.terms]
valid_ptrs [in LemmaOverloading.terms]
value [in LemmaOverloading.finmap]
val_throwR [in LemmaOverloading.stlogR]
val_allocbR [in LemmaOverloading.stlogR]
val_allocR [in LemmaOverloading.stlogR]
val_retR [in LemmaOverloading.stlogR]
vareq [in LemmaOverloading.terms]
vars [in LemmaOverloading.terms]
var_tag [in LemmaOverloading.cancel]
var_tag [in LemmaOverloading.auto]
verify' [in LemmaOverloading.stsep]
W
without_notation [in LemmaOverloading.noalias]write [in LemmaOverloading.stsep]
write_s [in LemmaOverloading.stsep]
Record Index
A
abs_heap [in LemmaOverloading.cancel2]abs_pts [in LemmaOverloading.cancel2]
ast [in LemmaOverloading.cancel]
Ast [in LemmaOverloading.cancelCTC]
B
bnd_form [in LemmaOverloading.stlogR]C
chain [in LemmaOverloading.domains]check [in LemmaOverloading.noalias]
check [in LemmaOverloading.auto]
check' [in LemmaOverloading.noalias]
CPO.class_of [in LemmaOverloading.domains]
CPO.mixin_of [in LemmaOverloading.domains]
CPO.type [in LemmaOverloading.domains]
ctx [in LemmaOverloading.terms]
D
Dyn.dynamic [in LemmaOverloading.prelude]E
equate_to [in LemmaOverloading.auto]F
find [in LemmaOverloading.indom]find [in LemmaOverloading.auto]
Find1 [in LemmaOverloading.stlogCTC]
finMap [in LemmaOverloading.finmap]
form [in LemmaOverloading.auto]
form [in LemmaOverloading.cancelD]
H
heapeq [in LemmaOverloading.cancel2]I
ideal [in LemmaOverloading.domains]Indom [in LemmaOverloading.indomCTC]
L
Lattice.class_of [in LemmaOverloading.domains]Lattice.mixin_of [in LemmaOverloading.domains]
Lattice.type [in LemmaOverloading.domains]
N
NoAlias.form [in LemmaOverloading.noalias]NoAlias.tagged_ptr [in LemmaOverloading.noalias]
NoAlias2.form [in LemmaOverloading.noaliasBT]
NoAlias2.tagged_bool [in LemmaOverloading.noaliasBT]
NoAlias3.form [in LemmaOverloading.noaliasBT]
O
Ordered.class_of [in LemmaOverloading.ordtype]Ordered.mixin_of [in LemmaOverloading.ordtype]
Ordered.type [in LemmaOverloading.ordtype]
P
pack_heap [in LemmaOverloading.cancel2]Poset.class_of [in LemmaOverloading.domains]
Poset.mixin_of [in LemmaOverloading.domains]
Poset.type [in LemmaOverloading.domains]
PredType [in LemmaOverloading.rels]
S
Scan [in LemmaOverloading.noaliasCTC]Scan.form [in LemmaOverloading.noalias]
Scan.tagged_heap [in LemmaOverloading.noalias]
Search [in LemmaOverloading.noaliasCTC]
Search.form [in LemmaOverloading.noalias]
Search.tagged_seq [in LemmaOverloading.noalias]
Search2 [in LemmaOverloading.noaliasCTC]
Search2.form [in LemmaOverloading.noalias]
Search2.tagged_seq [in LemmaOverloading.noalias]
ST [in LemmaOverloading.stmod]
T
tagged_heap [in LemmaOverloading.cancel]tagged_heap [in LemmaOverloading.indom]
tagged_prop [in LemmaOverloading.auto]
tagged_seq [in LemmaOverloading.auto]
tagged_prop [in LemmaOverloading.cancelD]
tagged_heap [in LemmaOverloading.stlogR]
trigger [in LemmaOverloading.cancel2]
try_form [in LemmaOverloading.stlogR]
U
Update [in LemmaOverloading.stlogCTC]update [in LemmaOverloading.stlogR]
V
val_form [in LemmaOverloading.stlogR]X
xfind [in LemmaOverloading.xfind]XFind [in LemmaOverloading.xfindCTC]
xtagged [in LemmaOverloading.xfind]
| 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 | (2070 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 | (72 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 | (22 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 | (312 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 | (28 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 | (711 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 | (97 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (80 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 | (16 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 | (137 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 | (24 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 | (69 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 | (436 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 | (64 entries) |