[STATEMENT]
lemma dg_prod_2_is_arrE:
  assumes "gf : ab \<mapsto>\<^bsub>\<AA> \<times>\<^sub>D\<^sub>G \<BB>\<^esub> cd"
  obtains g f a b c d 
    where "gf = [g, f]\<^sub>\<circ>"
      and "ab = [a, b]\<^sub>\<circ>"
      and "cd = [c, d]\<^sub>\<circ>"
      and "g : a \<mapsto>\<^bsub>\<AA>\<^esub> c"
      and "f : b \<mapsto>\<^bsub>\<BB>\<^esub> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from dg_prod_is_arrD[OF assms[unfolded dg_prod_2_def]]
[PROOF STATE]
proof (chain)
picking this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>
[PROOF STEP]
have [simp]: "vsv gf" "\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>" "vsv ab" "\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>" "vsv cd" "\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>"
    and gf_app: 
      "\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> : ab\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = 0 then \<AA> else \<BB>\<^esub> cd\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>

goal (1 subgoal):
 1. ((vsv gf &&& \<D>\<^sub>\<circ> gf = 2\<^sub>\<nat> &&& vsv ab) &&& \<D>\<^sub>\<circ> ab = 2\<^sub>\<nat> &&& vsv cd &&& \<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>) &&& (\<And>i. i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>i\<rparr> : ab\<lparr>i\<rparr> \<mapsto>\<^bsub>if i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>i\<rparr>)
[PROOF STEP]
by (auto simp: two)
[PROOF STATE]
proof (state)
this:
vsv gf
\<D>\<^sub>\<circ> gf = 2\<^sub>\<nat>
vsv ab
\<D>\<^sub>\<circ> ab = 2\<^sub>\<nat>
vsv cd
\<D>\<^sub>\<circ> cd = 2\<^sub>\<nat>
?i \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>?i\<rparr> : ab\<lparr>?i\<rparr> \<mapsto>\<^bsub>if ?i = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>?i\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "gf = [vpfst gf, vpsnd gf]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "ab = [vpfst ab, vpsnd ab]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "cd = [vpfst cd, vpsnd cd]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vsv_vfsequence_two)
[PROOF STATE]
proof (state)
this:
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of 0]
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
have "vpfst gf : vpfst ab \<mapsto>\<^bsub>\<AA>\<^esub> vpfst cd"
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>if []\<^sub>\<circ> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from gf_app[of \<open>1\<^sub>\<nat>\<close>]
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
have "vpsnd gf : vpsnd ab \<mapsto>\<^bsub>\<BB>\<^esub> vpsnd cd"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat> \<Longrightarrow> gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>if 1\<^sub>\<nat> = []\<^sub>\<circ> \<Rightarrow> \<AA> | otherwise \<Rightarrow> \<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. (\<And>g f a b c d. \<lbrakk>gf = [g, f]\<^sub>\<circ>; ab = [a, b]\<^sub>\<circ>; cd = [c, d]\<^sub>\<circ>; g : a \<mapsto>\<^bsub>\<AA>\<^esub> c; f : b \<mapsto>\<^bsub>\<BB>\<^esub> d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
gf = [gf\<lparr>[]\<^sub>\<circ>\<rparr>, gf\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
ab = [ab\<lparr>[]\<^sub>\<circ>\<rparr>, ab\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
cd = [cd\<lparr>[]\<^sub>\<circ>\<rparr>, cd\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
gf\<lparr>[]\<^sub>\<circ>\<rparr> : ab\<lparr>[]\<^sub>\<circ>\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> cd\<lparr>[]\<^sub>\<circ>\<rparr>
gf\<lparr>1\<^sub>\<nat>\<rparr> : ab\<lparr>1\<^sub>\<nat>\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> cd\<lparr>1\<^sub>\<nat>\<rparr>
\<lbrakk>gf = [?g, ?f]\<^sub>\<circ>; ab = [?a, ?b]\<^sub>\<circ>; cd = [?c, ?d]\<^sub>\<circ>; ?g : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?c; ?f : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?d\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed