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

list-last/bc is used by lls-fold-tail,
list-last/butlast-def is used by lls-unfold-tail, lls-fold-tail2,
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, lls-fold-tail2,
list-last/last-one is used by lls-fold-tail,
list-last/prefix-nil is used by lls-prefix-gen,
list-last/prefix-rec-03 is used by lls-prefix-gen,

Used from specification heapfuns

heapfuns/subset-refl is used by lls-prefix, lls-merge, lls-lasso-inj,
heapfuns/union-subset is used by lls-prefix-gen, lls-merge-gen, lls-lasso-inj-gen,

Used from specification maplet

maplet/at-rw is used by lls-fold-head, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
maplet/eq-objs is used by lls-unfold-tail, lls-to-ls, lls-lasso-inj, lls-injective, lls-fold-tail, lls-consecutive,
maplet/ex is used by ls-split, ls-lls-last, ls-lls, lls-unfold-tail, lls-split, lls-prefix-gen, lls-one, lls-null, lls-merge-gen, lls-lasso-inj,
maplet/ex1-shift is used by lls-unfold-tail, lls-unfold-head, lls-to-ls, lls-split, lls-merge-gen, lls-lasso-inj-gen, lls-injective, lls-fold-tail, lls-fold-head, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
maplet/map-null is used by lls-null,
maplet/map-same is used by lls-lasso-inj-gen,
maplet/maplet-unique is used by lls-prefix-gen, lls-lasso-inj-gen,
maplet/precise-map is used by lls-merge-gen,

Used from specification linked-list

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

Used from specification list-data

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

Used from specification heap-sep

heap-sep/Eq-P is used by lls-to-ls,
heap-sep/sep is used by ls-lls, lls-split, lls-prefix-gen, lls-merge-gen, lls-lasso-inj-gen,
heap-sep/And-inj is used by lls-null,
heap-sep/and is used by ls-lls, lls-unfold-tail, lls-to-ls, lls-split, lls-prefix-gen, lls-one, lls-merge-gen, lls-lasso-inj-gen, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-end, ll-trav1-end,
heap-sep/and-ass is used by ls-lls, lls-unfold-tail, lls-unfold-head-simp, lls-to-ls, lls-split, lls-prefix-gen, lls-one, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-init, ll-trav1-end,
heap-sep/and-com is used by ls-lls, lls-unfold-tail, lls-unfold-head-simp, lls-to-ls, lls-split, lls-prefix-gen, lls-one, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-init, ll-trav1-end,
heap-sep/emp is used by ls-lls, lls-prefix-gen,
heap-sep/emp-sep is used by lls-unfold-tail, lls-to-ls, lls-split, lls-one, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-init, ll-trav1-end,
heap-sep/false-and is used by lls-unfold-head-simp, lls-null, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
heap-sep/false-rev is used by lls-unfold-head-simp, lls-one, lls-null, lls-injective, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
heap-sep/false-sep is used by lls-unfold-head-simp, lls-null, lls-lasso-inj-gen, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
heap-sep/falseH is used by lls-unfold-head-simp, lls-one, lls-null, lls-lasso-inj-gen, lls-injective, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
heap-sep/precise-split-l is used by lls-merge-gen,
heap-sep/prop is used by ls-lls, lls-unfold-tail, lls-to-ls, lls-split, lls-prefix-gen, lls-one, lls-merge-gen, lls-lasso-inj-gen, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-end, ll-trav1-end,
heap-sep/prop-shift is used by lls-unfold-tail, lls-to-ls, lls-split, lls-one, lls-merge-gen, lls-lasso-inj-gen, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-end, ll-trav1-end,
heap-sep/sep-ass is used by ls-lls, lls-unfold-tail, lls-unfold-head-simp, lls-unfold-head, lls-to-ls, lls-split, lls-one, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail2, lls-fold-tail, lls-fold-head, lls-consecutive, ll-trav2-next, ll-trav2-init, ll-trav2-end, ll-trav1-next, ll-trav1-init, ll-trav1-end,
heap-sep/sep-com is used by ls-lls, lls-unfold-tail, lls-unfold-head-simp, lls-unfold-head, lls-to-ls, lls-split, lls-one, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail2, lls-fold-tail, lls-fold-head, lls-consecutive, ll-trav2-next, ll-trav2-init, ll-trav2-end, ll-trav1-next, ll-trav1-init, ll-trav1-end,
heap-sep/split-union is used by lls-split, lls-lasso-inj-gen,
heap-sep/true-and is used by ls-lls, lls-to-ls, lls-null, lls-lasso-inj, ll-trav2-next, ll-trav2-end, ll-trav1-init, ll-trav1-end,
heap-sep/true-rev is used by ls-lls, lls-to-ls, lls-null, lls-lasso-inj, ll-trav2-next, ll-trav2-end, ll-trav1-init, ll-trav1-end,

Used from specification cell

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

Used from specification list

list/One is used by lls-one,
list/c is used by lls-one,
list/c-06 is used by lls-lasso-inj-gen,
list/Last is used by lls-lasso-inj-gen, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
list/Nil is used by lls-unfold-tail, lls-split, lls-merge-gen, lls-consecutive, ll-trav2-next, ll-trav1-init,
list/a is used by ls-split, ls-lls-last, ls-lls, lls-unfold-tail, lls-unfold-head-simp, lls-unfold-head, lls-to-ls, lls-split, lls-prefix-gen, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail2, lls-fold-tail, lls-fold-head, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-init, ll-trav1-end,
list/app is used by lls-fold-tail, ll-trav2-end, ll-trav1-end,
list/app-02 is used by lls-unfold-tail, lls-unfold-head-simp, lls-unfold-head, lls-null, lls-lasso-inj-gen, lls-lasso-inj, lls-fold-tail2, lls-fold-tail, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
list/c is used by ls-lls, lls-unfold-tail, lls-unfold-head, lls-to-ls, lls-split, lls-prefix-gen, lls-null, lls-merge-gen, lls-lasso-inj-gen, lls-lasso-inj, lls-injective, lls-fold-tail, lls-consecutive, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
list/c-04 is used by ll-trav2-next,
list/c-06 is used by lls-unfold-head, lls-lasso-inj,
list/e is used by lls-unfold-tail, lls-unfold-head-simp, lls-unfold-head, lls-null, lls-lasso-inj-gen, lls-lasso-inj, lls-fold-tail2, lls-fold-tail, ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
list/len-01 is used by ll-trav2-next, ll-trav1-next,
list/len-06 is used by ll-trav2-next, ll-trav2-end, ll-trav1-end,

Used from specification separation

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