[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/f is used by id-idx-write-left, id-idx-write, id-idx-trans,
nat-basic/lf-01 is used by id-idx-write-left, id-idx-write, id-idx-trans,

Used from specification nat

nat/lels is used by id-idx-write,
nat/ls-le-simp is used by id-idx-write,

Used from specification array

array/index-array-base/Put-other is used by id-idx-write-left, id-idx-write,
array/index-array-base/Put-same is used by id-idx-write-left,
array/index-array-base/Size-put is used by id-idx-write-left, id-idx-write,
array/index-array-base/cgetput is used by id-idx-write,

Used from specification elem-index

elem-index/elim is used by id-idx-write-left, id-idx-write, id-idx-trans,
elem-index/inj is used by id-idx-write-left, id-idx-write,
elem-index/sel-01 is used by id-idx-write-left, id-idx-write, id-idx-trans,
elem-index/upd-02 is used by id-idx-write-left, id-idx-write,