[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 dlls-last-fold-tail,
list-last/butlast-def is used by dlls-unfold-tail,
list-last/butlast-one is used by dlls-last-fold-tail,
list-last/l-02 is used by dlls-last-fold-tail,
list-last/last-def is used by dlls-unfold-tail,
list-last/last-one is used by dlls-last-fold-tail,

Used from specification map-sep

map-sep/And-inj is used by dlls-to-dll-prev, dlls-last-head-null, dlls-null,
map-sep/and is used by dlls-last-one, dlls-last-fold-tail, dlls-one, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail,
map-sep/and-ass is used by dlls-last-one, dlls-last-unfold-head-simp, dll-trav-next, dlls-last-fold-tail, dlls-one, dlls-to-dll-prev, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
map-sep/and-com is used by dlls-last-one, dlls-last-unfold-head-simp, dll-trav-next, dlls-last-fold-tail, dlls-one, dlls-to-dll-prev, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
map-sep/emp-sep is used by dlls-last-one, dll-trav-next, dlls-last-fold-tail, dlls-one, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail,
map-sep/false-and is used by dlls-last-unfold-head-simp, dll-trav-next, dlls-last-head-null, dll-trav-end, dlls-null, dlls-unfold-head-simp,
map-sep/false-rev is used by dlls-last-one, dlls-last-unfold-head-simp, dll-trav-next, dlls-one, dlls-last-head-null, dll-trav-end, dlls-null, dlls-unfold-head-simp,
map-sep/false-sep is used by dlls-last-unfold-head-simp, dll-trav-next, dlls-last-head-null, dll-trav-end, dlls-null, dlls-unfold-head-simp,
map-sep/falseH is used by dlls-last-one, dlls-last-unfold-head-simp, dll-trav-next, dlls-one, dlls-last-head-null, dll-trav-end, dlls-null, dlls-unfold-head-simp,
map-sep/prop is used by dlls-last-one, dlls-last-fold-tail, dlls-one, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail,
map-sep/prop-shift is used by dlls-last-one, dlls-last-fold-tail, dlls-one, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail,
map-sep/sep-ass is used by dlls-last-one, dlls-last-unfold-head-simp, dlls-fold-head, dll-trav-next, dlls-last-fold-head, dlls-unfold-head, dlls-last-fold-tail, dlls-last-unfold-head, dlls-one, dll-trav-init, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
map-sep/sep-com is used by dlls-last-one, dlls-last-unfold-head-simp, dlls-fold-head, dll-trav-next, dlls-last-fold-head, dlls-unfold-head, dlls-last-fold-tail, dlls-last-unfold-head, dlls-one, dll-trav-init, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
map-sep/true-and is used by dlls-last-one, dll-trav-next, dlls-last-fold-tail, dlls-last-head-null, dll-trav-end, dlls-unfold-tail, dlls-null,
map-sep/true-rev is used by dlls-last-one, dll-trav-next, dlls-last-fold-tail, dlls-last-head-null, dll-trav-end, dlls-unfold-tail, dlls-null,

Used from specification node

node/elim-mknode is used by dlls-fold-head, dlls-last-fold-head,
node/inj-mknode is used by dlls-fold-head, dll-trav-next, dlls-last-fold-head, dll-trav-end,

Used from specification refmap-maplet

refmap-maplet/at-rw is used by dlls-fold-head, dll-trav-next, dlls-last-fold-head, dll-trav-end,
refmap-maplet/eq-objs is used by dlls-last-fold-tail, dlls-last-consecutive, dlls-unfold-tail,
refmap-maplet/ex is used by dlls-last-one, dlls-one, dlls-to-dll-prev, dlls-last-head-null, dlls-unfold-tail, dlls-null,
refmap-maplet/ex1-shift is used by dlls-last-unfold-head-simp, dlls-fold-head, dll-trav-next, dlls-last-fold-head, dlls-unfold-head, dlls-last-fold-tail, dlls-last-unfold-head, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-unfold-head-simp,
refmap-maplet/map-null is used by dll-trav-next, dlls-last-head-null, dlls-null,

Used from specification list-data

list-data/elim-list-c is used by dll-trav-next,

Used from specification list

list/elim-first is used by dlls-unfold-head, dlls-last-unfold-head,
list/Last is used by dll-trav-next, dll-trav-end,
list/Nil is used by dll-trav-next, dlls-last-consecutive, dlls-unfold-tail,
list/a is used by dlls-last-one, dlls-last-unfold-head-simp, dlls-fold-head, dll-trav-next, dlls-last-fold-head, dlls-unfold-head, dlls-last-fold-tail, dlls-last-unfold-head, dlls-one, dlls-to-dll-prev, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
list/app is used by dlls-last-one, dlls-last-fold-tail, dlls-one, dll-trav-end,
list/app-02 is used by dlls-last-unfold-head-simp, dll-trav-next, dlls-last-fold-tail, dlls-last-head-null, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
list/c is used by dlls-last-unfold-head-simp, dll-trav-next, dlls-last-fold-tail, dlls-to-dll-prev, dlls-last-head-null, dlls-last-consecutive, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
list/c-06 is used by dlls-last-unfold-head-simp, dlls-unfold-head, dlls-last-unfold-head, dlls-unfold-head-simp,
list/e is used by dlls-last-unfold-head-simp, dll-trav-next, dlls-last-fold-tail, dlls-last-head-null, dll-trav-end, dlls-unfold-tail, dlls-null, dlls-unfold-head-simp,
list/len-01 is used by dll-trav-next,
list/len-06 is used by dll-trav-end,

Used from specification dlinked-maplist

dlinked-maplist/dll is used by dlls-to-dll,
dlinked-maplist/dll-base is used by dlls-to-dll-prev,
dlinked-maplist/dll-rec is used by dlls-to-dll-prev,

Used from specification refmap-separation

refmap-separation/True is used by dlls-fold-head, dlls-last-fold-head,