Proof step 2 from proof predef-13 (conclusion)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 1:

  ⊦ is_predefined_class(((* str)) .class) ↔ ¬ ¬ ( str .class = `java.lang.Object' .class ∨ str .class = `*Array*' .class ∨ str .class = `java.lang.NullPointerException' .class ∨ str .class = `java.lang.ArithmeticException' .class ∨ str .class = `java.lang.ClassCastException' .class ∨ str .class = `java.lang.ArrayStoreException' .class ∨ str .class = `java.lang.NegativeArraySizeException' .class ∨ str .class = `java.lang.ArrayIndexOutOfBoundsException' .class ∨ str .class = `java.lang.IndexOutOfBoundsException' .class ∨ str .class = `java.lang.NoClassDefFoundError' .class ∨ str .class = `java.lang.ExceptionInInitializerError' .class ∨ str .class = `java.lang.Error' .class ∨ str .class = `java.lang.RuntimeException' .class ∨ str .class = `java.lang.Exception' .class ∨ str .class = `java.lang.Throwable' .class)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDSEQ : classname, , inj, ⊦ stringvar .class = stringvar0 .class ↔ stringvar = stringvar0])]]