[STATEMENT]
lemma sim_move10_into_red0:
  assumes wwf: "wwf_J_prog P"
  and sim: "sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'"
  and fv: "fv e = {}"
  shows "if \<tau>move1 P h e2
         then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty) \<and> ta = \<epsilon> \<and> h = h'
         else \<exists>e'' ta'. \<tau>Red0r P t h (e, es) (e'', es) \<and>
                        (call1 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
proof(cases "\<tau>move1 P h e2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
 2. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<tau>move1 P h e2

goal (2 subgoals):
 1. \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
 2. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
with sim
[PROOF STATE]
proof (chain)
picking this:
sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'
\<tau>move1 P h e2
[PROOF STEP]
have "\<not> final e2"
    and red: "\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<or>
              countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty"
    and [simp]: "h' = h" "ta = \<epsilon>" "ta' = \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'
\<tau>move1 P h e2

goal (1 subgoal):
 1. \<not> final e2 &&& \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty &&& h' = h &&& ta = \<lbrace>\<rbrace> &&& ta' = \<lbrace>\<rbrace>
[PROOF STEP]
by(simp_all add: sim_move10_def)
[PROOF STATE]
proof (state)
this:
\<not> final e2
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
h' = h
ta = \<lbrace>\<rbrace>
ta' = \<lbrace>\<rbrace>

goal (2 subgoals):
 1. \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
 2. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
from red
[PROOF STATE]
proof (chain)
picking this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
have "\<tau>Red0t P t h (e, es) (e', es) \<or>
                 countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty"
[PROOF STATE]
proof (prove)
using this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty

goal (1 subgoal):
 1. \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
assume red: "\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x')"
[PROOF STATE]
proof (state)
this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x')

goal (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
from \<tau>red0t_fv_subset[OF wwf red] \<tau>red0t_dom_lcl[OF wwf red] fv
[PROOF STATE]
proof (chain)
picking this:
fv e' \<subseteq> fv e
dom x' \<subseteq> dom Map.empty \<union> fv e
fv e = {}
[PROOF STEP]
have "dom x' \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
fv e' \<subseteq> fv e
dom x' \<subseteq> dom Map.empty \<union> fv e
fv e = {}

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

goal (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[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 (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
with red
[PROOF STATE]
proof (chain)
picking this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x')
x' = Map.empty
[PROOF STEP]
have "\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)"
[PROOF STATE]
proof (prove)
using this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x')
x' = Map.empty

goal (1 subgoal):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)

goal (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
with wwf
[PROOF STATE]
proof (chain)
picking this:
wwf_J_prog P
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)
[PROOF STEP]
have "\<tau>Red0t P t h (e, es) (e', es)"
[PROOF STATE]
proof (prove)
using this:
wwf_J_prog P
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)

goal (1 subgoal):
 1. \<tau>Red0t P t h (e, es) (e', es)
[PROOF STEP]
using fv
[PROOF STATE]
proof (prove)
using this:
wwf_J_prog P
\<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)
fv e = {}

goal (1 subgoal):
 1. \<tau>Red0t P t h (e, es) (e', es)
[PROOF STEP]
by(rule \<tau>red0t_into_\<tau>Red0t)
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h (e, es) (e', es)

goal (2 subgoals):
 1. \<tau>red0t (extTA2J0 P) P t h (e, Map.empty) (e', x') \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
 2. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0t P t h (e, es) (e', es)

goal (1 subgoal):
 1. \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty

goal (1 subgoal):
 1. countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty \<Longrightarrow> \<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty

goal (2 subgoals):
 1. \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
 2. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
\<tau>move1 P h e2
\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau>move1 P h e2
\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = e \<and> x' = Map.empty

goal (1 subgoal):
 1. if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<tau>move1 P h e2

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
with sim
[PROOF STATE]
proof (chain)
picking this:
sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'
\<not> \<tau>move1 P h e2
[PROOF STEP]
obtain e'' xs'' where "\<not> final e2"
    and \<tau>red: "\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs'')"
    and red: "extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>"
    and call: "call1 e2 = None \<or> call e = None \<or> e'' = e"
    and "\<not> \<tau>move0 P h e''" "ta_bisim01 ta' (extTA2J1 (compP1 P) ta)" "no_call P h e''"
[PROOF STATE]
proof (prove)
using this:
sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'
\<not> \<tau>move1 P h e2

goal (1 subgoal):
 1. (\<And>e'' xs''. \<lbrakk>\<not> final e2; \<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>e',(h', x')\<rangle>; call1 e2 = None \<or> call e = None \<or> e'' = e; \<not> \<tau>move0 P h e''; ta_bisim01 ta' (extTA2J1 (compP1 P) ta); no_call P h e''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: sim_move10_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<not> final e2
\<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>e',(h', x')\<rangle>
call1 e2 = None \<or> call e = None \<or> e'' = e
\<not> \<tau>move0 P h e''
ta_bisim01 ta' (extTA2J1 (compP1 P) ta)
no_call P h e''

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
from \<tau>red0r_fv_subset[OF wwf \<tau>red] \<tau>red0r_dom_lcl[OF wwf \<tau>red] fv
[PROOF STATE]
proof (chain)
picking this:
fv e'' \<subseteq> fv e
dom xs'' \<subseteq> dom Map.empty \<union> fv e
fv e = {}
[PROOF STEP]
have "dom xs'' \<subseteq> {}"
[PROOF STATE]
proof (prove)
using this:
fv e'' \<subseteq> fv e
dom xs'' \<subseteq> dom Map.empty \<union> fv e
fv e = {}

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

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
hence "xs'' = Map.empty"
[PROOF STATE]
proof (prove)
using this:
dom xs'' \<subseteq> {}

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

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
with \<tau>red
[PROOF STATE]
proof (chain)
picking this:
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs'')
xs'' = Map.empty
[PROOF STEP]
have "\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)"
[PROOF STATE]
proof (prove)
using this:
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs'')
xs'' = Map.empty

goal (1 subgoal):
 1. \<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
with wwf
[PROOF STATE]
proof (chain)
picking this:
wwf_J_prog P
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)
[PROOF STEP]
have "\<tau>Red0r P t h (e, es) (e'', es)"
[PROOF STATE]
proof (prove)
using this:
wwf_J_prog P
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)

goal (1 subgoal):
 1. \<tau>Red0r P t h (e, es) (e'', es)
[PROOF STEP]
using fv
[PROOF STATE]
proof (prove)
using this:
wwf_J_prog P
\<tau>red0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)
fv e = {}

goal (1 subgoal):
 1. \<tau>Red0r P t h (e, es) (e'', es)
[PROOF STEP]
by(rule \<tau>red0r_into_\<tau>Red0r)
[PROOF STATE]
proof (state)
this:
\<tau>Red0r P t h (e, es) (e'', es)

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>Red0r P t h (e, es) (e'', es)

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
from red \<open>xs'' = Map.empty\<close>
[PROOF STATE]
proof (chain)
picking this:
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>
xs'' = Map.empty
[PROOF STEP]
have "extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, Map.empty)\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>"
[PROOF STATE]
proof (prove)
using this:
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>
xs'' = Map.empty

goal (1 subgoal):
 1. extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, Map.empty)\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, Map.empty)\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
from red0Red[OF this] \<open>no_call P h e''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>aMvs. call e'' = \<lfloor>aMvs\<rfloor> \<longrightarrow> synthesized_call P h aMvs \<Longrightarrow> P,t \<turnstile>0 \<langle>e''/?es,h\<rangle> -ta'\<rightarrow> \<langle>e'/?es,h'\<rangle>
no_call P h e''
[PROOF STEP]
have "P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<forall>aMvs. call e'' = \<lfloor>aMvs\<rfloor> \<longrightarrow> synthesized_call P h aMvs \<Longrightarrow> P,t \<turnstile>0 \<langle>e''/?es,h\<rangle> -ta'\<rightarrow> \<langle>e'/?es,h'\<rangle>
no_call P h e''

goal (1 subgoal):
 1. P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>
[PROOF STEP]
by(simp add: no_call_def)
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
from \<open>\<not> \<tau>move0 P h e''\<close> red
[PROOF STATE]
proof (chain)
picking this:
\<not> \<tau>move0 P h e''
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>
[PROOF STEP]
have "\<not> \<tau>Move0 P h (e'', es)"
[PROOF STATE]
proof (prove)
using this:
\<not> \<tau>move0 P h e''
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e',(h', x')\<rangle>

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

goal (1 subgoal):
 1. \<not> \<tau>move1 P h e2 \<Longrightarrow> if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau>Red0r P t h (e, es) (e'', es)
P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>
\<not> \<tau>Move0 P h (e'', es)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0r P t h (e, es) (e'', es)
P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>
\<not> \<tau>Move0 P h (e'', es)

goal (1 subgoal):
 1. if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
using False \<open>ta_bisim01 ta' (extTA2J1 (compP1 P) ta)\<close> call
[PROOF STATE]
proof (prove)
using this:
\<tau>Red0r P t h (e, es) (e'', es)
P,t \<turnstile>0 \<langle>e''/es,h\<rangle> -ta'\<rightarrow> \<langle>e'/es,h'\<rangle>
\<not> \<tau>Move0 P h (e'', es)
\<not> \<tau>move1 P h e2
ta_bisim01 ta' (extTA2J1 (compP1 P) ta)
call1 e2 = None \<or> call e = None \<or> e'' = e

goal (1 subgoal):
 1. if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)
[PROOF STEP]
by(simp del: \<tau>Move0.simps) blast
[PROOF STATE]
proof (state)
this:
if \<tau>move1 P h e2 then (\<tau>Red0t P t h (e, es) (e', es) \<or> countInitBlock e2' < countInitBlock e2 \<and> e' = 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 e2 = None \<or> call e = None \<or> e'' = e) \<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' (extTA2J1 (compP1 P) ta)

goal:
No subgoals!
[PROOF STEP]
qed