[STATEMENT]
lemma denote_while_n_add:
  assumes M0: "x1 0 \<in> carrier_mat d d" and
    M1: "x1 1 \<in> carrier_mat d d" and
    wc: "well_com x2" and mea: "measurement d 2 x1" and
    DS: "(\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<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 x2 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2 \<rho>\<^sub>1 + denote x2 \<rho>\<^sub>2)"
  shows "\<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_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2
[PROOF STEP]
proof (auto, induct k arbitrary: \<rho>\<^sub>1 \<rho>\<^sub>2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>2 * adjoint (x1 0)
 2. \<And>k \<rho>\<^sub>1 \<rho>\<^sub>2. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<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>\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>2 * adjoint (x1 0)
 2. \<And>k \<rho>\<^sub>1 \<rho>\<^sub>2. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<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:
\<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. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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> x1 0 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
using M0
[PROOF STATE]
proof (prove)
using this:
x1 0 \<in> carrier_mat d d

goal (1 subgoal):
 1. \<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> x1 0 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho>\<^sub>2 * adjoint (x1 0)

goal (1 subgoal):
 1. \<And>k \<rho>\<^sub>1 \<rho>\<^sub>2. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k \<rho>\<^sub>1 \<rho>\<^sub>2. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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 \<rho>\<^sub>1 \<rho>\<^sub>2. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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>?\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
let ?A = "x1 0" and ?B = "x1 1"
[PROOF STATE]
proof (state)
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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[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. \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have lo1: "adjoint ?B * ?B \<le>\<^sub>L 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
using measurement_le_one_mat assms
[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
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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

goal (1 subgoal):
 1. adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m 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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have dim1: "x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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. x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
by (metis adjoint_dim mult_carrier_mat)
[PROOF STATE]
proof (state)
this:
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have pdo1: "partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))
[PROOF STEP]
using pdo_close_under_measurement assms(2) Suc(2,4) lo1
[PROOF STATE]
proof (prove)
using this:
\<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)
x1 1 \<in> carrier_mat d d
\<rho>\<^sub>1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))
[PROOF STEP]
have dimr1: "denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))

goal (1 subgoal):
 1. denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
using dx2
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))
\<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. denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have dim2: "x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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. x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
by (metis adjoint_dim mult_carrier_mat)
[PROOF STATE]
proof (state)
this:
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have pdo2: "partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
[PROOF STEP]
using pdo_close_under_measurement assms(2) Suc lo1
[PROOF STATE]
proof (prove)
using this:
\<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)
x1 1 \<in> carrier_mat d d
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
[PROOF STEP]
have dimr2: "denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))

goal (1 subgoal):
 1. denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
using dx2
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
\<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. denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have pdor1: "partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)))
[PROOF STEP]
using denote_partial_density_operator assms dim1 pdo1
[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>)
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have pdor2: "partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))
[PROOF STEP]
using denote_partial_density_operator assms dim2 pdo2
[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>)
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have "trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))
[PROOF STEP]
using dx2 dim1 pdo1
[PROOF STATE]
proof (prove)
using 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
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have tr1: "\<dots> \<le> trace \<rho>\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>1
[PROOF STEP]
using trace_decrease_mul_adj assms Suc lo1
[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>
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1
[PROOF STEP]
have trr1:" trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have "trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
[PROOF STEP]
using dx2 dim2 pdo2
[PROOF STATE]
proof (prove)
using 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
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have tr2: "\<dots> \<le> trace \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
using trace_decrease_mul_adj assms Suc lo1
[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>
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
well_com x2
measurement d 2 x1
\<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
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
have trr2:" trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>2

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
from tr1 tr2 Suc
[PROOF STATE]
proof (chain)
picking this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>1
trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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]
have "trace ( (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) +  (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>1
trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using trace_add_linear trace_add_linear[of "(x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))" d "(x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"]
            trace_add_linear[of \<rho>\<^sub>1 d \<rho>\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>1
trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
\<lbrakk>x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d; x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) = trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
\<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) = trace \<rho>\<^sub>1 + trace \<rho>\<^sub>2

goal (1 subgoal):
 1. trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using dim1 dim2
[PROOF STATE]
proof (prove)
using this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<le> trace \<rho>\<^sub>1
trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
\<lbrakk>x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d; x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) = trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + trace (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
\<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) = trace \<rho>\<^sub>1 + trace \<rho>\<^sub>2
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
have trless1: "trace ( (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) +  (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)

goal (1 subgoal):
 1. trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> trace (\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> 1

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
from trr1 trr2 Suc
[PROOF STATE]
proof (chain)
picking this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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]
have "trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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 x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using trace_add_linear[of "denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))" d "denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"]
            trace_add_linear[of \<rho>\<^sub>1 d \<rho>\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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>denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d; denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) = trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) + trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))
\<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) = trace \<rho>\<^sub>1 + trace \<rho>\<^sub>2

goal (1 subgoal):
 1. trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using dimr1 dimr2
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) \<le> trace \<rho>\<^sub>1
trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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>denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d; denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) = trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))) + trace (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))
\<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) = trace \<rho>\<^sub>1 + trace \<rho>\<^sub>2
denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d
denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
have trless2: "trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)

goal (1 subgoal):
 1. trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> trace (\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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 x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
have "x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)
[PROOF STEP]
using M1 Suc
[PROOF STATE]
proof (prove)
using this:
x1 1 \<in> carrier_mat d d
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
\<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. x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)
[PROOF STEP]
by (mat_assoc d)
[PROOF STATE]
proof (state)
this:
x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)
[PROOF STEP]
have deadd: "denote x2 (x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1)) =
        denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
using this:
x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)

goal (1 subgoal):
 1. denote x2 (x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1)) = denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
[PROOF STEP]
using assms(5) dim1 dim2 pdo1 pdo2 trless1
[PROOF STATE]
proof (prove)
using this:
x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1) = x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)
\<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
x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) \<in> carrier_mat d d
x1 1 * \<rho>\<^sub>2 * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1))
partial_density_operator (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
trace (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1) + x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<le> 1

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

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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k \<rho>\<^sub>2 * adjoint (x1 0); \<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)
[PROOF STEP]
from dimr1 dimr2 pdor1 pdor2 trless2 Suc(1) deadd
[PROOF STATE]
proof (chain)
picking this:
denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d
denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d
partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)))
partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
denote x2 (x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1)) = denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) \<in> carrier_mat d d
denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)) \<in> carrier_mat d d
partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)))
partial_density_operator (denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1)))
trace (denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))) \<le> 1
\<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> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) k ?\<rho>\<^sub>2 * adjoint (x1 0)
denote x2 (x1 1 * (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 1)) = denote x2 (x1 1 * \<rho>\<^sub>1 * adjoint (x1 1)) + denote x2 (x1 1 * \<rho>\<^sub>2 * adjoint (x1 1))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) (\<rho>\<^sub>1 + \<rho>\<^sub>2) * adjoint (x1 0) = x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>1 * adjoint (x1 0) + x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc k) \<rho>\<^sub>2 * adjoint (x1 0)

goal:
No subgoals!
[PROOF STEP]
qed