[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 43 from proof predef_supers-if (previous step)

⊦ class = `java.lang.Throwable' .class, class = `java.lang.Object' .class, class = `*Array*' .class, predef_supers(class) = ((class = `java.lang.Error' .class ⊃ `java.lang.Error' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.Exception' .class ⊃ `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NoClassDefFoundError' .class ⊃ `java.lang.NoClassDefFoundError' .class ' + `java.lang.Error' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ExceptionInInitializerError' .class ⊃ `java.lang.ExceptionInInitializerError' .class ' + `java.lang.Error' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.RuntimeException' .class ⊃ `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NullPointerException' .class ⊃ `java.lang.NullPointerException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ArithmeticException' .class ⊃ `java.lang.ArithmeticException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ClassCastException' .class ⊃ `java.lang.ClassCastException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ArrayStoreException' .class ⊃ `java.lang.ArrayStoreException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NegativeArraySizeException' .class ⊃ `java.lang.NegativeArraySizeException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.IndexOutOfBoundsException' .class ⊃ `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `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 ' ; [] ) ) ) ) ) ) ) ) ) ) ) ) )

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

Proof step 4:
⊦ predef_supers(`java.lang.Error' .class) = `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class)
Proof step 42:
class ≠ `java.lang.Error' .class ⊦ predef_supers(class) = ((class = `java.lang.Exception' .class ⊃ `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NoClassDefFoundError' .class ⊃ `java.lang.NoClassDefFoundError' .class ' + `java.lang.Error' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ExceptionInInitializerError' .class ⊃ `java.lang.ExceptionInInitializerError' .class ' + `java.lang.Error' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.RuntimeException' .class ⊃ `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NullPointerException' .class ⊃ `java.lang.NullPointerException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ArithmeticException' .class ⊃ `java.lang.ArithmeticException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ClassCastException' .class ⊃ `java.lang.ClassCastException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.ArrayStoreException' .class ⊃ `java.lang.ArrayStoreException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.NegativeArraySizeException' .class ⊃ `java.lang.NegativeArraySizeException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `java.lang.IndexOutOfBoundsException' .class ⊃ `java.lang.IndexOutOfBoundsException' .class ' + `java.lang.RuntimeException' .class ' + `java.lang.Exception' .class ' + `java.lang.Throwable' .class ' + `java.lang.Object' .class ' ; (class = `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 ' ; [] ) ) ) ) ) ) ) ) ) ) ) ), class = `java.lang.Throwable' .class, class = `java.lang.Object' .class, class = `*Array*' .class

Rule argument

[CASEDARG : pos: right 4, ()]

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : list, classnames, Two, ⊦ class + class0 = class ' + class0 '], [CSIMPNAMEDSEQ : list, classnames, c, ⊦ class + classes = class ' + classes], [CSIMPNAMEDSEQ : list, classnames, app-01, ⊦ classes + classes0 = classes + classes1 ↔ classes0 = classes1], [CSIMPNAMEDSEQ : list, classnames, a, ⊦ (classes + classes0) + classes1 = classes + classes0 + classes1])]]