[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 list-last

list-last/l-02 is used by remtau-split,
list-last/lapp is used by remtau-split,
list-last/last-def is used by remtau-split,
list-last/last-one is used by remtau-split,

Used from specification nat

nat/add-01 is used by remtau-inf,
nat/elim-pred-c is used by remtau-empty-equiv, remtau-inf,
nat/elim-sub is used by remtau-inf,
nat/eq-01 is used by remtau-inf, remtau-fromempty-to,
nat/fle is used by remtau-inf,
nat/fle-01 is used by remtau-inf,
nat/le-def is used by not-lessto, remtau-inf,
nat/lels is used by remtau-toempty-from, not-lessto, remtau-empty-equiv, remtau-inf, to-addone,
nat/lels-03 is used by remtau-inf,
nat/lep is used by not-lessto-fin, remtau-inf, remtau-fromempty-to,
nat/ler is used by to-addone,
nat/lez is used by remtau-inf,
nat/ls-01 is used by remtau-inf,
nat/ls-02 is used by remtau-inf,
nat/ls-03 is used by remtau-inf,
nat/ls-le-simp is used by remtau-toempty-from, not-lessto, remtau-inf,
nat/succ-01 is used by remtau-empty-equiv, remtau-inf,
nat/zero is used by remtau-inf, to-addone, remtau-equiv,

Used from specification stream

stream/add-list-fun-def is used by remtau-inf,
stream/append-finfin is used by finremtau-cons,
stream/append-gr-to is used by remtau-equiv,
stream/empty is used by finremtau-empty,
stream/extensionality is used by remtau-inf, remtau-equiv,
stream/extensionality-to is used by remtau-equiv,
stream/get-append-ls is used by remtau-toempty-from,
stream/get-append-notls is used by to-addone, remtau-fromempty-to,
stream/hd-selzero is used by to-addone,
stream/intrace-expand is used by remtau-empty-equiv, remtau-inf,
stream/append-assoc is used by remtau-nontau-lem, remtau-split, remtau-split-weak, remtau-split-list-inf, finremtau-cons, remtau-split-one-inf, remtau-split-one, remtau-append-fin, remtau_of_to-to_of_rmtau, remtau-split-fin, remtau-toempty-from, remtau-split-list-weak, remtau-one, remtau-split-list, one-eq-empty, not-lessto, remtau-empty-equiv, remtau-split-inf, remtau-inf, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to, remtau-split-list-fin, remtau-split-one-fin, finremtau-split-fin, remtau-append, remtau-equiv, finremtau-split-weak,
stream/append-cut1 is used by remtau-append-fin,
stream/append-empty is used by remtau-one, remtau-split-list, one-eq-empty, remtau-split-list-fin,
stream/append-empty-01 is used by remtau-split-one, remtau-empty-equiv,
stream/append-fin-is-inf is used by remtau-inf,
stream/append-finfin is used by remtau-split, remtau-split-one, remtau-append-fin, remtau-split-fin, remtau-empty-equiv, remtau-inf, remtau-split-one-fin, finremtau-split-fin,
stream/append-le-to is used by remtau-equiv,
stream/append-split-fin is used by remtau-split, remtau-split-one, remtau_of_to-to_of_rmtau, remtau-split-fin, finremtau-split-fin, remtau-append,
stream/append-to-addsize-01 is used by to-addone,
stream/append-to-size-01 is used by remtau_of_to-to_of_rmtau, to_of_remtau-remtau_of_to,
stream/append-two-is-fin is used by remtau-split-one-fin,
stream/appendend-equal is used by remtau-split-list-weak, remtau-split-list, remtau-fromempty-to,
stream/appfin-sel is used by remtau-split-one-fin,
stream/appinf-sel is used by remtau-inf,
stream/appinf-selfun is used by not-lessto, not-lessto-inf, remtau-equiv,
stream/cons-append is used by remtau-split-one, remtau-empty-equiv, remtau-inf, to-addone,
stream/cons-empty is used by remtau-split-one, remtau-empty-equiv,
stream/cons-eq is used by remtau-nontau-lem, remtau-split-one,
stream/elim-fromto is used by remtau_of_to-to_of_rmtau, remtau-toempty-from, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to,
stream/elim-fromto-inf is used by not-lessto, not-lessto-inf, remtau-equiv,
stream/elim-hd-tl is used by remtau-split-one, to-addone,
stream/empty is used by remtau-split, remtau-split-weak, remtau-split-one, remtau-append-fin, remtau_of_to-to_of_rmtau, remtau-toempty-from, remtau-split-list-weak, remtau-empty-equiv, remtau-inf,
stream/empty-append is used by remtau-split, remtau-split-weak, finremtau-cons, remtau-split-one, remtau-append-fin, remtau_of_to-to_of_rmtau, remtau-toempty-from, remtau-split-list-weak, remtau-empty-equiv,
stream/eq-stream-to-list-2-1 is used by remtau-split, finremtau-cons, remtau-split-fin, remtau-split-one-fin, finremtau-split-fin, finremtau-split-weak,
stream/fin-empty is used by remtau-split, remtau-split-weak, remtau-split-one, remtau-toempty-from, finremtau-empty-equiv, finremtau-empty, one-eq-empty, remtau-empty-equiv, remtau-inf, remtau-split-list-fin, remtau-split-one-fin,
stream/from-inf is used by remtau-toempty-from-inf,
stream/get-append-ls is used by to-addone, remtau-fromempty-to,
stream/get-append-notls is used by remtau-toempty-from,
stream/get-cons-succ is used by remtau-split-one,
stream/get-cons-zero is used by remtau-split-one,
stream/infappone-zero is used by remtau-inf,
stream/neq-fin-inf-01 is used by remtau-split-fin, remtau-split-one-fin, finremtau-split-weak,
stream/neq-fin-inf-03 is used by remtau-split-list-inf, remtau-split-one-inf, remtau-split-inf,
stream/sel-fin is used by remtau-toempty-from, finremtau-empty-equiv, remtau-empty-equiv, remtau-inf, to-addone, remtau-fromempty-to,
stream/sel-inf is used by remtau-empty-equiv, remtau-inf, remtau-toempty-from-inf, remtau-equiv,
stream/size-append is used by remtau-split-one, remtau_of_to-to_of_rmtau, remtau-toempty-from, not-lessto, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to, remtau-equiv,
stream/size-empty-equiv is used by to-addone,
stream/size-fin is used by remtau-split-one, remtau_of_to-to_of_rmtau, remtau-toempty-from, finremtau-empty-equiv, not-lessto, remtau-empty-equiv, remtau-inf, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to, remtau-notless, size-to-less, remtau-equiv,
stream/size-inf is used by not-lessto, remtau-empty-equiv, remtau-inf, remtau-toempty-from-inf, remtau-notless, remtau-equiv,
stream/size-inf-to is used by remtau-equiv,
stream/size-succ is used by remtau-equiv,
stream/to-fin is used by not-lessto, remtau-equiv,
stream/to-inf is used by not-lessto, remtau-equiv,
stream/to-to-eq-inf is used by remtau-equiv,
stream/to-zero is used by remtau_of_to-to_of_rmtau, remtau-equiv,
stream/toone-cons is used by to-addone,
stream/zero-len is used by remtau-split-one,

Used from specification nat-inf

nat-inf/notinf-fin is used by remtau-equiv,
nat-inf/add-all-zero is used by remtau-split-one,
nat-inf/add-assoc is used by remtau-split-one, remtau_of_to-to_of_rmtau, remtau-toempty-from, not-lessto, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to, remtau-equiv,
nat-inf/add-comm is used by remtau-split-one, remtau_of_to-to_of_rmtau, remtau-toempty-from, not-lessto, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to, remtau-equiv,
nat-inf/add-fin is used by remtau-split-one, to-addone, remtau-fromempty-to, remtau-equiv,
nat-inf/add-ls-cancel-01 is used by to-addone, remtau-fromempty-to,
nat-inf/add-ls-cancel-num-04 is used by remtau-split-one,
nat-inf/add-not-less is used by remtau_of_to-to_of_rmtau, remtau-toempty-from, not-lessto, not-lessto-inf, to-addone, to_of_remtau-remtau_of_to, remtau-fromempty-to,
nat-inf/addeqinf-cancel is used by remtau-equiv,
nat-inf/disj-rqui-infty is used by remtau-fromempty-to,
nat-inf/lels-trans is used by size-to-less,
nat-inf/less-fin is used by remtau-toempty-from, finremtau-empty-equiv, ex-first-nontau, not-lessto, remtau-empty-equiv, remtau-inf, to-addone, remtau-notless, remtau-equiv,
nat-inf/less-inf1 is used by not-lessto, remtau-toempty-from-inf, remtau-notless, remtau-equiv,
nat-inf/less-inf2 is used by remtau-empty-equiv, remtau-inf, remtau-equiv,
nat-inf/less-succ-leq is used by remtau-split-one, remtau-equiv,
nat-inf/ls-natinf-to-nat-2-1 is used by to-addone, remtau-fromempty-to,
nat-inf/ls-trans is used by to-addone,
nat-inf/lsle-trans is used by ex-first-nontau, size-to-less,
nat-inf/not-less-zero is used by remtau_of_to-to_of_rmtau,
nat-inf/onels-neqzero is used by to-addone,
nat-inf/sel-rqui-dotn is used by remtau-toempty-from, to-addone, remtau-fromempty-to,

Used from specification stream-basic

stream-basic/disj-rqui-rqui0 is used by remtau-split-list-inf, remtau-split-one-inf, remtau-fin, remtau-split-inf, remtau-split-one-fin,
stream-basic/elim-finp-ant is used by remtau-append-fin, remtau-fin, remtau-inf, remtau-split-one-fin,
stream-basic/elim-finp-suc is used by remtau-fin, remtau-inf, remtau-equiv,
stream-basic/inj-rqui is used by remtau-split, remtau-split-weak, finremtau-cons, remtau_of_to-to_of_rmtau, remtau-split-fin, remtau-one, remtau-split-list, remtau-split-inf, to_of_remtau-remtau_of_to, remtau-split-list-fin, remtau-split-one-fin, finremtau-split-fin, remtau-equiv, finremtau-split-weak,
stream-basic/sel-rqui-dotl is used by remtau-split-one-fin, remtau-equiv,
stream-basic/test-finp-rqui is used by remtau-split-one-fin, remtau-append,

Used from specification list-data

list-data/l is used by remtau-notless-fin, remtau-toempty-from, remtau-empty-equiv, remtau-inf,
list-data/size-nil is used by remtau-notless-fin, remtau-empty-equiv,

Used from specification nat-basic

nat-basic/a is used by remtau-notless-fin, remtau-split-one, not-lessto-fin, remtau-empty-equiv, remtau-inf, to-addone, remtau-fromempty-to, remtau-equiv,
nat-basic/add-base is used by remtau-notless-fin, remtau-inf,
nat-basic/c is used by remtau-notless-fin, remtau-split-one, not-lessto-fin, remtau-empty-equiv, remtau-inf, to-addone, remtau-fromempty-to, remtau-equiv,
nat-basic/f is used by remtau-notless-fin, remtau-toempty-from, ex-first-nontau, remtau-empty-equiv, remtau-inf, remtau-toempty-from-inf,
nat-basic/l is used by remtau-notless-fin, remtau-inf,
nat-basic/l-02 is used by not-lessto-fin, remtau-inf, to-addone, remtau-fromempty-to,
nat-basic/l-05 is used by remtau-inf,
nat-basic/less-zero is used by remtau-split-one, remtau-empty-equiv, remtau-inf,
nat-basic/lf is used by remtau-inf,
nat-basic/ls-02 is used by ex-first-nontau, remtau-inf,
nat-basic/nls-fst is used by remtau-notless-fin,
nat-basic/one-01 is used by remtau-empty-equiv, remtau-inf,
nat-basic/oz is used by remtau-empty-equiv, remtau-inf,
nat-basic/refl-Nat is used by remtau-inf, to-addone, remtau-equiv,
nat-basic/s-04 is used by remtau-split-one, remtau-empty-equiv, remtau-inf,
nat-basic/succ is used by remtau-notless-fin, remtau-split-one, remtau-empty-equiv, remtau-inf,
nat-basic/trans-Nat is used by remtau-inf,

Used from specification list

list/Nil is used by remtau-split, finremtau-cons, remtau-split-one, remtau-one-03, finremtau-append, remtau-split-one-fin,
list/a is used by remtau-notless-fin, remtau-split, finremtau-nontau-lem, finremtau-cons, remtau-split-one, remtau-append-fin, remtau-one-03, remtau-split-fin, not-lessto-fin, remtau-empty-equiv, remtau-inf, finremtau-append, to-addone, remtau-split-one-fin, finremtau-split-fin, remtau-equiv, finremtau-split-weak,
list/app is used by remtau-split, remtau-one-03, remtau-equiv,
list/app-02 is used by remtau-split,
list/c is used by remtau-notless-fin, remtau-split, remtau-split-one, remtau-append-fin, remtau-empty-equiv, remtau-inf, finremtau-append,
list/c-04 is used by remtau-split, finremtau-one, remtau-one-02, remtau-split-one-fin,
list/c-05 is used by remtau-split,
list/e is used by remtau-split, remtau-split-one, one-eq-empty, remtau-empty-equiv, remtau-one-02,
list/in-14 is used by remtau-split-one-fin,
list/in-17 is used by remtau-split-one-fin,
list/in-append is used by remtau-split-one-fin,
list/in-empty is used by remtau-split-one-fin,
list/in-rec is used by remtau-split-one-fin,
list/len is used by remtau-notless-fin, not-lessto-fin,
list/len-01 is used by finremtau-nontau-lem, remtau-split-fin, finremtau-append, to-addone, remtau-split-one-fin, finremtau-split-fin, finremtau-split-weak,
list/len-02 is used by remtau-notless-fin, remtau-split-one, remtau-empty-equiv, remtau-inf,
list/len-05 is used by remtau-notless-fin, remtau-empty-equiv,
list/len-06 is used by remtau-split, remtau-split-one-fin,

Used from specification option

option/disj-Some-None is used by remtau-split, remtau-split-one, remtau-one, remtau-inf, remtau-one-02, remtau-split-one-fin,
option/elim-Some is used by remtau-split-one, remtau-one,
option/sel-Some-dotget is used by remtau-split, remtau-split-one, remtau-one, remtau-one-02, remtau-split-one-fin,

Used from specification list-del

list-del/get-append-grt is used by remtau-empty-equiv,
list-del/elim-firstn-restn is used by not-lessto-fin,
list-del/get-append-less is used by remtau-empty-equiv,
list-del/get-succ is used by remtau-empty-equiv,
list-del/get-zero is used by remtau-empty-equiv,
list-del/one-03 is used by remtau-empty-equiv, remtau-inf,