[STATEMENT]
lemma sim_move01_into_Red1:
  "sim_move01 P t ta e E' h xs ta' e2' h' xs'
  \<Longrightarrow> if \<tau>Move0 P h (e, es1)
      then \<tau>Red1't P t h ((E', xs), exs2) ((e2', xs'), exs2) \<and> ta = \<epsilon> \<and> h = h'
      else \<exists>ex2' exs2' ta'. \<tau>Red1'r P t h ((E', xs), exs2) (ex2', exs2') \<and>
                           (call e = None \<or> call1 E' = None \<or> ex2' = (E', xs) \<and> exs2' = exs2) \<and>
                           False,P,t \<turnstile>1 \<langle>ex2'/exs2',h\<rangle> -ta'\<rightarrow> \<langle>(e2', xs')/exs2,h'\<rangle> \<and>
                           \<not> \<tau>Move1 P h (ex2', exs2') \<and> ta_bisim01 ta ta'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move01 P t ta e E' h xs ta' e2' h' xs' \<Longrightarrow> if \<tau>Move0 P h (e, es1) then \<tau>Red1't P t h ((E', xs), exs2) ((e2', xs'), exs2) \<and> ta = \<lbrace>\<rbrace> \<and> h = h' else \<exists>ex2' exs2' ta'. \<tau>Red1'r P t h ((E', xs), exs2) (ex2', exs2') \<and> (call e = None \<or> call1 E' = None \<or> ex2' = (E', xs) \<and> exs2' = exs2) \<and> False,P,t \<turnstile>1 \<langle>ex2'/exs2',h\<rangle> -ta'\<rightarrow> \<langle>(e2', xs')/exs2,h'\<rangle> \<and> \<not> \<tau>Move1 P h (ex2', exs2') \<and> ta_bisim01 ta ta'
[PROOF STEP]
apply(auto simp add: sim_move01_def intro: \<tau>red1t_into_\<tau>Red1t \<tau>red1r_into_\<tau>Red1r red1Red split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e; \<not> final e; ta_bisim01 ta (extTA2J1 P ta'); \<tau>red1'r P t h (E', xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e2',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call e = None\<rbrakk> \<Longrightarrow> \<exists>ex2' exs2'. \<tau>Red1'r P t h ((E', xs), exs2) (ex2', exs2') \<and> (\<exists>ta'. False,P,t \<turnstile>1 \<langle>ex2'/exs2',h\<rangle> -ta'\<rightarrow> \<langle>(e2', xs')/exs2,h'\<rangle> \<and> \<not> \<tau>Move1 P h (ex2', exs2') \<and> ta_bisim01 ta ta')
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e; \<not> final e; ta_bisim01 ta (extTA2J1 P ta'); \<tau>red1'r P t h (E', xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta'\<rightarrow> \<langle>e2',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 E' = None\<rbrakk> \<Longrightarrow> \<exists>ex2' exs2'. \<tau>Red1'r P t h ((E', xs), exs2) (ex2', exs2') \<and> (\<exists>ta'. False,P,t \<turnstile>1 \<langle>ex2'/exs2',h\<rangle> -ta'\<rightarrow> \<langle>(e2', xs')/exs2,h'\<rangle> \<and> \<not> \<tau>Move1 P h (ex2', exs2') \<and> ta_bisim01 ta ta')
 3. \<And>a aa b ab ac ba. \<lbrakk>\<not> \<tau>move0 P h e; call e = \<lfloor>(a, aa, b)\<rfloor>; call1 E' = \<lfloor>(ab, ac, ba)\<rfloor>; \<not> final e; ta_bisim01 ta (extTA2J1 P ta'); False,P,t \<turnstile>1 \<langle>E',(h, xs)\<rangle> -ta'\<rightarrow> \<langle>e2',(h', xs')\<rangle>; \<not> \<tau>move1 P h E'\<rbrakk> \<Longrightarrow> \<exists>ta'. False,P,t \<turnstile>1 \<langle>(E', xs)/exs2,h\<rangle> -ta'\<rightarrow> \<langle>(e2', xs')/exs2,h'\<rangle> \<and> \<not> final E' \<and> ta_bisim01 ta ta'
[PROOF STEP]
apply(fastforce intro: red1Red intro!: \<tau>red1r_into_\<tau>Red1r)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move01_max_vars_decr:
  "sim_move01 P t ta e0 e h xs ta' e' h' xs' \<Longrightarrow> max_vars e' \<le> max_vars e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move01 P t ta e0 e h xs ta' e' h' xs' \<Longrightarrow> max_vars e' \<le> max_vars e
[PROOF STEP]
by(fastforce simp add: sim_move01_def split: if_split_asm dest: \<tau>red1t_max_vars red1_max_vars_decr \<tau>red1r_max_vars)