[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 apersistence-base
Status:
Proved!
Axioms: 10, User Theorems: 33 (Proved: 33, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 191, Interactions: 73
crash-group-at(0,0)
dom-disj-in-l(2,0)
elems-def(0,0)
elems-prepend(1,1)
fwd-inv-gblock-rem-del(6,2)
in-crash-in-gstore(9,3)
store-diff-union-elems-notin(3,1)
crash-group-in(0,0)
dom-disj-in-r(5,2)
elems-empty(2,1)
elems-subseteq-add-diff-notin(9,4)
fwd-inv-iblock(2,0)
inv(0,0)
crash-gstore-inv(13,6)
dom-gstore-crash(3,2)
elems-in-diff(3,1)
fwd-in-gstore-loghead(6,2)
fwd-inv-loghead(9,4)
inv-crash(5,2)
crash-index-at(0,0)
dom-gstore-intersect-in-gstore(5,2)
elems-in-fwd(5,1)
fwd-in-gstore0(6,3)
icrash-inv(10,3)
inv-index(0,0)
crash-index-in(0,0)
dom-istore-crash(1,1)
elems-in-notin-ginval(5,2)
fwd-in-log-in-gstore(4,1)
icrash-refsize-cons(17,7)
inv-journal(0,0)
crash-logblock(0,0)
dom-istore-crash-refm-refsize0(11,3)
elems-log-subset-gstore-union-ginval(6,2)
fwd-inv-gblock(2,0)
icrash-remove-refsize0-prefix(14,6)
inv-state(0,0)
crash-update-reverted(10,5)
elems-append(1,1)
elems-minus(1,1)
fwd-inv-gblock-rem(2,0)
in-crash-at-gstore(9,3)
notin-gstore-ginval-notin-gstore0(4,1)