[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/prefix is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, montrl-equiv,
list-last/prefix-eq is used by conttr-relative-thm, conttr-thm,
list-last/prefix-equality is used by cont-thm, cont-relative-thm,
list-last/prefix-app-size-eq is used by pconttr-lifted, monl-equiv, lift-pcont, pcont-lifted, lifttr-pcont, montrl-equiv,
list-last/prefix-eq is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont,
list-last/prefix-longer-01 is used by monl-equiv, montrl-equiv,
list-last/prefix-size-eq is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, twomon-limsize,
list-last/prefix-trans is used by pconttr-lifted, lifttr-cont, lift-pcont, pcont-lifted, lifttr-pcont, lift-cont,

Used from specification nat

nat/eqle-one is used by montrl-equiv,
nat/fle is used by montrl-equiv,
nat/fle-01 is used by monl-equiv, montrl-equiv,
nat/le-def is used by monl-equiv, conttr-relative-thm, conttr-thm, pfxclosed-lift, montrl-equiv,
nat/lels is used by monl-equiv, montrl-equiv,
nat/lels-03 is used by conttr-relative-thm, conttr-thm,
nat/ler is used by pfxclosed-lift,
nat/ls-le-simp is used by monl-equiv, montrl-equiv,
nat/zero is used by pfxclosed-lift,

Used from specification stream

stream/add-list-fun-def is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm,
stream/extensionality is used by twomon-limsize,
stream/infapp-to-ge is used by pfxclosed-lift,
stream/leq-trans is used by conttr-relative-thm, conttr-thm,
stream/prefix-def is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift, twomon-limsize,
stream/to-unwind-end-inf is used by pconttr-lifted, monl-equiv, lift-pcont, pcont-lifted, lifttr-pcont, montrl-equiv,
stream/to-unwind-end-inf2 is used by pconttr-lifted, lifttr-pcont, montrl-equiv,
stream/append-assoc is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift, twomon-limsize,
stream/append-fin-is-inf is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, pfxclosed-lift,
stream/append-finfin is used by monl-equiv, conttr-relative-thm, conttr-thm, twomon-limsize,
stream/append-split-fin is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-rel-thm, lifttr-pcont, lift-cont,
stream/append-two-is-fin is used by conttr-relative-thm, conttr-thm, twomon-limsize,
stream/appinf-sel is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-rel-thm, lifttr-pcont, lift-cont,
stream/elim-fromto-inf is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-rel-thm, lifttr-pcont, lift-cont,
stream/eq-stream-to-list-2-1 is used by monl-equiv, conttr-relative-thm, conttr-thm,
stream/fin-finlen-tolen is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
stream/fun-nonempty is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
stream/get-infto is used by monl-equiv, conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, montrl-equiv,
stream/inf-size-to is used by conttr-relative-thm, conttr-thm, twomon-limsize,
stream/inf-take-prefix is used by conttr-relative-thm, cont-relative-thm,
stream/infapp-embed is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont,
stream/leq-append-right is used by monl-equiv, conttr-relative-thm, conttr-thm,
stream/leq-refl is used by pconttr-lifted, lifttr-cont, lift-pcont, pcont-lifted, lifttr-pcont, lift-cont,
stream/leq-symm-2 is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, twomon-limsize,
stream/leq-trans is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont,
stream/neq-fin-inf-01 is used by monl-equiv,
stream/not-prefix-inf-fin is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift,
stream/prefix-bothfin-listprefix is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift, twomon-limsize, montrl-equiv,
stream/prefix-inf-inf-equal is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, cont-rel-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift,
stream/sel-inf is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,
stream/size-append is used by twomon-limsize,
stream/size-fin is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
stream/size-inf is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,
stream/size-inf-to is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, montrl-equiv,
stream/to-fin is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
stream/to-inf is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
stream/to-zero-nf is used by pfxclosed-lift,

Used from specification nat-inf

nat-inf/add-all-zero is used by conttr-relative-thm, conttr-thm,
nat-inf/add-assoc is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, twomon-limsize, montrl-equiv,
nat-inf/add-cancel-01 is used by twomon-limsize,
nat-inf/add-cancel-03 is used by twomon-limsize,
nat-inf/add-cancel-num-02 is used by twomon-limsize,
nat-inf/add-cancel-num-03 is used by conttr-relative-thm, conttr-thm,
nat-inf/add-comm is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, twomon-limsize, montrl-equiv,
nat-inf/add-fin is used by conttr-relative-thm, conttr-thm, twomon-limsize,
nat-inf/add-inf2 is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, conttr-thm, lifttr-pcont, twomon-limsize,
nat-inf/addeqinf-cancel is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, twomon-limsize, montrl-equiv,
nat-inf/disj-rqui-infty is used by pconttr-lifted, monl-equiv, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, twomon-limsize, montrl-equiv,
nat-inf/eq-natinf-to-nat-2-1 is used by pconttr-lifted, pfxclosed-lift-tr, conttr-rel-thm, conttr-relative-thm, lifttr-cont, conttr-thm, lifttr-pcont, twomon-limsize,
nat-inf/inf-inseq-reduce is used by twomon-limsize,
nat-inf/inf-less is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, montrl-equiv,
nat-inf/inj-rqui is used by conttr-relative-thm, conttr-thm,
nat-inf/less-fin is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
nat-inf/less-inf1 is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
nat-inf/less-inf2 is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,
nat-inf/ls-natinf-to-nat-2-1 is used by conttr-relative-thm, conttr-thm,
nat-inf/sum-zero-fin is used by twomon-limsize,

Used from specification stream-basic

stream-basic/disj-rqui-rqui0 is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm,
stream-basic/elim-finp-ant is used by conttr-relative-thm, conttr-thm, twomon-limsize,
stream-basic/elim-finp-suc is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, pfxclosed-lift,
stream-basic/inj-rqui is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm,
stream-basic/inj-rqui0 is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm,
stream-basic/sel-rqui-dotl is used by conttr-relative-thm, conttr-thm, twomon-limsize,
stream-basic/sel-rqui0-dotf is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, pfxclosed-lift,

Used from specification list-data

list-data/l is used by monl-equiv, conttr-relative-thm, conttr-thm, twomon-limsize, montrl-equiv,

Used from specification nat-basic

nat-basic/a is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,
nat-basic/c is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,
nat-basic/eq-01 is used by pconttr-lifted, monl-equiv, lifttr-pcont, montrl-equiv,
nat-basic/eq-02 is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
nat-basic/f is used by monl-equiv, conttr-relative-thm, fun-neq, conttr-thm, twomon-limsize, montrl-equiv,
nat-basic/l is used by twomon-limsize,
nat-basic/l-02 is used by monl-equiv, twomon-limsize, montrl-equiv,
nat-basic/l-06 is used by montrl-equiv,
nat-basic/lf is used by montrl-equiv,
nat-basic/lf-01 is used by twomon-limsize, montrl-equiv,
nat-basic/neq-01 is used by twomon-limsize,
nat-basic/refl-Nat is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift, twomon-limsize,
nat-basic/s-04 is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm, montrl-equiv,
nat-basic/succ is used by montrl-equiv,
nat-basic/trans-Nat is used by montrl-equiv,
nat-basic/z-01 is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont,

Used from specification list

list/a is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, pfxclosed-lift, twomon-limsize, montrl-equiv,
list/app is used by pfxclosed-lift,
list/app-04 is used by conttr-relative-thm, conttr-thm,
list/len is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize, montrl-equiv,

Used from specification list-del

list-del/get-append-less is used by monl-equiv, montrl-equiv,

Used from specification list-getput

list-getput/extension is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, montrl-equiv,

Used from specification streamseq-mon-lim

streamseq-mon-lim/equal-prepostfix is used by conttr-relative-thm, cont-thm, cont-relative-thm, conttr-thm,
streamseq-mon-lim/lim-def is used by pconttr-lifted, conttr-relative-thm, lifttr-cont, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, lift-cont, twomon-limsize,
streamseq-mon-lim/mon-def is used by pconttr-lifted, monl-equiv, conttr-relative-thm, lift-pcont, pcont-lifted, cont-thm, cont-relative-thm, conttr-thm, lifttr-pcont, montrl-equiv,
streamseq-mon-lim/mon-lem is used by monl-equiv, conttr-relative-thm, conttr-thm, montrl-equiv,