[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 size-01, size,
nat-basic/c is used by size-01, size,
nat-basic/eq-01 is used by size-01, size,

Used from specification list-data

list-data/elim-list-c is used by combine-ordered-sublists,
list-data/size-nil is used by size,

Used from specification list

list/Nil is used by ins-01, sort-02,
list/a is used by ole, combine-ordered-sublists, two, size-01, ins-01, sort-02, perm-01, ins, size, sort, emptyp, ins-02, sort-append-three, two-01, rec, appins, one, sort-append, eq, del1, sort-01,
list/app is used by combine-ordered-sublists, one,
list/app-01 is used by ole, two, two-01, eq,
list/c is used by combine-ordered-sublists, ins-01, sort-02, perm-01, ins, size, sort, emptyp, rec, appins, eq, del1,
list/c-08 is used by combine-ordered-sublists,
list/e-01 is used by combine-ordered-sublists,
list/in-append is used by appins,
list/len is used by size,
list/len-02 is used by size,

Used from specification list-perm

list-perm/del-01 is used by appins,
list-perm/sym is used by ordered-perm-sort, perm-01,
list-perm/trans is used by perm-01,
list-perm/a is used by perm-01,
list-perm/app-beg-beg is used by perm-01, ins, rec, appins,
list-perm/app-beg-end is used by ins-02, sort-append-three, sort-append,
list-perm/app-end-end is used by combine-ordered-sublists, ins-02, sort-append-three, sort-01,
list-perm/empty-01 is used by empty,
list-perm/in is used by in,
list-perm/ref is used by combine-ordered-sublists, perm, perm-01, in, ins, ins-02, sort-append-three, rec, appins, sort-append, sort-01, sperm,
list-perm/sym-01 is used by perm, in, sperm,
list-perm/sym-02 is used by perm, ins, rec, appins, sort-01, sperm,
list-perm/trans is used by perm, in, sperm,

Used from specification olist

olist/del1-01-02 is used by del1,
olist/eqdef is used by ins, ins-02, rec, appins, sort-01, sperm,
olist/ins-y is used by ins-01,
olist/ordered-append is used by combine-ordered-sublists,
olist/app-01 is used by eq,
olist/cons-03 is used by eq,
olist/del1-02 is used by insdel, del1,
olist/empty is used by emptyp,
olist/eq is used by ins-01, sort-02, sort,
olist/in-04 is used by appins,
olist/ins-e is used by ins-01, one,
olist/ins-n is used by ins-01,
olist/ins-one is used by two,
olist/ins-one-01 is used by two-01,
olist/ins2 is used by ins-01,
olist/insperm-03 is used by perm-01, ins, rec, appins,
olist/len is used by size-01, size,
olist/ole-01 is used by ins, ins-02, rec, appins,
olist/perm-ins is used by appins,

Used from specification list-del

list-del/del1-n is used by del1,
list-del/del1-e is used by del1,
list-del/del1-y is used by del1,