[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. 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,

Proof step 13 from proof okval-case (conclusion)

⊦ okval(val, ty) ↔ is_boolvalue(val) ∧ ty = boolean_type ∨ is_integervalue(val) ∧ ty = int_type ∨ is_shortvalue(val) ∧ ty = short_type ∨ is_bytevalue(val) ∧ ty = byte_type ∨ is_longvalue(val) ∧ ty = long_type ∨ is_floatvalue(val) ∧ ty = float_type ∨ is_doublevalue(val) ∧ ty = double_type ∨ is_charvalue(val) ∧ ty = char_type ∨ is_referencevalue(val) ∧ (is_classtype(ty) ∨ is_arraytype(ty) ∨ ty = void_type)

User applied rule structural induction

And obtained the following new goals

Proof step 1:
⊦ okval(val, boolean_type) ↔ is_boolvalue(val)
Proof step 2:
⊦ okval(val, int_type) ↔ is_integervalue(val)
Proof step 3:
⊦ okval(val, short_type) ↔ is_shortvalue(val)
Proof step 4:
⊦ okval(val, byte_type) ↔ is_bytevalue(val)
Proof step 5:
⊦ okval(val, long_type) ↔ is_longvalue(val)
Proof step 6:
⊦ okval(val, float_type) ↔ is_floatvalue(val)
Proof step 7:
⊦ okval(val, double_type) ↔ is_doublevalue(val)
Proof step 8:
⊦ okval(val, char_type) ↔ is_charvalue(val)
Proof step 9:
⊦ okval(val, void_type) ↔ is_referencevalue(val)
Proof step 10:
⊦ ¬ okval(val, abstract_type)
Proof step 11:
⊦ okval(val, mkclasstype(class1)) ↔ is_referencevalue(val)
Proof step 12:
⊦ okval(val, mkarraytype(ty)) ↔ is_referencevalue(val)

Rule argument

[VARWITHVARSEQSARG : ty, ()]

Additional information

[[CONCRETESIMPRULES : ([CSIMPGEN : javatype generated by boolean_type, int_type, short_type, byte_type, long_type, float_type, double_type, char_type, void_type, abstract_type, mkclasstype, mkarraytype;], [CSIMPSEQ : ⊦ byte_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ short_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ int_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ boolean_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ is_arraytype(mkarraytype(ty))], [CSIMPSEQ : ⊦ ¬ is_classtype(mkarraytype(ty))], [CSIMPSEQ : ⊦ char_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ double_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ float_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ long_type ≠ mkarraytype(ty)], [CSIMPSEQ : ⊦ byte_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ short_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ int_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ boolean_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ is_classtype(mkclasstype(class))], [CSIMPSEQ : ⊦ char_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ double_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ float_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ long_type ≠ mkclasstype(class)], [CSIMPSEQ : ⊦ void_type ≠ abstract_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(abstract_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(abstract_type)], [CSIMPSEQ : ⊦ char_type ≠ abstract_type], [CSIMPSEQ : ⊦ double_type ≠ abstract_type], [CSIMPSEQ : ⊦ float_type ≠ abstract_type], [CSIMPSEQ : ⊦ long_type ≠ abstract_type], [CSIMPSEQ : ⊦ byte_type ≠ abstract_type], [CSIMPSEQ : ⊦ short_type ≠ abstract_type], [CSIMPSEQ : ⊦ int_type ≠ abstract_type], [CSIMPSEQ : ⊦ boolean_type ≠ abstract_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(void_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(void_type)], [CSIMPSEQ : ⊦ is_referencevalue(val) → ¬ is_bytevalue(val)], [CSIMPSEQ : ⊦ is_referencevalue(val) → ¬ is_shortvalue(val)], [CSIMPSEQ : ⊦ is_referencevalue(val) → ¬ is_integervalue(val)], [CSIMPSEQ : ⊦ is_referencevalue(val) → ¬ is_boolvalue(val)], [CSIMPSEQ : ⊦ char_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(char_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(char_type)], [CSIMPSEQ : ⊦ double_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(double_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(double_type)], [CSIMPSEQ : ⊦ double_type ≠ char_type], [CSIMPSEQ : ⊦ float_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(float_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(float_type)], [CSIMPSEQ : ⊦ float_type ≠ char_type], [CSIMPSEQ : ⊦ float_type ≠ double_type], [CSIMPSEQ : ⊦ long_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(long_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(long_type)], [CSIMPSEQ : ⊦ long_type ≠ char_type], [CSIMPSEQ : ⊦ long_type ≠ double_type], [CSIMPSEQ : ⊦ long_type ≠ float_type], [CSIMPSEQ : ⊦ byte_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(byte_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(byte_type)], [CSIMPSEQ : ⊦ byte_type ≠ char_type], [CSIMPSEQ : ⊦ byte_type ≠ double_type], [CSIMPSEQ : ⊦ byte_type ≠ float_type], [CSIMPSEQ : ⊦ byte_type ≠ long_type], [CSIMPSEQ : ⊦ is_bytevalue(val) → ¬ is_shortvalue(val)], [CSIMPSEQ : ⊦ is_bytevalue(val) → ¬ is_integervalue(val)], [CSIMPSEQ : ⊦ is_bytevalue(val) → ¬ is_boolvalue(val)], [CSIMPSEQ : ⊦ short_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(short_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(short_type)], [CSIMPSEQ : ⊦ short_type ≠ char_type], [CSIMPSEQ : ⊦ short_type ≠ double_type], [CSIMPSEQ : ⊦ short_type ≠ float_type], [CSIMPSEQ : ⊦ short_type ≠ long_type], [CSIMPSEQ : ⊦ short_type ≠ byte_type], [CSIMPSEQ : ⊦ is_shortvalue(val) → ¬ is_integervalue(val)], [CSIMPSEQ : ⊦ is_shortvalue(val) → ¬ is_boolvalue(val)], [CSIMPSEQ : ⊦ boolean_type ≠ void_type], [CSIMPSEQ : ⊦ ¬ is_arraytype(boolean_type)], [CSIMPSEQ : ⊦ ¬ is_classtype(boolean_type)], [CSIMPSEQ : ⊦ boolean_type ≠ char_type], [CSIMPSEQ : ⊦ boolean_type ≠ double_type], [CSIMPSEQ : ⊦ boolean_type ≠ float_type], [CSIMPSEQ : ⊦ boolean_type ≠ long_type], [CSIMPSEQ : ⊦ boolean_type ≠ byte_type], [CSIMPSEQ : ⊦ boolean_type ≠ short_type], [CSIMPSEQ : ⊦ is_integervalue(val) → ¬ is_boolvalue(val)], [CSIMPSEQ : ⊦ boolean_type ≠ int_type], [CSIMPSEQ : ⊦ int_type ≠ short_type], [CSIMPSEQ : ⊦ int_type ≠ byte_type], [CSIMPSEQ : ⊦ int_type ≠ long_type], [CSIMPSEQ : ⊦ int_type ≠ float_type], [CSIMPSEQ : ⊦ int_type ≠ double_type], [CSIMPSEQ : ⊦ int_type ≠ char_type], [CSIMPSEQ : ⊦ ¬ is_classtype(int_type)], [CSIMPSEQ : ⊦ ¬ is_arraytype(int_type)], [CSIMPSEQ : ⊦ int_type ≠ void_type])]]