[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/elim-pred-c is used by put-at,
nat/elim-sub is used by get-rec,
nat/le-def is used by get-rec,
nat/lels is used by put-length, putset-same, put-at-eq,
nat/succ-01 is used by put-length, putset-same, put-at-eq,

Used from specification list-data

list-data/disj-nil-add is used by put-length, extension, putset-same, put-at-eq, put-at,
list-data/elim-add is used by get-zero-01,
list-data/elim-list-c is used by get-rec-01, extension,
list-data/inj-add is used by extension, putset-same,
list-data/l is used by put-length, extension, putset-same, put-at-eq, put-at,
list-data/sel-add-dottail is used by put-at,
list-data/size-add is used by put-length, extension, putset-same, put-at-eq, put-at,
list-data/size-nil is used by extension,

Used from specification nat-basic

nat-basic/a is used by get-rec, put-length, extension, putset-same, put-at-eq, put-at,
nat-basic/c is used by get-rec, put-length, extension, putset-same, put-at-eq, put-at,
nat-basic/eq-01 is used by put-length, extension, put-at,
nat-basic/f is used by put-length, extension, putset-same, put-at-eq, put-at,
nat-basic/l is used by put-at,
nat-basic/lf-01 is used by extension,
nat-basic/one-01 is used by get-rec,
nat-basic/oz is used by extension, put-at,
nat-basic/s-04 is used by put-length, extension, putset-same, put-at-eq,
nat-basic/succ is used by put-length, extension, putset-same, put-at-eq, put-at,
nat-basic/zero is used by extension, put-at,