[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 forall-indexWhere

forall-indexWhere/filter-forall is used by rely-persist-FO-weak,
forall-indexWhere/forall-get-def is used by rely-persist-FO-weak,
forall-indexWhere/indexWhere-rec1 is used by at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, firstPersistW-rec-W,
forall-indexWhere/indexWhere-rec2 is used by firstPersistW-rec-FO, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO,
forall-indexWhere/exists-base is used by firstPersistW-lt-filter-W-empty,
forall-indexWhere/exists-rec is used by firstPersistW-lt-filter-W-empty,
forall-indexWhere/indexWhere-base is used by fo-in-del-firstPersistW, firstPersistW-base,
forall-indexWhere/indexWhere-length-eq is used by firstPersistW-lt-filter-W-empty,
forall-indexWhere/indexWhere-rec1 is used by firstPersistW-rec-FO, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO,
forall-indexWhere/indexWhere-rec2 is used by at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, firstPersistW-rec-W,

Used from specification nat

nat/anti is used by one-pending-del-persist-FO-no-pending,
nat/elim-pred-c is used by one-pending-del-persist-FO-no-pending,
nat/elim-sub is used by rely-fo-follows-w-stable,
nat/eqle-one is used by take-firstPersistW-filter-FO,
nat/fle-01 is used by isPersistFO-rec, rely-fo-follows-w-stable,
nat/l-num-06 is used by one-pending-del-persist-FO-no-pending,
nat/le-def is used by one-pending-del-persist-FO-no-pending,
nat/lels is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, take-firstPersistW-filter-FO, rely-persist-FO-weak, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-persist-W-weak, rely-fo-follows-w-stable,
nat/lels-03 is used by rely-persist-FO-weak,
nat/lep is used by rely-fo-follows-w-stable,
nat/lep-02 is used by rely-fo-follows-w-stable,
nat/ler is used by one-pending-del-persist-FO-no-pending,
nat/lez is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, isPersistFO-rec, isPersistFO-leading-W,
nat/lez-01 is used by isPersistFO-del-no-W-stable,
nat/ls is used by one-pending-del-persist-FO-no-pending,
nat/ls-01 is used by one-pending-del-persist-FO-no-pending,
nat/ls-le-simp is used by rely-persist-FO-weak, rely-persist-W-weak,
nat/succ-01 is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, take-firstPersistW-filter-FO, rely-persist-FO-weak, isPersistFO-rec, isPersistFO-leading-W, rely-persist-W-weak,

Used from specification FLITPSC-preds

FLITPSC-preds/FOFollowsW-def is used by one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
FLITPSC-preds/filterfos-def is used by rely-persist-FO-weak,
FLITPSC-preds/noPending is used by rely-no-pending-stable,
FLITPSC-preds/noPendingW is used by rely-no-pending-w-stable, one-pending-del-persist-FO-no-pending,
FLITPSC-preds/onePendingW is used by rely-one-pending-stable, one-pending-del-persist-FO-no-pending,
FLITPSC-preds/pendingOk is used by rely-one-pending-stable,
FLITPSC-preds/filter-FO-append is used by take-firstPersistW-filter-FO, rely-persist-FO-weak, rely-persist-W-weak,
FLITPSC-preds/filter-FO-empty is used by rely-persist, take-firstPersistW-filter-FO, rely-persist-FO-weak, rely-add-other-fo, rely-refl, rely-add-other-w, rely-persist-W-weak,
FLITPSC-preds/filter-FO-one-FO is used by take-firstPersistW-filter-FO, rely-persist-W-weak,
FLITPSC-preds/filter-FO-one-W is used by take-firstPersistW-filter-FO, rely-persist-W-weak,
FLITPSC-preds/filter-W-append is used by rely-one-pending-stable, isPersistFO-del-no-W-stable, firstPersistW-lt-filter-W-empty,
FLITPSC-preds/filter-W-one-fo is used by isPersistFO-del-no-W-stable, firstPersistW-lt-filter-W-empty,
FLITPSC-preds/filter-W-one-w is used by isPersistFO-del-no-W-stable, firstPersistW-lt-filter-W-empty,
FLITPSC-preds/filter-t-append is used by rely-one-pending-stable,
FLITPSC-preds/filter-t-one is used by rely-add-other-fo, rely-add-other-w,
FLITPSC-preds/filter-tid-empty is used by rely-persist, rely-persist-FO-weak, rely-add-other-fo, rely-refl, rely-add-other-w, rely-persist-W-weak,
FLITPSC-preds/filter-w-empty is used by isPersistFO-del-no-W-stable, firstPersistW-lt-filter-W-empty,
FLITPSC-preds/in-filter-FO is used by rely-one-pending-stable, rely-no-pending-w-stable, rely-no-pending-stable, rely-no-event-added-by-other, rely-fo-follows-w-stable,
FLITPSC-preds/in-filter-W is used by rely-one-pending-stable, rely-no-pending-w-stable, one-pending-del-persist-FO-no-pending,
FLITPSC-preds/in-filter-t is used by rely-one-pending-stable, rely-no-pending-w-stable, rely-no-pending-stable, one-pending-del-persist-FO-no-pending, rely-no-event-added-by-other, rely-fo-follows-w-stable,

Used from specification list-getput

list-getput/get-zero-01 is used by one-pending-del-persist-FO-no-pending,

Used from specification nat-basic

nat-basic/a is used by firstPersistW-rec-FO, isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, rely-persist-FO-weak, firstPersistW-rec-W, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-persist-W-weak, rely-fo-follows-w-stable,
nat-basic/c is used by firstPersistW-rec-FO, isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, rely-persist-FO-weak, firstPersistW-rec-W, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-persist-W-weak, rely-fo-follows-w-stable,
nat-basic/eq-01 is used by take-firstPersistW-filter-FO,
nat-basic/f is used by isPersistFO-del-no-W-stable, take-firstPersistW-filter-FO, rely-persist-FO-weak, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-persist-W-weak, rely-fo-follows-w-stable,
nat-basic/l is used by isPersistFO-rec, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
nat-basic/l-01 is used by rely-fo-follows-w-stable,
nat-basic/l-02 is used by rely-fo-follows-w-stable,
nat-basic/l-05 is used by rely-fo-follows-w-stable,
nat-basic/l-08 is used by rely-fo-follows-w-stable,
nat-basic/less-zero is used by isPersistFO-del-no-W-stable, isPersistFO-rec, isPersistFO-leading-W,
nat-basic/lf is used by isPersistFO-del-no-W-stable, rely-persist-FO-weak, isPersistFO-rec, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
nat-basic/lf-02 is used by take-firstPersistW-filter-FO, one-pending-del-persist-FO-no-pending,
nat-basic/ls-02 is used by one-pending-del-persist-FO-no-pending,
nat-basic/one-01 is used by one-pending-del-persist-FO-no-pending,
nat-basic/oz is used by firstPersistW-rec-FO, rely-persist-FO-weak, firstPersistW-rec-W, one-pending-del-persist-FO-no-pending, rely-persist-W-weak,
nat-basic/pred is used by rely-persist-FO-weak, rely-persist-W-weak,
nat-basic/s-04 is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, take-firstPersistW-filter-FO, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending,
nat-basic/succ is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, take-firstPersistW-filter-FO, rely-persist-FO-weak, isPersistFO-rec, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
nat-basic/trans-Nat is used by isPersistFO-del-no-W-stable, rely-persist-FO-weak, isPersistFO-rec, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
nat-basic/z-01 is used by take-firstPersistW-filter-FO,
nat-basic/zero is used by isPersistFO-rec,

Used from specification list

list/some-element is used by rely-one-pending-stable, rely-no-pending-w-stable, rely-no-pending-stable, one-pending-del-persist-FO-no-pending, rely-no-event-added-by-other, rely-fo-follows-w-stable,
list/Last is used by rely-persist-FO-weak, rely-persist-W-weak,
list/Nil is used by rely-persist, take-firstPersistW-filter-FO, rely-persist-FO-weak, rely-add-other-fo, rely-refl, rely-add-other-w, rely-persist-W-weak,
list/a is used by rely-persist, rely-one-pending-stable, firstPersistW-rec-FO, isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, rely-no-pending-w-stable, take-firstPersistW-filter-FO, rely-persist-FO-weak, rely-add-other-fo, firstPersistW-rec-W, isPersistFO-rec, rely-no-pending-stable, isPersistFO-leading-W, firstPersistW-lt-filter-W-empty, rely-refl, rely-add-other-w, rely-persist-W-weak, rely-no-event-added-by-other, rely-fo-follows-w-stable,
list/app is used by rely-persist, isPersistFO-del-no-W-stable, rely-persist-FO-weak, rely-add-other-fo, rely-refl, rely-add-other-w, rely-persist-W-weak,
list/app-02 is used by rely-one-pending-stable, isPersistFO-del-no-W-stable, take-firstPersistW-filter-FO, firstPersistW-lt-filter-W-empty, rely-fo-follows-w-stable,
list/app-05 is used by isPersistFO-del-no-W-stable,
list/c is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, firstPersistW-lt-filter-W-empty,
list/e is used by isPersistFO-del-no-W-stable, take-firstPersistW-filter-FO, firstPersistW-lt-filter-W-empty,
list/in-06 is used by fo-in-del-firstPersistW,
list/in-14 is used by rely-persist,
list/in-append is used by rely-one-pending-stable, rely-no-pending-w-stable, rely-no-pending-stable, rely-no-event-added-by-other,
list/in-empty is used by fo-in-del-firstPersistW,
list/in-rec is used by fo-in-del-firstPersistW,
list/len is used by rely-fo-follows-w-stable,
list/len-01 is used by isPersistFO-del-no-W-stable, take-firstPersistW-filter-FO,
list/len-05 is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, take-firstPersistW-filter-FO, isPersistFO-rec, isPersistFO-leading-W,

Used from specification FOW

FOW/disj-FO-W is used by fo-in-del-firstPersistW, one-pending-del-persist-FO-no-pending,
FOW/elim-FO is used by isPersistFO-del-no-W-stable, isPersistFO-rec,
FOW/elim-W is used by rely-one-pending-stable, rely-no-pending-w-stable, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
FOW/inj-FO is used by fo-in-del-firstPersistW,
FOW/sel-FO-dottid is used by rely-add-other-fo, isPersistFO-rec, one-pending-del-persist-FO-no-pending,
FOW/sel-W-dottid is used by rely-one-pending-stable, rely-no-pending-w-stable, isPersistFO-leading-W, one-pending-del-persist-FO-no-pending, rely-add-other-w, rely-fo-follows-w-stable,
FOW/test-dotFOque-FO is used by isPersistFO-del-no-W-stable, isPersistFO-rec, one-pending-del-persist-FO-no-pending,
FOW/test-dotFOque-W is used by rely-one-pending-stable, isPersistFO-del-no-W-stable, isPersistFO-leading-W, rely-fo-follows-w-stable,
FOW/test-dotWque-FO is used by firstPersistW-rec-FO, at-firstPersistW-is-W, fo-in-del-firstPersistW, take-firstPersistW-filter-FO, firstPersistW-lt-filter-W-empty, rely-persist-W-weak,
FOW/test-dotWque-W is used by rely-one-pending-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, rely-no-pending-w-stable, take-firstPersistW-filter-FO, firstPersistW-rec-W, one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,

Used from specification list-set

list-set/subset is used by rely-fo-follows-w-stable,
list-set/sub-in is used by rely-one-pending-stable, rely-no-pending-w-stable, rely-no-pending-stable, rely-no-event-added-by-other,
list-set/subset-app is used by rely-persist-FO-weak,
list-set/subset-empty is used by rely-persist, rely-persist-FO-weak, rely-add-other-fo, rely-refl, rely-add-other-w, rely-persist-W-weak,
list-set/subset-ref is used by rely-persist-W-weak,

Used from specification list-data

Used from specification filter-count

filter-count/filter-one is used by rely-persist-FO-weak,

Used from specification list-del

list-del/firstn-last-rec is used by rely-persist-FO-weak, rely-persist-W-weak,
list-del/firstn-restn-eq is used by rely-persist-FO-weak, rely-persist-W-weak,
list-del/get-append-grt is used by rely-fo-follows-w-stable,
list-del/get-append-less is used by rely-fo-follows-w-stable,
list-del/get-firstn is used by rely-persist-FO-weak,
list-del/in-get is used by one-pending-del-persist-FO-no-pending, rely-fo-follows-w-stable,
list-del/rmpos-take-drop is used by rely-persist-FO-weak, rely-persist-W-weak,
list-del/delnr-one is used by isPersistFO-del-no-W-stable,
list-del/delpos-base is used by isPersistFO-del-no-W-stable,
list-del/delpos-get-fw is used by fo-in-del-firstPersistW, one-pending-del-persist-FO-no-pending,
list-del/delpos-rec is used by isPersistFO-del-no-W-stable, fo-in-del-firstPersistW,
list-del/firstN-zero is used by take-firstPersistW-filter-FO,
list-del/firstn-length-03 is used by rely-persist-FO-weak,
list-del/get-append-grt-02 is used by rely-fo-follows-w-stable,
list-del/get-succ is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, isPersistFO-rec, isPersistFO-leading-W,
list-del/get-zero is used by isPersistFO-del-no-W-stable, at-firstPersistW-is-W, fo-in-del-firstPersistW, isPersistFO-rec, isPersistFO-leading-W,
list-del/one-03 is used by isPersistFO-del-no-W-stable,
list-del/rmpos-get is used by one-pending-del-persist-FO-no-pending,
list-del/rmpos-not-in is used by fo-in-del-firstPersistW,
list-del/rmpos-size is used by one-pending-del-persist-FO-no-pending,
list-del/weak-firstN-rec is used by take-firstPersistW-filter-FO,