[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,

Theorem base summary for Specification FLIT-preds

B-postfix-weak(0,0)B-restrict-SF-l(0,0)FOWs-loc-empty(14,2)SFTrainling-prop-FO(17,7)isPropFO-not-leading-FO(4,2)noPendingW-no-leading-bq-W(4,2)pendingOk-add-FO(28,7)readFOsOk-not-leading-W(4,2)rely-prop-FO(8,1)writersOk(0,0)
B-postfix-weak-FOWs-postfix(28,13)BrestrictL-def(0,0)FOWs-one-FO(2,1)W-in-FOWs(20,4)isPropFO-not-leading-W(4,2)oplus-noPendingW(5,2)pendingOk-add-SF(29,7)readFOsOk-not-one-SF(3,1)rely-prop-SF(3,0)writersOk-add-FO(13,1)
B-postfix-weak-append(2,0)FO-in-FOWs(20,4)FOWs-one-SF(2,1)isPropFO-FOWs-delpos-other(16,8)isPropFO-other-FO-in-delpos(26,8)oplus-v-append(10,2)pendingOk-add-pending(38,15)readFOsOk-not-one-W(4,2)rely-prop-W(10,2)writersOk-add-SF(13,1)
B-postfix-weak-delpos-propFO(12,5)FOFollowsW-def(0,0)FOWs-one-W(2,1)isPropFO-FOWs-delpos-tail(20,6)isPropFO-rec(12,6)oplus-v-one-FO(2,1)pendingOk-empty-bq(24,7)readFOsOk-prop-FO(12,1)rely-refl(2,0)writersOk-empty-bq(11,1)
B-postfix-weak-empty(2,0)FOFollowsW-old-def(0,0)FOs(0,0)isPropFO-SF-in-delpos(25,7)isPropFO-restrict-SF-l-head(19,7)oplus-v-one-SF(2,1)pendingOk-no-two-buffered-Ws(6,3)readFOsOk-rm-writer(7,0)rely-update-other-bq(2,0)writersOk-persist(16,4)
B-postfix-weak-not-in-stable(4,2)FOWs-FO(0,0)FOs-not-leading-W(4,2)isPropFO-W-in-delpos(26,8)isPropFO-restrict-delpos(11,5)oplus-v-one-W(2,1)pendingOk-persist(12,6)rely-FOFollowsW-stable(82,46)restrict-SF-eq-FOWs-eq(27,8)writersOk-prop-FO(16,2)
B-postfix-weak-of-empty(5,1)FOWs-FO-split(34,11)FOs-not-one-SF(3,1)isPropFO-cons-leading-FO(24,8)noPending(0,0)overwrite-base(0,0)pendingOk-prop-FO(20,10)rely-def(0,0)restrict-l-FO(2,1)writersOk-prop-W(20,5)
B-postfix-weak-one(27,10)FOWs-SF(0,0)FOs-not-one-W(5,3)isPropFO-def(0,0)noPending-no-leading-bq-W(2,0)overwrite-def(0,0)pendingOk-prop-W(39,15)rely-local-def(0,0)restrict-l-SF(2,1)writersok-add-pending(11,1)
B-postfix-weak-one-ws(2,1)FOWs-W(0,0)SFTrailing(0,0)isPropFO-delpos-last-SF(4,2)noPending-then-noPendingW(6,3)overwrite-rec-FO(0,0)readFOsOk(0,0)rely-noPending-stable(4,2)restrict-l-W-other(2,1)writersok-add-writer(23,5)
B-postfix-weak-refl(2,0)FOWs-W-split(34,11)SFTrailing-attach(12,3)isPropFO-drop-last-SF(8,4)noPendingW(0,0)overwrite-rec-SF(0,0)readFOsOk-add-FO(11,0)rely-noPending-stable-strong(17,9)restrict-l-W-same(2,1)writersok-rm-writer(26,7)
B-postfix-weak-same-loc(21,9)FOWs-append(10,1)SFTrailing-leading-SF(6,3)isPropFO-empty(2,1)noPendingW-add-FO(3,1)overwrite-rec-W(0,0)readFOsOk-add-writer(7,0)rely-noPendingW-stable(23,12)restrict-l-append(6,3)
B-postfix-weak-same-loc-postfix(8,3)FOWs-base(0,0)SFTrailing-tail(10,3)isPropFO-leading-SF(4,2)noPendingW-add-SF(3,1)pendingOk(0,0)readFOsOk-empty-rfo-while-writing(3,0)rely-persist(5,1)restrict-l-empty(2,1)