[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 heap-sep

heap-sep/cell-heap/and is used by remove-contract, insert-contract,
heap-sep/cell-heap/and-ass is used by remove-simple-contract, remove-contract, insert-contract,
heap-sep/cell-heap/and-com is used by remove-simple-contract, remove-contract, insert-contract,
heap-sep/cell-heap/emp-sep is used by remove-contract,
heap-sep/cell-heap/false-and is used by remove-simple-contract,
heap-sep/cell-heap/false-rev is used by remove-simple-contract,
heap-sep/cell-heap/false-sep is used by remove-simple-contract,
heap-sep/cell-heap/falseH is used by remove-simple-contract,
heap-sep/cell-heap/prop is used by remove-contract, insert-contract,
heap-sep/cell-heap/prop-shift is used by remove-contract, insert-contract,
heap-sep/cell-heap/sep-ass is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
heap-sep/cell-heap/sep-com is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
heap-sep/cell-heap/true-and is used by remove-contract, insert-contract,
heap-sep/cell-heap/true-rev is used by remove-contract, insert-contract,

Used from specification nat

nat/add-num-01 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, insert-contract,
nat/lels-01 is used by remove-simple-contract,

Used from specification maplet

maplet/cell-heap/at-rw is used by remove-contract, insert-contract,
maplet/cell-heap/eq-objs is used by remove-insert-inverse-twice,
maplet/cell-heap/ex1-shift is used by remove-simple-contract, remove-contract, insert-contract,
maplet/cell-heap/ex2-shift is used by remove-contract, insert-contract,

Used from specification list-last

list-last/reflist/last-def is used by remove-contract, insert-contract,

Used from specification list-data

list-data/reflist/elim-list-c is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, insert-contract,
list-data/l is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, insert-contract,
list-data/reflist/l is used by remove-simple-contract, remove-contract, insert-contract,
list-data/size-01 is used by remove-simple-contract, remove-contract, insert-contract,
list-data/reflist/size-01 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-contract,

Used from specification dllist

dllist/dls-last is used by remove-simple-contract, remove-contract, insert-contract,
dllist/dls-one is used by insert-contract,
dllist/dls-rec is used by remove-simple-contract, remove-contract, insert-contract,
dllist/dls-split is used by remove-contract, insert-contract,
dllist/dls-emp is used by remove-contract,
dllist/dls-length is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,

Used from specification list

list/reflist/In is used by remove-simple-contract,
list/lastdiv-rew is used by remove-contract, insert-contract,
list/reflist/lastdiv-rew is used by remove-contract, insert-contract,
list/split-first is used by remove-simple-contract,
list/reflist/Nil is used by remove-simple-contract, remove-contract, insert-contract,
list/Nil is used by remove-simple-contract, remove-contract, insert-contract,
list/a is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
list/reflist/a is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
list/app is used by remove-simple-contract,
list/reflist/app is used by remove-simple-contract, remove-insert-inverse-twice,
list/reflist/c is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-contract,
list/c is used by remove-simple-contract, remove-contract, insert-contract,
list/reflist/c-07 is used by remove-simple-contract, remove-contract, insert-contract,
list/reflist/c-08 is used by remove-simple-contract, remove-contract, insert-simple-contract, insert-contract,
list/e is used by insert-contract,
list/reflist/e-01 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-contract,
list/e-01 is used by remove-contract, insert-contract,
list/e-02 is used by insert-contract,
list/reflist/in-01 is used by remove-insert-inverse-twice,
list/reflist/in-13 is used by remove-insert-inverse-twice, remove-insert-inverse,
list/reflist/in-17 is used by remove-insert-inverse-twice,
list/reflist/in-append is used by remove-insert-inverse-twice,
list/len is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
list/reflist/len is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
list/reflist/len-02 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
list/len-02 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-contract,

Used from specification nat-basic2

nat-basic2/a is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
nat-basic2/c is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
nat-basic2/eq-01 is used by remove-simple-contract, remove-insert-inverse-twice, remove-insert-inverse, remove-contract, insert-simple-contract, insert-contract,
nat-basic2/l-02 is used by remove-simple-contract,
nat-basic2/oz is used by remove-simple-contract, remove-contract, insert-contract,

Used from specification separation

separation/cell-heap/assign-known is used by remove-contract, insert-contract,

Used from specification cell

cell/sel-02 is used by remove-contract, insert-contract,
cell/sel-03 is used by remove-contract, insert-contract,
cell/upd-02 is used by remove-contract, insert-contract,
cell/upd-03 is used by remove-contract, insert-contract,

Used from specification nat-basic1

nat-basic1/f is used by remove-simple-contract,
nat-basic1/lf-02 is used by remove-simple-contract,