[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 linked-list

linked-list/ls-base is used by lls-to-ls,
linked-list/ls-fold1 is used by lls-to-ls,
linked-list/ls-null is used by lls-to-ls,
linked-list/ls-unfold2 is used by lls-to-ls,

Used from specification heap-sep

heap-sep/Eq-P is used by lls-to-ls,
heap-sep/And-prop-inj is used by lls-null,
heap-sep/and is used by lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-consecutive,
heap-sep/and-ass is used by lls-null, ll-trav1-next, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-unfold-head-simp, lls-consecutive, ll-trav2-next, ll-trav1-init,
heap-sep/and-com is used by lls-null, ll-trav1-next, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-unfold-head-simp, lls-consecutive, ll-trav2-next, ll-trav1-init,
heap-sep/emp-sep is used by lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-consecutive, ll-trav2-next, ll-trav1-init,
heap-sep/false-and is used by lls-null, ll-trav1-next, ll-trav2-end, ll-trav1-end, lls-unfold-head-simp, ll-trav2-next,
heap-sep/false-rev is used by lls-null, ll-trav1-next, ll-trav2-end, lls-one, ll-trav1-end, lls-unfold-head-simp, ll-trav2-next,
heap-sep/false-sep is used by lls-null, ll-trav1-next, ll-trav2-end, ll-trav1-end, lls-unfold-head-simp, ll-trav2-next,
heap-sep/falseH is used by lls-null, ll-trav1-next, ll-trav2-end, lls-one, ll-trav1-end, lls-unfold-head-simp, ll-trav2-next,
heap-sep/prop is used by lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-consecutive,
heap-sep/prop-shift is used by lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, lls-consecutive,
heap-sep/sep-ass is used by lls-null, lls-fold-head, ll-trav1-next, lls-unfold-head, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, ll-trav2-init, lls-unfold-head-simp, lls-consecutive, ll-trav2-next, ll-trav1-init,
heap-sep/sep-com is used by lls-null, lls-fold-head, ll-trav1-next, lls-unfold-head, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-one, lls-to-ls, ll-trav1-end, ll-trav2-init, lls-unfold-head-simp, lls-consecutive, ll-trav2-next, ll-trav1-init,
heap-sep/true-and is used by lls-null, ll-trav2-end, lls-to-ls, ll-trav1-end, ll-trav2-next, ll-trav1-init,
heap-sep/true-rev is used by lls-null, ll-trav2-end, lls-to-ls, ll-trav1-end, ll-trav2-next, ll-trav1-init,

Used from specification maplet

maplet/cell-heap/at-eq is used by lls-fold-head, ll-trav1-next, ll-trav2-end, ll-trav1-end, ll-trav2-next,
maplet/cell-heap/eq-objs is used by lls-fold-tail, lls-consecutive,
maplet/cell-heap/ex1 is used by lls-null, lls-unfold-tail, lls-one,
maplet/cell-heap/ex1-shift is used by lls-fold-head, ll-trav1-next, lls-unfold-head, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-to-ls, ll-trav1-end, lls-consecutive, ll-trav2-next,
maplet/cell-heap/map-null is used by lls-null,

Used from specification list-last

list-last/bc is used by lls-fold-tail,
list-last/butlast-def is used by lls-unfold-tail,
list-last/butlast-one is used by lls-fold-tail,
list-last/l-02 is used by lls-fold-tail,
list-last/last-def is used by lls-unfold-tail,
list-last/last-one is used by lls-fold-tail,

Used from specification list-data

list-data/elim-list-c is used by ll-trav1-next, ll-trav2-next,

Used from specification list

list/One is used by lls-one,
list/c is used by lls-one,
list/Last is used by ll-trav1-next, ll-trav2-end, ll-trav1-end, ll-trav2-next,
list/Nil is used by lls-unfold-tail, lls-consecutive, ll-trav2-next, ll-trav1-init,
list/a is used by lls-null, lls-fold-head, ll-trav1-next, lls-unfold-head, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-to-ls, ll-trav1-end, lls-unfold-head-simp, lls-consecutive, ll-trav2-next, ll-trav1-init,
list/app is used by ll-trav2-end, lls-fold-tail, ll-trav1-end,
list/app-01 is used by ll-trav1-next, ll-trav2-next,
list/app-02 is used by ll-trav2-end, ll-trav1-end,
list/app-03 is used by ll-trav2-end, ll-trav1-end,
list/app-07 is used by ll-trav2-next,
list/app-08 is used by ll-trav1-next, ll-trav2-next,
list/c is used by lls-null, ll-trav1-next, lls-unfold-head, lls-unfold-tail, ll-trav2-end, lls-fold-tail, lls-to-ls, ll-trav1-end, lls-consecutive, ll-trav2-next,
list/c-06 is used by lls-unfold-head,
list/e-01 is used by lls-null, ll-trav1-next, lls-unfold-head, ll-trav2-end, lls-fold-tail, ll-trav1-end, lls-unfold-head-simp, ll-trav2-next,
list/e-02 is used by lls-unfold-tail, ll-trav2-end, ll-trav1-end,
list/e-03 is used by ll-trav1-end,

Used from specification cell

cell/elim-tim is used by lls-fold-head,
cell/inj-tim is used by lls-fold-head, ll-trav1-next, ll-trav2-end, ll-trav1-end, ll-trav2-next,

Used from specification separation

separation/cell-heap/True is used by lls-fold-head,