[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/inj-03 is used by n2s-zero,
string-data/elim is used by s2n-rec-01, s2n-app,

Used from specification string-less

string-less/append-eqlen-01 is used by inject-n2s,
string-less/neq-length is used by n2s-zero, inject-n2s,
string-less/Length-empty is used by test-02, s2n-char-01, s2n-app, n2s-zero, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0,
string-less/Length-rec is used by s2n-rec-01, s2n-char-01, s2n-app,
string-less/len-app is used by s2n-app, n2s-zero, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, inject-n2s,
string-less/len-str-01 is used by test-02, n2s-zero, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0,
string-less/len-zero is used by s2n-rec-01, s2n-char-01, s2n-app, n2s-zero, inject-n2s,
string-less/length-one is used by s2n-rec-last,

Used from specification nat

nat/add-01 is used by s2n-rec-01,
nat/add-num-04 is used by n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2,
nat/elim-pred-c is used by n2s-zero, n2s-s2n-identity, n2s-chars,
nat/fle is used by inject-n2s,
nat/fle-01 is used by n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02,
nat/l-num-05 is used by n2s-zero, n2s-s2n-identity, n2s-chars,
nat/lels is used by n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-empty, n2s-chars, inject-n2s,
nat/lels-01 is used by n2s-zero, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-chars,
nat/let is used by n2s-s2n-identity, n2s-chars, inject-n2s,
nat/ls-le-simp is used by n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02,
nat/not-zero is used by n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-empty, n2s-chars, inject-n2s,
nat/pred-03 is used by s2n-rec-01, n2s-s2n-identity, n2s-chars,

Used from specification nat-pot

nat-pot/add is used by s2n-rec-01, s2n-app,

Used from specification string-append

string-append/append-base is used by s2n-app,
string-append/assoc is used by s2n-rec-01, s2n-char-01, s2n-app, n2s-zero, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-length, n2s-empty, n2s-chars, inject-n2s,
string-append/chartostring-01 is used by s2n-rec-01, s2n-char-01, s2n-app, n2s-zero, n2s-s2n-identity, n2s-length, n2s-empty, n2s-chars, inject-n2s,
string-append/empty is used by n2s-empty,
string-append/empty-01 is used by s2n-rec-01, s2n-char-01, s2n-app, n2s-zero, n2s-s2n-identity, n2s-length, n2s-empty, n2s-chars, inject-n2s,
string-append/first-01 is used by s2n-app,
string-append/first-one is used by s2n-char-01, s2n-app, n2s-zero,
string-append/one is used by s2n-app,
string-append/one-01 is used by s2n-rec-last, n2s-zero, n2s-empty,
string-append/rest-01 is used by s2n-app,
string-append/rest-one is used by s2n-app,

Used from specification list

list/charlist/Two is used by s2n-char-01, n2s-zero, n2s-s2n-identity, n2s-length, n2s-empty, n2s-chars, inject-n2s, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0, char9, char8, char7, char6, char5, char4, char3, char2, char1, char0,
list/charlist/a is used by s2n-char-01, n2s-zero, n2s-s2n-identity, n2s-chars, inject-n2s, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0, char9, char8, char7, char6, char5, char4, char3, char2, char1, char0,
list/charlist/c is used by s2n-char-01, n2s-zero, n2s-s2n-identity, n2s-length, n2s-empty, n2s-chars, inject-n2s, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0, char9, char8, char7, char6, char5, char4, char3, char2, char1, char0,
list/charlist/c-07 is used by n2s-zero, n2s-chars,
list/charlist/e-01 is used by n2s-zero, n2s-chars,
list/charlist/in-01 is used by n2s-chars,
list/charlist/in-06 is used by n2s-chars,
list/charlist/in-17 is used by n2s-chars, inject-n2s,
list/charlist/in-append is used by n2s-chars, inject-n2s,
list/charlist/len is used by inject-n2s,
list/charlist/len-02 is used by inject-n2s,

Used from specification nat-basic2

nat-basic2/a is used by s2n-rec-last, s2n-rec-01, s2n-char-01, s2n-app, n2s-zero, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-chars, inject-n2s, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2,
nat-basic2/add-base is used by s2n-rec-01,
nat-basic2/c is used by s2n-rec-last, s2n-rec-01, s2n-num, s2n-char-01, s2n-app, n2s-zero, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-chars, inject-n2s, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2,
nat-basic2/eq-01 is used by s2n-rec-last, s2n-rec-01, s2n-app,
nat-basic2/one is used by s2n-rec-01,
nat-basic2/one-03 is used by s2n-char-01, s2n-app, n2s-zero, inject-n2s,
nat-basic2/oz is used by s2n-app, n2s-zero, n2s-s2n-identity, n2s-chars,
nat-basic2/pred is used by s2n-app,
nat-basic2/succ is used by s2n-rec-01,
nat-basic2/z-01 is used by s2n-app,

Used from specification list-dup

list-dup/charlist/c is used by inject-n2s,
list-dup/charlist/rec is used by inject-n2s,

Used from specification string2list

string2list/at-eq is used by inject-n2s,
string2list/length-at is used by n2s-length, inject-n2s,
string2list/s2l-app is used by n2s-chars,
string2list/s2l-one is used by n2s-chars,

Used from specification nat-mult

nat-mult/dist is used by s2n-app,
nat-mult/leone is used by n2s-s2n-identity, n2s-empty, n2s-chars, inject-n2s,
nat-mult/mult-a is used by s2n-rec-01, s2n-app, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-empty, n2s-chars, inject-n2s,
nat-mult/mult-c is used by s2n-rec-01, s2n-num, s2n-app, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-empty, n2s-chars, inject-n2s,
nat-mult/one is used by s2n-app,

Used from specification nat-basic1

nat-basic1/f is used by n2s-zero, n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-length, n2s-chars, inject-n2s,
nat-basic1/lf-02 is used by n2s-zero, n2s-chars,
nat-basic1/one is used by s2n-rec-01, s2n-app,
nat-basic1/twols-02 is used by n2s-zero, n2s-s2n-identity, n2s-chars,

Used from specification list-del

list-del/charlist/get-numrec is used by n2s-s2n-identity, n2s-chars,
list-del/charlist/get-rec is used by n2s-zero, n2s-chars,
list-del/charlist/pos-n is used by n2s-s2n-identity, charn9, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1,
list-del/charlist/get-numrec is used by char9, char8, char7, char6, char5, char4, char3, char2, char1,
list-del/charlist/get-zero-01 is used by n2s-zero, n2s-s2n-identity, n2s-chars, char8, char7, char6, char5, char4, char3, char2, char1, char0,
list-del/charlist/one-03 is used by n2s-zero, n2s-s2n-identity, n2s-chars, char9,
list-del/charlist/pos-one is used by n2s-s2n-identity, charn9,
list-del/charlist/pos-y is used by n2s-s2n-identity, charn8, charn7, charn6, charn5, charn4, charn3, charn2, charn1, charn0,

Used from specification nat-div

nat-div/Moddef is used by n2s-s2n-identity,
nat-div/div-elim is used by inject-n2s,
nat-div/le-div-to-mult is used by n2s-s2n-identity, n2s-length-10, n2s-length-09, n2s-length-08, n2s-length-07, n2s-length-06, n2s-length-05, n2s-length-04, n2s-length-03, n2s-length-02, n2s-empty, n2s-chars, inject-n2s,
nat-div/mod-le-03 is used by n2s-s2n-identity, n2s-chars, inject-n2s,
nat-div/mod-ls is used by n2s-length-01, inject-n2s,