[STATEMENT]
lemma reachNT_non_isPC_isChair:
assumes "reachNT s" and "uid \<in> UIDs"
shows
"(PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> phase s cid \<ge> disPH \<longrightarrow> pref s uid PID = Conflict) \<and>
 (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> phase s cid \<ge> disPH \<longrightarrow> pref s uid PID = Conflict)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reachNT s
uid \<in> UIDs

goal (1 subgoal):
 1. (PID \<in>\<in> paperIDs s cid \<and> isPC s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs s cid \<and> isChair s cid uid \<and> disPH \<le> phase s cid \<longrightarrow> pref s uid PID = Conflict)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs istate cid \<and> isPC istate cid uid \<and> disPH \<le> phase istate cid \<longrightarrow> pref istate uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs istate cid \<and> isChair istate cid uid \<and> disPH \<le> phase istate cid \<longrightarrow> pref istate uid PID = Conflict)
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict)
[PROOF STEP]
apply (auto simp: istate_def)[]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict)
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
 2. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
subgoal for trn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isPC (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
apply(cases trn, auto simp: T.simps reachNT_reach)[]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
.
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>trn. \<lbrakk>reachNT (srcOf trn); uid \<in> UIDs \<Longrightarrow> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isPC (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict) \<and> (PID \<in>\<in> paperIDs (srcOf trn) cid \<and> isChair (srcOf trn) cid uid \<and> disPH \<le> phase (srcOf trn) cid \<longrightarrow> pref (srcOf trn) uid PID = Conflict); validTrans trn; \<not> T trn; uid \<in> UIDs\<rbrakk> \<Longrightarrow> PID \<in>\<in> paperIDs (tgtOf trn) cid \<and> isChair (tgtOf trn) cid uid \<and> disPH \<le> phase (tgtOf trn) cid \<longrightarrow> pref (tgtOf trn) uid PID = Conflict
[PROOF STEP]
by (metis T.elims(3) isChair_isPC reachNT_reach reach.Step tgtOf_simps)


[STATEMENT]
lemma tensor_tensor:
    assumes "arr f" and "arr g" and "arr h"
    shows "(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
    and "f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) &&& f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
 2. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
show "(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
using assms Diag_Diagonalize TensorDiag_preserves_Diag Diag_implies_Arr
                \<F>C.COD_mkarr \<F>C.DOM_mkarr \<F>C.strict_arr_char tensor_char
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Diag (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Dom (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Cod (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u
Diag ?t \<Longrightarrow> Arr ?t
Arr ?t \<Longrightarrow> \<F>C.COD (\<F>C.mkarr ?t) = Cod ?t
Arr ?t \<Longrightarrow> \<F>C.DOM (\<F>C.mkarr ?t) = Dom ?t
arr ?f = (\<F>C.arr ?f \<and> Diag (\<F>C.DOM ?f) \<and> Diag (\<F>C.COD ?f))
\<lbrakk>arr ?f; arr ?g\<rbrakk> \<Longrightarrow> ?f \<otimes>\<^sub>S ?g = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep ?f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep ?g\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have
          "... = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor>
                           \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
using assms arr_char\<^sub>S\<^sub>b\<^sub>C tensor_char
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
arr ?f = (\<F>C.arr ?f \<and> (\<F>C.ide (\<F>C.dom ?f) \<and> Diag (\<F>C.DOM (\<F>C.dom ?f))) \<and> \<F>C.ide (\<F>C.cod ?f) \<and> Diag (\<F>C.DOM (\<F>C.cod ?f)))
\<lbrakk>arr ?f; arr ?g\<rbrakk> \<Longrightarrow> ?f \<otimes>\<^sub>S ?g = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep ?f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep ?g\<^bold>\<rfloor>)

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (f \<otimes>\<^sub>S g)\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
using assms \<F>C.rep_mkarr TensorDiag_in_Hom Diag_Diagonalize
                TensorDiag_preserves_Diag arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?f \<Longrightarrow> \<F>C.rep (\<F>C.mkarr ?f) = \<^bold>\<parallel>?f\<^bold>\<parallel>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u \<in> Hom (Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u) (Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u)
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Diag (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Dom (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Cod (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u
arr ?f = (\<F>C.arr ?f \<and> (\<F>C.ide (\<F>C.dom ?f) \<and> Diag (\<F>C.DOM (\<F>C.dom ?f))) \<and> \<F>C.ide (\<F>C.cod ?f) \<and> Diag (\<F>C.DOM (\<F>C.cod ?f)))

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>))\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
using assms Diag_Diagonalize TensorDiag_preserves_Diag TensorDiag_assoc arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Diag (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Dom (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Cod (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u
\<lbrakk>Diag ?t; Diag ?u; Diag ?v\<rbrakk> \<Longrightarrow> (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?v = ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?v
arr ?f = (\<F>C.arr ?f \<and> (\<F>C.ide (\<F>C.dom ?f) \<and> Diag (\<F>C.DOM (\<F>C.dom ?f))) \<and> \<F>C.ide (\<F>C.cod ?f) \<and> Diag (\<F>C.DOM (\<F>C.cod ?f)))

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. (f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f \<otimes>\<^sub>S g) \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
show "f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>)
[PROOF STEP]
using assms Diag_Diagonalize TensorDiag_preserves_Diag arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Diag (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Dom (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Cod (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u
arr ?f = (\<F>C.arr ?f \<and> (\<F>C.ide (\<F>C.dom ?f) \<and> Diag (\<F>C.DOM (\<F>C.dom ?f))) \<and> \<F>C.ide (\<F>C.cod ?f) \<and> Diag (\<F>C.DOM (\<F>C.cod ?f)))

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor>
                                   (\<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>)
[PROOF STEP]
using assms \<F>C.rep_mkarr TensorDiag_in_Hom Diag_Diagonalize arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?f \<Longrightarrow> \<F>C.rep (\<F>C.mkarr ?f) = \<^bold>\<parallel>?f\<^bold>\<parallel>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u \<in> Hom (Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u) (Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u)
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
arr ?f = (\<F>C.arr ?f \<and> (\<F>C.ide (\<F>C.dom ?f) \<and> Diag (\<F>C.DOM (\<F>C.dom ?f))) \<and> \<F>C.ide (\<F>C.cod ?f) \<and> Diag (\<F>C.DOM (\<F>C.cod ?f)))

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>)
[PROOF STEP]
using assms tensor_char
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
\<lbrakk>arr ?f; arr ?g\<rbrakk> \<Longrightarrow> ?f \<otimes>\<^sub>S ?g = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep ?f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep ?g\<^bold>\<rfloor>)

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>))\<^bold>\<rfloor>) = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>)

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
have "... = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>) = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h
[PROOF STEP]
using assms Diag_Diagonalize TensorDiag_preserves_Diag Diag_implies_Arr
                \<F>C.COD_mkarr \<F>C.DOM_mkarr \<F>C.strict_arr_char tensor_char
[PROOF STATE]
proof (prove)
using this:
arr f
arr g
arr h
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Diag (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Dom (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Dom ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Dom ?u
\<lbrakk>Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Cod (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u) = Cod ?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> Cod ?u
Diag ?t \<Longrightarrow> Arr ?t
Arr ?t \<Longrightarrow> \<F>C.COD (\<F>C.mkarr ?t) = Cod ?t
Arr ?t \<Longrightarrow> \<F>C.DOM (\<F>C.mkarr ?t) = Dom ?t
arr ?f = (\<F>C.arr ?f \<and> Diag (\<F>C.DOM ?f) \<and> Diag (\<F>C.COD ?f))
\<lbrakk>arr ?f; arr ?g\<rbrakk> \<Longrightarrow> ?f \<otimes>\<^sub>S ?g = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep ?f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep ?g\<^bold>\<rfloor>)

goal (1 subgoal):
 1. \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>) = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep (g \<otimes>\<^sub>S h)\<^bold>\<rfloor>) = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>) = f \<otimes>\<^sub>S g \<otimes>\<^sub>S h

goal (1 subgoal):
 1. f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f \<otimes>\<^sub>S g \<otimes>\<^sub>S h = \<F>C.mkarr (\<^bold>\<lfloor>\<F>C.rep f\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep g\<^bold>\<rfloor> \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> \<^bold>\<lfloor>\<F>C.rep h\<^bold>\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_generalised_output_of_does_not_subsume:
  "is_generalised_output_of t' t r p \<Longrightarrow>
   p < length (Outputs t) \<Longrightarrow>
   nth (Outputs t) p = L v \<Longrightarrow>
   c $ r \<noteq> Some v \<Longrightarrow>
   \<exists>i. can_take_transition t i c \<Longrightarrow>
   \<not>subsumes t' c t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; \<exists>i. can_take_transition t i c\<rbrakk> \<Longrightarrow> \<not> subsumes t' c t
[PROOF STEP]
apply (rule bad_outputs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; \<exists>i. can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>i. can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply (rule_tac x=i in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> can_take_transition t i c \<and> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> evaluate_outputs t i c \<noteq> evaluate_outputs t' i c
[PROOF STEP]
apply (rule lists_neq_if)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> \<exists>ia. evaluate_outputs t i c ! ia \<noteq> evaluate_outputs t' i c ! ia
[PROOF STEP]
apply (rule_tac x=p in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_generalised_output_of t' t r p; p < length (Outputs t); Outputs t ! p = L v; c $ r \<noteq> Some v; can_take_transition t i c\<rbrakk> \<Longrightarrow> evaluate_outputs t i c ! p \<noteq> evaluate_outputs t' i c ! p
[PROOF STEP]
by (simp add: is_generalised_output_of_def generalise_output_def apply_outputs_nth join_ir_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rg_fo_inv[simp]: "residualGraph c (flow_of_cf cf) = cf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
using rg_is_cf
[PROOF STATE]
proof (prove)
using this:
f.cf = cf

goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
cf_of (flow_of_cf cf) = cf

goal (1 subgoal):
 1. cf_of (flow_of_cf cf) = cf
[PROOF STEP]
.


[STATEMENT]
lemma cong_dec:
  shows "Cong A B C D \<or> \<not> Cong A B C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cong A B C D \<or> \<not> Cong A B C D
[PROOF STEP]
by simp


[STATEMENT]
lemma le1221:
  shows "A B Le B A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A B Le B A
[PROOF STEP]
by (simp add: cong__le cong_pseudo_reflexivity)


[STATEMENT]
lemma bet2_lt_le__lt:
  assumes "Bet a Po b" and
    "Bet A PO B" and
    "Cong Po a PO A" and
    "Po b Lt PO B"
  shows "a b Lt A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a b Lt A B
[PROOF STEP]
by (smt Lt_def Tarski_neutral_dimensionless.l4_3_1 Tarski_neutral_dimensionless_axioms assms(1) assms(2) assms(3) assms(4) bet2_le2__le cong__le not_cong_2143)


[STATEMENT]
lemma coplanar_perm_18:
  assumes "Coplanar A B C D"
  shows "Coplanar D A B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
obtain X where P1: "(Col A B X \<and> Col C D X) \<or> (Col A C X \<and> Col B D X) \<or> (Col A D X \<and> Col B C X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Coplanar_def assms
[PROOF STATE]
proof (prove)
using this:
Coplanar ?A ?B ?C ?D \<equiv> \<exists>X. Col ?A ?B X \<and> Col ?C ?D X \<or> Col ?A ?C X \<and> Col ?B ?D X \<or> Col ?A ?D X \<and> Col ?B ?C X
Coplanar A B C D

goal (1 subgoal):
 1. (\<And>X. Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X

goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X

goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
using Coplanar_def col_permutation_4
[PROOF STATE]
proof (prove)
using this:
Col A B X \<and> Col C D X \<or> Col A C X \<and> Col B D X \<or> Col A D X \<and> Col B C X
Coplanar ?A ?B ?C ?D \<equiv> \<exists>X. Col ?A ?B X \<and> Col ?C ?D X \<or> Col ?A ?C X \<and> Col ?B ?D X \<or> Col ?A ?D X \<and> Col ?B ?C X
Col ?A ?B ?C \<Longrightarrow> Col ?B ?A ?C

goal (1 subgoal):
 1. Coplanar D A B C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Coplanar D A B C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l9_17:
  assumes "P Q OS A C" and
    "Bet A B C"
  shows "P Q OS A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P Q OS A B
 2. \<not> ?P \<Longrightarrow> P Q OS A B
[PROOF STEP]
assume "A = C"
[PROOF STATE]
proof (state)
this:
A = C

goal (2 subgoals):
 1. ?P \<Longrightarrow> P Q OS A B
 2. \<not> ?P \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = C

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using assms(1) assms(2) between_identity
[PROOF STATE]
proof (prove)
using this:
A = C
P Q OS A C
Bet A B C
\<forall>a b. Bet a b a \<longrightarrow> a = b

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q OS A B

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
assume P1: "\<not> A = C"
[PROOF STATE]
proof (state)
this:
A \<noteq> C

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain D where P2: "P Q TS A D \<and> P Q TS C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D. P Q TS A D \<and> P Q TS C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using OS_def assms(1)
[PROOF STATE]
proof (prove)
using this:
?A ?B OS ?P ?Q \<equiv> \<exists>R. ?A ?B TS ?P R \<and> ?A ?B TS ?Q R
P Q OS A C

goal (1 subgoal):
 1. (\<And>D. P Q TS A D \<and> P Q TS C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q TS A D \<and> P Q TS C D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P Q TS A D \<and> P Q TS C D
[PROOF STEP]
have P3: "P \<noteq> Q"
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D

goal (1 subgoal):
 1. P \<noteq> Q
[PROOF STEP]
using ts_distincts
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<Longrightarrow> ?A \<noteq> ?B \<and> ?A \<noteq> ?P \<and> ?A \<noteq> ?Q \<and> ?B \<noteq> ?P \<and> ?B \<noteq> ?Q \<and> ?P \<noteq> ?Q

goal (1 subgoal):
 1. P \<noteq> Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<noteq> Q

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain X where P4: "Col X P Q \<and> Bet A X D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X. Col X P Q \<and> Bet A X D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. (\<And>X. Col X P Q \<and> Bet A X D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col X P Q \<and> Bet A X D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain Y where P5: "Col Y P Q \<and> Bet C Y D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. Col Y P Q \<and> Bet C Y D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. (\<And>Y. Col Y P Q \<and> Bet C Y D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col Y P Q \<and> Bet C Y D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
obtain T where P6: "Bet B T D \<and> Bet X T Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using P4 P5 assms(2) l3_17
[PROOF STATE]
proof (prove)
using this:
Col X P Q \<and> Bet A X D
Col Y P Q \<and> Bet C Y D
Bet A B C
\<lbrakk>Bet ?A ?B ?C; Bet ?A' ?B' ?C; Bet ?A ?P ?A'\<rbrakk> \<Longrightarrow> \<exists>Q. Bet ?P Q ?C \<and> Bet ?B Q ?B'

goal (1 subgoal):
 1. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet B T D \<and> Bet X T Y

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
have P7: "P Q TS A D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q TS A D
[PROOF STEP]
by (simp add: P2)
[PROOF STATE]
proof (state)
this:
P Q TS A D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
have "P Q TS B D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
have Q1: "\<not> Col B P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Col B P Q
[PROOF STEP]
using assms(1) assms(2) one_side_chara
[PROOF STATE]
proof (prove)
using this:
P Q OS A C
Bet A B C
?P ?Q OS ?A ?B \<Longrightarrow> \<forall>X. Col X ?P ?Q \<longrightarrow> \<not> Bet ?A X ?B

goal (1 subgoal):
 1. \<not> Col B P Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Col B P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
have Q2: "\<not> Col D P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Col D P Q
[PROOF STEP]
using P2 TS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS A D \<and> P Q TS C D
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. \<not> Col D P Q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> Col D P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
obtain T0 where "Col T0 P Q \<and> Bet B T0 D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume a1: "\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
Col ?T0.0 P Q \<and> Bet B ?T0.0 D \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain pp :: 'p where
        f2: "Bet B pp D \<and> Bet X pp Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pp. Bet B pp D \<and> Bet X pp Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<And>thesis. (\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>T. Bet B T D \<and> Bet X T Y \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>pp. Bet B pp D \<and> Bet X pp Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Bet B pp D \<and> Bet X pp Y

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "Col P Q Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Col P Q Y
[PROOF STEP]
using Col_def P5
[PROOF STATE]
proof (prove)
using this:
Col ?A ?B ?C \<equiv> Bet ?A ?B ?C \<or> Bet ?B ?C ?A \<or> Bet ?C ?A ?B
Col Y P Q \<and> Bet C Y D

goal (1 subgoal):
 1. Col P Q Y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col P Q Y

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col P Q Y
[PROOF STEP]
have "Y = X \<or> Col P Q pp"
[PROOF STATE]
proof (prove)
using this:
Col P Q Y

goal (1 subgoal):
 1. Y = X \<or> Col P Q pp
[PROOF STEP]
using f2 Col_def P4 colx
[PROOF STATE]
proof (prove)
using this:
Col P Q Y
Bet B pp D \<and> Bet X pp Y
Col ?A ?B ?C \<equiv> Bet ?A ?B ?C \<or> Bet ?B ?C ?A \<or> Bet ?C ?A ?B
Col X P Q \<and> Bet A X D
\<lbrakk>?A \<noteq> ?B; Col ?X ?Y ?A; Col ?X ?Y ?B; Col ?A ?B ?C\<rbrakk> \<Longrightarrow> Col ?X ?Y ?C

goal (1 subgoal):
 1. Y = X \<or> Col P Q pp
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y = X \<or> Col P Q pp

goal (1 subgoal):
 1. (\<And>T0. Col T0 P Q \<and> Bet B T0 D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y = X \<or> Col P Q pp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Y = X \<or> Col P Q pp

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using f2 a1
[PROOF STATE]
proof (prove)
using this:
Y = X \<or> Col P Q pp
Bet B pp D \<and> Bet X pp Y
Col ?T0.0 P Q \<and> Bet B ?T0.0 D \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis BetSEq BetS_def Col_def P4)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Col T0 P Q \<and> Bet B T0 D

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col T0 P Q \<and> Bet B T0 D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
using Q1 Q2
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D
\<not> Col B P Q
\<not> Col D P Q

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
using TS_def
[PROOF STATE]
proof (prove)
using this:
Col T0 P Q \<and> Bet B T0 D
\<not> Col B P Q
\<not> Col D P Q
?A ?B TS ?P ?Q \<equiv> \<not> Col ?P ?A ?B \<and> \<not> Col ?Q ?A ?B \<and> (\<exists>T. Col T ?A ?B \<and> Bet ?P T ?Q)

goal (1 subgoal):
 1. P Q TS B D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q TS B D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P Q TS B D

goal (1 subgoal):
 1. A \<noteq> C \<Longrightarrow> P Q OS A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P Q TS B D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P Q TS B D

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using P7
[PROOF STATE]
proof (prove)
using this:
P Q TS B D
P Q TS A D

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
using OS_def
[PROOF STATE]
proof (prove)
using this:
P Q TS B D
P Q TS A D
?A ?B OS ?P ?Q \<equiv> \<exists>R. ?A ?B TS ?P R \<and> ?A ?B TS ?Q R

goal (1 subgoal):
 1. P Q OS A B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P Q OS A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cop_not_par_other_side:
  assumes "C \<noteq> D" and
    "Col A B I" and
    "Col C D I" and
    "\<not> Col A B C" and
    "\<not> Col A B P" and
    "Coplanar A B C P"
  shows "\<exists> Q. Col C D Q \<and> A B TS P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
obtain X Y where P1:"Col C D X \<and> Col C D Y \<and> A B TS X Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X Y. Col C D X \<and> Col C D Y \<and> A B TS X Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1) assms(2) assms(3) assms(4) not_par_two_sides
[PROOF STATE]
proof (prove)
using this:
C \<noteq> D
Col A B I
Col C D I
\<not> Col A B C
\<lbrakk>?C \<noteq> ?D; Col ?A ?B ?I; Col ?C ?D ?I; \<not> Col ?A ?B ?C\<rbrakk> \<Longrightarrow> \<exists>X Y. Col ?C ?D X \<and> Col ?C ?D Y \<and> ?A ?B TS X Y

goal (1 subgoal):
 1. (\<And>X Y. Col C D X \<and> Col C D Y \<and> A B TS X Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col C D X \<and> Col C D Y \<and> A B TS X Y

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col C D X \<and> Col C D Y \<and> A B TS X Y
[PROOF STEP]
have "Coplanar C A B X"
[PROOF STATE]
proof (prove)
using this:
Col C D X \<and> Col C D Y \<and> A B TS X Y

goal (1 subgoal):
 1. Coplanar C A B X
[PROOF STEP]
using Coplanar_def assms(1) assms(2) assms(3) col_transitivity_1
[PROOF STATE]
proof (prove)
using this:
Col C D X \<and> Col C D Y \<and> A B TS X Y
Coplanar ?A ?B ?C ?D \<equiv> \<exists>X. Col ?A ?B X \<and> Col ?C ?D X \<or> Col ?A ?C X \<and> Col ?B ?D X \<or> Col ?A ?D X \<and> Col ?B ?C X
C \<noteq> D
Col A B I
Col C D I
\<lbrakk>?P \<noteq> ?Q; Col ?P ?Q ?A; Col ?P ?Q ?B\<rbrakk> \<Longrightarrow> Col ?P ?A ?B

goal (1 subgoal):
 1. Coplanar C A B X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Coplanar C A B X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Coplanar C A B X
[PROOF STEP]
have "Coplanar A B P X"
[PROOF STATE]
proof (prove)
using this:
Coplanar C A B X

goal (1 subgoal):
 1. Coplanar A B P X
[PROOF STEP]
using assms(4) assms(6) col_permutation_3 coplanar_trans_1 ncoplanar_perm_2 ncoplanar_perm_6
[PROOF STATE]
proof (prove)
using this:
Coplanar C A B X
\<not> Col A B C
Coplanar A B C P
Col ?A ?B ?C \<Longrightarrow> Col ?C ?B ?A
\<lbrakk>\<not> Col ?P ?Q ?R; Coplanar ?P ?Q ?R ?A; Coplanar ?P ?Q ?R ?B\<rbrakk> \<Longrightarrow> Coplanar ?Q ?R ?A ?B
\<not> Coplanar ?A ?B ?C ?D \<Longrightarrow> \<not> Coplanar ?A ?C ?B ?D
\<not> Coplanar ?A ?B ?C ?D \<Longrightarrow> \<not> Coplanar ?B ?A ?C ?D

goal (1 subgoal):
 1. Coplanar A B P X
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Coplanar A B P X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Coplanar A B P X
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Coplanar A B P X

goal (1 subgoal):
 1. \<exists>Q. Col C D Q \<and> A B TS P Q
[PROOF STEP]
by (meson P1 l9_8_2 TS_def assms(5) cop_nts__os not_col_permutation_2 one_side_symmetry)
[PROOF STATE]
proof (state)
this:
\<exists>Q. Col C D Q \<and> A B TS P Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma par_neq1:
  assumes "A B Par C D"
  shows "A \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> B
[PROOF STEP]
using Par_def assms par_strict_neq1
[PROOF STATE]
proof (prove)
using this:
?A ?B Par ?C ?D \<equiv> ?A ?B ParStrict ?C ?D \<or> ?A \<noteq> ?B \<and> ?C \<noteq> ?D \<and> Col ?A ?C ?D \<and> Col ?B ?C ?D
A B Par C D
?A ?B ParStrict ?C ?D \<Longrightarrow> ?A \<noteq> ?B

goal (1 subgoal):
 1. A \<noteq> B
[PROOF STEP]
by blast


[STATEMENT]
lemma col_cop_perp2__pars_bis:
  assumes "\<not> Col A B P" and
    "Col C D P" and
    "Coplanar A B C D" and
    "P Perp2 A B C D"
  shows "A B ParStrict C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
obtain X Y where P1: "Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X Y. Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Perp2_def assms(4)
[PROOF STATE]
proof (prove)
using this:
?P Perp2 ?A ?B ?C ?D \<equiv> \<exists>X Y. Col ?P X Y \<and> X Y Perp ?A ?B \<and> X Y Perp ?C ?D
P Perp2 A B C D

goal (1 subgoal):
 1. (\<And>X Y. Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D
[PROOF STEP]
have "Col X Y P"
[PROOF STATE]
proof (prove)
using this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D

goal (1 subgoal):
 1. Col X Y P
[PROOF STEP]
using Col_perm
[PROOF STATE]
proof (prove)
using this:
Col P X Y \<and> X Y Perp A B \<and> X Y Perp C D
Col ?A ?B ?C \<Longrightarrow> Col ?A ?B ?C \<and> Col ?A ?C ?B \<and> Col ?B ?A ?C \<and> Col ?B ?C ?A \<and> Col ?C ?A ?B \<and> Col ?C ?B ?A

goal (1 subgoal):
 1. Col X Y P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Col X Y P

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
obtain Q where "X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>Col X Y P\<close> diff_col_ex3
[PROOF STATE]
proof (prove)
using this:
Col X Y P
Col ?A ?B ?C \<Longrightarrow> \<exists>D. ?A \<noteq> D \<and> ?B \<noteq> D \<and> ?C \<noteq> D \<and> Col ?A ?B D

goal (1 subgoal):
 1. (\<And>Q. X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<noteq> Q \<and> Y \<noteq> Q \<and> P \<noteq> Q \<and> Col X Y Q

goal (1 subgoal):
 1. A B ParStrict C D
[PROOF STEP]
by (smt P1 Perp_perm assms(1) assms(2) assms(3) col_cop_perp2_pars col_permutation_1 col_transitivity_2 not_col_distincts perp_col4 perp_distinct)
[PROOF STATE]
proof (state)
this:
A B ParStrict C D

goal:
No subgoals!
[PROOF STEP]
qed