[STATEMENT]
lemma mulfact:
  fixes c:: real and a:: complex and b:: complex
  assumes "c\<ge>0" "a \<le> b"
  shows "c * a \<le> c * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real c * a \<le> complex_of_real c * b
[PROOF STEP]
using assms mult_le_cancel_iff2
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
a \<le> b
(0::?'a) < ?z \<Longrightarrow> (?z * ?x \<le> ?z * ?y) = (?x \<le> ?y)

goal (1 subgoal):
 1. complex_of_real c * a \<le> complex_of_real c * b
[PROOF STEP]
unfolding less_eq_complex_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
Re a \<le> Re b \<and> Im a = Im b
(0::?'a) < ?z \<Longrightarrow> (?z * ?x \<le> ?z * ?y) = (?x \<le> ?y)

goal (1 subgoal):
 1. Re (complex_of_real c * a) \<le> Re (complex_of_real c * b) \<and> Im (complex_of_real c * a) = Im (complex_of_real c * b)
[PROOF STEP]
by force


[STATEMENT]
lemma denote_while_n_scale:
  fixes c:: real
  assumes "c\<ge>0"
    "measurement d 2 x1" "well_com x2"
    "(\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> trace (c \<cdot>\<^sub>m \<rho>) \<le> 1 \<Longrightarrow>
      denote x2 (c \<cdot>\<^sub>m \<rho>) =  c \<cdot>\<^sub>m denote x2 \<rho>)"
  shows "\<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> trace (c \<cdot>\<^sub>m \<rho>) \<le> 1 \<Longrightarrow>
    denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) = c \<cdot>\<^sub>m (denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>
[PROOF STEP]
proof (auto, induct n arbitrary: \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho> * adjoint (x1 0))
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (2 subgoals):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho> * adjoint (x1 0))
 2. \<And>n \<rho>. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

goal (1 subgoal):
 1. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho> * adjoint (x1 0))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * \<rho> * adjoint (x1 0))
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 0 \<in> carrier_mat d d
[PROOF STEP]
using assms measurement_dim
[PROOF STATE]
proof (prove)
using this:
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. x1 0 \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) 0 \<rho> * adjoint (x1 0))

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

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

goal (1 subgoal):
 1. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
let ?A = "x1 0" and ?B = "x1 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * 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 assms
[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
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>

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>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * 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
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>

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>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have dim1: "x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
using assms(2) Suc(2) measurement_dim
[PROOF STATE]
proof (prove)
using this:
measurement d 2 x1
\<rho> \<in> carrier_mat d d
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
[PROOF STEP]
by (meson adjoint_dim mult_carrier_mat one_less_numeral_iff semiring_norm(76))
[PROOF STATE]
proof (state)
this:
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have pdo1: "partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))
[PROOF STEP]
using pdo_close_under_measurement assms  Suc lo1 measurement_dim
[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)
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m ?\<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n ?\<rho> * adjoint (x1 0))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))
[PROOF STEP]
by (metis One_nat_def lessI numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))
[PROOF STEP]
have dimr: "denote x2 (x1 1 * \<rho> * adjoint (x1 1)) \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))

goal (1 subgoal):
 1. denote x2 (x1 1 * \<rho> * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
using dx2
[PROOF STATE]
proof (prove)
using this:
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * 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> * adjoint (x1 1)) \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote x2 (x1 1 * \<rho> * adjoint (x1 1)) \<in> carrier_mat d d

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have pdor: "partial_density_operator (denote x2 (x1 1 * \<rho> * adjoint (x1 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (denote x2 (x1 1 * \<rho> * 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>)
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have "trace (denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (x1 1 * \<rho> * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (x1 1 * \<rho> * 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> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have trr1: "\<dots> \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (x1 1 * \<rho> * adjoint (x1 1)) \<le> trace \<rho>
[PROOF STEP]
using trace_decrease_mul_adj assms Suc lo1 measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>partial_density_operator ?\<rho>; ?\<rho> \<in> carrier_mat d d; ?x \<in> carrier_mat d d; adjoint ?x * ?x \<le>\<^sub>L 1\<^sub>m d\<rbrakk> \<Longrightarrow> trace (?x * ?\<rho> * adjoint ?x) \<le> trace ?\<rho>
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m ?\<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n ?\<rho> * adjoint (x1 0))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
adjoint (x1 1) * x1 1 \<le>\<^sub>L 1\<^sub>m d
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
using assms(1) state_sig.mulfact
[PROOF STATE]
proof (prove)
using this:
trace (denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace \<rho>
trace (complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))) = complex_of_real c * trace (denote x2 (x1 1 * \<rho> * adjoint (x1 1)))
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c * trace \<rho>
0 \<le> c
\<lbrakk>0 \<le> ?c; ?a \<le> ?b\<rbrakk> \<Longrightarrow> complex_of_real ?c * ?a \<le> complex_of_real ?c * ?b

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

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m ?\<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n ?\<rho> * adjoint (x1 0))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

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

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

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

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
using trcr trr1 assms(1)
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) = complex_of_real c * trace (x1 1 * \<rho> * adjoint (x1 1))
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c * trace \<rho>
trace (x1 1 * \<rho> * adjoint (x1 1)) \<le> trace \<rho>
0 \<le> c

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
using state_sig.mulfact
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) = complex_of_real c * trace (x1 1 * \<rho> * adjoint (x1 1))
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c * trace \<rho>
trace (x1 1 * \<rho> * adjoint (x1 1)) \<le> trace \<rho>
0 \<le> c
\<lbrakk>0 \<le> ?c; ?a \<le> ?b\<rbrakk> \<Longrightarrow> complex_of_real ?c * ?a \<le> complex_of_real ?c * ?b

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

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) \<le> 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m ?\<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n ?\<rho> * adjoint (x1 0))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have "x1 1 * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 1) = complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 1 * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 1) = complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))
[PROOF STEP]
apply (mat_assoc d)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x1 1 \<in> carrier_mat d d
 2. \<rho> \<in> carrier_mat d d
[PROOF STEP]
using Suc.prems(1) assms measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<rho> \<in> carrier_mat d d
0 \<le> c
measurement d 2 x1
well_com x2
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
\<lbrakk>measurement ?d ?n ?M; ?k < ?n\<rbrakk> \<Longrightarrow> ?M ?k \<in> carrier_mat ?d ?d

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n \<rho> * adjoint (x1 0)); \<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
have "denote x2 (c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) = c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote x2 (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) = complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))
[PROOF STEP]
using assms(4) dim1 pdo1 trrle
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (complex_of_real c \<cdot>\<^sub>m ?\<rho>) = complex_of_real c \<cdot>\<^sub>m denote x2 ?\<rho>
x1 1 * \<rho> * adjoint (x1 1) \<in> carrier_mat d d
partial_density_operator (x1 1 * \<rho> * adjoint (x1 1))
trace (complex_of_real c \<cdot>\<^sub>m (x1 1 * \<rho> * adjoint (x1 1))) \<le> 1

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

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

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

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

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

goal (1 subgoal):
 1. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))
[PROOF STEP]
using Suc dimr pdor trrc
[PROOF STATE]
proof (prove)
using this:
denote x2 (x1 1 * (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 1)) = complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))
\<lbrakk>?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>; trace (complex_of_real c \<cdot>\<^sub>m ?\<rho>) \<le> 1\<rbrakk> \<Longrightarrow> x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n (complex_of_real c \<cdot>\<^sub>m ?\<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) n ?\<rho> * adjoint (x1 0))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
denote x2 (x1 1 * \<rho> * adjoint (x1 1)) \<in> carrier_mat d d
partial_density_operator (denote x2 (x1 1 * \<rho> * adjoint (x1 1)))
trace (complex_of_real c \<cdot>\<^sub>m denote x2 (x1 1 * \<rho> * adjoint (x1 1))) \<le> 1

goal (1 subgoal):
 1. x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * 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 n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * 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 n) (complex_of_real c \<cdot>\<^sub>m \<rho>) * adjoint (x1 0) = complex_of_real c \<cdot>\<^sub>m (x1 0 * denote_while_n_iter (x1 0) (x1 (Suc 0)) (denote x2) (Suc n) \<rho> * adjoint (x1 0))

goal:
No subgoals!
[PROOF STEP]
qed