[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 string-less

string-less/Pos-rec is used by pos-at,
string-less/sortedchars-divided is used by sortedchars-no-dups,
string-less/Length-empty is used by s2l-length, l2s-length,
string-less/Length-rec is used by s2l-length, pos-at, l2s-length,
string-less/Pos-found is used by pos-at,
string-less/len-zero is used by pos-at,
string-less/length-one is used by length-at,

Used from specification string-data

string-data/inj-03 is used by at-eq,
string-data/elim is used by s2l-rec-01, inject-s2l,

Used from specification nat

nat/elim-pred-c is used by pos-at,
nat/lels is used by pos-at,
nat/ls-le-simp is used by pos-at,
nat/pred-03 is used by pos-at,
nat/succ-01 is used by pos-at,

Used from specification string-append

string-append/app is used by string2string, l2s-app,
string-append/append-base is used by s2l-app, l2s-app,
string-append/assoc is used by string2string, s2l-rec-01, s2l-length, s2l-empty-01, s2l-app, pos-at, l2s-one, l2s-length, l2s-app, inject-s2l,
string-append/chartostring-01 is used by string2string, s2l-rec-01, s2l-length, s2l-empty-01, s2l-app, pos-at, l2s-one, l2s-app, inject-s2l,
string-append/empty-01 is used by l2s-one,
string-append/first-one is used by s2l-one, at-eq,
string-append/one is used by inject-s2l,
string-append/one-01 is used by s2l-one, at-eq,
string-append/rest-one is used by s2l-one,

Used from specification list-data

list-data/charlist/l is used by at-eq,
list-data/charlist/size-01 is used by s2l-length, l2s-length,

Used from specification list

list/charlist/Nil is used by s2l-app, l2s-app,
list/charlist/a is used by string2string, sortedchars-no-dups, s2l-rec-01, s2l-one, s2l-length, s2l-empty-01, s2l-app, pos-at, l2s-one, l2s-length, l2s-app, inject-s2l,
list/charlist/app is used by sortedchars-no-dups, s2l-one, l2s-one,
list/charlist/app-01 is used by s2l-rec-01, s2l-app,
list/charlist/app-02-ant is used by s2l-empty-01, inject-s2l,
list/charlist/c is used by l2s-length, l2s-app,
list/charlist/c-04 is used by s2l-one,
list/charlist/c-06 is used by inject-s2l,
list/charlist/e is used by s2l-empty-01, inject-s2l,
list/charlist/in-14 is used by inject-s2l,
list/charlist/in-17 is used by sortedchars-no-dups, inject-s2l,
list/charlist/in-append is used by sortedchars-no-dups, inject-s2l,
list/charlist/len is used by s2l-length, l2s-length,
list/charlist/len-02 is used by s2l-length, l2s-length,

Used from specification list-dup

list-dup/charlist/c is used by sortedchars-no-dups,
list-dup/charlist/dups-cons is used by pos-at,
list-dup/charlist/rec is used by sortedchars-no-dups,

Used from specification nat-basic2

nat-basic2/a is used by s2l-length, pos-at, l2s-length,
nat-basic2/c is used by s2l-length, pos-at, l2s-length,
nat-basic2/eq-01 is used by s2l-length, pos-at, l2s-length,
nat-basic2/oz is used by pos-at,
nat-basic2/s is used by pos-at,

Used from specification nat-basic1

nat-basic1/f is used by pos-at, at-eq,

Used from specification list-del

list-del/charlist/get-in is used by pos-at,
list-del/charlist/get-numrec is used by pos-at,
list-del/charlist/get-nodups is used by at-eq,
list-del/charlist/get-zero-01 is used by pos-at,

Used from specification list-set

list-set/charlist/dups-app is used by sortedchars-no-dups,
list-set/charlist/filter-empty-def is used by sortedchars-no-dups,