[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 store+set
Status:
Proved!
Axioms: 8, User Theorems: 42 (Proved: 42, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 187, Interactions: 54
Data-in(0,0)
Data-in-puteq(3,0)
Diff-del-rw(9,5)
Diff-rec-rev(6,3)
dom-add-in(2,0)
dom-union-l(4,2)
rem-write-cases(2,1)
restrict-intersect-empty-write-add(3,1)
Data-in-del(3,0)
Data-in-putsame(3,0)
Diff-empty(2,1)
Dom(0,0)
dom-del(2,1)
in-dom-eq(4,1)
rem-write-other(9,3)
Data-in-delput(5,0)
Data-notin-other(5,0)
Diff-ext(6,3)
In-data-in(4,1)
dom-emp(2,0)
in-dom-inter(2,0)
restrict(0,0)
Data-in-delput-2(7,0)
Data-notin-other-2(7,0)
Diff-get(5,4)
diff-add-notin(3,1)
dom-ins(2,1)
oplus-l-at-left(0,0)
restrict-at(3,1)
Data-in-other(5,2)
Data-notin-other-3(9,0)
Diff-mems-get(3,1)
diff-add-rem(2,0)
dom-isemp(6,2)
oplus-l-at-right(0,0)
restrict-empty(3,1)
Data-in-putdel(5,0)
Diff-Diff-com(6,3)
Diff-mod(6,4)
diff-get-add(2,0)
dom-rem(4,2)
oplus-l-in(0,0)
restrict-in(3,1)
Data-in-putdelput(7,0)
Diff-base(0,0)
Diff-rec(0,0)
diff-subset(2,1)
dom-restrict(5,2)
rem-write(7,2)
restrict-intersect-empty(9,4)