[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/SetInv is used by inv-tid,
Set/gstepf-invInsert-DOINSERT is used by allinserts-finished-false-implies-notin-ind, frag-in, frag-rely-inv, insert-inset-after-retinsert-ind,
Set/gstepf-invMember-DOMEMBER is used by frag-in, frag-rely-inv, insert-inset-after-retinsert-ind, frag-retMem,
Set/gstepf-retInsert-RETINSERT is used by frag-in, frag-rely-inv, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
Set/gstepf-retMember-RETMEMBER is used by frag-in, frag-rely-inv, insert-inset-after-retinsert-ind,
Set/lstepf-idle-INVINSERT is used by frag-DoIns, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem,
Set/lstepf-idle-INVMEMBER is used by inset-member-returns-true-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/lstepf-invInsert-DOINSERT is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem,
Set/lstepf-invMember-DOMEMBER is used by inset-member-returns-true-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/lstepf-retInsert-RETINSERT is used by frag-DoIns, frag-retIns, frag-retMem,
Set/lstepf-retMember-RETMEMBER is used by frag-DoIns, frag-retIns, frag-retMem,
Set/pcstepf-idle-INVINSERT is used by insert-inset-after-retinsert-ind,
Set/pcstepf-idle-INVMEMBER is used by inset-member-returns-true-ind,
Set/pcstepf-invInsert-DOINSERT is used by insert-inset-after-retinsert-ind,
Set/pcstepf-invMember-DOMEMBER is used by inset-member-returns-true-ind,
Set/setInit is used by theorem-member-returns-true-after-insert,
Set/setStep is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/disj-ADoInsert-ADoMember is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in,
Set/disj-ADoInsert-AInvInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, insert-inset-after-retinsert-ind,
Set/disj-ADoInsert-AInvMember is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in,
Set/disj-ADoInsert-ARetInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retIns, insert-inset-after-retinsert,
Set/disj-ADoInsert-ARetMember is used by inset-member-returns-true, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retMem,
Set/disj-ADoInsert-tau is used by frag-DoIns, frag-retIns, frag-retMem,
Set/disj-ADoMember-AInvInsert is used by insert-inset-after-retinsert-ind,
Set/disj-ADoMember-AInvMember is used by inset-member-returns-true-ind,
Set/disj-ADoMember-ARetInsert is used by frag-retIns, insert-inset-after-retinsert,
Set/disj-ADoMember-ARetMember is used by inset-member-returns-true, frag-retMem,
Set/disj-ADoMember-tau is used by frag-DoIns, frag-retIns, frag-retMem,
Set/disj-AInvInsert-AInvMember is used by inset-member-returns-true-ind, frag-DoIns, insert-inset-after-retinsert-ind,
Set/disj-AInvInsert-ARetInsert is used by frag-retIns, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
Set/disj-AInvInsert-ARetMember is used by inset-member-returns-true, insert-inset-after-retinsert-ind, frag-retMem,
Set/disj-AInvInsert-tau is used by frag-DoIns, frag-retIns, frag-retMem,
Set/disj-AInvMember-ARetInsert is used by inset-member-returns-true-ind, frag-retIns, insert-inset-after-retinsert,
Set/disj-AInvMember-ARetMember is used by inset-member-returns-true, inset-member-returns-true-ind, frag-retMem,
Set/disj-AInvMember-tau is used by frag-DoIns, frag-retIns, frag-retMem,
Set/disj-ARetInsert-ARetMember is used by inset-member-returns-true, frag-retIns, frag-retMem, insert-inset-after-retinsert,
Set/disj-ARetInsert-tau is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/disj-ARetMember-tau is used by frag-DoIns, frag-retIns, frag-retMem,
Set/disj-idle-invInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns,
Set/disj-idle-invMember is used by frag-DoIns,
Set/disj-idle-retInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns,
Set/disj-idle-retMember is used by frag-DoIns, frag-retMem,
Set/disj-invInsert-invMember is used by frag-DoIns, frag-in, frag-retIns,
Set/disj-invInsert-retInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retIns, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
Set/disj-invInsert-retMember is used by frag-DoIns, frag-in, frag-retIns, frag-retMem,
Set/disj-invMember-retInsert is used by allinserts-finished-false-implies-notin-ind, frag-retIns,
Set/disj-invMember-retMember is used by inset-member-returns-true, inset-member-returns-true-ind, frag-retMem,
Set/disj-retInsert-retMember is used by allinserts-finished-false-implies-notin-ind, frag-retIns, frag-retMem,
Set/elim-mkstate is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, theorem-allinserts-finished-false-implies-notin, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/gstepf-idle is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem,
Set/gstepf-invInsert-DOINSERT is used by allinserts-finished-false-implies-notin-ind, frag-retIns,
Set/gstepf-invMember-DOMEMBER is used by allinserts-finished-false-implies-notin-ind, frag-retMem,
Set/gstepf-retInsert-RETINSERT is used by allinserts-finished-false-implies-notin-ind,
Set/gstepf-retMember-RETMEMBER is used by allinserts-finished-false-implies-notin-ind,
Set/inj-ADoInsert is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retIns,
Set/inj-ADoMember is used by frag-retMem,
Set/inj-AInvInsert is used by frag-DoIns, insert-inset-after-retinsert-ind,
Set/inj-AInvMember is used by inset-member-returns-true-ind,
Set/inj-ARetInsert is used by frag-retIns, insert-inset-after-retinsert,
Set/inj-ARetMember is used by inset-member-returns-true, frag-retMem,
Set/inj-mkstate is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, theorem-allinserts-finished-false-implies-notin, frag-in, frag-rely-inv, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
Set/lstep is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/lstepf-invInsert-DOINSERT is used by allinserts-finished-false-implies-notin-ind, frag-in,
Set/lstepf-invMember-DOMEMBER is used by allinserts-finished-false-implies-notin-ind,
Set/lstepf-retInsert-RETINSERT is used by allinserts-finished-false-implies-notin-ind,
Set/lstepf-retMember-RETMEMBER is used by allinserts-finished-false-implies-notin-ind,
Set/pcstepf-idle-INVINSERT is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/pcstepf-idle-INVMEMBER is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/pcstepf-invInsert-DOINSERT is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retIns, frag-retMem,
Set/pcstepf-invMember-DOMEMBER is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/pcstepf-retInsert-RETINSERT is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/pcstepf-retMember-RETMEMBER is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/pre-idle is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/pre-invInsert is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/pre-invMember is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/pre-retInsert is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/pre-retMember is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/sel-ADoInsert-dottid is used by frag-DoIns, frag-retIns, frag-retMem,
Set/sel-ADoMember-dottid is used by frag-DoIns, frag-retIns, frag-retMem,
Set/sel-AInvInsert-dottid is used by frag-DoIns, frag-retIns, frag-retMem,
Set/sel-AInvMember-dottid is used by frag-DoIns, frag-retIns, frag-retMem,
Set/sel-ARetInsert-dottid is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
Set/sel-ARetMember-dottid is used by frag-DoIns, frag-retIns, frag-retMem,
Set/sel-mkstate-dotgstate is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-in, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/sel-mkstate-dotlsf is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/sel-mkstate-dotpcf is used by inset-member-returns-true, inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem, insert-inset-after-retinsert,
Set/setInit is used by allinserts-finished-false-implies-notin-ind,
Set/updsel--dotlb-dotlb is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem,
Set/updsel--dotlb-dotle is used by allinserts-finished-false-implies-notin-ind, frag-DoIns,
Set/updsel--dotle-dotle is used by inset-member-returns-true-ind, frag-DoIns, insert-inset-after-retinsert-ind,
Set/updsel--dotset-dotset is used by allinserts-finished-false-implies-notin-ind, frag-in, frag-rely-inv, insert-inset-after-retinsert-ind,

Used from specification IO-Aut-data

Used from specification nat-basic

Used from specification nat

nat/add-01 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, theorem-allinserts-finished-false-implies-notin,
nat/add-num-01 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-retIns, frag-retMem,
nat/add-num-03 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/add-num-04 is used by frag-DoIns, frag-retIns, frag-retMem,
nat/cancel-01 is used by theorem-member-returns-true-after-insert,
nat/elim-pred-c is used by theorem-member-returns-true-after-insert, frag-DoIns, theorem-allinserts-finished-false-implies-notin, frag-in, frag-retIns, frag-retMem,
nat/eq is used by theorem-member-returns-true-after-insert,
nat/eqle-one is used by theorem-member-returns-true-after-insert,
nat/fle is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-retIns, frag-retMem,
nat/l-num-01 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/l-num-06 is used by theorem-member-returns-true-after-insert, frag-DoIns, frag-retIns, frag-retMem,
nat/le-add is used by theorem-member-returns-true-after-insert,
nat/le-def is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, theorem-allinserts-finished-false-implies-notin,
nat/le-num-02 is used by theorem-member-returns-true-after-insert,
nat/le-num-06 is used by theorem-member-returns-true-after-insert,
nat/lels is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-retIns, frag-retMem,
nat/lels-03 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/lep is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/lep-02 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/ler is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/lez is used by frag-DoIns, frag-in, frag-retIns, frag-retMem,
nat/ls-01 is used by theorem-allinserts-finished-false-implies-notin,
nat/one-01 is used by theorem-member-returns-true-after-insert,
nat/pred-03 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
nat/succ-01 is used by allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-retIns, frag-retMem,
nat/zero is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,

Used from specification remtau

Used from specification set-basic

set-basic/In-empty is used by allinserts-finished-false-implies-notin-ind,
set-basic/add is used by insert-inset-after-retinsert-ind,
set-basic/in is used by frag-in, insert-inset-after-retinsert-ind,
set-basic/in-03 is used by allinserts-finished-false-implies-notin-ind, frag-in,
set-basic/ne is used by allinserts-finished-false-implies-notin-ind, frag-in,
set-basic/ne-01 is used by inset-member-returns-true, inset-member-returns-true-ind, theorem-member-returns-true-after-insert, theorem-allinserts-finished-false-implies-notin, frag-in, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
set-basic/size-zero-01 is used by inset-member-returns-true, inset-member-returns-true-ind, theorem-member-returns-true-after-insert, theorem-allinserts-finished-false-implies-notin, frag-in, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
set-basic/sub-add-03 is used by frag-rely-inv,
set-basic/sub-e is used by allinserts-finished-false-implies-notin-ind,
set-basic/sub-in is used by inset-member-returns-true, inset-member-returns-true-ind, theorem-member-returns-true-after-insert,
set-basic/sub-ntrans-01 is used by frag-rely-inv,
set-basic/sub-trans is used by theorem-member-returns-true-after-insert,
set-basic/subsize-eq-01 is used by theorem-member-returns-true-after-insert, frag-rely-inv,

Used from specification list-last

list-last/lapp is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-last/l-01 is used by inset-member-returns-true-ind, insert-inset-after-retinsert-ind,
list-last/l-02 is used by inset-member-returns-true-ind, frag-DoIns, frag-retIns, insert-inset-after-retinsert-ind,
list-last/l-06 is used by frag-DoIns, frag-in, frag-retIns,
list-last/last-01 is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-last/last-def is used by insert-inset-after-retinsert-ind,
list-last/last-elim is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, insert-inset-after-retinsert-ind, insert-inset-after-retinsert,
list-last/last-one is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-rely-inv,
list-last/last-rec is used by frag-DoIns, frag-in, frag-rely-inv, frag-retIns,

Used from specification opt

Used from specification list-data

Used from specification stream

stream/append-to-gr is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
stream/append-to-le is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
stream/append-from-gt is used by theorem-member-returns-true-after-insert,
stream/append-from-le is used by allinserts-finished-false-implies-notin-ind,
stream/append-from-size is used by theorem-member-returns-true-after-insert,
stream/append-to-gr is used by allinserts-finished-false-implies-notin-ind,
stream/append-to-size is used by theorem-member-returns-true-after-insert,
stream/from-cons-one-fin is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
stream/from-succ-cons-l-lem is used by allinserts-finished-false-implies-notin-ind,
stream/get-finto is used by allinserts-finished-false-implies-notin-ind,
stream/lslen-fromnotempty-list is used by allinserts-finished-false-implies-notin-ind,
stream/to-succ-cons-l-lem is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,

Used from specification IOtrace

Used from specification list

Used from specification Set-proofs

Set-proofs/SetInv-thm is used by frag-in, frag-rely-inv,
Set-proofs/init-state-inv is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
Set-proofs/SetInv-thm is used by inset-member-returns-true-ind, allinserts-finished-false-implies-notin-ind, frag-DoIns, frag-in, frag-rely-inv, frag-retIns, insert-inset-after-retinsert-ind, frag-retMem,

Used from specification list-del

list-del/firstN-num-rec is used by allinserts-finished-false-implies-notin-ind,
list-del/firstn-last-rec is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-del/get-append-grt is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-retIns, frag-retMem,
list-del/get-append-less is used by frag-in,
list-del/get-last-nonempty is used by theorem-allinserts-finished-false-implies-notin,
list-del/elim-firstn-restn is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-del/first-length is used by allinserts-finished-false-implies-notin-ind,
list-del/firstn-app is used by allinserts-finished-false-implies-notin-ind,
list-del/firstn-length-03 is used by allinserts-finished-false-implies-notin-ind,
list-del/firstn-one is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-del/firstn-one-01 is used by allinserts-finished-false-implies-notin-ind,
list-del/get-app is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-del/get-append-grt is used by frag-in,
list-del/get-append-grt-02 is used by allinserts-finished-false-implies-notin-ind,
list-del/get-append-less is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert,
list-del/get-butlast is used by allinserts-finished-false-implies-notin-ind,
list-del/get-succ is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-retIns, frag-retMem,
list-del/get-zero is used by allinserts-finished-false-implies-notin-ind, theorem-member-returns-true-after-insert, frag-DoIns, frag-in, frag-retIns, frag-retMem,
list-del/one-03 is used by frag-in,
list-del/restn-app is used by allinserts-finished-false-implies-notin-ind,

Used from specification list-getput