[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 32 from proof supers-nodups (previous step)

dups(predef_supers(class)) ⊦

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 1:
⊦ predef_supers(class) = ((class = `java.lang.Object' .class ⊃ `java.lang.Object' .class ' ; (class = `*Array*' .class ⊃ `*Array*' .class + `java.lang.Object' .class ; (class = `java.lang.Throwable' .class ⊃ `java.lang.Throwable' .class + `java.lang.Object' .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) ; [] ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
Proof step 31:
dups ((class = `java.lang.Object' .class ⊃ `java.lang.Object' .class ' ; (class = `*Array*' .class ⊃ `*Array*' .class + `java.lang.Object' .class ; (class = `java.lang.Throwable' .class ⊃ `java.lang.Throwable' .class + `java.lang.Object' .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) ; [] ) ) ) ) ) ) ) ) ) ) ) ) ) ) )) ⊦

Rule argument

[x0lemmaarg: spec-name: predefined instance-name: lemma-name: predef_supers-if antecedent: succedent: predef_supers(class) = ((class = `java.lang.Object' .class ⊃ `java.lang.Object' .class ' ; (class = `*Array*' .class ⊃ `*Array*' .class + `java.lang.Object' .class ; (class = `java.lang.Throwable' .class ⊃ `java.lang.Throwable' .class + `java.lang.Object' .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 ) ; [] ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) substlist: [class] → [class] add preconditions?: F is rewrite lemma?: T current spec?: T rotate lemma?: F replace all?: T paths: () dummy: () ]

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (class)]]