[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

nat/anti is used by infinite-append-prefixnextli,
nat/elim-sub is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/fle is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/fle-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/le-add is used by infinite-append-prefixnextli, infinite-append-prefixnextnli,
nat/le-def is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/le-ls-simp is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/le-one is used by infinite-append-prefixnextli,
nat/lels is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/lels-02 is used by nextli-lemma, nextnli-lemma,
nat/lels-03 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,
nat/lep is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/lep-02 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/ler is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/let is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/lez is used by nextli-lemma, nextnli-lemma,
nat/ls is used by infinite-append-prefixnextnli,
nat/ls-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/ls-le-simp is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat/succ-01 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,

Used from specification nat-inf

nat-inf/add-assoc is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/add-comm is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/add-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/disj-rqui-infty is used by infinite-append-prefixnextli,
nat-inf/inj-rqui is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/lele-trans is used by infinite-append-prefixnextnli,
nat-inf/lels-trans is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/less-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/less-inf1 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/less-inf2 is used by infinite-append-prefixnextnli,
nat-inf/ls-lsadd is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak,
nat-inf/ls-natinf-to-nat-1-2 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/ls-natinf-to-nat-2-1 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-inf/sel-rqui-dotn is used by infinite-append-prefixnextnli,

Used from specification stream-basic

Used from specification list-data

list-data/l is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
list-data/size-nil is used by infinite-append-prefixnextli, infinite-append-prefixnextnli,

Used from specification nat-basic

nat-basic/a is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/add-base is used by infinite-append-prefixnextli, infinite-append-prefixnextnli,
nat-basic/c is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/eq-01 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/eq-02 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,
nat-basic/f is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/l is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/l-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/l-02 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/l-05 is used by infinite-append-prefixnextli,
nat-basic/less-zero is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,
nat-basic/lf is used by infinite-append-prefixnextli,
nat-basic/lf-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/lf-02 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/ls-02 is used by infinite-append-prefixnextli, infinite-append-prefixnextnli,
nat-basic/neq-01 is used by infinite-append-prefixnextli,
nat-basic/oz is used by nextli-lemma, nextnli-lemma,
nat-basic/refl-nat is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,
nat-basic/s-04 is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma,
nat-basic/succ is used by nextli-lemma, infinite-append-prefixnextli, nextnli-lemma, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
nat-basic/trans-nat is used by infinite-append-prefixnextli,

Used from specification list

list/a is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
list/app is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
list/len is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
list/len-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak,

Used from specification stream-old

stream-old/extensionality is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/fin-size-from is used by infinite-append-prefixnextnli,
stream-old/fin-size-from2 is used by infinite-append-prefixnextnli,
stream-old/get-to is used by infinite-append-prefixnextnli,
stream-old/empty is used by infinite-append-prefixnextli,
stream-old/extract-empty is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/fin-finlen-tolen is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/from-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/from-inf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/get-finto is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/get-from-01 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/get-from-inf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/get-to is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/get-to-02 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/length-from is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/length-to is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/notfin-sizeinf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/sel-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/sel-inf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/size-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/size-from-less is used by infinite-append-prefixnextnli,
stream-old/size-inf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/size-to is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/size-to-02 is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/to-fin is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/to-inf is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/to-zero is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,
stream-old/to-zero-l is used by infinite-append-prefixnextli, infinite-append-prefixnextnli,

Used from specification list-del

Used from specification list-last

list-last/prefix is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,

Used from specification infinite-append-old

infinite-append-old/infinite-append is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,

Used from specification list-getput

list-getput/extension is used by infinite-append-prefixnextli, infinite-append-prefixnextli-weak, infinite-append-prefixnextnli,