theory Noninterference_Refinement

lemma ADT_C_if_big_step_R_terminate:
  "rel_terminate (ADT_C_if fp utf) s0
           (internal_R (ADT_C_if fp utf) big_step_R)
           {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and>
                hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in>
                 lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
           (\<lambda>s s'. internal_R (ADT_C_if fp utf) measuref_if s s')" apply (rule_tac S="lift_fst_rel (lift_snd_rel state_relation) O
                 (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})"
             and Ia="Collect invs_if" and A="ADT_A_if utf" in LI_rel_terminate) apply blast prefer 8 apply (simp add: internal_R_ADT_A_if) apply (rule ADT_A_if_big_step_R_terminate) apply (simp add: internal_R_ADT_A_if, simp add: ADT_A_if_def) apply (rule_tac x="s0" in bexI) apply (drule internal_R_tranclp) apply (simp add: Fin_Init_s0_ADT_C_if) apply clarsimp apply (rule big_step_R_tranclp_abs) apply force apply assumption apply simp apply (clarsimp simp: invs_if_full_invs_if extras_s0) apply (drule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]]) apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def) apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]]) apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def) apply (rule_tac x="((aa, bc), bd)" in bexI) apply (rule_tac b="((aa, bb), bd)" in relcompI) apply simp apply (force simp: ADT_H_if_def) apply simp apply (rule invs_if_inv_holds_ADT_A_if) apply (simp add: ADT_A_if_def invs_if_full_invs_if extras_s0) apply (rule ADT_C_if_inv_holds_transport) apply (rule ADT_C_if_Init_transport) apply (rule weaken_LI[OF LI_abs_to_c]) apply (clarsimp simp: invs_if_full_invs_if) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (9 subgoals):
 1. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} \<Longrightarrow> \<exists>s. s \<in> Collect invs_if \<and> (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (internal_R (ADT_A_if utf) big_step_R)\<^sup>+\<^sup>+ s0' s
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)})
 9. rel_terminate (ADT_A_if utf) s0 (internal_R (ADT_A_if utf) big_step_R) (Collect invs_if) (internal_R (ADT_A_if utf) measuref_if) proof (prove)
goal (8 subgoals):
 1. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (internal_R (ADT_A_if utf) big_step_R)\<^sup>+\<^sup>+ s0' s
 2. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)})
 8. rel_terminate (ADT_A_if utf) s0 (internal_R (ADT_A_if utf) big_step_R) (Collect invs_if) (internal_R (ADT_A_if utf) measuref_if) proof (prove)
goal (8 subgoals):
 1. rel_terminate (ADT_A_if utf) s0 (internal_R (ADT_A_if utf) big_step_R) (Collect invs_if) (internal_R (ADT_A_if utf) measuref_if)
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (internal_R (ADT_A_if utf) big_step_R)\<^sup>+\<^sup>+ s0' s
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. rel_terminate (ADT_A_if utf) s0 big_step_R (Collect invs_if) measuref_if
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (internal_R (ADT_A_if utf) big_step_R)\<^sup>+\<^sup>+ s0' s
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (7 subgoals):
 1. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (internal_R (ADT_A_if utf) big_step_R)\<^sup>+\<^sup>+ s0' s
 2. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (7 subgoals):
 1. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>{s0} \<inter> full_invs_if \<inter> Collect step_restrict. big_step_R\<^sup>+\<^sup>+ s0' s
 2. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>s s' s0''. \<lbrakk>s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}); big_step_R\<^sup>+\<^sup>+ (Fin (ADT_C_if fp utf) s0'') (Fin (ADT_C_if fp utf) s')\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>s s' s0''. \<lbrakk>s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}); big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) s')\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 ((ac, bf), bg)
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (10 subgoals):
 1. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> (((ac, bf), bg), ?s'46 ab bd be ac bf bg ad bh bi ae bj bk) \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr)
 2. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 (?s''46 ab bd be ac bf bg ad bh bi ae bj bk)
 3. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?s''46 ab bd be ac bf bg ad bh bi ae bj bk = Fin (ADT_C_if fp utf) (?s'46 ab bd be ac bf bg ad bh bi ae bj bk)
 4. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 5. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 6. ADT_A_if utf [> Collect invs_if
 7. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 8. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 9. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 10. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (9 subgoals):
 1. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 (?s''46 ab bd be ac bf bg ad bh bi ae bj bk)
 2. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> ?s''46 ab bd be ac bf bg ad bh bi ae bj bk = Fin (ADT_C_if fp utf) ((ae, bj), bk)
 3. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 4. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 5. ADT_A_if utf [> Collect invs_if
 6. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 7. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 9. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>ab bd be ac bf bg ad bh bi ae bj bk. \<lbrakk>((ab, bd), be) \<in> Init (ADT_C_if fp utf) s0; big_step_R\<^sup>+\<^sup>+ s0 (Fin (ADT_C_if fp utf) ((ae, bj), bk)); (((ac, bf), bg), (ad, bh), bi) \<in> lift_fst_rel (lift_snd_rel state_relation); (((ad, bh), bi), (ae, bj), bk) \<in> lift_fst_rel (lift_snd_rel rf_sr); ((ad, bh), bi) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> Fin (ADT_C_if fp utf) ((ae, bj), bk) = Fin (ADT_C_if fp utf) ((ae, bj), bk)
 2. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 3. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (7 subgoals):
 1. \<And>s s' s0''. \<lbrakk>(internal_R (ADT_C_if fp utf) big_step_R)\<^sup>+\<^sup>+ s0'' s'; s0'' \<in> Init (ADT_C_if fp utf) s0; (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})\<rbrakk> \<Longrightarrow> s0 \<in> {s0} \<inter> full_invs_if \<inter> Collect step_restrict
 2. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>s0''. s0'' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>s0''. s0'' \<in> lift_fst_rel (lift_snd_rel rf_sr) `` Init (valid_initial_state_noenabled.ADT_H_if utf) s0 \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', s0'') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>a b ba bb. \<lbrakk>((a, bb), ba) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', (a, b), ba) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> state_relation} O ({(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'})
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>a b ba bb. \<lbrakk>((a, bb), ba) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, bb), ba) \<in> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if utf) s0\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', (a, b), ba) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> state_relation} O ({(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'})
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init (ADT_A_if utf) s0. (s0', (aa, b), bd) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> state_relation} O ({(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'})
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (7 subgoals):
 1. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (((aa, bc), bd), (aa, b), bd) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> state_relation} O ({(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'})
 2. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (8 subgoals):
 1. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (((aa, bc), bd), (aa, bb), bd) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> state_relation}
 2. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (((aa, bb), bd), (aa, b), bd) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'}
 3. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0
 4. ADT_A_if utf [> Collect invs_if
 5. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 6. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 8. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (7 subgoals):
 1. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (((aa, bb), bd), (aa, b), bd) \<in> {(r, r'). snd r = snd r' \<and> fst (fst r) = fst (fst r') \<and> (internal_state_if r, internal_state_if r') \<in> rf_sr} \<inter> {(h, c). h \<in> full_invs_if'}
 2. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0
 3. ADT_A_if utf [> Collect invs_if
 4. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 5. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 7. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (6 subgoals):
 1. \<And>b bb aa bc bd. \<lbrakk>((aa, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0; (bc, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((aa, bc), bd) \<in> Init (ADT_A_if utf) s0
 2. ADT_A_if utf [> Collect invs_if
 3. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 4. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 6. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (5 subgoals):
 1. ADT_A_if utf [> Collect invs_if
 2. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 3. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 4. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 5. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (4 subgoals):
 1. Init (ADT_A_if utf) s0 \<subseteq> Collect invs_if
 2. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 3. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 4. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (3 subgoals):
 1. ADT_C_if fp utf [> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 2. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 3. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (2 subgoals):
 1. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 2. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (1 subgoal):
 1. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}) proof (prove)
goal (1 subgoal):
 1. Collect invs_if \<times> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} \<subseteq> full_invs_if \<times> UNIV proof (prove)
goal:
No subgoals!