[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 list-data

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

Used from specification list

list/Nil is used by sort-02, ins-01,
list/a is used by two-01, two, sort-append-three, sort-append, sort-02, sort-01, sort, size-01, size, rec, perm-01, one, ole, ins-02, ins-01, ins, eq, emptyp, del1, combine-ordered-sublists, appins,
list/app is used by one, combine-ordered-sublists,
list/app-01 is used by ole,
list/app-08 is used by two-01, two, eq,
list/c is used by sort-02, sort, size, rec, perm-01, ins-01, ins, eq, emptyp, del1, combine-ordered-sublists, appins,
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-05 is used by size,

Used from specification nat-basic2

nat-basic2/a is used by size-01, size,
nat-basic2/c is used by size-01, size,
nat-basic2/eq-01 is used by size-01, size,
nat-basic2/succ is used by size,

Used from specification list-perm

list-perm/perm-l is used by appins,
list-perm/sym is used by perm-01, ordered-perm-sort,
list-perm/trans is used by perm-01,
list-perm/a is used by perm-01,
list-perm/app is used by rec, ins, appins,
list-perm/app-01 is used by sort-append-three, sort-01, ins-02, combine-ordered-sublists,
list-perm/app-02 is used by sort-append-three, sort-append, ins-02,
list-perm/cons is used by perm-01,
list-perm/in is used by in,
list-perm/perm-r is used by empty,
list-perm/perm-rmv-in-list is used by combine-ordered-sublists,
list-perm/ref is used by sperm, sort-append-three, sort-append, sort-01, rec, perm-01, perm, ins-02, ins, in, combine-ordered-sublists, appins,
list-perm/sym-01 is used by sperm, perm, in,
list-perm/sym-02 is used by sperm, sort-01, rec, perm, ins, appins,
list-perm/trans is used by sperm, perm, in,

Used from specification olist

olist/del1-01-02 is used by del1,
olist/eqdef is used by sperm, sort-01, rec, ins-02, ins, appins,
olist/ins-y is used by ins-01,
olist/ordered-append is used by combine-ordered-sublists,
olist/cons-02 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 sort-02, sort, ins-01,
olist/in-04 is used by appins,
olist/ins-e is used by one, ins-01,
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 rec, perm-01, ins, appins,
olist/len is used by size-01, size,
olist/ole-01 is used by rec, ins-02, ins, 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,