[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-basic1

nat-basic1/f is used by INVR-step, INVR-nextlevel, INV-nextlevel,
nat-basic1/lf-01 is used by INV-nextlevel,
nat-basic1/ls-02 is used by INVR-nextlevel,
nat-basic1/ref-1 is used by INV-nextlevel,

Used from specification set-basic

set-basic/In-empty is used by INVR-nextlevel, INV-nextlevel, INV-init,
set-basic/in-04 is used by INVR-init, INV-init,
set-basic/ne-01 is used by INVR-step, INVR-nextlevel, INV-step, INV-nextlevel,
set-basic/size-zero-01 is used by INVR-step, INVR-nextlevel, INV-step, INV-nextlevel,

Used from specification nat

nat/add-num-03 is used by INV-nextlevel,
nat/ax-10 is used by INVR-init,
nat/cancel-01 is used by INVR-nextlevel,
nat/elim-pred-c is used by INVR-step, INVR-nextlevel,
nat/elim-sub is used by INVR-step, INVR-nextlevel,
nat/eqle-one is used by INV-nextlevel,
nat/l-num-01 is used by INV-nextlevel,
nat/le-ls-simp is used by INVR-step, INV-nextlevel,
nat/lels is used by INVR-step, INVR-nextlevel, INV-nextlevel,
nat/lels-01 is used by INVR-nextlevel,
nat/lels-03 is used by INVR-nextlevel,
nat/lep is used by INVR-step,
nat/lep-02 is used by INV-nextlevel,
nat/lez is used by INVR-init,
nat/ls-le-simp is used by INVR-nextlevel,
nat/succ-01 is used by INVR-nextlevel,

Used from specification graph

graph/reach-rec-rev is used by INVR-step,
graph/reach-succ is used by INV-nextlevel,
graph/reach-trans is used by INVR-step,
graph/reachls-def is used by INVR-step, INV-nextlevel,
graph/reachset-def is used by INVR-step, INV-step,
graph/reach-one is used by INV-init,
graph/reach-succ is used by INVR-step, INVR-nextlevel, INV-step, INV-nextlevel,
graph/reach-zero is used by INVR-step, INV-init,
graph/reachless-edge is used by INV-step,
graph/reachless-next is used by INV-nextlevel,
graph/reachless-one is used by INV-init,
graph/reachless-succ is used by INV-nextlevel,
graph/reachless-succ-edge is used by INV-nextlevel,
graph/reachless-zero is used by INV-init,
graph/reachset-del is used by INV-step,
graph/reachset-emptyset is used by INVR-nextlevel, INV-nextlevel, INV-init,
graph/reachset-mem-reach is used by INVR-step, INV-step,
graph/reachset-one is used by INVR-step, INVR-nextlevel, INVR-init, INV-step, INV-nextlevel, INV-init,

Used from specification nat-basic2

nat-basic2/a is used by INVR-step, INVR-nextlevel, INV-step, INV-nextlevel,
nat-basic2/between is used by INV-nextlevel,
nat-basic2/c is used by INVR-step, INVR-nextlevel, INV-step, INV-nextlevel,
nat-basic2/l is used by INVR-step,
nat-basic2/l-01 is used by INVR-step, INVR-nextlevel,
nat-basic2/oz is used by INVR-step, INVR-nextlevel, INV-nextlevel,
nat-basic2/s is used by INVR-step, INV-nextlevel,
nat-basic2/z is used by INVR-step,

Used from specification set-union

set-union/Difference is used by INVR-step, INV-step,
set-union/One is used by INVR-step, INVR-nextlevel, INVR-init, INV-step, INV-nextlevel, INV-init,
set-union/Union is used by INVR-step, INV-step,
set-union/del-rax is used by INVR-step, INV-step,
set-union/una is used by INVR-step, INV-step,
set-union/unc is used by INVR-step, INV-step,
set-union/unin is used by INVR-step,