[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 valuefuns
- Status: unproved.
- Axioms: 112,
User Theorems:
(Proved: 81,
Partially proved: 0,
Unproved: 0,
Invalid: 0,
Siginvalid: 0)
- Proof steps: 283,
Interactions: 43
| base(0,0) | coerce-array(0,0) | flatten-shift(0,0) | init_val_int(0,0) | okprimtype-array(0,0) | okval-class(0,0) | refin-float(0,0) | refin-return(0,0) | replref-long(0,0) | typeval(6,0) |
| base-boolval(1,0) | coerce-bool(0,0) | get-rec(0,0) | init_val_long(0,0) | okprimtype-bool(0,0) | okval-double(0,0) | refin-initval(0,0) | refin-short(0,0) | replref-noval(0,0) | typeval-01(2,1) |
| base-break(1,0) | coerce-byte(0,0) | get-zero(0,0) | init_val_short(0,0) | okprimtype-byte(0,0) | okval-float(0,0) | refin-int(0,0) | refin-string(0,0) | replref-ref(0,0) | typeval-02(2,1) |
| base-byteval(1,0) | coerce-char(0,0) | getRange-base(0,0) | init_val_void(0,0) | okprimtype-char(0,0) | okval-int(0,0) | refin-list(0,0) | refin-throw(0,0) | replref-return(0,0) | typeval-03(2,1) |
| base-continue(1,0) | coerce-class(0,0) | getRange-rec(0,0) | initial-okval(2,1) | okprimtype-class(0,0) | okval-long(0,0) | refin-long(0,0) | refin-type(0,0) | replref-short(0,0) | typeval-04(2,1) |
| base-initval(4,0) | coerce-double(0,0) | hasclasstype(2,1) | initial-value(2,1) | okprimtype-double(0,0) | okval-noval(2,1) | refin-not(2,0) | refp(0,0) | replref-string(0,0) | typeval-05(2,1) |
| base-intval(7,0) | coerce-float(0,0) | incdec-byte(0,0) | initial-value-01(1,1) | okprimtype-float(0,0) | okval-reftype(2,1) | refin-not-01(2,0) | refp-01(4,1) | replref-throw(0,0) | typeval-06(2,1) |
| base-noval(1,0) | coerce-int(0,0) | incdec-byte-01(1,1) | initial-value-02(2,1) | okprimtype-int(0,0) | okval-refval(1,1) | refin-not-02(2,0) | refp-02(1,1) | replref-type(0,0) | typeval-xtra(0,0) |
| base-refval(1,0) | coerce-long(0,0) | incdec-int(1,1) | initval(13,0) | okprimtype-long(0,0) | okval-refval-01(2,1) | refin-not-03(2,0) | refval(6,0) | return(6,0) | val2int-byte(0,0) |
| base-return(13,0) | coerce-okval(2,1) | incdec-other(0,0) | initval-ref(4,2) | okprimtype-okval(2,1) | okval-short(0,0) | refin-not-04(2,0) | refval-xtra(0,0) | shiftright-base(0,0) | val2int-int(0,0) |
| base-shortval(1,0) | coerce-ref(2,1) | incdec-short(0,0) | intval(7,0) | okprimtype-okval-01(2,1) | okval-subtype(1,0) | refin-not-05(2,0) | replref-bool(0,0) | shiftright-rec(0,0) | val2int-int-01(2,0) |
| base-stringval(3,0) | coerce-short(0,0) | incdec-short-01(1,1) | intval-xtra(0,0) | okprimtype-refval(2,1) | okval-subtype-01(4,2) | refin-not-06(1,0) | replref-break(0,0) | shiftright-shift(0,0) | val2int-short(0,0) |
| base-throw(1,0) | coerce-void(0,0) | init_val_abst(0,0) | normal_mode(0,0) | okprimtype-short(0,0) | okval-supertype(2,1) | refin-not-07(2,0) | replref-byte(0,0) | shortval(6,0) | val2int-xtra(0,0) |
| base-typeval(1,0) | continue(5,0) | init_val_array(0,0) | noval(6,0) | okprimtype-void(0,0) | okval-void(0,0) | refin-not-08(2,0) | replref-char(0,0) | string2ref(0,0) |
| boolval(13,0) | exlist(41,2) | init_val_bool(0,0) | noval-01(8,2) | okval-abstract(0,0) | refin-bool(0,0) | refin-not-09(2,0) | replref-continue(0,0) | stringval(9,0) |
| boolval-xtra(0,0) | flatten-char(6,0) | init_val_byte(0,0) | okprim-array(2,1) | okval-array(0,0) | refin-break(0,0) | refin-not-10(2,0) | replref-double(0,0) | throw(6,0) |
| boolval-xtra-01(2,1) | flatten-double(1,1) | init_val_char(0,0) | okprim-class(2,1) | okval-bool(0,0) | refin-byte(0,0) | refin-not-11(2,0) | replref-float(0,0) | type4value-bool(0,0) |
| break(5,0) | flatten-float(1,1) | init_val_class(0,0) | okprim-letype(2,1) | okval-byte(0,0) | refin-char(0,0) | refin-not-12(2,0) | replref-initval(0,0) | type4value-byte(0,0) |
| byteval(6,0) | flatten-long(1,1) | init_val_double(0,0) | okprim-ref(2,1) | okval-case(1,1) | refin-continue(0,0) | refin-noval(0,0) | replref-int(0,0) | type4value-int(0,0) |
| coerce-abstract(0,0) | flatten-rec(0,0) | init_val_float(0,0) | okprimtype-abstract(0,0) | okval-char(0,0) | refin-double(0,0) | refin-ref(0,0) | replref-list(0,0) | type4value-short(0,0) |