[STATEMENT]
lemma ClassMain_imp_MethodMain:
  "(P, C0, Main) \<turnstile> (C', M', pc', nt') -ek\<rightarrow> (ClassMain P, M, pc, nt) \<Longrightarrow> M = MethodMain P"
  "(P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, pc, nt) \<Longrightarrow> M = MethodMain P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( (P, C0, Main) \<turnstile> (C', M', pc', nt') -ek\<rightarrow> (ClassMain P, M, pc, nt) \<Longrightarrow> M = MethodMain P) &&& ( (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, pc, nt) \<Longrightarrow> M = MethodMain P)
[PROOF STEP]
proof (induct P=="P" C0\<equiv>"C0" Main\<equiv>Main C' M' pc' nt' ek C''=="ClassMain P" M pc nt and
              P=="P" C0\<equiv>"C0" Main\<equiv>Main C'=="ClassMain P" M pc nt
       rule: JVMCFG_reachable_inducts)
[PROOF STATE]
proof (state)
goal (51 subgoals):
 1. MethodMain P = MethodMain P
 2. \<And>ab ac ad ba e af ag bb. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab = ClassMain P \<Longrightarrow> ac = MethodMain P;  (P, C0, Main) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ClassMain P, af, ag, bb); af = MethodMain P\<rbrakk> \<Longrightarrow> af = MethodMain P
 3. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 4. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 5. \<And>T mxs mxl\<^sub>0 is xt initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in ClassMain P; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(ClassMain P, Main)\<^esub>initParams\<rbrakk> \<Longrightarrow> Main = MethodMain P
 6. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 7. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 8. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 9. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, ClassMain P, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> M = MethodMain P
 10. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, ClassMain P, M) pc - 1)))\<rbrakk> \<Longrightarrow> M = MethodMain P
A total of 51 subgoals...
[PROOF STEP]
case CFG_Return_from_Method
[PROOF STATE]
proof (state)
this:
 (P, C0, Main) \<turnstile> \<Rightarrow>(C_, M_, None, nodeType.Return)
C_ = ClassMain P \<Longrightarrow> M_ = MethodMain P
 (P, C0, Main) \<turnstile> (ClassMain P, M'_, \<lfloor>pc'_\<rfloor>, Normal) -Q'_:(ClassMain P, M'_, pc'_)\<hookrightarrow>\<^bsub>(C_, M_)\<^esub>ps_\<rightarrow> (C_, M_, None, Enter)
C_ = ClassMain P \<Longrightarrow> M_ = MethodMain P
Q_ = (\<lambda>(s, ret). ret = (ClassMain P, M'_, pc'_))
stateUpdate_ = (\<lambda>s s'. s'(Heap := s Heap, Exception := s Exception, Stack (stkLength (P, ClassMain P, M'_) (Suc pc'_) - 1) := s (Stack 0)))
ek_ = Q_\<hookleftarrow>\<^bsub>(C_, M_)\<^esub>stateUpdate_

goal (51 subgoals):
 1. MethodMain P = MethodMain P
 2. \<And>ab ac ad ba e af ag bb. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab = ClassMain P \<Longrightarrow> ac = MethodMain P;  (P, C0, Main) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ClassMain P, af, ag, bb); af = MethodMain P\<rbrakk> \<Longrightarrow> af = MethodMain P
 3. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 4. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 5. \<And>T mxs mxl\<^sub>0 is xt initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in ClassMain P; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(ClassMain P, Main)\<^esub>initParams\<rbrakk> \<Longrightarrow> Main = MethodMain P
 6. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 7. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 8. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 9. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, ClassMain P, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> M = MethodMain P
 10. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, ClassMain P, M) pc - 1)))\<rbrakk> \<Longrightarrow> M = MethodMain P
A total of 51 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
 (P, C0, Main) \<turnstile> \<Rightarrow>(C_, M_, None, nodeType.Return)
C_ = ClassMain P \<Longrightarrow> M_ = MethodMain P
 (P, C0, Main) \<turnstile> (ClassMain P, M'_, \<lfloor>pc'_\<rfloor>, Normal) -Q'_:(ClassMain P, M'_, pc'_)\<hookrightarrow>\<^bsub>(C_, M_)\<^esub>ps_\<rightarrow> (C_, M_, None, Enter)
C_ = ClassMain P \<Longrightarrow> M_ = MethodMain P
Q_ = (\<lambda>(s, ret). ret = (ClassMain P, M'_, pc'_))
stateUpdate_ = (\<lambda>s s'. s'(Heap := s Heap, Exception := s Exception, Stack (stkLength (P, ClassMain P, M'_) (Suc pc'_) - 1) := s (Stack 0)))
ek_ = Q_\<hookleftarrow>\<^bsub>(C_, M_)\<^esub>stateUpdate_

goal (1 subgoal):
 1. M'_ = MethodMain P
[PROOF STEP]
by (fastforce elim: JVMCFG.cases)
[PROOF STATE]
proof (state)
this:
M'_ = MethodMain P

goal (50 subgoals):
 1. MethodMain P = MethodMain P
 2. \<And>ab ac ad ba e af ag bb. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab = ClassMain P \<Longrightarrow> ac = MethodMain P;  (P, C0, Main) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ClassMain P, af, ag, bb); af = MethodMain P\<rbrakk> \<Longrightarrow> af = MethodMain P
 3. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 4. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 5. \<And>T mxs mxl\<^sub>0 is xt initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); MethodMain P = MethodMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in ClassMain P; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(ClassMain P, Main)\<^esub>initParams\<rbrakk> \<Longrightarrow> Main = MethodMain P
 6. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); MethodMain P = MethodMain P\<rbrakk> \<Longrightarrow> MethodMain P = MethodMain P
 7. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 8. \<And>M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, None, Enter); M = MethodMain P\<rbrakk> \<Longrightarrow> M = MethodMain P
 9. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, ClassMain P, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> M = MethodMain P
 10. \<And>M pc n ek. \<lbrakk>ClassMain P \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, M, \<lfloor>pc\<rfloor>, Enter); M = MethodMain P; instrs_of (PROG P) (ClassMain P) M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, ClassMain P, M) pc - 1)))\<rbrakk> \<Longrightarrow> M = MethodMain P
A total of 50 subgoals...
[PROOF STEP]
qed auto


[STATEMENT]
lemma ClassMain_no_Call_target [dest!]:
  "(P, C0, Main) \<turnstile> (C, M, pc, nt) -Q:(C', M', pc')\<hookrightarrow>\<^bsub>(D,M'')\<^esub>paramDefs\<rightarrow> (ClassMain P, M''', pc'', nt')
  \<Longrightarrow> False"
  and
  "(P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt) \<Longrightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( (P, C0, Main) \<turnstile> (C, M, pc, nt) -Q:(C', M', pc')\<hookrightarrow>\<^bsub>(D, M'')\<^esub>paramDefs\<rightarrow> (ClassMain P, M''', pc'', nt') \<Longrightarrow> False) &&& ( (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt) \<Longrightarrow> True)
[PROOF STEP]
by (induct  P C0 Main C M pc nt ek=="Q:(C', M', pc')\<hookrightarrow>\<^bsub>(D,M'')\<^esub>paramDefs"
                         C''=="ClassMain P" M''' pc'' nt' and
               P C0 Main C M pc nt
    rule: JVMCFG_reachable_inducts) auto


[STATEMENT]
lemma method_of_src_and_trg_exists:
  "\<lbrakk> (P, C0, Main) \<turnstile> (C', M', pc', nt') -ek\<rightarrow> (C, M, pc, nt); C \<noteq> ClassMain P; C' \<noteq> ClassMain P \<rbrakk>
  \<Longrightarrow> (\<exists>Ts T mb. (PROG P) \<turnstile> C sees M:Ts\<rightarrow>T = mb in C) \<and>
     (\<exists>Ts T mb. (PROG P) \<turnstile> C' sees M':Ts\<rightarrow>T = mb in C')"
  and method_of_reachable_node_exists:
  "\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt); C \<noteq> ClassMain P \<rbrakk>
  \<Longrightarrow> \<exists>Ts T mb. (PROG P) \<turnstile> C sees M:Ts\<rightarrow>T = mb in C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk> (P, C0, Main) \<turnstile> (C', M', pc', nt') -ek\<rightarrow> (C, M, pc, nt); C \<noteq> ClassMain P; C' \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C')) &&& (\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt); C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
[PROOF STEP]
proof (induct rule: JVMCFG_reachable_inducts)
[PROOF STATE]
proof (state)
goal (51 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>a aa b ab ac ad ba e ae af ag bb. \<lbrakk> (a, aa, b) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab \<noteq> ClassMain a \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab;  (a, aa, b) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ae, af, ag, bb); \<lbrakk>ae \<noteq> ClassMain a; ab \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae) \<and> (\<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab); ae \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 51 subgoals...
[PROOF STEP]
case CFG_Invoke_Call
[PROOF STATE]
proof (state)
this:
C_ \<noteq> ClassMain P_
 (P_, C0_, Main_) \<turnstile> \<Rightarrow>(C_, M_, \<lfloor>pc_\<rfloor>, Normal)
C_ \<noteq> ClassMain P_ \<Longrightarrow> \<exists>Ts T mb. PROG P_ \<turnstile> C_ sees M_: Ts\<rightarrow>T = mb in C_
instrs_of (PROG P_) C_ M_ ! pc_ = Invoke M'_ n_
TYPING P_ C_ M_ ! pc_ = \<lfloor>(ST_, LT_)\<rfloor>
ST_ ! n_ = Class D'_
PROG P_ \<turnstile> D'_ sees M'_: Ts_\<rightarrow>T_ = (mxs_, mxl\<^sub>0_, is_, xt_) in D_
Q_ = (\<lambda>(s, ret). let r = stkAt s (stkLength (P_, C_, M_) pc_ - Suc n_); C' = cname_of (heap_of s) (the_Addr r) in D_ = fst (method (PROG P_) C' M'_))
paramDefs_ = (\<lambda>s. s Heap) # (\<lambda>s. s (Stack (stkLength (P_, C_, M_) pc_ - Suc n_))) # rev (map (\<lambda>i s. s (Stack (stkLength (P_, C_, M_) pc_ - Suc i))) [0..<n_])
ek_ = Q_:(C_, M_, pc_)\<hookrightarrow>\<^bsub>(D_, M'_)\<^esub>paramDefs_
D_ \<noteq> ClassMain P_
C_ \<noteq> ClassMain P_

goal (51 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>a aa b ab ac ad ba e ae af ag bb. \<lbrakk> (a, aa, b) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab \<noteq> ClassMain a \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab;  (a, aa, b) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ae, af, ag, bb); \<lbrakk>ae \<noteq> ClassMain a; ab \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae) \<and> (\<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab); ae \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 51 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
C_ \<noteq> ClassMain P_
 (P_, C0_, Main_) \<turnstile> \<Rightarrow>(C_, M_, \<lfloor>pc_\<rfloor>, Normal)
C_ \<noteq> ClassMain P_ \<Longrightarrow> \<exists>Ts T mb. PROG P_ \<turnstile> C_ sees M_: Ts\<rightarrow>T = mb in C_
instrs_of (PROG P_) C_ M_ ! pc_ = Invoke M'_ n_
TYPING P_ C_ M_ ! pc_ = \<lfloor>(ST_, LT_)\<rfloor>
ST_ ! n_ = Class D'_
PROG P_ \<turnstile> D'_ sees M'_: Ts_\<rightarrow>T_ = (mxs_, mxl\<^sub>0_, is_, xt_) in D_
Q_ = (\<lambda>(s, ret). let r = stkAt s (stkLength (P_, C_, M_) pc_ - Suc n_); C' = cname_of (heap_of s) (the_Addr r) in D_ = fst (method (PROG P_) C' M'_))
paramDefs_ = (\<lambda>s. s Heap) # (\<lambda>s. s (Stack (stkLength (P_, C_, M_) pc_ - Suc n_))) # rev (map (\<lambda>i s. s (Stack (stkLength (P_, C_, M_) pc_ - Suc i))) [0..<n_])
ek_ = Q_:(C_, M_, pc_)\<hookrightarrow>\<^bsub>(D_, M'_)\<^esub>paramDefs_
D_ \<noteq> ClassMain P_
C_ \<noteq> ClassMain P_

goal (1 subgoal):
 1. (\<exists>Ts T mb. PROG P_ \<turnstile> D_ sees M'_: Ts\<rightarrow>T = mb in D_) \<and> (\<exists>Ts T mb. PROG P_ \<turnstile> C_ sees M_: Ts\<rightarrow>T = mb in C_)
[PROOF STEP]
by (blast dest: sees_method_idemp)
[PROOF STATE]
proof (state)
this:
(\<exists>Ts T mb. PROG P_ \<turnstile> D_ sees M'_: Ts\<rightarrow>T = mb in D_) \<and> (\<exists>Ts T mb. PROG P_ \<turnstile> C_ sees M_: Ts\<rightarrow>T = mb in C_)

goal (50 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>a aa b ab ac ad ba e ae af ag bb. \<lbrakk> (a, aa, b) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab \<noteq> ClassMain a \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab;  (a, aa, b) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ae, af, ag, bb); \<lbrakk>ae \<noteq> ClassMain a; ab \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae) \<and> (\<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab); ae \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 50 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (50 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>a aa b ab ac ad ba e ae af ag bb. \<lbrakk> (a, aa, b) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab \<noteq> ClassMain a \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab;  (a, aa, b) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ae, af, ag, bb); \<lbrakk>ae \<noteq> ClassMain a; ab \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae) \<and> (\<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab); ae \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 50 subgoals...
[PROOF STEP]
case (reachable_step P C0 Main C M pc nt ek C' M' pc' nt')
[PROOF STATE]
proof (state)
this:
 (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C
 (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
\<lbrakk>C' \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C') \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
C' \<noteq> ClassMain P

goal (50 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>a aa b ab ac ad ba e ae af ag bb. \<lbrakk> (a, aa, b) \<turnstile> \<Rightarrow>(ab, ac, ad, ba); ab \<noteq> ClassMain a \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab;  (a, aa, b) \<turnstile> (ab, ac, ad, ba) -e\<rightarrow> (ae, af, ag, bb); \<lbrakk>ae \<noteq> ClassMain a; ab \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae) \<and> (\<exists>Ts T mb. PROG a \<turnstile> ab sees ac: Ts\<rightarrow>T = mb in ab); ae \<noteq> ClassMain a\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG a \<turnstile> ae sees af: Ts\<rightarrow>T = mb in ae
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 50 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
proof (cases "C = ClassMain P")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C = ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 2. C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C = ClassMain P

goal (2 subgoals):
 1. C = ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 2. C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
with \<open>(P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')\<close> \<open>C' \<noteq> ClassMain P\<close>
[PROOF STATE]
proof (chain)
picking this:
 (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C' \<noteq> ClassMain P
C = ClassMain P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
C' \<noteq> ClassMain P
C = ClassMain P

goal (1 subgoal):
 1. \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (49 subgoals):
 1. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Enter; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = Normal;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 2. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Normal; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 3. \<And>T mxs mxl\<^sub>0 is xt initParams. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Normal; M' = Main; pc' = None; nt' = Enter;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C'; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(C', Main)\<^esub>initParams\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 4. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = nodeType.Return; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 5. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = C; M' = M; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 6. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. True)\<^sub>\<surd>; C' = C; M' = M; pc' = \<lfloor>0\<rfloor>; nt' = Enter;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 7. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 8. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 9. \<And>pc v. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Push v; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 10. \<And>pc. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Pop; ek = \<Up>id\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
A total of 49 subgoals...
[PROOF STEP]
case Main_Call
[PROOF STATE]
proof (state)
this:
C = ClassMain P
M = MethodMain P
pc = \<lfloor>0\<rfloor>
nt = Normal
M' = Main
pc' = None
nt' = Enter
 (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)
PROG P \<turnstile> C0 sees Main: []\<rightarrow>T_ = (mxs_, mxl\<^sub>0_, is_, xt_) in C'
initParams_ = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]
ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(C', Main)\<^esub>initParams_

goal (49 subgoals):
 1. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Enter; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = Normal;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 2. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Normal; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 3. \<And>T mxs mxl\<^sub>0 is xt initParams. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Normal; M' = Main; pc' = None; nt' = Enter;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C'; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(C', Main)\<^esub>initParams\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 4. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = nodeType.Return; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 5. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = C; M' = M; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 6. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. True)\<^sub>\<surd>; C' = C; M' = M; pc' = \<lfloor>0\<rfloor>; nt' = Enter;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 7. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 8. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 9. \<And>pc v. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Push v; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 10. \<And>pc. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Pop; ek = \<Up>id\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
A total of 49 subgoals...
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C = ClassMain P
M = MethodMain P
pc = \<lfloor>0\<rfloor>
nt = Normal
M' = Main
pc' = None
nt' = Enter
 (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)
PROG P \<turnstile> C0 sees Main: []\<rightarrow>T_ = (mxs_, mxl\<^sub>0_, is_, xt_) in C'
initParams_ = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]
ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(C', Main)\<^esub>initParams_

goal (1 subgoal):
 1. \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
by (blast dest: sees_method_idemp)
[PROOF STATE]
proof (state)
this:
\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal (48 subgoals):
 1. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Enter; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = Normal;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 2. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = Normal; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = ClassMain P; M' = MethodMain P; pc' = \<lfloor>0\<rfloor>; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 3. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; C = ClassMain P; M = MethodMain P; pc = \<lfloor>0\<rfloor>; nt = nodeType.Return; ek = \<Up>id; C' = ClassMain P; M' = MethodMain P; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 4. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. False)\<^sub>\<surd>; C' = C; M' = M; pc' = None; nt' = nodeType.Return;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 5. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = None; nt = Enter; ek = (\<lambda>s. True)\<^sub>\<surd>; C' = C; M' = M; pc' = \<lfloor>0\<rfloor>; nt' = Enter;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 6. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 7. \<And>pc n. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1)))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 8. \<And>pc v. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Push v; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v)\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 9. \<And>pc. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = Pop; ek = \<Up>id\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
 10. \<And>pc. \<lbrakk>C' \<noteq> ClassMain P; C = ClassMain P; pc = \<lfloor>pc\<rfloor>; nt = Enter; C' = C; M' = M; pc' = \<lfloor>Suc pc\<rfloor>; nt' = Enter; C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); instrs_of (PROG P) C M ! pc = IAdd; ek = \<Up>\<lambda>s. let i1 = the_Intg (stkAt s (stkLength (P, C, M) pc - 1)); i2 = the_Intg (stkAt s (stkLength (P, C, M) pc - 2)) in s(Stack (stkLength (P, C, M) pc - 2) \<mapsto> Value (Intg (i1 + i2)))\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
A total of 48 subgoals...
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal (1 subgoal):
 1. C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<noteq> ClassMain P

goal (1 subgoal):
 1. C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
with reachable_step
[PROOF STATE]
proof (chain)
picking this:
 (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C
 (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
\<lbrakk>C' \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C') \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
C' \<noteq> ClassMain P
C \<noteq> ClassMain P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, pc, nt)
C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C
 (P, C0, Main) \<turnstile> (C, M, pc, nt) -ek\<rightarrow> (C', M', pc', nt')
\<lbrakk>C' \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C') \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
C' \<noteq> ClassMain P
C \<noteq> ClassMain P

goal (1 subgoal):
 1. \<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Ts T mb. PROG P \<turnstile> C' sees M': Ts\<rightarrow>T = mb in C'

goal (49 subgoals):
 1. \<And>P C0 Main. ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P
 2. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Enter); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 3. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 4. \<And>P C0 Main T mxs mxl\<^sub>0 is xt D initParams ek. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, Normal); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; PROG P \<turnstile> C0 sees Main: []\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in D; initParams = [\<lambda>s. s Heap, \<lambda>s. \<lfloor>Value Null\<rfloor>]; ek = \<lambda>(s, ret). True:(ClassMain P, MethodMain P, 0)\<hookrightarrow>\<^bsub>(D, Main)\<^esub>initParams; D \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> D sees Main: Ts\<rightarrow>T = mb in D) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 5. \<And>P C0 Main. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(ClassMain P, MethodMain P, \<lfloor>0\<rfloor>, nodeType.Return); ClassMain P \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P; ClassMain P \<noteq> ClassMain P; ClassMain P \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P) \<and> (\<exists>Ts T mb. PROG P \<turnstile> ClassMain P sees MethodMain P: Ts\<rightarrow>T = mb in ClassMain P)
 6. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 7. \<And>P C0 Main C M. \<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, None, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 8. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Load n; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) := s (Local n)); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 9. \<And>C P C0 Main M pc n ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Store n; ek = \<Up>\<lambda>s. s(Local n := s (Stack (stkLength (P, C, M) pc - 1))); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
 10. \<And>C P C0 Main M pc v ek. \<lbrakk>C \<noteq> ClassMain P;  (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, Enter); C \<noteq> ClassMain P \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C; instrs_of (PROG P) C M ! pc = Push v; ek = \<Up>\<lambda>s. s(Stack (stkLength (P, C, M) pc) \<mapsto> Value v); C \<noteq> ClassMain P; C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C) \<and> (\<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C)
A total of 49 subgoals...
[PROOF STEP]
qed simp_all