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

classOf(0,0)eqex-sym(3,2)exception-03(1,0)instore-inrefs-02(2,1)nouninit-put-03(12,6)onlymod-mode-01(1,0)refs-equal-in(2,1)reftypep(0,0)union-def(27,5)union-rec(0,0)
classof(1,1)eqex-tput(39,20)has_type(0,0)lookup-xtra(0,0)nouninit-put-statfield(12,6)onlymod-other(4,1)refs-notin(2,1)subset-is-union(50,22)union-empty(0,0)union-rec-rew(1,0)
classof-01(4,2)eqex-trans(5,3)init(0,0)mode-notin(2,1)nouninit-undone(3,1)onlymod-put(8,4)refs-put(12,6)subset-size(36,17)union-empty-01(3,2)union-refs(6,5)
classof-02(2,1)eqexmode(0,0)init-def(0,0)mode-notin-01(2,1)onlyModified(0,0)onlymod-put-01(14,6)reftype-01(2,0)typeOf(0,0)union-in(4,2)union-subset(2,1)
classof-03(2,1)eqkeys(0,0)init-one(1,1)mode-notin-02(4,2)onlyModifiedSet-def(0,0)onlymod-same(1,1)reftype-02(2,1)uninit(0,0)union-in-01(15,7)union-subset-left(9,4)
classof-04(3,2)eqmode(1,1)init-set(7,3)newref-same(7,5)onlymod-del(11,6)onlymod-shift(179,7)reftype-03(1,0)uninit-empty(1,1)union-in-02(1,0)
classof-05(3,2)eqmode-01(4,1)initdone-def(0,0)noiniterror(0,0)onlymod-in(4,1)onlymod-sym(1,0)reftype-04(1,0)uninit-one(1,1)union-init(9,5)
classof-06(2,1)eqmode-length(2,1)initdone-empty(1,1)nouninit(0,0)onlymod-in-01(2,1)onlymod-sym-01(17,3)reftype-int(1,0)uninit-rec(10,4)union-init-01(8,4)
classof-07(4,2)eqobj(0,0)initdone-one(1,1)nouninit-empty(1,1)onlymod-init(9,5)onlymod-type(6,2)reftype-int-01(1,0)uninit-uninit(5,2)union-init-02(2,1)
eq-mod(17,8)eqobjid(0,0)initdone-rec(10,4)nouninit-mode(3,2)onlymod-init-01(26,10)refs-def(0,0)reftype-int-02(2,1)union-at-left(4,1)union-init-03(4,2)
eqex(0,0)equalXmode(0,0)initerror(0,0)nouninit-mode-01(5,2)onlymod-init-02(12,5)refs-del(7,4)reftype-jvmref(1,1)union-at-right(2,1)union-keys(3,2)
eqex-at(6,3)exception(0,0)initerror-one(1,1)nouninit-put(7,3)onlymod-length(8,1)refs-empty(4,2)reftype-mode(1,0)union-at-right-01(6,1)union-newref(3,2)
eqex-mode(5,4)exception-01(1,1)instore-inrefs(1,1)nouninit-put-01(7,3)onlymod-length-01(2,1)refs-empty-01(8,3)reftype-out(6,1)union-at-right-02(2,1)union-newref-01(2,1)
eqex-ref(1,1)exception-02(1,0)instore-inrefs-01(2,1)nouninit-put-02(6,2)onlymod-mode(5,3)refs-equal(28,13)reftype-put(1,0)union-at-right-03(2,1)union-newref-02(5,3)