[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/bapp is used by rem-stays-reachable-aux2,
list-last/lapp is used by acyclic-rem-not-reachable, reachable-split-last, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list-last/splitlasteq is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list-last/splitlasteq-01 is used by rem-stays-reachable-aux2,
list-last/bc is used by rem-stays-reachable-aux1,
list-last/bin is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list-last/butlast-last is used by rem-stays-reachable-aux1,
list-last/butlast-one is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list-last/butlast-rec is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list-last/l-02 is used by reach-alloc, reach-n-path-n, linearity, reachable-addnew, rem-stays-reachable-aux2, fromnext-reachable, reachable-addnew-rev, null-not-reachable, frommodified, reachable-split-first, path-last, add-preserves-reachable-rev,
list-last/l-in is used by reachable-nodups-def, rem-stays-reachable-aux2, reachable-addnew-rev,
list-last/lapp is used by k-reachable-def,
list-last/lapp-01 is used by reachable-nodups-def, rem-stays-reachable-aux1, rem-stays-reachable-aux2, k-reachable-def, reachable-addnew-rev,
list-last/lapp-02 is used by frommodified,
list-last/lapp-03 is used by rem-reachable-rev, add-preserves-reachable, rem-stays-reachable-aux2, reachable-addnew-rev,
list-last/last-01 is used by acyclic-rem-not-reachable, reach-reachnext, rem-stays-reachable-aux1, rem-stays-reachable-aux2, rem-stays-reachable-aux,
list-last/last-def is used by acyclic-rem-not-reachable, reach-n-path-n, k-reachable-def, reachable-addnew-rev, frommodified, reachnext, add-preserves-reachable-rev,
list-last/last-elim is used by acyclic-rem-not-reachable, reachable-split-last, linearity, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list-last/last-one is used by modnotreachable-reachable-rev, rem-reachable-rev, reach-alloc, acyclic-rem-not-reachable, reachable-modbehind, reachable-split-last, id-reachable, linearity, add-preserves-reachable, reachable-nodups-def, reachable-addnew, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, reachable-addnewtonull-rev, rem-stays-reachable-aux2, k-reachable-def, rem-reachable, fromnext-reachable, self-reachable, reachable-addnew-rev, modified-stays-reachable, path-split-last, null-not-reachable, rem-stays-reachable-aux, reachable-trans, frommodified, reachnext, reachable-split-first, path-last, path-trans, add-preserves-reachable-rev,
list-last/last-rec is used by modnotreachable-reachable-rev, rem-reachable-rev, reachable-modbehind, reach-n-path-n, id-reachable, add-preserves-reachable, reachable-nodups-def, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, reachable-addnewtonull-rev, rem-stays-reachable-aux2, rem-reachable, self-reachable, fromnext-reachable-rev, reachable-addnew-rev, modified-stays-reachable, path-split-last, rem-stays-reachable-aux, reachable-trans, frommodified, reachnext, path-trans, add-preserves-reachable-rev,
list-last/last-sizeone is used by reach-n-path-n,
list-last/lin-01 is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list-last/lin-02 is used by rem-stays-reachable-aux2,
list-last/lthree is used by rem-stays-reachable-aux2,

Used from specification nat

nat/add-num-01 is used by reach-n-path-n,
nat/add-num-03 is used by reach-n-path-n, k-path,
nat/add-num-04 is used by reach-n-path-n, k-path,
nat/anti is used by reach-n-split-le,
nat/elim-sub is used by reach-n-split,
nat/eq-01 is used by reachable-n-rec-rev,
nat/ge is used by reach-n-path-n, k-path,
nat/le-def is used by reachable-n-rec-rev,
nat/le-num-04 is used by reach-n-path-n,
nat/lels is used by reach-n-split-le,
nat/lels-03 is used by reach-n-split,
nat/lep is used by reach-n-path-n, k-path,
nat/ler is used by reach-n-split-le,
nat/succ-02 is used by reachable-n-rec-rev,
nat/zero is used by reach-n-split-le,

Used from specification list-dup

list-dup/a is used by acyclic-rem-not-reachable, reachable-nodups-def,
list-dup/e-01 is used by acyclic-rem-not-reachable, reachable-nodups-def, rem-stays-reachable-aux2, rem-stays-reachable-aux,
list-dup/f is used by acyclic-rem-not-reachable, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list-dup/f-01 is used by acyclic-rem-not-reachable, reachable-nodups-def, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list-dup/l-03 is used by rem-stays-reachable-aux2,
list-dup/rec is used by acyclic-rem-not-reachable, reachable-nodups-def, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,

Used from specification list-data

list-data/elim-list-c is used by reach-n-path-n, k-path,
list-data/l is used by reach-n-path-n, k-path,
list-data/size-nil is used by reach-n-path-n, k-path,

Used from specification nat-basic

nat-basic/a is used by reach-n-path-n, reachable-n-rec-rev2, linearity, reachable-n-rec-strong2, k-reachable-def, reachable-n-rec2, reach-n-unique, reachable-n-trans, reachable-n-rec-rev, k-path, reach-n-split,
nat-basic/c is used by reach-n-path-n, reachable-n-rec-rev2, linearity, reachable-n-rec-strong2, k-reachable-def, reachable-n-rec2, reach-n-unique, reachable-n-trans, reachable-n-rec-rev, k-path, reach-n-split,
nat-basic/l-01 is used by reach-n-split,
nat-basic/one-06 is used by reach-n-path-n, k-path,
nat-basic/oz is used by reach-n-path-n, k-reachable-def,
nat-basic/refl-Nat is used by linearity, reachable-n-rec-rev,
nat-basic/s-04 is used by linearity,
nat-basic/succ is used by reach-n-path-n, k-reachable-def, reach-n-unique, reachable-n-trans, reach-n-split,
nat-basic/z-01 is used by reach-n-path-n,
nat-basic/z-02 is used by reachable-n-trans, reach-n-split,

Used from specification list

list/firstoc-rew is used by rem-stays-reachable-aux,
list/in-def is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev,
list/lastoc-rew is used by acyclic-rem-not-reachable, reachable-nodups-def,
list/Last is used by acyclic-rem-not-reachable, reach-reachnext, rem-stays-reachable-aux,
list/Nil is used by path-postfix, acyclic-rem-not-reachable, path-prefix, path-last-not-null, path-modify-strong, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, path-split-last, rem-stays-reachable-aux, linearity-path, path-butlast, path-trans,
list/a is used by removed-stays-reachable, modnotreachable-reachable-rev, rem-reachable-rev, path-postfix, reach-alloc, acyclic-rem-not-reachable, reachable-modbehind, reachable-split-last, reach-n-path-n, id-reachable, linearity, add-preserves-reachable, path-delnonmember, reachable-nodups-def, path-prefix, reachable-addnew, path-last-not-null, path-modify-strong, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, reachable-addnewtonull-rev, rem-stays-reachable-aux2, k-reachable-def, rem-reachable, path-modify, startnotinH-notreachable, fromnext-reachable, self-reachable, fromnext-reachable-rev, reachable-addnew-rev, modified-stays-reachable, path-new-irrelevant-strong, path-first-in-H, path-split-last, null-not-reachable, rem-stays-reachable-aux, modnotreachable-reachable, null-not-start-of-path, path-prelast, changenonnxt-reachable, reachable-trans, frommodified, reachnext, linearity-path, reachable-split-first, notnull-reachable, path-butlast, path-last, k-path, path-trans, add-preserves-reachable-rev,
list/app is used by modnotreachable-reachable-rev, rem-reachable-rev, reach-alloc, acyclic-rem-not-reachable, reachable-modbehind, reachable-split-last, reach-n-path-n, id-reachable, linearity, add-preserves-reachable, path-delnonmember, reachable-nodups-def, path-prefix, reachable-addnew, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, reachable-addnewtonull-rev, rem-stays-reachable-aux2, k-reachable-def, rem-reachable, path-modify, startnotinH-notreachable, fromnext-reachable, self-reachable, reachable-addnew-rev, modified-stays-reachable, path-new-irrelevant-strong, path-first-in-H, path-split-last, null-not-reachable, rem-stays-reachable-aux, modnotreachable-reachable, null-not-start-of-path, changenonnxt-reachable, reachable-trans, frommodified, reachnext, linearity-path, reachable-split-first, path-butlast, path-last, k-path, path-trans, add-preserves-reachable-rev,
list/app-01 is used by acyclic-rem-not-reachable,
list/app-02 is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list/app-03 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux2,
list/app-04 is used by acyclic-rem-not-reachable, linearity-path,
list/app-06 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list/c is used by modnotreachable-reachable-rev, rem-reachable-rev, path-postfix, reach-alloc, acyclic-rem-not-reachable, reachable-modbehind, reach-n-path-n, id-reachable, add-preserves-reachable, path-delnonmember, reachable-nodups-def, path-prefix, reachable-addnew, path-last-not-null, path-modify-strong, path-last-nxt, reach-reachnext, rem-stays-reachable-aux1, reachable-addnewtonull-rev, rem-stays-reachable-aux2, k-reachable-def, rem-reachable, path-modify, startnotinH-notreachable, fromnext-reachable, self-reachable, reachable-addnew-rev, modified-stays-reachable, path-new-irrelevant-strong, path-first-in-H, path-split-last, null-not-reachable, rem-stays-reachable-aux, modnotreachable-reachable, null-not-start-of-path, changenonnxt-reachable, reachable-trans, frommodified, reachnext, linearity-path, reachable-split-first, path-butlast, path-last, k-path, path-trans, add-preserves-reachable-rev,
list/c-03 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux2,
list/c-06 is used by acyclic-rem-not-reachable, linearity-path,
list/c-07 is used by reach-n-path-n,
list/c-08 is used by reach-n-path-n,
list/e is used by rem-stays-reachable-aux2,
list/e-01 is used by reach-alloc, reach-n-path-n, reachable-addnew, rem-stays-reachable-aux1, rem-stays-reachable-aux2, k-reachable-def, startnotinH-notreachable, fromnext-reachable, null-not-reachable, linearity-path, reachable-split-first, path-last, k-path,
list/e-02 is used by acyclic-rem-not-reachable, reachable-split-last, linearity, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list/e-03 is used by rem-stays-reachable-aux1, rem-stays-reachable-aux2, linearity-path,
list/eq-04 is used by rem-stays-reachable-aux2,
list/in-01 is used by acyclic-rem-not-reachable, reachable-nodups-def, rem-stays-reachable-aux1, rem-stays-reachable-aux2, rem-stays-reachable-aux,
list/in-06 is used by acyclic-rem-not-reachable, path-delnonmember, path-modify-strong, rem-stays-reachable-aux1, rem-stays-reachable-aux2, path-modify, reachable-addnew-rev, path-new-irrelevant-strong, rem-stays-reachable-aux,
list/in-14 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux2,
list/in-15 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux1, rem-stays-reachable-aux2,
list/in-16 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux2,
list/in-17 is used by acyclic-rem-not-reachable, path-modify-strong, rem-stays-reachable-aux1, rem-stays-reachable-aux2, path-modify, reachable-addnew-rev, rem-stays-reachable-aux,
list/in-append is used by acyclic-rem-not-reachable, reachable-nodups-def, path-modify-strong, rem-stays-reachable-aux1, rem-stays-reachable-aux2, path-modify, reachable-addnew-rev, rem-stays-reachable-aux,
list/in-empty is used by acyclic-rem-not-reachable, reachable-nodups-def, path-modify-strong, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, path-new-irrelevant-strong, rem-stays-reachable-aux,
list/in-rec is used by acyclic-rem-not-reachable, reachable-nodups-def, rem-stays-reachable-aux1, rem-stays-reachable-aux2, reachable-addnew-rev, rem-stays-reachable-aux,
list/inapp is used by rem-stays-reachable-aux2,
list/inapp-14 is used by rem-stays-reachable-aux2,
list/inex is used by acyclic-rem-not-reachable, rem-stays-reachable-aux2,
list/len is used by reach-n-path-n, linearity, k-path,
list/len-01 is used by linearity-path,
list/len-02 is used by reach-n-path-n, linearity, k-path,
list/neq-03 is used by acyclic-rem-not-reachable, rem-stays-reachable-aux1, rem-stays-reachable-aux2,

Used from specification map