[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/anti
is used by
rg2-lem2-term-unfair,
- nat/eqle-one
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/le-ls-simp
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/le-one
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/lels
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/lels-03
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/lep
is used by
rg2-lem1-term-unfair,
- nat/lep-02
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat/les
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
Used from specification nat-basic2
- nat-basic2/a
is used by
rg2-sound-main-unfair,
rg2-not-pre1-unfair,
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
not-pre1-term-unfair,
fair-sustains-implies-always,
fair-never-violates-left-rely,
fair-always-left-rely,
- nat-basic2/c
is used by
rg2-sound-main-unfair,
rg2-not-pre1-unfair,
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
not-pre1-term-unfair,
fair-sustains-implies-always,
fair-never-violates-left-rely,
fair-always-left-rely,
- nat-basic2/eq
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat-basic2/eq-01
is used by
rg2-lem1-term-unfair,
- nat-basic2/l
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
not-pre1-term-unfair,
- nat-basic2/oz
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat-basic2/s
is used by
rg2-sound-main-unfair,
rg2-not-pre1-unfair,
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
not-pre1-term-unfair,
fair-sustains-implies-always,
fair-never-violates-left-rely,
fair-always-left-rely,
- nat-basic2/succ
is used by
rg2-sound-main-unfair,
rg2-not-pre1-unfair,
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
not-pre1-term-unfair,
fair-sustains-implies-always,
fair-never-violates-left-rely,
fair-always-left-rely,
Used from specification nat-basic1
- nat-basic1/f
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat-basic1/lf-01
is used by
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
- nat-basic1/ref-1
is used by
rg2-sound-main-unfair,
rg2-not-pre1-unfair,
rg2-lem2-term-unfair,
rg2-lem1-term-unfair,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
not-pre1-term-unfair,
fair-sustains-implies-always,
fair-never-violates-left-rely,
fair-always-left-rely,