[STATEMENT]
lemma assoc_coherence:
    shows "LHS = RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LHS = RHS
[PROOF STEP]
proof (intro Span.arr_eqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Span.par LHS RHS
 2. Chn LHS = Chn RHS
[PROOF STEP]
show "Span.par LHS RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Span.par LHS RHS
[PROOF STEP]
using par_LHS_RHS
[PROOF STATE]
proof (prove)
using this:
Span.par LHS RHS

goal (1 subgoal):
 1. Span.par LHS RHS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Span.par LHS RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
show "Chn LHS = Chn RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using Chn_LHS_eq
[PROOF STATE]
proof (prove)
using this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Chn LHS = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> =
                \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive HHfgh_HfHgh.is_map THfgh_HHfgh.is_map
                  TTfgh_THfgh.is_map left_adjoints_compose
                  Maps.comp_CLS
                    [of THfgh_HHfgh.chine TTfgh_THfgh.chine "THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"]
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint THfgh_HHfgh.chine; is_left_adjoint TTfgh_THfgh.chine; THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> =
                \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
have "ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
using fg gh HHfgh_HfHgh.is_map THfgh_HHfgh.is_map TTfgh_THfgh.is_map
                      left_adjoint_is_ide left_adjoints_compose
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
is_left_adjoint ?f \<Longrightarrow> ide ?f
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')

goal (1 subgoal):
 1. ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
have "src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
using fg gh HHfgh_HfHgh.chine_in_hom \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<guillemotleft>HHfgh_HfHgh.chine : src (tab\<^sub>0 (local.dom (\<alpha> (f, g, h)))) \<rightarrow> src (tab\<^sub>0 (cod (\<alpha> (f, g, h))))\<guillemotright>
\<guillemotleft>HHfgh_HfHgh.chine : HHfgh_HfHgh.chine \<rightarrow> HHfgh_HfHgh.chine\<guillemotright>
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src HHfgh_HfHgh.chine = trg (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive HHfgh_HfHgh.is_map THfgh_HHfgh.is_map
                    TTfgh_THfgh.is_map left_adjoints_compose
                    Maps.comp_CLS
                      [of HHfgh_HfHgh.chine "THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"
                          "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"]
[PROOF STATE]
proof (prove)
using this:
ide (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine)
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint HHfgh_HfHgh.chine
is_left_adjoint THfgh_HHfgh.chine
is_left_adjoint TTfgh_THfgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint HHfgh_HfHgh.chine; is_left_adjoint (THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine); HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>THfgh_HHfgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret A: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfTgh.tab \<open>(tab\<^sub>0 h \<star> Tgh.p\<^sub>0) \<star> TfTgh.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfTgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfHgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 (g \<star> h) \<star> TfHgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfHgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>\<a>[f, g, h]\<close> \<open>f \<star> g \<star> h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfTgh.tab ((tab\<^sub>0 h \<star> g\<^sub>0h\<^sub>1.p\<^sub>0) \<star> f\<^sub>0gh\<^sub>1.p\<^sub>0) (tab\<^sub>1 f \<star> f\<^sub>0gh\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret B: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> TfHgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 (g \<star> h) \<star> TfHgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 f \<star> TfHgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>\<a>[f, g, h]\<close> \<open>f \<star> g \<star> h\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) (f \<star> g \<star> h) TfHgh.\<rho>\<sigma>.tab (tab\<^sub>0 (g \<star> h) \<star> TfHgh.p\<^sub>0) (tab\<^sub>1 f \<star> TfHgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) \<a>[f, g, h] (f \<star> g \<star> h)
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret C: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> THfgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 h \<star> THfgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 (f \<star> g) \<star> THfgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>(f \<star> g) \<star> h\<close> HHfgh.tab \<open>tab\<^sub>0 ((f \<star> g) \<star> h)\<close> \<open>tab\<^sub>1 ((f \<star> g) \<star> h)\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>(f \<star> g) \<star> h\<close> \<open>\<a>[f, g, h]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) ((f \<star> g) \<star> h) HHfgh.tab (tab\<^sub>0 ((f \<star> g) \<star> h)) (tab\<^sub>1 ((f \<star> g) \<star> h)) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) ((f \<star> g) \<star> h) HHfgh.tab (tab\<^sub>0 ((f \<star> g) \<star> h)) (tab\<^sub>1 ((f \<star> g) \<star> h)) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
interpret D: vertical_composite_of_arrows_of_tabulations_in_maps V H \<a> \<i> src trg
                         \<open>(f \<star> g) \<star> h\<close> TTfgh.tab \<open>tab\<^sub>0 h \<star> TTfgh.p\<^sub>0\<close> \<open>(tab\<^sub>1 f \<star> Tfg.p\<^sub>1) \<star> TTfgh.p\<^sub>1\<close>
                         \<open>(f \<star> g) \<star> h\<close> THfgh.\<rho>\<sigma>.tab \<open>tab\<^sub>0 h \<star> THfgh.\<rho>\<sigma>.p\<^sub>0\<close> \<open>tab\<^sub>1 (f \<star> g) \<star> THfgh.\<rho>\<sigma>.p\<^sub>1\<close>
                         \<open>f \<star> g \<star> h\<close> HfHgh.tab \<open>tab\<^sub>0 (f \<star> g \<star> h)\<close> \<open>tab\<^sub>1 (f \<star> g \<star> h)\<close>
                         \<open>(f \<star> g) \<star> h\<close> \<open>\<a>[f, g, h]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
using fg gh
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h

goal (1 subgoal):
 1. vertical_composite_of_arrows_of_tabulations_in_maps (\<cdot>) (\<star>) \<a> \<i> src trg ((f \<star> g) \<star> h) TTfgh.tab (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) ((tab\<^sub>1 f \<star> f\<^sub>0g\<^sub>1.p\<^sub>1) \<star> fg\<^sub>0h\<^sub>1.p\<^sub>1) ((f \<star> g) \<star> h) THfgh.\<rho>\<sigma>.tab (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) (tab\<^sub>1 (f \<star> g) \<star> THfgh.p\<^sub>1) (f \<star> g \<star> h) HfHgh.tab (tab\<^sub>0 (f \<star> g \<star> h)) (tab\<^sub>1 (f \<star> g \<star> h)) ((f \<star> g) \<star> h) \<a>[f, g, h]
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using D.chine_char
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.chine \<cong> D.\<pi>.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> C.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using fg gh comp_arr_dom isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.\<pi>.chine \<star> TTfgh_THfgh.chine \<cong> C.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
using C.chine_char hcomp_isomorphic_ide
[PROOF STATE]
proof (prove)
using this:
C.chine \<cong> C.\<pi>.chine \<star> THfgh_HHfgh.chine
\<lbrakk>?f \<cong> ?g; ide ?h; src ?f = trg ?h\<rbrakk> \<Longrightarrow> ?f \<star> ?h \<cong> ?g \<star> ?h

goal (1 subgoal):
 1. C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C.chine \<star> TTfgh_THfgh.chine \<cong> (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "C.\<pi>.chine = HHfgh_HfHgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C.\<pi>.chine = HHfgh_HfHgh.chine
[PROOF STEP]
using fg gh comp_arr_dom comp_cod_arr \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. C.\<pi>.chine = HHfgh_HfHgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.\<pi>.chine = HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
hence "isomorphic C.\<pi>.chine HHfgh_HfHgh.chine"
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine = HHfgh_HfHgh.chine

goal (1 subgoal):
 1. C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
[PROOF STEP]
using isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine = HHfgh_HfHgh.chine
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
using hcomp_isomorphic_ide
[PROOF STATE]
proof (prove)
using this:
C.\<pi>.chine \<cong> HHfgh_HfHgh.chine
\<lbrakk>?f \<cong> ?g; ide ?h; src ?f = trg ?h\<rbrakk> \<Longrightarrow> ?f \<star> ?h \<cong> ?g \<star> ?h

goal (1 subgoal):
 1. (C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(C.\<pi>.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
have "... \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
have "src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and>
                             src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
using fg gh HHfgh_HfHgh.chine_in_hom THfgh_HHfgh.chine_in_hom
                      TTfgh_THfgh.chine_in_hom \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<guillemotleft>HHfgh_HfHgh.chine : src (tab\<^sub>0 (local.dom (\<alpha> (f, g, h)))) \<rightarrow> src (tab\<^sub>0 (cod (\<alpha> (f, g, h))))\<guillemotright>
\<guillemotleft>HHfgh_HfHgh.chine : HHfgh_HfHgh.chine \<rightarrow> HHfgh_HfHgh.chine\<guillemotright>
\<guillemotleft>THfgh_HHfgh.chine : src (tab\<^sub>0 h \<star> THfgh.p\<^sub>0) \<rightarrow> src (tab\<^sub>0 ((f \<star> g) \<star> h))\<guillemotright>
\<guillemotleft>THfgh_HHfgh.chine : THfgh_HHfgh.chine \<rightarrow> THfgh_HHfgh.chine\<guillemotright>
\<guillemotleft>TTfgh_THfgh.chine : src (tab\<^sub>0 h \<star> fg\<^sub>0h\<^sub>1.p\<^sub>0) \<rightarrow> src (tab\<^sub>0 h \<star> THfgh.p\<^sub>0)\<guillemotright>
\<guillemotleft>TTfgh_THfgh.chine : TTfgh_THfgh.chine \<rightarrow> TTfgh_THfgh.chine\<guillemotright>
\<alpha> ?\<mu>\<nu>\<tau> \<equiv> \<a>[fst ?\<mu>\<nu>\<tau>, fst (snd ?\<mu>\<nu>\<tau>), snd (snd ?\<mu>\<nu>\<tau>)]

goal (1 subgoal):
 1. src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
using fg gh iso_assoc isomorphic_def
                       assoc_in_hom [of HHfgh_HfHgh.chine THfgh_HHfgh.chine TTfgh_THfgh.chine]
[PROOF STATE]
proof (prove)
using this:
ide HHfgh_HfHgh.chine \<and> ide THfgh_HHfgh.chine \<and> ide TTfgh_THfgh.chine
src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine \<and> src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine
src f = trg g
src g = trg h
\<lbrakk>ide ?f; ide ?g; ide ?h; src ?f = trg ?g; src ?g = trg ?h\<rbrakk> \<Longrightarrow> local.iso \<a>[?f, ?g, ?h]
(?a \<cong> ?a') = (\<exists>f. \<guillemotleft>f : ?a \<rightarrow> ?a'\<guillemotright> \<and> local.iso f)
\<lbrakk>ide HHfgh_HfHgh.chine; ide THfgh_HHfgh.chine; ide TTfgh_THfgh.chine; src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine; src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<guillemotleft>\<a>[HHfgh_HfHgh.chine, THfgh_HHfgh.chine, TTfgh_THfgh.chine] : src TTfgh_THfgh.chine \<rightarrow> trg HHfgh_HfHgh.chine\<guillemotright>
\<lbrakk>ide HHfgh_HfHgh.chine; ide THfgh_HHfgh.chine; ide TTfgh_THfgh.chine; src HHfgh_HfHgh.chine = trg THfgh_HHfgh.chine; src THfgh_HHfgh.chine = trg TTfgh_THfgh.chine\<rbrakk> \<Longrightarrow> \<guillemotleft>\<a>[HHfgh_HfHgh.chine, THfgh_HHfgh.chine, TTfgh_THfgh.chine] : (local.dom HHfgh_HfHgh.chine \<star> local.dom THfgh_HHfgh.chine) \<star> local.dom TTfgh_THfgh.chine \<rightarrow> cod HHfgh_HfHgh.chine \<star> cod THfgh_HHfgh.chine \<star> cod TTfgh_THfgh.chine\<guillemotright>

goal (1 subgoal):
 1. (HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine) \<star> TTfgh_THfgh.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
using isomorphic_symmetric
[PROOF STATE]
proof (prove)
using this:
D.chine \<cong> HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine
?f \<cong> ?g \<Longrightarrow> ?g \<cong> ?f

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> D.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "... \<cong> B.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
have "D.chine = B.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D.chine = B.chine
[PROOF STEP]
using fg gh comp_arr_dom comp_cod_arr
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; local.dom ?f = ?a\<rbrakk> \<Longrightarrow> ?f \<cdot> ?a = ?f
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f

goal (1 subgoal):
 1. D.chine = B.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine = B.chine

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
D.chine = B.chine

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
using isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
D.chine = B.chine
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. D.chine \<cong> B.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
D.chine \<cong> B.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine
[PROOF STEP]
using B.chine_char
[PROOF STATE]
proof (prove)
using this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> B.\<mu>.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> A.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine
[PROOF STEP]
using fg gh comp_cod_arr isomorphic_reflexive
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
\<lbrakk>arr ?f; cod ?f = ?b\<rbrakk> \<Longrightarrow> ?b \<cdot> ?f = ?f
ide ?f \<Longrightarrow> ?f \<cong> ?f

goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> B.\<mu>.chine \<cong> TfHgh_HfHgh.chine \<star> A.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "... \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
using A.chine_char hcomp_ide_isomorphic
[PROOF STATE]
proof (prove)
using this:
A.chine \<cong> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
\<lbrakk>ide ?f; ?g \<cong> ?h; src ?f = trg ?g\<rbrakk> \<Longrightarrow> ?f \<star> ?g \<cong> ?f \<star> ?h

goal (1 subgoal):
 1. TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TfHgh_HfHgh.chine \<star> A.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
have "HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong>
                        TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh Maps.CLS_eqI isomorphic_implies_hpar(1)
[PROOF STATE]
proof (prove)
using this:
HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> (\<lbrakk>\<lbrakk>?f\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>?g\<rbrakk>\<rbrakk>) = (?f \<cong> ?g)
?f \<cong> ?f' \<Longrightarrow> ide ?f

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>HHfgh_HfHgh.chine \<star> THfgh_HHfgh.chine \<star> TTfgh_THfgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
using fg gh isomorphic_reflexive TfTgh_TfHgh.is_map TfHgh_HfHgh.is_map TTfgh_TfTgh.is_map
                left_adjoints_compose
                Maps.comp_CLS
                  [of TfTgh_TfHgh.chine TTfgh_TfTgh.chine "TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"]
                Maps.comp_CLS
                  [of TfHgh_HfHgh.chine "TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"
                      "TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine"]
[PROOF STATE]
proof (prove)
using this:
src f = trg g
src g = trg h
ide ?f \<Longrightarrow> ?f \<cong> ?f
is_left_adjoint TfTgh_TfHgh.chine
is_left_adjoint TfHgh_HfHgh.chine
is_left_adjoint TTfgh_TfTgh.chine
\<lbrakk>is_left_adjoint ?f; is_left_adjoint ?f'; src ?f = trg ?f'\<rbrakk> \<Longrightarrow> is_left_adjoint (?f \<star> ?f')
\<lbrakk>is_left_adjoint TfTgh_TfHgh.chine; is_left_adjoint TTfgh_TfTgh.chine; TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine \<cong> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
\<lbrakk>is_left_adjoint TfHgh_HfHgh.chine; is_left_adjoint (TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine); TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine \<cong> TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk> \<Longrightarrow> \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine \<star> TfTgh_TfHgh.chine \<star> TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk>

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
have "... = Chn RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS
[PROOF STEP]
using Chn_RHS_eq CLS_chine tuple_ABC_eq_ABC'(2)
[PROOF STATE]
proof (prove)
using this:
Chn RHS = \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> tuple_ABC'
\<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = tuple_ABC
tuple_ABC = tuple_ABC'

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>TfHgh_HfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TfTgh_TfHgh.chine\<rbrakk>\<rbrakk> \<odot> \<lbrakk>\<lbrakk>TTfgh_TfTgh.chine\<rbrakk>\<rbrakk> = Chn RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Chn LHS = Chn RHS
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Chn LHS = Chn RHS

goal (1 subgoal):
 1. Chn LHS = Chn RHS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Chn LHS = Chn RHS

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Chn LHS = Chn RHS

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_subset_trans: "ta_subset \<A> \<B> \<Longrightarrow> ta_subset \<B> \<CC> \<Longrightarrow> ta_subset \<A> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ta_subset \<A> \<B>; ta_subset \<B> \<CC>\<rbrakk> \<Longrightarrow> ta_subset \<A> \<CC>
[PROOF STEP]
unfolding ta_subset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rules \<A> |\<subseteq>| rules \<B> \<and> eps \<A> |\<subseteq>| eps \<B>; rules \<B> |\<subseteq>| rules \<CC> \<and> eps \<B> |\<subseteq>| eps \<CC>\<rbrakk> \<Longrightarrow> rules \<A> |\<subseteq>| rules \<CC> \<and> eps \<A> |\<subseteq>| eps \<CC>
[PROOF STEP]
by auto


[STATEMENT]
lemma SBHWriteVolatile':
  "\<lbrakk>sb'= sb@[Write\<^sub>s\<^sub>b True a (D,f) (f \<theta>) A L R W]; ghst = (\<D>, \<O>, \<R>, \<S>); ghst' = (True, \<O>,\<R>, \<S>)\<rbrakk>
   \<Longrightarrow>
   (Write True a (D,f) A L R W# is,\<theta>, sb, m,ghst) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h
         (is,\<theta>, sb', m,ghst')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sb' = sb @ [Write\<^sub>s\<^sub>b True a (D, f) (f \<theta>) A L R W]; ghst = (\<D>, \<O>, \<R>, \<S>); ghst' = (True, \<O>, \<R>, \<S>)\<rbrakk> \<Longrightarrow> (Write True a (D, f) A L R W # is, \<theta>, sb, m, ghst) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h (is, \<theta>, sb', m, ghst')
[PROOF STEP]
by (simp add: SBHWriteVolatile)


[STATEMENT]
lemma release_and_right_distrib:
  "w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) \<longleftrightarrow> w \<Turnstile>\<^sub>n (\<phi> R\<^sub>n \<psi>\<^sub>1) and\<^sub>n (\<phi> R\<^sub>n \<psi>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile>\<^sub>n \<phi> R\<^sub>n (\<psi>\<^sub>1 and\<^sub>n \<psi>\<^sub>2) = w \<Turnstile>\<^sub>n \<phi> R\<^sub>n \<psi>\<^sub>1 and\<^sub>n \<phi> R\<^sub>n \<psi>\<^sub>2
[PROOF STEP]
by auto


[STATEMENT]
lemma INFM_nat_add:
  "(\<exists>\<^sub>\<infinity>i::nat. P i) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>i. P (i + j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>\<infinity>i. P i) = (\<exists>\<^sub>\<infinity>i. P (i + j))
[PROOF STEP]
using MOST_nat_add not_MOST not_INFM
[PROOF STATE]
proof (prove)
using this:
(\<forall>\<^sub>\<infinity>i. ?P i) = (\<forall>\<^sub>\<infinity>i. ?P (i + ?j))
(\<not> (\<forall>\<^sub>\<infinity>x. ?P x)) = (\<exists>\<^sub>\<infinity>x. \<not> ?P x)
(\<not> (\<exists>\<^sub>\<infinity>x. ?P x)) = (\<forall>\<^sub>\<infinity>x. \<not> ?P x)

goal (1 subgoal):
 1. (\<exists>\<^sub>\<infinity>i. P i) = (\<exists>\<^sub>\<infinity>i. P (i + j))
[PROOF STEP]
by blast


[STATEMENT]
lemma pos_le_neg[simp]: "Pos A \<le> Neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pos A \<le> Neg A
[PROOF STEP]
unfolding less_eq_literal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atm_of (Pos A) < atm_of (Neg A) \<or> atm_of (Pos A) \<le> atm_of (Neg A) \<and> is_neg (Pos A) \<le> is_neg (Neg A)
[PROOF STEP]
by simp


[STATEMENT]
lemma aux_even_pow2_factor: "a > 0 \<Longrightarrow> \<exists>k b. ((a::nat) = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
proof(induction  a rule: full_nat_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
proof (cases "odd n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
 2. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
odd n

goal (2 subgoals):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
 2. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
odd n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd n

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
by (metis nat_power_eq_Suc_0_iff power_Suc power_Suc0_right power_commutes)
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> odd n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
have "(\<exists>t. n = 2 * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. n = 2 * t
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> odd n

goal (1 subgoal):
 1. \<exists>t. n = 2 * t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t. n = 2 * t

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. n = 2 * t
[PROOF STEP]
obtain t where n_def:"n = 2 * t"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. n = 2 * t

goal (1 subgoal):
 1. (\<And>t. n = 2 * t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
n = 2 * t

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 2 * t
[PROOF STEP]
have "t < n"
[PROOF STATE]
proof (prove)
using this:
n = 2 * t

goal (1 subgoal):
 1. t < n
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
n = 2 * t
0 < n

goal (1 subgoal):
 1. t < n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
t < n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t < n
[PROOF STEP]
have ih:"\<exists>r s. t = 2^r * s \<and> odd s"
[PROOF STATE]
proof (prove)
using this:
t < n

goal (1 subgoal):
 1. \<exists>r s. t = 2 ^ r * s \<and> odd s
[PROOF STEP]
using 1 n_def
[PROOF STATE]
proof (prove)
using this:
t < n
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n
n = 2 * t

goal (1 subgoal):
 1. \<exists>r s. t = 2 ^ r * s \<and> odd s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>r s. t = 2 ^ r * s \<and> odd s

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r s. t = 2 ^ r * s \<and> odd s
[PROOF STEP]
have "\<exists>r s. n = 2^(Suc r) * s"
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. t = 2 ^ r * s \<and> odd s

goal (1 subgoal):
 1. \<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
using n_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. t = 2 ^ r * s \<and> odd s
n = 2 * t

goal (1 subgoal):
 1. \<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r s. n = 2 ^ Suc r * s

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. n = 2 ^ Suc r * s

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
by (metis ih n_def power_commutes semiring_normalization_rules(18)
                          semiring_normalization_rules(28))
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aux0_digit_wise_equiv:"a > 0 \<Longrightarrow> (\<exists>k. nth_bit a k = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
assume a_geq_0: "a > 0"
[PROOF STATE]
proof (state)
this:
0 < a

goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
consider (odd) "a mod 2 = 1" | (even) "a mod 2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a mod 2 = 1 \<Longrightarrow> thesis; a mod 2 = 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a mod 2 = 1 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
 2. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
case odd
[PROOF STATE]
proof (state)
this:
a mod 2 = 1

goal (2 subgoals):
 1. a mod 2 = 1 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
 2. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod 2 = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 1

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
by (metis div_by_1 nth_bit_def power_0)
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
case even
[PROOF STATE]
proof (state)
this:
a mod 2 = 0

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod 2 = 0
[PROOF STEP]
have bk_def:"\<exists>k b. (a = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 0

goal (1 subgoal):
 1. \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
using aux_even_pow2_factor a_geq_0
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 0
0 < ?a \<Longrightarrow> \<exists>k b. ?a = 2 ^ k * b \<and> odd b
0 < a

goal (1 subgoal):
 1. \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
obtain b k where bk_cond:"(a = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. (\<And>k b. a = 2 ^ k * b \<and> odd b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = 2 ^ k * b \<and> odd b
[PROOF STEP]
have "b = a div (2^k)"
[PROOF STATE]
proof (prove)
using this:
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. b = a div 2 ^ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = a div 2 ^ k

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a div 2 ^ k
[PROOF STEP]
have digi_b:"nth_bit b 0 = 1"
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
using bk_def
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
using bk_cond nth_bit_def odd_iff_mod_2_eq_one
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k
\<exists>k b. a = 2 ^ k * b \<and> odd b
a = 2 ^ k * b \<and> odd b
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
odd ?a = (?a mod (2::?'a) = (1::?'a))

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b \<exclamdown> 0 = 1

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<exclamdown> 0 = 1
[PROOF STEP]
have "nth_bit a k = (nth_bit b 0)"
[PROOF STATE]
proof (prove)
using this:
b \<exclamdown> 0 = 1

goal (1 subgoal):
 1. a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
using nth_bit_def bk_cond
[PROOF STATE]
proof (prove)
using this:
b \<exclamdown> 0 = 1
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a \<exclamdown> k = b \<exclamdown> 0

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
have "nth_bit a k = 1"
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = b \<exclamdown> 0

goal (1 subgoal):
 1. a \<exclamdown> k = 1
[PROOF STEP]
using digi_b
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = b \<exclamdown> 0
b \<exclamdown> 0 = 1

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

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<exclamdown> k = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = 1

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma meet_ord: "ad x \<le> ad y \<longleftrightarrow> ad x \<cdot> ad y = ad x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ad x \<le> ad y) = (ad x \<cdot> ad y = ad x)
[PROOF STEP]
by (metis a_d_closed a_subid_aux d1_a order.antisym mult_1_right mult_isol)


[STATEMENT]
lemma steps_Suc: "(x, y) \<in> steps rel (Suc n) \<longleftrightarrow>
  (x, y) \<in> steps rel n \<or> (x, n) \<in> steps rel n \<and> (n, y) \<in> steps rel n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> steps rel (Suc n)) = ((x, y) \<in> steps rel n \<or> (x, n) \<in> steps rel n \<and> (n, y) \<in> steps rel n)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_repeated:
  "x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. x >>= body\<cdot>x'\<cdot>y'))
  = x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. body\<cdot>x'\<cdot>y'\<cdot>x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. x >>= body\<cdot>x'\<cdot>y')) = x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. body\<cdot>x'\<cdot>y'\<cdot>x'))
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma ignores_old_varsD:
  "ignores_old_vars P \<Longrightarrow> length mdss = length mdss' \<Longrightarrow> length mdss' = length cms \<Longrightarrow>
  (map (\<lambda>x m. x m \<inter> (- range var\<^sub>C_of)) mdss) = (map (\<lambda>x m. x m \<inter> (- range var\<^sub>C_of)) mdss') \<Longrightarrow>
  P mdss = P mdss'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ignores_old_vars P; length mdss = length mdss'; length mdss' = length cms; map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss'\<rbrakk> \<Longrightarrow> P mdss = P mdss'
[PROOF STEP]
unfolding ignores_old_vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>mdss mdss'. length mdss = length mdss' \<and> length mdss' = length cms \<longrightarrow> map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss' \<longrightarrow> P mdss = P mdss'; length mdss = length mdss'; length mdss' = length cms; map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss = map (\<lambda>x m. x m \<inter> - range var\<^sub>C_of) mdss'\<rbrakk> \<Longrightarrow> P mdss = P mdss'
[PROOF STEP]
by force


[STATEMENT]
lemma G_edge_succ_a'_no_loop:
    assumes no_loop_a: "head G a \<noteq> tail G a" shows G_edge_succ_a': "edge_succ M a' = a'" (is ?t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
have *: "out_arcs G (tail G a') = {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out_arcs G (tail G a') = {a'}
[PROOF STEP]
using a_in isolated_head no_loop_a
[PROOF STATE]
proof (prove)
using this:
a \<in> arcs G
head G a \<in> H.isolated_verts
head G a \<noteq> tail G a

goal (1 subgoal):
 1. out_arcs G (tail G a') = {a'}
[PROOF STEP]
by (auto simp: H.isolated_verts_def verts_H out_arcs_def arcs_H tail_H)
[PROOF STATE]
proof (state)
this:
out_arcs G (tail G a') = {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
obtain "edge_succ M a' \<in> {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G.edge_succ_cyclic[of "tail G a'"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tail G a' \<in> verts G; out_arcs G (tail G a') \<noteq> {}\<rbrakk> \<Longrightarrow> cyclic_on (edge_succ M) (out_arcs G (tail G a'))

goal (1 subgoal):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule eq_on_cyclic_on_iff1[where x="a'"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> tail G a' \<in> verts G
 2. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> out_arcs G (tail G a') \<noteq> {}
 3. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> a' \<in> out_arcs G (tail G a')
 4. \<lbrakk>edge_succ M a' \<in> {a'} \<Longrightarrow> thesis; edge_succ M a' \<in> out_arcs G (tail G a'); (edge_succ M a' = a') = (card (out_arcs G (tail G a')) = 1)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using * a_in a_neq_a' no_loop_a
[PROOF STATE]
proof (prove)
using this:
out_arcs G (tail G a') = {a'}
a \<in> arcs G
a \<noteq> a'
head G a \<noteq> tail G a

goal (4 subgoals):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> tail G a' \<in> verts G
 2. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> out_arcs G (tail G a') \<noteq> {}
 3. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> a' \<in> out_arcs G (tail G a')
 4. \<lbrakk>edge_succ M a' \<in> {a'} \<Longrightarrow> thesis; edge_succ M a' \<in> out_arcs G (tail G a'); (edge_succ M a' = a') = (card (out_arcs G (tail G a')) = 1)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
edge_succ M a' \<in> {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
edge_succ M a' \<in> {a'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
edge_succ M a' \<in> {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edge_succ M a' = a'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj1_linear:
  fixes K V1 V2
  assumes h1: "vectorspace K V1" and h2: "vectorspace K V2"
  shows "linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
from h1 h2
[PROOF STATE]
proof (chain)
picking this:
vectorspace K V1
vectorspace K V2
[PROOF STEP]
have mod: "mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)"
[PROOF STATE]
proof (prove)
using this:
vectorspace K V1
vectorspace K V2

goal (1 subgoal):
 1. mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
by (unfold vectorspace_def, intro inj1_hom, auto)
[PROOF STATE]
proof (state)
this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)

goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
from mod h1 h2
[PROOF STATE]
proof (chain)
picking this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
vectorspace K V1
vectorspace K V2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mod_hom K V1 (direct_sum V1 V2) (inj1 V1 V2)
vectorspace K V1
vectorspace K V2

goal (1 subgoal):
 1. linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)
[PROOF STEP]
by (unfold linear_map_def vectorspace_def , auto, intro direct_sum_is_module, auto)
[PROOF STATE]
proof (state)
this:
linear_map K V1 (direct_sum V1 V2) (inj1 V1 V2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smcf_proj_components:
  shows "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>). a\<lparr>i\<rparr>)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>). f\<lparr>i\<rparr>)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>HomDom\<rparr> = (\<Prod>\<^sub>S\<^sub>M\<^sub>Ci\<in>\<^sub>\<circ>I. \<AA> i)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>HomCod\<rparr> = \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>HomDom\<rparr> = smc_prod I \<AA> &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
[PROOF STEP]
unfolding smcf_proj_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = smc_prod I \<AA> &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<AA> i
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma endofunctor_L:
    shows "endofunctor V L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. endofunctor (\<cdot>) L
[PROOF STEP]
..


[STATEMENT]
lemma poly_eval_smult:
  assumes "P \<in> Pring_set R I"
  assumes "a \<in> carrier R"
  assumes "closed_fun R g"
  shows "poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P)  =a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P) = a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P
[PROOF STEP]
using poly_eval_scalar_mult assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k \<in> carrier R; ?g \<in> UNIV \<rightarrow> carrier R; ?P \<in> carrier R [\<X>\<^bsub>?I\<^esub>]\<rbrakk> \<Longrightarrow> poly_eval R ?S ?g (poly_scalar_mult R ?k ?P) = poly_scalar_mult R ?k (poly_eval R ?S ?g ?P)
P \<in> carrier R [\<X>\<^bsub>I\<^esub>]
a \<in> carrier R
g \<in> UNIV \<rightarrow> carrier R

goal (1 subgoal):
 1. poly_eval R S g (a \<odot>\<^bsub>Pring R I\<^esub> P) = a \<odot>\<^bsub>Pring R I\<^esub> poly_eval R S g P
[PROOF STEP]
by (metis Pring_smult)


[STATEMENT]
lemma IP_to_UP_closed:
  assumes "cring R"
  assumes "P \<in> carrier (Pring R {i::'c})"
  shows "IP_to_UP i P \<in> carrier (UP R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
have "IP_to_UP i P \<in> up R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i P \<in> up R
[PROOF STEP]
apply(rule mem_upI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. IP_to_UP i P n \<in> carrier R
 2. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cring R
P \<in> carrier (Pring R {i})

goal (2 subgoals):
 1. \<And>n. IP_to_UP i P n \<in> carrier R
 2. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
apply (metis cring_def IP_to_UP_def ring.Pring_carrier_coeff')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. bound \<zero> n (IP_to_UP i P)
[PROOF STEP]
unfolding bound_def IP_to_UP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
assume A: "\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>\<^bsub>R\<^esub>"
[PROOF STATE]
proof (state)
this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>
[PROOF STEP]
have 0: "\<forall>n. \<exists>m> n. (nat_to_mset i m) \<in> monomials_of R P"
[PROOF STATE]
proof (prove)
using this:
\<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero>

goal (1 subgoal):
 1. \<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P
[PROOF STEP]
by (meson assms(1) cring_def ring.complement_of_monomials_of)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have "\<not> finite {m. (nat_to_mset i m) \<in> monomials_of R P }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
assume "finite {m. nat_to_mset i m \<in> monomials_of R P}"
[PROOF STATE]
proof (state)
this:
finite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
have "\<exists>n. \<forall>m>n.  m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}"
[PROOF STATE]
proof (prove)
using this:
finite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
by (meson finite_nat_set_iff_bounded nat_less_le order.strict_trans)
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
have "\<exists>n. \<forall>m>n.  nat_to_mset i m \<notin> monomials_of R P"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. m \<notin> {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
[PROOF STEP]
by (simp add: monomials_of_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P

goal (1 subgoal):
 1. finite {m. nat_to_mset i m \<in> monomials_of R P} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P

goal (1 subgoal):
 1. False
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
\<exists>n. \<forall>m>n. nat_to_mset i m \<notin> monomials_of R P
\<forall>n. \<exists>m>n. nat_to_mset i m \<in> monomials_of R P

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}
[PROOF STEP]
obtain S where S_def: "infinite (S::nat set) \<and> (\<forall>m \<in> S. (nat_to_mset i m) \<in> monomials_of R P)"
[PROOF STATE]
proof (prove)
using this:
infinite {m. nat_to_mset i m \<in> monomials_of R P}

goal (1 subgoal):
 1. (\<And>S. infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have "inj_on (nat_to_mset i) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (nat_to_mset i) S
[PROOF STEP]
using inj_onI[of S "nat_to_mset i"]
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> S; y \<in> S; nat_to_mset i x = nat_to_mset i y\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. inj_on (nat_to_mset i) S
[PROOF STEP]
by (meson nat_to_mset_inj)
[PROOF STATE]
proof (state)
this:
inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on (nat_to_mset i) S
[PROOF STEP]
have 1: "infinite (nat_to_mset i ` S)"
[PROOF STATE]
proof (prove)
using this:
inj_on (nat_to_mset i) S

goal (1 subgoal):
 1. infinite (nat_to_mset i ` S)
[PROOF STEP]
using S_def finite_imageD
[PROOF STATE]
proof (prove)
using this:
inj_on (nat_to_mset i) S
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)
\<lbrakk>finite (?f ` ?A); inj_on ?f ?A\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite (nat_to_mset i ` S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (nat_to_mset i ` S)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
have 2: "(nat_to_mset i ` S) \<subseteq> (monomials_of R P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
using S_def
[PROOF STATE]
proof (prove)
using this:
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)

goal (1 subgoal):
 1. nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
nat_to_mset i ` S \<subseteq> monomials_of R P

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_mset i ` S \<subseteq> monomials_of R P
[PROOF STEP]
have "infinite (monomials_of R P)"
[PROOF STATE]
proof (prove)
using this:
nat_to_mset i ` S \<subseteq> monomials_of R P

goal (1 subgoal):
 1. infinite (monomials_of R P)
[PROOF STEP]
using S_def "1" finite_subset
[PROOF STATE]
proof (prove)
using this:
nat_to_mset i ` S \<subseteq> monomials_of R P
infinite S \<and> (\<forall>m\<in>S. nat_to_mset i m \<in> monomials_of R P)
infinite (nat_to_mset i ` S)
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite (monomials_of R P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (monomials_of R P)

goal (1 subgoal):
 1. \<nexists>n. \<forall>m>n. P (nat_to_mset i m) = \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infinite (monomials_of R P)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
infinite (monomials_of R P)

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
infinite (monomials_of R P)
cring R
P \<in> carrier (Pring R {i})

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis Pring_def cring_def partial_object.select_convs(1) ring.monomials_finite)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
IP_to_UP i P \<in> up R

goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IP_to_UP i P \<in> up R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
IP_to_UP i P \<in> up R

goal (1 subgoal):
 1. IP_to_UP i P \<in> carrier (UP R)
[PROOF STEP]
by (metis (no_types, lifting) UP_def partial_object.select_convs(1))
[PROOF STATE]
proof (state)
this:
IP_to_UP i P \<in> carrier (UP R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in append_impl)
  shows
   "\<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>\<^sub>t
      \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and>  List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<rbrace>
       \<acute>p :== PROC append(\<acute>p,\<acute>q)
      \<lbrace>List \<acute>p \<acute>next (Ps@Qs) \<and> (\<forall>x. x\<notin>set Ps \<longrightarrow> \<acute>next x = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> Ps Qs. \<Gamma>\<turnstile>\<^sub>t \<lbrace>\<sigma>. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> \<acute>p :== PROC append(\<acute>p,\<acute>q) \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>\<^esup>next x)\<rbrace>
[PROOF STEP]
apply (hoare_rule HoareTotal.ProcRec1
            [where r="measure (\<lambda>(s,p). length (list \<^bsup>s\<^esup>p \<^bsup>s\<^esup>next))"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma> \<sigma>' Ps Qs. \<Gamma>,(\<Union>\<sigma>' Ps Qs. {(\<lbrace>\<sigma>'. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace> \<inter> \<lbrace>length (list \<acute>p \<acute>next) < length (list \<^bsup>\<sigma>\<^esup>p \<^bsup>\<sigma>\<^esup>next)\<rbrace>, append_'proc, \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>'\<^esup>next x)\<rbrace>, {})})\<turnstile>\<^sub>t ({\<sigma>} \<inter> \<lbrace>\<sigma>'. List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {}\<rbrace>) IF \<acute>p = Null THEN \<acute>p :== \<acute>q ELSE \<acute>p\<rightarrow>\<acute>next :== CALL append(\<acute>p\<rightarrow>\<acute>next,\<acute>q) FI \<lbrace>List \<acute>p \<acute>next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> x\<rightarrow>\<acute>next = \<^bsup>\<sigma>'\<^esup>next x)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps Qs next p q. \<lbrakk>List p next Ps; List q next Qs; set Ps \<inter> set Qs = {}\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> List q next (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> next x = next x)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>Psa. List (next p) next Psa \<and> (\<exists>Qsa. List q next Qsa \<and> set Psa \<inter> set Qsa = {} \<and> length (list (next p) next) < length (list p next) \<and> (\<forall>nexta pa. List pa nexta (Psa @ Qsa) \<and> (\<forall>x. x \<notin> set Psa \<longrightarrow> nexta x = next x) \<longrightarrow> List p (nexta(p := pa)) (Ps @ Qs) \<and> (\<forall>x. x \<notin> set Ps \<longrightarrow> (nexta(p := pa)) x = next x)))))
[PROOF STEP]
apply (fastforce  simp add: List_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma diff_solve_axiom2:
  fixes c::"'a::{heine_borel, banach}"
  shows "wp (x\<acute>=(\<lambda>s. c) & G) \<lceil>Q\<rceil> =
  \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp x\<acute>=\<lambda>t s. c & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 \<lceil>Q\<rceil> = \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>
[PROOF STEP]
apply(subst local_flow.wp_g_ode_subset[where \<phi>="(\<lambda>t s. s + t *\<^sub>R c)" and T=UNIV])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. local_flow (\<lambda>s. c) UNIV UNIV (\<lambda>t s. s + t *\<^sub>R c)
 2. \<And>s. s \<in> UNIV \<Longrightarrow> 0 \<in> Collect ((\<le>) 0) \<and> is_interval (Collect ((\<le>) 0)) \<and> Collect ((\<le>) 0) \<subseteq> UNIV
 3. \<lceil>\<lambda>s. s \<in> UNIV \<longrightarrow> (\<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c))\<rceil> = \<lceil>\<lambda>s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> Q (s + t *\<^sub>R c)\<rceil>
[PROOF STEP]
by (rule line_is_local_flow, auto)