[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-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/eq
is used by
rg2-sound-main-unfair,
RG2-Sound+DF+Term,
- nat/eqle-one
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/le-ls-simp
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/le-one
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/lels
is used by
rg2-sound-main-unfair,
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
RG2-Sound+DF+Term,
- nat/lels-03
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/lep
is used by
rg2-lem1-term-strnger-term-unfair,
- nat/lep-02
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat/les
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
Used from specification nat-basic2
- nat-basic2/a
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-not-pre2-unfair,
rg2-not-pre2-term-strnger,
rg2-not-pre2-term,
rg2-not-pre2,
rg2-not-pre1-unfair,
rg2-not-pre1-term-strnger,
rg2-not-pre1-term,
rg2-not-pre1,
rg2-lem2-term-strnger-term-unfair,
rg2-lem2-term-strnger,
rg2-lem2-term,
rg2-lem1-term-strnger-term-unfair,
rg2-lem1-term-strnger,
rg2-lem1-term,
rg-blocked2-not-r2-unfair,
rg-blocked2-not-r2-term-unfair,
rg-blocked2-not-r2-term,
rg-blocked2-not-r2,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
rg-blocked1-not-r1-term,
rg-blocked1-not-r1,
not-pre2-term-unfair,
not-pre1-term-unfair,
RG2-Sound+DF+Term,
- nat-basic2/c
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-not-pre2-unfair,
rg2-not-pre2-term-strnger,
rg2-not-pre2-term,
rg2-not-pre2,
rg2-not-pre1-unfair,
rg2-not-pre1-term-strnger,
rg2-not-pre1-term,
rg2-not-pre1,
rg2-lem2-term-strnger-term-unfair,
rg2-lem2-term-strnger,
rg2-lem2-term,
rg2-lem1-term-strnger-term-unfair,
rg2-lem1-term-strnger,
rg2-lem1-term,
rg-blocked2-not-r2-unfair,
rg-blocked2-not-r2-term-unfair,
rg-blocked2-not-r2-term,
rg-blocked2-not-r2,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
rg-blocked1-not-r1-term,
rg-blocked1-not-r1,
not-pre2-term-unfair,
not-pre1-term-unfair,
RG2-Sound+DF+Term,
- nat-basic2/eq
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat-basic2/eq-01
is used by
rg2-lem2-term-strnger-term-unfair,
- nat-basic2/l
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
not-pre1-term-unfair,
- nat-basic2/l-01
is used by
rg2-lem2-term-strnger-term-unfair,
- nat-basic2/oz
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat-basic2/s
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-not-pre2-unfair,
rg2-not-pre2-term-strnger,
rg2-not-pre2-term,
rg2-not-pre2,
rg2-not-pre1-unfair,
rg2-not-pre1-term-strnger,
rg2-not-pre1-term,
rg2-not-pre1,
rg2-lem2-term-strnger-term-unfair,
rg2-lem2-term-strnger,
rg2-lem2-term,
rg2-lem1-term-strnger-term-unfair,
rg2-lem1-term-strnger,
rg2-lem1-term,
rg-blocked2-not-r2-unfair,
rg-blocked2-not-r2-term-unfair,
rg-blocked2-not-r2-term,
rg-blocked2-not-r2,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
rg-blocked1-not-r1-term,
rg-blocked1-not-r1,
not-pre2-term-unfair,
not-pre1-term-unfair,
- nat-basic2/succ
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-not-pre2-unfair,
rg2-not-pre2-term-strnger,
rg2-not-pre2-term,
rg2-not-pre2,
rg2-not-pre1-unfair,
rg2-not-pre1-term-strnger,
rg2-not-pre1-term,
rg2-not-pre1,
rg2-lem2-term-strnger-term-unfair,
rg2-lem2-term-strnger,
rg2-lem2-term,
rg2-lem1-term-strnger-term-unfair,
rg2-lem1-term-strnger,
rg2-lem1-term,
rg-blocked2-not-r2-unfair,
rg-blocked2-not-r2-term-unfair,
rg-blocked2-not-r2-term,
rg-blocked2-not-r2,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
rg-blocked1-not-r1-term,
rg-blocked1-not-r1,
not-pre2-term-unfair,
not-pre1-term-unfair,
RG2-Sound+DF+Term,
Used from specification nat-basic1
- nat-basic1/f
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat-basic1/lf-01
is used by
rg2-lem2-term-strnger-term-unfair,
rg2-lem1-term-strnger-term-unfair,
- nat-basic1/ref-1
is used by
rg2-sound-main-unfair,
rg2-sound-main,
rg2-not-pre2-unfair,
rg2-not-pre2-term-strnger,
rg2-not-pre2-term,
rg2-not-pre2,
rg2-not-pre1-unfair,
rg2-not-pre1-term-strnger,
rg2-not-pre1-term,
rg2-not-pre1,
rg2-lem2-term-strnger-term-unfair,
rg2-lem2-term-strnger,
rg2-lem2-term,
rg2-lem1-term-strnger-term-unfair,
rg2-lem1-term-strnger,
rg2-lem1-term,
rg-blocked2-not-r2-unfair,
rg-blocked2-not-r2-term-unfair,
rg-blocked2-not-r2-term,
rg-blocked2-not-r2,
rg-blocked1-not-r1-unfair,
rg-blocked1-not-r1-term-unfair,
rg-blocked1-not-r1-term,
rg-blocked1-not-r1,
not-pre2-term-unfair,
not-pre1-term-unfair,