[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/postfix is used by rely-FOFollowsW-stable, B-postfix-weak-one, rely-noPendingW-stable,
list-last/postfix-in-01 is used by B-postfix-weak-same-loc, B-postfix-weak-not-in-stable,
list-last/postfix-rec-right is used by B-postfix-weak-FOWs-postfix,
list-last/bin-01 is used by SFTrainling-prop-FO, SFTrailing-tail, SFTrailing-attach,
list-last/bin-02 is used by SFTrainling-prop-FO,
list-last/butlast-def is used by SFTrailing-attach,
list-last/last-elim is used by SFTrailing-leading-SF, SFTrainling-prop-FO, SFTrailing-tail,
list-last/lin-02 is used by SFTrainling-prop-FO,
list-last/postfix-app is used by B-postfix-weak-same-loc,
list-last/postfix-app-01 is used by rely-persist, B-postfix-weak-append, B-postfix-weak-delpos-propFO,
list-last/postfix-app-02 is used by rely-persist, rely-prop-W, rely-prop-SF, rely-prop-FO, rely-update-other-bq, rely-refl,
list-last/postfix-empty is used by B-postfix-weak-delpos-propFO, B-postfix-weak-one, B-postfix-weak-empty,
list-last/postfix-empty-03 is used by rely-noPending-stable-strong, B-postfix-weak-of-empty, B-postfix-weak-FOWs-postfix, B-postfix-weak-one, rely-noPending-stable,
list-last/postfix-reflexivity is used by rely-persist, B-postfix-weak-refl, B-postfix-weak-delpos-propFO, rely-prop-W, B-postfix-weak-FOWs-postfix, rely-prop-SF, B-postfix-weak-one, rely-prop-FO, rely-update-other-bq, rely-refl,

Used from specification forall-indexWhere

forall-indexWhere/filter-forall is used by B-postfix-weak-same-loc-postfix,
forall-indexWhere/forall-in-def is used by B-postfix-weak-same-loc, FOs-not-one-W,
forall-indexWhere/forall-append is used by readFOsOk-add-FO,
forall-indexWhere/forall-base is used by B-postfix-weak-same-loc,
forall-indexWhere/forall-one is used by readFOsOk-add-FO, readFOsOk-not-one-SF, FOs-not-one-SF, readFOsOk-not-one-W,
forall-indexWhere/forall-rec is used by B-postfix-weak-same-loc, FOs-not-leading-W, readFOsOk-not-leading-W,
forall-indexWhere/forall-rmpos is used by readFOsOk-prop-FO,

Used from specification nat

nat/add-01 is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/anti is used by isPropFO-delpos-last-SF,
nat/elim-pred-c is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/eqle-one is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/fle is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/fle-01 is used by isPropFO-other-FO-in-delpos, isPropFO-rec, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/le-def is used by pendingOk-prop-FO, isPropFO-other-FO-in-delpos, rely-FOFollowsW-stable, pendingOk-persist, pendingOk-add-SF, pendingOk-add-FO, isPropFO-SF-in-delpos, isPropFO-W-in-delpos, pendingOk-prop-W, pendingOk-add-pending, pendingOk-empty-bq,
nat/le-ls-simp is used by isPropFO-other-FO-in-delpos, rely-FOFollowsW-stable, isPropFO-W-in-delpos,
nat/lels is used by isPropFO-drop-last-SF, isPropFO-other-FO-in-delpos, rely-FOFollowsW-stable, isPropFO-delpos-last-SF, B-postfix-weak-delpos-propFO, isPropFO-rec, SFTrainling-prop-FO, isPropFO-SF-in-delpos, isPropFO-leading-SF, isPropFO-W-in-delpos, isPropFO-not-leading-W,
nat/lels-02 is used by pendingOk-prop-FO, isPropFO-drop-last-SF, pendingOk-persist, pendingOk-prop-W, pendingOk-add-pending,
nat/lep-02 is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/leprf is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/les is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/let is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/lez is used by isPropFO-other-FO-in-delpos, isPropFO-rec, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/lez-01 is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/ls is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/ls-01 is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
nat/ls-le-simp is used by isPropFO-other-FO-in-delpos, rely-FOFollowsW-stable, isPropFO-W-in-delpos,
nat/one-01 is used by pendingOk-persist, pendingOk-no-two-buffered-Ws, pendingOk-prop-W, pendingOk-empty-bq,
nat/one-02 is used by pendingOk-prop-FO, pendingOk-persist, pendingOk-add-SF, pendingOk-add-FO, pendingOk-prop-W, pendingOk-add-pending, pendingOk-empty-bq,
nat/pred-03 is used by pendingOk-empty-bq,
nat/succ-01 is used by isPropFO-rec,
nat/zero is used by SFTrainling-prop-FO,

Used from specification FLITPSC-preds

FLITPSC-preds/filter-W-append is used by writersOk-persist,
FLITPSC-preds/filter-W-t-swap is used by writersok-rm-writer, noPending-then-noPendingW, pendingOk-add-pending, rely-noPendingW-stable,
FLITPSC-preds/filter-t-split is used by rely-FOFollowsW-stable,
FLITPSC-preds/filterwrites-def is used by rely-noPendingW-stable,
FLITPSC-preds/filter-W-append is used by pendingOk-prop-FO, pendingOk-persist, writersOk-prop-FO, FOWs-loc-empty, pendingOk-prop-W, writersOk-prop-W, rely-noPendingW-stable,
FLITPSC-preds/filter-W-one-fo is used by pendingOk-prop-FO, writersOk-prop-FO, FOWs-loc-empty,
FLITPSC-preds/filter-W-one-w is used by pendingOk-prop-W, writersOk-prop-W,
FLITPSC-preds/filter-t-append is used by rely-persist, rely-FOFollowsW-stable, pendingOk-persist, writersOk-persist, rely-prop-W, rely-prop-FO, pendingOk-prop-W, writersOk-prop-W,
FLITPSC-preds/filter-t-one is used by rely-persist, rely-FOFollowsW-stable, rely-prop-W, rely-prop-FO, pendingOk-prop-W, writersOk-prop-W,
FLITPSC-preds/filter-w-empty is used by FOWs-loc-empty, writersok-rm-writer, noPending-then-noPendingW, pendingOk-add-pending,
FLITPSC-preds/notMember-not-in is used by readFOsOk-add-FO, writersok-add-writer,
FLITPSC-preds/onemember-eq is used by writersok-add-pending, writersok-rm-writer,

Used from specification set-basic

set-basic/In-insert is used by writersok-add-writer, readFOsOk-add-writer,
set-basic/add is used by writersok-add-writer,
set-basic/ne is used by writersok-add-writer, readFOsOk-add-writer,
set-basic/ne-01 is used by readFOsOk-add-FO, writersok-add-pending, writersOk-prop-FO, writersOk-add-SF, writersOk-persist, readFOsOk-prop-FO, readFOsOk-rm-writer, writersOk-add-FO, writersok-add-writer, writersok-rm-writer, readFOsOk-add-writer, readFOsOk-empty-rfo-while-writing, writersOk-empty-bq, writersOk-prop-W,
set-basic/size-zero is used by readFOsOk-rm-writer, writersok-add-writer, writersok-rm-writer, readFOsOk-add-writer,
set-basic/size-zero-01 is used by readFOsOk-add-FO, writersok-add-pending, writersOk-prop-FO, writersOk-add-SF, writersOk-persist, readFOsOk-prop-FO, readFOsOk-rm-writer, writersOk-add-FO, writersok-add-writer, writersok-rm-writer, readFOsOk-add-writer, readFOsOk-empty-rfo-while-writing, writersOk-empty-bq, writersOk-prop-W,

Used from specification list-getput

list-getput/get-zero-01 is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,

Used from specification nat-basic

Used from specification list

list/append-size-less is used by rely-FOFollowsW-stable,
list/append-size-less-eq is used by rely-FOFollowsW-stable,
list/elim-first is used by rely-noPending-stable-strong,
list/in-def is used by rely-FOFollowsW-stable, pendingOk-no-two-buffered-Ws,
list/lastdiv-rew is used by SFTrailing-leading-SF,
list/some-element is used by rely-noPendingW-stable,
list/Nil is used by B-postfix-weak-same-loc, rely-FOFollowsW-stable, isPropFO-FOWs-delpos-tail, FOWs-append, isPropFO-cons-leading-FO, rely-prop-W, restrict-SF-eq-FOWs-eq, B-postfix-weak-FOWs-postfix, B-postfix-weak-one, isPropFO-restrict-SF-l-head, FOWs-W-split, rely-prop-FO, pendingOk-prop-W, oplus-v-append, FOWs-FO-split,
list/a is used by B-postfix-weak-same-loc, rely-persist, pendingOk-prop-FO, isPropFO-drop-last-SF, readFOsOk-add-FO, rely-FOFollowsW-stable, B-postfix-weak-one-ws, isPropFO-FOWs-delpos-tail, SFTrailing-leading-SF, pendingOk-persist, FOWs-append, pendingOk-add-SF, writersok-add-pending, isPropFO-delpos-last-SF, noPending-no-leading-bq-W, writersOk-prop-FO, isPropFO-cons-leading-FO, pendingOk-no-two-buffered-Ws, FOs-not-leading-W, rely-noPending-stable-strong, isPropFO-restrict-delpos, writersOk-add-SF, noPendingW-no-leading-bq-W, writersOk-persist, B-postfix-weak-append, pendingOk-add-FO, B-postfix-weak-delpos-propFO, B-postfix-weak-of-empty, FOWs-loc-empty, rely-prop-W, isPropFO-rec, FOWs-one-W, SFTrainling-prop-FO, writersOk-add-FO, restrict-SF-eq-FOWs-eq, readFOsOk-not-leading-W, oplus-v-one-SF, B-postfix-weak-FOWs-postfix, rely-prop-SF, isPropFO-leading-SF, B-postfix-weak-one, rely-noPending-stable, noPendingW-add-SF, oplus-v-one-FO, isPropFO-not-leading-W, FOWs-one-SF, isPropFO-restrict-SF-l-head, FOWs-W-split, rely-prop-FO, isPropFO-not-leading-FO, noPendingW-add-FO, rely-update-other-bq, rely-refl, pendingOk-prop-W, SFTrailing-tail, SFTrailing-attach, restrict-l-append, pendingOk-add-pending, FOWs-one-FO, writersOk-prop-W, oplus-v-one-W, oplus-v-append, rely-noPendingW-stable, isPropFO-FOWs-delpos-other, FO-in-FOWs, FOWs-FO-split, W-in-FOWs,
list/app is used by pendingOk-prop-FO, rely-FOFollowsW-stable, B-postfix-weak-one-ws, pendingOk-persist, pendingOk-add-SF, writersOk-prop-FO, rely-noPending-stable-strong, writersOk-add-SF, pendingOk-add-FO, FOWs-one-W, writersOk-add-FO, oplus-v-one-SF, rely-prop-SF, B-postfix-weak-one, rely-noPending-stable, noPendingW-add-SF, oplus-v-one-FO, FOWs-one-SF, noPendingW-add-FO, pendingOk-prop-W, pendingOk-add-pending, FOWs-one-FO, oplus-v-one-W, rely-noPendingW-stable,
list/app-02 is used by readFOsOk-add-FO, rely-FOFollowsW-stable, B-postfix-weak-one-ws, SFTrailing-leading-SF, writersok-add-pending, noPending-no-leading-bq-W, isPropFO-cons-leading-FO, rely-noPending-stable-strong, noPendingW-no-leading-bq-W, writersOk-persist, B-postfix-weak-delpos-propFO, B-postfix-weak-of-empty, FOWs-loc-empty, SFTrainling-prop-FO, restrict-SF-eq-FOWs-eq, B-postfix-weak-FOWs-postfix, B-postfix-weak-one, FOWs-W-split, pendingOk-prop-W, SFTrailing-tail, SFTrailing-attach, pendingOk-add-pending, writersOk-prop-W, rely-noPendingW-stable, FOWs-FO-split,
list/app-05 is used by isPropFO-restrict-delpos, restrict-SF-eq-FOWs-eq, isPropFO-FOWs-delpos-other,
list/app-06 is used by SFTrainling-prop-FO,
list/c is used by B-postfix-weak-same-loc, pendingOk-prop-FO, rely-FOFollowsW-stable, B-postfix-weak-one-ws, isPropFO-FOWs-delpos-tail, pendingOk-persist, FOWs-append, isPropFO-cons-leading-FO, pendingOk-no-two-buffered-Ws, isPropFO-restrict-delpos, B-postfix-weak-delpos-propFO, B-postfix-weak-of-empty, FOWs-loc-empty, restrict-SF-eq-FOWs-eq, B-postfix-weak-FOWs-postfix, B-postfix-weak-one, isPropFO-restrict-SF-l-head, FOWs-W-split, pendingOk-prop-W, pendingOk-add-pending, oplus-v-append, isPropFO-FOWs-delpos-other, FO-in-FOWs, FOWs-FO-split, W-in-FOWs,
list/c-03 is used by B-postfix-weak-one-ws, pendingOk-add-pending,
list/c-04 is used by B-postfix-weak-one-ws, isPropFO-cons-leading-FO, restrict-l-W-same,
list/c-05 is used by B-postfix-weak-one,
list/c-06 is used by rely-FOFollowsW-stable, restrict-SF-eq-FOWs-eq, FOWs-W-split, FOWs-FO-split,
list/c-07 is used by isPropFO-FOWs-delpos-tail, isPropFO-cons-leading-FO, isPropFO-restrict-SF-l-head,
list/e is used by pendingOk-prop-FO, readFOsOk-add-FO, rely-FOFollowsW-stable, B-postfix-weak-one-ws, SFTrailing-leading-SF, pendingOk-persist, noPending-no-leading-bq-W, isPropFO-cons-leading-FO, rely-noPending-stable-strong, noPendingW-no-leading-bq-W, B-postfix-weak-delpos-propFO, B-postfix-weak-of-empty, FOWs-loc-empty, SFTrainling-prop-FO, restrict-SF-eq-FOWs-eq, B-postfix-weak-FOWs-postfix, B-postfix-weak-one, FOWs-W-split, pendingOk-prop-W, SFTrailing-tail, SFTrailing-attach, pendingOk-add-pending, writersOk-prop-W, isPropFO-FOWs-delpos-other, FOWs-FO-split,
list/eq-03 is used by SFTrailing-leading-SF, SFTrailing-tail,
list/eq-04 is used by B-postfix-weak-one,
list/in-06 is used by SFTrailing-leading-SF,
list/in-11 is used by SFTrailing-tail, SFTrailing-attach,
list/in-12 is used by SFTrailing-tail,
list/in-13 is used by rely-FOFollowsW-stable,
list/in-14 is used by rely-persist, rely-FOFollowsW-stable, SFTrailing-leading-SF, pendingOk-persist, noPending-no-leading-bq-W, pendingOk-no-two-buffered-Ws, FOs-not-leading-W, rely-noPending-stable-strong, noPendingW-no-leading-bq-W, writersOk-persist, B-postfix-weak-delpos-propFO, rely-prop-W, restrict-SF-eq-FOWs-eq, readFOsOk-not-leading-W, B-postfix-weak-FOWs-postfix, FOWs-W-split, pendingOk-prop-W, SFTrailing-tail, pendingOk-add-pending, writersOk-prop-W, FOWs-FO-split,
list/in-15 is used by SFTrailing-leading-SF, SFTrainling-prop-FO, SFTrailing-tail,
list/in-17 is used by FOs-not-one-W, SFTrainling-prop-FO, pendingOk-add-pending, FO-in-FOWs, W-in-FOWs,
list/in-append is used by rely-FOFollowsW-stable, SFTrainling-prop-FO, FOWs-W-split, FO-in-FOWs, FOWs-FO-split, W-in-FOWs,
list/in-empty is used by rely-FOFollowsW-stable, FOWs-W-split, FO-in-FOWs, W-in-FOWs,
list/in-rec is used by B-postfix-weak-same-loc, rely-persist, rely-FOFollowsW-stable, pendingOk-persist, FOs-not-leading-W, rely-noPending-stable-strong, rely-prop-W, restrict-SF-eq-FOWs-eq, readFOsOk-not-leading-W, FOWs-W-split, pendingOk-prop-W, FO-in-FOWs, FOWs-FO-split, W-in-FOWs,
list/inapp-02 is used by FOWs-W-split, FOWs-FO-split,
list/len is used by isPropFO-drop-last-SF, rely-FOFollowsW-stable, pendingOk-persist, isPropFO-delpos-last-SF, pendingOk-no-two-buffered-Ws, SFTrainling-prop-FO, pendingOk-prop-W, pendingOk-add-pending,
list/len-01 is used by FOWs-append, isPropFO-cons-leading-FO, isPropFO-restrict-delpos, restrict-SF-eq-FOWs-eq, FOWs-W-split, isPropFO-FOWs-delpos-other, FOWs-FO-split,
list/len-02 is used by isPropFO-drop-last-SF, isPropFO-delpos-last-SF, SFTrainling-prop-FO, pendingOk-prop-W, pendingOk-add-pending,
list/len-05 is used by rely-FOFollowsW-stable, isPropFO-FOWs-delpos-tail, pendingOk-no-two-buffered-Ws, isPropFO-restrict-delpos, isPropFO-rec, isPropFO-leading-SF, isPropFO-not-leading-W, isPropFO-restrict-SF-l-head, isPropFO-not-leading-FO, pendingOk-prop-W,
list/len-06 is used by rely-FOFollowsW-stable, isPropFO-cons-leading-FO, restrict-l-append,
list/neq is used by rely-FOFollowsW-stable,

Used from specification FOW

FOW/disj-FO-W is used by isPropFO-cons-leading-FO, FOWs-W-split, FO-in-FOWs, FOWs-FO-split, W-in-FOWs,
FOW/inj-FO is used by FO-in-FOWs,
FOW/inj-W is used by FOWs-W-split, W-in-FOWs,
FOW/sel-FO-dottid is used by rely-FOFollowsW-stable, rely-prop-FO,
FOW/sel-W-dottid is used by rely-FOFollowsW-stable, rely-prop-W, pendingOk-prop-W, writersOk-prop-W,
FOW/test-dotWque-W is used by rely-noPendingW-stable,

Used from specification set-union

set-union/Delete is used by readFOsOk-rm-writer, writersok-rm-writer,
set-union/del-e-02 is used by readFOsOk-rm-writer, writersok-rm-writer,

Used from specification list-data

list-data/le-one is used by pendingOk-prop-FO, pendingOk-persist, pendingOk-add-SF, pendingOk-add-FO, pendingOk-prop-W, pendingOk-add-pending, pendingOk-empty-bq,
list-data/length-rest-intro is used by pendingOk-empty-bq,
list-data/elim-add is used by pendingOk-add-pending,
list-data/elim-list-c is used by B-postfix-weak-delpos-propFO,
list-data/l is used by pendingOk-prop-FO, isPropFO-drop-last-SF, isPropFO-other-FO-in-delpos, rely-FOFollowsW-stable, pendingOk-persist, pendingOk-add-SF, pendingOk-add-FO, B-postfix-weak-delpos-propFO, isPropFO-rec, SFTrainling-prop-FO, isPropFO-SF-in-delpos, isPropFO-W-in-delpos, isPropFO-restrict-SF-l-head, isPropFO-not-leading-FO, pendingOk-prop-W, pendingOk-add-pending, pendingOk-empty-bq,
list-data/le-one is used by pendingOk-add-pending,
list-data/length-rest is used by pendingOk-empty-bq,
list-data/lf-01 is used by pendingOk-prop-FO, pendingOk-persist, pendingOk-prop-W, pendingOk-add-pending,
list-data/size-nil is used by isPropFO-empty, pendingOk-add-pending, pendingOk-empty-bq,

Used from specification filter-count

Used from specification Bevent

Used from specification list-del

list-del/delpos-append-size-lt is used by isPropFO-delpos-last-SF, SFTrainling-prop-FO,
list-del/in-get is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
list-del/delpos-base is used by isPropFO-FOWs-delpos-tail, isPropFO-restrict-delpos, isPropFO-restrict-SF-l-head, isPropFO-FOWs-delpos-other,
list-del/delpos-empty is used by isPropFO-other-FO-in-delpos, isPropFO-FOWs-delpos-tail, isPropFO-restrict-delpos, readFOsOk-prop-FO, SFTrainling-prop-FO, isPropFO-W-in-delpos, isPropFO-restrict-SF-l-head, isPropFO-FOWs-delpos-other,
list-del/delpos-rec is used by isPropFO-FOWs-delpos-tail, isPropFO-restrict-delpos, isPropFO-restrict-SF-l-head, isPropFO-FOWs-delpos-other,
list-del/get-append-grt is used by SFTrainling-prop-FO,
list-del/get-butlast is used by isPropFO-drop-last-SF, SFTrainling-prop-FO,
list-del/get-last is used by isPropFO-delpos-last-SF,
list-del/get-last-03 is used by isPropFO-drop-last-SF,
list-del/get-succ is used by isPropFO-rec, isPropFO-restrict-SF-l-head, isPropFO-not-leading-FO,
list-del/get-zero is used by isPropFO-FOWs-delpos-tail, isPropFO-cons-leading-FO, isPropFO-restrict-delpos, isPropFO-rec, isPropFO-leading-SF, isPropFO-not-leading-W, isPropFO-restrict-SF-l-head, isPropFO-not-leading-FO, isPropFO-FOWs-delpos-other,
list-del/one-03 is used by SFTrainling-prop-FO,
list-del/rmpos-get is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
list-del/rmpos-not-in is used by SFTrainling-prop-FO,
list-del/rmpos-size is used by isPropFO-other-FO-in-delpos, isPropFO-SF-in-delpos, isPropFO-W-in-delpos,
list-del/rmtoobigpos is used by isPropFO-delpos-last-SF, B-postfix-weak-delpos-propFO,