[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/disj-ADoInsert-tau is used by abs-is-fwsim,
Set/disj-ADoMember-tau is used by abs-is-fwsim,
Set/disj-AInvInsert-tau is used by abs-is-fwsim,
Set/disj-AInvMember-tau is used by abs-is-fwsim,
Set/disj-ARetInsert-tau is used by abs-is-fwsim,
Set/disj-ARetMember-tau is used by abs-is-fwsim,
Set/inj-mkstate is used by abs-is-fwsim,
Set/sel-mkstate-dotgstate is used by abs-is-fwsim,
Set/sel-mkstate-dotlsf is used by abs-is-fwsim,
Set/sel-mkstate-dotpcf is used by abs-is-fwsim,
Set/setInit is used by abs-is-fwsim,

Used from specification IO-Aut-data

IO-Aut-data/sel-IOAut-dotext is used by abs-is-fwsim,

Used from specification nat-basic

nat-basic/zero is used by abs-is-fwsim,

Used from specification Hashset-refines-Set

Hashset-refines-Set/abs-init is used by abs-is-fwsim,
Hashset-refines-Set/abs-theorem is used by abs-is-fwsim,
Hashset-refines-Set/abs-def is used by abs-is-fwsim,
Hashset-refines-Set/gabs-def is used by abs-is-fwsim,
Hashset-refines-Set/ren-doINSERT is used by abs-is-fwsim,
Hashset-refines-Set/ren-doMEMBER is used by abs-is-fwsim,
Hashset-refines-Set/ren-invINSERT is used by abs-is-fwsim,
Hashset-refines-Set/ren-invMEMBER is used by abs-is-fwsim,
Hashset-refines-Set/ren-retINSERT is used by abs-is-fwsim,
Hashset-refines-Set/ren-retMEMBER is used by abs-is-fwsim,
Hashset-refines-Set/ren-tau is used by abs-is-fwsim,

Used from specification Hashset

Hashset/hashsetInit is used by abs-is-fwsim,
Hashset/sel-mkstate-dotgstate is used by abs-is-fwsim,
Hashset/sel-mkstate-dotlsf is used by abs-is-fwsim,
Hashset/sel-mkstate-dotpcf is used by abs-is-fwsim,

Used from specification remtau

remtau/finremtau-one is used by abs-is-fwsim,

Used from specification nat

nat/gr-def is used by abs-is-fwsim,

Used from specification list-last

list-last/last-def is used by abs-is-fwsim,

Used from specification opt

opt/disj-rqui-tau is used by abs-is-fwsim,
opt/elim-rqui is used by abs-is-fwsim,
opt/sel-rqui-dote is used by abs-is-fwsim,

Used from specification Set-Test-IOAut

Set-Test-IOAut/SetIOA-def is used by abs-is-fwsim,
Set-Test-IOAut/ext-DoInsert is used by abs-is-fwsim,
Set-Test-IOAut/ext-DoMember is used by abs-is-fwsim,
Set-Test-IOAut/ext-InvInsert is used by abs-is-fwsim,
Set-Test-IOAut/ext-InvMember is used by abs-is-fwsim,
Set-Test-IOAut/ext-RetInsert is used by abs-is-fwsim,
Set-Test-IOAut/ext-RetMember is used by abs-is-fwsim,

Used from specification IOtrace

IOtrace/move is used by abs-is-fwsim,
IOtrace/finfrag-two is used by abs-is-fwsim,
IOtrace/move-empty is used by abs-is-fwsim,

Used from specification Set-proofs

Set-proofs/init-state-inv is used by abs-is-fwsim,
Set-proofs/SetInv-thm is used by abs-is-fwsim,

Used from specification list

list/a is used by abs-is-fwsim,
list/c-04 is used by abs-is-fwsim,
list/e is used by abs-is-fwsim,

Used from specification list-del

list-del/get-zero is used by abs-is-fwsim,

Used from specification IOforward-is-leqrefine

IOforward-is-leqrefine/forward-implies-leqrefine is used by Hashset-refines-Set,

Used from specification IOforward

IOforward/forwardsim-def is used by Hashset-fwsim-Set,
IOforward/proofobls-forwardsim is used by abs-is-fwsim,

Used from specification Hashset-proofs

Hashset-proofs/HashsetInv-thm is used by abs-is-fwsim,
Hashset-proofs/init-state-inv is used by abs-is-fwsim,