[STATEMENT]
lemma dghm_comp_dghm_tdghm_comp_assoc:
  assumes "\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
  shows "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<AA> \<BB> \<HH> \<HH>' \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
interpret \<FF>: is_dghm \<alpha> \<BB> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
interpret \<GG>: is_dghm \<alpha> \<CC> \
 \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> :
    \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (6 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = ?\<FF>'
 4. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \
 = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = ?\<FF>'
 4. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \
 = ?\<BB>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) :
    \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (5 subgoals):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>'
 4. \<AA> = \<AA>
 5. \
 = \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
have dom_rhs:
    "\<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>'
 4. \<AA> = \<AA>
 5. \
 = \

[PROOF STEP]
show
    "((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> =
      (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
      "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
        (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>'
 3. \<AA> = \<AA>
 4. \
 = \

[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in is_tdghm) tdghm_dghm_tdghm_comp_dghm_id[dg_cs_simps]:
  "dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<NN>
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<NN> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show "dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (6 subgoals):
 1. \<NN> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 3. \<FF> = ?\<FF>'
 4. \<GG> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \<BB> = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<NN> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 3. \<FF> = ?\<FF>'
 4. \<GG> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \<BB> = ?\<BB>'
[PROOF STEP]
show "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (5 subgoals):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 2. \<FF> = \<FF>
 3. \<GG> = \<GG>
 4. \<AA> = \<AA>
 5. \<BB> = \<BB>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dg_cs_simps)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv (\<NN>\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv (\<NN>\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<NN>\<lparr>NTMap\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (\<NN>\<lparr>NTMap\<rparr>)

goal (3 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 3. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (2 subgoals):
 1. vsv ((dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>)
 2. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: dg_cs_intros)+
[PROOF STATE]
proof (state)
this:
(dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>
 2. \<GG> = \<GG>
 3. \<AA> = \<AA>
 4. \<BB> = \<BB>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dghm_tdghm_comp_tdghm_dghm_comp_assoc:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
    and "\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<BB> \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<HH>: is_dghm \<alpha> \<CC> \
 \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<KK>: is_dghm \<alpha> \<AA> \<BB> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have dom_lhs:
      "\<D>\<^sub>\<circ> (((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (7 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have dom_rhs:
      "\<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (7 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show
      "((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> =
        (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<lparr>NTMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>))\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ngba_param[param]:
    "(ngba, ngba) \<in> \<langle>L\<rangle> set_rel \<rightarrow> \<langle>S\<rangle> set_rel \<rightarrow> (L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel) \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel \<rightarrow>
      \<langle>L, S\<rangle> ngba_rel"
    "(alphabet, alphabet) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>L\<rangle> set_rel"
    "(initial, initial) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S\<rangle> set_rel"
    "(transition, transition) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel"
    "(accepting, accepting) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle> list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ngba, ngba) \<in> \<langle>L\<rangle>set_rel \<rightarrow> \<langle>S\<rangle>set_rel \<rightarrow> (L \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel) \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle>list_rel \<rightarrow> \<langle>L, S\<rangle>ngba_rel &&& (alphabet, alphabet) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>L\<rangle>set_rel) &&& (initial, initial) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>S\<rangle>set_rel &&& (transition, transition) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> L \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel &&& (accepting, accepting) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>S \<rightarrow> bool_rel\<rangle>list_rel
[PROOF STEP]
unfolding ngba_rel_def fun_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ngba, ngba) \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>L\<rangle>set_rel. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>S\<rangle>set_rel. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>{(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}}. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel. (f a, f' a') \<in> {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}} \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}}}}} &&& (alphabet, alphabet) \<in> {(f, f'). \<forall>(a, a')\<in>{(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}} \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}. (f a, f' a') \<in> \<langle>L\<rangle>set_rel}) &&& (initial, initial) \<in> {(f, f'). \<forall>(a, a')\<in>{(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}} \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}. (f a, f' a') \<in> \<langle>S\<rangle>set_rel} &&& (transition, transition) \<in> {(f, f'). \<forall>(a, a')\<in>{(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}} \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}}} &&& (accepting, accepting) \<in> {(f, f'). \<forall>(a, a')\<in>{(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>L\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>S\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> {(f, f'). \<forall>(a, a')\<in>L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> \<langle>S\<rangle>set_rel}} \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}. (f a, f' a') \<in> \<langle>{(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> bool_rel}\<rangle>list_rel}
[PROOF STEP]
by auto


[STATEMENT]
lemma ngba_rel_id[simp]: "\<langle>Id, Id\<rangle> ngba_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id, Id\<rangle>ngba_rel = Id
[PROOF STEP]
unfolding ngba_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>set_rel \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>Id \<rightarrow> bool_rel\<rangle>list_rel} = Id
[PROOF STEP]
using ngba.expand
[PROOF STATE]
proof (prove)
using this:
alphabet ?ngba = alphabet ?ngba' \<and> initial ?ngba = initial ?ngba' \<and> transition ?ngba = transition ?ngba' \<and> accepting ?ngba = accepting ?ngba' \<Longrightarrow> ?ngba = ?ngba'

goal (1 subgoal):
 1. {(A\<^sub>1, A\<^sub>2). (alphabet A\<^sub>1, alphabet A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (initial A\<^sub>1, initial A\<^sub>2) \<in> \<langle>Id\<rangle>set_rel \<and> (transition A\<^sub>1, transition A\<^sub>2) \<in> Id \<rightarrow> Id \<rightarrow> \<langle>Id\<rangle>set_rel \<and> (accepting A\<^sub>1, accepting A\<^sub>2) \<in> \<langle>Id \<rightarrow> bool_rel\<rangle>list_rel} = Id
[PROOF STEP]
by auto


[STATEMENT]
lemma enableds_param[param]: "(ngba.enableds, ngba.enableds) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>L \<times>\<^sub>r S\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ngba.enableds, ngba.enableds) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>L \<times>\<^sub>r S\<rangle>set_rel
[PROOF STEP]
using ngba_param(2, 4)
[PROOF STATE]
proof (prove)
using this:
(alphabet, alphabet) \<in> \<langle>?L, ?S\<rangle>ngba_rel \<rightarrow> \<langle>?L\<rangle>set_rel
(transition, transition) \<in> \<langle>?L, ?S\<rangle>ngba_rel \<rightarrow> ?L \<rightarrow> ?S \<rightarrow> \<langle>?S\<rangle>set_rel

goal (1 subgoal):
 1. (ngba.enableds, ngba.enableds) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>L \<times>\<^sub>r S\<rangle>set_rel
[PROOF STEP]
unfolding ngba.enableds_def fun_rel_def set_rel_def
[PROOF STATE]
proof (prove)
using this:
(alphabet, alphabet) \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>?L, ?S\<rangle>ngba_rel. (f a, f' a') \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> ?L) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> ?L)}}
(transition, transition) \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>?L, ?S\<rangle>ngba_rel. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>?L. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>?S. (f a, f' a') \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> ?S) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> ?S)}}}}

goal (1 subgoal):
 1. (\<lambda>A p. {a. fst a \<in> alphabet A \<and> snd a \<in> transition A (fst a) p}, \<lambda>A p. {a. fst a \<in> alphabet A \<and> snd a \<in> transition A (fst a) p}) \<in> {(f, f'). \<forall>(a, a')\<in>\<langle>L, S\<rangle>ngba_rel. (f a, f' a') \<in> {(f, f'). \<forall>(a, a')\<in>S. (f a, f' a') \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> L \<times>\<^sub>r S) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> L \<times>\<^sub>r S)}}}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma paths_param[param]: "(ngba.paths, ngba.paths) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle> list_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ngba.paths, ngba.paths) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle>list_rel\<rangle>set_rel
[PROOF STEP]
using enableds_param[param_fo]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x1, ?x'1) \<in> \<langle>?L2, ?A\<rangle>ngba_rel; (?x, ?x') \<in> ?A\<rbrakk> \<Longrightarrow> (ngba.enableds ?x1 ?x, ngba.enableds ?x'1 ?x') \<in> \<langle>?L2 \<times>\<^sub>r ?A\<rangle>set_rel

goal (1 subgoal):
 1. (ngba.paths, ngba.paths) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle>list_rel\<rangle>set_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma runs_param[param]: "(ngba.runs, ngba.runs) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle> stream_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ngba.runs, ngba.runs) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
using enableds_param[param_fo]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x1, ?x'1) \<in> \<langle>?L2, ?A\<rangle>ngba_rel; (?x, ?x') \<in> ?A\<rbrakk> \<Longrightarrow> (ngba.enableds ?x1 ?x, ngba.enableds ?x'1 ?x') \<in> \<langle>?L2 \<times>\<^sub>r ?A\<rangle>set_rel

goal (1 subgoal):
 1. (ngba.runs, ngba.runs) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>\<langle>L \<times>\<^sub>r S\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma reachable_param[param]: "(reachable, reachable) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (reachable, reachable) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (reachable, reachable) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
have 1: "reachable A p = (\<lambda> wr. target wr p) ` ngba.paths A p" for A :: "('label, 'state) ngba" and p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable A p = (\<lambda>wr. target wr p) ` ngba.paths A p
[PROOF STEP]
unfolding ngba.reachable_alt_def ngba.paths_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {target r p |r. path A r p} = (\<lambda>wr. target wr p) ` {r. path A r p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable ?A1 ?p1 = (\<lambda>wr. target wr ?p1) ` ngba.paths ?A1 ?p1

goal (1 subgoal):
 1. (reachable, reachable) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (reachable, reachable) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A p. (\<lambda>wr. target wr p) ` ngba.paths A p, \<lambda>A p. (\<lambda>wr. target wr p) ` ngba.paths A p) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
using enableds_param[param_fo]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x1, ?x'1) \<in> \<langle>?L2, ?A\<rangle>ngba_rel; (?x, ?x') \<in> ?A\<rbrakk> \<Longrightarrow> (ngba.enableds ?x1 ?x, ngba.enableds ?x'1 ?x') \<in> \<langle>?L2 \<times>\<^sub>r ?A\<rangle>set_rel

goal (1 subgoal):
 1. (\<lambda>A p. (\<lambda>wr. target wr p) ` ngba.paths A p, \<lambda>A p. (\<lambda>wr. target wr p) ` ngba.paths A p) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(reachable, reachable) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> S \<rightarrow> \<langle>S\<rangle>set_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nodes_param[param]: "(nodes, nodes) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>S\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nodes, nodes) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
unfolding ngba.nodes_alt_def Collect_mem_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. \<Union> (reachable A ` initial A), \<lambda>A. \<Union> (reachable A ` initial A)) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>S\<rangle>set_rel
[PROOF STEP]
by parametricity


[STATEMENT]
lemma language_param[param]: "(language, language) \<in> \<langle>L, S\<rangle> ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle> stream_rel\<rangle> set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language, language) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (language, language) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
have 1: "language A = (\<Union> p \<in> initial A. \<Union> wr \<in> ngba.runs A p.
      if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})"
      for A :: "('label, 'state) ngba"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. language A = (\<Union>p\<in>initial A. \<Union>wr\<in>ngba.runs A p. if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {})
[PROOF STEP]
unfolding ngba.language_def ngba.runs_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>w r p. uu_ = w \<and> p \<in> initial A \<and> run A (w ||| r) p \<and> gen infs (accepting A) (p ## r)} = \<Union> {y. \<exists>x\<in>initial A. y = \<Union> {y. \<exists>xa\<in>{r. run A r x}. y = (if gen infs (accepting A) (x ## smap snd xa) then {smap fst xa} else {})}}
[PROOF STEP]
by (auto iff: split_szip_ex simp del: alw_smap)
[PROOF STATE]
proof (state)
this:
language ?A1 = (\<Union>p\<in>initial ?A1. \<Union>wr\<in>ngba.runs ?A1 p. if gen infs (accepting ?A1) (p ## smap snd wr) then {smap fst wr} else {})

goal (1 subgoal):
 1. (language, language) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language, language) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>A. \<Union>p\<in>initial A. \<Union>wr\<in>ngba.runs A p. if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {}, \<lambda>A. \<Union>p\<in>initial A. \<Union>wr\<in>ngba.runs A p. if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {}) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
using enableds_param[param_fo]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x1, ?x'1) \<in> \<langle>?L2, ?A\<rangle>ngba_rel; (?x, ?x') \<in> ?A\<rbrakk> \<Longrightarrow> (ngba.enableds ?x1 ?x, ngba.enableds ?x'1 ?x') \<in> \<langle>?L2 \<times>\<^sub>r ?A\<rangle>set_rel

goal (1 subgoal):
 1. (\<lambda>A. \<Union>p\<in>initial A. \<Union>wr\<in>ngba.runs A p. if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {}, \<lambda>A. \<Union>p\<in>initial A. \<Union>wr\<in>ngba.runs A p. if gen infs (accepting A) (p ## smap snd wr) then {smap fst wr} else {}) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(language, language) \<in> \<langle>L, S\<rangle>ngba_rel \<rightarrow> \<langle>\<langle>L\<rangle>stream_rel\<rangle>set_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma OT_12_P1_assms_bound': "\<bar>spmf (bind_spmf (R1_OT12 (m0,m1) c) (\<lambda> view. ((D::'v_OT121 \<Rightarrow> bool spmf) view ))) True
                - spmf (bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (D view ))) True\<bar> \<le> adv_OT12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
have "sim_det_def.adv_P1 R1_OT12 S1_OT12 funct_OT_12 (m0,m1) c D =
                      \<bar>spmf (bind_spmf (R1_OT12 (m0,m1) c) (\<lambda> view. (D view ))) True
                                    - spmf (funct_OT_12 (m0,m1) c \<bind> (\<lambda> ((out1::unit), (out2::bool)).
                                              S1_OT12 (m0,m1) out1 \<bind> (\<lambda> view. D view))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>
[PROOF STEP]
using sim_det_def.adv_P1_def
[PROOF STATE]
proof (prove)
using this:
sim_det_def ?R1.0 ?S1.0 ?R2.0 ?S2.0 ?funct \<Longrightarrow> sim_det_def.adv_P1 ?R1.0 ?S1.0 ?funct ?m1.0 ?m2.0 ?D \<equiv> \<bar>spmf (?R1.0 ?m1.0 ?m2.0 \<bind> ?D) True - spmf (?funct ?m1.0 ?m2.0 \<bind> (\<lambda>(o1, o2). ?S1.0 ?m1.0 o1 \<bind> ?D)) True\<bar>

goal (1 subgoal):
 1. OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>
[PROOF STEP]
using  OT_12_sim.adv_P1_def
[PROOF STATE]
proof (prove)
using this:
sim_det_def ?R1.0 ?S1.0 ?R2.0 ?S2.0 ?funct \<Longrightarrow> sim_det_def.adv_P1 ?R1.0 ?S1.0 ?funct ?m1.0 ?m2.0 ?D \<equiv> \<bar>spmf (?R1.0 ?m1.0 ?m2.0 \<bind> ?D) True - spmf (?funct ?m1.0 ?m2.0 \<bind> (\<lambda>(o1, o2). ?S1.0 ?m1.0 o1 \<bind> ?D)) True\<bar>
OT_12_sim.adv_P1 ?m1.0 ?m2.0 ?D \<equiv> \<bar>spmf (R1_OT12 ?m1.0 ?m2.0 \<bind> ?D) True - spmf (funct_OT_12 ?m1.0 ?m2.0 \<bind> (\<lambda>(o1, o2). S1_OT12 ?m1.0 o1 \<bind> ?D)) True\<bar>

goal (1 subgoal):
 1. OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
have "... = \<bar>spmf (bind_spmf (R1_OT12 (m0,m1) c) (\<lambda> view. ((D::'v_OT121 \<Rightarrow> bool spmf) view ))) True
                - spmf (bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (D view ))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar> = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar>
[PROOF STEP]
by(simp add: funct_OT_12_def)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar> = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>
\<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar> = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
OT_12_sim.adv_P1 (m0, m1) c D = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar>
\<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (funct_OT_12 (m0, m1) c \<bind> (\<lambda>(out1, out2). S1_OT12 (m0, m1) out1 \<bind> D)) True\<bar> = \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar>

goal (1 subgoal):
 1. \<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12
[PROOF STEP]
by(metis ass_adv_OT12)
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_OT12 (m0, m1) c \<bind> D) True - spmf (S1_OT12 (m0, m1) () \<bind> D) True\<bar> \<le> adv_OT12

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma OT_12_P2_assm: "R2_OT12 (m0,m1) \<sigma> = funct_OT_12 (m0,m1) \<sigma> \<bind> (\<lambda> (out1, out2). S2_OT12 \<sigma> out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_OT12 (m0, m1) \<sigma> = funct_OT_12 (m0, m1) \<sigma> \<bind> (\<lambda>(out1, out2). S2_OT12 \<sigma> out2)
[PROOF STEP]
using inf_th_OT12_P2 OT_12_sim.perfect_sec_P2_def
[PROOF STATE]
proof (prove)
using this:
sim_det_def.perfect_sec_P2 R2_OT12 S2_OT12 ?funct_OT12.0 (?m0.0, ?m1.0) ?\<sigma>
OT_12_sim.perfect_sec_P2 ?m1.0 ?m2.0 \<equiv> R2_OT12 ?m1.0 ?m2.0 = funct_OT_12 ?m1.0 ?m2.0 \<bind> (\<lambda>(s1, s2). S2_OT12 ?m2.0 s2)

goal (1 subgoal):
 1. R2_OT12 (m0, m1) \<sigma> = funct_OT_12 (m0, m1) \<sigma> \<bind> (\<lambda>(out1, out2). S2_OT12 \<sigma> out2)
[PROOF STEP]
by blast


[STATEMENT]
lemma lossless_protocol_14_OT: "lossless_spmf (protocol_14_OT M C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (protocol_14_OT M C)
[PROOF STEP]
by(simp add: protocol_14_OT_def lossless_protocol_OT12 split_def)


[STATEMENT]
lemma lossless_R1_14: "lossless_spmf (R1_14 msgs C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (R1_14 msgs C)
[PROOF STEP]
by(simp add: R1_14_def split_def lossless_R1_12)


[STATEMENT]
lemma lossless_R1_14_interm1: "lossless_spmf (R1_14_interm1 msgs C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (R1_14_interm1 msgs C)
[PROOF STEP]
by(simp add: R1_14_interm1_def split_def lossless_R1_12 lossless_S1_12)


[STATEMENT]
lemma lossless_R1_14_interm2: "lossless_spmf (R1_14_interm2 msgs C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (R1_14_interm2 msgs C)
[PROOF STEP]
by(simp add: R1_14_interm2_def split_def lossless_R1_12 lossless_S1_12)


[STATEMENT]
lemma lossless_S1_14: "lossless_spmf (S1_14 m out)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (S1_14 m out)
[PROOF STEP]
by(simp add: S1_14_def lossless_S1_12)


[STATEMENT]
lemma reduction_step1:
  shows "\<exists> A1. \<bar>spmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True\<bar> =
              \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (\<lambda> view. (A1 view (m0,m1))))) True -
                  spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1 view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
define A1' where "A1' == \<lambda> (view :: 'v_OT121) (m0,m1). do {
    S2 :: bool \<leftarrow> coin_spmf;
    S3 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    S5 :: bool \<leftarrow> coin_spmf;
    b :: 'v_OT121 \<leftarrow> R1_OT12 (S2, S3) c1;
    c :: 'v_OT121 \<leftarrow> R1_OT12 (S4, S5) c1;
    let R = (M, (m0,m1, S2, S3, S4, S5), view, b, c);
    D R}"
[PROOF STATE]
proof (state)
this:
A1' \<equiv> \<lambda>view (m0, m1). coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. Let (M, (m0, m1, S2, S3, S4, S5), view, b, c) D))))))

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
have "\<bar>spmf (bind_spmf (R1_14 M (c0, c1)) D) True - spmf (bind_spmf (R1_14_interm1 M (c0, c1)) D) True\<bar> =
       \<bar>spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (R1_OT12 (m0,m1) c0) (\<lambda> view. (A1' view (m0,m1))))) True -
        spmf (bind_spmf (pair_spmf coin_spmf coin_spmf) (\<lambda>(m0, m1). bind_spmf (S1_OT12 (m0,m1) ()) (\<lambda> view. (A1' view (m0,m1))))) True\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
apply(simp add: pair_spmf_alt_def R1_14_def R1_14_interm1_def A1'_def Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. S1_OT12 (y, ya) () \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True\<bar>
[PROOF STEP]
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. S1_OT12 (y, ya) () \<bind> (\<lambda>x. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (yb, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, S3, S4, S5), x, b, c))))))))))) True\<bar>
[PROOF STEP]
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. S1_OT12 (y, ya) () \<bind> (\<lambda>x. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, yc, S4, S5), x, b, c))))))))))) True\<bar>
[PROOF STEP]
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yd. S1_OT12 (y, ya) () \<bind> (\<lambda>x. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, yc, S4, S5), x, yd, c))))))))))) True\<bar>
[PROOF STEP]
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. S1_OT12 (y, ya) () \<bind> (\<lambda>x. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (ye, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, yc, ye, S5), x, yd, c))))))))))) True\<bar>
[PROOF STEP]
apply(subst bind_commute_spmf[of "S1_OT12 _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. R1_OT12 (yf, yg) c1 \<bind> (\<lambda>yh. D (M, (y, ya, yc, yd, yf, yg), yb, ye, yh))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c1 \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. coin_spmf \<bind> (\<lambda>yd. R1_OT12 (yc, yd) c1 \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. coin_spmf \<bind> (\<lambda>yg. S1_OT12 (yf, yg) () \<bind> (\<lambda>yh. D (M, (yf, yg, y, ya, yc, yd), yh, yb, ye))))))))))) True\<bar> = \<bar>spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. R1_OT12 (y, ya) c0 \<bind> (\<lambda>view. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S3. R1_OT12 (S2, S3) c1 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>S5. R1_OT12 (S4, S5) c1 \<bind> (\<lambda>c. D (M, (y, ya, S2, S3, S4, S5), view, b, c))))))))))) True - spmf (coin_spmf \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. coin_spmf \<bind> (\<lambda>yc. R1_OT12 (yb, yc) c1 \<bind> (\<lambda>yd. coin_spmf \<bind> (\<lambda>ye. coin_spmf \<bind> (\<lambda>yf. S1_OT12 (y, ya) () \<bind> (\<lambda>x. R1_OT12 (ye, yf) c1 \<bind> (\<lambda>c. D (M, (y, ya, yb, yc, ye, yf), x, yd, c))))))))))) True\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1' view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1' view (m0, m1)))) True\<bar>

goal (1 subgoal):
 1. \<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>A1. \<bar>spmf (R1_14 M (c0, c1) \<bind> D) True - spmf (R1_14_interm1 M (c0, c1) \<bind> D) True\<bar> = \<bar>spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). R1_OT12 (m0, m1) c0 \<bind> (\<lambda>view. A1 view (m0, m1)))) True - spmf (pair_spmf coin_spmf coin_spmf \<bind> (\<lambda>(m0, m1). S1_OT12 (m0, m1) () \<bind> (\<lambda>view. A1 view (m0, m1)))) True\<bar>

goal:
No subgoals!
[PROOF STEP]
qed