[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
gcd-loop-partial,
- nat/elim-sub
is used by
gcd-loop-partial,
- nat/fle
is used by
gcd-partial,
gcd-loop-partial,
- nat/fle-01
is used by
gcd-partial,
gcd-loop-partial,
- nat/le-add
is used by
gcd-loop-partial,
- nat/le-ls-simp
is used by
gcd-partial,
- nat/lels
is used by
gcd-loop-partial,
- nat/lels-01
is used by
gcd-partial,
gcd-loop-partial,
- nat/lels-02
is used by
gcd-partial,
gcd-loop-partial,
- nat/lep
is used by
gcd-loop-partial,
- nat/ler
is used by
gcd-partial,
gcd-loop-partial,
- nat/let
is used by
gcd-partial,
gcd-loop-partial,
- nat/ls-02
is used by
gcd-loop-partial,
- nat/ls-03
is used by
gcd-loop-partial,
Used from specification nat-prime
Used from specification nat-basic2
Used from specification nat-mult
Used from specification nat-basic1
- nat-basic1/f
is used by
gcd-partial,
gcd-loop-partial,
- nat-basic1/lf
is used by
gcd-partial,
gcd-loop-partial,
- nat-basic1/lf-01
is used by
gcd-partial,
gcd-loop-partial,
- nat-basic1/lf-02
is used by
gcd-partial,
gcd-loop-partial,
- nat-basic1/ls-02
is used by
gcd-loop-partial,
- nat-basic1/neq-01
is used by
gcd-loop-partial,
- nat-basic1/ref-1
is used by
gcd-partial,
gcd-loop-partial,
- nat-basic1/trans-1
is used by
gcd-partial,
gcd-loop-partial,
Used from specification RG2-Theory