[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 scan-strong, scan-min, scan-max-0, scan-max, scan-lt-0, scan-lt, scan-le-0, scan-le, scan-last, scan-given-0, scan-given, scan-entry-0, scan-entry, scan-branch-0, scan-branch, save-load-save, save-branches-last, load-branches-last, at-shr, at-shl, at-save-out-upper, at-save-out-lower, at-save-0, at-save, at-load-0, at-load,
nat-basic/add-base is used by scan-strong, scan-max-0, scan-max, scan-lt-0, scan-lt, scan-le-0, scan-le, scan-given-0, scan-entry-0, scan-entry, scan-branch-0, scan-branch, save-branches-last, load-branches-last, at-save-0, at-save, at-load-0, at-load,
nat-basic/c is used by scan-strong, scan-min, scan-max-0, scan-max, scan-lt-0, scan-lt, scan-le-0, scan-le, scan-last, scan-given-0, scan-given, scan-entry-0, scan-entry, scan-branch-0, scan-branch, save-load-save, save-branches-last, load-branches-last, at-shr, at-shl, at-save-out-upper, at-save-out-lower, at-save-0, at-save, at-load-0, at-load,
nat-basic/eq-01 is used by scan-given,
nat-basic/eq-02 is used by scan-entry, scan-branch, save-branches-last, load-branches-last, at-save, at-load,
nat-basic/f is used by scan-strong, scan-min-eq, scan-min, scan-max, scan-lt-0, scan-lt, scan-le-0, scan-le, scan-given-0, scan-given, scan-entry-0, scan-entry, scan-branch-0, scan-branch, save-load-save, at-shr, at-save-out-upper, at-save-out-lower, at-save-0, at-save, at-load-0, at-load,
nat-basic/l is used by scan-entry, scan-branch,
nat-basic/l-02 is used by scan-max, scan-lt, at-save, at-load,
nat-basic/lf is used by scan-strong, scan-entry, scan-branch, at-save-out-upper,
nat-basic/lf-01 is used by scan-strong,
nat-basic/lf-02 is used by scan-strong,
nat-basic/ls-02 is used by scan-strong, scan-min, scan-entry, scan-branch, at-save-out-lower,
nat-basic/oz is used by scan-entry, scan-branch, save-branches-last, load-branches-last, at-save, at-load,
nat-basic/ref is used by scan-min, scan-max, scan-le,
nat-basic/s-04 is used by scan-min, scan-le, scan-entry, scan-branch, at-shr, at-save-out-lower, at-save, at-load,
nat-basic/succ is used by scan-strong, scan-min, scan-max, scan-lt, scan-le, scan-last, scan-entry, scan-branch, save-size, save-branches-last, load-size, load-branches-last, at-save-out-upper, at-save-out-lower, at-save, at-load,
nat-basic/trans is used by scan-strong, scan-entry, scan-branch, at-save-out-upper,
nat-basic/z-01 is used by save-branches-last, load-branches-last,
nat-basic/zero-01 is used by scan-entry, scan-branch, at-save, at-load,

Used from specification zbranch

zbranch/disj-02 is used by load-branch-child,
zbranch/elim-01 is used by load-child,
zbranch/inj is used by load-branch-child,
zbranch/sel-02 is used by scan-given, load-save-key,
zbranch/sel-04 is used by scan-given, load-save-key,
zbranch/test-02 is used by load-save-branch,
zbranch/test-03 is used by load-save-branch,
zbranch/test-05 is used by load-save-entry,
zbranch/test-06 is used by load-save-entry,

Used from specification znode

znode/inj is used by load-properties,

Used from specification nat

nat/le-addex is used by save-load-save,
nat/cancel-01 is used by at-shr,
nat/eq-01 is used by at-shl,
nat/fle is used by scan-strong, scan-given-0, scan-given, scan-entry-0, scan-entry, scan-branch-0, scan-branch, at-save-0, at-save, at-load-0, at-load,
nat/fle-01 is used by save-load-save, at-save-out-upper,
nat/le-def is used by scan-strong, scan-min-eq, scan-min, save-load-save, at-save-0, at-load-0,
nat/le-ls-simp is used by scan-le, at-save-0, at-load-0,
nat/lels is used by scan-strong, scan-max-0, scan-le-0, scan-le, scan-entry, scan-branch, save-load-save, at-shr, at-save, at-load,
nat/lels-03 is used by scan-strong, at-save-1, at-load-1,
nat/lep-02 is used by save-load-save,
nat/let is used by scan-strong, scan-given-0, scan-entry-0, scan-branch-0,
nat/lez is used by scan-entry, scan-branch, at-save, at-load,
nat/ls-le-simp is used by scan-strong, scan-min-eq, scan-max-0, scan-le-0, at-shr,
nat/sub-add is used by at-shr,
nat/succ-01 is used by scan-entry, scan-branch, at-shr, at-save-out-upper, at-save-out-lower, at-save, at-load,

Used from specification constants

constants/branchsize-0 is used by save-load-save, at-save-out-upper, at-save-out-lower, at-save-0, at-save, at-load-0, at-load,

Used from specification branch

branch/inj is used by load-branch-child,

Used from specification indexnode

indexnode/inj-05 is used by save-properties,

Used from specification array-copy

array-copy/zbranch-array/at-copy is used by at-shr, at-shl,
array-copy/zbranch-array/size-copy is used by size-shr, size-shl,

Used from specification oelem

oelem/key-order/nnn is used by scan-strong,

Used from specification zbranch-array-sorted

zbranch-array-sorted/le-key is used by scan-strong, scan-min, scan-max, scan-lt, scan-le, scan-last, scan-entry, scan-branch,
zbranch-array-sorted/sorted-base is used by scan-entry, scan-branch,
zbranch-array-sorted/sorted-branch-lt-post is used by scan-branch,
zbranch-array-sorted/sorted-entry-lt-post is used by scan-entry,
zbranch-array-sorted/sorted-lt is used by scan-strong,
zbranch-array-sorted/sorted-rec1 is used by scan-entry, scan-branch,

Used from specification array

array/branch-array/Extension is used by save-load-save,
array/zbranch-array/cputput-reverse is used by load-branches-last,
array/branch-array/cputput-reverse is used by save-branches-last,
array/zbranch-array/Size-mkarray is used by load-size,
array/branch-array/Size-mkarray is used by save-size,
array/branch-array/Size-put is used by save-size,
array/zbranch-array/Size-put is used by load-size,
array/zbranch-array/cgetput is used by at-load,
array/branch-array/cgetput is used by at-save,
array/zbranch-array/cngetput is used by at-load,
array/branch-array/cngetput is used by at-save,
array/branch-array/ngp-07 is used by at-save-out-lower,
array/branch-array/ngp-08 is used by at-save-out-upper,