[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 nat-basic

nat-basic/a is used by reachable-n-trans, reachable-n-rec2, reachable-n-rec-strong2, reachable-n-rec-rev2, reachable-n-rec-rev, reach-n-unique, reach-n-split, reach-n-path-n, linearity, k-reachable-def, k-path,
nat-basic/c is used by reachable-n-trans, reachable-n-rec2, reachable-n-rec-strong2, reachable-n-rec-rev2, reachable-n-rec-rev, reach-n-unique, reach-n-split, reach-n-path-n, linearity, k-reachable-def, k-path,
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/ref is used by reachable-n-rec-rev, linearity,
nat-basic/s-04 is used by linearity,
nat-basic/succ is used by reachable-n-trans, reach-n-unique, reach-n-split, reach-n-path-n, k-reachable-def,
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 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 store

store/linheap/At-other is used by rem-stays-reachable-aux, rem-reachable-rev-weak, rem-reachable, reachable-modbehind, reachable-addnewtonull-rev, reachable-addnew-rev, modnotreachable-reachable-rev-weak, modnotreachable-reachable-rev, modnotreachable-reachable, modified-stays-reachable, changenonnxt-reachable, add-preserves-reachable-rev, add-preserves-reachable,
store/linheap/In-insert is used by reachable-addnew-rev,
store/linheap/At-in-out is used by reachable-addnewtonull-rev, reachable-addnew-rev, reachable-addnew, path-new-irrelevant-strong,
store/linheap/At-other is used by rem-stays-reachable-aux, reachable-addnew-rev, path-modify-strong, path-modify, frommodified, add-preserves-reachable,
store/linheap/At-same is used by removed-stays-reachable, rem-stays-reachable-aux, rem-reachable-rev-weak, rem-reachable, reachable-modbehind, reachable-addnewtonull-rev, reachable-addnew-rev, modnotreachable-reachable-rev-weak, modnotreachable-reachable-rev, modified-stays-reachable, frommodified, changenonnxt-reachable-rev, changenonnxt-reachable, add-preserves-reachable-rev, add-preserves-reachable, acyclic-rem-not-reachable,
store/linheap/Del-at is used by path-delnonmember,
store/linheap/Del-in is used by path-delnonmember,
store/linheap/In-insert is used by removed-stays-reachable, rem-reachable-rev-weak, rem-reachable, reachable-modbehind, reachable-addnewtonull-rev, reachable-addnew-rev, reachable-addnew, path-new-irrelevant-strong, path-modify-strong, modnotreachable-reachable-rev-weak, modnotreachable-reachable-rev, modnotreachable-reachable, modified-stays-reachable, changenonnxt-reachable, add-preserves-reachable-rev, add-preserves-reachable,
store/linheap/in-neq is used by rem-stays-reachable-aux, reachable-modbehind, reachable-addnew-rev, path-modify-strong, path-modify, modnotreachable-reachable-rev, frommodified, add-preserves-reachable-rev, acyclic-rem-not-reachable,
store/linheap/ins-same-01 is used by modified-stays-reachable-rev, changenonnxt-reachable-rev,
store/linheap/insin is used by removed-stays-reachable, rem-stays-reachable-aux, rem-reachable-rev-weak, reachable-modbehind, reachable-addnew-rev, modnotreachable-reachable-rev-weak, modnotreachable-reachable-rev, frommodified, add-preserves-reachable-rev, acyclic-rem-not-reachable,
store/linheap/insins is used by modified-stays-reachable-rev, changenonnxt-reachable-rev,
store/linheap/k-At-same is used by rem-stays-reachable-aux, add-preserves-reachable-rev,
store/linheap/notmemlookup is used by modified-stays-reachable,

Used from specification list-last

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

Used from specification list-data

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

Used from specification list

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

Used from specification list-dup

list-dup/reflist/a is used by rem-stays-reachable-aux2, rem-stays-reachable-aux1, rem-stays-reachable-aux, reachable-nodups-def, reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/c-02 is used by reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/dups-cons is used by rem-stays-reachable-aux2, rem-stays-reachable-aux1, rem-stays-reachable-aux, reachable-nodups-def, reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/e-01 is used by rem-stays-reachable-aux2, rem-stays-reachable-aux1, rem-stays-reachable-aux, reachable-nodups-def, reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/f is used by rem-stays-reachable-aux2, rem-stays-reachable-aux1, rem-stays-reachable-aux, reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/f-01 is used by rem-stays-reachable-aux2, rem-stays-reachable-aux1, rem-stays-reachable-aux, reachable-nodups-def, reachable-addnew-rev, acyclic-rem-not-reachable,
list-dup/reflist/rec is used by reachable-nodups-def,