[STATEMENT]
lemma denote_while_scale:
  fixes c:: real
  assumes "\<rho> \<in> carrier_mat d d"
    "partial_density_operator \<rho>"
    "trace (c \<cdot>\<^sub>m \<rho>) \<le> 1" "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 "denote_while (x1 0) (x1 1) (denote x2) (c \<cdot>\<^sub>m \<rho>) = c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
let ?A = "x1 0" and ?B = "x1 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have dx2:"(\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive ((denote x2) \<rho>) \<and> trace ((denote x2) \<rho>) \<le> trace \<rho> \<and> (denote x2) \<rho> \<in> carrier_mat d d) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 \<rho>) \<and> trace (denote x2 \<rho>) \<le> trace \<rho> \<and> denote x2 \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim 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
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have lo1: "adjoint ?A * ?A + adjoint ?B * ?B = 1\<^sub>m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
using measurement_id2 assms
[PROOF STATE]
proof (prove)
using this:
measurement ?d 2 ?M \<Longrightarrow> adjoint (?M 0) * ?M 0 + adjoint (?M 1) * ?M 1 = 1\<^sub>m ?d
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 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. adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have ms: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
using denote_while_n_sum_mat_seq assms measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?x1.0 0 \<in> carrier_mat d d; ?x1.0 1 \<in> carrier_mat d d; partial_density_operator ?\<rho>; well_com ?x2.0; measurement d 2 ?x1.0\<rbrakk> \<Longrightarrow> matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (?x1.0 0) (?x1.0 1) (denote ?x2.0) n ?\<rho>))
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have trcless: "trace (c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
have dimr: "matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using assms dx2 denote_while_n_dim matrix_sum_dim
[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
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>\<rbrakk> \<Longrightarrow> positive (denote x2 ?\<rho>) \<and> trace (denote x2 ?\<rho>) \<le> trace ?\<rho> \<and> denote x2 ?\<rho> \<in> carrier_mat d d
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d ?f ?n \<in> carrier_mat ?d ?d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d
[PROOF STEP]
using matrix_seq.dim ms
[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
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>\<rbrakk> \<Longrightarrow> positive (denote x2 ?\<rho>) \<and> trace (denote x2 ?\<rho>) \<le> trace ?\<rho> \<and> denote x2 ?\<rho> \<in> carrier_mat d d
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
(\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d) \<Longrightarrow> matrix_sum ?d ?f ?n \<in> carrier_mat ?d ?d
matrix_seq ?dim ?f \<Longrightarrow> ?f ?n \<in> carrier_mat ?dim ?dim
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>) n) \<le> trace \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
using denote_while_n_sum_trace dx2 lo1 assms measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; adjoint ?M0.0 * ?M0.0 + adjoint ?M1.0 * ?M1.0 = 1\<^sub>m d; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (?DS \<rho>) \<and> trace (?DS \<rho>) \<le> trace \<rho> \<and> ?DS \<rho> \<in> carrier_mat d d; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> trace (matrix_sum d (\<lambda>n. denote_while_n ?M0.0 ?M1.0 ?DS n ?\<rho>) ?n) \<le> trace ?\<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
adjoint (x1 0) * x1 0 + adjoint (x1 1) * x1 1 = 1\<^sub>m d
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
have "trace (c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
[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
matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n \<in> carrier_mat d d

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

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
have "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 assms
[PROOF STATE]
proof (prove)
using this:
?A \<in> carrier_mat ?n ?n \<Longrightarrow> trace (?c \<cdot>\<^sub>m ?A) = ?c * trace ?A
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. 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. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c * trace \<rho>
[PROOF STEP]
have "trace (c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (c \<cdot>\<^sub>m \<rho>)"
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
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 matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
using  assms(4)
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace \<rho>
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c * trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c * trace \<rho>
0 \<le> c

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
by (simp add: ordered_comm_semiring_class.comm_mult_left_mono less_eq_complex_def)
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)

goal (1 subgoal):
 1. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> trace (complex_of_real c \<cdot>\<^sub>m \<rho>)
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) ?n) \<le> 1

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have llscale: "matrix_seq.lowner_lub  (\<lambda>n. c \<cdot>\<^sub>m (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>)) n)
    = c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
using lowner_lub_scale[of d "(matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))" c] ms trcless assms(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>)); \<forall>n. trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) \<le> 1; 0 \<le> c\<rbrakk> \<Longrightarrow> matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
trace (complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) ?n) \<le> 1
0 \<le> c

goal (1 subgoal):
 1. matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
have "matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m
    = c \<cdot>\<^sub>m (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>)) m"
    for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
have  dim:"(\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_dim dx2  assms measurement_dim
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<rho> \<in> carrier_mat d d; ?M0.0 \<in> carrier_mat d d; ?M1.0 \<in> carrier_mat d d; partial_density_operator ?\<rho>; \<And>\<rho>'. \<lbrakk>\<rho>' \<in> carrier_mat d d; partial_density_operator \<rho>'\<rbrakk> \<Longrightarrow> positive (?DS \<rho>') \<and> trace (?DS \<rho>') \<le> trace \<rho>' \<and> ?DS \<rho>' \<in> carrier_mat d d\<rbrakk> \<Longrightarrow> denote_while_n ?M0.0 ?M1.0 ?DS ?n ?\<rho> \<in> carrier_mat d d
\<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
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. \<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho> \<in> carrier_mat d d
[PROOF STEP]
have dimr: "(\<And>k. k < m \<Longrightarrow> c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> \<in> carrier_mat d d)"
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho> \<in> carrier_mat d d

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

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
have "\<forall> n<m. 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. \<forall>n<m. 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]
using denote_while_n_scale assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?c; measurement d 2 ?x1.0; well_com ?x2.0; \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>; trace (complex_of_real ?c \<cdot>\<^sub>m \<rho>) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x2.0 (complex_of_real ?c \<cdot>\<^sub>m \<rho>) = complex_of_real ?c \<cdot>\<^sub>m denote ?x2.0 \<rho>; ?\<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 0) (?x1.0 1) (denote ?x2.0) ?n (complex_of_real ?c \<cdot>\<^sub>m ?\<rho>) = complex_of_real ?c \<cdot>\<^sub>m denote_while_n (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?n ?\<rho>
\<rho> \<in> carrier_mat d d
partial_density_operator \<rho>
trace (complex_of_real c \<cdot>\<^sub>m \<rho>) \<le> 1
0 \<le> c
measurement d 2 x1
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. \<forall>n<m. 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]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n<m. 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>

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<m. 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]
have "(matrix_sum d (\<lambda>n. c \<cdot>\<^sub>m denote_while_n ?A ?B (denote x2) n \<rho>)) m =
      matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m "
[PROOF STATE]
proof (prove)
using this:
\<forall>n<m. 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>

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m
[PROOF STEP]
using matrix_sum_cong[of m "\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>"] dimr
[PROOF STATE]
proof (prove)
using this:
\<forall>n<m. 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>
(\<And>k. k < m \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> = ?f' k) \<Longrightarrow> matrix_sum ?d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum ?d ?f' m
?k < m \<Longrightarrow> complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho> \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
have "(matrix_sum d (\<lambda>n. c \<cdot>\<^sub>m denote_while_n ?A ?B (denote x2) n \<rho>)) m = c \<cdot>\<^sub>m (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>)) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
using matrix_sum_smult[of m "(\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>)" d c] dim
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho> \<in> carrier_mat d d) \<Longrightarrow> matrix_sum d (\<lambda>k. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho> \<in> carrier_mat d d

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) m
matrix_sum d (\<lambda>n. complex_of_real c \<cdot>\<^sub>m denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) m

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) ?m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) ?m

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) ?m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) ?m
[PROOF STEP]
have "matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) =
    matrix_seq.lowner_lub (\<lambda>n. c \<cdot>\<^sub>m (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>)) n)"
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>)) ?m = complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) ?m

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>
[PROOF STEP]
unfolding denote_while_def matrix_inf_sum_def
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. 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 matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
using llscale
[PROOF STATE]
proof (prove)
using this:
matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (complex_of_real c \<cdot>\<^sub>m \<rho>))) = matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n)
matrix_seq.lowner_lub (\<lambda>n. complex_of_real c \<cdot>\<^sub>m matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>) n) = complex_of_real c \<cdot>\<^sub>m matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. 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 matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
denote_while (x1 0) (x1 1) (denote x2) (complex_of_real c \<cdot>\<^sub>m \<rho>) = complex_of_real c \<cdot>\<^sub>m denote_while (x1 0) (x1 1) (denote x2) \<rho>

goal:
No subgoals!
[PROOF STEP]
qed