[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 hpal-reachset-set, finreach-fin,
list-last/l-06 is used by finreach-fin,
list-last/last-01 is used by finreach-fin,
list-last/last-def is used by KoenigsLemma, hpal-next,
list-last/last-elim is used by finreach-fin,
list-last/last-one is used by KoenigsLemma-aux, finreach-fin,

Used from specification nat

nat/add-01 is used by hpal-next,
nat/add-num-01 is used by KoenigsLemma-aux, hpal-next-aux, finreach-fin,
nat/add-num-03 is used by finreach-fin,
nat/anti is used by finreach-fin, hpal-next,
nat/elim-pred-c is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
nat/eqle-one is used by hpal-next,
nat/fle is used by hpal-next-auxh, finreachle-fin,
nat/fle-01 is used by hpal-next-auxh, hpal-reachset-set,
nat/l-num-01 is used by hpal-next-aux, finreach-fin,
nat/le-add is used by finreach-fin,
nat/le-def is used by hpal-reachset-set, finset-nextfin, finreachle-fin, finreach-fin,
nat/le-ls-simp is used by hpal-next-auxh, hpal-next-aux,
nat/lels is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat/lels-02 is used by hpal-reachset-set,
nat/lels-03 is used by hpal-reachset-set, finreach-fin, hpal-next,
nat/lep is used by hpal-next-auxh,
nat/lep-02 is used by finreachle-fin,
nat/ler is used by finreach-fin, hpal-next,
nat/les is used by finreachle-fin, hpal-next,
nat/let is used by hpal-next-auxh, finreach-fin,
nat/lez is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
nat/lez-01 is used by finreachle-fin,
nat/ls-01 is used by hpal-reachset-set, finset-nextfin, finreach-fin,
nat/ls-le-simp is used by hpal-reachset-set,
nat/succ-01 is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
nat/zero is used by finreach-fin, hpal-next,

Used from specification infgraph-gen-basic

infgraph-gen-basic/dom-def is used by finreach-fin,
infgraph-gen-basic/edge-def is used by finreach-fin,

Used from specification set-basic

set-basic/In-empty is used by hpal-next-auxh, hpal-reachset-set, finset-nextfin, finreach-fin,
set-basic/In-insert is used by hpal-next-auxh, finreach-fin,
set-basic/ne-01 is used by hpal-root, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finset-nextfin, finreachle-fin, finreach-fin, hpal-next,
set-basic/size-zero-01 is used by hpal-root, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finset-nextfin, finreachle-fin, finreach-fin, hpal-next,

Used from specification list-getput

list-getput/get-zero-01 is used by hpal-next-auxh, finreach-fin,

Used from specification nat-basic

nat-basic/a is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finset-nextfin, finreachle-fin, finreach-fin, hpal-next,
nat-basic/add-base is used by hpal-next,
nat-basic/c is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finset-nextfin, finreachle-fin, finreach-fin, hpal-next,
nat-basic/eq-01 is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,
nat-basic/f is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreachle-fin, finreach-fin, hpal-next,
nat-basic/l is used by KoenigsLemma, hpal-next-auxh, hpal-next,
nat-basic/l-02 is used by hpal-next-auxh, hpal-next-aux, finreachle-fin,
nat-basic/l-05 is used by hpal-next-auxh,
nat-basic/l-08 is used by hpal-next-auxh,
nat-basic/less-zero is used by KoenigsLemma-aux, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-basic/lf is used by hpal-next-auxh, hpal-reachset-set,
nat-basic/lf-01 is used by hpal-next,
nat-basic/lf-02 is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
nat-basic/ls-02 is used by hpal-next-auxh, finreach-fin,
nat-basic/nls-fst is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
nat-basic/one-01 is used by KoenigsLemma-aux, hpal-next-auxh, hpal-reachset-set, finset-nextfin, finreach-fin, hpal-next,
nat-basic/oz is used by hpal-next-auxh, hpal-reachset-set, finreach-fin, hpal-next,
nat-basic/refl-Nat is used by KoenigsLemma, hpal-reachset-set, finset-nextfin, finreach-fin, hpal-next,
nat-basic/s-04 is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finset-nextfin, finreach-fin, hpal-next,
nat-basic/succ is used by KoenigsLemma-aux, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreachle-fin, finreach-fin,
nat-basic/trans-Nat is used by hpal-next-auxh, hpal-reachset-set,
nat-basic/z-01 is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-aux, finreach-fin,
nat-basic/zero is used by hpal-next-auxh, hpal-reachset-set, finreach-fin, hpal-next,

Used from specification list

list/Last is used by finreach-fin,
list/Nil is used by finreach-fin,
list/a is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list/app is used by finreach-fin, hpal-next,
list/app-02 is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,
list/c is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list/c-03 is used by finreach-fin, hpal-next,
list/c-04 is used by hpal-next,
list/c-06 is used by finreach-fin,
list/c-08 is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
list/e is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list/first is used by finreach-fin,
list/in-14 is used by finreach-fin,
list/in-15 is used by KoenigsLemma-aux, KoenigsLemma, finreach-fin,
list/in-17 is used by KoenigsLemma, finreach-fin,
list/in-append is used by KoenigsLemma, finreach-fin,
list/in-empty is used by finreach-fin,
list/in-rec is used by finreach-fin,
list/len is used by KoenigsLemma-aux, hpal-next-auxh, finreach-fin,
list/len-01 is used by hpal-next,
list/len-02 is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list/len-05 is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,

Used from specification set-union

set-union/Delete is used by hpal-reachset-set, finset-nextfin, finreach-fin,
set-union/Union is used by hpal-reachset-set, finset-nextfin, finreachle-fin,
set-union/del-size is used by hpal-reachset-set, finset-nextfin, finreach-fin,
set-union/una is used by hpal-reachset-set, finset-nextfin, finreachle-fin,
set-union/unc is used by hpal-reachset-set, finset-nextfin, finreachle-fin,

Used from specification stream

stream/append-assoc is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/append-empty is used by finreach-fin,
stream/append-finfin is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/empty is used by finreach-fin,
stream/get-append2-fin is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/get-append3-fin is used by hpal-next-auxh, hpal-next-aux, finreach-fin,
stream/get-cons-succ is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,
stream/sel-fin is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/sel-inf is used by KoenigsLemma,
stream/size-append is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/size-fin is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
stream/size-inf is used by KoenigsLemma,
stream/to-succ-cons-l-lem is used by hpal-next-auxh, hpal-reachset-set,

Used from specification nat-inf

nat-inf/add-all-zero is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/add-assoc is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/add-comm is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/add-fin is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/add-ls-cancel-num-03 is used by KoenigsLemma-aux, finreach-fin, hpal-next,
nat-inf/add-ls-cancel-num-04 is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/addeqinf-cancel is used by KoenigsLemma,
nat-inf/disj-rqui-infty is used by KoenigsLemma,
nat-inf/inf-less is used by KoenigsLemma,
nat-inf/less-fin is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/less-inf2 is used by KoenigsLemma,
nat-inf/less-succ-leq is used by KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
nat-inf/ls-natinf-to-nat-1-2 is used by hpal-next-auxh, hpal-next-aux, finreach-fin,
nat-inf/ls-natinf-to-nat-2-1 is used by KoenigsLemma, hpal-next-auxh, hpal-next,
nat-inf/num-add is used by hpal-next-aux, finreach-fin,

Used from specification list-data

list-data/elim-add is used by hpal-reachset-set,
list-data/elim-list-c is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list-data/l is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,
list-data/lf-01 is used by finreach-fin, hpal-next,
list-data/size-nil is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-aux, finreach-fin,

Used from specification list-del

list-del/get-append-grt is used by hpal-reachset-set, finreach-fin, hpal-next,
list-del/get-append-less is used by hpal-next-auxh, hpal-reachset-set, finreach-fin, hpal-next,
list-del/get-firstn is used by hpal-reachset-set,
list-del/get-last-nonempty is used by hpal-next,
list-del/elim-firstn-restn is used by hpal-next-auxh,
list-del/firstn-length-03 is used by hpal-reachset-set,
list-del/firstn-length-04 is used by hpal-next-auxh,
list-del/get-append-grt is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
list-del/get-append-less is used by hpal-next-auxh, hpal-reachset-set, finreach-fin,
list-del/get-butlast is used by KoenigsLemma, finreach-fin, hpal-next,
list-del/get-last is used by KoenigsLemma, finreach-fin, hpal-next,
list-del/get-last-03 is used by finreach-fin,
list-del/get-last-04 is used by finreach-fin,
list-del/get-succ is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,
list-del/get-zero is used by hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin,
list-del/one-03 is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-reachset-set, finreach-fin, hpal-next,

Used from specification infgraph-gen

infgraph-gen/isroot-def is used by KoenigsLemma-aux,
infgraph-gen/path-def is used by hpal-reachset-set,
infgraph-gen/pathp-def is used by KoenigsLemma-aux, KoenigsLemma, hpal-next-auxh, hpal-next-aux, hpal-reachset-set, finreach-fin, hpal-next,