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