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