[STATEMENT]
lemma cf_const_if_HomCod_is_cat_1:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>"
  shows "\<KK> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 4. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<open>cat_1 \<aa> \<ff>\<close> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 4. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>) : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_1 \<aa> \<ff>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = \<BB>
 5. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
have ObjMap_dom_lhs: "\<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = \<BB>
 5. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
have ObjMap_dom_rhs: "\<D>\<^sub>\<circ> (cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = \<BB>
 5. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
have ArrMap_dom_lhs: "\<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (simp add: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = \<BB>
 5. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
have ArrMap_dom_rhs: "\<D>\<^sub>\<circ> (cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (simp add: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = \<BB>
 5. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
show "\<KK>\<lparr>ObjMap\<rparr> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
have "\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
[PROOF STEP]
by (auto intro: \<KK>.cf_ObjMap_app_in_HomCod_Obj)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
[PROOF STEP]
have "\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<aa>"
[PROOF STATE]
proof (prove)
using this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<aa>
[PROOF STEP]
by (auto simp: cat_1_components)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<aa>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<aa>
[PROOF STEP]
show "\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<aa>

goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (auto simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>

goal (4 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
 3. ?\<AA> = \<BB>
 4. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
show "\<KK>\<lparr>ArrMap\<rparr> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
have "\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto intro: \<KK>.cf_ArrMap_app_in_HomCod_Arr)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
[PROOF STEP]
have "\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<ff>"
[PROOF STATE]
proof (prove)
using this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<ff>
[PROOF STEP]
by (auto simp: cat_1_components)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<ff>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<ff>
[PROOF STEP]
show "\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<ff>

goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (auto simp: cat_1_CId_app cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
qed (auto intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>

goal (3 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. ?\<AA> = \<BB>
 3. ?\<BB> = cat_1 \<aa> \<ff>
[PROOF STEP]
qed (simp_all add: assms)


[STATEMENT]
lemma cf_const_if_HomDom_is_cat_1:
  assumes "\<KK> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<KK> = cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<CC> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
from cat_1_components(1)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}
[PROOF STEP]
have \<aa>: "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}

goal (1 subgoal):
 1. \<aa> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<KK>.HomDom.cat_in_Obj_in_Vset)
[PROOF STATE]
proof (state)
this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
from cat_1_components(2)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}
[PROOF STEP]
have \<ff>: "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}

goal (1 subgoal):
 1. \<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<KK>.HomDom.cat_in_Arr_in_Vset)
[PROOF STATE]
proof (state)
this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
from \<aa> \<ff>
[PROOF STATE]
proof (chain)
picking this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
interpret cf_1:
    is_tm_functor \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<CC> \<open>cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>m\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: cat_small_cs_intros cat_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. \<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>
 4. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = cat_1 \<aa> \<ff>
 5. ?\<BB> = \<CC>
[PROOF STEP]
have ObjMap_dom_lhs: "\<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = set {\<aa>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = ZFC_in_HOL.set {\<aa>}
[PROOF STEP]
by (simp add: cat_cs_simps cat_1_components)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<KK>\<lparr>ObjMap\<rparr>) = ZFC_in_HOL.set {\<aa>}

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = cat_1 \<aa> \<ff>
 5. ?\<BB> = \<CC>
[PROOF STEP]
have ObjMap_dom_rhs:
      "\<D>\<^sub>\<circ> (cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>) = set {\<aa>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>) = ZFC_in_HOL.set {\<aa>}
[PROOF STEP]
by (simp add: cat_cs_simps cat_1_components)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>) = ZFC_in_HOL.set {\<aa>}

goal (5 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>
 3. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 4. ?\<AA> = cat_1 \<aa> \<ff>
 5. ?\<BB> = \<CC>
[PROOF STEP]
show "\<KK>\<lparr>ObjMap\<rparr> = cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. ZFC_in_HOL.set {\<aa>} = ZFC_in_HOL.set {\<aa>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>} \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. ZFC_in_HOL.set {\<aa>} = ZFC_in_HOL.set {\<aa>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>} \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> set {\<aa>}"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>}

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. ZFC_in_HOL.set {\<aa>} = ZFC_in_HOL.set {\<aa>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>} \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>}
[PROOF STEP]
have a_def: "a = \<aa>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>}

goal (1 subgoal):
 1. a = \<aa>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = \<aa>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. ZFC_in_HOL.set {\<aa>} = ZFC_in_HOL.set {\<aa>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>} \<Longrightarrow> \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_1_components(1) cat_cs_simps a_def
              cs_intro: V_cs_intros
          )
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (\<KK>\<lparr>ObjMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>)
 3. ZFC_in_HOL.set {\<aa>} = ZFC_in_HOL.set {\<aa>}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ObjMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ObjMap\<rparr>

goal (4 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 3. ?\<AA> = cat_1 \<aa> \<ff>
 4. ?\<BB> = \<CC>
[PROOF STEP]
have ArrMap_dom_lhs: "\<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = set {\<ff>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
by (simp add: cat_cs_simps cat_1_components)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<KK>\<lparr>ArrMap\<rparr>) = ZFC_in_HOL.set {\<ff>}

goal (4 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 3. ?\<AA> = cat_1 \<aa> \<ff>
 4. ?\<BB> = \<CC>
[PROOF STEP]
have ArrMap_dom_rhs:
      "\<D>\<^sub>\<circ> (cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>) = set {\<ff>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>) = ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
by (simp add: cat_cs_simps cat_1_components)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>) = ZFC_in_HOL.set {\<ff>}

goal (4 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
 3. ?\<AA> = cat_1 \<aa> \<ff>
 4. ?\<BB> = \<CC>
[PROOF STEP]
show "\<KK>\<lparr>ArrMap\<rparr> = cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. ZFC_in_HOL.set {\<ff>} = ZFC_in_HOL.set {\<ff>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>} \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. ZFC_in_HOL.set {\<ff>} = ZFC_in_HOL.set {\<ff>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>} \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "f \<in>\<^sub>\<circ> set {\<ff>}"
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. ZFC_in_HOL.set {\<ff>} = ZFC_in_HOL.set {\<ff>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>} \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
have f_def: "f = \<ff>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}

goal (1 subgoal):
 1. f = \<ff>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = \<ff>

goal (4 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. ZFC_in_HOL.set {\<ff>} = ZFC_in_HOL.set {\<ff>}
 4. \<And>a. a \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>} \<Longrightarrow> \<KK>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = cf_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK>\<lparr>ArrMap\<rparr>\<lparr>\<ff>\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>\<ff>\<rparr>
[PROOF STEP]
by (subst cat_1_CId_app[symmetric, of \<ff> \<aa>])
          (
            cs_concl cs_shallow
              cs_simp: cat_1_components(1,2) cat_cs_simps
              cs_intro: V_cs_intros cat_cs_intros
          )
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (3 subgoals):
 1. vsv (\<KK>\<lparr>ArrMap\<rparr>)
 2. vsv (dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>)
 3. ZFC_in_HOL.set {\<ff>} = ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<KK>\<lparr>ArrMap\<rparr> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)\<lparr>ArrMap\<rparr>

goal (3 subgoals):
 1. \<KK> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. ?\<AA> = cat_1 \<aa> \<ff>
 3. ?\<BB> = \<CC>
[PROOF STEP]
qed (simp_all add: assms)
[PROOF STATE]
proof (state)
this:
\<KK> = dghm_const (cat_1 \<aa> \<ff>) \<CC> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<CC>\<lparr>CId\<rparr>\<lparr>\<KK>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma if_cong':
  "b = c \<Longrightarrow> x = u \<Longrightarrow> y = v \<Longrightarrow> (if b then x else y) = (if c then u else v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = c; x = u; y = v\<rbrakk> \<Longrightarrow> (if b then x else y) = (if c then u else v)
[PROOF STEP]
by auto


[STATEMENT]
lemma ta_der_strict_Var:
  "q |\<in>| ta_der_strict \<A> (Var x) \<longleftrightarrow> x = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q |\<in>| ta_der_strict \<A> (Var x)) = (x = q)
[PROOF STEP]
unfolding ta_der.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q |\<in>| ta_der_strict \<A> (Var x)) = (x = q)
[PROOF STEP]
by auto


[STATEMENT]
lemma ta_der_strict_Fun:
  "q |\<in>| ta_der_strict \<A> (Fun f ts) \<longleftrightarrow> (\<exists> ps p. TA_rule f ps p |\<in>| (rules \<A>) \<and>
      (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and>
      (\<forall> i < length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i)))" (is "?Ls \<longleftrightarrow> ?Rs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q |\<in>| ta_der_strict \<A> (Fun f ts)) = (\<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i)))
[PROOF STEP]
unfolding ta_der_strict.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q |\<in>| {|uu_. \<exists>q' q qs. uu_ = q' \<and> f qs \<rightarrow> q |\<in>| rules \<A> \<and> (q = q' \<or> (q, q') |\<in>| (eps \<A>)|\<^sup>+|) \<and> length qs = length ts \<and> (\<forall>i<length ts. qs ! i |\<in>| ta_der_strict \<A> (ts ! i))|}) = (\<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i)))
[PROOF STEP]
by (intro iffI fCollect_memberI finite_Collect_less_eq[OF _ finite_eps[of \<A>]]) auto


[STATEMENT]
lemma ta_der_strict_sub_ta_der:
  "ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. ta_der_strict \<A> (Var x) |\<subseteq>| ta_der \<A> (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ta_der_strict \<A> x2a |\<subseteq>| ta_der \<A> x2a) \<Longrightarrow> ta_der_strict \<A> (Fun x1a x2) |\<subseteq>| ta_der \<A> (Fun x1a x2)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
?x2a \<in> set ts \<Longrightarrow> ta_der_strict \<A> ?x2a |\<subseteq>| ta_der \<A> ?x2a

goal (2 subgoals):
 1. \<And>x. ta_der_strict \<A> (Var x) |\<subseteq>| ta_der \<A> (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ta_der_strict \<A> x2a |\<subseteq>| ta_der \<A> x2a) \<Longrightarrow> ta_der_strict \<A> (Fun x1a x2) |\<subseteq>| ta_der \<A> (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2a \<in> set ts \<Longrightarrow> ta_der_strict \<A> ?x2a |\<subseteq>| ta_der \<A> ?x2a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x2a \<in> set ts \<Longrightarrow> ta_der_strict \<A> ?x2a |\<subseteq>| ta_der \<A> ?x2a

goal (1 subgoal):
 1. ta_der_strict \<A> (Fun f ts) |\<subseteq>| ta_der \<A> (Fun f ts)
[PROOF STEP]
by auto (metis fsubsetD nth_mem)+
[PROOF STATE]
proof (state)
this:
ta_der_strict \<A> (Fun f ts) |\<subseteq>| ta_der \<A> (Fun f ts)

goal (1 subgoal):
 1. \<And>x. ta_der_strict \<A> (Var x) |\<subseteq>| ta_der \<A> (Var x)
[PROOF STEP]
qed auto


[STATEMENT]
lemma ta_der_strict_ta_der_eq_on_ground:
  assumes"ground t"
  shows "ta_der \<A> t = ta_der_strict \<A> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_der \<A> t = ta_der_strict \<A> t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
fix q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
assume "q |\<in>| ta_der \<A> t"
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der \<A> t

goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| ta_der \<A> t
[PROOF STEP]
have "q |\<in>| ta_der_strict \<A> t"
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \<A> t

goal (1 subgoal):
 1. q |\<in>| ta_der_strict \<A> t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der \<A> t
ground t

goal (1 subgoal):
 1. q |\<in>| ta_der_strict \<A> t
[PROOF STEP]
proof (induct t arbitrary: q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der \<A> (Var x); ground (Var x)\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> (Var x)
 2. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der \<A> x2a; ground x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; q |\<in>| ta_der \<A> (Fun x1a x2); ground (Fun x1a x2)\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> (Fun x1a x2)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set ts; ?q |\<in>| ta_der \<A> ?x2a; ground ?x2a\<rbrakk> \<Longrightarrow> ?q |\<in>| ta_der_strict \<A> ?x2a
q |\<in>| ta_der \<A> (Fun f ts)
ground (Fun f ts)

goal (2 subgoals):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der \<A> (Var x); ground (Var x)\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> (Var x)
 2. \<And>x1a x2 q. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set x2; q |\<in>| ta_der \<A> x2a; ground x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; q |\<in>| ta_der \<A> (Fun x1a x2); ground (Fun x1a x2)\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set ts; ?q |\<in>| ta_der \<A> ?x2a; ground ?x2a\<rbrakk> \<Longrightarrow> ?q |\<in>| ta_der_strict \<A> ?x2a
q |\<in>| ta_der \<A> (Fun f ts)
ground (Fun f ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; ?q |\<in>| ta_der \<A> ?x2a; ground ?x2a\<rbrakk> \<Longrightarrow> ?q |\<in>| ta_der_strict \<A> ?x2a
q |\<in>| ta_der \<A> (Fun f ts)
ground (Fun f ts)

goal (1 subgoal):
 1. q |\<in>| ta_der_strict \<A> (Fun f ts)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ps. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set ts; q |\<in>| ta_der \<A> x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; \<forall>x\<in>set ts. ground x; f ps \<rightarrow> q |\<in>| rules \<A>; length ps = length ts; \<forall>i<length ts. ps ! i |\<in>| ta_der \<A> (ts ! i)\<rbrakk> \<Longrightarrow> \<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i))
 2. \<And>ps p. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set ts; q |\<in>| ta_der \<A> x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; \<forall>x\<in>set ts. ground x; f ps \<rightarrow> p |\<in>| rules \<A>; length ps = length ts; \<forall>i<length ts. ps ! i |\<in>| ta_der \<A> (ts ! i); (p, q) |\<in>| (eps \<A>)|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i))
[PROOF STEP]
using nth_mem
[PROOF STATE]
proof (prove)
using this:
?n < length ?xs \<Longrightarrow> ?xs ! ?n \<in> set ?xs

goal (2 subgoals):
 1. \<And>ps. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set ts; q |\<in>| ta_der \<A> x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; \<forall>x\<in>set ts. ground x; f ps \<rightarrow> q |\<in>| rules \<A>; length ps = length ts; \<forall>i<length ts. ps ! i |\<in>| ta_der \<A> (ts ! i)\<rbrakk> \<Longrightarrow> \<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i))
 2. \<And>ps p. \<lbrakk>\<And>x2a q. \<lbrakk>x2a \<in> set ts; q |\<in>| ta_der \<A> x2a\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> x2a; \<forall>x\<in>set ts. ground x; f ps \<rightarrow> p |\<in>| rules \<A>; length ps = length ts; \<forall>i<length ts. ps ! i |\<in>| ta_der \<A> (ts ! i); (p, q) |\<in>| (eps \<A>)|\<^sup>+|\<rbrakk> \<Longrightarrow> \<exists>ps p. f ps \<rightarrow> p |\<in>| rules \<A> \<and> (p = q \<or> (p, q) |\<in>| (eps \<A>)|\<^sup>+|) \<and> length ps = length ts \<and> (\<forall>i<length ts. ps ! i |\<in>| ta_der_strict \<A> (ts ! i))
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der_strict \<A> (Fun f ts)

goal (1 subgoal):
 1. \<And>x q. \<lbrakk>q |\<in>| ta_der \<A> (Var x); ground (Var x)\<rbrakk> \<Longrightarrow> q |\<in>| ta_der_strict \<A> (Var x)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
q |\<in>| ta_der_strict \<A> t

goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?q2 |\<in>| ta_der \<A> t \<Longrightarrow> ?q2 |\<in>| ta_der_strict \<A> t

goal (2 subgoals):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
 2. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?q2 |\<in>| ta_der \<A> t \<Longrightarrow> ?q2 |\<in>| ta_der_strict \<A> t
[PROOF STEP]
show "ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t"
[PROOF STATE]
proof (prove)
using this:
?q2 |\<in>| ta_der \<A> t \<Longrightarrow> ?q2 |\<in>| ta_der_strict \<A> t

goal (1 subgoal):
 1. ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ta_der \<A> t |\<subseteq>| ta_der_strict \<A> t

goal (1 subgoal):
 1. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
show "ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
using ta_der_strict_sub_ta_der
[PROOF STATE]
proof (prove)
using this:
ta_der_strict ?\<A> ?t |\<subseteq>| ta_der ?\<A> ?t

goal (1 subgoal):
 1. ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ta_der_strict \<A> t |\<subseteq>| ta_der \<A> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_der_to_ta_strict:
  assumes "q |\<in>| ta_der A C\<langle>Var p\<rangle>" and "ground_ctxt C"
  shows "\<exists> q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der A C\<langle>Var p\<rangle>
ground_ctxt C

goal (1 subgoal):
 1. \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>
[PROOF STEP]
proof (induct C arbitrary: q p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
 2. \<And>x1 x2 C x4 q p. \<lbrakk>\<And>q p. \<lbrakk>q |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>; q |\<in>| ta_der A (More x1 x2 C x4)\<langle>Var p\<rangle>; ground_ctxt (More x1 x2 C x4)\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More x1 x2 C x4)\<langle>Var q'\<rangle>
[PROOF STEP]
case (More f ss C ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?q |\<in>| ta_der A C\<langle>Var ?p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (?p = q' \<or> (?p, q') |\<in>| (eps A)|\<^sup>+|) \<and> ?q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>
q |\<in>| ta_der A (More f ss C ts)\<langle>Var p\<rangle>
ground_ctxt (More f ss C ts)

goal (2 subgoals):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
 2. \<And>x1 x2 C x4 q p. \<lbrakk>\<And>q p. \<lbrakk>q |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>; q |\<in>| ta_der A (More x1 x2 C x4)\<langle>Var p\<rangle>; ground_ctxt (More x1 x2 C x4)\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More x1 x2 C x4)\<langle>Var q'\<rangle>
[PROOF STEP]
from More(2)
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| ta_der A (More f ss C ts)\<langle>Var p\<rangle>
[PROOF STEP]
obtain qs q' where
    r: "TA_rule f qs q' |\<in>| rules A" "length qs = Suc (length ss + length ts)" "q' = q \<or> (q', q) |\<in>| (eps A)|\<^sup>+|" and
    rec: "\<forall> i < length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)"
[PROOF STATE]
proof (prove)
using this:
q |\<in>| ta_der A (More f ss C ts)\<langle>Var p\<rangle>

goal (1 subgoal):
 1. (\<And>qs q'. \<lbrakk>f qs \<rightarrow> q' |\<in>| rules A; length qs = Suc (length ss + length ts); q' = q \<or> (q', q) |\<in>| (eps A)|\<^sup>+|; \<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f qs \<rightarrow> q' |\<in>| rules A
length qs = Suc (length ss + length ts)
q' = q \<or> (q', q) |\<in>| (eps A)|\<^sup>+|
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)

goal (2 subgoals):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
 2. \<And>x1 x2 C x4 q p. \<lbrakk>\<And>q p. \<lbrakk>q |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>; q |\<in>| ta_der A (More x1 x2 C x4)\<langle>Var p\<rangle>; ground_ctxt (More x1 x2 C x4)\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More x1 x2 C x4)\<langle>Var q'\<rangle>
[PROOF STEP]
from More(1)[of "qs ! length ss" p] More(3) rec r(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>qs ! length ss |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>
ground_ctxt (More f ss C ts)
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)
length qs = Suc (length ss + length ts)
[PROOF STEP]
obtain q'' where
    mid: "(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>qs ! length ss |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>
ground_ctxt (More f ss C ts)
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)
length qs = Suc (length ss + length ts)

goal (1 subgoal):
 1. (\<And>q''. (p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto (metis length_map less_add_Suc1 nth_append_length)
[PROOF STATE]
proof (state)
this:
(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>

goal (2 subgoals):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
 2. \<And>x1 x2 C x4 q p. \<lbrakk>\<And>q p. \<lbrakk>q |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>; q |\<in>| ta_der A (More x1 x2 C x4)\<langle>Var p\<rangle>; ground_ctxt (More x1 x2 C x4)\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More x1 x2 C x4)\<langle>Var q'\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>
[PROOF STEP]
have "\<forall> i < length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)"
[PROOF STATE]
proof (prove)
using this:
(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>

goal (1 subgoal):
 1. \<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)
[PROOF STEP]
using rec r(2) More(3)
[PROOF STATE]
proof (prove)
using this:
(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)
length qs = Suc (length ss + length ts)
ground_ctxt (More f ss C ts)

goal (1 subgoal):
 1. \<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)
[PROOF STEP]
using ta_der_strict_ta_der_eq_on_ground[of _ A]
[PROOF STATE]
proof (prove)
using this:
(p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|) \<and> qs ! length ss |\<in>| ta_der_strict A C\<langle>Var q''\<rangle>
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)
length qs = Suc (length ss + length ts)
ground_ctxt (More f ss C ts)
ground ?t \<Longrightarrow> ta_der A ?t = ta_der_strict A ?t

goal (1 subgoal):
 1. \<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)
[PROOF STEP]
by (auto simp: nth_append_Cons all_Suc_conv fmember.rep_eq split:if_splits cong: if_cong')
[PROOF STATE]
proof (state)
this:
\<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)

goal (2 subgoals):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
 2. \<And>x1 x2 C x4 q p. \<lbrakk>\<And>q p. \<lbrakk>q |\<in>| ta_der A C\<langle>Var p\<rangle>; ground_ctxt C\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A C\<langle>Var q'\<rangle>; q |\<in>| ta_der A (More x1 x2 C x4)\<langle>Var p\<rangle>; ground_ctxt (More x1 x2 C x4)\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More x1 x2 C x4)\<langle>Var q'\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)

goal (1 subgoal):
 1. \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More f ss C ts)\<langle>Var q'\<rangle>
[PROOF STEP]
using rec r conjunct1[OF mid]
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length qs. qs ! i |\<in>| ta_der_strict A ((ss @ C\<langle>Var q''\<rangle> # ts) ! i)
\<forall>i<length qs. qs ! i |\<in>| ta_der A ((ss @ C\<langle>Var p\<rangle> # ts) ! i)
f qs \<rightarrow> q' |\<in>| rules A
length qs = Suc (length ss + length ts)
q' = q \<or> (q', q) |\<in>| (eps A)|\<^sup>+|
p = q'' \<or> (p, q'') |\<in>| (eps A)|\<^sup>+|

goal (1 subgoal):
 1. \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More f ss C ts)\<langle>Var q'\<rangle>
[PROOF STEP]
by (rule_tac x = q'' in exI, auto intro!: exI[of _ q'] exI[of _ qs])
[PROOF STATE]
proof (state)
this:
\<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A (More f ss C ts)\<langle>Var q'\<rangle>

goal (1 subgoal):
 1. \<And>q p. \<lbrakk>q |\<in>| ta_der A \<box>\<langle>Var p\<rangle>; ground_ctxt \<box>\<rbrakk> \<Longrightarrow> \<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps A)|\<^sup>+|) \<and> q |\<in>| ta_der_strict A \<box>\<langle>Var q'\<rangle>
[PROOF STEP]
qed auto


[STATEMENT]
lemma root_to_root_ctxt [simp]:
  assumes "C \<noteq> \<box>"
  shows "fst (the (root C\<langle>t\<rangle>)) \<longleftrightarrow> root_ctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (root C\<langle>t\<rangle>)) = root_ctxt C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<noteq> \<box>

goal (1 subgoal):
 1. fst (the (root C\<langle>t\<rangle>)) = root_ctxt C
[PROOF STEP]
by (cases C) auto


[STATEMENT]
lemma Q_inf_states_ta_states:
  assumes "(p, q) \<in> Q_inf \"
  shows "p |\<in>| \<Q> \" "q |\<in>| \<Q> \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p |\<in>| \<Q> \ &&& q |\<in>| \<Q> \
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> Q_inf \

goal (1 subgoal):
 1. p |\<in>| \<Q> \ &&& q |\<in>| \<Q> \
[PROOF STEP]
by (induct) (auto simp: rule_statesD eps_statesD)


[STATEMENT]
lemma Q_inf_finite:
  "finite (Q_inf \<A>)" "finite (Q_inf_e \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Q_inf \<A>) &&& finite (Q_inf_e \<A>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (Q_inf \<A>)
 2. finite (Q_inf_e \<A>)
[PROOF STEP]
have *: "Q_inf \<A> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<A>)" "Q_inf_e \<A> \<subseteq> fset (\<Q> \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q_inf \<A> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<A>) &&& Q_inf_e \<A> \<subseteq> fset (\<Q> \<A>)
[PROOF STEP]
by (auto simp add: Q_inf_states_ta_states(1, 2) subrelI simp flip: fmember.rep_eq)
[PROOF STATE]
proof (state)
this:
Q_inf \<A> \<subseteq> fset (\<Q> \<A> |\<times>| \<Q> \<A>)
Q_inf_e \<A> \<subseteq> fset (\<Q> \<A>)

goal (2 subgoals):
 1. finite (Q_inf \<A>)
 2. finite (Q_inf_e \<A>)
[PROOF STEP]
show "finite (Q_inf \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Q_inf \<A>)
[PROOF STEP]
by (intro finite_subset[OF *(1)]) simp
[PROOF STATE]
proof (state)
this:
finite (Q_inf \<A>)

goal (1 subgoal):
 1. finite (Q_inf_e \<A>)
[PROOF STEP]
show "finite (Q_inf_e \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Q_inf_e \<A>)
[PROOF STEP]
by (intro finite_subset[OF *(2)]) simp
[PROOF STATE]
proof (state)
this:
finite (Q_inf_e \<A>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_inf_ta_eps_Q_inf:
  assumes "(p, q) \<in> Q_inf \" and "(q, q') |\<in>| (eps \)|\<^sup>+|"
  shows "(p, q') \<in> Q_inf \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q') \<in> Q_inf \
[PROOF STEP]
using assms(2, 1)
[PROOF STATE]
proof (prove)
using this:
(q, q') |\<in>| (eps \)|\<^sup>+|
(p, q) \<in> Q_inf \

goal (1 subgoal):
 1. (p, q') \<in> Q_inf \
[PROOF STEP]
by (induct rule: ftrancl_induct) (auto simp add: Q_inf.eps)


[STATEMENT]
lemma lhs_state_rule:
  assumes "(p, q) \<in> Q_inf \<A>"
  shows "\<exists> f qs r. (None, Some f) qs \<rightarrow> r |\<in>| rules \<A> \<and> p |\<in>| fset_of_list qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f qs r. lift_None_Some f qs \<rightarrow> r |\<in>| rules \<A> \<and> p |\<in>| fset_of_list qs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> Q_inf \<A>

goal (1 subgoal):
 1. \<exists>f qs r. lift_None_Some f qs \<rightarrow> r |\<in>| rules \<A> \<and> p |\<in>| fset_of_list qs
[PROOF STEP]
by induct (force intro: nth_mem)+