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

Lemma dependency for Specification valuefuns

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
okval-subtypeprovedall subs proved okval-reftype,
okval-subtype-01provedall subs proved okval-reftype,
okval-supertypeprovedall subs proved okval-refval-01, okval-reftype,
okval-reftypeprovedall subs proved okval-array, okval-class, okval-refval-01,
noval-01provedall subs proved base, flatten-shift, exlist, base-noval,
okval-refval-01provedall subs proved okval-refval,
exlistprovedall subs proved throw, return, continue, break, initval, typeval, flatten-rec, stringval, flatten-double, flatten-float, flatten-long, flatten-char, boolval, refval, shortval, byteval, intval, noval,
coerce-okvalprovedall subs proved coerce-array, coerce-class, okval-refval, coerce-void, okval-char, coerce-char, okval-double, coerce-double, okval-float, coerce-float, okval-long, coerce-long, okval-byte, coerce-byte, okval-short, coerce-short, okval-int, coerce-int, okval-bool, coerce-bool, okval-abstract, coerce-abstract,
initval-refprovedall subs proved init_val_array, init_val_class, init_val_abst, init_val_char, init_val_double, init_val_float, init_val_long, init_val_byte, init_val_short, init_val_int, init_val_bool, init_val_void, initial-value-02,
okval-novalprovedall subs proved okval-case,
throwprovedall subs proved base, flatten-shift,
returnprovedall subs proved base, flatten-shift,
continueprovedall subs proved base, flatten-shift,
breakprovedall subs proved base, flatten-shift,
initvalprovedall subs proved base, flatten-shift,
typevalprovedall subs proved base, flatten-shift,
stringvalprovedall subs proved base, flatten-shift,
flatten-doubleprovedall subs proved flatten-shift,
flatten-floatprovedall subs proved flatten-shift,
flatten-longprovedall subs proved flatten-shift,
flatten-charprovedall subs proved base, flatten-shift,
boolvalprovedall subs proved base, flatten-shift,
refvalprovedall subs proved base, flatten-shift,
shortvalprovedall subs proved base, flatten-shift,
bytevalprovedall subs proved base, flatten-shift,
intvalprovedall subs proved flatten-shift,
novalprovedall subs proved base, flatten-shift,
initial-value-02provedall subs proved init_val_array, init_val_class, init_val_abst, init_val_void, init_val_char, init_val_double, init_val_float, init_val_long, init_val_byte, init_val_short, init_val_int, init_val_bool,
base-novalprovedall subs proved base,
okval-caseprovedall subs proved okval-array, okval-class, okval-abstract, okval-void, okval-char, okval-double, okval-float, okval-long, okval-byte, okval-short, okval-int, okval-bool,
okval-refvalprovedall subs proved okval-array, okval-class, okval-abstract, okval-void, okval-char, okval-double, okval-float, okval-long, okval-byte, okval-short, okval-int, okval-bool,
val2int-int-01provedall subs proved val2int-int,
typeval-06provedall subs proved typeval-xtra,
typeval-05provedall subs proved typeval-xtra,
typeval-04provedall subs proved typeval-xtra,
typeval-03provedall subs proved typeval-xtra,
typeval-02provedall subs proved typeval-xtra,
typeval-01provedall subs proved typeval-xtra,
refp-02provedall subs proved refp,
refp-01provedall subs proved refp,
refin-not-12provedall subs proved refin-throw,
refin-not-11provedall subs proved refin-return,
refin-not-10provedall subs proved refin-continue,
refin-not-09provedall subs proved refin-break,
refin-not-08provedall subs proved refin-initval,
refin-not-07provedall subs proved refin-type,
refin-not-06provedall subs proved refin-noval,
refin-not-05provedall subs proved refin-string,
refin-not-04provedall subs proved refin-ref,
refin-not-03provedall subs proved refin-bool,
refin-not-02provedall subs proved refin-short,
refin-not-01provedall subs proved refin-byte,
refin-notprovedall subs proved refin-int,
okprimtype-refvalprovedall subs proved okprimtype-array, okprimtype-class, okprimtype-abstract, okprimtype-void, okprimtype-char, okprimtype-double, okprimtype-float, okprimtype-long, okprimtype-byte, okprimtype-short, okprimtype-int, okprimtype-bool,
okprimtype-okval-01provedall subs proved okprimtype-array, okprimtype-class, okprimtype-abstract, okprimtype-void, okval-char, okprimtype-char, okval-double, okprimtype-double, okval-float, okprimtype-float, okval-long, okprimtype-long, okval-byte, okprimtype-byte, okval-short, okprimtype-short, okval-int, okprimtype-int, okval-bool, okprimtype-bool,
okprimtype-okvalprovedall subs proved okprimtype-array, okprimtype-class, okprimtype-abstract, okprimtype-void, okval-char, okprimtype-char, okval-double, okprimtype-double, okval-float, okprimtype-float, okval-long, okprimtype-long, okval-byte, okprimtype-byte, okval-short, okprimtype-short, okval-int, okprimtype-int, okval-bool, okprimtype-bool,
okprim-refprovedall subs proved okprimtype-array, okprimtype-class,
okprim-letypeprovedall subs proved okprimtype-array, okprimtype-class,
okprim-classprovedall subs proved okprimtype-array, okprimtype-class, okprimtype-abstract, okprimtype-void, okprimtype-byte, okprimtype-short, okprimtype-int, okprimtype-bool,
okprim-arrayprovedall subs proved okprimtype-array, okprimtype-class, okprimtype-abstract, okprimtype-void, okprimtype-byte, okprimtype-short, okprimtype-int, okprimtype-bool,
initial-value-01provedall subs proved init_val_array, init_val_class, init_val_abst, init_val_void, init_val_char, init_val_double, init_val_float, init_val_long, init_val_byte, init_val_short, init_val_int, init_val_bool,
initial-valueprovedall subs proved init_val_array, init_val_class, init_val_abst, init_val_void, init_val_char, init_val_double, init_val_float, init_val_long, init_val_byte, init_val_short, init_val_int, init_val_bool,
initial-okvalprovedall subs proved okval-array, init_val_array, okval-class, init_val_class, okval-void, init_val_void, okval-char, init_val_char, okval-double, init_val_double, okval-float, init_val_float, okval-long, init_val_long, okval-byte, init_val_byte, okval-short, init_val_short, okval-int, init_val_int, okval-bool, init_val_bool, okval-abstract, init_val_abst,
incdec-short-01provedall subs proved incdec-short,
incdec-intprovedall subs proved incdec-other,
incdec-byte-01provedall subs proved incdec-byte,
hasclasstypeprovedall subs proved okprimtype-array, okprimtype-class,
coerce-refprovedall subs proved coerce-array, coerce-class, coerce-abstract, coerce-void, coerce-char, coerce-double, coerce-float, coerce-long, coerce-byte, coerce-short, coerce-int, coerce-bool,
boolval-xtra-01provedall subs proved boolval-xtra,
base-typevalprovedall subs proved base,
base-throwprovedall subs proved base,
base-stringvalprovedall subs proved base,
base-shortvalprovedall subs proved base,
base-returnprovedall subs proved base,
base-refvalprovedall subs proved base,
base-intvalprovedall subs proved base,
base-initvalprovedall subs proved base,
base-continueprovedall subs proved base,
base-bytevalprovedall subs proved base,
base-breakprovedall subs proved base,
base-boolvalprovedall subs proved base,
val2int-intaxiom
typeval-xtraaxiom
refpaxiom
refin-throwaxiom
refin-returnaxiom
refin-continueaxiom
refin-breakaxiom
refin-initvalaxiom
refin-typeaxiom
refin-novalaxiom
refin-stringaxiom
refin-refaxiom
refin-boolaxiom
refin-shortaxiom
refin-byteaxiom
refin-intaxiom
okprimtype-longaxiom
okprimtype-floataxiom
okprimtype-doubleaxiom
okprimtype-charaxiom
okprimtype-boolaxiom
okprimtype-intaxiom
okprimtype-shortaxiom
okprimtype-byteaxiom
okprimtype-voidaxiom
okprimtype-abstractaxiom
init_val_abstaxiom
init_val_boolaxiom
init_val_intaxiom
init_val_shortaxiom
init_val_byteaxiom
init_val_longaxiom
init_val_floataxiom
init_val_doubleaxiom
init_val_charaxiom
init_val_voidaxiom
okval-voidaxiom
init_val_classaxiom
okval-classaxiom
init_val_arrayaxiom
okval-arrayaxiom
incdec-shortaxiom
incdec-otheraxiom
incdec-byteaxiom
okprimtype-classaxiom
okprimtype-arrayaxiom
flatten-recaxiom
coerce-abstractaxiom
okval-abstractaxiom
coerce-boolaxiom
okval-boolaxiom
coerce-intaxiom
okval-intaxiom
coerce-shortaxiom
okval-shortaxiom
coerce-byteaxiom
okval-byteaxiom
coerce-longaxiom
okval-longaxiom
coerce-floataxiom
okval-floataxiom
coerce-doubleaxiom
okval-doubleaxiom
coerce-charaxiom
okval-charaxiom
coerce-voidaxiom
coerce-classaxiom
coerce-arrayaxiom
boolval-xtraaxiom
flatten-shiftaxiom
baseaxiom