[STATEMENT]
lemma DynCastRedsNull:
  "P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle>
[PROOF STEP]
apply(rule rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> ((Cast C e, s), ?b) \<in> (Red P E)\<^sup>*
 2. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> (?b, null, s') \<in> Red P E
[PROOF STEP]
apply(erule DynCastReds)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,E \<turnstile> \<langle>e,s\<rangle> \<rightarrow>* \<langle>null,s'\<rangle> \<Longrightarrow> ((Cast C null, s'), null, s') \<in> Red P E
[PROOF STEP]
apply(simp add:RedDynCastNull)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done