[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

nat/elim-pred-c is used by insert-rec-correct, insert-correct,
nat/lels is used by less, inv-reduce, hash-given, at-put,
nat/ls-le-simp is used by less, inv-reduce, hash-given, at-put,
nat/pred-03 is used by insert-rec-correct, insert-correct,

Used from specification set-basic

set-basic/Extension is used by insert-rec-correct, insert-correct, abs-sym,
set-basic/eq-03 is used by insert-correct,
set-basic/rax is used by insert-rec-correct, insert-correct,

Used from specification slot

slot/disj is used by insert-rec-correct, insert-correct, disj-reduce, disj-neq,
slot/elim is used by insert-rec-correct, insert-correct, disj-reduce,
slot/inj is used by insert-rec-correct, insert-correct,
slot/sel is used by insert-rec-correct, insert-correct,
slot/upd is used by insert-correct,

Used from specification nat-basic2

nat-basic2/a is used by insert-rec-correct, insert-correct,
nat-basic2/c is used by insert-rec-correct, insert-correct,
nat-basic2/oz is used by insert-rec-correct, insert-correct,
nat-basic2/s is used by insert-rec-correct, insert-correct,

Used from specification nat-basic1

nat-basic1/f is used by inv-reduce, insert-rec-correct, insert-correct, hash-same, disj-reduce, disj-neq,
nat-basic1/lf-01 is used by inv-reduce, hash-same,
nat-basic1/lf-02 is used by insert-correct,
nat-basic1/ref-1 is used by insert-rec-correct, insert-correct,

Used from specification array

array/table/Put-same is used by at-put,
array/table/Put-other is used by insert-rec-correct, insert-correct, at-put,
array/table/Size-put is used by insert-rec-correct, insert-correct,
array/table/cngetput is used by insert-rec-correct,