theory Noninterference_Refinement

lemma LI_trans:
  "\<lbrakk>LI A H R (Ia \<times> Ih); LI H C S (Ih \<times> Ic); H \<Turnstile> Ih\<rbrakk>
    \<Longrightarrow> LI A C (R O (S \<inter> {(h, c). h \<in> Ih})) (Ia \<times> Ic)" apply (clarsimp simp: LI_def) apply safe apply (clarsimp simp: Image_def) apply (erule_tac x=s in allE)+ apply (drule(1) set_mp) apply clarsimp apply (drule(1) set_mp) apply (clarsimp simp: invariant_holds_def) apply blast apply (clarsimp simp: rel_semi_def) apply (erule_tac x=j in allE)+ apply (drule_tac c="(ya, z)" in set_mp) apply blast apply (clarsimp simp: invariant_holds_def) apply blast apply (erule_tac x=x in allE) apply (erule_tac x=y in allE)+ apply (erule_tac x=z in allE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LI A H R (Ia \<times> Ih); LI H C S (Ih \<times> Ic); H \<Turnstile> Ih\<rbrakk> \<Longrightarrow> LI A C (R O (S \<inter> {(h, c). h \<in> Ih})) (Ia \<times> Ic) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s\<rbrakk> \<Longrightarrow> (\<forall>s. Init C s \<subseteq> (R O (S \<inter> {(h, c). h \<in> Ih})) `` Init A s) \<and> (\<forall>j. R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})) \<and> (\<forall>s s'. (s, s') \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s) proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s\<rbrakk> \<Longrightarrow> x \<in> (R O (S \<inter> {(h, c). h \<in> Ih})) `` Init A s
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> {y. \<exists>x\<in>Init A s. (x, y) \<in> R}; \<forall>s. Init C s \<subseteq> {y. \<exists>x\<in>Init H s. (x, y) \<in> S}; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>H \<Turnstile> Ih; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s; Init H s \<subseteq> {y. \<exists>x\<in>Init A s. (x, y) \<in> R}; Init C s \<subseteq> {y. \<exists>x\<in>Init H s. (x, y) \<in> S}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>H \<Turnstile> Ih; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s; Init H s \<subseteq> {y. \<exists>x\<in>Init A s. (x, y) \<in> R}; x \<in> {y. \<exists>x\<in>Init H s. (x, y) \<in> S}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa. \<lbrakk>H \<Turnstile> Ih; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s; Init H s \<subseteq> {y. \<exists>x\<in>Init A s. (x, y) \<in> R}; xa \<in> Init H s; (xa, x) \<in> S\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa. \<lbrakk>H \<Turnstile> Ih; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s; xa \<in> Init H s; (xa, x) \<in> S; xa \<in> {y. \<exists>x\<in>Init A s. (x, y) \<in> R}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>s x xa xb. \<lbrakk>\<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; x \<in> Init C s; xa \<in> Init H s; (xa, x) \<in> S; xb \<in> Init A s; (xb, xa) \<in> R; \<forall>s. Init H s \<subseteq> Ih; \<forall>j. Step H j `` Ih \<subseteq> Ih\<rbrakk> \<Longrightarrow> \<exists>xa\<in>Init A s. (xa, x) \<in> R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>j a b. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (a, b) \<in> R O (S \<inter> {(h, c). h \<in> Ih}) \<inter> Ia \<times> Ic ;;; Step C j\<rbrakk> \<Longrightarrow> (a, b) \<in> Step A j ;;; R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>j z xa ya za. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. (S \<inter> Ih \<times> Ic) O Step C j \<subseteq> Step H j O S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, z) \<in> Step C j; (xa, ya) \<in> R; (ya, za) \<in> S; ya \<in> Ih; xa \<in> Ia; za \<in> Ic\<rbrakk> \<Longrightarrow> (xa, z) \<in> Step A j O R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>j z xa ya za. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, z) \<in> Step C j; (xa, ya) \<in> R; (ya, za) \<in> S; ya \<in> Ih; xa \<in> Ia; za \<in> Ic; (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R; (S \<inter> Ih \<times> Ic) O Step C j \<subseteq> Step H j O S\<rbrakk> \<Longrightarrow> (xa, z) \<in> Step A j O R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>j z xa ya za. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, z) \<in> Step C j; (xa, ya) \<in> R; (ya, za) \<in> S; ya \<in> Ih; xa \<in> Ia; za \<in> Ic; (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> (ya, z) \<in> (S \<inter> Ih \<times> Ic) O Step C j
 2. \<And>j z xa ya za. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, z) \<in> Step C j; (xa, ya) \<in> R; (ya, za) \<in> S; ya \<in> Ih; xa \<in> Ia; za \<in> Ic; (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R; (ya, z) \<in> Step H j O S\<rbrakk> \<Longrightarrow> (xa, z) \<in> Step A j O R O (S \<inter> {(h, c). h \<in> Ih})
 3. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>j z xa ya za. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, z) \<in> Step C j; (xa, ya) \<in> R; (ya, za) \<in> S; ya \<in> Ih; xa \<in> Ia; za \<in> Ic; (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R; (ya, z) \<in> Step H j O S\<rbrakk> \<Longrightarrow> (xa, z) \<in> Step A j O R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>j xa za x y zb. \<lbrakk>\<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (za, zb) \<in> Step C j; (xa, x) \<in> R; (x, za) \<in> S; x \<in> Ih; xa \<in> Ia; za \<in> Ic; (R \<inter> Ia \<times> Ih) O Step H j \<subseteq> Step A j O R; (x, y) \<in> Step H j; (y, zb) \<in> S; \<forall>s. Init H s \<subseteq> Ih; \<forall>j. Step H j `` Ih \<subseteq> Ih\<rbrakk> \<Longrightarrow> (xa, zb) \<in> Step A j O R O (S \<inter> {(h, c). h \<in> Ih})
 2. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A s; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H s; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic; \<forall>s'. (x, s') \<in> R \<and> x \<in> Ia \<and> s' \<in> Ih \<longrightarrow> Fin H s' = Fin A x\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic; \<forall>s'. (y, s') \<in> S \<and> y \<in> Ih \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin H y; (x, y) \<in> R \<and> x \<in> Ia \<and> y \<in> Ih \<longrightarrow> Fin H y = Fin A x\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>s s' x y z. \<lbrakk>H \<Turnstile> Ih; \<forall>s. Init H s \<subseteq> R `` Init A s; \<forall>s. Init C s \<subseteq> S `` Init H s; \<forall>j. R \<inter> Ia \<times> Ih ;;; Step H j \<subseteq> Step A j ;;; R; \<forall>j. S \<inter> Ih \<times> Ic ;;; Step C j \<subseteq> Step H j ;;; S; (x, y) \<in> R; (y, z) \<in> S; y \<in> Ih; x \<in> Ia; z \<in> Ic; (x, y) \<in> R \<and> x \<in> Ia \<and> y \<in> Ih \<longrightarrow> Fin H y = Fin A x; (y, z) \<in> S \<and> y \<in> Ih \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin H y\<rbrakk> \<Longrightarrow> Fin C z = Fin A x proof (prove)
goal:
No subgoals!