[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,
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 map-sep

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

Used from specification linked-maplist

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

Used from specification refmap-maplet

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

Used from specification list-data

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

Used from specification cell

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

Used from specification list

list/One is used by lls-one,
list/c is used by lls-one,
list/Last is used by ll-trav2-next, ll-trav2-end, ll-trav1-next, ll-trav1-end,
list/Nil is used by ll-trav2-next, lls-consecutive, ll-trav1-init, lls-unfold-tail,
list/a is used by lls-unfold-head-simp, lls-unfold-head, lls-fold-tail, lls-to-ls, ll-trav2-next, ll-trav2-end, lls-consecutive, lls-null, ll-trav1-init, ll-trav1-next, lls-fold-head, lls-unfold-tail, 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-head-simp, lls-unfold-head, lls-fold-tail, ll-trav2-next, ll-trav2-end, lls-null, ll-trav1-next, lls-unfold-tail, ll-trav1-end,
list/c is used by lls-unfold-head, lls-fold-tail, lls-to-ls, ll-trav2-next, ll-trav2-end, lls-consecutive, lls-null, ll-trav1-next, lls-unfold-tail, ll-trav1-end,
list/c-04 is used by ll-trav2-next,
list/c-06 is used by lls-unfold-head,
list/e is used by lls-unfold-head-simp, lls-unfold-head, lls-fold-tail, ll-trav2-next, ll-trav2-end, lls-null, ll-trav1-next, lls-unfold-tail, 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 refmap-separation

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