[STATEMENT]
lemma op_dg_dg_prod_2[dg_op_simps]: "op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>) = op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>) = op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>))
 2. vsv (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 3. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>))
[PROOF STEP]
unfolding op_dg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv [(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>, (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>, (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>, (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>))

goal (3 subgoals):
 1. vsv (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 2. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Obj\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Arr\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> op_dg \<AA> | otherwise \<Rightarrow> op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: op_dg_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = 4\<^sub>\<nat>

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
[PROOF STEP]
unfolding dom_lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4\<^sub>\<nat> = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)
[PROOF STEP]
by (simp add: dg_prod_2_def dg_prod_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) = \<D>\<^sub>\<circ> (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)

goal (1 subgoal):
 1. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
have Cod_Dom: "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)
 2. vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
by (rule dg_prod_2_Cod_vsv)
[PROOF STATE]
proof (state)
this:
vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)

goal (3 subgoals):
 1. vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 2. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_prod_2_Dom_vsv dg_op_intros)+
[PROOF STATE]
proof (state)
this:
vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
unfolding dom_lhs
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: dg_cs_simps dg_op_simps cs_intro: dg_op_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>)

goal (1 subgoal):
 1. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>"
      if "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)" for gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>)

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
unfolding dom_lhs
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
assume "gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain g f
        where gf_def: "gf = [g, f]\<^sub>\<circ>"
          and g: "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
          and f: "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule dg_prod_2_ArrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
from \<AA> \<BB> g f
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
unfolding gf_def
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: dg_prod_cs_simps dg_op_simps
              cs_intro: dg_prod_cs_intros dg_op_intros
          )
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr>\<lparr>?gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>\<lparr>?gf\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>

goal (1 subgoal):
 1. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
have Dom_Cod: "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
 2. vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_prod_2_Cod_vsv dg_op_intros)+
[PROOF STATE]
proof (state)
this:
vsv ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)

goal (3 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
 2. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (3 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
 2. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
unfolding dom_lhs
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: dg_cs_simps dg_op_simps cs_intro: dg_op_intros
        )
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) = \<D>\<^sub>\<circ> ((op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>)

goal (2 subgoals):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>"
      if "gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)" for gf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
unfolding dom_lhs
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
assume "gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
obtain g f
        where gf_def: "gf = [g, f]\<^sub>\<circ>"
          and g: "g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
          and f: "f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>g f. \<lbrakk>gf = [g, f]\<^sub>\<circ>; g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule dg_prod_2_ArrE[OF \<AA> \<BB>]) simp
[PROOF STATE]
proof (state)
this:
gf = [g, f]\<^sub>\<circ>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. gf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
from \<AA> \<BB> g f
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>
[PROOF STEP]
unfolding gf_def
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
g \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: dg_cs_simps dg_prod_cs_simps dg_op_simps
              cs_intro: dg_op_intros dg_prod_cs_intros
          )
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>gf\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?gf \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>) \<Longrightarrow> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>\<lparr>?gf\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>\<lparr>?gf\<rparr>

goal (1 subgoal):
 1. vsv ((\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr>)
[PROOF STEP]
qed (auto intro: \<AA> \<BB> dg_prod_2_Dom_vsv)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>

goal (1 subgoal):
 1. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow>
    op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>a\<rparr>
[PROOF STEP]
proof
    (
      unfold dom_lhs,
      elim_in_numeral,
      fold dg_field_simps,
      unfold op_dg_components
    )
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
 2. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
 3. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>
 4. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_op_simps cs_intro: dg_op_intros)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
 2. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>
 3. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>
[PROOF STEP]
from \<AA> \<BB>
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>
[PROOF STEP]
show "(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
digraph \<alpha> \<BB>

goal (1 subgoal):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_op_simps cs_intro: dg_op_intros)
[PROOF STATE]
proof (state)
this:
(\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Cod\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Dom\<rparr>
 2. (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Dom\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>Cod\<rparr>
[PROOF STEP]
qed (auto simp: \<AA> \<BB> Cod_Dom Dom_Cod)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)) \<Longrightarrow> op_dg (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>?a\<rparr> = (op_dg \<AA> \<times>\<^sub>D\<^sub>G op_dg \<BB>)\<lparr>?a\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_proj_fst_ObjMap_app[dg_cs_simps]:
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr>\<lparr>a, b\<rparr>\<^sub>\<bullet> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = 0 then \<AA> else \<BB>)\<lparr>Obj\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr>\<lparr>a, b\<rparr>\<^sub>\<bullet> = a"
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
unfolding dghm_proj_fst_def dghm_proj_components dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>. a\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>a, b\<rparr>\<^sub>\<bullet> = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_proj_snd_ObjMap_app[dg_cs_simps]:
  assumes "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr>\<lparr>a, b\<rparr>\<^sub>\<bullet> = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = 0 then \<AA> else \<BB>)\<lparr>Obj\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr>\<lparr>a, b\<rparr>\<^sub>\<bullet> = b"
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
unfolding dghm_proj_snd_def dghm_proj_components dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Obj\<rparr>. a\<lparr>1\<^sub>\<nat>\<rparr>) \<lparr>a, b\<rparr>\<^sub>\<bullet> = b
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ObjMap\<rparr> \<lparr>a, b\<rparr>\<^sub>\<bullet> = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_proj_fst_ArrMap_app[dg_cs_simps]:
  assumes "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = g
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = g
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = 0 then \<AA> else \<BB>)\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = g"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = g
[PROOF STEP]
unfolding dghm_proj_fst_def dghm_proj_components dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. f\<lparr>[]\<^sub>\<circ>\<rparr>) \<lparr>g, f\<rparr>\<^sub>\<bullet> = g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_proj_snd_ArrMap_app[dg_cs_simps]:
  assumes "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = 0 then \<AA> else \<BB>)\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G \<BB>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
unfolding dg_prod_2_def dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. [g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr>\<lparr>g, f\<rparr>\<^sub>\<bullet> = f"
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = f
[PROOF STEP]
unfolding dghm_proj_snd_def dghm_proj_components dg_prod_components
[PROOF STATE]
proof (prove)
using this:
[g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>2\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)\<lparr>Arr\<rparr>. f\<lparr>1\<^sub>\<nat>\<rparr>) \<lparr>g, f\<rparr>\<^sub>\<bullet> = f
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>ArrMap\<rparr> \<lparr>g, f\<rparr>\<^sub>\<bullet> = f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_proj_fst_HomDom: "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>HomDom\<rparr> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>HomDom\<rparr> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>
[PROOF STEP]
unfolding dghm_proj_fst_def dghm_proj_components dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>) = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
[PROOF STEP]
..


[STATEMENT]
lemma dghm_proj_fst_HomCod: "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>HomCod\<rparr> = \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB>\<lparr>HomCod\<rparr> = \<AA>
[PROOF STEP]
unfolding dghm_proj_fst_def dghm_proj_components dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>) = \<AA>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_proj_snd_HomDom: "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>HomDom\<rparr> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>HomDom\<rparr> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>
[PROOF STEP]
unfolding dghm_proj_snd_def dghm_proj_components dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>) = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>2\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>)
[PROOF STEP]
..


[STATEMENT]
lemma dghm_proj_snd_HomCod: "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>HomCod\<rparr> = \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB>\<lparr>HomCod\<rparr> = \<BB>
[PROOF STEP]
unfolding dghm_proj_snd_def dghm_proj_components dg_prod_2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>) = \<BB>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_proj_fst_is_dghm:
  assumes "i \<in>\<^sub>\<circ> I"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
    (
      rule pdg_dghm_proj_is_dghm[
        where i=0, simplified, folded dghm_proj_fst_def dg_prod_2_def
        ]
    )


[STATEMENT]
lemma dghm_proj_fst_is_dghm'[dg_cs_intros]:
  assumes "i \<in>\<^sub>\<circ> I" and "\<CC> = \<AA> \<times>\<^sub>D\<^sub>G \<BB>" and "\
 = \<AA>"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>1 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule dghm_proj_fst_is_dghm)


[STATEMENT]
lemma dghm_proj_snd_is_dghm:
  assumes "i \<in>\<^sub>\<circ> I"
  shows "\<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G\<^sub>.\<^sub>2 \<AA> \<BB> : \<AA> \<times>\<^sub>D\<^sub>G \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by
    (
      rule pdg_dghm_proj_is_dghm[
        where i=\<open>1\<^sub>\<nat>\<close>, simplified, folded dghm_proj_snd_def dg_prod_2_def
        ]
    )


[STATEMENT]
lemma finite_pdigraph_dg_prod_3:
  "finite_pdigraph \<alpha> (3\<^sub>\<nat>) (if3 \<AA> \<BB> \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_pdigraph \<alpha> (3\<^sub>\<nat>) (\<lambda>i. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)
[PROOF STEP]
proof(intro finite_pdigraphI pdigraph_baseI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<Z> \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)
 3. 3\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
 4. vfinite (3\<^sub>\<nat>)
[PROOF STEP]
from Axiom_of_Infinity
[PROOF STATE]
proof (chain)
picking this:
\<omega> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show z1_in_Vset: "3\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<omega> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. 3\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
3\<^sub>\<nat> \<in>\<^sub>\<circ> Vset \<alpha>

goal (3 subgoals):
 1. \<Z> \<alpha>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)
 3. vfinite (3\<^sub>\<nat>)
[PROOF STEP]
show "digraph \<alpha> (if3 \<AA> \<BB> \<CC> i)" if "i \<in>\<^sub>\<circ> 3\<^sub>\<nat>" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> digraph \<alpha> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)

goal (2 subgoals):
 1. \<Z> \<alpha>
 2. vfinite (3\<^sub>\<nat>)
[PROOF STEP]
qed auto


[STATEMENT]
lemma digraph_dg_prod_3[dg_cs_intros]: "digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)
[PROOF STEP]
unfolding dg_prod_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>3\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)
[PROOF STEP]
by (rule pdg_digraph_dg_prod)
[PROOF STATE]
proof (state)
this:
digraph \<alpha> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_ObjI:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>" and "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "[a, b, c]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b, c]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a, b, c]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(intro vproductI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv [a, b, c]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [a, b, c]\<^sub>\<circ> = 3\<^sub>\<nat>
 3. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> [a, b, c]\<^sub>\<circ> = 3\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [a, b, c]\<^sub>\<circ> = 3\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [a, b, c]\<^sub>\<circ> = 3\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [a, b, c]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv [a, b, c]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> 3\<^sub>\<nat>"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [a, b, c]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close> | \<open>i = 2\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding three
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>, 2\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vsv [a, b, c]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "[a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if3 \<AA> \<BB> \<CC> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms)
[PROOF STATE]
proof (state)
this:
[a, b, c]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv [a, b, c]\<^sub>\<circ>
[PROOF STEP]
qed auto


[STATEMENT]
lemma dg_prod_3_ObjI'[dg_prod_cs_intros]:
  assumes "abc = [a, b, c]\<^sub>\<circ>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>" and "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "abc \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abc \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
using assms(2-4)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. abc \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. [a, b, c]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule dg_prod_3_ObjI)


[STATEMENT]
lemma dg_prod_3_ObjE:
  assumes "abc \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Obj\<rparr>"
  obtains a b c
    where "abc = [a, b, c]\<^sub>\<circ>"
      and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
      and "b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
      and "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_3_def dg_prod_components]]
[PROOF STATE]
proof (chain)
picking this:
vsv abc
\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>
\<forall>i\<in>elts (3\<^sub>\<nat>). abc\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
have vsv_abc: "vsv abc"
    and dom_abc: "\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>"
    and abc_app: "\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if3 \<AA> \<BB> \<CC> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv abc
\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>
\<forall>i\<in>elts (3\<^sub>\<nat>). abc\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv abc &&& \<D>\<^sub>\<circ> abc = 3\<^sub>\<nat> &&& (\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv abc
\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have dom_abc[simp]: "\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>
[PROOF STEP]
unfolding dom_abc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3\<^sub>\<nat> = 3\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps two)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> abc = 3\<^sub>\<nat>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vsv abc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv abc
[PROOF STEP]
by (rule vsv_abc)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "abc = [vpfst abc, vpsnd abc, vpthrd abc]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (rule vsv_vfsequence_three[symmetric]) auto
[PROOF STATE]
proof (state)
this:
abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from abc_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "vpfst abc \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from abc_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "vpsnd abc \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from abc_app[of \<open>2\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>
[PROOF STEP]
have "vpthrd abc \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<And>a b c. \<lbrakk>abc = [a, b, c]\<^sub>\<circ>; a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
abc = [abc\<lparr>[]\<^sub>\<circ>\<rparr>, abc\<lparr>1\<^sub>\<nat>\<rparr>, abc\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
abc\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
abc\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
abc\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<lbrakk>abc = [?a, ?b, ?c]\<^sub>\<circ>; ?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; ?b \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>; ?c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_ArrI:
  assumes "h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" and "g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>" and "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
  shows "[h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_3_def dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>3\<^sub>\<nat>. (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>)
[PROOF STEP]
proof(intro vproductI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv [h, g, f]\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [h, g, f]\<^sub>\<circ> = 3\<^sub>\<nat>
 3. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> [h, g, f]\<^sub>\<circ> = 3\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [h, g, f]\<^sub>\<circ> = 3\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps three)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [h, g, f]\<^sub>\<circ> = 3\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [h, g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv [h, g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> 3\<^sub>\<nat>"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>

goal (2 subgoals):
 1. vsv [h, g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close> | \<open>i = 2\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding three
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>, 2\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vsv [h, g, f]\<^sub>\<circ>
 2. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "[h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if3 \<AA> \<BB> \<CC> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms)
[PROOF STATE]
proof (state)
this:
[h, g, f]\<^sub>\<circ>\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv [h, g, f]\<^sub>\<circ>
[PROOF STEP]
qed auto


[STATEMENT]
lemma dg_prod_3_ArrI'[dg_prod_cs_intros]:
  assumes "hgf = [h, g, f]\<^sub>\<circ>"
    and "h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
    and "g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
    and "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
  shows "[h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
using assms(2-4)
[PROOF STATE]
proof (prove)
using this:
h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding assms(1)
[PROOF STATE]
proof (prove)
using this:
h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. [h, g, f]\<^sub>\<circ> \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
by (rule dg_prod_3_ArrI)


[STATEMENT]
lemma dg_prod_3_ArrE:
  assumes "hgf \<in>\<^sub>\<circ> (\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>)\<lparr>Arr\<rparr>"
  obtains h g f
    where "hgf = [h, g, f]\<^sub>\<circ>"
      and "h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
      and "g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
      and "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vproductD[OF assms[unfolded dg_prod_3_def dg_prod_components]]
[PROOF STATE]
proof (chain)
picking this:
vsv hgf
\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>
\<forall>i\<in>elts (3\<^sub>\<nat>). hgf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
have vsv_hgf: "vsv hgf"
    and dom_hgf: "\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>"
    and hgf_app: "\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if3 \<AA> \<BB> \<CC> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv hgf
\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>
\<forall>i\<in>elts (3\<^sub>\<nat>). hgf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv hgf &&& \<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat> &&& (\<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>i\<rparr> \<in>\<^sub>\<circ> (if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv hgf
\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>?i\<rparr> \<in>\<^sub>\<circ> (if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have dom_hgf[simp]: "\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>
[PROOF STEP]
unfolding dom_hgf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3\<^sub>\<nat> = 3\<^sub>\<nat>
[PROOF STEP]
by (simp add: three)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> hgf = 3\<^sub>\<nat>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vsv hgf
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv hgf
[PROOF STEP]
by (rule vsv_hgf)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "hgf = [vpfst hgf, vpsnd hgf, vpthrd hgf]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (rule vsv_vfsequence_three[symmetric]) auto
[PROOF STATE]
proof (state)
this:
hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from hgf_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "vpfst hgf \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> (if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | []\<^sub>\<circ> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from hgf_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "vpsnd hgf \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 1\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from hgf_app[of \<open>2\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>
[PROOF STEP]
have "vpthrd hgf \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> (if 2\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | 2\<^sub>\<nat> = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>)\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>h g f. \<lbrakk>hgf = [h, g, f]\<^sub>\<circ>; h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
hgf = [hgf\<lparr>[]\<^sub>\<circ>\<rparr>, hgf\<lparr>1\<^sub>\<nat>\<rparr>, hgf\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
hgf\<lparr>[]\<^sub>\<circ>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
hgf\<lparr>1\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
hgf\<lparr>2\<^sub>\<nat>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
\<lbrakk>hgf = [?h, ?g, ?f]\<^sub>\<circ>; ?h \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; ?g \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>; ?f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_prod_3_is_arrI:
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "f' : a' \<mapsto>\<^bsub>\<BB>\<^esub> b'" and "f'' : a'' \<mapsto>\<^bsub>\<CC>\<^esub> b''"
  shows "[f, f', f'']\<^sub>\<circ> : [a, a', a'']\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ> : [a, a', a'']\<^sub>\<circ> \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G\<^sub>3 \<BB> \<times>\<^sub>D\<^sub>G\<^sub>3 \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>
[PROOF STEP]
unfolding dg_prod_3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ> : [a, a', a'']\<^sub>\<circ> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>3\<^sub>\<nat>. if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>
[PROOF STEP]
proof(rule dg_prod_is_arrI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv [f, f', f'']\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [f, f', f'']\<^sub>\<circ> = 3\<^sub>\<nat>
 3. vsv [a, a', a'']\<^sub>\<circ>
 4. \<D>\<^sub>\<circ> [a, a', a'']\<^sub>\<circ> = 3\<^sub>\<nat>
 5. vsv [b, b', b'']\<^sub>\<circ>
 6. \<D>\<^sub>\<circ> [b, b', b'']\<^sub>\<circ> = 3\<^sub>\<nat>
 7. \<And>i. i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
show "[f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if3 \<AA> \<BB> \<CC> i\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>"
    if "i \<in>\<^sub>\<circ> 3\<^sub>\<nat>" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>
[PROOF STEP]
consider \<open>i = 0\<close> | \<open>i = 1\<^sub>\<nat>\<close> | \<open>i = 2\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> 3\<^sub>\<nat>

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding three
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>, 2\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> thesis; i = 1\<^sub>\<nat> \<Longrightarrow> thesis; i = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show
      "[f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if3 \<AA> \<BB> \<CC> i\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i = []\<^sub>\<circ> \<Longrightarrow> ?thesis; i = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; i = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. [f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>
[PROOF STEP]
by cases (simp_all add: nat_omega_simps assms)
[PROOF STATE]
proof (state)
this:
[f, f', f'']\<^sub>\<circ>\<lparr>i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>i\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<in>\<^sub>\<circ> 3\<^sub>\<nat> \<Longrightarrow> [f, f', f'']\<^sub>\<circ>\<lparr>?i\<rparr> : [a, a', a'']\<^sub>\<circ>\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | ?i = 1\<^sub>\<nat> \<Rightarrow> \<BB> | otherwise \<Rightarrow> \<CC>\<^esub> [b, b', b'']\<^sub>\<circ>\<lparr>?i\<rparr>

goal (6 subgoals):
 1. vsv [f, f', f'']\<^sub>\<circ>
 2. \<D>\<^sub>\<circ> [f, f', f'']\<^sub>\<circ> = 3\<^sub>\<nat>
 3. vsv [a, a', a'']\<^sub>\<circ>
 4. \<D>\<^sub>\<circ> [a, a', a'']\<^sub>\<circ> = 3\<^sub>\<nat>
 5. vsv [b, b', b'']\<^sub>\<circ>
 6. \<D>\<^sub>\<circ> [b, b', b'']\<^sub>\<circ> = 3\<^sub>\<nat>
[PROOF STEP]
qed (auto simp: nat_omega_simps three)