theory ADT_IF

lemma LI_big_steps:
  "\<lbrakk> (s, s') \<in> big_steps C (internal_R C R) exmap ev;
     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, t') \<in> big_steps A (internal_R A R) exmap ev \<and> (t', s') \<in> S \<and> t' \<in> Ia" apply (drule big_stepsD) apply clarsimp apply (frule(2) sub_big_steps_I_holds[OF invariant_holds_inv_holds]) apply (drule (6) LI_sub_big_steps) apply clarsimp apply (clarsimp simp: LI_def) apply (erule_tac x=a in allE) apply (clarsimp simp: rel_semi_def) apply (drule_tac c="(t', s')" in set_mp) apply (rule_tac b="s'a" in relcompI) apply simp apply simp apply clarsimp apply (rule_tac x=y in exI) apply simp apply (subst conj_commute) apply (rule context_conjI) apply (clarsimp simp: invariant_holds_def, blast) apply (rule big_steps.cstep) apply assumption+ apply (simp add: internal_R_def) apply (subgoal_tac "Fin A t = Fin C s") apply (subgoal_tac "s' \<in> Ic") apply (subgoal_tac "Fin A y = Fin C s'") apply metis apply metis apply (simp(no_asm_use) add: invariant_holds_def, blast) apply force apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> big_steps C (internal_R C R) exmap ev; 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, t') \<in> big_steps A (internal_R A R) exmap ev \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; \<exists>s'a as a. (s'a, as) \<in> sub_big_steps C (internal_R C R) s \<and> (s'a, s') \<in> Step C a \<and> internal_R C R s s' \<and> ev = exmap (as @ [a])\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap ev \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, as) \<in> sub_big_steps C (internal_R C R) s; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a])\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, as) \<in> sub_big_steps C (internal_R C R) s; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; \<exists>t'. (t', as) \<in> sub_big_steps A (internal_R A R) t \<and> (t', s'a) \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a t'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; 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, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; S \<inter> Ia \<times> Ic ;;; Step C a \<subseteq> Step A a ;;; S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (S \<inter> Ia \<times> Ic) O Step C a \<subseteq> Step A a O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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', s') \<in> (S \<inter> Ia \<times> Ic) O Step C a
 2. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> Step A a O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (3 subgoals):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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', s'a) \<in> S \<inter> Ia \<times> Ic
 2. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> (s'a, s') \<in> Step C a
 3. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> Step A a O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> (s'a, s') \<in> Step C a
 2. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> Step A a O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (t', as) \<in> sub_big_steps A (internal_R A R) t; (t', s'a) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A 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> Step A a O S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S\<rbrakk> \<Longrightarrow> \<exists>t'. (t, t') \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (t', s') \<in> S \<and> t' \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S\<rbrakk> \<Longrightarrow> (t, y) \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> (y, s') \<in> S \<and> y \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S\<rbrakk> \<Longrightarrow> (t, y) \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) \<and> y \<in> Ia proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S\<rbrakk> \<Longrightarrow> y \<in> Ia \<and> (t, y) \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S\<rbrakk> \<Longrightarrow> y \<in> Ia
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (t, y) \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (t, y) \<in> big_steps A (internal_R A R) exmap (exmap (as @ [a])) proof (prove)
goal (4 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (?s'138 s'a as a x y, ?as138 s'a as a x y) \<in> sub_big_steps A (internal_R A R) t
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> (?s'138 s'a as a x y, y) \<in> Step A (?a138 s'a as a x y)
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> internal_R A R t y
 4. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (?as138 s'a as a x y @ [?a138 s'a as a x y]) proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> internal_R A R t y
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> R (Fin A t) (Fin A y)
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (3 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> R (Fin A t) (Fin A y)
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (4 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s; s' \<in> Ic\<rbrakk> \<Longrightarrow> R (Fin A t) (Fin A y)
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> s' \<in> Ic
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 4. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (5 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s; s' \<in> Ic; Fin A y = Fin C s'\<rbrakk> \<Longrightarrow> R (Fin A t) (Fin A y)
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s; s' \<in> Ic\<rbrakk> \<Longrightarrow> Fin A y = Fin C s'
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> s' \<in> Ic
 4. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 5. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (4 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s; s' \<in> Ic\<rbrakk> \<Longrightarrow> Fin A y = Fin C s'
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> s' \<in> Ic
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 4. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (3 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia; Fin A t = Fin C s\<rbrakk> \<Longrightarrow> s' \<in> Ic
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 3. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (2 subgoals):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; R (Fin A t) (Fin C s'); ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> Fin A t = Fin C s
 2. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal (1 subgoal):
 1. \<And>s'a as a x y. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; (t, s) \<in> S; s \<in> Ic; t \<in> Ia; (s'a, s') \<in> Step C a; internal_R C R s s'; ev = exmap (as @ [a]); s'a \<in> Ic; (x, as) \<in> sub_big_steps A (internal_R A R) t; (x, s'a) \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; (x, y) \<in> Step A a; (y, s') \<in> S; y \<in> Ia\<rbrakk> \<Longrightarrow> exmap (as @ [a]) = exmap (as @ [a]) proof (prove)
goal:
No subgoals!