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

at-put-first(3,2)del-subset(3,2)init-def(22,8)init-put-21(1,0)initdone-put-rkvs(1,0)lookup-list-intro(1,1)lookup-two(1,1)newref-in-02(2,0)newrefs-length(3,0)put-rkvs-absorb-01(1,0)
at-put-first-01(2,1)del-subset-del(3,2)init-done(1,0)init-put-22(1,0)initdone-uninit(4,1)lookup-list-intro-01(12,5)maxref-empty(0,0)newref-in-03(4,1)newrefs-new(8,2)put-rkvs-append(5,1)
at-put-first-02(2,1)del-switch(17,9)init-done-01(6,0)init-put-23(22,5)initdoneP(0,0)lookup-list-intro-02(12,5)maxref-exists(25,12)newref-jvmref(4,2)newrefs-new-01(18,9)put-rkvs-last(3,1)
at-put-first-03(3,1)delete-at(2,0)init-endfmode(1,1)init-put-24(4,1)initerror(0,0)lookup-list-intro-03(1,1)maxref-exists-01(10,5)newref-new(1,0)newrefs-null(4,1)put-rkvs-list(1,0)
at-put-first-04(3,2)deleteref(0,0)init-endfmode-01(1,1)init-put-field(26,5)initerror-01(1,0)lookup-list-intro-04(1,1)maxref-ok(0,0)newref-newref(4,3)newrefs-one(1,1)put-rkvs-list-01(1,0)
at-put-first-05(2,1)exists-fournew(38,12)init-endfmode-02(1,1)init-put-field-01(6,3)initerror-02(1,0)lookup-list-intro-05(2,1)mode-01(4,2)newref-newref-notin(2,1)newrefs-one-01(3,2)put-rkvs-list-02(1,1)
at-put-first-06(1,1)exists-twonew(20,7)init-error(1,0)init-put-field-02(2,1)initerror-03(1,0)lookup-list-intro-06(1,1)mode-at-type(1,1)newref-newref-subset(4,2)newrefs-rec(18,7)put-rkvs-one(1,1)
at-put-first-rec(2,1)extension-neqrefs(1,0)init-existing(0,0)init-put-field-03(2,1)initerror-04(6,0)lookup-list-list-append(1,1)mode-at-type-01(1,1)newref-newreflist-subset(7,5)newrefs-rec-01(4,1)put-rkvs-one-01(1,0)
at-put-first-rec-01(2,1)getrefs-empty(0,0)init-mode-03(1,0)init-put-field-04(2,1)initerror-05(4,1)lookup-list-put-ex(21,9)mode-at-type-02(1,1)newref-notin(1,0)newrefs-rest(4,2)put-rkvs-rec(1,0)
at-put-first-rec-02(1,1)getrefs-rec(0,0)init-mode-04(1,0)init-put-field-05(2,1)initundone(0,0)lookup-one(0,0)mode-at-type-03(1,1)newref-notin-01(2,1)newrefs-succ(0,0)put-rkvs-switch(11,5)
at-put-first-rec-03(2,1)in-butmin(7,4)init-mode-05(1,0)init-put-field-06(2,1)initundone-01(2,1)lookup-put-ex-first(29,13)mode-at-type-04(1,1)newref-put(1,1)newrefs-three(36,28)put-rkvs-switch-01(2,1)
at-put-first-rec-04(2,1)in-butmin-01(2,1)init-out(1,0)init-put-field-07(2,1)initundone-02(1,0)lookup-put-keys(2,1)mode-at-type-05(1,1)newref-put-01(3,2)newrefs-two(16,11)put-rkvs-switch-02(2,1)
at-put-keys(3,1)in-del(1,0)init-out-01(4,0)init-put-index(5,3)initundone-03(4,0)lookup-put-keys-01(3,1)mode-del(3,2)newref-put-in(3,1)newrefs-zero(0,0)put-sks-fs-array(1,1)
at-put-keys-01(6,2)in-del-01(8,2)init-out-02(1,0)init-put-nonvoid(20,7)initundone-04(5,0)lookup-put-keys-02(3,1)mode-notin(3,2)newref-put-in-01(3,2)newrefsnew(2,1)put-sks-fs-array-01(1,1)
at-put-keys-02(2,1)in-empty(2,1)init-put(1,0)init-put-notnull(6,3)initundone-05(4,1)lookup-put-other(6,2)mode-put-sks-array(1,1)newref-same(28,14)normal(2,1)put-staticfield(0,0)
at-put-keys-03(3,1)in-list-put(12,5)init-put-01(1,0)init-put-rkvs(2,1)initundoneP(0,0)lookup-put-rkvs(8,2)mode-put-sks-array-01(1,1)newref-subset(2,0)normal-lookup(1,0)put-storerefs(0,0)
at-put-keys-04(3,1)in-list-subset(13,7)init-put-02(1,0)init-put-rkvs-01(14,7)instore(0,0)lookup-put-rkvs-01(2,1)neqref-type(1,0)newref-subset-01(1,0)normal-lookup-01(4,2)put-two(1,1)
at-put-keys-05(3,1)in-min(3,1)init-put-03(1,0)init-put-short(16,2)instore-01(2,0)lookup-put-rkvs-diff(2,1)new-insert(4,0)newref-subset-02(1,0)normal-lookup-02(4,2)ref-in(1,0)
at-put-last-other(8,4)in-mode-put(3,1)init-put-04(1,0)init-total(5,3)instore-02(11,4)lookup-put-rkvs-diff-01(2,1)new-insert-01(1,0)newreflist-dups(1,0)normal-out(3,2)refin(1,0)
at-put-last-other-01(4,2)in-put(19,9)init-put-05(1,0)init-uninit(1,0)instore-empty(0,0)lookup-put-rkvs-diff-02(2,1)new-mode(1,0)newreflist-dups-01(6,3)normal-return(1,0)refin-del(13,7)
at-put-other(3,2)in-put-keys(6,3)init-put-06(20,5)init-uninit-01(4,2)instore-one(0,0)lookup-put-rkvs-diff-03(3,1)new-mode-01(11,2)newreflist-null(1,0)normal-throw(1,0)stsubset-new(20,4)
at-put-other-01(18,7)in-put-keys-01(3,1)init-put-07(1,1)initP-put(1,0)instore-rec(0,0)lookup-put-rkvs-mode(6,2)new-out(11,2)newreflist-null-01(2,1)normalmode(0,0)subset-delete(20,7)
at-put-other-02(9,3)in-put-keys-02(3,1)init-put-08(1,0)initdone(0,0)instore-rec-01(6,4)lookup-put-rkvs-notin(6,1)newjvmref(1,0)newrefs(4,1)out(0,0)subset-instore(1,0)
at-put-other-03(1,1)in-put-rkvs(11,5)init-put-09(1,1)initdone-01(4,2)instore-two(2,1)lookup-rec(0,0)newref(0,0)newrefs-01(1,0)put-last-rec(8,3)subset-newref(4,2)
at-put-same(10,4)in-put-rkvs-01(1,0)init-put-10(1,0)initdone-02(1,0)is_a_newref(0,0)lookup-rec-01(2,1)newref-01(1,0)newrefs-base(1,1)put-last-rec-better(1,1)subset-notin(5,2)
at-put-same-01(1,1)in-put-rkvs-mode(1,0)init-put-11(1,0)initdone-03(1,0)is_the_newref(0,0)lookup-rec-refval(4,1)newref-02(15,4)newrefs-butlast(2,2)put-list-intro(1,1)subset-put-notin(4,2)
at-put-same-02(2,1)in-put-same(1,1)init-put-12(1,0)initdone-04(1,0)jump(0,0)lookup-seven(2,2)newref-03(2,0)newrefs-butlast-01(13,6)put-list-intro-01(1,1)uninit(0,0)
at-put-same-04(1,1)indel(2,1)init-put-13(1,1)initdone-05(1,0)list_ok(0,0)lookup-six(2,2)newref-def(8,2)newrefs-empty(5,3)put-one(0,0)uninit-01(4,2)
catch-break(0,0)init(1,0)init-put-14(1,1)initdone-06(1,0)look-del(4,1)lookup-sk-list-append(2,1)newref-del(4,0)newrefs-first(1,1)put-put-first-01(2,1)uninit-02(4,2)
catch-continue(0,0)init-01(1,0)init-put-15(1,1)initdone-at-type(1,1)lookup-append(12,5)lookup-staticfield(0,0)newref-del-01(2,0)newrefs-firstn(6,3)put-put-switch(10,4)uninit-03(4,2)
del-notin(2,1)init-02(1,0)init-put-16(1,1)initdone-at-type-01(1,1)lookup-empty(0,0)lookup-storerefs(0,0)newref-empty(1,0)newrefs-in(8,3)put-rec(0,0)uninit-def(19,7)
del-notin-01(8,4)init-03(1,0)init-put-17(1,0)initdone-at-type-02(1,1)lookup-five(2,2)lookup-subset(12,5)newref-exists(21,9)newrefs-jvmref(3,0)put-rec-01(2,1)uninit-existing(0,0)
del-put(9,5)init-04(0,0)init-put-18(1,0)initdone-at-type-03(1,1)lookup-four(2,2)lookup-subset-01(2,1)newref-fun(0,0)newrefs-last(1,1)put-refkeyvalues-empty(0,0)
del-put-switch(16,7)init-05(1,0)init-put-19(1,0)initdone-at-type-04(1,1)lookup-last-rec(8,3)lookup-superset(2,1)newref-in(9,3)newrefs-last-01(13,6)put-refkeyvalues-rec(0,0)
del-refs-size(8,3)init-06(1,0)init-put-20(1,0)initdone-at-type-05(1,1)lookup-list-butlast(4,2)lookup-three(2,2)newref-in-01(4,1)newrefs-lastn(7,3)put-rkvs-absorb(14,7)