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

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

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

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

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

goal (1 subgoal):
 1. denote (Utrans U) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Utrans U) \<rho>\<^sub>1 + denote (Utrans U) \<rho>\<^sub>2
[PROOF STEP]
by (clarsimp, mat_assoc d)
[PROOF STATE]
proof (state)
this:
denote (Utrans U) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Utrans U) \<rho>\<^sub>1 + denote (Utrans U) \<rho>\<^sub>2

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

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

goal (1 subgoal):
 1. denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x1; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x2a; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a \<rho>\<^sub>1 + denote x2a \<rho>\<^sub>2; well_com (x1;; x2a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
have dim1: "denote x1 \<rho>\<^sub>1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote x1 \<rho>\<^sub>1 \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim Seq
[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>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x1 ?\<rho>\<^sub>1 + denote x1 ?\<rho>\<^sub>2
\<lbrakk>well_com x2a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2a ?\<rho>\<^sub>1 + denote x2a ?\<rho>\<^sub>2
well_com (x1;; x2a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x1; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x2a; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a \<rho>\<^sub>1 + denote x2a \<rho>\<^sub>2; well_com (x1;; x2a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
have dim2: "denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim Seq
[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>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x1 ?\<rho>\<^sub>1 + denote x1 ?\<rho>\<^sub>2
\<lbrakk>well_com x2a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2a ?\<rho>\<^sub>1 + denote x2a ?\<rho>\<^sub>2
well_com (x1;; x2a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

goal (1 subgoal):
 1. denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x1; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x2a; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a \<rho>\<^sub>1 + denote x2a \<rho>\<^sub>2; well_com (x1;; x2a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
have "trace (denote x1  \<rho>\<^sub>1) \<le> trace \<rho>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote x1 \<rho>\<^sub>1) \<le> trace \<rho>\<^sub>1
[PROOF STEP]
using denote_positive_trace_dim Seq
[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>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x1 ?\<rho>\<^sub>1 + denote x1 ?\<rho>\<^sub>2
\<lbrakk>well_com x2a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2a ?\<rho>\<^sub>1 + denote x2a ?\<rho>\<^sub>2
well_com (x1;; x2a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x1; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x2a; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a \<rho>\<^sub>1 + denote x2a \<rho>\<^sub>2; well_com (x1;; x2a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
have "trace (denote x1 \<rho>\<^sub>2) \<le> trace \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote x1 \<rho>\<^sub>2) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
using denote_positive_trace_dim Seq
[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>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x1 ?\<rho>\<^sub>1 + denote x1 ?\<rho>\<^sub>2
\<lbrakk>well_com x2a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2a ?\<rho>\<^sub>1 + denote x2a ?\<rho>\<^sub>2
well_com (x1;; x2a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

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

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

goal (1 subgoal):
 1. trace (denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2) \<le> 1
[PROOF STEP]
using Seq(4,5,8) trace_add_linear dim1 dim2
[PROOF STATE]
proof (prove)
using this:
trace (denote x1 \<rho>\<^sub>1) \<le> trace \<rho>\<^sub>1
trace (denote x1 \<rho>\<^sub>2) \<le> trace \<rho>\<^sub>2
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
denote x1 \<rho>\<^sub>1 \<in> carrier_mat d d
denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2) \<le> 1
[PROOF STEP]
by (smt add_mono order_trans)
[PROOF STATE]
proof (state)
this:
trace (denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2) \<le> 1

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x1; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>well_com x2a; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a \<rho>\<^sub>1 + denote x2a \<rho>\<^sub>2; well_com (x1;; x2a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
have "denote (Seq x1 x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a (denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a (denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a (denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2))

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. partial_density_operator (denote x1 \<rho>\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partial_density_operator (denote x1 \<rho>\<^sub>2)

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

goal (1 subgoal):
 1. denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2
[PROOF STEP]
using Seq dim1 dim2 tr
[PROOF STATE]
proof (prove)
using this:
denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2a (denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2))
denote x1 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2
partial_density_operator (denote x1 \<rho>\<^sub>1)
partial_density_operator (denote x1 \<rho>\<^sub>2)
\<lbrakk>well_com x1; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x1 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x1 ?\<rho>\<^sub>1 + denote x1 ?\<rho>\<^sub>2
\<lbrakk>well_com x2a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2a ?\<rho>\<^sub>1 + denote x2a ?\<rho>\<^sub>2
well_com (x1;; x2a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
denote x1 \<rho>\<^sub>1 \<in> carrier_mat d d
denote x1 \<rho>\<^sub>2 \<in> carrier_mat d d
trace (denote x1 \<rho>\<^sub>1 + denote x1 \<rho>\<^sub>2) \<le> 1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
denote (x1;; x2a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (x1;; x2a) \<rho>\<^sub>1 + denote (x1;; x2a) \<rho>\<^sub>2

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

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

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[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>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<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>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking 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
[PROOF STEP]
have map:"\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> \<forall> k < x1. positive ((map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)))
               \<and> ((map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) \<in> carrier_mat d d
               \<and> trace ((map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) \<le> trace (x2a k * \<rho> * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
using 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. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * \<rho> * adjoint (x2a k))) \<le> trace (x2a k * \<rho> * adjoint (x2a k))
[PROOF STEP]
using Measure map_denote_positive_trace_dim
[PROOF STATE]
proof (prove)
using 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
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
\<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))

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

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

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
using Measure
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k))) \<le> trace (x2a k * ?\<rho> * adjoint (x2a k))
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * 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>\<^sub>1 * adjoint (x2a ?k)) \<in> carrier_mat d d

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

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
using Measure
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> \<forall>k<x1. positive ((map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k))) \<and> (map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k)) \<in> carrier_mat d d \<and> trace ((map denote x3a ! k) (x2a k * ?\<rho> * adjoint (x2a k))) \<le> trace (x2a k * ?\<rho> * adjoint (x2a k))
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * 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>\<^sub>2 * adjoint (x2a ?k)) \<in> carrier_mat d d

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

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

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

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

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

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
have lea: "\<And>k. k < x1 \<Longrightarrow> adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> adjoint (x2a k) * x2a k \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat Measure
[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
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

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

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> adjoint (x2a ?k) * x2a ?k \<le>\<^sub>L 1\<^sub>m d

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

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

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

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> partial_density_operator (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<and> partial_density_operator (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
using pdo_close_under_measurement Measure measurement_dim
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> adjoint (x2a ?k) * x2a ?k \<le>\<^sub>L 1\<^sub>m d
?k < x1 \<Longrightarrow> x2a ?k \<in> carrier_mat d 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)
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> partial_density_operator (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<and> partial_density_operator (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> partial_density_operator (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) \<and> partial_density_operator (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k))

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
have trless: "trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1"
      if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
have "trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1
[PROOF STEP]
using trace_decrease_mul_adj dimx Measure lea k
[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>
?k < x1 \<Longrightarrow> x2a ?k \<in> carrier_mat d d
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
?k < x1 \<Longrightarrow> adjoint (x2a ?k) * x2a ?k \<le>\<^sub>L 1\<^sub>m d
k < x1

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

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
have "trace (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
using trace_decrease_mul_adj dimx Measure lea k
[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>
?k < x1 \<Longrightarrow> x2a ?k \<in> carrier_mat d d
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
?k < x1 \<Longrightarrow> adjoint (x2a ?k) * x2a ?k \<le>\<^sub>L 1\<^sub>m d
k < x1

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

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1
trace (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
have "trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1
trace (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>2

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using trace_add_linear dim1 dim2 Measure k
[PROOF STATE]
proof (prove)
using this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>1
trace (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace \<rho>\<^sub>2
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
?k < x1 \<Longrightarrow> x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k) \<in> carrier_mat d d
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
k < x1

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
by (metis add_mono_thms_linordered_semiring(1))
[PROOF STATE]
proof (state)
this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)

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

goal (1 subgoal):
 1. trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> 1
[PROOF STEP]
using Measure(7)
[PROOF STATE]
proof (prove)
using this:
trace (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>x3aa \<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>x3aa \<in> set x3a; well_com x3aa; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x3aa (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x3aa \<rho>\<^sub>1 + denote x3aa \<rho>\<^sub>2; well_com (Measure x1 x2a x3a); \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
have dist: "(x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))"
      if k: "k < x1" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
have "(x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = ((x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = (x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k)
[PROOF STEP]
using mult_add_distrib_mat Measure well_com.simps(4) measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A \<in> carrier_mat ?nr ?n; ?B \<in> carrier_mat ?n ?nc; ?C \<in> carrier_mat ?n ?nc\<rbrakk> \<Longrightarrow> ?A * (?B + ?C) = ?A * ?B + ?A * ?C
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com (Measure ?n ?M ?S) = (measurement d ?n ?M \<and> length ?S = ?n \<and> list_all well_com ?S)
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = (x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k)
[PROOF STEP]
by (metis k)
[PROOF STATE]
proof (state)
this:
x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = (x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k)

goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = (x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k)

goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
have "\<dots> = (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. x2a k \<in> carrier_mat d d
 2. \<rho>\<^sub>2 \<in> carrier_mat d d
 3. \<rho>\<^sub>1 \<in> carrier_mat d d
[PROOF STEP]
using Measure k well_com.simps(4) measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
k < x1
well_com (Measure ?n ?M ?S) = (measurement d ?n ?M \<and> length ?S = ?n \<and> list_all well_com ?S)
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (3 subgoals):
 1. x2a k \<in> carrier_mat d d
 2. \<rho>\<^sub>2 \<in> carrier_mat d d
 3. \<rho>\<^sub>1 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x2a k * \<rho>\<^sub>1 + x2a k * \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)

goal (1 subgoal):
 1. x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k) = x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k < x1 \<Longrightarrow> x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k) = x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k) + x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k)

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

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

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = denote (x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))
[PROOF STEP]
have mapx: "(map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) =  denote (x3a ! k) ((x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)))"
[PROOF STATE]
proof (prove)
using this:
(map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = denote (x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
using dist k
[PROOF STATE]
proof (prove)
using this:
(map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = denote (x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))
?k < x1 \<Longrightarrow> x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k) = x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k) + x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k)
k < x1

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

goal (1 subgoal):
 1. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
have "denote (x3a ! k) ((x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)))
           = denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + denote (x3a ! k) (x2a k * \<rho>\<^sub>2  * adjoint (x2a k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) = denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + denote (x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
using Measure(1,2) dim1 dim2 pdo12 trless k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x3a (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote ?x3a ?\<rho>\<^sub>1 + denote ?x3a ?\<rho>\<^sub>2
well_com (Measure x1 x2a x3a)
?k < x1 \<Longrightarrow> x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> partial_density_operator (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) \<and> partial_density_operator (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k))
?k < x1 \<Longrightarrow> trace (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k) + x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k)) \<le> 1
k < x1

goal (1 subgoal):
 1. denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) = denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + denote (x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))
[PROOF STEP]
by (simp add: list_all_length)
[PROOF STATE]
proof (state)
this:
denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k) + x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) = denote (x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + denote (x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))

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

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

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

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

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

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) \<in> carrier_mat d d
[PROOF STEP]
using mapd1 mapd2
[PROOF STATE]
proof (prove)
using this:
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k)) = (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) + (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k))
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k)) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * 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>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k)) \<in> carrier_mat d d

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k))) x1 + matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))) x1
[PROOF STEP]
using mapd12 mapd1 mapd2 mapadd
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) \<in> carrier_mat d d; \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) \<in> carrier_mat d d; \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k)) \<in> carrier_mat d d; \<And>k. k < x1 \<Longrightarrow> (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k)) = (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k)) + (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k))) x1 + matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))) x1
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k)) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k)) \<in> carrier_mat d d
?k < x1 \<Longrightarrow> (map denote x3a ! ?k) (x2a ?k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a ?k)) = (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>1 * adjoint (x2a ?k)) + (map denote x3a ! ?k) (x2a ?k * \<rho>\<^sub>2 * adjoint (x2a ?k))

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

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

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
using denote.simps(4)
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k))) x1 + matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))) x1
denote (Measure ?n ?M ?S) ?\<rho> = denote_measure ?n ?M (map denote ?S) ?\<rho>

goal (1 subgoal):
 1. denote (Measure x1 x2a x3a) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (Measure x1 x2a x3a) \<rho>\<^sub>1 + denote (Measure x1 x2a x3a) \<rho>\<^sub>2
[PROOF STEP]
unfolding denote_measure_def
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x2a k))) x1 = matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>1 * adjoint (x2a k))) x1 + matrix_sum d (\<lambda>k. (map denote x3a ! k) (x2a k * \<rho>\<^sub>2 * adjoint (x2a k))) x1
denote (Measure ?n ?M ?S) ?\<rho> = matrix_sum d (\<lambda>k. (map denote ?S ! k) (?M k * ?\<rho> * adjoint (?M k))) ?n

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

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

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

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

goal (1 subgoal):
 1. denote (While x1 x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote (While x1 x2) \<rho>\<^sub>1 + denote (While x1 x2) \<rho>\<^sub>2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2 \<rho>\<^sub>1 + denote x2 \<rho>\<^sub>2; \<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1; measurement d 2 x1; well_com x2\<rbrakk> \<Longrightarrow> denote_while (x1 0) (x1 (Suc 0)) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 (Suc 0)) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 (Suc 0)) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
using denote_while_add measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; ?x1.0 0 \<in> carrier_mat d d; ?x1.0 1 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1; well_com ?x2.0; measurement d 2 ?x1.0; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x2.0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote ?x2.0 \<rho>\<^sub>1 + denote ?x2.0 \<rho>\<^sub>2\<rbrakk> \<Longrightarrow> denote_while (?x1.0 0) (?x1.0 1) (denote ?x2.0) (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote_while (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?\<rho>\<^sub>1 + denote_while (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?\<rho>\<^sub>2
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

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

goal:
No subgoals!
[PROOF STEP]
qed