[STATEMENT]
lemma denote_positive_trace_dim:
  "well_com S \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
   \<Longrightarrow> (positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> trace \<rho> \<and> denote S \<rho> \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
proof (induction arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<rho>. \<lbrakk>well_com SKIP; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote SKIP \<rho>) \<and> trace (denote SKIP \<rho>) \<le> trace \<rho> \<and> denote SKIP \<rho> \<in> carrier_mat d d
 2. \<And>x \<rho>. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
 3. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
 4. \<And>x1 x2a x3 \<rho>. \<lbrakk>\<And>x3a \<rho>. \<lbrakk>x3a \<in> set x3; well_com x3a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x3a \<rho>) \<and> trace (denote x3a \<rho>) \<le> trace \<rho> \<and> denote x3a \<rho> \<in> carrier_mat d d; well_com (Measure x1 x2a x3); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (Measure x1 x2a x3) \<rho>) \<and> trace (denote (Measure x1 x2a x3) \<rho>) \<le> trace \<rho> \<and> denote (Measure x1 x2a x3) \<rho> \<in> carrier_mat d d
 5. \<And>x1 x2a \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
case SKIP
[PROOF STATE]
proof (state)
this:
well_com SKIP
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

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

goal (1 subgoal):
 1. positive (denote SKIP \<rho>) \<and> trace (denote SKIP \<rho>) \<le> trace \<rho> \<and> denote SKIP \<rho> \<in> carrier_mat d d
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
\<rho> \<in> carrier_mat d d
positive \<rho> \<and> trace \<rho> \<le> 1

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

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

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

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
assume wc: "well_com (Utrans x)" and r: "\<rho> \<in> carrier_mat d d" and pdo: "partial_density_operator \<rho>"
[PROOF STATE]
proof (state)
this:
well_com (Utrans x)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<lbrakk>well_com (Utrans x); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
show "positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "trace (x * \<rho> * adjoint x) = trace ((adjoint x * x) * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_mat d d
[PROOF STEP]
using wc
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans x)

goal (1 subgoal):
 1. x \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) = trace (adjoint x * x * \<rho>)

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "\<dots> = trace (1\<^sub>m d * \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (adjoint x * x * \<rho>) = trace (1\<^sub>m d * \<rho>)
[PROOF STEP]
using wc inverts_mat_def inverts_mat_symm adjoint_dim
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans x)
inverts_mat ?A ?B \<equiv> ?A * ?B = 1\<^sub>m (dim_row ?A)
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n; inverts_mat ?A ?B\<rbrakk> \<Longrightarrow> inverts_mat ?B ?A
?A \<in> carrier_mat ?n ?n \<Longrightarrow> adjoint ?A \<in> carrier_mat ?n ?n

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

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (adjoint x * x * \<rho>) = trace (1\<^sub>m d * \<rho>)

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "\<dots> = trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (1\<^sub>m d * \<rho>) = trace \<rho>
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (x * \<rho> * adjoint x) = trace \<rho>
[PROOF STEP]
have fst: "trace (x * \<rho> * adjoint x) = trace \<rho>"
[PROOF STATE]
proof (prove)
using this:
trace (x * \<rho> * adjoint x) = trace \<rho>

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

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (x * \<rho> * adjoint x) = trace \<rho>

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "positive (x * \<rho> * adjoint x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (x * \<rho> * adjoint x)
[PROOF STEP]
using positive_close_under_left_right_mult_adjoint r pdo wc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> positive (?M * ?A * adjoint ?M)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
well_com (Utrans x)

goal (1 subgoal):
 1. positive (x * \<rho> * adjoint x)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M \<in> carrier_mat ?n ?n; ?A \<in> carrier_mat ?n ?n; positive ?A\<rbrakk> \<Longrightarrow> positive (?M * ?A * adjoint ?M)
\<rho> \<in> carrier_mat d d
positive \<rho> \<and> trace \<rho> \<le> 1
well_com (Utrans x)

goal (1 subgoal):
 1. positive (x * \<rho> * adjoint x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
positive (x * \<rho> * adjoint x)

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
positive (x * \<rho> * adjoint x)

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "x * \<rho> * adjoint x \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * \<rho> * adjoint x \<in> carrier_mat d d
[PROOF STEP]
using r wc adjoint_dim index_mult_mat
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
well_com (Utrans x)
?A \<in> carrier_mat ?n ?n \<Longrightarrow> adjoint ?A \<in> carrier_mat ?n ?n
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?B\<rbrakk> \<Longrightarrow> (?A * ?B) $$ (?i, ?j) = row ?A ?i \<bullet> col ?B ?j
dim_row (?A * ?B) = dim_row ?A
dim_col (?A * ?B) = dim_col ?B

goal (1 subgoal):
 1. x * \<rho> * adjoint x \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * \<rho> * adjoint x \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (x * \<rho> * adjoint x) = trace \<rho>
positive (x * \<rho> * adjoint x)
x * \<rho> * adjoint x \<in> carrier_mat d d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (x * \<rho> * adjoint x) = trace \<rho>
positive (x * \<rho> * adjoint x)
x * \<rho> * adjoint x \<in> carrier_mat d d

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote (Utrans x) \<rho>) \<and> trace (denote (Utrans x) \<rho>) \<le> trace \<rho> \<and> denote (Utrans x) \<rho> \<in> carrier_mat d d

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

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

goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
assume dx1: "(\<And>\<rho>. well_com x1 \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d)"
       and dx2a: "(\<And>\<rho>. well_com x2a \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d)"
       and wc: "well_com (Seq x1 x2a)" and r: "\<rho> \<in> carrier_mat d d" and pdo: "partial_density_operator \<rho>"
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x1 ?\<rho>) \<and> trace (denote x1 ?\<rho>) \<le> trace ?\<rho> \<and> denote x1 ?\<rho> \<in> carrier_mat d d
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x1; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d; \<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (x1;; x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
show "positive (denote (Seq x1 x2a) \<rho>) \<and> trace (denote (Seq x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (Seq x1 x2a) \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have ptc: "positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d
[PROOF STEP]
using wc r pdo dx1
[PROOF STATE]
proof (prove)
using this:
well_com (x1;; x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<lbrakk>well_com x1; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x1 ?\<rho>) \<and> trace (denote x1 ?\<rho>) \<le> trace ?\<rho> \<and> denote x1 ?\<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "partial_density_operator (denote x1 \<rho>)"
[PROOF STATE]
proof (prove)
using this:
positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. partial_density_operator (denote x1 \<rho>)
[PROOF STEP]
using pdo
[PROOF STATE]
proof (prove)
using this:
positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. partial_density_operator (denote x1 \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d
positive \<rho> \<and> trace \<rho> \<le> 1

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

goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_density_operator (denote x1 \<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (denote x1 \<rho>)

goal (1 subgoal):
 1. positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
using ptc dx2a wc  dual_order.trans
[PROOF STATE]
proof (prove)
using this:
partial_density_operator (denote x1 \<rho>)
positive (denote x1 \<rho>) \<and> trace (denote x1 \<rho>) \<le> trace \<rho> \<and> denote x1 \<rho> \<in> carrier_mat d d
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
well_com (x1;; x2a)
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote (x1;; x2a) \<rho>) \<and> trace (denote (x1;; x2a) \<rho>) \<le> trace \<rho> \<and> denote (x1;; x2a) \<rho> \<in> carrier_mat d d

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

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

goal (1 subgoal):
 1. positive (denote (Measure x1 x2a x3a) \<rho>) \<and> trace (denote (Measure x1 x2a x3a) \<rho>) \<le> trace \<rho> \<and> denote (Measure x1 x2a x3a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_measure_positive_trace_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set x3a; well_com ?x3a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?x3a ?\<rho>) \<and> trace (denote ?x3a ?\<rho>) \<le> trace ?\<rho> \<and> denote ?x3a ?\<rho> \<in> carrier_mat d d
well_com (Measure x1 x2a x3a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
\<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> positive (denote (Measure ?x1.0 ?x2a ?x3a) ?x4.0) \<and> trace (denote (Measure ?x1.0 ?x2a ?x3a) ?x4.0) \<le> trace ?x4.0 \<and> denote (Measure ?x1.0 ?x2a ?x3a) ?x4.0 \<in> carrier_mat d d

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

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

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

goal (1 subgoal):
 1. positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "adjoint (x1 0) * (x1 0) + adjoint (x1 1) * (x1 1) = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
using measurement_id2 While
[PROOF STATE]
proof (prove)
using this:
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
have "x1 0 \<in> carrier_mat d d \<and> x1 1 \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 0 \<in> carrier_mat d d \<and> x1 1 \<in> carrier_mat d d
[PROOF STEP]
using measurement_dim While
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

goal (1 subgoal):
 1. x1 0 \<in> carrier_mat d d \<and> x1 1 \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x1 0 \<in> carrier_mat d d \<and> x1 1 \<in> carrier_mat d d

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2a) \<rho> \<in> carrier_mat d d \<and> positive (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<and> trace (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<le> trace \<rho>
[PROOF STEP]
using denote_while_dim_positive[of "x1 0" "x1 1" "denote x2a" "\<rho>"] While
[PROOF STATE]
proof (prove)
using this:
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d \<and> x1 1 \<in> carrier_mat d d
\<lbrakk>x1 0 \<in> carrier_mat d d; x1 1 \<in> carrier_mat d d; adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; \<rho> \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> denote_while (x1 0) (x1 1) (denote x2a) \<rho> \<in> carrier_mat d d \<and> positive (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<and> trace (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<le> trace \<rho>
\<lbrakk>well_com x2a; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a ?\<rho>) \<and> trace (denote x2a ?\<rho>) \<le> trace ?\<rho> \<and> denote x2a ?\<rho> \<in> carrier_mat d d
well_com (While x1 x2a)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>well_com x2a; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2a \<rho>) \<and> trace (denote x2a \<rho>) \<le> trace \<rho> \<and> denote x2a \<rho> \<in> carrier_mat d d; well_com (While x1 x2a); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
denote_while (x1 0) (x1 1) (denote x2a) \<rho> \<in> carrier_mat d d \<and> positive (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<and> trace (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<le> trace \<rho>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote_while (x1 0) (x1 1) (denote x2a) \<rho> \<in> carrier_mat d d \<and> positive (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<and> trace (denote_while (x1 0) (x1 1) (denote x2a) \<rho>) \<le> trace \<rho>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
positive (denote (While x1 x2a) \<rho>) \<and> trace (denote (While x1 x2a) \<rho>) \<le> trace \<rho> \<and> denote (While x1 x2a) \<rho> \<in> carrier_mat d d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma denote_dim_pdo:
  "well_com S \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
   \<Longrightarrow> (denote S \<rho> \<in> carrier_mat d d) \<and> (partial_density_operator (denote S \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote S \<rho>)
[PROOF STEP]
using denote_positive_trace_dim
[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

goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> carrier_mat d d \<and> partial_density_operator (denote S \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; positive ?\<rho> \<and> trace ?\<rho> \<le> 1\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; positive \<rho> \<and> trace \<rho> \<le> 1\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> carrier_mat d d \<and> positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> 1
[PROOF STEP]
by fastforce


[STATEMENT]
lemma denote_dim:
  "well_com S \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
   \<Longrightarrow> (denote S \<rho> \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim
[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

goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> denote S \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto


[STATEMENT]
lemma denote_trace:
  "well_com S \<Longrightarrow> \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>
   \<Longrightarrow> trace (denote S \<rho>) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> trace (denote S \<rho>) \<le> trace \<rho>
[PROOF STEP]
using denote_positive_trace_dim
[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

goal (1 subgoal):
 1. \<lbrakk>well_com S; \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> trace (denote S \<rho>) \<le> trace \<rho>
[PROOF STEP]
by auto


[STATEMENT]
lemma denote_partial_density_operator:
  assumes "well_com S" "partial_density_operator \<rho>" "\<rho> \<in> carrier_mat d d"
  shows "partial_density_operator (denote S \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote S \<rho>)
[PROOF STEP]
using assms denote_positive_trace_dim
[PROOF STATE]
proof (prove)
using this:
well_com S
partial_density_operator \<rho>
\<rho> \<in> carrier_mat d d
\<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

goal (1 subgoal):
 1. partial_density_operator (denote S \<rho>)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
well_com S
positive \<rho> \<and> trace \<rho> \<le> 1
\<rho> \<in> carrier_mat d d
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; positive ?\<rho> \<and> trace ?\<rho> \<le> 1\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> 1
[PROOF STEP]
using dual_order.trans
[PROOF STATE]
proof (prove)
using this:
well_com S
positive \<rho> \<and> trace \<rho> \<le> 1
\<rho> \<in> carrier_mat d d
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; positive ?\<rho> \<and> trace ?\<rho> \<le> 1\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

goal (1 subgoal):
 1. positive (denote S \<rho>) \<and> trace (denote S \<rho>) \<le> 1
[PROOF STEP]
by blast


[STATEMENT]
lemma denote_while_n_sum_mat_seq:
  assumes "\<rho> \<in> carrier_mat d d" and
    "x1 0 \<in> carrier_mat d d" and
    "x1 1 \<in> carrier_mat d d" and
    "partial_density_operator \<rho>" and
    wc: "well_com x2" and mea: "measurement d 2 x1"
  shows "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
let ?A = "x1 0" and ?B = "x1 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
have dx2:"\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow>
            positive ((denote x2) \<rho>) \<and> trace ((denote x2) \<rho>) \<le> trace \<rho> \<and> (denote x2) \<rho> \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 \<rho>) \<and> trace (denote x2 \<rho>) \<le> trace \<rho> \<and> denote x2 \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim wc
[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
well_com x2

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

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
have lo1: "adjoint ?A * ?A + adjoint ?B * ?B = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
using measurement_id2 assms
[PROOF STATE]
proof (prove)
using this:
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d
\<rho> \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>
well_com x2
measurement d 2 x1

goal (1 subgoal):
 1. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
have "\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using assms dx2
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 ?\<rho>) \<and> trace (denote x2 ?\<rho>) \<le> trace ?\<rho> \<and> denote x2 ?\<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
by (metis denote_while_n_dim matrix_sum_dim)
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
have "(\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
[PROOF STEP]
using assms dx2 lo1
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 ?\<rho>) \<and> trace (denote x2 ?\<rho>) \<le> trace ?\<rho> \<and> denote x2 ?\<rho> \<in> carrier_mat d d
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d

goal (1 subgoal):
 1. \<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
[PROOF STEP]
by (metis denote_while_n_sum_partial_density)
[PROOF STATE]
proof (state)
this:
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
have "(\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)
[PROOF STEP]
using assms dx2 lo1
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 ?\<rho>) \<and> trace (denote x2 ?\<rho>) \<le> trace ?\<rho> \<and> denote x2 ?\<rho> \<in> carrier_mat d d
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d

goal (1 subgoal):
 1. \<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)
[PROOF STEP]
by (metis denote_while_n_sum_lowner_le)
[PROOF STATE]
proof (state)
this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
unfolding matrix_seq_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n)

goal (1 subgoal):
 1. (\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d) \<and> (\<forall>n. partial_density_operator (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)) \<and> (\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<le>\<^sub>L matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))

goal:
No subgoals!
[PROOF STEP]
qed