theory Noninterference_Refinement

lemma LI_rel_terminate:
  fixes s0
  assumes ex_abs: "\<And>s'. s' \<in> Ic \<Longrightarrow> (\<exists>s. s \<in> Ia \<and> (s, s') \<in> S)"
  assumes rel_correct: "\<And>s s' s0''. \<lbrakk>(internal_R C R)\<^sup>+\<^sup>+ s0'' s'; s0''\<in>Init C s0; (s, s') \<in> S\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s"
  assumes init_rel_correct: "\<And>s0''. s0'' \<in> Init C s0 \<Longrightarrow> \<exists>s0' \<in> Init A s0. (s0', s0'') \<in> S"
  assumes Ia_inv: "A [> Ia"
  assumes s0_Ia: "Init A s0 \<subseteq> Ia"
  assumes Ic_inv: "C [> Ic"
  assumes s0_Ic: "Init C s0 \<subseteq> Ic"
  assumes li: "LI A C S (Ia \<times> Ic)"
  shows "\<lbrakk>rel_terminate A s0 (internal_R A R) Ia (internal_R A measuref)\<rbrakk>
    \<Longrightarrow> rel_terminate C s0 (internal_R C R) Ic (internal_R C measuref)" apply (simp add: rel_terminate_def) apply (clarsimp simp: rtranclp_def2) apply (erule disjE) apply (cut_tac s'=s in ex_abs, assumption) apply clarsimp apply (cut_tac s=sa and s'=s in rel_correct, assumption+) apply (erule_tac x="sa" in allE) apply simp apply (erule impE) apply blast apply (erule_tac x=as in allE) apply (frule(3) LI_sub_big_steps'[OF _ li Ia_inv Ic_inv]) apply clarsimp apply (erule_tac x=t' in allE) apply simp using li apply (clarsimp simp: LI_def) apply (erule_tac x=a in allE) apply (clarsimp simp: rel_semi_def) apply (frule(1) sub_big_steps_I_holds[OF Ic_inv]) apply (drule_tac c="(t', s'')" in set_mp) apply blast apply clarsimp apply (erule_tac x=y in allE) apply (erule impE) apply blast apply (simp add: internal_R_def) apply (frule_tac x=sa in spec, drule_tac x=s in spec) apply (frule_tac x=y in spec, drule_tac x=z in spec) apply (drule_tac x=x in spec, drule_tac x=s' in spec) apply simp using Ia_inv Ic_inv apply (clarsimp simp: invariant_holds_def inv_holds_def) apply (erule_tac x=a in allE)+ apply (drule_tac c=y in set_mp, blast) apply (drule_tac c=z in set_mp, blast) apply simp apply clarsimp apply (cut_tac s0''=s0' in init_rel_correct, assumption+) apply clarsimp apply (erule_tac x="s0'a" in allE) apply (frule set_mp[OF s0_Ia]) apply (erule impE) apply blast apply (erule_tac x=as in allE) apply (frule(3) LI_sub_big_steps'[OF _ li Ia_inv Ic_inv]) apply clarsimp apply (erule_tac x=t' in allE) apply simp using li apply (clarsimp simp: LI_def) apply (erule_tac x=a in allE)+ apply (clarsimp simp: rel_semi_def) apply (frule(1) sub_big_steps_I_holds[OF Ic_inv]) apply (drule_tac c="(t', s'')" in set_mp) apply blast apply clarsimp apply (erule_tac x=y in allE) apply (erule impE) apply blast apply (simp add: internal_R_def) apply (frule_tac x=s0'a in spec, drule_tac x=s0' in spec) apply (frule_tac x=y in spec, drule_tac x=z in spec) apply (drule_tac x=x in spec, drule_tac x=s' in spec) apply simp using Ia_inv Ic_inv apply (clarsimp simp: invariant_holds_def inv_holds_def) apply (erule_tac x=a in allE)+ apply (drule_tac c=y in set_mp, blast) apply (drule_tac c=z in set_mp, blast) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_terminate A s0 (internal_R A R) Ia (internal_R A measuref) \<Longrightarrow> rel_terminate C s0 (internal_R C R) Ic (internal_R C measuref) proof (prove)
goal (1 subgoal):
 1. \<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>*\<^sup>* s0' s) \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))) \<Longrightarrow> \<forall>s. s \<in> Ic \<and> (\<exists>s0'\<in>Init C s0. (internal_R C R)\<^sup>*\<^sup>* s0' s) \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps C (internal_R C R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step C a) \<longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s''))) proof (prove)
goal (1 subgoal):
 1. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (internal_R C R)\<^sup>+\<^sup>+ s0' s \<or> s = s0'; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; \<exists>sa. sa \<in> Ia \<and> (sa, s) \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; sa \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa \<or> sa = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa \<or> sa = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (3 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa \<or> sa = s0'
 2. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; \<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 3. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; \<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' sa; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')); \<exists>t'. (t', as) \<in> sub_big_steps A (internal_R A R) sa \<and> (t', s') \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa s' \<and> (0 < internal_R A measuref sa s' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')); s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) sa \<longrightarrow> (\<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
using this:
LI A C S (Ia \<times> Ic)

goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s'')\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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; s' \<in> Ic\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (3 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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' \<in> Ic\<rbrakk> \<Longrightarrow> (t', s'') \<in> (S \<inter> Ia \<times> Ic) O Step C a
 2. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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' \<in> Ic; (t', s'') \<in> Step A a O S\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 3. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' s'' a sa s0'a t'. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (t', as) \<in> sub_big_steps A (internal_R A R) sa; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa t' \<and> (0 < internal_R A measuref sa t' \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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' \<in> Ic; (t', s'') \<in> Step A a O S\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'')
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s''. (\<exists>a. (x, s'') \<in> Step A a) \<longrightarrow> internal_R A measuref sa s'' < internal_R A measuref sa x \<and> (0 < internal_R A measuref sa x \<longrightarrow> internal_R A measuref sa s'' = 0 \<longrightarrow> internal_R A R sa s''); \<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' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s z < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s z = 0 \<longrightarrow> internal_R C R s z)
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; (\<exists>a. (x, y) \<in> Step A a) \<longrightarrow> internal_R A measuref sa y < internal_R A measuref sa x \<and> (0 < internal_R A measuref sa x \<longrightarrow> internal_R A measuref sa y = 0 \<longrightarrow> internal_R A R sa y)\<rbrakk> \<Longrightarrow> internal_R C measuref s z < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s z = 0 \<longrightarrow> internal_R C R s z)
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (3 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S\<rbrakk> \<Longrightarrow> \<exists>a. (x, y) \<in> Step A a
 2. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; internal_R A measuref sa y < internal_R A measuref sa x \<and> (0 < internal_R A measuref sa x \<longrightarrow> internal_R A measuref sa y = 0 \<longrightarrow> internal_R A R sa y)\<rbrakk> \<Longrightarrow> internal_R C measuref s z < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s z = 0 \<longrightarrow> internal_R C R s z)
 3. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; internal_R A measuref sa y < internal_R A measuref sa x \<and> (0 < internal_R A measuref sa x \<longrightarrow> internal_R A measuref sa y = 0 \<longrightarrow> internal_R A R sa y)\<rbrakk> \<Longrightarrow> internal_R C measuref s z < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s z = 0 \<longrightarrow> internal_R C R s z)
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y))\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)); (sa, s) \<in> S \<and> sa \<in> Ia \<and> s \<in> Ic \<longrightarrow> Fin C s = Fin A sa\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)); (sa, s) \<in> S \<and> sa \<in> Ia \<and> s \<in> Ic \<longrightarrow> Fin C s = Fin A sa; (y, z) \<in> S \<and> y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)); (sa, s) \<in> S \<and> sa \<in> Ia \<and> s \<in> Ic \<longrightarrow> Fin C s = Fin A sa; (y, z) \<in> S \<and> y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; (x, s') \<in> S \<and> x \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)); Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
using this:
A [> Ia
C [> Ic

goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x) \<and> (0 < measuref (Fin A sa) (Fin A x) \<longrightarrow> measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)); Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; \<forall>j. Step A j `` Ia \<subseteq> Ia; \<forall>j. Step C j `` Ic \<subseteq> Ic; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x); measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y)\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x); measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y); Step A a `` Ia \<subseteq> Ia; Step C a `` Ic \<subseteq> Ic\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x); measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y); Step C a `` Ic \<subseteq> Ic; y \<in> Ia\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (2 subgoals):
 1. \<And>s as s' s0' a sa s0'a x y z. \<lbrakk>s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', z) \<in> Step C a; (internal_R C R)\<^sup>+\<^sup>+ s0' s; sa \<in> Ia; (sa, s) \<in> S; s0'a \<in> Init A s0; (internal_R A R)\<^sup>+\<^sup>+ s0'a sa; (x, as) \<in> sub_big_steps A (internal_R A R) sa; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s = Fin A sa; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A sa) (Fin A y) < measuref (Fin A sa) (Fin A x); measuref (Fin A sa) (Fin A y) = 0 \<longrightarrow> R (Fin A sa) (Fin A y); y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> measuref (Fin A sa) (Fin C z) < measuref (Fin A sa) (Fin A x) \<and> (measuref (Fin A sa) (Fin C z) = 0 \<longrightarrow> R (Fin A sa) (Fin C z))
 2. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>s as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s; (s', s'') \<in> Step C a; s = s0'\<rbrakk> \<Longrightarrow> internal_R C measuref s s'' < internal_R C measuref s s' \<and> (0 < internal_R C measuref s s' \<longrightarrow> internal_R C measuref s s'' = 0 \<longrightarrow> internal_R C R s s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; \<exists>s0'a\<in>Init A s0. (s0'a, s0') \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>\<forall>s. s \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s \<or> s = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s s'' < internal_R A measuref s s' \<and> (0 < internal_R A measuref s s' \<longrightarrow> internal_R A measuref s s'' = 0 \<longrightarrow> internal_R A R s s''))); s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s0'a \<or> s0'a = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s'')))\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s0'a \<or> s0'a = s0') \<longrightarrow> (\<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''))); s0'a \<in> Ia\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (2 subgoals):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia\<rbrakk> \<Longrightarrow> s0'a \<in> Ia \<and> (\<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s0'a \<or> s0'a = s0')
 2. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; \<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; \<forall>as s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s'')); \<exists>t'. (t', as) \<in> sub_big_steps A (internal_R A R) s0'a \<and> (t', s') \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; \<forall>s'. (s', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (s', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a s' \<and> (0 < internal_R A measuref s0'a s' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s'')); (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a \<longrightarrow> (\<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''))\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s'')\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
using this:
LI A C S (Ia \<times> Ic)

goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s'')\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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; s' \<in> Ic\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (2 subgoals):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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' \<in> Ic\<rbrakk> \<Longrightarrow> (t', s'') \<in> (S \<inter> Ia \<times> Ic) O Step C a
 2. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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' \<in> Ic; (t', s'') \<in> Step A a O S\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' s'' a s0'a t'. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', s'') \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (t', as) \<in> sub_big_steps A (internal_R A R) s0'a; (t', s') \<in> S; t' \<in> Ia; \<forall>s''. (\<exists>a. (t', s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a t' \<and> (0 < internal_R A measuref s0'a t' \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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' \<in> Ic; (t', s'') \<in> Step A a O S\<rbrakk> \<Longrightarrow> internal_R C measuref s0' s'' < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' s'' = 0 \<longrightarrow> internal_R C R s0' s'') proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s''. (\<exists>a. (x, s'') \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a s'' < internal_R A measuref s0'a x \<and> (0 < internal_R A measuref s0'a x \<longrightarrow> internal_R A measuref s0'a s'' = 0 \<longrightarrow> internal_R A R s0'a s''); \<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' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S\<rbrakk> \<Longrightarrow> internal_R C measuref s0' z < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' z = 0 \<longrightarrow> internal_R C R s0' z) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; (\<exists>a. (x, y) \<in> Step A a) \<longrightarrow> internal_R A measuref s0'a y < internal_R A measuref s0'a x \<and> (0 < internal_R A measuref s0'a x \<longrightarrow> internal_R A measuref s0'a y = 0 \<longrightarrow> internal_R A R s0'a y)\<rbrakk> \<Longrightarrow> internal_R C measuref s0' z < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' z = 0 \<longrightarrow> internal_R C R s0' z) proof (prove)
goal (2 subgoals):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S\<rbrakk> \<Longrightarrow> \<exists>a. (x, y) \<in> Step A a
 2. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; internal_R A measuref s0'a y < internal_R A measuref s0'a x \<and> (0 < internal_R A measuref s0'a x \<longrightarrow> internal_R A measuref s0'a y = 0 \<longrightarrow> internal_R A R s0'a y)\<rbrakk> \<Longrightarrow> internal_R C measuref s0' z < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' z = 0 \<longrightarrow> internal_R C R s0' z) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; internal_R A measuref s0'a y < internal_R A measuref s0'a x \<and> (0 < internal_R A measuref s0'a x \<longrightarrow> internal_R A measuref s0'a y = 0 \<longrightarrow> internal_R A R s0'a y)\<rbrakk> \<Longrightarrow> internal_R C measuref s0' z < internal_R C measuref s0' s' \<and> (0 < internal_R C measuref s0' s' \<longrightarrow> internal_R C measuref s0' z = 0 \<longrightarrow> internal_R C R s0' z) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y))\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)); (s0'a, s0') \<in> S \<and> s0'a \<in> Ia \<and> s0' \<in> Ic \<longrightarrow> Fin C s0' = Fin A s0'a\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<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; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)); (s0'a, s0') \<in> S \<and> s0'a \<in> Ia \<and> s0' \<in> Ic \<longrightarrow> Fin C s0' = Fin A s0'a; (y, z) \<in> S \<and> y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)); (s0'a, s0') \<in> S \<and> s0'a \<in> Ia \<and> s0' \<in> Ic \<longrightarrow> Fin C s0' = Fin A s0'a; (y, z) \<in> S \<and> y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; (x, s') \<in> S \<and> x \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)); Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
using this:
A [> Ia
C [> Ic

goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x) \<and> (0 < measuref (Fin A s0'a) (Fin A x) \<longrightarrow> measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)); Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; \<forall>j. Step A j `` Ia \<subseteq> Ia; \<forall>j. Step C j `` Ic \<subseteq> Ic; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x); measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y)\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x); measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y); Step A a `` Ia \<subseteq> Ia; Step C a `` Ic \<subseteq> Ic\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x); measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y); Step C a `` Ic \<subseteq> Ic; y \<in> Ia\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal (1 subgoal):
 1. \<And>as s' s0' a s0'a x y z. \<lbrakk>s0' \<in> Ic; s0' \<in> Init C s0; (s', as) \<in> sub_big_steps C (internal_R C R) s0'; (s', z) \<in> Step C a; s0'a \<in> Init A s0; (s0'a, s0') \<in> S; s0'a \<in> Ia; (x, as) \<in> sub_big_steps A (internal_R A R) s0'a; (x, s') \<in> S; x \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; s' \<in> Ic; (x, y) \<in> Step A a; (y, z) \<in> S; Fin C s0' = Fin A s0'a; y \<in> Ia \<and> z \<in> Ic \<longrightarrow> Fin C z = Fin A y; Fin C s' = Fin A x; measuref (Fin A s0'a) (Fin A y) < measuref (Fin A s0'a) (Fin A x); measuref (Fin A s0'a) (Fin A y) = 0 \<longrightarrow> R (Fin A s0'a) (Fin A y); y \<in> Ia; z \<in> Ic\<rbrakk> \<Longrightarrow> measuref (Fin A s0'a) (Fin C z) < measuref (Fin A s0'a) (Fin A x) \<and> (measuref (Fin A s0'a) (Fin C z) = 0 \<longrightarrow> R (Fin A s0'a) (Fin C z)) proof (prove)
goal:
No subgoals!