theory ADT_IF

lemma LI_sub_big_steps:
  "\<lbrakk> (s',as) \<in> sub_big_steps C (internal_R C R) s;
     LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia \<rbrakk>
     \<Longrightarrow> \<exists>t'. (t',as) \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia" apply (induct rule: sub_big_steps.induct) apply (clarsimp simp: LI_def) apply (rule_tac x=t in exI) apply clarsimp apply (rule sub_big_steps.nil, simp_all)[1] apply (force simp: internal_R_def) apply (clarsimp simp: LI_def) apply (erule_tac x=e in allE) apply (clarsimp simp: rel_semi_def) apply (drule_tac c="(t', ta)" in set_mp) apply (rule_tac b=s' in relcompI) apply simp apply (rule sub_big_steps_I_holds) apply (rule invariant_holds_inv_holds, assumption+) apply clarsimp apply (rule_tac x=y in exI) apply clarsimp apply (subst conj_commute) apply (rule context_conjI) apply (erule inv_holdsE[OF invariant_holds_inv_holds]) apply assumption+ apply (rule sub_big_steps.step[OF refl]) apply assumption+ apply (subgoal_tac "z \<in> Ic") prefer 2 apply (rule_tac I=Ic in inv_holdsE[OF invariant_holds_inv_holds]) apply assumption+ apply (erule sub_big_steps_I_holds[OF invariant_holds_inv_holds]) apply assumption+ apply (subgoal_tac "Fin A t = Fin C s") apply (subgoal_tac "Fin A y = Fin C z") apply (simp(no_asm_use) add: internal_R_def) apply metis apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps C (internal_R C R) s; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', as) \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<And>evlist ta. \<lbrakk>evlist = []; ta = s; \<not> internal_R C R s s; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia
 2. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> internal_R C R s s; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<exists>t'. (t', []) \<in> sub_big_steps A (internal_R A R) t \<and> (t', s) \<in> S \<and> t' \<in> Ia
 2. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> internal_R C R s s; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (t, []) \<in> sub_big_steps A (internal_R A R) t \<and> (t, s) \<in> S \<and> t \<in> Ia
 2. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> internal_R C R s s; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (t, []) \<in> sub_big_steps A (internal_R A R) t
 2. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> internal_R C R s s; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<not> internal_R A R t t
 2. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist evlist' e s' ta. \<lbrakk>evlist = evlist' @ [e]; (s', evlist') \<in> sub_big_steps C (internal_R C R) s; \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist') \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; S \<inter> Ia \<times> Ic ;;; Step C e \<subseteq> Step A e ;;; S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (S \<inter> Ia \<times> Ic) O Step C e \<subseteq> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (t', ta) \<in> (S \<inter> Ia \<times> Ic) O Step C e
 2. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (t', ta) \<in> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (t', s') \<in> S \<inter> Ia \<times> Ic
 2. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (s', ta) \<in> Step C e
 3. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (t', ta) \<in> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> s' \<in> Ic
 2. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (s', ta) \<in> Step C e
 3. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (t', ta) \<in> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (5 subgoals):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> ?A31 evlist' e s' ta t' [> Ic
 2. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> ?s31 evlist' e s' ta t' \<in> Ic
 3. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (s', ?xs31 evlist' e s' ta t') \<in> sub_big_steps (?A31 evlist' e s' ta t') (?R31 evlist' e s' ta t') (?s31 evlist' e s' ta t')
 4. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (s', ta) \<in> Step C e
 5. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (t', ta) \<in> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' ta t'. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', ta) \<in> Step C e; \<not> internal_R C R s ta; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (t', evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (t', s') \<in> S; t' \<in> Ia; (t', ta) \<in> Step A e O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', ta) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> \<exists>t'. (t', evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (t', z) \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> (y, z) \<in> S \<and> y \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t \<and> y \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> y \<in> Ia \<and> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> y \<in> Ia
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t proof (prove)
goal (4 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> (?s47 evlist' e s' x y z, ?t47 evlist' e s' x y z) \<in> Step A (?e47 evlist' e s' x y z)
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S\<rbrakk> \<Longrightarrow> ?s47 evlist' e s' x y z \<in> Ia
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; ?t47 evlist' e s' x y z \<in> Ia\<rbrakk> \<Longrightarrow> y \<in> Ia
 4. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (y, evlist' @ [e]) \<in> sub_big_steps A (internal_R A R) t proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (?s'52 evlist' e s' x y z, evlist') \<in> sub_big_steps A (internal_R A R) t
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (?s'52 evlist' e s' x y z, y) \<in> Step A e
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> z \<in> Ic proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> z \<in> Ic
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (5 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> ?A58 evlist' e s' x y z \<Turnstile> Ic
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (?s58 evlist' e s' x y z, ?t58 evlist' e s' x y z) \<in> Step (?A58 evlist' e s' x y z) (?e58 evlist' e s' x y z)
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> ?s58 evlist' e s' x y z \<in> Ic
 4. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; ?t58 evlist' e s' x y z \<in> Ic\<rbrakk> \<Longrightarrow> z \<in> Ic
 5. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> s' \<in> Ic
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> z \<in> Ic
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (4 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> ?s59 evlist' e s' x y z \<in> Ic
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (s', ?xs59 evlist' e s' x y z) \<in> sub_big_steps C (?R59 evlist' e s' x y z) (?s59 evlist' e s' x y z)
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> z \<in> Ic
 4. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (1 subgoal):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin A t = Fin C s proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s; Fin A y = Fin C z\<rbrakk> \<Longrightarrow> \<not> internal_R A R t y
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> Fin A y = Fin C z
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin A t = Fin C s proof (prove)
goal (3 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> R (Fin C s) (Fin C z); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s; Fin A y = Fin C z\<rbrakk> \<Longrightarrow> \<not> R (Fin A t) (Fin A y)
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> Fin A y = Fin C z
 3. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin A t = Fin C s proof (prove)
goal (2 subgoals):
 1. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> Fin A y = Fin C z
 2. \<And>evlist' e s' x y z. \<lbrakk>(s', evlist') \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C e; \<not> internal_R C R s z; A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; (x, evlist') \<in> sub_big_steps A (internal_R A R) t; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, s') \<in> S; x \<in> Ia; (x, y) \<in> Step A e; (y, z) \<in> S; y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin A t = Fin C s proof (prove)
goal:
No subgoals!