[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/ablock-store-nat-store/Dom is used by prefix-subseteq-dom-nodes-rev,
store+set/address-store/Dom is used by prefix-subseteq-dom-nodes-rev, prefix-imp-dom-nodes-subset, notin-add-diff-dom-nodes, insert-inter-notin-dom-nodes,

Used from specification ablock

ablock/elim is used by prefix-subseteq-dom-nodes-rev, nodes-append, nodes-alloc-append, nodes-alloc,
ablock/inj is used by nodes-append, nodes-alloc-append, nodes-alloc,
ablock/sel-01 is used by prefix-subseteq-dom-nodes-rev, nodes-write-refsize, nodes-append, nodes-alloc-append,
ablock/sel-02 is used by prefix-subseteq-dom-nodes-rev, nodes-write-refsize, nodes-append, nodes-alloc-append,

Used from specification nat-basic

nat-basic/a is used by nodes-append,
nat-basic/add-base is used by nodes-append,
nat-basic/c is used by nodes-append,

Used from specification ablock-store-inv

ablock-store-inv/at is used by nodes-append, nodes-alloc-append,
ablock-store-inv/blockstore-prefix is used by prefix-subseteq-dom-nodes-rev,
ablock-store-inv/in is used by prefix-subseteq-dom-nodes-rev, nodes-alloc-append, nodes-alloc,
ablock-store-inv/inv-block is used by nodes-append,
ablock-store-inv/at-alloc is used by nodes-at-alloc,
ablock-store-inv/at-explicit-other is used by nodes-alloc-append, nodes-alloc,
ablock-store-inv/at-write-same is used by nodes-write-refsize,
ablock-store-inv/in-adr-in is used by nodes-append,
ablock-store-inv/in-alloc is used by nodes-at-alloc, nodes-alloc-subseteq, nodes-alloc-append, nodes-alloc,
ablock-store-inv/in-empty is used by nodes-empty,
ablock-store-inv/in-in-adr is used by nodes-alloc-append, nodes-alloc,
ablock-store-inv/in-write-app is used by nodes-append,
ablock-store-inv/in-write-explicit is used by nodes-append, nodes-alloc-append,
ablock-store-inv/in-write-same is used by nodes-write-refsize,
ablock-store-inv/inv-eq-list-size is used by nodes-append,
ablock-store-inv/notin-notin is used by nodes-alloc-append, nodes-alloc,
ablock-store-inv/prefix-at is used by prefix-imp-nodes-subset, prefix-imp-dom-nodes-subset,
ablock-store-inv/prefix-in is used by prefix-imp-nodes-subset, prefix-imp-dom-nodes-subset,
ablock-store-inv/prefix-notin-fwd is used by prefix-imp-dom-nodes-subset,
ablock-store-inv/to-adrs-one is used by nodes-append,

Used from specification set-union

set-union/address-store/Difference is used by notin-add-diff-dom-nodes,
set-union/address-store/Intersect is used by insert-inter-notin-dom-nodes,
set-union/nat-set/subdef is used by prefix-subseteq-dom-nodes-rev,
set-union/address-store/subdef is used by prefix-subseteq-dom-nodes-rev, prefix-imp-dom-nodes-subset,
set-union/address-store/int-a is used by insert-inter-notin-dom-nodes,
set-union/address-store/int-c is used by insert-inter-notin-dom-nodes,

Used from specification store

store/ablock-store-nat-store/At-other is used by nodes-alloc,
store/ablock-store-nat-store/In-insert is used by nodes-alloc,
store/address-store/Subset is used by prefix-imp-nodes-subset, nodes-alloc-subseteq,
store/address-store/k-Extension is used by nodes-write-refsize, nodes-empty, nodes-append, nodes-alloc-append, nodes-alloc,
store/ablock-store-nat-store/At-other is used by nodes-append, nodes-alloc-append,
store/address-store/At-other is used by nodes-append, nodes-alloc-append,
store/ablock-store-nat-store/At-same is used by nodes-append, nodes-alloc-append, nodes-alloc,
store/address-store/At-same is used by nodes-append, nodes-alloc-append,
store/address-store/In-empty is used by nodes-empty,
store/ablock-store-nat-store/In-insert is used by nodes-alloc-append,
store/ablock-store-nat-store/in-neq is used by nodes-alloc-append,
store/address-store/in-neq is used by nodes-append, nodes-alloc-append,
store/address-store/insin is used by nodes-append, nodes-alloc-append,

Used from specification nat

nat/lels is used by nodes-append,

Used from specification set-basic

set-basic/address-store/Extension is used by prefix-subseteq-dom-nodes-rev, notin-add-diff-dom-nodes, insert-inter-notin-dom-nodes,
set-basic/address-store/In-insert is used by notin-add-diff-dom-nodes, insert-inter-notin-dom-nodes,
set-basic/address-store/in-02 is used by notin-add-diff-dom-nodes,

Used from specification list-last

list-last/laddress-list/prefix-notin is used by prefix-subseteq-dom-nodes-rev,

Used from specification laddress

laddress/elim is used by nodes-append, nodes-alloc-append,
laddress/inj is used by nodes-alloc-append,
laddress/sel-01 is used by nodes-append,
laddress/sel-02 is used by nodes-append,

Used from specification list

list/a is used by nodes-append,
list/laddress-list/a is used by nodes-append,
list/laddress-list/in-15 is used by nodes-append,
list/in-15 is used by nodes-append,
list/laddress-list/in-17 is used by nodes-append, nodes-alloc-append,
list/address-list-set/in-17 is used by nodes-append,
list/in-17 is used by nodes-append,
list/laddress-list/in-append is used by nodes-append,
list/in-append is used by nodes-append,
list/laddress-list/in-empty is used by nodes-alloc,
list/len-02 is used by nodes-append,
list/laddress-list/len-02 is used by nodes-append,

Used from specification address-data

address-data/elim is used by nodes-append, nodes-alloc-append, nodes-alloc,
address-data/sel-03 is used by prefix-subseteq-dom-nodes-rev, nodes-append, nodes-alloc-append,
address-data/sel-04 is used by prefix-subseteq-dom-nodes-rev, nodes-append, nodes-alloc-append,
address-data/sel-05 is used by prefix-subseteq-dom-nodes-rev, nodes-append, nodes-alloc-append,

Used from specification list-del

list-del/laddress-list/app-05-neg is used by nodes-append,
list-del/get-append-grt is used by nodes-append,
list-del/laddress-list/app-05 is used by nodes-append,
list-del/get-butlast is used by nodes-append,
list-del/get-last is used by nodes-append,
list-del/laddress-list/inl-01 is used by nodes-append,
list-del/laddress-list/notin-03 is used by nodes-append,
list-del/one-03 is used by nodes-alloc-append,
list-del/laddress-list/pos-one is used by nodes-append, nodes-alloc-append,