[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification Set

Set/SetGInv is used by init-state-inv,
Set/SetInv is used by init-state-inv,
Set/SetLInv is used by init-state-inv,
Set/disj-AInvInsert-AInvMember is used by step-idle-invInsert,
Set/disj-idle-invInsert is used by init-state-inv,
Set/disj-idle-invMember is used by init-state-inv,
Set/disj-idle-retInsert is used by init-state-inv,
Set/disj-idle-retMember is used by init-state-inv,
Set/disj-invInsert-invMember is used by step-idle-invMember,
Set/gstepf-invInsert-DOINSERT is used by step-invInsert-retInsert, rely-invInsert-retInsert,
Set/gstepf-invMember-DOMEMBER is used by step-invMember-retMember,
Set/inj-ADoInsert is used by definedness-invInsert-ADoInsert,
Set/lstepf-idle-INVINSERT is used by step-idle-invInsert,
Set/lstepf-idle-INVMEMBER is used by step-idle-invMember, step-idle-invInsert,
Set/lstepf-invInsert-DOINSERT is used by step-invInsert-retInsert,
Set/lstepf-invMember-DOMEMBER is used by step-invMember-retMember,
Set/pcstepf-idle-INVINSERT is used by step-idle-invMember, step-idle-invInsert,
Set/pcstepf-invInsert-DOINSERT is used by step-invInsert-retInsert, rely-invInsert-retInsert,
Set/pcstepf-invMember-DOMEMBER is used by step-invMember-retMember,
Set/pre-idle is used by step-idle-invMember, step-idle-invInsert,
Set/pre-invInsert is used by step-invInsert-retInsert, rely-invInsert-retInsert, definedness-invInsert-ADoInsert,
Set/pre-invMember is used by step-invMember-retMember,
Set/updsel--dotlb-dotlb is used by step-invInsert-retInsert, step-invMember-retMember,
Set/updsel--dotlb-dotle is used by step-invInsert-retInsert, step-invMember-retMember,
Set/updsel--dotle-dotle is used by step-idle-invMember, step-idle-invInsert,
Set/updsel--dotset-dotset is used by step-invInsert-retInsert, rely-invInsert-retInsert,

Used from specification set-basic

set-basic/add is used by step-invInsert-retInsert,
set-basic/ne-01 is used by stable-retInsert,
set-basic/sub-add-01 is used by rely-invInsert-retInsert,
set-basic/sub-in is used by stable-retInsert,
set-basic/subsize-eq-01 is used by rely-invInsert-retInsert, rely-reflexive,