[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 Inv-last-inner-reduce, Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-reduce, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/c is used by Inv-last-inner-reduce, Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-reduce, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/eq-01 is used by Inv-last-inner-init-b,
nat-basic/eq-02 is used by Inv-last-inner-init-b,
nat-basic/f is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/l is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/l-01 is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/l-02 is used by Inv-last-inner-init-b, Inv-first-inner-init-b,
nat-basic/lf is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/lf-01 is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/lf-02 is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/nls-fst is used by Inv-last-inner-init-a, Inv-first-inner-init-a,
nat-basic/one is used by Inv-last-inner-init-a,
nat-basic/one-01 is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/oz is used by Inv-last-inner-init-b,
nat-basic/ref is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/s-04 is used by Inv-last-inner-init-b,
nat-basic/succ is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/trans is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat-basic/twols is used by Inv-last-inner-init-a,
nat-basic/twols-02 is used by Inv-last-inner-init-a,
nat-basic/zero is used by Inv-last-inner-init-b,

Used from specification nat

nat/add-num-03 is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat/anti is used by Inv-first-inner-init-b,
nat/cancel-01 is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat/elim-pred-c is used by Inv-last-inner-init-b,
nat/eqle-one is used by Inv-last-inner-init-b,
nat/fle is used by Inv-last-inner-init-b,
nat/fle-01 is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat/ge is used by Inv-last-inner-init-b,
nat/gr-def is used by Inv-last-inner-init-b,
nat/l-num-01 is used by Inv-last-inner-init-b,
nat/le-def is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
nat/lels is used by Inv-last-inner-init-b, Inv-first-inner-init-b,
nat/lels-02 is used by Inv-last-inner-init-a,
nat/lep is used by Inv-last-inner-init-b,
nat/lep-02 is used by Inv-last-inner-reduce, Inv-last-inner-init-b, Inv-first-inner-reduce,
nat/ler is used by Inv-last-inner-init-b, Inv-first-inner-init-b, Inv-first-inner-init-a, Inv-end-init,
nat/let is used by Inv-last-inner-init-b,
nat/lez is used by Inv-main-init, Inv-last-inner-init-a,
nat/ls-add-not-01 is used by Inv-last-inner-init-b,
nat/ls-le-simp is used by Inv-first-inner-init-b,
nat/succ-01 is used by Inv-last-inner-init-b,
nat/zero is used by Inv-first-inner-init-b, Inv-first-inner-init-a,

Used from specification oarray-sorted

oarray-sorted/sorted-0-or-1 is used by Inv-last-inner-init-a,
oarray-sorted/sorted-inc-left is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
oarray-sorted/less-eq-elem is used by Inv-last-inner-reduce, Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-reduce, Inv-first-inner-init-b, Inv-first-inner-init-a, Inv-end-reduce,
oarray-sorted/sorted-0-or-1 is used by Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-init-b, Inv-first-inner-init-a,
oarray-sorted/sorted-emtpy is used by Inv-main-init, Inv-last-inner-init-a,
oarray-sorted/sorted-higher-lower-bound is used by Inv-main-reduce, Inv-last-inner-reduce, Inv-last-inner-init-b, Inv-last-inner-init-a, Inv-first-inner-reduce, Inv-first-inner-init-b, Inv-first-inner-init-a, Inv-end-reduce, Inv-end-init,
oarray-sorted/sorted-merge is used by Inv-last-inner-init-b,
oarray-sorted/sorted-mixup is used by Inv-last-inner-init-b,
oarray-sorted/sorted-write-other is used by Inv-last-inner-init-b, Inv-last-inner-init-a,

Used from specification oarray-perm

oarray-perm/perm-ident is used by Inv-main-init, Inv-first-inner-init-b, Inv-first-inner-init-a, Inv-end-init,
oarray-perm/perm-swap is used by Inv-first-inner-init-a,
oarray-perm/perm-trans is used by Inv-first-inner-init-b, Inv-first-inner-init-a,

Used from specification oelem

oelem/irreflexivity is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
oelem/ls-le is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
oelem/nll is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
oelem/transitivity is used by Inv-last-inner-init-b, Inv-last-inner-init-a,

Used from specification array

array/cputput-reverse is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
array/put-same-content is used by Inv-end-init,
array/Size-put is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
array/cgetput is used by Inv-last-inner-init-b, Inv-last-inner-init-a,
array/cngetput is used by Inv-last-inner-init-b,
array/putgetinv is used by Inv-first-inner-init-b,