[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 valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat-basic/c is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat-basic/f is used by valid-indices-nonrec, valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, map-indices-size, map-indices-at, map-indices-append, map-ifn-at, map-ifn-0, map-if-at, indices-where-in-h,
nat-basic/lf is used by indices-where-in-h,
nat-basic/lf-01 is used by valid-indices-indiceswhere-h-strong,
nat-basic/lf-02 is used by valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat-basic/ls-02 is used by valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat-basic/ref is used by valid-indices-nodups-h, valid-indices-nodups, indices-where-in-h, indices-where-in,
nat-basic/s-04 is used by indices-where-in-h,
nat-basic/succ is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat-basic/zero-01 is used by map-ifn-0, indices-where-in-h,

Used from specification nat

nat/anti is used by indices-where-in-h,
nat/fle is used by valid-indices-nonrec,
nat/fle-01 is used by indices-where-in-h,
nat/le-def is used by valid-indices-nodups, indices-where-in,
nat/le-ls-simp is used by valid-indices-nonrec, valid-indices-indiceswhere-h, valid-indices-append,
nat/lels is used by valid-indices-nonrec, valid-indices-indiceswhere-h-strong, valid-indices-indiceswhere-h, valid-indices-append, map-indices-at, map-indices-append, indices-where-in-h,
nat/lels-02 is used by indices-where-in-h,
nat/lels-03 is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
nat/let is used by valid-indices-indiceswhere-h,
nat/lez is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, map-ifn-0,
nat/ls-le-simp is used by map-indices-at, map-indices-append,
nat/succ-01 is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,

Used from specification set-basic

set-basic/nat-list-set/Extension is used by map-set-empty,
set-basic/nat-list-set/In-empty is used by map-set-empty, map-indices-empty,
set-basic/nat-list-set/size-zero is used by map-set-empty,
set-basic/nat-list-set/size-zero-01 is used by map-set-empty,

Used from specification nat-list-less

nat-list-less/ls-ext is used by valid-indices-one, valid-indices-append,
nat-list-less/ls-rec is used by valid-indices-nonrec,
nat-list-less/ls-base is used by valid-indices-nonrec,
nat-list-less/ls-rec is used by valid-indices-nonrec, map-indices-size, map-indices-at, map-indices-append,

Used from specification list

list/nat-list-set/One is used by map-indices-one,
list/nat-list-set/c is used by map-indices-one,
list/nat-list-set/Nil is used by map-indices-append,
list/nat-list-set/a is used by valid-indices-nonrec, valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, valid-indices-append, map-indices-size, map-indices-at, map-indices-append, indices-where-in-h,
list/nat-list-set/app is used by valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
list/nat-list-set/c is used by valid-indices-nonrec, valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, map-indices-size, map-indices-at, map-indices-append, indices-where-in-h,
list/nat-list-set/in-06 is used by map-indices-append,
list/nat-list-set/in-17 is used by valid-indices-one, valid-indices-nodups-h, valid-indices-indiceswhere-h-strong, indices-where-in-h,
list/nat-list-set/in-append is used by valid-indices-indiceswhere-h-strong, valid-indices-append, indices-where-in-h,
list/nat-list-set/in-empty is used by valid-indices-nonrec, valid-indices-indiceswhere-h-strong, map-indices-at, indices-where-in-h,
list/nat-list-set/in-rec is used by valid-indices-nonrec, map-indices-at,

Used from specification list-dup

list-dup/nat-list-set/dups-appex is used by valid-indices-nodups-h,
list-dup/nat-list-set/c is used by valid-indices-nodups-h,
list-dup/nat-list-set/dups-cons is used by map-indices-at,
list-dup/nat-list-set/e-01 is used by valid-indices-nodups-h,

Used from specification array

array/Extension is used by map-indices-empty, map-ifn-0,
array/Put-other is used by map-indices-at, map-indices-append,
array/Put-same is used by map-indices-at,
array/Size-put is used by valid-indices-write, map-indices-size, map-indices-at, map-indices-append,
array/cngetput is used by map-indices-at,