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

asgcomp(0,0)exactarray-jvmref-01(2,1)getvals-rec(0,0)instore-rec-01(1,0)is_array-subset(2,1)isarray-union(10,3)okarray-put(1,0)okarrays-put-03(2,0)okreftype-istypeval(1,1)subset-oktype(1,0)
byteval(6,3)exactarray-len(2,1)getvals-rec-01(1,0)instore-rec-02(0,0)is_array-type(1,0)isarray-union-disjoint(2,1)okarray-put-01(4,2)okarrays-rec(0,0)okreftype-notin(1,0)union-okarray(26,9)
byteval-01(2,1)exactarray-length(2,1)gft(1,0)instore-rec-03(4,1)is_array-type-01(1,0)isarray-update(33,11)okarray-put-02(15,5)okarrays-rec-01(3,1)okreftype-null(1,1)update-at(6,2)
byteval-02(1,0)exactarray-length-01(6,2)gft-mode-01(3,2)intval-01(4,2)is_array-type-02(1,0)keys-at(11,2)okarray-put-03(2,1)okarraytype(0,0)okreftype-put(2,1)update-at-01(2,0)
bytevalues-eq(6,4)exactarray-length-02(2,1)gft-not(4,0)is-any-array(0,0)is_array-type-03(1,0)keys-empty(2,1)okarray-put-04(1,0)okarraytype-01(2,1)okreftype-subset(8,3)update-at-notin(6,2)
comp-same(6,3)exactarray-lenin(10,2)gft-not-01(10,2)is-real-array-def(0,0)is_array-type-04(1,0)keys-in(5,3)okarray-put-05(1,0)okbar(2,1)okreftype-subset-01(6,1)update-atin(8,2)
copy-comp(91,47)exactarray-new(6,2)gft-null(1,0)is-real-array-def-01(1,0)is_array-typeex(1,0)keys-in-01(1,1)okarray-put-06(15,4)okbar-01(2,1)okreftype-union(5,2)update-empty(0,0)
copy-same(1,0)exactarray-new-01(2,1)gft-out(8,2)is_array-abstract(2,1)is_array-typeex-01(1,0)keys-length(1,1)okarray-put-07(28,6)okbar-bytes2int-same(5,3)okstore(0,0)update-ex-nodups(11,5)
copy-same-01(16,6)exactarray-null(2,1)gft-out-01(3,2)is_array-arrayreftype(1,0)is_array-typele(4,1)keys-notin(1,0)okarray-put-08(14,3)okbar-byteval(10,2)okstore-01(10,5)update-in(1,0)
copy-same-01-01(14,6)exactarray-out(6,3)gft-put(1,0)is_array-arraytype(1,0)is_array-union(2,1)keys-notin-01(2,1)okarray-put-badfield(14,3)okbar-len(2,1)okstore-02(8,2)update-in-01(1,0)
copy-same-02(1,0)exactarray-primput(8,3)gft-union(1,0)is_array-badlength(1,0)is_array-union-disjoint(6,3)keys-notin-02(2,1)okarray-put-okval(28,6)okbar-lenfield(4,2)okstore-03(25,4)update-in-02(1,0)
dups-fis-keys(3,2)exactarray-put(16,5)gfts(1,0)is_array-byte-noref(9,3)is_array-update(1,0)keys-put(2,2)okarray-put-okval-01(22,6)okbar-new(2,1)okstore-04(4,1)update-in-03(10,3)
eqref(0,0)exactarray-put-01(7,3)gfts-all(10,3)is_array-byte-noref-01(1,0)is_javastore(0,0)keys-put-in(8,2)okarray-put-other(14,3)okbar-norefval(12,4)okstore-05(1,0)update-init(4,2)
eqval-booll(0,0)exactarray-put-02(16,5)gfts-in(4,1)is_array-bytearray(1,0)isarray-abstract(12,3)keys-put-notin(1,0)okarray-put-samefield(1,0)okbar-put(6,2)okstore-06(4,1)update-init-01(4,2)
eqval-boolr(0,0)exactarray-put-03(8,3)gfts-not(4,0)is_array-bytearray-01(1,0)isarray-arrayreftype(11,3)mode(2,1)okarray-put-samefield-01(16,5)okbar-put-01(5,3)okstore-07(1,0)update-keyin(8,4)
eqval-breakl(0,0)exactarray-put-04(1,0)gfts-not-01(4,1)is_array-classtype(2,1)isarray-arrayrefval(2,1)mode-01(1,0)okarray-putar(18,6)okbar-put-byte-01(5,3)okstore-08(4,2)update-keyin-01(10,6)
eqval-breakr(0,0)exactarray-put-05(10,3)gfts-null(8,2)is_array-del(1,0)isarray-bytearray(3,2)mode-02(1,1)okarray-putba(22,6)okbar-put-byte-same(2,1)okstore-09(4,2)update-length(6,1)
eqval-bytel(0,0)exactarray-put-06(10,3)gfts-put(6,3)is_array-del-01(1,0)isarray-del(4,2)mode-02-01(3,2)okarray-putbar(2,1)okbar-putbar(20,7)okstore-10(4,2)update-mode(6,2)
eqval-byter(0,0)exactarray-put-07(6,2)good-base(0,0)is_array-hasnoclasstype(1,0)isarray-del-01(2,1)mode-03(1,1)okarray-putbar-01(22,7)okbar-putbar-01(5,3)okstore-11(4,1)update-newref(4,2)
eqval-concl(0,0)exactarray-putar(16,6)good-field(0,0)is_array-hasnoclasstype-01(1,0)isarray-isarrayref(16,4)nonnullrefs-dups(20,8)okarray-putbar-02(3,2)okbar-putbar-02(2,1)okstore-jvmref(10,4)update-one(1,1)
eqval-concr(0,0)exactarray-putbar(16,6)good-field-01(1,0)is_array-is-array(1,0)isarray-keyin(18,5)nonnullrefs-dups-key(26,11)okarray-putbar-03(1,0)okbar-putbar-03(2,1)okstore-mode(9,5)update-put(8,3)
eqval-continuel(0,0)exactarray-putin(8,3)good-field-02(1,0)is_array-isarrayref(1,0)isarray-len(2,1)nonnullrefs-in(14,3)okarray-putbar-04(1,0)okbar-putbar-04(5,3)okstore-other(17,9)update-put-notin(10,4)
eqval-continuer(0,0)exactarray-type(2,1)good-field-def(1,0)is_array-keyin(1,0)isarray-lenfield(8,2)nonnullrefs-in-key(22,9)okarray-putbar-05(4,2)okbar-putbar-05(4,2)okstore-out(11,5)update-put-rew(8,4)
eqval-initl(0,0)exactarray-type-01(2,1)good-field-del(1,0)is_array-len(1,0)isarray-length(2,1)okarray-01(2,1)okarray-putbar-any(4,2)okbar-putbar-same(11,6)oksubtype(0,0)update-put-same(8,4)
eqval-initr(0,0)exactarray-type-02(2,1)good-field-field(2,0)is_array-lenfield(1,0)isarray-length-01(1,0)okarray-02(2,1)okarray-putbar-any-01(6,2)okbytearray(29,9)oktype(1,0)update-putfis-sw(9,5)
eqval-intl(0,0)exactarray-type-03(2,1)good-field-field-01(1,0)is_array-length(1,0)isarray-length-02(4,1)okarray-04(1,0)okarray-putbar-other(20,5)okbytearray-01(0,0)oktype-01(1,0)update-rec(0,0)
eqval-intr(0,0)exactref-in(1,0)good-field-field-02(1,0)is_array-length-01(1,0)isarray-length-03(4,1)okarray-05(2,1)okarray-putbar-same(8,3)okbytearray-02(2,1)oktype-02(1,0)update-rec-01(1,0)
eqval-novall(0,0)exactref-put(1,0)good-field-field-03(2,0)is_array-length-02(1,0)isarray-length-04(1,0)okarray-06(1,0)okarray-putbar-same-01(10,5)okbytearray-bad-type(1,0)oktype-03(5,3)update-rec-02(2,0)
eqval-novalr(0,0)exactref-put-01(4,1)good-field-in(1,0)is_array-length-03(1,0)isarray-length-05(4,1)okarray-07(1,0)okarray-putbar-same-02(10,5)okbytearray-byteval(1,0)oktype-04(1,0)update-refs(4,2)
eqval-refl(0,0)exactreftype(0,0)good-field-in-01(2,1)is_array-length-04(1,0)isarray-length-06(1,0)okarray-08(21,5)okarray-putbar-same-03(20,7)okbytearray-getarray-length(2,1)oktype-abstract(0,0)update-type(2,1)
eqval-refr(0,0)exacttype-abstract(0,0)good-field-index(2,1)is_array-length-05(1,0)isarray-length-07(8,2)okarray-byte(18,4)okarray-refval(2,1)okbytearray-index-in(10,2)oktype-array(0,0)update-type-01(1,0)
eqval-returnl(0,0)exacttype-array(0,0)good-field-put(3,0)is_array-length-06(1,0)isarray-newref(2,1)okarray-byte-01(18,4)okarray-subset(29,9)okbytearray-index-in-zero(2,1)oktype-bool(0,0)update-union-switch(9,5)
eqval-returnr(0,0)exacttype-bool(0,0)good-field-rew(1,0)is_array-length-07(1,0)isarray-notin(2,1)okarray-byteput(1,0)okarray-subset-01(1,0)okbytearray-is-byte(6,3)oktype-byte(0,0)validFieldValue-def(0,0)
eqval-shortl(0,0)exacttype-byte(0,0)good-field-subset(8,2)is_array-newref(1,0)isarray-notin-01(14,3)okarray-copy(23,4)okarray-subset-02(1,0)okbytearray-isarray(2,1)oktype-char(0,0)validFieldValues-def(0,0)
eqval-shortr(0,0)exacttype-class(0,0)good-index(0,0)is_array-noreftype(12,2)isarray-null(2,1)okarray-copy-01(19,6)okarray-substore(39,19)okbytearray-isarrayref(4,2)oktype-class(0,0)validFields(0,0)
eqval-throwl(0,0)exacttype-int(0,0)good-one(1,1)is_array-norefval(12,2)isarray-okarray(20,7)okarray-del(14,3)okarray-supertype(15,4)okbytearray-length-zero(1,0)oktype-del(1,1)validFields-del(6,2)
eqval-throwr(0,0)exacttype-short(0,0)good-rec(0,0)is_array-notin(1,0)isarray-okarray-01(5,1)okarray-getbar-len(5,2)okarray-type(2,1)okbytearray-not(10,2)oktype-double(0,0)validFields-empty(1,1)
eqval-typel(0,0)exacttype-void(0,0)good-rec-01(1,0)is_array-notin-01(1,0)isarray-okreftype(4,1)okarray-int-put(1,0)okarray-type-01(2,1)okbytearray-put-byteval(12,5)oktype-float(0,0)validFields-empty-01(4,2)
eqval-typer(0,0)gengft(14,3)goodfields-putba(1,0)is_array-nottypeex(4,1)isarray-okval(12,2)okarray-int-put-01(1,0)okarray-type-02(2,1)okbytearray-put-byteval-01(4,2)oktype-int(0,0)validFields-fis(6,2)
exact-base(0,0)gengfts(7,3)hasKeys-all(11,5)is_array-notypeval(1,0)isarray-put(20,6)okarray-int-put-02(1,0)okarray-type-03(2,1)okbytearray-put-byteval-equiv(27,11)oktype-long(0,0)validFields-put(3,2)
exact-field(0,0)getarray-bytes(4,3)hasKeys-app(5,3)is_array-null(1,0)isarray-put-01(4,2)okarray-intval(1,0)okarray-union(25,9)okbytearray-put-field(17,6)oktype-new(1,0)validFields-put-01(6,4)
exact-index(0,0)getarray-subset(43,17)hasKeys-empty(0,0)is_array-okarray(1,0)isarray-put-array-badindex(38,15)okarray-intval-01(4,2)okarray-union-01(2,1)okbytearray-put-field-01(3,1)oktype-okval(2,1)validFields-putfis(24,14)
exact-rec(0,0)getarray-subset-01(2,1)hasKeys-one(1,1)is_array-okarray-01(1,0)isarray-put-badfield(1,0)okarray-jvmref(1,0)okarray-union-02(4,2)okbytearray-put-field-02(3,1)oktype-out(1,1)validFields-rec(3,2)
exactarray-01(0,0)getarray-subset-02(18,5)hasKeys-put(5,3)is_array-okbytearray(2,1)isarray-put-byte(5,2)okarray-jvmref-01(2,1)okarray-union-03(45,17)okbytearray-put-field-03(2,1)oktype-put-other(1,0)validFields-type(2,1)
exactarray-01-01(2,1)getarray-superset(2,1)hasKeys-put-01(7,4)is_array-primtype(1,0)isarray-put-field(18,5)okarray-len(2,1)okarray-union-04(2,1)okbytearray-put-field-04(2,0)oktype-reftype(1,0)vals-at(11,2)
exactarray-02(0,0)getarray-superset-01(2,1)hasKeys-put-02(5,3)is_array-primtype-01(11,4)isarray-put-jvmref(8,2)okarray-length(1,0)okarray-update(8,3)okbytearray-subset(3,2)oktype-refval(1,1)vals-at-in(3,1)
exactarray-02-01(8,3)getbar-subset(16,5)hasKeys-rec(0,0)is_array-put(2,1)isarray-put-okval(8,2)okarray-length-01(8,2)okarray-update-01(2,1)okbytearray-type(4,2)oktype-rew(1,1)vals-at-in-01(1,0)
exactarray-04(1,0)getbar-superset(2,1)infis-jvmref(10,3)is_array-put-01(1,0)isarray-put-samefield(12,3)okarray-length-02(4,2)okarrayNotNull(0,0)okbytearray-type-01(4,2)oktype-short(0,0)vals-in(14,6)
exactarray-05(2,1)getbar-update(4,1)infis-notin(1,0)is_array-put-badfield(1,0)isarray-put-samefield-01(12,3)okarray-new(6,2)okarrayOfLength(0,0)okclass(0,0)oktype-st(1,0)vals-length(1,1)
exactarray-06(10,3)getbar-update-01(6,2)infis-notin-01(6,3)is_array-put-byte(1,0)isarray-putbar(27,10)okarray-new-01(2,1)okarrays-all(20,10)okclass-01(1,1)oktype-void(0,0)vals-one(1,1)
exactarray-07(1,0)getbytearray-mkjavavalues(17,10)inst-in(9,4)is_array-put-field(1,0)isarray-reftype(4,1)okarray-noval(2,1)okarrays-base(0,0)okclass-02(4,2)okval-oktype(2,1)
exactarray-08(16,5)getintarray-subset(10,3)inst-single(9,5)is_array-put-jvmref(2,0)isarray-subset(11,4)okarray-null(2,1)okarrays-mode(4,2)okclass-03(10,5)onlymod-is-update(74,33)
exactarray-byteput(1,0)getintarray-subset-01(2,1)instore-afterputs(30,14)is_array-put-okval(1,0)isarray-type(2,1)okarray-okarray(18,4)okarrays-not(15,5)okclass-copy(4,2)short-length(4,2)
exactarray-copy(10,3)getkeys-app(5,2)instore-base(0,0)is_array-put-samefield(1,0)isarray-type-01(2,1)okarray-okarray-01(17,4)okarrays-one(1,0)okclass-int(2,1)short-length-01(2,1)
exactarray-copy-01(26,9)getkeys-empty(0,0)instore-empty(0,0)is_array-put-samefield-01(1,0)isarray-type-02(2,1)okarray-okarray-02(2,1)okarrays-one-01(6,2)okclass-out(2,1)subset-exactarray(23,9)
exactarray-in(8,2)getkeys-one(3,1)instore-null(9,4)is_array-putbar(2,1)isarray-type-03(1,0)okarray-onlymod(31,13)okarrays-put(17,5)okprim-oktype(1,1)subset-len(4,3)
exactarray-intval-01(4,2)getkeys-rec(0,0)instore-one(1,1)is_array-putbar-01(2,1)isarray-type-04(1,0)okarray-out(3,1)okarrays-put-01(1,0)okreftype(0,0)subset-len-01(15,4)
exactarray-jvmref(1,0)getvals-empty(0,0)instore-rec(0,0)is_array-reftype(1,0)isarray-type-05(2,1)okarray-primput(15,4)okarrays-put-02(9,4)okreftype-02(1,0)subset-okarray(35,14)