[STATEMENT]
lemma red0_simulates_Red1:
  assumes wf: "wf_J_prog P"
  and red: "False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2, h\<rangle> -ta\<rightarrow> \<langle>ex2'/exs2', h'\<rangle>"
  and bisiml: "bisim_list1 (e, es) (ex2, exs2)"
  shows "\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and>
                 (if \<tau>Move1 P h (ex2, exs2)
                  then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and>
                        ta = \<epsilon> \<and> h = h'
                  else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and>
                                      (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and>
                                      P,t \<turnstile>0 \<langle>e''/es'', h\<rangle> -ta'\<rightarrow> \<langle>e'/es', h'\<rangle> \<and>
                                      \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)"
  (is "\<exists>e' es' . _ \<and> ?red e' es'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
using red
[PROOF STATE]
proof (prove)
using this:
False,compP1 P,t \<turnstile>1 \<langle>ex2/exs2,h\<rangle> -ta\<rightarrow> \<langle>ex2'/exs2',h'\<rangle>

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
case (red1Red E xs TA E' xs')
[PROOF STATE]
proof (state)
this:
ex2 = (E, xs)
ta = extTA2J1 (compP1 P) TA
ex2' = (E', xs')
exs2' = exs2
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note red = \<open>False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>\<close>
    and ex2 = \<open>ex2 = (E, xs)\<close>
    and ex2' = \<open>ex2' = (E', xs')\<close>
    and [simp] = \<open>ta = extTA2J1 (compP1 P) TA\<close> \<open>exs2' = exs2\<close>
[PROOF STATE]
proof (state)
this:
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>
ex2 = (E, xs)
ex2' = (E', xs')
ta = extTA2J1 (compP1 P) TA
exs2' = exs2

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bisiml ex2
[PROOF STATE]
proof (chain)
picking this:
bisim_list1 (e, es) (ex2, exs2)
ex2 = (E, xs)
[PROOF STEP]
have bisim: "bisim [] e E xs" and fv: "fv e = {}"
    and length: "max_vars E \<le> length xs" and bsl: "bisim_list es exs2"
    and D: "\<D> e \<lfloor>{}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
bisim_list1 (e, es) (ex2, exs2)
ex2 = (E, xs)

goal (1 subgoal):
 1. (bisim [] e E xs &&& fv e = {}) &&& max_vars E \<le> length xs &&& bisim_list es exs2 &&& \<D> e \<lfloor>{}\<rfloor>
[PROOF STEP]
by(auto elim: bisim_list1_elim)
[PROOF STATE]
proof (state)
this:
bisim [] e E xs
fv e = {}
max_vars E \<le> length xs
bisim_list es exs2
\<D> e \<lfloor>{}\<rfloor>

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from red_simulates_red1_aux[OF wf red, simplified, OF bisim, of Map.empty] fv length D
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>fv e \<subseteq> set []; Map.empty \<subseteq>\<^sub>m [[] [\<mapsto>] xs]; length [] + max_vars E \<le> length xs; \<D> e \<lfloor>dom Map.empty\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>ta e2' x'. sim_move10 P t TA E E' e h Map.empty ta e2' h' x' \<and> bisim [] e2' E' xs' \<and> x' \<subseteq>\<^sub>m [[] [\<mapsto>] xs']
fv e = {}
max_vars E \<le> length xs
\<D> e \<lfloor>{}\<rfloor>
[PROOF STEP]
obtain TA' e2' x' where red': "sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'"
    and bisim'': "bisim [] e2' E' xs'" and lcl': "x' \<subseteq>\<^sub>m Map.empty"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fv e \<subseteq> set []; Map.empty \<subseteq>\<^sub>m [[] [\<mapsto>] xs]; length [] + max_vars E \<le> length xs; \<D> e \<lfloor>dom Map.empty\<rfloor>\<rbrakk> \<Longrightarrow> \<exists>ta e2' x'. sim_move10 P t TA E E' e h Map.empty ta e2' h' x' \<and> bisim [] e2' E' xs' \<and> x' \<subseteq>\<^sub>m [[] [\<mapsto>] xs']
fv e = {}
max_vars E \<le> length xs
\<D> e \<lfloor>{}\<rfloor>

goal (1 subgoal):
 1. (\<And>TA' e2' x'. \<lbrakk>sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'; bisim [] e2' E' xs'; x' \<subseteq>\<^sub>m Map.empty\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
bisim [] e2' E' xs'
x' \<subseteq>\<^sub>m Map.empty

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>
[PROOF STEP]
have "\<not> final E"
[PROOF STATE]
proof (prove)
using this:
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>

goal (1 subgoal):
 1. \<not> final E
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> final E

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with sim_move10_into_red0[OF wf_prog_wwf_prog[OF wf] red', of es] fv ex2 ex2'
[PROOF STATE]
proof (chain)
picking this:
fv e = {} \<Longrightarrow> if \<tau>move1 P h E then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock E' < countInitBlock E \<and> e2' = e \<and> x' = Map.empty) \<and> TA = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' ta'. \<tau>Red0r P t h (e, es) (e'', es) \<and> (call1 E = None \<or> call e = None \<or> e'' = e) \<and> P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es) \<and> ta_bisim01 ta' (extTA2J1 (compP1 P) TA)
fv e = {}
ex2 = (E, xs)
ex2' = (E', xs')
\<not> final E
[PROOF STEP]
have red'': "?red e2' es"
[PROOF STATE]
proof (prove)
using this:
fv e = {} \<Longrightarrow> if \<tau>move1 P h E then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock E' < countInitBlock E \<and> e2' = e \<and> x' = Map.empty) \<and> TA = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' ta'. \<tau>Red0r P t h (e, es) (e'', es) \<and> (call1 E = None \<or> call e = None \<or> e'' = e) \<and> P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es) \<and> ta_bisim01 ta' (extTA2J1 (compP1 P) TA)
fv e = {}
ex2 = (E, xs)
ex2' = (E', xs')
\<not> final E

goal (1 subgoal):
 1. if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note bsl bisim''
[PROOF STATE]
proof (state)
this:
bisim_list es exs2
bisim [] e2' E' xs'

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_list es exs2
bisim [] e2' E' xs'

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from red' fv
[PROOF STATE]
proof (chain)
picking this:
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
fv e = {}
[PROOF STEP]
have "fv e2' = {}"
[PROOF STATE]
proof (prove)
using this:
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
fv e = {}

goal (1 subgoal):
 1. fv e2' = {}
[PROOF STEP]
by(fastforce simp add: sim_move10_def split: if_split_asm dest: \<tau>red0r_fv_subset[OF wf_prog_wwf_prog[OF wf]] \<tau>red0t_fv_subset[OF wf_prog_wwf_prog[OF wf]] red_fv_subset[OF wf_prog_wwf_prog[OF wf]])
[PROOF STATE]
proof (state)
this:
fv e2' = {}

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fv e2' = {}

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from red'
[PROOF STATE]
proof (chain)
picking this:
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
[PROOF STEP]
have "dom x' \<subseteq> dom (Map.empty) \<union> fv e"
[PROOF STATE]
proof (prove)
using this:
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'

goal (1 subgoal):
 1. dom x' \<subseteq> dom Map.empty \<union> fv e
[PROOF STEP]
unfolding sim_move10_def
[PROOF STATE]
proof (prove)
using this:
\<not> final E \<and> (if \<tau>move1 P h E then (\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e2', x') \<or> countInitBlock E' < countInitBlock E \<and> e2' = e \<and> x' = Map.empty) \<and> h' = h \<and> TA = \<lbrace>\<rbrace> \<and> TA' = \<lbrace>\<rbrace> else ta_bisim01 TA' (extTA2J1 (compP1 P) TA) \<and> (if call e = None \<or> call1 E = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>e,(h, Map.empty)\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e))

goal (1 subgoal):
 1. dom x' \<subseteq> dom Map.empty \<union> fv e
[PROOF STEP]
apply(auto split: if_split_asm del: subsetI dest: \<tau>red0r_dom_lcl[OF wf_prog_wwf_prog[OF wf]] \<tau>red0t_dom_lcl[OF wf_prog_wwf_prog[OF wf]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move1 P h E; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) TA); \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call e = None\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move1 P h E; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) TA); \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call1 E = None\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
 3. \<And>a aa b ab ac ba. \<lbrakk>\<not> \<tau>move1 P h E; call e = \<lfloor>(a, aa, b)\<rfloor>; call1 E = \<lfloor>(ab, ac, ba)\<rfloor>; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) TA); extTA2J0 P,P,t \<turnstile> \<langle>e,(h, Map.empty)\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e; \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
[PROOF STEP]
apply(frule_tac [1-2] \<tau>red0r_fv_subset[OF wf_prog_wwf_prog[OF wf]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move1 P h E; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) TA); \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call e = None; fv e'' \<subseteq> fv e\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move1 P h E; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) TA); \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call1 E = None; fv e'' \<subseteq> fv e\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
 3. \<And>a aa b ab ac ba. \<lbrakk>\<not> \<tau>move1 P h E; call e = \<lfloor>(a, aa, b)\<rfloor>; call1 E = \<lfloor>(ab, ac, ba)\<rfloor>; \<not> final E; ta_bisim01 TA' (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) TA); extTA2J0 P,P,t \<turnstile> \<langle>e,(h, Map.empty)\<rangle> -TA'\<rightarrow> \<langle>e2',(h', x')\<rangle>; no_call P h e; \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> dom x' \<subseteq> fv e
[PROOF STEP]
apply(auto dest!: \<tau>red0r_dom_lcl[OF wf_prog_wwf_prog[OF wf]] red_dom_lcl del: subsetI, blast+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
dom x' \<subseteq> dom Map.empty \<union> fv e

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with fv
[PROOF STATE]
proof (chain)
picking this:
fv e = {}
dom x' \<subseteq> dom Map.empty \<union> fv e
[PROOF STEP]
have "dom x' \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
fv e = {}
dom x' \<subseteq> dom Map.empty \<union> fv e

goal (1 subgoal):
 1. dom x' \<subseteq> {}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
dom x' \<subseteq> {}

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
hence "x' = Map.empty"
[PROOF STATE]
proof (prove)
using this:
dom x' \<subseteq> {}

goal (1 subgoal):
 1. x' = Map.empty
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
x' = Map.empty

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with D red'
[PROOF STATE]
proof (chain)
picking this:
\<D> e \<lfloor>{}\<rfloor>
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
x' = Map.empty
[PROOF STEP]
have "\<D> e2' \<lfloor>{}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<D> e \<lfloor>{}\<rfloor>
sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'
x' = Map.empty

goal (1 subgoal):
 1. \<D> e2' \<lfloor>{}\<rfloor>
[PROOF STEP]
by(auto dest!: sim_move10_preserves_defass[OF wf] split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<D> e2' \<lfloor>{}\<rfloor>

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<D> e2' \<lfloor>{}\<rfloor>

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>
[PROOF STEP]
have "length xs' = length xs"
[PROOF STATE]
proof (prove)
using this:
False,compP1 P,t \<turnstile>1 \<langle>E,(h, xs)\<rangle> -TA\<rightarrow> \<langle>E',(h', xs')\<rangle>

goal (1 subgoal):
 1. length xs' = length xs
[PROOF STEP]
by(auto dest: red1_preserves_len)
[PROOF STATE]
proof (state)
this:
length xs' = length xs

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with red1_max_vars[OF red] length
[PROOF STATE]
proof (chain)
picking this:
max_vars E' \<le> max_vars E
max_vars E \<le> length xs
length xs' = length xs
[PROOF STEP]
have "max_vars E' \<le> length xs'"
[PROOF STATE]
proof (prove)
using this:
max_vars E' \<le> max_vars E
max_vars E \<le> length xs
length xs' = length xs

goal (1 subgoal):
 1. max_vars E' \<le> length xs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
max_vars E' \<le> length xs'

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bisim_list es exs2
bisim [] e2' E' xs'
fv e2' = {}
\<D> e2' \<lfloor>{}\<rfloor>
max_vars E' \<le> length xs'
[PROOF STEP]
have "bisim_list1 (e2', es) ((E', xs'), exs2)"
[PROOF STATE]
proof (prove)
using this:
bisim_list es exs2
bisim [] e2' E' xs'
fv e2' = {}
\<D> e2' \<lfloor>{}\<rfloor>
max_vars E' \<le> length xs'

goal (1 subgoal):
 1. bisim_list1 (e2', es) ((E', xs'), exs2)
[PROOF STEP]
by(rule bisim_list1I)
[PROOF STATE]
proof (state)
this:
bisim_list1 (e2', es) ((E', xs'), exs2)

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bisim_list1 (e2', es) ((E', xs'), exs2)

goal (3 subgoals):
 1. \<And>ea x taa e' x'. \<lbrakk>ex2 = (ea, x); ta = extTA2J1 (compP1 P) taa; ex2' = (e', x'); exs2' = exs2; False,compP1 P,t \<turnstile>1 \<langle>ea,(h, x)\<rangle> -taa\<rightarrow> \<langle>e',(h', x')\<rangle>\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 3. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta
bisim_list1 (e2', es) ((E', xs'), exs2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta
bisim_list1 (e2', es) ((E', xs'), exs2)

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
using ex2'
[PROOF STATE]
proof (prove)
using this:
if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e2', es) \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e2' = e \<and> es = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e2'/es,h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta
bisim_list1 (e2', es) ((E', xs'), exs2)
ex2' = (E', xs')

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
by(clarsimp split: if_split_asm)(rule exI conjI|assumption|simp)+
[PROOF STATE]
proof (state)
this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
case (red1Call E a M vs U Ts T body D xs)
[PROOF STATE]
proof (state)
this:
ex2 = (E, xs)
ta = \<lbrace>\<rbrace>
ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value)
exs2' = (E, xs) # exs2
h' = h
call1 E = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
length vs = length Ts

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note [simp] = \<open>ex2 = (E, xs)\<close> \<open>h' = h\<close> \<open>ta = \<epsilon>\<close>
    and ex2' = \<open>ex2' = (blocks1 0 (Class D#Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value)\<close>
    and exs' = \<open>exs2' = (E, xs) # exs2\<close>
    and call = \<open>call1 E = \<lfloor>(a, M, vs)\<rfloor>\<close> and ha = \<open>typeof_addr h a = \<lfloor>U\<rfloor>\<close>
    and sees = \<open>compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D\<close>
    and len = \<open>length vs = length Ts\<close>
[PROOF STATE]
proof (state)
this:
ex2 = (E, xs)
h' = h
ta = \<lbrace>\<rbrace>
ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value)
exs2' = (E, xs) # exs2
call1 E = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
length vs = length Ts

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
let ?e2' = "blocks1 0 (Class D#Ts) body"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
let ?xs2' = "Addr a # vs @ replicate (max_vars body) undefined_value"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bisiml
[PROOF STATE]
proof (chain)
picking this:
bisim_list1 (e, es) (ex2, exs2)
[PROOF STEP]
have bisim: "bisim [] e E xs" and fv: "fv e = {}"
    and length: "max_vars E \<le> length xs" and bsl: "bisim_list es exs2"
    and D: "\<D> e \<lfloor>{}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
bisim_list1 (e, es) (ex2, exs2)

goal (1 subgoal):
 1. (bisim [] e E xs &&& fv e = {}) &&& max_vars E \<le> length xs &&& bisim_list es exs2 &&& \<D> e \<lfloor>{}\<rfloor>
[PROOF STEP]
by(auto elim: bisim_list1_elim)
[PROOF STATE]
proof (state)
this:
bisim [] e E xs
fv e = {}
max_vars E \<le> length xs
bisim_list es exs2
\<D> e \<lfloor>{}\<rfloor>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bisim \<open>call1 E = \<lfloor>(a, M, vs)\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
bisim [] e E xs
call1 E = \<lfloor>(a, M, vs)\<rfloor>
[PROOF STEP]
have "call e = \<lfloor>(a, M, vs)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
bisim [] e E xs
call1 E = \<lfloor>(a, M, vs)\<rfloor>

goal (1 subgoal):
 1. call e = \<lfloor>(a, M, vs)\<rfloor>
[PROOF STEP]
by(rule bisim_call1_Some_call)
[PROOF STATE]
proof (state)
this:
call e = \<lfloor>(a, M, vs)\<rfloor>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
call e = \<lfloor>(a, M, vs)\<rfloor>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note ha
[PROOF STATE]
proof (state)
this:
typeof_addr h a = \<lfloor>U\<rfloor>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
typeof_addr h a = \<lfloor>U\<rfloor>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from \<open>compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D\<close>
[PROOF STATE]
proof (chain)
picking this:
compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
[PROOF STEP]
obtain pns Jbody where sees': "P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D"
    and body: "body = compE1 (this # pns) Jbody"
[PROOF STATE]
proof (prove)
using this:
compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. (\<And>pns Jbody. \<lbrakk>P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D; body = compE1 (this # pns) Jbody\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: sees_method_compPD)
[PROOF STATE]
proof (state)
this:
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
body = compE1 (this # pns) Jbody

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
let ?e' = "blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note sees'
[PROOF STATE]
proof (state)
this:
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from wf sees'
[PROOF STATE]
proof (chain)
picking this:
wf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
[PROOF STEP]
have "length Ts = length pns"
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. length Ts = length pns
[PROOF STEP]
by(auto dest!: sees_wf_mdecl simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
length Ts = length pns

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with len
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
length Ts = length pns
[PROOF STEP]
have "length vs = length pns" "length Ts = length pns"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts
length Ts = length pns

goal (1 subgoal):
 1. length vs = length pns &&& length Ts = length pns
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length vs = length pns
length Ts = length pns

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
call e = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
length vs = length pns
length Ts = length pns
[PROOF STEP]
have red': "P,t \<turnstile>0 \<langle>e/es, h\<rangle> -\<epsilon>\<rightarrow> \<langle>?e'/e#es, h\<rangle>"
[PROOF STATE]
proof (prove)
using this:
call e = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
length vs = length pns
length Ts = length pns

goal (1 subgoal):
 1. P,t \<turnstile>0 \<langle>e/es,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody/e # es,h\<rangle>
[PROOF STEP]
by(rule red0Call)
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e/es,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody/e # es,h\<rangle>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e/es,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody/e # es,h\<rangle>

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from \<open>call e = \<lfloor>(a, M, vs)\<rfloor>\<close> ha sees'
[PROOF STATE]
proof (chain)
picking this:
call e = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
[PROOF STEP]
have "\<tau>Move0 P h (e, es)"
[PROOF STATE]
proof (prove)
using this:
call e = \<lfloor>(a, M, vs)\<rfloor>
typeof_addr h a = \<lfloor>U\<rfloor>
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. \<tau>Move0 P h (e, es)
[PROOF STEP]
by(fastforce simp add: synthesized_call_def dest: \<tau>move0_callD[where P=P and h=h] sees_method_fun)
[PROOF STATE]
proof (state)
this:
\<tau>Move0 P h (e, es)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P,t \<turnstile>0 \<langle>e/es,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody/e # es,h\<rangle>
\<tau>Move0 P h (e, es)
[PROOF STEP]
have "\<tau>Red0t P t h (e, es) (?e', e#es)"
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile>0 \<langle>e/es,h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody/e # es,h\<rangle>
\<tau>Move0 P h (e, es)

goal (1 subgoal):
 1. \<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bsl bisim fv D length \<open>call e = \<lfloor>(a, M, vs)\<rfloor>\<close> \<open>call1 E = \<lfloor>(a, M, vs)\<rfloor>\<close>
[PROOF STATE]
proof (chain)
picking this:
bisim_list es exs2
bisim [] e E xs
fv e = {}
\<D> e \<lfloor>{}\<rfloor>
max_vars E \<le> length xs
call e = \<lfloor>(a, M, vs)\<rfloor>
call1 E = \<lfloor>(a, M, vs)\<rfloor>
[PROOF STEP]
have "bisim_list (e # es) ((E, xs) # exs2)"
[PROOF STATE]
proof (prove)
using this:
bisim_list es exs2
bisim [] e E xs
fv e = {}
\<D> e \<lfloor>{}\<rfloor>
max_vars E \<le> length xs
call e = \<lfloor>(a, M, vs)\<rfloor>
call1 E = \<lfloor>(a, M, vs)\<rfloor>

goal (1 subgoal):
 1. bisim_list (e # es) ((E, xs) # exs2)
[PROOF STEP]
by(rule bisim_list.intros)
[PROOF STATE]
proof (state)
this:
bisim_list (e # es) ((E, xs) # exs2)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
hence "bisim_list1 (?e', e # es) (ex2', (E, xs) # exs2)"
[PROOF STATE]
proof (prove)
using this:
bisim_list (e # es) ((E, xs) # exs2)

goal (1 subgoal):
 1. bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)
[PROOF STEP]
unfolding ex2'
[PROOF STATE]
proof (prove)
using this:
bisim_list (e # es) ((E, xs) # exs2)

goal (1 subgoal):
 1. bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) ((blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value), (E, xs) # exs2)
[PROOF STEP]
proof(rule bisim_list1I)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
from wf_prog_wwf_prog[OF wf] sees'
[PROOF STATE]
proof (chain)
picking this:
wwf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
[PROOF STEP]
have "wf_mdecl wwf_J_mdecl P D (M,Ts,T,\<lfloor>(pns,Jbody)\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
wwf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. wf_mdecl wwf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)
[PROOF STEP]
by(rule sees_wf_mdecl)
[PROOF STATE]
proof (state)
this:
wf_mdecl wwf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
hence "fv Jbody \<subseteq> set pns \<union> {this}"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wwf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)

goal (1 subgoal):
 1. fv Jbody \<subseteq> set pns \<union> {this}
[PROOF STEP]
by(auto simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
fv Jbody \<subseteq> set pns \<union> {this}

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fv Jbody \<subseteq> set pns \<union> {this}

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
from sees'
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
[PROOF STEP]
have "\<not> contains_insync Jbody"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. \<not> contains_insync Jbody
[PROOF STEP]
by(auto dest!: sees_wf_mdecl[OF wf] WT_expr_locks simp add: wf_mdecl_def contains_insync_conv)
[PROOF STATE]
proof (state)
this:
\<not> contains_insync Jbody

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fv Jbody \<subseteq> set pns \<union> {this}
\<not> contains_insync Jbody
[PROOF STEP]
have "bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) ?xs2'"
[PROOF STATE]
proof (prove)
using this:
fv Jbody \<subseteq> set pns \<union> {this}
\<not> contains_insync Jbody

goal (1 subgoal):
 1. bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by -(rule compE1_bisim, auto)
[PROOF STATE]
proof (state)
this:
bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) (Addr a # vs @ replicate (max_vars body) undefined_value)

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
with \<open>length vs = length Ts\<close> \<open>length Ts = length pns\<close> body
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
length Ts = length pns
body = compE1 (this # pns) Jbody
bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
have "bisim [] ?e' (blocks1 (length ([] :: vname list)) (Class D # Ts) body) ?xs2'"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts
length Ts = length pns
body = compE1 (this # pns) Jbody
bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) (Addr a # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 (length []) (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by -(rule blocks_bisim, auto simp add: nth_append nth_Cons')
[PROOF STATE]
proof (state)
this:
bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 (length []) (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)

goal (4 subgoals):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
 2. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 3. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 4. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
thus "bisim [] ?e' ?e2' ?xs2'"
[PROOF STATE]
proof (prove)
using this:
bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 (length []) (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bisim [] (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) (blocks1 0 (Class D # Ts) body) (Addr a # vs @ replicate (max_vars body) undefined_value)

goal (3 subgoals):
 1. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
 2. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 3. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
from \<open>length vs = length Ts\<close> \<open>length Ts = length pns\<close> \<open>fv Jbody \<subseteq> set pns \<union> {this}\<close>
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
length Ts = length pns
fv Jbody \<subseteq> set pns \<union> {this}
[PROOF STEP]
show "fv ?e' = {}"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts
length Ts = length pns
fv Jbody \<subseteq> set pns \<union> {this}

goal (1 subgoal):
 1. fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) = {}

goal (2 subgoals):
 1. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 2. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
from wf sees'
[PROOF STATE]
proof (chain)
picking this:
wf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D
[PROOF STEP]
have "wf_mdecl wf_J_mdecl P D (M,Ts,T,\<lfloor>(pns,Jbody)\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. wf_mdecl wf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)
[PROOF STEP]
by(rule sees_wf_mdecl)
[PROOF STATE]
proof (state)
this:
wf_mdecl wf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)

goal (2 subgoals):
 1. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 2. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
hence "\<D> Jbody \<lfloor>set pns \<union> {this}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, Jbody)\<rfloor>)

goal (1 subgoal):
 1. \<D> Jbody \<lfloor>set pns \<union> {this}\<rfloor>
[PROOF STEP]
by(auto simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
\<D> Jbody \<lfloor>set pns \<union> {this}\<rfloor>

goal (2 subgoals):
 1. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 2. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
with \<open>length vs = length Ts\<close> \<open>length Ts = length pns\<close>
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
length Ts = length pns
\<D> Jbody \<lfloor>set pns \<union> {this}\<rfloor>
[PROOF STEP]
have "\<D> (blocks pns Ts vs Jbody) \<lfloor>dom [this \<mapsto> Addr a]\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts
length Ts = length pns
\<D> Jbody \<lfloor>set pns \<union> {this}\<rfloor>

goal (1 subgoal):
 1. \<D> (blocks pns Ts vs Jbody) \<lfloor>dom [this \<mapsto> Addr a]\<rfloor>
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<D> (blocks pns Ts vs Jbody) \<lfloor>dom [this \<mapsto> Addr a]\<rfloor>

goal (2 subgoals):
 1. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
 2. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
thus "\<D> ?e' \<lfloor>{}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<D> (blocks pns Ts vs Jbody) \<lfloor>dom [this \<mapsto> Addr a]\<rfloor>

goal (1 subgoal):
 1. \<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D> (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody) \<lfloor>{}\<rfloor>

goal (1 subgoal):
 1. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
[PROOF STEP]
show "max_vars ?e2' \<le> length ?xs2'"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts

goal (1 subgoal):
 1. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by(simp add: blocks1_max_vars)
[PROOF STATE]
proof (state)
this:
max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Addr a # vs @ replicate (max_vars body) undefined_value)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
have "\<tau>Move1 P h (ex2, exs2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Move1 P h (ex2, exs2)
[PROOF STEP]
using ha \<open>call1 E = \<lfloor>(a, M, vs)\<rfloor>\<close> sees'
[PROOF STATE]
proof (prove)
using this:
typeof_addr h a = \<lfloor>U\<rfloor>
call1 E = \<lfloor>(a, M, vs)\<rfloor>
P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>(pns, Jbody)\<rfloor> in D

goal (1 subgoal):
 1. \<tau>Move1 P h (ex2, exs2)
[PROOF STEP]
by(auto simp add: synthesized_call_def \<tau>external'_def dest!: \<tau>move1_not_call1[where P=P and h=h] dest: sees_method_fun)
[PROOF STATE]
proof (state)
this:
\<tau>Move1 P h (ex2, exs2)

goal (2 subgoals):
 1. \<And>ea a M vs U Ts T body D x. \<lbrakk>ex2 = (ea, x); ta = \<lbrace>\<rbrace>; ex2' = (blocks1 0 (Class D # Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value); exs2' = (ea, x) # exs2; h' = h; call1 ea = \<lfloor>(a, M, vs)\<rfloor>; typeof_addr h a = \<lfloor>U\<rfloor>; compP1 P \<turnstile> class_type_of U sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; length vs = length Ts\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
 2. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)
bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)
\<tau>Move1 P h (ex2, exs2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)
bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)
\<tau>Move1 P h (ex2, exs2)

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
using exs'
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0t P t h (e, es) (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es)
bisim_list1 (blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody, e # es) (ex2', (E, xs) # exs2)
\<tau>Move1 P h (ex2, exs2)
exs2' = (E, xs) # exs2

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
by(simp del: \<tau>Move1.simps \<tau>Move0.simps)(rule exI conjI rtranclp.rtrancl_refl|assumption)+
[PROOF STATE]
proof (state)
this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
case (red1Return E' x' E x)
[PROOF STATE]
proof (state)
this:
ex2 = (E', x')
exs2 = (E, x) # exs2'
ta = \<lbrace>\<rbrace>
ex2' = (inline_call E' E, x)
h' = h
final E'

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
note [simp] = \<open>h' = h\<close> \<open>ta = \<epsilon>\<close>
    and ex2 = \<open>ex2 = (E', x')\<close> and exs2 = \<open>exs2 = (E, x) # exs2'\<close>
    and ex2' = \<open>ex2' = (inline_call E' E, x)\<close>
    and fin = \<open>final E'\<close>
[PROOF STATE]
proof (state)
this:
h' = h
ta = \<lbrace>\<rbrace>
ex2 = (E', x')
exs2 = (E, x) # exs2'
ex2' = (inline_call E' E, x)
final E'

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bisiml ex2 exs2
[PROOF STATE]
proof (chain)
picking this:
bisim_list1 (e, es) (ex2, exs2)
ex2 = (E', x')
exs2 = (E, x) # exs2'
[PROOF STEP]
obtain e' es' aMvs where es: "es = e' # es'"
    and bsl: "bisim_list es' exs2'"
    and bisim: "bisim [] e E' x'"
    and bisim': "bisim [] e' E x"
    and fv: "fv e' = {}"
    and length: "max_vars E \<le> length x"
    and D: "\<D> e' \<lfloor>{}\<rfloor>"
    and call: "call e' = \<lfloor>aMvs\<rfloor>"
    and call1: "call1 E = \<lfloor>aMvs\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
bisim_list1 (e, es) (ex2, exs2)
ex2 = (E', x')
exs2 = (E, x) # exs2'

goal (1 subgoal):
 1. (\<And>e' es' aMvs. \<lbrakk>es = e' # es'; bisim_list es' exs2'; bisim [] e E' x'; bisim [] e' E x; fv e' = {}; max_vars E \<le> length x; \<D> e' \<lfloor>{}\<rfloor>; call e' = \<lfloor>aMvs\<rfloor>; call1 E = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!: bisim_list1_elim)
[PROOF STATE]
proof (state)
this:
es = e' # es'
bisim_list es' exs2'
bisim [] e E' x'
bisim [] e' E x
fv e' = {}
max_vars E \<le> length x
\<D> e' \<lfloor>{}\<rfloor>
call e' = \<lfloor>aMvs\<rfloor>
call1 E = \<lfloor>aMvs\<rfloor>

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from \<open>final E'\<close> bisim
[PROOF STATE]
proof (chain)
picking this:
final E'
bisim [] e E' x'
[PROOF STEP]
have fin': "final e"
[PROOF STATE]
proof (prove)
using this:
final E'
bisim [] e E' x'

goal (1 subgoal):
 1. final e
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
final e

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
hence "P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<epsilon>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>"
[PROOF STATE]
proof (prove)
using this:
final e

goal (1 subgoal):
 1. P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>
[PROOF STEP]
by(rule red0Return)
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
from bisim fin' bisim' call
[PROOF STATE]
proof (chain)
picking this:
bisim [] e E' x'
final e
bisim [] e' E x
call e' = \<lfloor>aMvs\<rfloor>
[PROOF STEP]
have "bisim [] (inline_call e e') (inline_call E' E) x"
[PROOF STATE]
proof (prove)
using this:
bisim [] e E' x'
final e
bisim [] e' E x
call e' = \<lfloor>aMvs\<rfloor>

goal (1 subgoal):
 1. bisim [] (inline_call e e') (inline_call E' E) x
[PROOF STEP]
by(rule bisim_inline_call)(simp add: fv)
[PROOF STATE]
proof (state)
this:
bisim [] (inline_call e e') (inline_call E' E) x

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
with bsl
[PROOF STATE]
proof (chain)
picking this:
bisim_list es' exs2'
bisim [] (inline_call e e') (inline_call E' E) x
[PROOF STEP]
have "bisim_list1 (inline_call e e', es') (ex2', exs2')"
[PROOF STATE]
proof (prove)
using this:
bisim_list es' exs2'
bisim [] (inline_call e e') (inline_call E' E) x

goal (1 subgoal):
 1. bisim_list1 (inline_call e e', es') (ex2', exs2')
[PROOF STEP]
unfolding ex2'
[PROOF STATE]
proof (prove)
using this:
bisim_list es' exs2'
bisim [] (inline_call e e') (inline_call E' E) x

goal (1 subgoal):
 1. bisim_list1 (inline_call e e', es') ((inline_call E' E, x), exs2')
[PROOF STEP]
proof(rule bisim_list1I)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. fv (inline_call e e') = {}
 2. \<D> (inline_call e e') \<lfloor>{}\<rfloor>
 3. max_vars (inline_call E' E) \<le> length x
[PROOF STEP]
from fin' fv_inline_call[of e e'] fv
[PROOF STATE]
proof (chain)
picking this:
final e
fv (inline_call e e') \<subseteq> fv e' \<union> fv e
fv e' = {}
[PROOF STEP]
show "fv (inline_call e e') = {}"
[PROOF STATE]
proof (prove)
using this:
final e
fv (inline_call e e') \<subseteq> fv e' \<union> fv e
fv e' = {}

goal (1 subgoal):
 1. fv (inline_call e e') = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (inline_call e e') = {}

goal (2 subgoals):
 1. \<D> (inline_call e e') \<lfloor>{}\<rfloor>
 2. max_vars (inline_call E' E) \<le> length x
[PROOF STEP]
from fin'
[PROOF STATE]
proof (chain)
picking this:
final e
[PROOF STEP]
show "\<D> (inline_call e e') \<lfloor>{}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
final e

goal (1 subgoal):
 1. \<D> (inline_call e e') \<lfloor>{}\<rfloor>
[PROOF STEP]
using call D
[PROOF STATE]
proof (prove)
using this:
final e
call e' = \<lfloor>aMvs\<rfloor>
\<D> e' \<lfloor>{}\<rfloor>

goal (1 subgoal):
 1. \<D> (inline_call e e') \<lfloor>{}\<rfloor>
[PROOF STEP]
by(rule defass_inline_call)
[PROOF STATE]
proof (state)
this:
\<D> (inline_call e e') \<lfloor>{}\<rfloor>

goal (1 subgoal):
 1. max_vars (inline_call E' E) \<le> length x
[PROOF STEP]
from call1_imp_call[OF call1]
[PROOF STATE]
proof (chain)
picking this:
call E = \<lfloor>aMvs\<rfloor>
[PROOF STEP]
have "max_vars (inline_call E' E) \<le> max_vars E + max_vars E'"
[PROOF STATE]
proof (prove)
using this:
call E = \<lfloor>aMvs\<rfloor>

goal (1 subgoal):
 1. max_vars (inline_call E' E) \<le> max_vars E + max_vars E'
[PROOF STEP]
by(rule inline_call_max_vars)
[PROOF STATE]
proof (state)
this:
max_vars (inline_call E' E) \<le> max_vars E + max_vars E'

goal (1 subgoal):
 1. max_vars (inline_call E' E) \<le> length x
[PROOF STEP]
with fin length
[PROOF STATE]
proof (chain)
picking this:
final E'
max_vars E \<le> length x
max_vars (inline_call E' E) \<le> max_vars E + max_vars E'
[PROOF STEP]
show "max_vars (inline_call E' E) \<le> length x"
[PROOF STATE]
proof (prove)
using this:
final E'
max_vars E \<le> length x
max_vars (inline_call E' E) \<le> max_vars E + max_vars E'

goal (1 subgoal):
 1. max_vars (inline_call E' E) \<le> length x
[PROOF STEP]
by(auto elim!: final.cases)
[PROOF STATE]
proof (state)
this:
max_vars (inline_call E' E) \<le> length x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bisim_list1 (inline_call e e', es') (ex2', exs2')

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim_list1 (inline_call e e', es') (ex2', exs2')

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
have "\<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)
[PROOF STEP]
using ex2 call1 call fin fin'
[PROOF STATE]
proof (prove)
using this:
ex2 = (E', x')
call1 E = \<lfloor>aMvs\<rfloor>
call e' = \<lfloor>aMvs\<rfloor>
final E'
final e

goal (1 subgoal):
 1. \<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)

goal (1 subgoal):
 1. \<And>e' x' ea x. \<lbrakk>ex2 = (e', x'); exs2 = (ea, x) # exs2'; ta = \<lbrace>\<rbrace>; ex2' = (inline_call e' ea, x); h' = h; final e'\<rbrakk> \<Longrightarrow> \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>
bisim_list1 (inline_call e e', es') (ex2', exs2')
\<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>
bisim_list1 (inline_call e e', es') (ex2', exs2')
\<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
using es
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile>0 \<langle>e/e' # es',h\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>inline_call e e'/es',h\<rangle>
bisim_list1 (inline_call e e', es') (ex2', exs2')
\<tau>Move1 P h (ex2, exs2) = \<tau>Move0 P h (e, es)
es = e' # es'

goal (1 subgoal):
 1. \<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)
[PROOF STEP]
by(simp del: \<tau>Move1.simps \<tau>Move0.simps) blast
[PROOF STATE]
proof (state)
this:
\<exists>e' es'. bisim_list1 (e', es') (ex2', exs2') \<and> (if \<tau>Move1 P h (ex2, exs2) then (\<tau>Red0t P t h (e, es) (e', es') \<or> countInitBlock (fst ex2') < countInitBlock (fst ex2) \<and> exs2' = exs2 \<and> e' = e \<and> es' = es) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>e'' es'' ta'. \<tau>Red0r P t h (e, es) (e'', es'') \<and> (call1 (fst ex2) = None \<or> call e = None \<or> e'' = e \<and> es'' = es) \<and> P,t \<turnstile>0 \<langle>e''/es'',h\<rangle> -ta'\<rightarrow> \<langle>e'/es',h'\<rangle> \<and> \<not> \<tau>Move0 P h (e'', es'') \<and> ta_bisim01 ta' ta)

goal:
No subgoals!
[PROOF STEP]
qed