[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 store
- store/node-index/At-other
is used by
put-le,
put-gt,
drop-le,
drop-gt,
- store/node-index/k-Extension
is used by
restrict-norm,
restrict-le4,
restrict-le3,
restrict-le2,
restrict-le1,
restrict-gt4,
restrict-gt3,
restrict-gt2,
restrict-gt1,
put-le,
put-gt,
le-emp,
gt-emp,
drop-le,
drop-gt,
deln-le,
deln-gt,
del-le,
del-gt,
- store/node-index/At-other
is used by
put-le,
put-gt,
- store/node-index/At-same
is used by
put-le,
put-gt,
- store/node-index/Del-at
is used by
del-le,
del-gt,
- store/node-index/Del-at-strong
is used by
deln-le,
deln-gt,
- store/node-index/Del-in
is used by
deln-le,
deln-gt,
del-le,
del-gt,
- store/node-index/In-empty
is used by
le-emp,
gt-emp,
- store/node-index/In-insert
is used by
drop-le,
drop-gt,
- store/node-index/in-neq
is used by
put-le,
put-gt,
drop-le,
drop-gt,
- store/node-index/insin
is used by
put-le,
put-gt,
drop-le,
drop-gt,
Used from specification oelem
- oelem/key-order/irreflexivity
is used by
at-le-lt,
- oelem/key-order/ls-le
is used by
restrict-le2,
restrict-le1,
- oelem/key-order/nll
is used by
restrict-le4,
restrict-le3,
restrict-le2,
restrict-le1,
restrict-gt4,
restrict-gt3,
restrict-gt2,
restrict-gt1,
deln-le,
deln-gt,
- oelem/key-order/nnn
is used by
restrict-le4,
restrict-le3,
restrict-gt4,
restrict-gt3,
- oelem/key-order/transitivity
is used by
restrict-le2,
restrict-le1,
restrict-gt2,
restrict-gt1,
at-le-lt,