[STATEMENT]
lemma dummy_stack_balanced:
  assumes "set S \<subseteq> Dummy ` UNIV"
  assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
  obtains T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from build_trace[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
[PROOF STEP]
obtain T where "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "\<forall> c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. \<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'
[PROOF STEP]
by (rule conjunct1[OF traces_list_all])
       (auto elim: step.cases simp add: dummy_stack_extended[OF \<open>set S \<subseteq> Dummy ` UNIV\<close>])
[PROOF STATE]
proof (state)
this:
\<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'

goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
\<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'
[PROOF STEP]
have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
\<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'

goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
[PROOF STEP]
by (rule balI) simp
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<And>T. (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_Rel_components:
  shows "cat_Rel \<alpha>\<lparr>Obj\<rparr> = Vset \<alpha>"
    and "cat_Rel \<alpha>\<lparr>Arr\<rparr> = set {T. arr_Rel \<alpha> T}"
    and "cat_Rel \<alpha>\<lparr>Dom\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>set {T. arr_Rel \<alpha> T}. T\<lparr>ArrDom\<rparr>)"
    and "cat_Rel \<alpha>\<lparr>Cod\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>set {T. arr_Rel \<alpha> T}. T\<lparr>ArrCod\<rparr>)"
    and "cat_Rel \<alpha>\<lparr>Comp\<rparr> = (\<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>0\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>)"
    and "cat_Rel \<alpha>\<lparr>CId\<rparr> = VLambda (Vset \<alpha>) id_Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cat_Rel \<alpha>\<lparr>Obj\<rparr> = Vset \<alpha> &&& cat_Rel \<alpha>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {T. arr_Rel \<alpha> T} &&& cat_Rel \<alpha>\<lparr>Dom\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set {T. arr_Rel \<alpha> T}. T\<lparr>ArrDom\<rparr>)) &&& cat_Rel \<alpha>\<lparr>Cod\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set {T. arr_Rel \<alpha> T}. T\<lparr>ArrCod\<rparr>) &&& cat_Rel \<alpha>\<lparr>Comp\<rparr> = (\<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>) &&& cat_Rel \<alpha>\<lparr>CId\<rparr> = VLambda (Vset \<alpha>) id_Rel
[PROOF STEP]
unfolding cat_Rel_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = Vset \<alpha> &&& [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {T. arr_Rel \<alpha> T} &&& [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set {T. arr_Rel \<alpha> T}. T\<lparr>ArrDom\<rparr>)) &&& [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set {T. arr_Rel \<alpha> T}. T\<lparr>ArrCod\<rparr>) &&& [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = (\<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>) &&& [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>\<lparr>5\<^sub>\<nat>\<rparr> = VLambda (Vset \<alpha>) id_Rel
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cat_smc_cat_Rel: "cat_smc (cat_Rel \<alpha>) = smc_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_smc (cat_Rel \<alpha>) = smc_Rel \<alpha>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (cat_smc (cat_Rel \<alpha>))
 2. vsv (smc_Rel \<alpha>)
 3. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (cat_smc (cat_Rel \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (cat_smc (cat_Rel \<alpha>))
[PROOF STEP]
unfolding cat_smc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv [cat_Rel \<alpha>\<lparr>Obj\<rparr>, cat_Rel \<alpha>\<lparr>Arr\<rparr>, cat_Rel \<alpha>\<lparr>Dom\<rparr>, cat_Rel \<alpha>\<lparr>Cod\<rparr>, cat_Rel \<alpha>\<lparr>Comp\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (cat_smc (cat_Rel \<alpha>))

goal (3 subgoals):
 1. vsv (smc_Rel \<alpha>)
 2. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (smc_Rel \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (smc_Rel \<alpha>)
[PROOF STEP]
unfolding smc_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (smc_Rel \<alpha>)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding cat_smc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [cat_Rel \<alpha>\<lparr>Obj\<rparr>, cat_Rel \<alpha>\<lparr>Arr\<rparr>, cat_Rel \<alpha>\<lparr>Dom\<rparr>, cat_Rel \<alpha>\<lparr>Cod\<rparr>, cat_Rel \<alpha>\<lparr>Comp\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = 5\<^sub>\<nat>

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (smc_Rel \<alpha>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (smc_Rel \<alpha>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding smc_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (smc_Rel \<alpha>) = 5\<^sub>\<nat>

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5\<^sub>\<nat> = 5\<^sub>\<nat>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) = \<D>\<^sub>\<circ> (smc_Rel \<alpha>)

goal (1 subgoal):
 1. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show
    "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>a\<rparr> = smc_Rel \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
by
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold cat_smc_def dg_field_simps cat_Rel_def smc_Rel_def
      )
      (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cat_smc (cat_Rel \<alpha>)) \<Longrightarrow> cat_smc (cat_Rel \<alpha>)\<lparr>?a\<rparr> = smc_Rel \<alpha>\<lparr>?a\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) cat_Rel_CId_app[cat_Rel_cs_simps]:
  assumes "T \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>T\<rparr> = id_Rel T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>T\<rparr> = id_Rel T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>T\<rparr> = id_Rel T
[PROOF STEP]
unfolding cat_Rel_components
[PROOF STATE]
proof (prove)
using this:
T \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. VLambda (Vset \<alpha>) id_Rel\<lparr>T\<rparr> = id_Rel T
[PROOF STEP]
by simp


[STATEMENT]
lemma (in \<Z>) category_cat_Rel: "category \<alpha> (cat_Rel \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
proof(rule categoryI, unfold cat_smc_cat_Rel)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (cat_Rel \<alpha>)
 3. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 4. vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>
 5. semicategory \<alpha> (smc_Rel \<alpha>)
 6. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
interpret Rel: semicategory \<alpha> \<open>cat_smc (cat_Rel \<alpha>)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> (cat_smc (cat_Rel \<alpha>))
[PROOF STEP]
unfolding cat_smc_cat_Rel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semicategory \<alpha> (smc_Rel \<alpha>)
[PROOF STEP]
by (simp add: semicategory_smc_Rel)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (cat_Rel \<alpha>)
 3. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 4. vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>
 5. semicategory \<alpha> (smc_Rel \<alpha>)
 6. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vfsequence (cat_Rel \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (cat_Rel \<alpha>)
[PROOF STEP]
unfolding cat_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (cat_Rel \<alpha>)

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 3. vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>
 4. semicategory \<alpha> (smc_Rel \<alpha>)
 5. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 6. \<And>a. a \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a
 7. \<And>a b f. f : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> f = f
 8. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>
[PROOF STEP]
unfolding cat_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [Vset \<alpha>, ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)), \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrDom\<rparr>, \<lambda>T\<in>\<^sub>\<circ>ZFC_in_HOL.set (Collect (arr_Rel \<alpha>)). T\<lparr>ArrCod\<rparr>, \<lambda>ST\<in>\<^sub>\<circ>composable_arrs (dg_Rel \<alpha>). ST\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>R\<^sub>e\<^sub>l ST\<lparr>1\<^sub>\<nat>\<rparr>, VLambda (Vset \<alpha>) id_Rel]\<^sub>\<circ> = 6\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (cat_Rel \<alpha>) = 6\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (smc_Rel \<alpha>)
 4. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> a
 6. \<And>a b f. f : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> f = f
 7. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr> : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
    if "A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>" for A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr> : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr> : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
unfolding cat_Rel_Obj_iff
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr> : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: cat_Rel_cs_simps cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI
      )
[PROOF STATE]
proof (state)
this:
?A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?A\<rparr> : ?A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> ?A

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (smc_Rel \<alpha>)
 4. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 5. \<And>a b f. f : a \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> b \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> f = f
 6. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F"
    if "F : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B" for F A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
F : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
have "arr_Rel \<alpha> F" "A \<in>\<^sub>\<circ> Vset \<alpha>" "B \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
F : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. arr_Rel \<alpha> F &&& A \<in>\<^sub>\<circ> Vset \<alpha> &&& B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto elim: cat_Rel_is_arrE simp: cat_Rel_cs_simps)
[PROOF STATE]
proof (state)
this:
arr_Rel \<alpha> F
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
F : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> F
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
arr_Rel \<alpha> F
A \<in>\<^sub>\<circ> Vset \<alpha>
B \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Rel_cs_simps
            cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI
        )
[PROOF STATE]
proof (state)
this:
cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> F = F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?F : ?A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> ?B \<Longrightarrow> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?B\<rparr> \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> ?F = ?F

goal (5 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (smc_Rel \<alpha>)
 4. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
 5. \<And>b c f. f : b \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F"
    if "F : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> C" for F B C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
F : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> C
[PROOF STEP]
have "arr_Rel \<alpha> F" "B \<in>\<^sub>\<circ> Vset \<alpha>" "C \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
F : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> C

goal (1 subgoal):
 1. arr_Rel \<alpha> F &&& B \<in>\<^sub>\<circ> Vset \<alpha> &&& C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto elim: cat_Rel_is_arrE simp: cat_Rel_cs_simps)
[PROOF STATE]
proof (state)
this:
arr_Rel \<alpha> F
B \<in>\<^sub>\<circ> Vset \<alpha>
C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
F : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> C
arr_Rel \<alpha> F
B \<in>\<^sub>\<circ> Vset \<alpha>
C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> C
arr_Rel \<alpha> F
B \<in>\<^sub>\<circ> Vset \<alpha>
C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Rel_cs_simps
            cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI
        )
[PROOF STATE]
proof (state)
this:
F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr> = F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?F : ?B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> ?C \<Longrightarrow> ?F \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?B\<rparr> = ?F

goal (4 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_Rel \<alpha>\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (smc_Rel \<alpha>)
 4. \<D>\<^sub>\<circ> (cat_Rel \<alpha>\<lparr>CId\<rparr>) = cat_Rel \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto simp: semicategory_smc_Rel cat_Rel_components)


[STATEMENT]
lemma (in \<Z>) category_cat_Rel'[cat_Rel_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<alpha>'' = \<alpha>"
  shows "category \<alpha>' (cat_Rel \<alpha>'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha>' (cat_Rel \<alpha>'')
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule category_cat_Rel)


[STATEMENT]
lemma cf_dag_Rel_components:
  shows "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr> = vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>)"
    and "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr> = VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel"
    and "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomDom\<rparr> = op_cat (cat_Rel \<alpha>)"
    and "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomCod\<rparr> = cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr> = vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>) &&& \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr> = VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel) &&& \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomDom\<rparr> = op_cat (cat_Rel \<alpha>) &&& \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomCod\<rparr> = cat_Rel \<alpha>
[PROOF STEP]
unfolding cf_dag_Rel_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>) &&& [vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel) &&& [vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = op_cat (cat_Rel \<alpha>) &&& [vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = cat_Rel \<alpha>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cf_smcf_cf_dag_Rel: "cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>))
 2. vsv (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 3. \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>a\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding cf_smcf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>, \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>, cat_smc (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomDom\<rparr>), cat_smc (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>HomCod\<rparr>)]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = 4\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>))
 2. vsv (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 3. \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>a\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding smcf_dag_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [vid_on (smc_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (smc_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_smc (smc_Rel \<alpha>), smc_Rel \<alpha>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>

goal (4 subgoals):
 1. vsv (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>))
 2. vsv (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 3. \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>a\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4\<^sub>\<nat> = 4\<^sub>\<nat>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) = \<D>\<^sub>\<circ> (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)

goal (3 subgoals):
 1. vsv (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>))
 2. vsv (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>a\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>a\<rparr>
[PROOF STEP]
show "A \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>A\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>A\<rparr>"
    for A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>A\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>A\<rparr>
[PROOF STEP]
by
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold dghm_field_simps[symmetric],
        unfold
          cat_smc_cat_Rel
          slicing_commute[symmetric]
          cf_smcf_components
          smcf_dag_Rel_components
          cf_dag_Rel_components
          smc_Rel_components
          cat_Rel_components
      )
      simp_all
[PROOF STATE]
proof (state)
this:
?A \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)) \<Longrightarrow> cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)\<lparr>?A\<rparr> = \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>?A\<rparr>

goal (2 subgoals):
 1. vsv (cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>))
 2. vsv (\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
[PROOF STEP]
qed (auto simp: cf_smcf_def smcf_dag_Rel_def)


[STATEMENT]
lemma (in \<Z>) cf_dag_Rel_is_iso_functor:
  "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
proof
  (
    rule is_iso_functorI,
    unfold
      cat_smc_cat_Rel
      cf_smcf_cf_dag_Rel
      cat_Rel_components
      cat_op_simps
      slicing_commute[symmetric]
  )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
 2. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
interpret is_iso_semifunctor \<alpha> \<open>op_smc (smc_Rel \<alpha>)\<close> \<open>smc_Rel \<alpha>\<close> \<open>\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
by (rule smcf_dag_Rel_is_iso_semifunctor)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
 2. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
interpret Rel: category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule category_cat_Rel)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
 2. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
show "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
proof
    (
      rule is_functorI,
      unfold
        cat_smc_cat_Rel
        cf_smcf_cf_dag_Rel
        cat_op_simps
        slicing_commute[symmetric]
        cf_dag_Rel_components(3,4)
    )
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
 3. category \<alpha> (op_cat (cat_Rel \<alpha>))
 4. category \<alpha> (cat_Rel \<alpha>)
 5. vcard (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>
 6. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
 7. op_cat (cat_Rel \<alpha>) = op_cat (cat_Rel \<alpha>)
 8. cat_Rel \<alpha> = cat_Rel \<alpha>
 9. \<And>c. c \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "vfsequence (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)
[PROOF STEP]
unfolding cf_dag_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>)

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (op_cat (cat_Rel \<alpha>))
 3. category \<alpha> (cat_Rel \<alpha>)
 4. vcard (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>
 5. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
 6. op_cat (cat_Rel \<alpha>) = op_cat (cat_Rel \<alpha>)
 7. cat_Rel \<alpha> = cat_Rel \<alpha>
 8. \<And>c. c \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "vcard (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding cf_dag_Rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [vid_on (cat_Rel \<alpha>\<lparr>Obj\<rparr>), VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel, op_cat (cat_Rel \<alpha>), cat_Rel \<alpha>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = 4\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (op_cat (cat_Rel \<alpha>))
 3. category \<alpha> (cat_Rel \<alpha>)
 4. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
 5. op_cat (cat_Rel \<alpha>) = op_cat (cat_Rel \<alpha>)
 6. cat_Rel \<alpha> = cat_Rel \<alpha>
 7. \<And>c. c \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>"
      if "C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>" for C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
have "C \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto elim: cat_Rel_is_arrE simp: cat_Rel_Obj_iff)
[PROOF STATE]
proof (state)
this:
C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
C \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
C \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_Rel_cs_simps cs_intro: cat_cs_intros arr_Rel_id_RelI
          )
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>C\<rparr>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?C \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr> \<Longrightarrow> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>?C\<rparr>\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>?C\<rparr>\<rparr>

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (op_cat (cat_Rel \<alpha>))
 3. category \<alpha> (cat_Rel \<alpha>)
 4. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
 5. op_cat (cat_Rel \<alpha>) = op_cat (cat_Rel \<alpha>)
 6. cat_Rel \<alpha> = cat_Rel \<alpha>
[PROOF STEP]
qed (auto simp: cat_cs_intros intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (1 subgoal):
 1. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
show "\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>
[PROOF STEP]
by (rule smcf_dag_Rel_is_iso_semifunctor)
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_smc (smc_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> smc_Rel \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) cf_dag_Rel_is_iso_functor'[cat_cs_intros]:
  assumes "\<AA>' = op_cat (cat_Rel \<alpha>)"
    and "\<BB>' = cat_Rel \<alpha>"
    and "\<alpha>' = \<alpha>"
  shows "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (rule cf_dag_Rel_is_iso_functor)


[STATEMENT]
lemma (in \<Z>) cf_cn_comp_cf_dag_Rel_cf_dag_Rel:
  "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> = cf_id (cat_Rel \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> = dghm_id (cat_Rel \<alpha>)
[PROOF STEP]
proof(rule cf_smcf_eqI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_id (cat_Rel \<alpha>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. ?\<AA> = ?\<CC>
 4. ?\<BB> = ?\

 5. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
interpret category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule category_cat_Rel)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_id (cat_Rel \<alpha>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. ?\<AA> = ?\<CC>
 4. ?\<BB> = ?\

 5. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
from cf_dag_Rel_is_iso_functor
[PROOF STATE]
proof (chain)
picking this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
have dag:
    "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (simp add: is_iso_functor.axioms(1))
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (5 subgoals):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_id (cat_Rel \<alpha>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. ?\<AA> = ?\<CC>
 4. ?\<BB> = ?\

 5. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
from cf_cn_comp_is_functorI[OF category_axioms dag dag]
[PROOF STATE]
proof (chain)
picking this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
show
    "\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (4 subgoals):
 1. dghm_id (cat_Rel \<alpha>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. cat_Rel \<alpha> = ?\<CC>
 3. cat_Rel \<alpha> = ?\

 4. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
show "cf_id (cat_Rel \<alpha>) : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id (cat_Rel \<alpha>) : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (auto simp: category.cat_cf_id_is_functor category_axioms)
[PROOF STATE]
proof (state)
this:
dghm_id (cat_Rel \<alpha>) : cat_Rel \<alpha> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>

goal (3 subgoals):
 1. cat_Rel \<alpha> = cat_Rel \<alpha>
 2. cat_Rel \<alpha> = cat_Rel \<alpha>
 3. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
show "cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (smcf_id (cat_Rel \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))
[PROOF STEP]
unfolding slicing_commute[symmetric] cat_smc_cat_Rel cf_smcf_cf_dag_Rel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>S\<^sub>M\<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> = dghm_id (smc_Rel \<alpha>)
[PROOF STEP]
by (simp add: smcf_cn_comp_smcf_dag_Rel_smcf_dag_Rel)
[PROOF STATE]
proof (state)
this:
cf_smcf (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> \<^sub>C\<^sub>F\<circ> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>) = cf_smcf (dghm_id (cat_Rel \<alpha>))

goal (2 subgoals):
 1. cat_Rel \<alpha> = cat_Rel \<alpha>
 2. cat_Rel \<alpha> = cat_Rel \<alpha>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma cat_Rel_is_iso_arr_right_vsubset:
  assumes "S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
    and "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
    and "S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>"
    and "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>"
  shows "S\<lparr>ArrVal\<rparr> \<subseteq>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> \<subseteq>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
proof(rule vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
interpret S: arr_Rel \<alpha> S
    rewrites "S\<lparr>ArrDom\<rparr> = B" and "S\<lparr>ArrCod\<rparr> = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> S &&& S\<lparr>ArrDom\<rparr> = B &&& S\<lparr>ArrCod\<rparr> = A
[PROOF STEP]
by (intro cat_Rel_is_arrD[OF assms(1)])+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
interpret T: arr_Rel \<alpha> T
    rewrites "T\<lparr>ArrDom\<rparr> = A" and "T\<lparr>ArrCod\<rparr> = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> T &&& T\<lparr>ArrDom\<rparr> = A &&& T\<lparr>ArrCod\<rparr> = B
[PROOF STEP]
by (intro cat_Rel_is_arrD[OF assms(2)])+
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
interpret Rel: category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (simp add: S.category_cat_Rel)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
interpret dag: is_iso_functor \<alpha> \<open>op_cat (cat_Rel \<alpha>)\<close> \<open>cat_Rel \<alpha>\<close> \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (auto simp: S.cf_dag_Rel_is_iso_functor)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
have A: "A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
have "(S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. (S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>
[PROOF STEP]
have [simp]: "S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A
[PROOF STEP]
unfolding cat_Rel_Comp_app[OF assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(S \<circ>\<^sub>R\<^sub>e\<^sub>l T)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A
[PROOF STEP]
by (simp add: id_Rel_components comp_Rel_components cat_Rel_components)
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> = vid_on A

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
have B: "B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
from assms(4)
[PROOF STATE]
proof (chain)
picking this:
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
have "(T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. (T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
with B
[PROOF STATE]
proof (chain)
picking this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>
[PROOF STEP]
have [simp]: "T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B"
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
[PROOF STEP]
unfolding cat_Rel_Comp_app[OF assms(2,1)]
[PROOF STATE]
proof (prove)
using this:
B \<in>\<^sub>\<circ> cat_Rel \<alpha>\<lparr>Obj\<rparr>
(T \<circ>\<^sub>R\<^sub>e\<^sub>l S)\<lparr>ArrVal\<rparr> = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B
[PROOF STEP]
by (simp add: id_Rel_components comp_Rel_components cat_Rel_components)
[PROOF STATE]
proof (state)
this:
T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> = vid_on B

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
fix ab
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
assume ab: "ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
with S.vbrelation
[PROOF STATE]
proof (chain)
picking this:
vpairs S = S
ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
obtain a b where ab_def: "ab = \<langle>a, b\<rangle>" and "a \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
using this:
vpairs S = S
ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>ab = \<langle>a, b\<rangle>; a \<in>\<^sub>\<circ> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis S.arr_Rel_ArrVal_vdomain S.ArrVal.vbrelation_vinE vsubsetE)
[PROOF STATE]
proof (state)
this:
ab = \<langle>a, b\<rangle>
a \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ab = \<langle>a, b\<rangle>
a \<in>\<^sub>\<circ> B
[PROOF STEP]
have "\<langle>a, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
ab = \<langle>a, b\<rangle>
a \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<langle>a, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
obtain c where "\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>" and ca[intro]: "\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<langle>a, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>; \<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>a, c\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
have "\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<Longrightarrow> False
[PROOF STEP]
assume "\<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (state)
this:
\<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<Longrightarrow> False
[PROOF STEP]
with ca
[PROOF STATE]
proof (chain)
picking this:
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
have "c \<noteq> b"
[PROOF STATE]
proof (prove)
using this:
\<langle>c, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
\<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. c \<noteq> b
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
c \<noteq> b

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<noteq> b

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<Longrightarrow> False
[PROOF STEP]
from ab
[PROOF STATE]
proof (chain)
picking this:
ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
have "\<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
ab \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
unfolding ab_def
[PROOF STATE]
proof (prove)
using this:
\<langle>a, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>b, a\<rangle> \<notin>\<^sub>\<circ> T\<lparr>ArrVal\<rparr> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> b
\<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
c \<noteq> b
\<langle>c, b\<rangle> \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<circ>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: vid_on_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> S\<lparr>ArrVal\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>
[PROOF STEP]
show "ab \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. ab \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
unfolding ab_def
[PROOF STATE]
proof (prove)
using this:
\<langle>b, a\<rangle> \<in>\<^sub>\<circ> T\<lparr>ArrVal\<rparr>

goal (1 subgoal):
 1. \<langle>a, b\<rangle> \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
ab \<in>\<^sub>\<circ> (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_Rel_is_iso_arr_left_vsubset:
  assumes "S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
    and "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
    and "S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>"
    and "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>"
  shows "(T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ> \<subseteq>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ> \<subseteq>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
using assms(2,3,4) cat_Rel_is_iso_arr_right_vsubset[OF assms(2,1)]
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
\<lbrakk>T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>; S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>\<rbrakk> \<Longrightarrow> T\<lparr>ArrVal\<rparr> \<subseteq>\<^sub>\<circ> (S\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>

goal (1 subgoal):
 1. (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ> \<subseteq>\<^sub>\<circ> S\<lparr>ArrVal\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma is_iso_arr_dag:
  assumes "S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A"
    and "T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B"
    and "S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>"
    and "T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>"
  shows "S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>
[PROOF STEP]
proof(rule arr_Rel_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Rel \<alpha> S
 2. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
 3. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 4. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 5. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
interpret S: arr_Rel \<alpha> S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_Rel \<alpha> S
[PROOF STEP]
by (intro cat_Rel_is_arrD(1)[OF assms(1)])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Rel \<alpha> S
 2. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
 3. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 4. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 5. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
interpret Rel: category \<alpha> \<open>cat_Rel \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_Rel \<alpha>)
[PROOF STEP]
by (rule S.category_cat_Rel)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Rel \<alpha> S
 2. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
 3. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 4. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 5. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
interpret dag: is_iso_functor \<alpha> \<open>op_cat (cat_Rel \<alpha>)\<close> \<open>cat_Rel \<alpha>\<close> \<open>\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha> : op_cat (cat_Rel \<alpha>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> cat_Rel \<alpha>
[PROOF STEP]
by (auto simp: S.cf_dag_Rel_is_iso_functor)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. arr_Rel \<alpha> S
 2. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
 3. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 4. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 5. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
[PROOF STEP]
show S: "arr_Rel \<alpha> S"
[PROOF STATE]
proof (prove)
using this:
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A

goal (1 subgoal):
 1. arr_Rel \<alpha> S
[PROOF STEP]
by (fastforce simp: cat_Rel_components(2))
[PROOF STATE]
proof (state)
this:
arr_Rel \<alpha> S

goal (4 subgoals):
 1. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
 2. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 3. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 4. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from cf_dag_Rel_app_is_arr[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>B\<rparr> \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>
[PROOF STEP]
show "arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr> : \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>B\<rparr> \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ObjMap\<rparr>\<lparr>A\<rparr>

goal (1 subgoal):
 1. arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)
[PROOF STEP]
by (auto elim!: cat_Rel_is_arrE)
[PROOF STATE]
proof (state)
this:
arr_Rel \<alpha> (\<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>)

goal (3 subgoals):
 1. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 2. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 3. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
[PROOF STEP]
have T: "arr_Rel \<alpha> T"
[PROOF STATE]
proof (prove)
using this:
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B

goal (1 subgoal):
 1. arr_Rel \<alpha> T
[PROOF STEP]
by (auto simp: cat_Rel_is_arrD(1))
[PROOF STATE]
proof (state)
this:
arr_Rel \<alpha> T

goal (3 subgoals):
 1. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
 2. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 3. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from S T assms
[PROOF STATE]
proof (chain)
picking this:
arr_Rel \<alpha> S
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
show "S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>"
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> S
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>
[PROOF STEP]
unfolding cf_dag_Rel_ArrMap_app[OF T] converse_Rel_components
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> S
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrVal\<rparr> = (T\<lparr>ArrVal\<rparr>)\<inverse>\<^sub>\<circ>
[PROOF STEP]
by (intro vsubset_antisym)
      (
        simp_all add:
          cat_Rel_is_iso_arr_left_vsubset
          cat_Rel_is_iso_arr_right_vsubset
      )
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrVal\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrVal\<rparr>

goal (2 subgoals):
 1. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
 2. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from T assms
[PROOF STATE]
proof (chain)
picking this:
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
show "S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>"
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
[PROOF STEP]
unfolding cf_dag_Rel_components
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> T
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrDom\<rparr> = VLambda (cat_Rel \<alpha>\<lparr>Arr\<rparr>) converse_Rel\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>
[PROOF STEP]
by (auto simp: cat_cs_simps cat_Rel_cs_simps converse_Rel_components(1))
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrDom\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrDom\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
from S assms
[PROOF STATE]
proof (chain)
picking this:
arr_Rel \<alpha> S
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>
[PROOF STEP]
show "S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
arr_Rel \<alpha> S
S : B \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> A
T : A \<mapsto>\<^bsub>cat_Rel \<alpha>\<^esub> B
S \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> T = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>A\<rparr>
T \<circ>\<^sub>A\<^bsub>cat_Rel \<alpha>\<^esub> S = cat_Rel \<alpha>\<lparr>CId\<rparr>\<lparr>B\<rparr>

goal (1 subgoal):
 1. S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>
[PROOF STEP]
by
      (
        cs_concl
          cs_intro: cat_op_intros cat_cs_intros
          cs_simp: cat_Rel_cs_simps cat_cs_simps
      )
[PROOF STATE]
proof (state)
this:
S\<lparr>ArrCod\<rparr> = \<dagger>\<^sub>C\<^sub>.\<^sub>R\<^sub>e\<^sub>l \<alpha>\<lparr>ArrMap\<rparr>\<lparr>T\<rparr>\<lparr>ArrCod\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed