[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 relyp-one-pending-stable, relyp-fo-follows-w-stable, relyp-no-pending-w-stable, relyp-persist,
list-last/postfix-in-01 is used by relyp-no-event-added-by-other,
list-last/postfix-in-02 is used by relyp-no-pending-stable,
list-last/postfix-reflexivity is used by relyp-add-other-w, relyp-add-other-fo, relyp-refl, relyp-persist,

Used from specification nat

nat/add-01 is used by ctrok-rm-writer,
nat/anti is used by fo-follows-last,
nat/elim-sub is used by relyp-fo-follows-w-stable,
nat/fle is used by relyp-fo-follows-w-stable, filter-FO-idx, one-pending-no-fo-no-pending,
nat/fle-01 is used by relyp-fo-follows-w-stable, filter-FO-idx,
nat/le-def is used by pendingsok-del-pos, add-pending-w-ok, add-pending-fo-ok, pending-ok-persist, filter-FO-idx,
nat/le-ls-simp is used by filter-FO-idx,
nat/lels is used by at-filter-FO-not-W, relyp-fo-follows-w-stable, fo-follows-last, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat/lels-02 is used by add-pending-w-ok, add-pending-fo-ok, pending-ok-persist,
nat/lep is used by relyp-fo-follows-w-stable,
nat/lez is used by get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat/one-01 is used by pendingsok-del-pos, pending-ok-persist,
nat/one-02 is used by pendingsok-del-pos,
nat/succ-01 is used by at-filter-FO-not-W, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat/zero is used by fo-follows-last,

Used from specification set-union

set-union/Delete is used by writersok-rm-writer, onemember-to-nomember, relyws-rm-other-writer,
set-union/del-e-02 is used by writersok-rm-writer, onemember-to-nomember,
set-union/del-size is used by ctrok-rm-writer,

Used from specification set-basic

set-basic/In-insert is used by nomember-to-onemember, writersok-add-writer,
set-basic/Size-insert is used by ctrok-add-writer,
set-basic/add is used by writersok-add-writer,
set-basic/in-02 is used by relyws-add-other-writer,
set-basic/ne is used by writersok-add-writer,
set-basic/ne-01 is used by nomember-to-onemember, writersok-add-pending, ctrok-rm-writer, onewriter-ctrok-nonzero, writersok-add-fo, writersok-persist, writersok-del-pos, writersok-add-writer, writersok-rm-writer, onemember-to-nomember, relyws-noWriter-stable, notMember-not-in,
set-basic/size-zero is used by writersok-add-writer, writersok-rm-writer,
set-basic/size-zero-01 is used by nomember-to-onemember, writersok-add-pending, onewriter-ctrok-nonzero, writersok-add-fo, writersok-persist, writersok-del-pos, writersok-add-writer, writersok-rm-writer, onemember-to-nomember, relyws-noWriter-stable, notMember-not-in,
set-basic/size-zero-02 is used by onewriter-ctrok-nonzero,

Used from specification list-data

list-data/l is used by at-filter-FO-not-W, add-pending-w-ok, add-pending-fo-ok, relyp-fo-follows-w-stable, get-filter-t, get-filter-t-rev, pending-ok-persist, filter-FO-idx, one-pending-no-fo-no-pending,
list-data/size-nil is used by at-filter-FO-not-W,

Used from specification filter-count

filter-count/count-zero-filter-nil is used by add-pending-w-ok, add-pending-fo-ok, pending-ok-persist, filter-FO-idx,
filter-count/filter-rec is used by pending-ok-persist,
filter-count/filter-split is used by filter-t-split,
filter-count/filter-swap is used by filter-W-t-swap,
filter-count/count-append is used by pendingsok-del-pos, add-pending-w-ok, pending-ok-persist,
filter-count/count-base is used by pendingsok-del-pos, get-filter-t-rev, pending-ok-persist,
filter-count/count-rec is used by get-filter-t, get-filter-t-rev, filter-FO-idx,
filter-count/count-single is used by pendingsok-del-pos, add-pending-w-ok, pending-ok-persist,
filter-count/count-sizefilter is used by relyp-one-pending-stable, pendingsok-del-pos, add-pending-w-ok, add-pending-fo-ok, get-filter-t, get-filter-t-rev, pending-ok-persist, filter-FO-idx,
filter-count/filter-append is used by relyp-one-pending-stable, writersok-add-pending, relyp-no-pending-stable, no-pending-w-add-fo-stable, writersok-add-fo, writersok-del-pos, filter-t-append, add-pending-w-ok, filter-W-append, add-pending-fo-ok, filter-FO-append, relyp-no-pending-w-stable,
filter-count/filter-base is used by pendingsok-del-pos, relyp-add-other-w, writersok-del-pos, relyp-add-other-fo, filter-FO-empty, oplus-same-writes-eq, filter-w-empty, filter-FO-idx, relyp-refl, filter-tid-empty, relyp-persist,
filter-count/filter-in is used by relyp-one-pending-stable, writersok-add-pending, relyp-no-pending-stable, in-filter-FO, no-pending-w-no-pending, writersok-persist, writersok-rm-writer, add-pending-w-one-pending, add-pending-w-ok, relyp-fo-follows-w-stable, oplus-same-writes-eq, in-filter-t, pending-ok-persist, relyp-no-event-added-by-other, one-pending-no-fo-no-pending, relyp-no-pending-w-stable, in-filter-W,
filter-count/filter-one is used by filter-t-one, relyp-add-other-w, writersok-add-pending, no-pending-w-add-fo-stable, writersok-add-fo, filter-FO-one-W, relyp-add-other-fo, add-pending-w-ok, add-pending-fo-ok, filter-W-one-w, filter-W-one-fo, filter-FO-one-FO,
filter-count/filter-rec is used by pendingsok-del-pos, filter-w-write, writersok-del-pos, oplus-same-writes-eq, get-filter-t, get-filter-t-rev, filter-w-fo, filter-FO-idx,

Used from specification nat-basic

nat-basic/zero is used by filter-FO-idx,
nat-basic/a is used by pendingsok-del-pos, at-filter-FO-not-W, ctrok-add-writer, ctrok-rm-writer, writersok-del-pos, add-pending-w-ok, relyp-fo-follows-w-stable, fo-follows-last, get-filter-t, get-filter-t-rev, pending-ok-persist, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/add-base is used by pendingsok-del-pos, at-filter-FO-not-W, ctrok-rm-writer, add-pending-w-ok, get-filter-t, get-filter-t-rev, pending-ok-persist, filter-FO-idx,
nat-basic/c is used by pendingsok-del-pos, at-filter-FO-not-W, ctrok-add-writer, ctrok-rm-writer, writersok-del-pos, add-pending-w-ok, relyp-fo-follows-w-stable, fo-follows-last, get-filter-t, get-filter-t-rev, pending-ok-persist, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/eq-01 is used by ctrok-add-writer,
nat-basic/f is used by at-filter-FO-not-W, relyp-fo-follows-w-stable, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/l is used by relyp-fo-follows-w-stable, one-pending-no-fo-no-pending,
nat-basic/l-01 is used by relyp-fo-follows-w-stable,
nat-basic/l-02 is used by relyp-fo-follows-w-stable, filter-FO-idx,
nat-basic/l-05 is used by relyp-fo-follows-w-stable,
nat-basic/less-zero is used by get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/lf is used by relyp-fo-follows-w-stable, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/ls-02 is used by one-pending-no-fo-no-pending,
nat-basic/one is used by pendingsok-del-pos, add-pending-w-ok, add-pending-fo-ok, pending-ok-persist,
nat-basic/one-01 is used by add-pending-w-ok, add-pending-fo-ok, pending-ok-persist,
nat-basic/one-03 is used by pendingsok-del-pos,
nat-basic/one-04 is used by add-pending-w-ok,
nat-basic/oz is used by pendingsok-del-pos,
nat-basic/refl-Nat is used by fo-follows-last,
nat-basic/s-04 is used by at-filter-FO-not-W, fo-follows-last, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/succ is used by pendingsok-del-pos, at-filter-FO-not-W, writersok-del-pos, relyp-fo-follows-w-stable, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/trans-Nat is used by relyp-fo-follows-w-stable, filter-FO-idx, one-pending-no-fo-no-pending,
nat-basic/z-01 is used by pendingsok-del-pos,

Used from specification list

list/some-element is used by relyp-one-pending-stable, writersok-add-pending, relyp-no-pending-stable, no-pending-w-no-pending, writersok-persist, writersok-rm-writer, add-pending-w-one-pending, add-pending-w-ok, relyp-fo-follows-w-stable, pending-ok-persist, relyp-no-event-added-by-other, one-pending-no-fo-no-pending, relyp-no-pending-w-stable,
list/Nil is used by at-filter-FO-not-W, oplus-addW-aux, oplus-same-writes-eq, get-filter-t, get-filter-t-rev, filter-w-fo, filter-FO-idx, oplus-addFO-aux, oplus-v-append,
list/a is used by oplus-addW, relyp-one-pending-stable, pendingsok-del-pos, relyp-add-other-w, oplus-addFO, writersok-add-pending, relyp-no-pending-stable, at-filter-FO-not-W, filter-w-write, no-pending-w-add-fo-stable, oplus-addW-aux, writersok-add-fo, writersok-persist, filter-t-split, writersok-del-pos, relyp-add-other-fo, filter-t-append, add-pending-w-ok, filter-W-append, add-pending-fo-ok, oplus-recW, relyp-fo-follows-w-stable, fo-follows-last, oplus-same-writes-eq, get-filter-t, get-filter-t-rev, oplus-v-one-FO, pending-ok-persist, filter-w-fo, filter-FO-idx, relyp-no-event-added-by-other, one-pending-no-fo-no-pending, filter-FO-append, relyp-refl, relyp-no-pending-w-stable, oplus-addFO-aux, oplus-v-one-W, relyp-persist, oplus-v-append,
list/app is used by relyp-add-other-w, no-pending-w-add-fo-stable, writersok-add-fo, relyp-add-other-fo, add-pending-w-ok, add-pending-fo-ok, oplus-v-one-FO, relyp-refl, oplus-v-one-W, relyp-persist,
list/app-02 is used by relyp-one-pending-stable, relyp-no-pending-stable, at-filter-FO-not-W, writersok-del-pos, add-pending-w-ok, oplus-same-writes-eq, get-filter-t, filter-FO-idx, one-pending-no-fo-no-pending, relyp-no-pending-w-stable,
list/c is used by pendingsok-del-pos, at-filter-FO-not-W, oplus-addW-aux, writersok-del-pos, oplus-same-writes-eq, get-filter-t, get-filter-t-rev, filter-FO-idx, oplus-addFO-aux, oplus-v-append,
list/c-04 is used by filter-W-one-w, filter-FO-one-FO,
list/c-06 is used by oplus-same-writes-eq,
list/e is used by at-filter-FO-not-W, add-pending-w-ok, oplus-same-writes-eq, get-filter-t, filter-FO-idx, one-pending-no-fo-no-pending,
list/in-10 is used by one-pending-no-fo-no-pending,
list/in-12 is used by writersok-persist,
list/in-14 is used by writersok-persist, oplus-recW, oplus-same-writes-eq, pending-ok-persist, one-pending-no-fo-no-pending, relyp-persist,
list/in-17 is used by writersok-add-pending, oplus-same-writes-eq,
list/in-append is used by writersok-add-pending, oplus-same-writes-eq, relyp-no-event-added-by-other,
list/in-rec is used by writersok-persist, oplus-same-writes-eq, pending-ok-persist,
list/len is used by at-filter-FO-not-W, relyp-fo-follows-w-stable, fo-follows-last,
list/len-01 is used by filter-w-write, filter-t-split, filter-t-append, filter-W-append, filter-FO-append,
list/len-02 is used by at-filter-FO-not-W, fo-follows-last,
list/len-05 is used by get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,

Used from specification FOW

FOW/inj-W is used by writersok-add-pending,
FOW/disj-FO-W is used by writersok-add-pending, at-filter-FO-not-W, fo-follows-last, oplus-same-writes-eq,
FOW/elim-W is used by pendingsok-del-pos, writersok-persist, relyp-fo-follows-w-stable, fo-follows-last, pending-ok-persist, one-pending-no-fo-no-pending,
FOW/inj-FO is used by fo-follows-last, filter-FO-idx, one-pending-no-fo-no-pending,
FOW/inj-W is used by oplus-same-writes-eq,
FOW/sel-FO-dottid is used by writersok-add-pending, relyp-add-other-fo,
FOW/sel-W-dottid is used by relyp-add-other-w, writersok-add-pending, add-pending-w-ok, relyp-fo-follows-w-stable, pending-ok-persist, one-pending-no-fo-no-pending,
FOW/test-dotFOque-FO is used by filter-FO-one-FO, filter-FO-idx,
FOW/test-dotFOque-W is used by filter-FO-one-W, filter-FO-idx,
FOW/test-dotWque-FO is used by writersok-add-pending, no-pending-w-add-fo-stable, writersok-add-fo, add-pending-fo-ok, filter-W-one-fo, oplus-same-writes-eq, filter-w-fo,
FOW/test-dotWque-W is used by pendingsok-del-pos, writersok-add-pending, filter-w-write, writersok-persist, add-pending-w-ok, filter-W-one-w, relyp-fo-follows-w-stable, fo-follows-last, oplus-same-writes-eq, pending-ok-persist, one-pending-no-fo-no-pending,

Used from specification list-del

list-del/get-append-grt is used by relyp-fo-follows-w-stable,
list-del/get-append-less is used by relyp-fo-follows-w-stable,
list-del/in-get is used by relyp-fo-follows-w-stable, one-pending-no-fo-no-pending,
list-del/delpos-base is used by pendingsok-del-pos, writersok-del-pos,
list-del/delpos-empty is used by pendingsok-del-pos, writersok-del-pos,
list-del/delpos-rec is used by pendingsok-del-pos, writersok-del-pos,
list-del/get-append-grt is used by relyp-fo-follows-w-stable, fo-follows-last,
list-del/get-append-grt-02 is used by relyp-fo-follows-w-stable,
list-del/get-last-03 is used by fo-follows-last,
list-del/get-succ is used by at-filter-FO-not-W, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
list-del/get-zero is used by at-filter-FO-not-W, get-filter-t, get-filter-t-rev, filter-FO-idx, one-pending-no-fo-no-pending,
list-del/one-03 is used by fo-follows-last,