[STATEMENT]
lemma  fixes E :: "('a,'b, 'addr) exp" and Es :: "('a,'b, 'addr) exp list"
  shows inline_call_eq_Throw [dest]: "inline_call e E = Throw a \<Longrightarrow> call E = \<lfloor>aMvs\<rfloor> \<Longrightarrow> e = Throw a \<or> e = addr a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inline_call e E = Throw a; call E = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw a \<or> e = addr a
[PROOF STEP]
by(induct E rule: exp.induct)(fastforce split:if_split_asm)+