theory Simulation

lemma fw_inv_transport:
  "\<lbrakk> A \<Turnstile> I\<^sub>a; C \<Turnstile> I\<^sub>c; LI A C R (I\<^sub>a \<times> I\<^sub>c) \<rbrakk> \<Longrightarrow> C \<Turnstile> {s'. \<exists>s. (s,s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}" apply (clarsimp simp: LI_def invariant_holds_def) apply (rule conjI) apply (rule allI) apply clarsimp apply (subgoal_tac "x \<in> (R `` Init A s)") prefer 2 apply fastforce apply blast apply clarsimp apply (erule_tac x=j in allE)+ apply (clarsimp simp: rel_semi_def) apply (subgoal_tac "(s,x) \<in> Step A j O R") prefer 2 apply blast apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Turnstile> I\<^sub>a; C \<Turnstile> I\<^sub>c; LI A C R (I\<^sub>a \<times> I\<^sub>c)\<rbrakk> \<Longrightarrow> C \<Turnstile> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (\<forall>s. Init C s \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}) \<and> (\<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>s. Init C s \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}
 2. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> Init C s \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c}
 2. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c
 2. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s; x \<in> R `` Init A s\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c
 2. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s\<rbrakk> \<Longrightarrow> x \<in> R `` Init A s
 3. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s\<rbrakk> \<Longrightarrow> x \<in> R `` Init A s
 2. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s; x \<in> R `` Init A s\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c
 3. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; x \<in> Init C s; x \<in> R `` Init A s\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c
 2. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<forall>j. Step C j `` {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} \<subseteq> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c} proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>j. Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>j. Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>j. R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; R \<inter> I\<^sub>a \<times> I\<^sub>c ;;; Step C j \<subseteq> Step A j ;;; R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c proof (prove)
goal (2 subgoals):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c
 2. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> (s, x) \<in> Step A j O R proof (prove)
goal (2 subgoals):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> (s, x) \<in> Step A j O R
 2. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>\<forall>s. Init A s \<subseteq> I\<^sub>a; \<forall>s. Init C s \<subseteq> I\<^sub>c; \<forall>s. Init C s \<subseteq> R `` Init A s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> I\<^sub>a \<and> s' \<in> I\<^sub>c \<longrightarrow> Fin C s' = Fin A s; (xa, x) \<in> Step C j; (s, xa) \<in> R; s \<in> I\<^sub>a; xa \<in> I\<^sub>c; Step A j `` I\<^sub>a \<subseteq> I\<^sub>a; Step C j `` I\<^sub>c \<subseteq> I\<^sub>c; (R \<inter> I\<^sub>a \<times> I\<^sub>c) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> I\<^sub>a \<and> x \<in> I\<^sub>c proof (prove)
goal:
No subgoals!