[STATEMENT]
lemma Theorem_9_stable_Xd1_Xd2:
  shows "Theorem_9.stable_on UNIV {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.stable_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
proof %invisible (rule Theorem_9.stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
note image_cong_simp [cong del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N =simp=> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
note INF_cong_simp [cong]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B =simp=> ?C x = ?D x\<rbrakk> \<Longrightarrow> Inf (?C ` ?A) = Inf (?D ` ?B)

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
note SUP_cong_simp [cong]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B =simp=> ?C x = ?D x\<rbrakk> \<Longrightarrow> Sup (?C ` ?A) = Sup (?D ` ?B)

goal (2 subgoals):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}
 2. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
show "Theorem_9.individually_rational_on UNIV {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
by (rule Theorem_9.individually_rational_onI)
       (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.CH_def insert_commute)
[PROOF STATE]
proof (state)
this:
Theorem_9.individually_rational_on UNIV {X3.Xd1, X3.Xd2}

goal (1 subgoal):
 1. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
show "Theorem_9.stable_no_blocking_on UNIV {Xd1, Xd2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}
[PROOF STEP]
apply (rule Theorem_9.stable_no_blocking_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1, X3.Xd2} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1, X3.Xd2}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1, X3.Xd2} \<union> X'')\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (case_tac h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1, X3.Xd2} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1, X3.Xd2}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1, X3.Xd2} \<union> X''); h = H\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac X=X'' in X3_pow)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h h ({X3.Xd1, X3.Xd2} \<union> X''); X'' \<noteq> CX3h h {X3.Xd1, X3.Xd2}; X'' \<subseteq> Theorem_9.CD_on UNIV ({X3.Xd1, X3.Xd2} \<union> X''); h = H; X'' \<in> set ` set (subseqs [X3.Xd1, X3.Xd1', X3.Xd2])\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h X''. \<lbrakk>X'' = CX3h H (insert X3.Xd1 (insert X3.Xd2 X'')); X'' \<noteq> {X3.Xd1, X3.Xd2}; X'' \<subseteq> Theorem_9.CD_on UNIV (insert X3.Xd1 (insert X3.Xd2 X'')); h = H; X'' = {X3.Xd1, X3.Xd1', X3.Xd2} \<or> X'' = {X3.Xd1, X3.Xd1'} \<or> X'' = {X3.Xd1} \<or> X'' = {X3.Xd1', X3.Xd2} \<or> X'' = {X3.Xd1'} \<or> X'' = {X3.Xd2} \<or> X'' = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1', X3.Xd2}; {X3.Xd1, X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1', X3.Xd2}; \<not> False; X3.Xd1' \<noteq> X3.Xd1; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd2
 2. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1'} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1'}; {X3.Xd1, X3.Xd1'} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1'}; \<not> False; X3.Xd1' \<noteq> X3.Xd1; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd2
 3. \<And>h X'' x. \<lbrakk>{X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1', X3.Xd2}; {X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1', X3.Xd2}; \<not> False; X3.Xd1' \<noteq> X3.Xd1; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd2
 4. \<And>h X'' x. \<lbrakk>{X3.Xd1'} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1'}; {X3.Xd1'} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1'}; \<not> False; X3.Xd1' \<noteq> X3.Xd1; X3.Xd1' \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1' = X3.Xd2
 5. \<And>h X'' x. \<lbrakk>{X3.Xd1', X3.Xd2} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1', X3.Xd2}; {X3.Xd1', X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1', X3.Xd2}; \<not> False; X3.Xd1 \<noteq> X3.Xd1'; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd2
 6. \<And>h X'' x. \<lbrakk>{X3.Xd1'} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1'}; {X3.Xd1'} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1'}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd1'
 7. \<And>h X'' x. \<lbrakk>{X3.Xd2} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd2}; {X3.Xd2} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd2}; \<not> False; X3.Xd1 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd1 = X3.Xd2
 8. \<And>h X'' x. \<lbrakk>{} = CX3h H {X3.Xd1, X3.Xd2}; {} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2}; \<not> False\<rbrakk> \<Longrightarrow> X3.Xd1 \<in> {}
 9. \<And>h X'' x. \<lbrakk>{X3.Xd1, X3.Xd1'} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1'}; {X3.Xd1, X3.Xd1'} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1, X3.Xd1'}; \<not> False; X3.Xd2 \<noteq> X3.Xd1; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1'
 10. \<And>h X'' x. \<lbrakk>{X3.Xd1} = CX3h H {X3.Xd1, X3.Xd2, X3.Xd1}; {X3.Xd1} \<subseteq> Theorem_9.CD_on UNIV {X3.Xd1, X3.Xd2, X3.Xd1}; \<not> False; X3.Xd2 \<notin> {}\<rbrakk> \<Longrightarrow> X3.Xd2 = X3.Xd1
A total of 12 subgoals...
[PROOF STEP]
apply (simp_all add: D2_UNION Theorem_9.CD_on_def Theorem_9.maxR_def linord_of_list_linord_of_listP insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Theorem_9.stable_no_blocking_on UNIV {X3.Xd1, X3.Xd2}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CX3h_not_lad:
  shows "\<not>lad (CX3h h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lad (CX3h h)
[PROOF STEP]
unfolding %invisible lad_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>B\<subseteq>UNIV. \<forall>C\<subseteq>B. card (CX3h h C) \<le> card (CX3h h B))
[PROOF STEP]
apply (cases h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = H \<Longrightarrow> \<not> (\<forall>B\<subseteq>UNIV. \<forall>C\<subseteq>B. card (CX3h h C) \<le> card (CX3h h B))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = H \<Longrightarrow> \<exists>B C. C \<subseteq> B \<and> \<not> card (CX3h H C) \<le> card (CX3h H B)
[PROOF STEP]
apply (rule exI[where x="{Xd1, Xd1', Xd2}"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = H \<Longrightarrow> \<exists>C\<subseteq>{X3.Xd1, X3.Xd1', X3.Xd2}. \<not> card (CX3h H C) \<le> card (CX3h H {X3.Xd1, X3.Xd1', X3.Xd2})
[PROOF STEP]
apply (rule exI[where x="{Xd1, Xd2}"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = H \<Longrightarrow> {X3.Xd1, X3.Xd2} \<subseteq> {X3.Xd1, X3.Xd1', X3.Xd2} \<and> \<not> card (CX3h H {X3.Xd1, X3.Xd2}) \<le> card (CX3h H {X3.Xd1, X3.Xd1', X3.Xd2})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cop_F_HM_cop_F:
  shows "cop_F_HM ds XD_XH = (- RH (snd XD_XH), cop_F ds (snd XD_XH))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cop_F_HM ds XD_XH = (- Rf CH (snd XD_XH), cop_F ds (snd XD_XH))
[PROOF STEP]
unfolding cop_F_HM_def cop_F_def split_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- Rf CH (snd XD_XH), snd XD_XH \<union> CD_on ds (- Rf CH (snd XD_XH))) = (- Rf CH (snd XD_XH), snd XD_XH \<union> CD_on ds (- Rf CH (snd XD_XH)))
[PROOF STEP]
by simp


[STATEMENT]
lemma cop_F_increasing:
  shows "x \<le> cop_F ds x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<subseteq> cop_F ds x
[PROOF STEP]
unfolding %invisible cop_F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<subseteq> x \<union> CD_on ds (- Rf CH x)
[PROOF STEP]
by simp


[STATEMENT]
lemma cop_F_cases:
  assumes "x \<in> cop_F ds fp"
  obtains (fp) "x \<in> fp" | (CD_on) "x \<in> CD_on ds (-RH fp) - fp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fp \<Longrightarrow> thesis; x \<in> CD_on ds (- Rf CH fp) - fp \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> cop_F ds fp

goal (1 subgoal):
 1. \<lbrakk>x \<in> fp \<Longrightarrow> thesis; x \<in> CD_on ds (- Rf CH fp) - fp \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding cop_F_def
[PROOF STATE]
proof (prove)
using this:
x \<in> fp \<union> CD_on ds (- Rf CH fp)

goal (1 subgoal):
 1. \<lbrakk>x \<in> fp \<Longrightarrow> thesis; x \<in> CD_on ds (- Rf CH fp) - fp \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma CH_cop_F_cases:
  assumes "x \<in> CH (cop_F ds fp)"
  obtains (CH) "x \<in> CH fp" | (RH_fp) "x \<in> RH fp" | (CD_on) "x \<in> CD_on ds (-RH fp) - fp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> CH fp \<Longrightarrow> thesis; x \<in> Rf CH fp \<Longrightarrow> thesis; x \<in> CD_on ds (- Rf CH fp) - fp \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms CH_range cop_F_def
[PROOF STATE]
proof (prove)
using this:
x \<in> CH (cop_F ds fp)
CH ?A \<subseteq> ?A
cop_F ?ds ?XH = ?XH \<union> CD_on ?ds (- Rf CH ?XH)

goal (1 subgoal):
 1. \<lbrakk>x \<in> CH fp \<Longrightarrow> thesis; x \<in> Rf CH fp \<Longrightarrow> thesis; x \<in> CD_on ds (- Rf CH fp) - fp \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma fp_cop_F_induct[case_names base step]:
  assumes "P {}"
  assumes "\<And>fp. P fp \<Longrightarrow> P (cop_F ds fp)"
  shows "P (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (fp_cop_F ds)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
P {}
P ?fp \<Longrightarrow> P (cop_F ds ?fp)

goal (1 subgoal):
 1. P (fp_cop_F ds)
[PROOF STEP]
by (induct rule: COP.fixp_above_induct[where a="{}", folded fp_cop_F_def])
   (fastforce intro: admissible_chfin)+


[STATEMENT]
lemma validI[case_names base step]:
  assumes "Q ds {}"
  assumes "\<And>fp. \<lbrakk>P ds fp; Q ds fp\<rbrakk> \<Longrightarrow> Q ds (cop_F ds fp)"
  shows "valid ds P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid ds P Q
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
Q ds {}
\<lbrakk>P ds ?fp; Q ds ?fp\<rbrakk> \<Longrightarrow> Q ds (cop_F ds ?fp)

goal (1 subgoal):
 1. valid ds P Q
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
Q ds {}
\<lbrakk>P ds ?fp; Q ds ?fp\<rbrakk> \<Longrightarrow> Q ds (cop_F ds ?fp)

goal (1 subgoal):
 1. Q ds {} \<and> (\<forall>fp. P ds fp \<and> Q ds fp \<longrightarrow> Q ds (cop_F ds fp))
[PROOF STEP]
by blast


[STATEMENT]
lemma invariant_cop_FD:
  assumes "invariant ds P"
  assumes "P ds fp"
  shows "P ds (cop_F ds fp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ds (cop_F ds fp)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
invariant ds P
P ds fp

goal (1 subgoal):
 1. P ds (cop_F ds fp)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
P ds {} \<and> (\<forall>fp. True \<and> P ds fp \<longrightarrow> P ds (cop_F ds fp))
P ds fp

goal (1 subgoal):
 1. P ds (cop_F ds fp)
[PROOF STEP]
by blast


[STATEMENT]
lemma invariantD:
  assumes "invariant ds P"
  shows "P ds (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ds (fp_cop_F ds)
[PROOF STEP]
using %invisible assms fp_cop_F_induct
[PROOF STATE]
proof (prove)
using this:
invariant ds P
\<lbrakk>?P {}; \<And>fp. ?P fp \<Longrightarrow> ?P (cop_F ?ds fp)\<rbrakk> \<Longrightarrow> ?P (fp_cop_F ?ds)

goal (1 subgoal):
 1. P ds (fp_cop_F ds)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
P ds {} \<and> (\<forall>fp. True \<and> P ds fp \<longrightarrow> P ds (cop_F ds fp))
\<lbrakk>?P {}; \<And>fp. ?P fp \<Longrightarrow> ?P (cop_F ?ds fp)\<rbrakk> \<Longrightarrow> ?P (fp_cop_F ?ds)

goal (1 subgoal):
 1. P ds (fp_cop_F ds)
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_pre:
  assumes "valid ds P' Q"
  assumes "\<And>fp. P ds fp \<Longrightarrow> P' ds fp"
  shows "valid ds P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid ds P Q
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
valid ds P' Q
P ds ?fp \<Longrightarrow> P' ds ?fp

goal (1 subgoal):
 1. valid ds P Q
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
Q ds {} \<and> (\<forall>fp. P' ds fp \<and> Q ds fp \<longrightarrow> Q ds (cop_F ds fp))
P ds ?fp \<Longrightarrow> P' ds ?fp

goal (1 subgoal):
 1. Q ds {} \<and> (\<forall>fp. P ds fp \<and> Q ds fp \<longrightarrow> Q ds (cop_F ds fp))
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_invariant:
  assumes "valid ds P Q"
  assumes "invariant ds P"
  shows "invariant ds (\<lambda> ds fp. P ds fp \<and> Q ds fp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant ds (\<lambda>ds fp. P ds fp \<and> Q ds fp)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
valid ds P Q
invariant ds P

goal (1 subgoal):
 1. invariant ds (\<lambda>ds fp. P ds fp \<and> Q ds fp)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
Q ds {} \<and> (\<forall>fp. P ds fp \<and> Q ds fp \<longrightarrow> Q ds (cop_F ds fp))
P ds {} \<and> (\<forall>fp. True \<and> P ds fp \<longrightarrow> P ds (cop_F ds fp))

goal (1 subgoal):
 1. (P ds {} \<and> Q ds {}) \<and> (\<forall>fp. True \<and> P ds fp \<and> Q ds fp \<longrightarrow> P ds (cop_F ds fp) \<and> Q ds (cop_F ds fp))
[PROOF STEP]
by blast


[STATEMENT]
lemma valid_conj:
  assumes "valid ds (\<lambda>ds fp. R ds fp \<and> P ds fp \<and> Q ds fp) P"
  assumes "valid ds (\<lambda>ds fp. R ds fp \<and> P ds fp \<and> Q ds fp) Q"
  shows "valid ds R (\<lambda> ds fp. P ds fp \<and> Q ds fp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid ds R (\<lambda>ds fp. P ds fp \<and> Q ds fp)
[PROOF STEP]
using %invisible assms
[PROOF STATE]
proof (prove)
using this:
valid ds (\<lambda>ds fp. R ds fp \<and> P ds fp \<and> Q ds fp) P
valid ds (\<lambda>ds fp. R ds fp \<and> P ds fp \<and> Q ds fp) Q

goal (1 subgoal):
 1. valid ds R (\<lambda>ds fp. P ds fp \<and> Q ds fp)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
P ds {} \<and> (\<forall>fp. (R ds fp \<and> P ds fp \<and> Q ds fp) \<and> P ds fp \<longrightarrow> P ds (cop_F ds fp))
Q ds {} \<and> (\<forall>fp. (R ds fp \<and> P ds fp \<and> Q ds fp) \<and> Q ds fp \<longrightarrow> Q ds (cop_F ds fp))

goal (1 subgoal):
 1. (P ds {} \<and> Q ds {}) \<and> (\<forall>fp. R ds fp \<and> P ds fp \<and> Q ds fp \<longrightarrow> P ds (cop_F ds fp) \<and> Q ds (cop_F ds fp))
[PROOF STEP]
by blast


[STATEMENT]
lemma lfp_F2_o_F1_fp_cop_F:
  shows "lfp (F2 ds \<circ> F1) = fp_cop_F ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfp (F2 ds \<circ> F1) = fp_cop_F ds
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lfp (F2 ds \<circ> F1) \<subseteq> fp_cop_F ds
 2. fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
have "(F2 ds \<circ> F1) (fp_cop_F ds) \<subseteq> cop_F ds (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F2 ds \<circ> F1) (fp_cop_F ds) \<subseteq> cop_F ds (fp_cop_F ds)
[PROOF STEP]
by (clarsimp simp: F2_def F1_def cop_F_def)
[PROOF STATE]
proof (state)
this:
(F2 ds \<circ> F1) (fp_cop_F ds) \<subseteq> cop_F ds (fp_cop_F ds)

goal (2 subgoals):
 1. lfp (F2 ds \<circ> F1) \<subseteq> fp_cop_F ds
 2. fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(F2 ds \<circ> F1) (fp_cop_F ds) \<subseteq> cop_F ds (fp_cop_F ds)
[PROOF STEP]
show "lfp (F2 ds \<circ> F1) \<subseteq> fp_cop_F ds"
[PROOF STATE]
proof (prove)
using this:
(F2 ds \<circ> F1) (fp_cop_F ds) \<subseteq> cop_F ds (fp_cop_F ds)

goal (1 subgoal):
 1. lfp (F2 ds \<circ> F1) \<subseteq> fp_cop_F ds
[PROOF STEP]
by (simp add: lfp_lowerbound fp_cop_F_unfold[symmetric])
[PROOF STATE]
proof (state)
this:
lfp (F2 ds \<circ> F1) \<subseteq> fp_cop_F ds

goal (1 subgoal):
 1. fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
show "fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
proof(induct rule: fp_cop_F_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> lfp (F2 ds \<circ> F1)
 2. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. {} \<subseteq> lfp (F2 ds \<circ> F1)
 2. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
case (step fp)
[PROOF STATE]
proof (state)
this:
fp \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
note IH = \<open>fp \<subseteq> lfp (F2 ds \<circ> F1)\<close>
[PROOF STATE]
proof (state)
this:
fp \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
have "CD_on ds (- RH fp) \<subseteq> lfp (F2 ds \<circ> F1)"
[PROOF STATE]
proof (prove)
using this:
fp \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
apply (subst lfp_unfold[OF F2_o_F1_mono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> CD_on ds (- Rf CH fp) \<subseteq> (F2 ds \<circ> F1) (lfp (F2 ds \<circ> F1))
[PROOF STEP]
by (smt (verit, ccfv_SIG) Compl_iff Contracts.F1_def Contracts.F2_def Contracts_axioms DiffD2
          F2_o_F1_mono comp_eq_dest_lhs in_mono monoD subsetI)
[PROOF STATE]
proof (state)
this:
CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. \<And>fp. fp \<subseteq> lfp (F2 ds \<circ> F1) \<Longrightarrow> cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
fp \<subseteq> lfp (F2 ds \<circ> F1)
CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fp \<subseteq> lfp (F2 ds \<circ> F1)
CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
unfolding cop_F_def
[PROOF STATE]
proof (prove)
using this:
fp \<subseteq> lfp (F2 ds \<circ> F1)
CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)

goal (1 subgoal):
 1. fp \<union> CD_on ds (- Rf CH fp) \<subseteq> lfp (F2 ds \<circ> F1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cop_F ds fp \<subseteq> lfp (F2 ds \<circ> F1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fp_cop_F ds \<subseteq> lfp (F2 ds \<circ> F1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Theorem_15:
  shows "gfp_F ds = (- RH (fp_cop_F ds), fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gfp_F ds = (- Rf CH (fp_cop_F ds), fp_cop_F ds)
[PROOF STEP]
using lfp_F2_o_F1_fp_cop_F
[PROOF STATE]
proof (prove)
using this:
lfp (F2 ?ds \<circ> F1) = fp_cop_F ?ds

goal (1 subgoal):
 1. gfp_F ds = (- Rf CH (fp_cop_F ds), fp_cop_F ds)
[PROOF STEP]
unfolding gfp_F_lfp_F F1_def
[PROOF STATE]
proof (prove)
using this:
lfp (F2 ?ds \<circ> (\<lambda>X'. - Rf CH X')) = fp_cop_F ?ds

goal (1 subgoal):
 1. (- Rf CH (lfp (F2 ds \<circ> (\<lambda>X'. - Rf CH X'))), lfp (F2 ds \<circ> (\<lambda>X'. - Rf CH X'))) = (- Rf CH (fp_cop_F ds), fp_cop_F ds)
[PROOF STEP]
by simp


[STATEMENT]
theorem Theorem_15_match:
  shows "match (gfp_F ds) = CH (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (gfp_F ds) = cop ds
[PROOF STEP]
using Theorem_15
[PROOF STATE]
proof (prove)
using this:
gfp_F ?ds = (- Rf CH (fp_cop_F ?ds), fp_cop_F ?ds)

goal (1 subgoal):
 1. match (gfp_F ds) = cop ds
[PROOF STEP]
by (fastforce dest: subsetD[OF CH_range])


[STATEMENT]
lemma P920_example_fp_cop_F_value:
  shows "P920_example_CH (P920_example_fp_cop_F UNIV) = {(D1, H1), (D2, H2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P920_example_CH (P920_example_fp_cop_F UNIV) = {(D1, H1), (D2, H2)}
[PROOF STEP]
by eval


[STATEMENT]
lemma %invisible CH_Ch_singular:
  assumes "(UNIV::'h set) = {h}"
  shows "CH A = Ch h A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH A = Ch h A
[PROOF STEP]
unfolding CH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>h. Ch h A) = Ch h A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
UNIV = {h}

goal (1 subgoal):
 1. (\<Union>h. Ch h A) = Ch h A
[PROOF STEP]
by auto


[STATEMENT]
lemma cop_F_range_inv:
  shows "invariant ds cop_F_range_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant ds cop_F_range_inv
[PROOF STEP]
unfolding valid_def cop_F_range_inv_def cop_F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{}. x \<in> Field (Pd (Xd x)) \<and> Xd x \<in> ds) \<and> (\<forall>fp. True \<and> (\<forall>x\<in>fp. x \<in> Field (Pd (Xd x)) \<and> Xd x \<in> ds) \<longrightarrow> (\<forall>x\<in>fp \<union> CD_on ds (- Rf CH fp). x \<in> Field (Pd (Xd x)) \<and> Xd x \<in> ds))
[PROOF STEP]
by (fastforce simp: mem_CD_on_Cd dest: Cd_range')


[STATEMENT]
lemma cop_F_closed_inv:
  shows "invariant ds cop_F_closed_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant ds cop_F_closed_inv
[PROOF STEP]
unfolding valid_def cop_F_closed_inv_def cop_F_def above_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{}. {b. (x, b) \<in> Pd (Xd x)} \<subseteq> {}) \<and> (\<forall>fp. True \<and> (\<forall>x\<in>fp. {b. (x, b) \<in> Pd (Xd x)} \<subseteq> fp) \<longrightarrow> (\<forall>x\<in>fp \<union> CD_on ds (- Rf CH fp). {b. (x, b) \<in> Pd (Xd x)} \<subseteq> fp \<union> CD_on ds (- Rf CH fp)))
[PROOF STEP]
by (clarsimp simp: subset_iff) (metis Cd_preferred ComplI Un_upper1 mem_CD_on_Cd subsetCE)


[STATEMENT]
lemma cop_F_RH:
  assumes "d \<in> ds"
  assumes "x \<in> Field (Pd d)"
  assumes "aboveS (Pd d) x \<subseteq> RH fp"
  shows "x \<in> cop_F ds fp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> cop_F ds fp
[PROOF STEP]
using %invisible assms Pd_linear
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
x \<in> Field (Pd d)
aboveS (Pd d) x \<subseteq> Rf CH fp
\<forall>d. Linear_order (Pd d)

goal (1 subgoal):
 1. x \<in> cop_F ds fp
[PROOF STEP]
unfolding cop_F_def
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
x \<in> Field (Pd d)
aboveS (Pd d) x \<subseteq> Rf CH fp
\<forall>d. Linear_order (Pd d)

goal (1 subgoal):
 1. x \<in> fp \<union> CD_on ds (- Rf CH fp)
[PROOF STEP]
by (clarsimp simp: mem_CD_on_Cd Cd_greatest greatest_def aboveS_def order_on_defs total_on_def subset_iff)
   (metis Compl_Diff_eq Compl_iff Diff_iff IntE Pd_Xd refl_onD)


[STATEMENT]
lemma fp_cop_F_all:
  assumes "d \<in> ds"
  assumes "d \<notin> Xd ` CH (fp_cop_F ds)"
  shows "Field (Pd d) \<subseteq> fp_cop_F ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Field (Pd d) \<subseteq> fp_cop_F ds
[PROOF STEP]
proof %invisible (rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Field (Pd d) \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Field (Pd d) \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
assume "x \<in> Field (Pd d)"
[PROOF STATE]
proof (state)
this:
x \<in> Field (Pd d)

goal (1 subgoal):
 1. \<And>x. x \<in> Field (Pd d) \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
from spec[OF Pd_linear] this finite[of "Pd d"]
[PROOF STATE]
proof (chain)
picking this:
Linear_order (Pd ?x)
x \<in> Field (Pd d)
finite (Pd d)
[PROOF STEP]
show "x \<in> fp_cop_F ds"
[PROOF STATE]
proof (prove)
using this:
Linear_order (Pd ?x)
x \<in> Field (Pd d)
finite (Pd d)

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
proof(induct rule: finite_Linear_order_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> Field (Pd d); \<And>y. y \<in> aboveS (Pd d) x \<Longrightarrow> y \<in> fp_cop_F ds\<rbrakk> \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
case (step x)
[PROOF STATE]
proof (state)
this:
x \<in> Field (Pd d)
?y \<in> aboveS (Pd d) x \<Longrightarrow> ?y \<in> fp_cop_F ds

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> Field (Pd d); \<And>y. y \<in> aboveS (Pd d) x \<Longrightarrow> y \<in> fp_cop_F ds\<rbrakk> \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
with assms Pd_range Pd_Xd cop_F_RH[of d ds _ "fp_cop_F ds", unfolded fp_cop_F_unfold[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
d \<in> ds
d \<notin> Xd ` cop ds
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
\<lbrakk>d \<in> ds; ?x \<in> Field (Pd d); aboveS (Pd d) ?x \<subseteq> Rf CH (fp_cop_F ds)\<rbrakk> \<Longrightarrow> ?x \<in> fp_cop_F ds
x \<in> Field (Pd d)
?y \<in> aboveS (Pd d) x \<Longrightarrow> ?y \<in> fp_cop_F ds
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
d \<notin> Xd ` cop ds
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
\<lbrakk>d \<in> ds; ?x \<in> Field (Pd d); aboveS (Pd d) ?x \<subseteq> Rf CH (fp_cop_F ds)\<rbrakk> \<Longrightarrow> ?x \<in> fp_cop_F ds
x \<in> Field (Pd d)
?y \<in> aboveS (Pd d) x \<Longrightarrow> ?y \<in> fp_cop_F ds

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
unfolding aboveS_def
[PROOF STATE]
proof (prove)
using this:
d \<in> ds
d \<notin> Xd ` cop ds
\<forall>d. Field (Pd d) \<subseteq> {x. Xd x = d}
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
\<lbrakk>d \<in> ds; ?x \<in> Field (Pd d); {b. b \<noteq> ?x \<and> (?x, b) \<in> Pd d} \<subseteq> Rf CH (fp_cop_F ds)\<rbrakk> \<Longrightarrow> ?x \<in> fp_cop_F ds
x \<in> Field (Pd d)
?y \<in> {b. b \<noteq> x \<and> (x, b) \<in> Pd d} \<Longrightarrow> ?y \<in> fp_cop_F ds

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
by (fastforce iff: image_iff)
[PROOF STATE]
proof (state)
this:
x \<in> fp_cop_F ds

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> fp_cop_F ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fp_cop_F_preferred:
  assumes "y \<in> CD_on ds (CH (fp_cop_F ds) \<union> X'')"
  assumes "x \<in> CH (fp_cop_F ds)"
  assumes "Xd x = Xd y"
  shows "(x, y) \<in> Pd (Xd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> Pd (Xd x)
[PROOF STEP]
using %invisible assms fp_cop_F_range_inv'[OF CH_range'[OF assms(2)]] Pd_Xd Pd_linear
[PROOF STATE]
proof (prove)
using this:
y \<in> CD_on ds (cop ds \<union> X'')
x \<in> cop ds
Xd x = Xd y
x \<in> Field (Pd (Xd x)) \<and> Xd x \<in> ds
(?x, ?y) \<in> Pd ?d \<Longrightarrow> Xd ?x = ?d \<and> Xd ?y = ?d
\<forall>d. Linear_order (Pd d)

goal (1 subgoal):
 1. (x, y) \<in> Pd (Xd x)
[PROOF STEP]
by (clarsimp simp: CD_on_def Cd_greatest greatest_def) (metis Int_iff Un_iff subset_refl underS_incl_iff)


[STATEMENT]
lemma X''_closed:
  assumes "X'' \<subseteq> CD_on ds (CH (fp_cop_F ds) \<union> X'')"
  shows "X'' \<subseteq> fp_cop_F ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X'' \<subseteq> fp_cop_F ds
[PROOF STEP]
proof(rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
assume "x \<in> X''"
[PROOF STATE]
proof (state)
this:
x \<in> X''

goal (1 subgoal):
 1. \<And>x. x \<in> X'' \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
show "x \<in> fp_cop_F ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
proof(cases "Xd x \<in> Xd ` CH (fp_cop_F ds)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Xd x \<in> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
 2. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Xd x \<in> Xd ` cop ds

goal (2 subgoals):
 1. Xd x \<in> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
 2. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Xd x \<in> Xd ` cop ds
[PROOF STEP]
obtain y where "Xd y = Xd x" and "y \<in> CH (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
using this:
Xd x \<in> Xd ` cop ds

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>Xd y = Xd x; y \<in> cop ds\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
Xd y = Xd x
y \<in> cop ds

goal (2 subgoals):
 1. Xd x \<in> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
 2. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
with assms \<open>x \<in> X''\<close>
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd y = Xd x
y \<in> cop ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd y = Xd x
y \<in> cop ds

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
using CH_range fp_cop_F_closed_inv' fp_cop_F_preferred
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd y = Xd x
y \<in> cop ds
CH ?A \<subseteq> ?A
\<lbrakk>?x \<in> fp_cop_F ?ds; ?c \<in> above (Pd (Xd ?x)) ?x\<rbrakk> \<Longrightarrow> ?c \<in> fp_cop_F ?ds
\<lbrakk>?y \<in> CD_on ?ds (cop ?ds \<union> ?X''); ?x \<in> cop ?ds; Xd ?x = Xd ?y\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> Pd (Xd ?x)

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
unfolding above_def
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd y = Xd x
y \<in> cop ds
CH ?A \<subseteq> ?A
\<lbrakk>?x \<in> fp_cop_F ?ds; ?c \<in> {b. (?x, b) \<in> Pd (Xd ?x)}\<rbrakk> \<Longrightarrow> ?c \<in> fp_cop_F ?ds
\<lbrakk>?y \<in> CD_on ?ds (cop ?ds \<union> ?X''); ?x \<in> cop ?ds; Xd ?x = Xd ?y\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> Pd (Xd ?x)

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> fp_cop_F ds

goal (1 subgoal):
 1. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Xd x \<notin> Xd ` cop ds

goal (1 subgoal):
 1. Xd x \<notin> Xd ` cop ds \<Longrightarrow> x \<in> fp_cop_F ds
[PROOF STEP]
with assms \<open>x \<in> X''\<close>
[PROOF STATE]
proof (chain)
picking this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd x \<notin> Xd ` cop ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X'' \<subseteq> CD_on ds (cop ds \<union> X'')
x \<in> X''
Xd x \<notin> Xd ` cop ds

goal (1 subgoal):
 1. x \<in> fp_cop_F ds
[PROOF STEP]
by (meson Cd_range' IntD2 fp_cop_F_all mem_CD_on_Cd rev_subsetD)
[PROOF STATE]
proof (state)
this:
x \<in> fp_cop_F ds

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> fp_cop_F ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Theorem_16:
  assumes h: "(UNIV::'c set) = {h}"
  shows "stable_on ds (cop ds)" (is "stable_on ds ?fp")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_on ds (cop ds)
[PROOF STEP]
proof(rule stable_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. individually_rational_on ds (cop ds)
 2. stable_no_blocking_on ds (cop ds)
[PROOF STEP]
show "individually_rational_on ds ?fp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. individually_rational_on ds (cop ds)
[PROOF STEP]
proof(rule individually_rational_onI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. CD_on ds (cop ds) = cop ds
 2. CH (cop ds) = cop ds
[PROOF STEP]
from h
[PROOF STATE]
proof (chain)
picking this:
UNIV = {h}
[PROOF STEP]
have "allocation ?fp"
[PROOF STATE]
proof (prove)
using this:
UNIV = {h}

goal (1 subgoal):
 1. inj_on Xd (cop ds)
[PROOF STEP]
by (simp add: Ch_singular CH_Ch_singular)
[PROOF STATE]
proof (state)
this:
inj_on Xd (cop ds)

goal (2 subgoals):
 1. CD_on ds (cop ds) = cop ds
 2. CH (cop ds) = cop ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on Xd (cop ds)
[PROOF STEP]
show "CD_on ds ?fp = ?fp"
[PROOF STATE]
proof (prove)
using this:
inj_on Xd (cop ds)

goal (1 subgoal):
 1. CD_on ds (cop ds) = cop ds
[PROOF STEP]
by (rule CD_on_closed) (blast dest: CH_range' fp_cop_F_range_inv')
[PROOF STATE]
proof (state)
this:
CD_on ds (cop ds) = cop ds

goal (1 subgoal):
 1. CH (cop ds) = cop ds
[PROOF STEP]
show "CH (CH (fp_cop_F ds)) = CH (fp_cop_F ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CH (cop ds) = cop ds
[PROOF STEP]
by (simp add: CH_irc_idem)
[PROOF STATE]
proof (state)
this:
CH (cop ds) = cop ds

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
individually_rational_on ds (cop ds)

goal (1 subgoal):
 1. stable_no_blocking_on ds (cop ds)
[PROOF STEP]
show "stable_no_blocking_on ds ?fp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_no_blocking_on ds (cop ds)
[PROOF STEP]
by (rule cop_stable_no_blocking_on)
[PROOF STATE]
proof (state)
this:
stable_no_blocking_on ds (cop ds)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ffact_add_nat:
  shows "ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "ffact k (n + m) = fact k * ((n + m) choose k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ffact k (n + m) = fact k * (n + m choose k)
[PROOF STEP]
by (simp only: ffact_eq_fact_mult_binomial)
[PROOF STATE]
proof (state)
this:
ffact k (n + m) = fact k * (n + m choose k)

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ffact k (n + m) = fact k * (n + m choose k)

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "\<dots> = fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact k * (n + m choose k) = fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i)))
[PROOF STEP]
by (simp only: vandermonde)
[PROOF STATE]
proof (state)
this:
fact k * (n + m choose k) = fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fact k * (n + m choose k) = fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i)))
[PROOF STEP]
by (simp add: sum_distrib_left field_simps)
[PROOF STATE]
proof (state)
this:
fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fact k * (\<Sum>i\<le>k. (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. (fact i * fact (k - i) * (k choose i)) * (n choose i) * (m choose (k - i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i)))
[PROOF STEP]
by (simp add: binomial_fact_lemma)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. fact k * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i)))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. fact i * fact (k - i) * (k choose i) * (n choose i) * (m choose (k - i))) = (\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i))))

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
have "\<dots> = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i)))) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
by (simp only: ffact_eq_fact_mult_binomial)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>k. (k choose i) * (fact i * (n choose i)) * (fact (k - i) * (m choose (k - i)))) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)

goal (1 subgoal):
 1. ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ffact k (n + m) = (\<Sum>i\<le>k. (k choose i) * ffact i n * ffact (k - i) m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) operational_correspondence_modulo_all_relation:
  shows "operational_complete {(T1, T2). True}"
    and "weakly_operational_sound {(T1, T2). True}"
    and "operational_sound {(T1, T2). True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. operational_complete (_Collect (T1, T2) True) &&& weakly_operational_sound (_Collect (T1, T2) True) &&& operational_sound (_Collect (T1, T2) True)
[PROOF STEP]
using steps_refl[where Cal="Source"] steps_refl[where Cal="Target"]
[PROOF STATE]
proof (prove)
using this:
?P \<longmapsto>Source* ?P
?P \<longmapsto>Target* ?P

goal (1 subgoal):
 1. operational_complete (_Collect (T1, T2) True) &&& weakly_operational_sound (_Collect (T1, T2) True) &&& operational_sound (_Collect (T1, T2) True)
[PROOF STEP]
by blast+


[STATEMENT]
lemma all_relation_is_weak_reduction_bisimulation:
  fixes Cal :: "'a processCalculus"
  shows "weak_reduction_bisimulation {(a, b). True} Cal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_reduction_bisimulation (_Collect (a, b) True) Cal
[PROOF STEP]
using steps_refl[where Cal="Cal"]
[PROOF STATE]
proof (prove)
using this:
?P \<longmapsto>Cal* ?P

goal (1 subgoal):
 1. weak_reduction_bisimulation (_Collect (a, b) True) Cal
[PROOF STEP]
by blast


[STATEMENT]
lemma (in encoding) operational_correspondence_modulo_some_target_relation:
  shows "\<exists>TRel. weakly_operational_corresponding TRel"
    and "\<exists>TRel. operational_corresponding TRel"
    and "\<exists>TRel. weakly_operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target"
    and "\<exists>TRel. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>TRel. weakly_operational_corresponding TRel &&& \<exists>TRel. operational_corresponding TRel) &&& \<exists>TRel. weakly_operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target &&& \<exists>TRel. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
using operational_correspondence_modulo_all_relation
            all_relation_is_weak_reduction_bisimulation[where Cal="Target"]
[PROOF STATE]
proof (prove)
using this:
operational_complete (_Collect (T1, T2) True)
weakly_operational_sound (_Collect (T1, T2) True)
operational_sound (_Collect (T1, T2) True)
weak_reduction_bisimulation (_Collect (a, b) True) Target

goal (1 subgoal):
 1. (\<exists>TRel. weakly_operational_corresponding TRel &&& \<exists>TRel. operational_corresponding TRel) &&& \<exists>TRel. weakly_operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target &&& \<exists>TRel. operational_corresponding TRel \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
by blast+


[STATEMENT]
lemma (in encoding) strong_operational_correspondence_modulo_some_target_relation:
  shows "(\<exists>TRel. strongly_operational_corresponding TRel)
         = (\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T))"
    and "(\<exists>TRel. strongly_operational_corresponding TRel
          \<and> weak_reduction_bisimulation TRel Target)
         = (\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)) &&& (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
 2. (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
have A1: "\<exists>TRel. strongly_operational_corresponding TRel
            \<Longrightarrow> \<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)

goal (2 subgoals):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
 2. (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)

goal (2 subgoals):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
 2. (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
have A2: "\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T)
                     \<Longrightarrow> \<exists>TRel. strongly_operational_corresponding TRel
                          \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
assume "\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T)"
[PROOF STATE]
proof (state)
this:
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)

goal (1 subgoal):
 1. \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
hence "strongly_operational_corresponding {(T1, T2). True}"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)

goal (1 subgoal):
 1. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True))

goal (1 subgoal):
 1. \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
thus "\<exists>TRel. strongly_operational_corresponding TRel
          \<and> weak_reduction_bisimulation TRel Target"
[PROOF STATE]
proof (prove)
using this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True))

goal (1 subgoal):
 1. \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
using all_relation_is_weak_reduction_bisimulation[where Cal="Target"]
[PROOF STATE]
proof (prove)
using this:
(\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> _Collect (T1, T2) True))
weak_reduction_bisimulation (_Collect (a, b) True) Target

goal (1 subgoal):
 1. \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target

goal (2 subgoals):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
 2. (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
show "(\<exists>TRel. strongly_operational_corresponding TRel
                    \<and> weak_reduction_bisimulation TRel Target)
                   = (\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T))"
[PROOF STATE]
proof (prove)
using this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. (\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))

goal (1 subgoal):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
from A1 A2
[PROOF STATE]
proof (chain)
picking this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target
[PROOF STEP]
show "(\<exists>TRel. strongly_operational_corresponding TRel)
                   = (\<forall>S. (\<exists>S'. S \<longmapsto>Source S') \<longleftrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T))"
[PROOF STATE]
proof (prove)
using this:
\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<Longrightarrow> \<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target)
\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target) \<Longrightarrow> \<exists>TRel. ((\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) \<and> weak_reduction_bisimulation TRel Target

goal (1 subgoal):
 1. (\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>TRel. (\<forall>S S'. S \<longmapsto>Source S' \<longrightarrow> (\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel)) \<and> (\<forall>S T. \<lbrakk>S\<rbrakk> \<longmapsto>Target T \<longrightarrow> (\<exists>S'. S \<longmapsto>Source S' \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel))) = (\<forall>S. Ex (step S Source) = Ex (step (\<lbrakk>S\<rbrakk>) Target))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding) weak_reduction_simulation_impl_OCom:
  fixes Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
    and TRel :: "('procT \<times> 'procT) set"
  assumes A1: "\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
      and A2: "\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*"
      and A3: "weak_reduction_simulation Rel (STCal Source Target)"
  shows "operational_complete (TRel\<^sup>*)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. operational_complete (TRel\<^sup>*)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
fix S S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
[PROOF STEP]
have "(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

goal (1 subgoal):
 1. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
assume "S \<longmapsto>Source* S'"
[PROOF STATE]
proof (state)
this:
S \<longmapsto>Source* S'

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
hence "SourceTerm S \<longmapsto>(STCal Source Target)* (SourceTerm S')"
[PROOF STATE]
proof (prove)
using this:
S \<longmapsto>Source* S'

goal (1 subgoal):
 1. SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
[PROOF STEP]
by (simp add: STCal_steps(1))
[PROOF STATE]
proof (state)
this:
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
[PROOF STEP]
obtain Q' where A5: "TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>(STCal Source Target)* Q'"
                         and A6: "(SourceTerm S', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'

goal (1 subgoal):
 1. (\<And>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<and> (SourceTerm S', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A3
[PROOF STATE]
proof (prove)
using this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> Rel
SourceTerm S \<longmapsto>STCal Source Target* SourceTerm S'
weak_reduction_simulation Rel (STCal Source Target)

goal (1 subgoal):
 1. (\<And>Q'. TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q' \<and> (SourceTerm S', Q') \<in> Rel \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q'
(SourceTerm S', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A5
[PROOF STATE]
proof (chain)
picking this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q'
[PROOF STEP]
obtain T where A7: "T \<in>T Q'" and A8: "\<lbrakk>S\<rbrakk> \<longmapsto>Target* T"
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<longmapsto>STCal Source Target* Q'

goal (1 subgoal):
 1. (\<And>T. T \<in>T Q' \<and> \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: STCal_steps(2))
[PROOF STATE]
proof (state)
this:
T \<in>T Q'
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
from A2 A6 A7
[PROOF STATE]
proof (chain)
picking this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
(SourceTerm S', Q') \<in> Rel
T \<in>T Q'
[PROOF STEP]
have "(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<forall>S T. (SourceTerm S, TargetTerm T) \<in> Rel \<longrightarrow> (\<lbrakk>S\<rbrakk>, T) \<in> TRel\<^sup>*
(SourceTerm S', Q') \<in> Rel
T \<in>T Q'

goal (1 subgoal):
 1. (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<And>S S'. S \<longmapsto>Source* S' \<Longrightarrow> \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
with A8
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
show "\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>S\<rbrakk> \<longmapsto>Target* T
(\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal (1 subgoal):
 1. \<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T. \<lbrakk>S\<rbrakk> \<longmapsto>Target* T \<and> (\<lbrakk>S'\<rbrakk>, T) \<in> TRel\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed