[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
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-split-last,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list-last/splitlasteq
is used by
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- 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-aux2,
rem-stays-reachable-aux1,
- list-last/butlast-last
is used by
rem-stays-reachable-aux1,
- list-last/butlast-one
is used by
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- list-last/butlast-rec
is used by
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- list-last/l-02
is used by
reachable-addnew-rev,
reachable-split-first,
reachable-addnew,
null-not-reachable,
reach-n-path-n,
rem-stays-reachable-aux2,
frommodified,
path-last,
add-preserves-reachable-rev,
fromnext-reachable,
reach-alloc,
linearity,
- list-last/l-in
is used by
reachable-addnew-rev,
reachable-nodups-def,
rem-stays-reachable-aux2,
- list-last/lapp
is used by
k-reachable-def,
- list-last/lapp-01
is used by
reachable-addnew-rev,
reachable-nodups-def,
rem-stays-reachable-aux2,
k-reachable-def,
rem-stays-reachable-aux1,
- list-last/lapp-02
is used by
frommodified,
- list-last/lapp-03
is used by
reachable-addnew-rev,
add-preserves-reachable,
rem-stays-reachable-aux2,
rem-reachable-rev,
- list-last/last-01
is used by
rem-stays-reachable-aux,
rem-stays-reachable-aux2,
reach-reachnext,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list-last/last-def
is used by
reachable-addnew-rev,
reachnext,
reach-n-path-n,
frommodified,
k-reachable-def,
add-preserves-reachable-rev,
acyclic-rem-not-reachable,
- list-last/last-elim
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-split-last,
rem-stays-reachable-aux2,
linearity,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list-last/last-one
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
self-reachable,
reachable-split-last,
reachnext,
reachable-split-first,
reachable-addnew,
add-preserves-reachable,
id-reachable,
null-not-reachable,
reachable-trans,
path-last-nxt,
rem-reachable,
rem-stays-reachable-aux2,
frommodified,
path-trans,
k-reachable-def,
path-last,
add-preserves-reachable-rev,
reach-reachnext,
fromnext-reachable,
path-split-last,
reach-alloc,
rem-reachable-rev,
modnotreachable-reachable-rev,
linearity,
reachable-addnewtonull-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
modified-stays-reachable,
- list-last/last-rec
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
self-reachable,
reachnext,
add-preserves-reachable,
id-reachable,
reachable-trans,
reach-n-path-n,
path-last-nxt,
rem-reachable,
rem-stays-reachable-aux2,
frommodified,
path-trans,
add-preserves-reachable-rev,
reach-reachnext,
fromnext-reachable-rev,
path-split-last,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-addnewtonull-rev,
reachable-modbehind,
rem-stays-reachable-aux1,
modified-stays-reachable,
- list-last/last-sizeone
is used by
reach-n-path-n,
- list-last/lin-01
is used by
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- 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
reachable-nodups-def,
acyclic-rem-not-reachable,
- list-dup/e-01
is used by
rem-stays-reachable-aux,
reachable-nodups-def,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list-dup/f
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list-dup/f-01
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list-dup/l-03
is used by
rem-stays-reachable-aux2,
- list-dup/rec
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
Used from specification list-data
Used from specification store
- store/At-other
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
changenonnxt-reachable,
add-preserves-reachable,
rem-reachable,
add-preserves-reachable-rev,
modnotreachable-reachable,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-addnewtonull-rev,
reachable-modbehind,
- store/In-insert
is used by
reachable-addnew-rev,
- store/At-in-out
is used by
reachable-addnew-rev,
reachable-addnew,
path-new-irrelevant-strong,
reachable-addnewtonull-rev,
- store/At-other
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
path-modify-strong,
add-preserves-reachable,
frommodified,
path-modify,
modified-stays-reachable,
- store/At-same
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
changenonnxt-reachable,
add-preserves-reachable,
rem-reachable,
removed-stays-reachable,
frommodified,
add-preserves-reachable-rev,
changenonnxt-reachable-rev,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-addnewtonull-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
- store/Del-at
is used by
path-delnonmember,
- store/Del-in
is used by
path-delnonmember,
- store/In-insert
is used by
reachable-addnew-rev,
path-modify-strong,
changenonnxt-reachable,
reachable-addnew,
add-preserves-reachable,
rem-reachable,
path-new-irrelevant-strong,
removed-stays-reachable,
add-preserves-reachable-rev,
modnotreachable-reachable,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-addnewtonull-rev,
reachable-modbehind,
modified-stays-reachable,
- store/in-neq
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
path-modify-strong,
changenonnxt-reachable,
add-preserves-reachable,
frommodified,
path-modify,
add-preserves-reachable-rev,
modnotreachable-reachable,
modnotreachable-reachable-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
- store/ins-same-01
is used by
modified-stays-reachable-rev,
changenonnxt-reachable-rev,
- store/insin
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
changenonnxt-reachable,
add-preserves-reachable,
removed-stays-reachable,
frommodified,
add-preserves-reachable-rev,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
modified-stays-reachable,
- store/insins
is used by
modified-stays-reachable-rev,
changenonnxt-reachable-rev,
- store/k-At-same
is used by
rem-stays-reachable-aux,
add-preserves-reachable-rev,
- store/notmemlookup
is used by
modified-stays-reachable,
Used from specification nat-basic
- nat-basic/a
is used by
reachable-n-rec-strong2,
reach-n-path-n,
reachable-n-trans,
k-reachable-def,
reachable-n-rec2,
reachable-n-rec-rev,
k-path,
reach-n-unique,
reach-n-split,
linearity,
reachable-n-rec-rev2,
- nat-basic/c
is used by
reachable-n-rec-strong2,
reach-n-path-n,
reachable-n-trans,
k-reachable-def,
reachable-n-rec2,
reachable-n-rec-rev,
k-path,
reach-n-unique,
reach-n-split,
linearity,
reachable-n-rec-rev2,
- 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
reachable-n-rec-rev,
linearity,
- nat-basic/s-04
is used by
linearity,
- nat-basic/succ
is used by
reach-n-path-n,
reachable-n-trans,
k-reachable-def,
reach-n-unique,
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
reachable-addnew-rev,
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- list/lastoc-rew
is used by
reachable-nodups-def,
acyclic-rem-not-reachable,
- list/Last
is used by
rem-stays-reachable-aux,
reach-reachnext,
acyclic-rem-not-reachable,
- list/Nil
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
path-modify-strong,
path-postfix,
path-butlast,
path-last-nxt,
rem-stays-reachable-aux2,
path-trans,
path-prefix,
path-last-not-null,
linearity-path,
reach-reachnext,
path-split-last,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/a
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
self-reachable,
path-modify-strong,
reachable-split-last,
path-postfix,
reachnext,
reachable-split-first,
changenonnxt-reachable,
reachable-addnew,
add-preserves-reachable,
id-reachable,
notnull-reachable,
path-butlast,
null-not-reachable,
reachable-trans,
startnotinH-notreachable,
reach-n-path-n,
path-last-nxt,
path-first-in-H,
rem-reachable,
path-new-irrelevant-strong,
rem-stays-reachable-aux2,
removed-stays-reachable,
frommodified,
path-trans,
path-prefix,
path-modify,
path-last-not-null,
null-not-start-of-path,
k-reachable-def,
path-delnonmember,
path-last,
k-path,
add-preserves-reachable-rev,
linearity-path,
reach-reachnext,
fromnext-reachable,
modnotreachable-reachable,
fromnext-reachable-rev,
path-split-last,
reach-alloc,
rem-reachable-rev,
path-prelast,
modnotreachable-reachable-rev,
linearity,
reachable-addnewtonull-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
modified-stays-reachable,
- list/app
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
self-reachable,
reachable-split-last,
reachnext,
reachable-split-first,
changenonnxt-reachable,
reachable-addnew,
add-preserves-reachable,
id-reachable,
path-butlast,
null-not-reachable,
reachable-trans,
startnotinH-notreachable,
reach-n-path-n,
path-last-nxt,
path-first-in-H,
rem-reachable,
path-new-irrelevant-strong,
rem-stays-reachable-aux2,
frommodified,
path-trans,
path-prefix,
path-modify,
null-not-start-of-path,
k-reachable-def,
path-delnonmember,
path-last,
k-path,
add-preserves-reachable-rev,
linearity-path,
reach-reachnext,
fromnext-reachable,
modnotreachable-reachable,
path-split-last,
reach-alloc,
rem-reachable-rev,
modnotreachable-reachable-rev,
linearity,
reachable-addnewtonull-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
modified-stays-reachable,
- list/app-01
is used by
acyclic-rem-not-reachable,
- list/app-02
is used by
rem-stays-reachable-aux2,
rem-stays-reachable-aux1,
- list/app-03
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list/app-04
is used by
linearity-path,
acyclic-rem-not-reachable,
- list/app-06
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/c
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
self-reachable,
path-modify-strong,
path-postfix,
reachnext,
reachable-split-first,
changenonnxt-reachable,
reachable-addnew,
add-preserves-reachable,
id-reachable,
path-butlast,
null-not-reachable,
reachable-trans,
startnotinH-notreachable,
reach-n-path-n,
path-last-nxt,
path-first-in-H,
rem-reachable,
path-new-irrelevant-strong,
rem-stays-reachable-aux2,
frommodified,
path-trans,
path-prefix,
path-modify,
path-last-not-null,
null-not-start-of-path,
k-reachable-def,
path-delnonmember,
path-last,
k-path,
add-preserves-reachable-rev,
linearity-path,
reach-reachnext,
fromnext-reachable,
modnotreachable-reachable,
path-split-last,
reach-alloc,
rem-reachable-rev,
modnotreachable-reachable-rev,
reachable-addnewtonull-rev,
reachable-modbehind,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
modified-stays-reachable,
- list/c-03
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list/c-06
is used by
linearity-path,
acyclic-rem-not-reachable,
- 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
reachable-split-first,
reachable-addnew,
null-not-reachable,
startnotinH-notreachable,
reach-n-path-n,
rem-stays-reachable-aux2,
k-reachable-def,
path-last,
k-path,
linearity-path,
fromnext-reachable,
reach-alloc,
rem-stays-reachable-aux1,
- list/e-02
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-split-last,
rem-stays-reachable-aux2,
linearity,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/e-03
is used by
rem-stays-reachable-aux2,
linearity-path,
rem-stays-reachable-aux1,
- list/eq-04
is used by
rem-stays-reachable-aux2,
- list/in-01
is used by
rem-stays-reachable-aux,
reachable-nodups-def,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-06
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
path-modify-strong,
path-new-irrelevant-strong,
rem-stays-reachable-aux2,
path-modify,
path-delnonmember,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-14
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list/in-15
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-16
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list/in-17
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
path-modify-strong,
rem-stays-reachable-aux2,
path-modify,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-append
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
path-modify-strong,
rem-stays-reachable-aux2,
path-modify,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-empty
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
path-modify-strong,
path-new-irrelevant-strong,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/in-rec
is used by
reachable-addnew-rev,
rem-stays-reachable-aux,
reachable-nodups-def,
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,
- list/inapp
is used by
rem-stays-reachable-aux2,
- list/inapp-14
is used by
rem-stays-reachable-aux2,
- list/inex
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
- list/len
is used by
reach-n-path-n,
k-path,
linearity,
- list/len-01
is used by
linearity-path,
- list/len-02
is used by
reach-n-path-n,
k-path,
linearity,
- list/neq-03
is used by
rem-stays-reachable-aux2,
acyclic-rem-not-reachable,
rem-stays-reachable-aux1,