theory Noninterference_Refinement

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 [> Ia; C [> 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 assumption+ apply clarsimp apply (rule_tac x=y in exI) apply clarsimp apply (subst conj_commute) apply (rule context_conjI) apply (erule inv_holdsE) 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) apply assumption+ apply (erule sub_big_steps_I_holds) apply assumption+ apply (force simp: internal_R_def) 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> 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> (?s45 evlist' e s' x y z, ?t45 evlist' e s' x y z) \<in> Step A (?e45 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 [> 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> ?s45 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 [> 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; ?t45 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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'49 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 [> Ia; C [> 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'49 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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> ?A55 evlist' e s' x y z [> 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 [> Ia; C [> 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> (?s55 evlist' e s' x y z, ?t55 evlist' e s' x y z) \<in> Step (?A55 evlist' e s' x y z) (?e55 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 [> Ia; C [> 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> ?s55 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 [> Ia; C [> 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; ?t55 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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 [> 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> ?s56 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 [> 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', ?xs56 evlist' e s' x y z) \<in> sub_big_steps C (?R56 evlist' e s' x y z) (?s56 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 [> Ia; C [> 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 [> Ia; C [> 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 [> Ia; C [> 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:
No subgoals!