[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-basic

nat-basic/a is used by inv-add,
nat-basic/c is used by inv-add,
nat-basic/eq-01 is used by inv-add,
nat-basic/f is used by inv-get,
nat-basic/neq-01 is used by inv-add,
nat-basic/oz is used by inv-add,
nat-basic/ref is used by inv-add,
nat-basic/s-04 is used by inv-add,
nat-basic/succ is used by inv-add,
nat-basic/zero is used by inv-init, inv-add,

Used from specification nat

nat/gr-def is used by inv-init,

Used from specification list-data

list-data/l is used by inv-init, inv-add, inv-get,
list-data/size-01 is used by inv-init, inv-add,

Used from specification list

list/a is used by inv-add,
list/c is used by inv-add,
list/len-05 is used by inv-add,