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

string-data/elim is used by substring-zero-rec, substring-offset-rec, substring-app-rec, prefix-num-01, prefix-num, downcase-rec,

Used from specification string-less

string-less/Sortedchars is used by upcase-a, downcase-C, downcase-B, downcase-A,
string-less/pos-a is used by upcase-a, downcase-lower-a, downcase-C, downcase-B, downcase-A,
string-less/pos-capital-a is used by upcase-a, downcase-lower-a, downcase-C, downcase-B, downcase-A,
string-less/pos-capital-b is used by downcase-B,
string-less/pos-capital-c is used by downcase-C,
string-less/pos-capital-z is used by downcase-lower-a, downcase-C, downcase-B, downcase-A,
string-less/pos-z is used by upcase-a,
string-less/Length-empty is used by substring-app-rec,
string-less/Length-rec is used by substring-app-rec,
string-less/len-zero is used by right-trim-trim, right-trim-app, butlast-length,

Used from specification nat

nat/add-01 is used by butlast-length,
nat/add-num-04 is used by downcase-C, downcase-B,
nat/elim-pred-c is used by substring-zero-rec, substring-offset-rec, natstring-chars, butlast-length,
nat/elim-sub is used by substring-app-rec, downcase-C, downcase-B,
nat/fle is used by downcase-C, downcase-B,
nat/l-num-05 is used by natstring-chars,
nat/lels is used by natstring-chars,
nat/lels-01 is used by upcase-a, right-trim-trim, right-trim-app, natstring-chars, downcase-C, downcase-B, downcase-A,
nat/lep is used by substring-app-rec,
nat/ler is used by upcase-a, downcase-A,
nat/let is used by natstring-chars, downcase-lower-a, downcase-C, downcase-B,
nat/ls-01 is used by right-trim-trim, right-trim-app,
nat/not-zero is used by upcase-a, natstring-chars, downcase-lower-a, downcase-C, downcase-B, downcase-A,
nat/pred-03 is used by substring-zero-rec, substring-offset-rec,

Used from specification list-last

list-last/charlist/bapp is used by butlast-app,
list-last/charlist/l-02 is used by last-in,
list-last/charlist/lapp is used by last-app,
list-last/charlist/lb is used by butlast-length,
list-last/charlist/bin-01 is used by butlast-in,
list-last/charlist/l is used by last-in,
list-last/charlist/postifx-app-03 is used by prefix-num,
list-last/charlist/prefix-empty is used by prefix-empty-01,
list-last/charlist/prefix-nil is used by prefix-empty,
list-last/charlist/prefix-rec-03 is used by prefix-num-01,
list-last/charlist/prefix-self is used by prefix-reflexive,

Used from specification string-append

string-append/chartostring-01 is used by downcase-rec,
string-append/app is used by substring-zero-rec, downcase-rec, butlast-app,
string-append/append-base is used by substring-app-rec,
string-append/assoc is used by substring-zero-rec, substring-offset-rec, substring-app-rec, right-trim-app, prefix-num-01, prefix-num, natstring-chars, last-in, last-app, downcase-rec, char-in-rec, char-in-app, butlast-app,
string-append/chartostring-01 is used by substring-zero-rec, substring-offset-rec, substring-app-rec, prefix-num-01, prefix-num, natstring-chars, last-in, downcase-rec, char-in,
string-append/empty is used by substring-app-rec, right-trim-app,
string-append/empty-01 is used by right-trim-app, natstring-chars,
string-append/one is used by substring-app-rec,
string-append/one-01 is used by substring-app-rec,

Used from specification list

list/charlist/Two is used by natstring-chars,
list/charlist/a is used by upcase-a, substring-zero-rec, substring-offset-rec, prefix-num-01, prefix-num, natstring-chars, last-in, downcase-C, downcase-B, downcase-A, char-in-rec, char-in-app, char-in, butlast-app,
list/charlist/app is used by upcase-a, natstring-chars, last-in, downcase-C, downcase-B, downcase-A,
list/charlist/app-02-ant is used by substring-zero-rec,
list/charlist/c is used by substring-zero-rec, natstring-chars, char-in,
list/charlist/c-07 is used by substring-zero-rec, substring-offset-rec, natstring-chars,
list/charlist/c-08 is used by substring-zero-rec,
list/charlist/e is used by substring-zero-rec,
list/charlist/e-01 is used by substring-zero-rec, natstring-chars,
list/charlist/in-01 is used by char-in-rec,
list/charlist/in-06 is used by natstring-chars,
list/charlist/in-17 is used by natstring-chars, char-in-rec, char-in-one, char-in,
list/charlist/in-append is used by natstring-chars, char-in-rec, char-in-app, char-in,
list/charlist/in-empty is used by char-in-empty, char-in,

Used from specification nat-basic2

nat-basic2/a is used by substring-zero-rec, substring-offset-rec, substring-app-rec, right-trim-trim, right-trim-app, natstring-chars, downcase-C, downcase-B, butlast-length,
nat-basic2/add-base is used by substring-app-rec, butlast-length,
nat-basic2/c is used by substring-zero-rec, substring-offset-rec, substring-app-rec, right-trim-trim, right-trim-app, natstring-chars, downcase-C, downcase-B, butlast-length,
nat-basic2/oz is used by substring-zero-rec, substring-offset-rec, substring-app-rec, natstring-chars,
nat-basic2/pred is used by substring-app-rec,
nat-basic2/s is used by right-trim-trim, right-trim-app,

Used from specification string2list

string2list/l2s-app is used by butlast-app,
string2list/l2s-empty is used by char-in,
string2list/l2s-length is used by butlast-length,
string2list/l2s-rec is used by substring-zero-rec, char-in,
string2list/s2l-app is used by last-app, char-in-app, butlast-app,
string2list/s2l-empty is used by upcase-a, prefix-empty-01, prefix-empty, natstring-chars, last-in, downcase-C, downcase-B, downcase-A, char-in-empty,
string2list/s2l-empty-01 is used by prefix-empty-01, last-in, last-app, butlast-length, butlast-in, butlast-app,
string2list/s2l-length is used by substring-all, butlast-length,
string2list/s2l-one is used by char-in-one,
string2list/s2l-rec is used by substring-zero-rec, substring-offset-rec, prefix-num-01, prefix-num, last-in, char-in-rec,
string2list/s2l-rec-01 is used by upcase-a, natstring-chars, downcase-C, downcase-B, downcase-A,
string2list/string2string is used by substring-all, butlast-app,

Used from specification nat-mult

nat-mult/leone is used by natstring-chars,
nat-mult/mult-a is used by natstring-chars,
nat-mult/mult-c is used by natstring-chars,

Used from specification nat-basic1

nat-basic1/f is used by upcase-a, natstring-chars, downcase-C, downcase-B, downcase-A,
nat-basic1/lf-02 is used by natstring-chars,
nat-basic1/one-01 is used by right-trim-trim, right-trim-app,
nat-basic1/ref-1 is used by right-trim-trim, right-trim-app,
nat-basic1/twols-02 is used by natstring-chars,

Used from specification nat-div

nat-div/le-div-to-mult is used by natstring-chars,
nat-div/mod-le-03 is used by natstring-chars,

Used from specification list-del

list-del/charlist/get-rec is used by natstring-chars,
list-del/charlist/sub-rec is used by substring-offset-rec,
list-del/charlist/sub-zerorec is used by substring-zero-rec,
list-del/charlist/sublist-all is used by substring-all,
list-del/charlist/get-numrec is used by upcase-a, downcase-C, downcase-B, downcase-A,
list-del/charlist/get-zero-01 is used by upcase-a, natstring-chars, downcase-C, downcase-B, downcase-A,
list-del/charlist/one-03 is used by natstring-chars,

Used from specification string2nat

string2nat/n2s-char is used by natstring-chars,
string2nat/n2s-rec is used by natstring-chars,