[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-inf-basic

nat-inf-basic/disj is used by infinite-append-butlast,
nat-inf-basic/inj is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-inf-basic/sel is used by infinite-append-butlast,

Used from specification nat

nat/add-01 is used by infinite-append-butlast,
nat/add-num-01 is used by nextl-nextj-lemma-butlast,
nat/add-num-03 is used by nextl-nextj-lemma-butlast,
nat/anti is used by weakmon-lem,
nat/elim-pred-c is used by weakmon-lem, nextl-lemma-butlast-nonempty, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/elim-sub is used by infinite-append-lem, infinite-append,
nat/eq-01 is used by infinite-append-lem, infinite-append,
nat/eq-02 is used by infinite-append-butlast,
nat/eqle-one is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/fle is used by weakmon-lem, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append,
nat/fle-01 is used by infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/ge is used by weakmon-lem, infinite-append,
nat/le-add is used by nextl-nextj-lemma-butlast, diag-theorem-butlast,
nat/le-ls-simp is used by weakmon-lem, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/le-one is used by infinite-append-butlast,
nat/lels is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/lels-01 is used by weakmon-lem, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/lels-02 is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem,
nat/lels-03 is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append,
nat/lep is used by nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append,
nat/lep-02 is used by nextl-nextj-lemma-butlast, infinite-append,
nat/leprf is used by infinite-append-butlast,
nat/ler is used by weakmon-lem, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append,
nat/les is used by weakmon-lem, infinite-append,
nat/let is used by weakmon-lem, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append,
nat/lez is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-butlast, infinite-append,
nat/lez-01 is used by weakmon-lem, nextl-nextj-lemma-butlast, infinite-append-butlast, infinite-append,
nat/ls is used by infinite-append-butlast,
nat/ls-01 is used by infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat/ls-02 is used by weakmon-lem, infinite-append-lem, infinite-append,
nat/ls-le-simp is used by infinite-append-lem, infinite-append,
nat/not-zero is used by infinite-append-butlast,
nat/succ-01 is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append,

Used from specification list-last

list-last/lapp is used by infinite-append-butlast,
list-last/l is used by nextl-nextj-lemma-butlast, infinite-append-butlast, diag-theorem-butlast,
list-last/l-01 is used by infinite-append-butlast,
list-last/last-elim is used by infinite-append-butlast,

Used from specification list-data

list-data/elim-1 is used by infinite-append-butlast, diag-theorem-butlast,
list-data/elim-list-c is used by infinite-append-butlast, diag-theorem-butlast,
list-data/l is used by infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
list-data/size-01 is used by infinite-append-butlast, infinite-append,

Used from specification stream

stream/append-split is used by infinite-append-butlast,
stream/extensionality is used by diag-theorem-butlast,
stream/fin-size-from is used by infinite-append-butlast,
stream/from-nf is used by infinite-append-lem,
stream/from-succ is used by infinite-append-butlast,
stream/get-from is used by infinite-append-butlast, diag-theorem-butlast,
stream/get-to is used by diag-theorem-butlast,
stream/size-to is used by infinite-append-butlast,
stream/to-unwind-end is used by infinite-append-butlast,
stream/append-assoc is used by infinite-append-butlast,
stream/append-finfin is used by infinite-append-butlast,
stream/cons-append is used by infinite-append-butlast,
stream/cons-eq is used by infinite-append-butlast,
stream/empty is used by infinite-append-butlast,
stream/fin-empty is used by diag-theorem-butlast,
stream/fin-to is used by infinite-append-butlast,
stream/finp-infto is used by infinite-append,
stream/from-fin is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream/from-inf is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream/from-zero is used by infinite-append-butlast, diag-theorem-butlast,
stream/fun-nonempty is used by diag-theorem-butlast,
stream/get-finto is used by infinite-append,
stream/get-from-01 is used by infinite-append,
stream/get-from-inf is used by infinite-append-lem, infinite-append,
stream/get-from-inf-zero is used by diag-theorem-butlast,
stream/get-infto is used by infinite-append-lem, infinite-append, diag-theorem-butlast,
stream/inf-size-to is used by infinite-append, diag-theorem-butlast,
stream/length-from is used by infinite-append, diag-theorem-butlast,
stream/length-to is used by infinite-append,
stream/less-size-from is used by infinite-append-butlast,
stream/notfin-sizeinf is used by infinite-append-butlast, diag-theorem-butlast,
stream/sel-fin is used by infinite-append-butlast, diag-theorem-butlast,
stream/sel-inf is used by infinite-append-butlast, diag-theorem-butlast,
stream/size-empty is used by diag-theorem-butlast,
stream/size-fin is used by infinite-append-butlast, diag-theorem-butlast,
stream/size-inf is used by infinite-append-butlast, infinite-append,
stream/size-inf-to is used by infinite-append-lem, infinite-append,
stream/size-succ is used by infinite-append-butlast,
stream/size-to is used by infinite-append-butlast, diag-theorem-butlast,
stream/to-fin is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream/to-inf is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream/to-succ-cons is used by infinite-append-butlast,
stream/to-zero is used by infinite-append-butlast,
stream/ton-fromn-inf is used by infinite-append,

Used from specification list

list/a is used by infinite-append-butlast, diag-theorem-butlast,
list/app is used by infinite-append-butlast, diag-theorem-butlast,
list/c is used by infinite-append-butlast, diag-theorem-butlast,
list/c-04 is used by nextl-nextj-lemma-butlast, infinite-append-butlast, diag-theorem-butlast,
list/c-08 is used by infinite-append-butlast,
list/e is used by nextl-lemma-butlast-nonempty, infinite-append-butlast, diag-theorem-butlast,
list/e-01 is used by infinite-append-butlast,
list/e-02 is used by infinite-append-butlast,
list/first is used by diag-theorem-butlast,
list/in-14 is used by infinite-append-butlast, diag-theorem-butlast,
list/in-rec is used by infinite-append-butlast,
list/len is used by infinite-append-butlast,
list/len-02 is used by infinite-append-butlast,
list/len-05 is used by infinite-append-butlast,
list/one-01 is used by infinite-append-butlast,

Used from specification nat-basic2

nat-basic2/a is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/add-base is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/c is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/eq is used by nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append,
nat-basic2/eq-01 is used by nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append,
nat-basic2/eqs is used by infinite-append-butlast,
nat-basic2/l is used by infinite-append-lem, infinite-append,
nat-basic2/l-01 is used by infinite-append-lem, infinite-append,
nat-basic2/l-02 is used by nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/l-05 is used by infinite-append-lem,
nat-basic2/l-06 is used by infinite-append-lem, infinite-append,
nat-basic2/nls-fst is used by infinite-append-butlast, infinite-append,
nat-basic2/oz is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/s is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/succ is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic2/succ-03 is used by nextl-nextj-lemma-butlast,
nat-basic2/z-01 is used by infinite-append-butlast, diag-theorem-butlast,

Used from specification stream-basic

stream-basic/inj-02 is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream-basic/stream-fin-forward is used by infinite-append-butlast, diag-theorem-butlast,
stream-basic/stream-inf-forward is used by infinite-append-butlast, diag-theorem-butlast,
stream-basic/test-01 is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
stream-basic/test-02 is used by infinite-append-butlast, diag-theorem-butlast,

Used from specification nat-inf

nat-inf/add-all-zero is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/add-assoc is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/add-comm is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/add-fin is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/add-ls-cancel-01 is used by infinite-append-butlast,
nat-inf/add-ls-cancel-num-04 is used by infinite-append-butlast,
nat-inf/addeqinf-cancel is used by infinite-append-butlast,
nat-inf/eq-natinf-to-nat-2-1 is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/inf-inseq-reduce is used by diag-theorem-butlast,
nat-inf/inf-less is used by infinite-append-butlast,
nat-inf/lele-trans is used by infinite-append-butlast,
nat-inf/leq-notgradd is used by infinite-append-butlast,
nat-inf/less-fin is used by infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-inf/less-inf1 is used by infinite-append-butlast, infinite-append,
nat-inf/less-inf2 is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/less-succ-leq is used by infinite-append-butlast,
nat-inf/ls-le is used by infinite-append-butlast,
nat-inf/ls-natinf-to-nat-2-1 is used by infinite-append-butlast,
nat-inf/ls-natinf-to-nat-3-1 is used by infinite-append-butlast,
nat-inf/lsle-trans is used by infinite-append-butlast, diag-theorem-butlast,
nat-inf/not-less-zero is used by infinite-append-butlast,
nat-inf/num-add is used by infinite-append-butlast,

Used from specification nat-basic1

nat-basic1/f is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic1/lf is used by infinite-append, diag-theorem-butlast,
nat-basic1/lf-01 is used by weakmon-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic1/lf-02 is used by weakmon-lem, infinite-append-lem, infinite-append-butlast, infinite-append, diag-theorem-butlast,
nat-basic1/ls-02 is used by infinite-append-lem, infinite-append,
nat-basic1/neq-01 is used by infinite-append,
nat-basic1/one-01 is used by weakmon-lem, infinite-append-lem, infinite-append-butlast, infinite-append,
nat-basic1/ref-1 is used by weakmon-lem, nextl-nextj-lemma-butlast, nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append-butlast, infinite-append,
nat-basic1/trans-1 is used by infinite-append, diag-theorem-butlast,
nat-basic1/zero is used by infinite-append-butlast, diag-theorem-butlast,
nat-basic1/zero-01 is used by nextl-lemma-butlast-nonempty, nextl-lemma-butlast, nextl-lemma, infinite-append-lem, infinite-append, diag-theorem-butlast,

Used from specification list-del

list-del/extension is used by infinite-append-lem, infinite-append,
list-del/get-zero is used by diag-theorem-butlast,