[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 list-data
Used from specification list
- list/natlista/One
is used by
sum-listlength-one,
- list/natlista/c
is used by
sum-listlength-one,
- list/natlista/Nil
is used by
sum-append,
prod-app,
- list/natlista/a
is used by
sum-append,
prod-one,
prod-last,
prod-eq-zero,
prod-eq-one-01,
prod-app,
- list/natlista/app
is used by
prod-one,
- list/natlista/c
is used by
sum-append,
prod-eq-zero,
prod-eq-one-01,
prod-app,
- list/natlista/in-06
is used by
prod-eq-zero,
- list/natlista/in-10
is used by
prod-eq-zero,
- list/natlista/in-12
is used by
prod-eq-zero,
- list/natlista/in-17
is used by
prod-eq-zero,
prod-eq-one-01,
- list/natlista/in-append
is used by
prod-eq-zero,
prod-eq-one-01,
- list/natlista/in-empty
is used by
prod-eq-zero,
prod-eq-one-01,
Used from specification nat-basic2
Used from specification nat-mult
- nat-mult/mult-a
is used by
prod-one,
prod-last,
prod-eq-zero,
prod-eq-one-01,
prod-app,
- nat-mult/mult-base
is used by
prod-eq-zero,
- nat-mult/mult-c
is used by
prod-one,
prod-last,
prod-eq-zero,
prod-eq-one-01,
prod-app,
- nat-mult/one
is used by
prod-one,
prod-app,
- nat-mult/one-01
is used by
prod-eq-one-01,
- nat-mult/zero-01
is used by
prod-eq-zero,
- nat-mult/zero-02
is used by
prod-last,
prod-app,
Used from specification nat-basic1
Used from specification list-del