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

INV/INV-def is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
INV/INVR-def is used by BFS-correct-if-reachable,
INV/INV-init is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
INV/INV-nextlevel is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
INV/INV-step is used by ADD-preserves-INV,
INV/INVR-init is used by BFS-correct-if-reachable,
INV/INVR-nextlevel is used by BFS-correct-if-reachable,
INV/INVR-step is used by ADD-preserves-INV-INVR,

Used from specification nat_or_fail

nat_or_fail/disj is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
nat_or_fail/inj is used by BFS-correct-if-reachable,

Used from specification nat-basic1

nat-basic1/f is used by BFS-correct-if-reachable,
nat-basic1/ls-02 is used by BFS-correct-if-reachable,
nat-basic1/one-01 is used by ADD-lemma,
nat-basic1/ref-1 is used by BFS-correct-if-reachable, ADD-lemma,

Used from specification set-basic

set-basic/In-empty is used by BFS-correct-if-reachable, ADD-lemma,
set-basic/Size-empty is used by BFS-correct-if-reachable,
set-basic/in-04 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-basic/ne is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-basic/ne-01 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable, ADD-preserves-INV-INVR, ADD-lemma,
set-basic/one-size is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-basic/rax is used by ADD-lemma,
set-basic/size-one-01 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-basic/size-zero is used by ADD-lemma,
set-basic/size-zero-01 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable, ADD-preserves-INV-INVR, ADD-lemma,
set-basic/size-zero-02 is used by BFS-correct-if-reachable, ADD-lemma,
set-basic/sub-e is used by ADD-lemma,
set-basic/sub-idem is used by ADD-lemma,
set-basic/sub-in is used by ADD-lemma,

Used from specification nat

nat/add-01 is used by BFS-correct-if-reachable,
nat/anti is used by BFS-correct-if-reachable,
nat/elim-sub is used by BFS-correct-if-reachable,
nat/eq-01 is used by BFS-correct-if-reachable,
nat/lels is used by BFS-correct-if-reachable,
nat/lels-01 is used by BFS-correct-if-reachable, ADD-lemma,
nat/lels-02 is used by BFS-correct-if-reachable,
nat/lels-03 is used by BFS-correct-if-reachable,
nat/ler is used by BFS-correct-if-reachable,
nat/ls-01 is used by ADD-lemma,
nat/succ-01 is used by BFS-correct-if-reachable,
nat/zero is used by BFS-correct-if-reachable,
nat/zero-02 is used by BFS-correct-if-reachable,

Used from specification graph

graph/reachls-def is used by BFS-correct-if-reachable,
graph/reachset-def is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
graph/reach-zero is used by BFS-correct-if-reachable,
graph/reachless-zero is used by BFS-correct-if-reachable,
graph/reachset-one is used by BFS-correct-if-reachable,

Used from specification nat-basic2

nat-basic2/a is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable, ADD-lemma,
nat-basic2/c is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable, ADD-lemma,
nat-basic2/eq is used by BFS-correct-if-reachable,
nat-basic2/eq-01 is used by BFS-correct-if-reachable,
nat-basic2/l-02 is used by BFS-correct-if-reachable,
nat-basic2/one-03 is used by BFS-correct-if-reachable,
nat-basic2/oz is used by BFS-correct-if-reachable,
nat-basic2/s is used by BFS-correct-if-reachable, ADD-lemma,
nat-basic2/succ is used by BFS-correct-if-reachable,
nat-basic2/z is used by BFS-correct-if-reachable,

Used from specification set-union

set-union/ext is used by BFS-correct-if-reachable, ADD-lemma,
set-union/subdef is used by ADD-lemma,
set-union/Delete is used by ADD-lemma,
set-union/Difference is used by ADD-lemma,
set-union/One is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-union/Union is used by ADD-lemma,
set-union/del-addeq-05 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-union/del-e-01 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-union/del-e-02 is used by BFS-returns-fail-implies-not-reachable, BFS-correct-if-reachable,
set-union/del-rax is used by ADD-lemma,
set-union/del-size is used by BFS-correct-if-reachable, ADD-lemma,
set-union/diff-e is used by ADD-lemma,
set-union/diff-idem is used by ADD-lemma,
set-union/diff-union is used by ADD-lemma,
set-union/sub-del-03 is used by ADD-lemma,
set-union/una is used by ADD-preserves-INV-INVR, ADD-preserves-INV, ADD-lemma,
set-union/unc is used by ADD-preserves-INV-INVR, ADD-preserves-INV, ADD-lemma,
set-union/undel is used by ADD-lemma,
set-union/une is used by ADD-lemma,
set-union/uneq is used by ADD-lemma,
set-union/unindel is used by ADD-lemma,