[STATEMENT]
lemma denote_scale:
  fixes c :: real
  assumes "c\<ge>0"
  shows "well_com S \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow>
         trace (c  \<cdot>\<^sub>m \<rho>) \<le> 1 \<Longrightarrow> denote S (c  \<cdot>\<^sub>m \<rho>) = c  \<cdot>\<^sub>m denote S \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote S (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote S \<rho>
[PROOF STEP]
proof (induction arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<rho>. \<lbrakk>well_com SKIP; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote SKIP (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote SKIP \<rho>
 2. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 4. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 5. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
case SKIP
[PROOF STATE]
proof (state)
this:
well_com SKIP
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (5 subgoals):
 1. \<And>\<rho>. \<lbrakk>well_com SKIP; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote SKIP (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote SKIP \<rho>
 2. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 4. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 5. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com SKIP
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote SKIP (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote SKIP \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote SKIP (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote SKIP \<rho>

goal (4 subgoals):
 1. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 3. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 4. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 3. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 4. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
case (Utrans x)
[PROOF STATE]
proof (state)
this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (4 subgoals):
 1. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 3. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 4. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>
[PROOF STEP]
unfolding denote.simps
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. x * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint x = complex_of_real c \<cdot>\<^sub>m (x * \<rho> * adjoint x)
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_mat d d
[PROOF STEP]
using Utrans
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. x \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (Utrans x) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Utrans x) \<rho>

goal (3 subgoals):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 2. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 2. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
case (Seq x1 x2a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (3 subgoals):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
 2. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
have cd: "denote x1 (c \<cdot>\<^sub>m \<rho>) = c \<cdot>\<^sub>m denote x1 \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>
[PROOF STEP]
using Seq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
have x1: "denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>
[PROOF STEP]
using denote_positive_trace_dim Seq denote_partial_density_operator
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
\<lbrakk>well_com ?S; partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> partial_density_operator (denote ?S ?\<rho>)

goal (1 subgoal):
 1. denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
have "trace (c \<cdot>\<^sub>m denote x1 \<rho>) = c * trace (denote x1 \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c * trace (denote x1 \<rho>)
[PROOF STEP]
using trace_smult x1
[PROOF STATE]
proof (prove)
using this:
?A \<in> carrier_mat ?n ?n \<Longrightarrow> trace (?c \<cdot>\<^sub>m ?A) = ?c * trace ?A
denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c * trace (denote x1 \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c * trace (denote x1 \<rho>)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c * trace (denote x1 \<rho>)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
have "\<dots> \<le> c * trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real c * trace (denote x1 \<rho>) \<le> complex_of_real c * trace \<rho>
[PROOF STEP]
using x1 assms
[PROOF STATE]
proof (prove)
using this:
denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>
0 \<le> c

goal (1 subgoal):
 1. complex_of_real c * trace (denote x1 \<rho>) \<le> complex_of_real c * trace \<rho>
[PROOF STEP]
by (metis Seq.prems cd denote_positive_trace_dim partial_density_operator_def positive_scale smult_carrier_mat trace_smult well_com.simps(3))
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace (denote x1 \<rho>) \<le> complex_of_real c * trace \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace (denote x1 \<rho>) \<le> complex_of_real c * trace \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
have "\<dots> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real c * trace \<rho> \<le> 1
[PROOF STEP]
using Seq(6) trace_smult Seq(4)
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
?A \<in> carrier_mat ?n ?n \<Longrightarrow> trace (?c \<cdot>\<^sub>m ?A) = ?c * trace ?A
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. complex_of_real c * trace \<rho> \<le> 1
[PROOF STEP]
by (simp add: trace_smult)
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace \<rho> \<le> 1

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1
[PROOF STEP]
have "trace (c \<cdot>\<^sub>m denote x1 \<rho>) \<le>1"
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1
[PROOF STEP]
have "denote x2a (c \<cdot>\<^sub>m denote x1 \<rho>) = c \<cdot>\<^sub>m denote x2a ( denote x1 \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1

goal (1 subgoal):
 1. denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)
[PROOF STEP]
using x1 Seq
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) \<le> 1
denote x1 \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho>
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 ?\<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)

goal (1 subgoal):
 1. denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
using denote.simps(4) cd
[PROOF STATE]
proof (prove)
using this:
denote x2a (complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a (denote x1 \<rho>)
denote (Measure ?n ?M ?S) ?\<rho> = denote_measure ?n ?M (map denote ?S) ?\<rho>
denote x1 (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x1 \<rho>

goal (1 subgoal):
 1. denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
denote (x1;; x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (x1;; x2a) \<rho>

goal (2 subgoals):
 1. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
case (Measure x1 x2a x3a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (2 subgoals):
 1. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3a \<rho>; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3) \<rho>
 2. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have ptc: "\<And>x3aa \<rho>. x3aa \<in> set x3a \<Longrightarrow> well_com x3aa \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
      \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim Measure
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. \<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3aa \<in> set x3a; well_com ?x3aa; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?x3aa ?\<rho>) \<and> trace (denote ?x3aa ?\<rho>) \<le> trace ?\<rho> \<and> denote ?x3aa ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have cad: "x2a k * (c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k) = c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))"
      if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k) = complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x2a k \<in> carrier_mat d d
 2. \<rho> \<in> carrier_mat d d
[PROOF STEP]
using well_com.simps Measure measurement_dim k
[PROOF STATE]
proof (prove)
using this:
well_com SKIP = True
well_com (Utrans ?U) = (?U \<in> carrier_mat d d \<and> unitary ?U)
well_com (?S1.0;; ?S2.0) = (well_com ?S1.0 \<and> well_com ?S2.0)
well_com (Measure ?n ?M ?S) = (measurement d ?n ?M \<and> length ?S = ?n \<and> list_all well_com ?S)
well_com (While ?M ?S) = (measurement d 2 ?M \<and> well_com ?S)
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d
k < x1

goal (2 subgoals):
 1. x2a k \<in> carrier_mat d d
 2. \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k) = complex_of_real c \<cdot>\<^sub>m (x2a ?k * \<rho> * adjoint (x2a ?k))

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have "\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
using Measure(2) measurement_dim Measure(3)
[PROOF STATE]
proof (prove)
using this:
well_com (Measure x1 x2a x3a)
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have lea: "\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat Measure(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement ?d ?n ?f; ?j < ?n\<rbrakk> \<Longrightarrow> adjoint (?f ?j) * ?f ?j \<le>\<^sub>L 1\<^sub>m ?d
well_com (Measure x1 x2a x3a)

goal (1 subgoal):
 1. \<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
have pdox: "\<forall> k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d

goal (1 subgoal):
 1. \<forall>k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using pdo_close_under_measurement Measure(2,3,4) measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?\<rho> \<in> carrier_mat ?n ?n; partial_density_operator ?\<rho>; adjoint ?M * ?M \<le>\<^sub>L 1\<^sub>m ?n\<rbrakk> \<Longrightarrow> partial_density_operator (?M * ?\<rho> * adjoint ?M)
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<forall>k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
by (meson state_sig.well_com.simps(4))
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have x2aa:"\<forall> k < x1. (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
using Measure(2,3) measurement_dim
[PROOF STATE]
proof (prove)
using this:
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have dimm: "(\<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
using map_denote_positive_trace_dim Measure(2,3,4) ptc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com (Measure ?x1.0 ?x2a ?x3a); ?x4.0 \<in> carrier_mat d d; partial_density_operator ?x4.0; \<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set ?x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x3aa \<rho>) \<and> trace (denote x3aa \<rho>) \<le> trace \<rho> \<and> denote x3aa \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> \<forall>k<?x1.0. positive ((map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k))) \<and> (map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k)) \<in> carrier_mat d d \<and> trace ((map denote ?x3a ! k) (?x2a k * ?x4.0 * adjoint (?x2a k))) \<le> trace (?x2a k * ?x4.0 * adjoint (?x2a k))
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>?x3aa \<in> set x3a; well_com ?x3aa; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?x3aa ?\<rho>) \<and> trace (denote ?x3aa ?\<rho>) \<le> trace ?\<rho> \<and> denote ?x3aa ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d
[PROOF STEP]
have dimcm: "(\<And>k. k < x1 \<Longrightarrow> c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
using smult_carrier_mat
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> ?k \<cdot>\<^sub>m ?A \<in> carrier_mat ?nr ?nc

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have tra: "\<forall> k < x1. trace ((x2a k * \<rho> * adjoint (x2a k))) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<x1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
[PROOF STEP]
using trace_decrease_mul_adj Measure lea measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d; ?x \<in> carrier_mat d d; adjoint ?x * ?x \<le>\<^sub>L 1\<^sub>m d\<rbrakk> \<Longrightarrow> trace (?x * ?\<rho> * adjoint ?x) \<le> trace ?\<rho>
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
\<forall>k<x1. adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<forall>k<x1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k<x1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have tra1: "trace (c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1" if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
have trle: "trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
[PROOF STEP]
using tra k
[PROOF STATE]
proof (prove)
using this:
\<forall>k<x1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
k < x1

goal (1 subgoal):
 1. trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
have "trace (c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = c * trace ((x2a k * \<rho> * adjoint (x2a k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using trace_smult x2aa k
[PROOF STATE]
proof (prove)
using this:
?A \<in> carrier_mat ?n ?n \<Longrightarrow> trace (?c \<cdot>\<^sub>m ?A) = ?c * trace ?A
\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
k < x1

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
have "\<dots> \<le> c * trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k)) \<le> complex_of_real c * trace \<rho>
[PROOF STEP]
using trle assms mulfact
[PROOF STATE]
proof (prove)
using this:
trace (x2a k * \<rho> * adjoint (x2a k)) \<le> trace \<rho>
0 \<le> c
\<lbrakk>0 \<le> ?c; ?a \<le> ?b\<rbrakk> \<Longrightarrow> complex_of_real ?c * ?a \<le> complex_of_real ?c * ?b

goal (1 subgoal):
 1. complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k)) \<le> complex_of_real c * trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k)) \<le> complex_of_real c * trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace (x2a k * \<rho> * adjoint (x2a k)) \<le> complex_of_real c * trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
have "\<dots> \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real c * trace \<rho> \<le> 1
[PROOF STEP]
using Measure(3,5) trace_smult
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
?A \<in> carrier_mat ?n ?n \<Longrightarrow> trace (?c \<cdot>\<^sub>m ?A) = ?c * trace ?A

goal (1 subgoal):
 1. complex_of_real c * trace \<rho> \<le> 1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
complex_of_real c * trace \<rho> \<le> 1

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> trace (complex_of_real c \<cdot>\<^sub>m (x2a ?k * \<rho> * adjoint (x2a ?k))) \<le> 1

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
have "(map denote x3a ! k) (x2a k * (c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))
        = c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))" if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
have "denote (x3a ! k) (x2a k * (c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = denote (x3a ! k) (c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k)))
[PROOF STEP]
using cad k
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k) = complex_of_real c \<cdot>\<^sub>m (x2a ?k * \<rho> * adjoint (x2a ?k))
k < x1

goal (1 subgoal):
 1. denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k)))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k)))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
have "\<dots> = c \<cdot>\<^sub>m denote (x3a ! k) ( (x2a k * \<rho> * adjoint (x2a k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using Measure(1,2) pdox x2aa tra1 k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<forall>k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))
\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> trace (complex_of_real c \<cdot>\<^sub>m (x2a ?k * \<rho> * adjoint (x2a ?k))) \<le> 1
k < x1

goal (1 subgoal):
 1. denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using measure_well_com
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote ?x3a ?\<rho>
well_com (Measure x1 x2a x3a)
\<forall>k<x1. partial_density_operator (x2a k * \<rho> * adjoint (x2a k))
\<forall>k<x1. x2a k * \<rho> * adjoint (x2a k) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> trace (complex_of_real c \<cdot>\<^sub>m (x2a ?k * \<rho> * adjoint (x2a ?k))) \<le> 1
k < x1
\<lbrakk>well_com (Measure ?n ?M ?S); ?k < ?n\<rbrakk> \<Longrightarrow> well_com (?S ! ?k)

goal (1 subgoal):
 1. denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (x3a ! k) (complex_of_real c \<cdot>\<^sub>m (x2a k * \<rho> * adjoint (x2a k))) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
have "denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
using this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using Measure.prems(1) k
[PROOF STATE]
proof (prove)
using this:
denote (x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m denote (x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
well_com (Measure x1 x2a x3a)
k < x1

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k))

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k))
[PROOF STEP]
have "matrix_sum d (\<lambda>k. c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 =
      matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1"
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k))

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
[PROOF STEP]
using matrix_sum_cong[of x1 "(\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)))"
        "(\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k)))"] dimcm
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a ?k)) = complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k))
(\<And>k. k < x1 \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) = (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) \<Longrightarrow> matrix_sum ?d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum ?d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
?k < x1 \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
[PROOF STEP]
have "matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 =
       c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
[PROOF STEP]
using matrix_sum_smult[of x1 "(\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)))" d c] dimm
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
(\<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d) \<Longrightarrow> matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho> * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
[PROOF STEP]
have "denote (Measure x1 x2a x3a) (c \<cdot>\<^sub>m \<rho>) = c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
using denote.simps(4)[of x1 x2a x3a "c \<cdot>\<^sub>m \<rho>"]
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = denote_measure x1 x2a (map denote x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>)

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
using denote.simps(4)[of x1 x2a x3a "\<rho>"]
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = denote_measure x1 x2a (map denote x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>)
denote (Measure x1 x2a x3a) \<rho> = denote_measure x1 x2a (map denote x3a) \<rho>

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1 = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x2a k))) x1
denote (Measure x1 x2a x3a) \<rho> = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) x1

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x3aa \<rho>; well_com (Measure x1 x2a x3a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
denote (Measure x1 x2a x3a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (Measure x1 x2a x3a) \<rho>

goal (1 subgoal):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
case (While x1 x2a)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a ?\<rho>
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1; measurement d 2 x1; well_com x2a\<rbrakk> \<Longrightarrow> denote_while (x1 0) (x1 (Suc 0)) (denote x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 (Suc 0)) (denote x2a) \<rho>
[PROOF STEP]
using denote_while_scale assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real ?c \<cdot>\<^sub>m ?\<rho>) \<le> 1; 0 \<le> ?c; measurement d 2 ?x1.0; well_com ?x2.0; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real ?c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x2.0 (complex_of_real ?c \<cdot>\<^sub>m \<rho>) = complex_of_real ?c \<cdot>\<^sub>m denote ?x2.0 \<rho>\<rbrakk> \<Longrightarrow> denote_while (?x1.0 0) (?x1.0 1) (denote ?x2.0) (complex_of_real ?c \<cdot>\<^sub>m ?\<rho>) = complex_of_real ?c \<cdot>\<^sub>m denote_while (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?\<rho>
0 \<le> c

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2a \<rho>; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1; measurement d 2 x1; well_com x2a\<rbrakk> \<Longrightarrow> denote_while (x1 0) (x1 (Suc 0)) (denote x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 (Suc 0)) (denote x2a) \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (While x1 x2a) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote (While x1 x2a) \<rho>

goal:
No subgoals!
[PROOF STEP]
qed