[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 73 from proof predsupers-in (previous step)

class ∈ ((class0 = `java.lang.NullPointerException' .class ⊃ `java.lang.NullPointerException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ArithmeticException' .class ⊃ `java.lang.ArithmeticException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ClassCastException' .class ⊃ `java.lang.ClassCastException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ArrayStoreException' .class ⊃ `java.lang.ArrayStoreException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.NegativeArraySizeException' .class ⊃ `java.lang.NegativeArraySizeException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.IndexOutOfBoundsException' .class ⊃ `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ArrayIndexOutOfBoundsException' .class ⊃ `java.lang.ArrayIndexOutOfBoundsException' .class ' + `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; [] ) ) ) ) ) ) ) ) ⊦ class0 = `java.lang.RuntimeException' .class, class0 = `java.lang.NoClassDefFoundError' .class, class0 = `java.lang.Error' .class, class0 = `*Array*' .class, class0 = `java.lang.Object' .class, class0 = `java.lang.Throwable' .class, class0 = `java.lang.Exception' .class, class0 = `java.lang.ExceptionInInitializerError' .class, is_predefined_class(class)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

Proof step 25:
⊦ is_predefined_class(`java.lang.NullPointerException' .class)
Proof step 26:
⊦ is_predefined_class(`java.lang.RuntimeException' .class)
Proof step 27:
⊦ is_predefined_class(`java.lang.Exception' .class)
Proof step 28:
⊦ is_predefined_class(`java.lang.Throwable' .class)
Proof step 29:
⊦ is_predefined_class(`java.lang.Object' .class)
Proof step 72:
class0 ≠ `java.lang.NullPointerException' .class, class ∈ ((class0 = `java.lang.ArithmeticException' .class ⊃ `java.lang.ArithmeticException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ClassCastException' .class ⊃ `java.lang.ClassCastException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ArrayStoreException' .class ⊃ `java.lang.ArrayStoreException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.NegativeArraySizeException' .class ⊃ `java.lang.NegativeArraySizeException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.IndexOutOfBoundsException' .class ⊃ `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class0 = `java.lang.ArrayIndexOutOfBoundsException' .class ⊃ `java.lang.ArrayIndexOutOfBoundsException' .class ' + `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; [] ) ) ) ) ) ) ) ⊦ class0 = `java.lang.RuntimeException' .class, class0 = `java.lang.NoClassDefFoundError' .class, class0 = `java.lang.Error' .class, class0 = `*Array*' .class, class0 = `java.lang.Object' .class, class0 = `java.lang.Throwable' .class, class0 = `java.lang.Exception' .class, class0 = `java.lang.ExceptionInInitializerError' .class, is_predefined_class(class)

Rule argument

[CASEDARG : pos: left 1, ()]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : classname, , inj, ⊦ stringvar .class = stringvar0 .class ↔ stringvar = stringvar0], [CSIMPNAMEDSEQ : list, classnames, in-append, ⊦ class ∈ classes + classes0 ↔ ¬ ¬ ( class ∈ classes ∨ class ∈ classes0)], [CSIMPNAMEDSEQ : list, classnames, in-17, ⊦ class ∈ class0 ' ↔ class = class0], [CSIMPNAMEDSEQ : list, classnames, a, ⊦ (classes + classes0) + classes1 = classes + classes0 + classes1])]]