[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 store+set

store+set/address-store/restrict-at is used by remove-refsize0-subset-refed,
store+set/address-store/Dom is used by subseteq-dom-nodes-alloc-restrict-empty, remove-refsize0-subset-refed, remove-refsize0-refsize-cons, refsize-cons-append, inv-valid-adrs,
store+set/address-store/restrict-at is used by restrict-subseteq,
store+set/address-store/restrict-in is used by restrict-subseteq, remove-refsize0-subset-refed,

Used from specification ablock

Used from specification nat-basic

nat-basic/a is used by size-rem, size-rec-simp, size-rec-rem, size-eq-0, remove-refsize0-refsize-cons, refsize-cons-remove-index, refsize-cons-append, refsize-cons-alloc, inv-valid-adrs, in-remove-refsize0-refsize-cons,
nat-basic/add-base is used by refsize-cons-alloc,
nat-basic/c is used by size-rem, size-rec-simp, size-rec-rem, size-eq-0, remove-refsize0-refsize-cons, refsize-cons-remove-index, refsize-cons-append, refsize-cons-alloc, inv-valid-adrs, in-remove-refsize0-refsize-cons,
nat-basic/eq-01 is used by size-rec-simp, size-rec-rem, refsize-cons-append,
nat-basic/l-02 is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
nat-basic/oz is used by size-eq-0,
nat-basic/s-04 is used by size-eq-0, remove-refsize0-refsize-cons, in-remove-refsize0-refsize-cons,
nat-basic/succ is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
nat-basic/z-01 is used by size-eq-0,

Used from specification ablock-nodes

ablock-nodes/at-nodes is used by remove-refsize0-subset-refed,
ablock-nodes/in-nodes is used by subseteq-dom-nodes-alloc-restrict-empty, remove-refsize0-subset-refed, remove-refsize0-refsize-cons, refsize-cons-append, inv-valid-adrs,

Used from specification ablock-store-inv

Used from specification set-union

set-union/address-store/Difference is used by restrict-union-inter-empty-left,
set-union/address-store/Intersect is used by restrict-union-inter-empty-left,
set-union/address-store/subdef is used by remove-refsize0-refsize-cons,
set-union/address-store/unrax is used by restrict-union-inter-empty-left, restrict-union,
set-union/address-store/Delete is used by restrict-del-other, restrict-del,
set-union/address-store/del-addeq-04 is used by size-rem,
set-union/address-store/del-e-01 is used by refsize-cons-alloc,
set-union/address-store/del-in is used by size-rem,
set-union/address-store/int-a is used by restrict-union-inter-empty-left,
set-union/address-store/int-c is used by restrict-union-inter-empty-left,
set-union/address-store/una is used by restrict-union,
set-union/address-store/unc is used by restrict-union,
set-union/address-store/unin is used by restrict-union,

Used from specification store

store/ablock-store-nat-store/At-other is used by refsize-cons-remove-index-0, refsize-cons-remove-index, refsize-cons-append, refsize-cons-alloc,
store/address-store/Subset is used by restrict-subseteq, remove-refsize0-subset-refed,
store/ablock-store-nat-store/At-other is used by refsize-cons-write,
store/ablock-store-nat-store/At-same is used by refsize-cons-write, refsize-cons-remove-index-0, refsize-cons-remove-index, refsize-cons-append, refsize-cons-alloc,
store/ablock-store-nat-store/Del-at is used by refsize-cons-dealloc,
store/ablock-store-nat-store/Del-in is used by refsize-cons-dealloc,
store/ablock-store-nat-store/In-empty is used by refsize-cons-emtpy,
store/ablock-store-nat-store/In-insert is used by refsize-cons-alloc,
store/ablock-store-nat-store/in-neq is used by refsize-cons-write, refsize-cons-remove-index-0, refsize-cons-remove-index, refsize-cons-append, refsize-cons-alloc,
store/ablock-store-nat-store/insin is used by refsize-cons-write, refsize-cons-remove-index-0, refsize-cons-remove-index, refsize-cons-append,
store/ablock-store-nat-store/notmemlookup is used by remove-refsize0-subset-refed, refsize-cons-write, in-remove-refsize0-refsize-cons,

Used from specification nat

nat/eq-01 is used by size-rem, size-rec-rem, refsize-cons-remove-index,
nat/lels is used by inv-valid-adrs,
nat/sub-base is used by size-rem, size-rec-rem,
nat/succ-01 is used by inv-valid-adrs,

Used from specification set-basic

set-basic/address-store/Extension is used by subseteq-dom-nodes-alloc-restrict-empty, size-eq-0, restrict-union-inter-empty-left, restrict-union, restrict-empty, restrict-del-other, restrict-del, restrict-add-other, restrict-add,
set-basic/address-store/indef is used by size-rem, size-rec-rem, size-eq-0,
set-basic/address-store/In-empty is used by subseteq-dom-nodes-alloc-restrict-empty, size-eq-0-alloc, size-eq-0, restrict-empty,
set-basic/address-store/In-insert is used by size-eq-0, restrict-add-other, restrict-add,
set-basic/address-store/Size-insert is used by size-eq-0,
set-basic/address-store/eq is used by size-rec-simp, size-rec-rem, refsize-cons-append,
set-basic/address-store/in-02 is used by restrict-add,
set-basic/address-store/ne is used by size-rem, size-rec-rem,
set-basic/address-store/ne-01 is used by subseteq-dom-nodes-alloc-restrict-empty, size-rem, size-rec-rem, size-eq-0, restrict-del-other, remove-refsize0-subset-refed, remove-refsize0-refsize-cons, refsize-cons-remove-index-0, refsize-cons-remove-index, refsize-cons-append, inv-valid-adrs, in-remove-refsize0-refsize-cons,
set-basic/address-store/size-zero is used by subseteq-dom-nodes-alloc-restrict-empty, size-eq-0, restrict-empty,
set-basic/address-store/size-zero-01 is used by subseteq-dom-nodes-alloc-restrict-empty, size-rem, size-rec-rem, size-eq-0, restrict-empty, remove-refsize0-subset-refed, remove-refsize0-refsize-cons, refsize-cons-remove-index-0, refsize-cons-remove-index, inv-valid-adrs, in-remove-refsize0-refsize-cons,
set-basic/address-store/sub-in is used by subseteq-dom-nodes-alloc-restrict-empty, remove-refsize0-subset-refed, remove-refsize0-refsize-cons, refsize-cons-append, inv-valid-adrs,
set-basic/address-store/sub-ntrans is used by remove-refsize0-refsize-cons,

Used from specification laddress

laddress/sel-01 is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,

Used from specification list

list/laddress-list/in-def is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
list/a is used by refsize-cons-append,
list/laddress-list/a is used by remove-refsize0-refsize-cons, refsize-cons-append, inv-valid-adrs, in-remove-refsize0-refsize-cons,
list/laddress-list/c is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
list/laddress-list/in-15 is used by refsize-cons-append,
list/in-15 is used by refsize-cons-append,
list/in-17 is used by refsize-cons-append,
list/laddress-list/in-17 is used by refsize-cons-append,
list/laddress-list/in-append is used by refsize-cons-append,
list/in-append is used by refsize-cons-append,
list/laddress-list/len is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
list/laddress-list/len-05 is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,

Used from specification list-dup

list-dup/laddress-list/a is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,
list-dup/laddress-list/f-01 is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,

Used from specification address-data

Used from specification oelem

oelem/nat-set/irreflexivity is used by size-eq-0,

Used from specification list-del

list-del/laddress-list/get-app is used by remove-refsize0-refsize-cons, inv-valid-adrs, in-remove-refsize0-refsize-cons,