[STATEMENT]
lemma denote_while_add:
  assumes r1: "\<rho>\<^sub>1 \<in> carrier_mat d d" and
    r2: "\<rho>\<^sub>2 \<in> carrier_mat d d" and
    M0: "x1 0 \<in> carrier_mat d d" and
    M1: "x1 1 \<in> carrier_mat d d" and
    pdo1: "partial_density_operator \<rho>\<^sub>1" and
    pdo2: "partial_density_operator \<rho>\<^sub>2" and tr12: "trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1" and
    wc: "well_com x2" and mea: "measurement d 2 x1" and
    DS: "(\<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<rho>\<^sub>1 \<in> carrier_mat d d \<Longrightarrow> \<rho>\<^sub>2 \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho>\<^sub>1 \<Longrightarrow>
      partial_density_operator \<rho>\<^sub>2 \<Longrightarrow> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1 \<Longrightarrow> denote x2 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote x2 \<rho>\<^sub>1 + denote x2 \<rho>\<^sub>2)"
    shows
    "denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[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) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have dx2:"(\<And>\<rho>. \<rho> \<in> carrier_mat d d \<Longrightarrow> partial_density_operator \<rho> \<Longrightarrow> positive ((denote x2) \<rho>) \<and> trace ((denote x2) \<rho>) \<le> trace \<rho> \<and> (denote x2) \<rho> \<in> carrier_mat d d) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<rho>. \<lbrakk>\<rho> \<in> carrier_mat d d; partial_density_operator \<rho>\<rbrakk> \<Longrightarrow> positive (denote x2 \<rho>) \<and> trace (denote x2 \<rho>) \<le> trace \<rho> \<and> denote x2 \<rho> \<in> carrier_mat d d
[PROOF STEP]
using denote_positive_trace_dim wc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com ?S; ?\<rho> \<in> carrier_mat d d; partial_density_operator ?\<rho>\<rbrakk> \<Longrightarrow> positive (denote ?S ?\<rho>) \<and> trace (denote ?S ?\<rho>) \<le> trace ?\<rho> \<and> denote ?S ?\<rho> \<in> carrier_mat d d
well_com x2

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

goal (1 subgoal):
 1. adjoint (x1 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) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have pdo12: "partial_density_operator (\<rho>\<^sub>1 + \<rho>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_density_operator (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using pdo1 pdo2
[PROOF STATE]
proof (prove)
using this:
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2

goal (1 subgoal):
 1. partial_density_operator (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
unfolding partial_density_operator_def
[PROOF STATE]
proof (prove)
using this:
positive \<rho>\<^sub>1 \<and> trace \<rho>\<^sub>1 \<le> 1
positive \<rho>\<^sub>2 \<and> trace \<rho>\<^sub>2 \<le> 1

goal (1 subgoal):
 1. positive (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<and> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
[PROOF STEP]
using tr12 positive_add assms
[PROOF STATE]
proof (prove)
using this:
positive \<rho>\<^sub>1 \<and> trace \<rho>\<^sub>1 \<le> 1
positive \<rho>\<^sub>2 \<and> trace \<rho>\<^sub>2 \<le> 1
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
\<lbrakk>positive ?A; positive ?B; ?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> positive (?A + ?B)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have ms1: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>1))"
[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>\<^sub>1))
[PROOF STEP]
using denote_while_n_sum_mat_seq assms
[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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1))
[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>\<^sub>1))

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have ms2: "matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>2))"
[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>\<^sub>2))
[PROOF STEP]
using denote_while_n_sum_mat_seq assms
[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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

goal (1 subgoal):
 1. matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))
[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>\<^sub>2))

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

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

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

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>1) n +
               matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)"
    for n
[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>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>1) n) \<le> trace \<rho>\<^sub>1"
[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>\<^sub>1) n) \<le> trace \<rho>\<^sub>1
[PROOF STEP]
using denote_while_n_sum_trace dx2 lo1 assms
[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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n) \<le> trace \<rho>\<^sub>1
[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>\<^sub>1) n) \<le> trace \<rho>\<^sub>1

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[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>\<^sub>1) n) \<le> trace \<rho>\<^sub>1

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
have "trace (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>2) n) \<le> trace \<rho>\<^sub>2"
[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>\<^sub>2) n) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
using denote_while_n_sum_trace dx2 lo1 assms
[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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace \<rho>\<^sub>2
[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>\<^sub>2) n) \<le> trace \<rho>\<^sub>2

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[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>\<^sub>1) n) \<le> trace \<rho>\<^sub>1
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace \<rho>\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n) \<le> trace \<rho>\<^sub>1
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace \<rho>\<^sub>2

goal (1 subgoal):
 1. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
using trace_add_linear dim1 dim2
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n) \<le> trace \<rho>\<^sub>1
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace \<rho>\<^sub>2
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n\<rbrakk> \<Longrightarrow> trace (?A + ?B) = trace ?A + trace ?B
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n \<in> carrier_mat d d
\<forall>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n \<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>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
by (metis add_mono_thms_linordered_semiring(1) r1 r2)
[PROOF STATE]
proof (state)
this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) ?n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) ?n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
[PROOF STEP]
have "\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>2) n) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) ?n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) ?n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)

goal (1 subgoal):
 1. \<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> 1
[PROOF STEP]
using assms(7) dual_order.trans
[PROOF STATE]
proof (prove)
using this:
trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) ?n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) ?n) \<le> trace (\<rho>\<^sub>1 + \<rho>\<^sub>2)
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a

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

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

goal (1 subgoal):
 1. matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) = matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1)) + matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))
[PROOF STEP]
using lowner_lub_add ms1 ms2
[PROOF STATE]
proof (prove)
using this:
\<forall>n. trace (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) \<le> 1
\<lbrakk>matrix_seq ?d ?f; matrix_seq ?d ?g; \<forall>n. trace (?f n + ?g n) \<le> 1\<rbrakk> \<Longrightarrow> matrix_seq.lowner_lub (\<lambda>n. ?f n + ?g n) = matrix_seq.lowner_lub ?f + matrix_seq.lowner_lub ?g
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1))
matrix_seq d (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[PROOF STEP]
have "matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m =
    matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n ?A ?B (denote x2) n \<rho>\<^sub>2) 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 (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) 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 (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
have "(\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<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>\<^sub>1 + \<rho>\<^sub>2) \<in> carrier_mat d d
[PROOF STEP]
using denote_while_n_dim dx2 pdo12 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
partial_density_operator (\<rho>\<^sub>1 + \<rho>\<^sub>2)
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2
\<lbrakk>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>\<^sub>1 + \<rho>\<^sub>2) \<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>\<^sub>1 + \<rho>\<^sub>2) \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
have "(\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 \<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>\<^sub>1 \<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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2
\<lbrakk>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>\<^sub>1 \<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>\<^sub>1 \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>1 \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
have "(\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2 \<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>\<^sub>2 \<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>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2
\<lbrakk>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>\<^sub>2 \<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>\<^sub>2 \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>2 \<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>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
have "(\<forall>  k < m.
      denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k<m. denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2
[PROOF STEP]
using denote_while_n_add assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x1.0 0 \<in> carrier_mat d d; ?x1.0 1 \<in> carrier_mat d d; well_com ?x2.0; measurement d 2 ?x1.0; \<And>\<rho>\<^sub>1 \<rho>\<^sub>2. \<lbrakk>\<rho>\<^sub>1 \<in> carrier_mat d d; \<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator \<rho>\<^sub>1; partial_density_operator \<rho>\<^sub>2; trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote ?x2.0 (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote ?x2.0 \<rho>\<^sub>1 + denote ?x2.0 \<rho>\<^sub>2; ?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote_while_n (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?k (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote_while_n (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?k ?\<rho>\<^sub>1 + denote_while_n (?x1.0 0) (?x1.0 1) (denote ?x2.0) ?k ?\<rho>\<^sub>2
\<rho>\<^sub>1 \<in> carrier_mat d d
\<rho>\<^sub>2 \<in> carrier_mat d d
x1 0 \<in> carrier_mat d d
x1 1 \<in> carrier_mat d d
partial_density_operator \<rho>\<^sub>1
partial_density_operator \<rho>\<^sub>2
trace (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<le> 1
well_com x2
measurement d 2 x1
\<lbrakk>?\<rho>\<^sub>1 \<in> carrier_mat d d; ?\<rho>\<^sub>2 \<in> carrier_mat d d; partial_density_operator ?\<rho>\<^sub>1; partial_density_operator ?\<rho>\<^sub>2; trace (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) \<le> 1\<rbrakk> \<Longrightarrow> denote x2 (?\<rho>\<^sub>1 + ?\<rho>\<^sub>2) = denote x2 ?\<rho>\<^sub>1 + denote x2 ?\<rho>\<^sub>2

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

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>1 \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>2 \<in> carrier_mat d d
\<forall>k<m. denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>1 \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>2 \<in> carrier_mat d d
\<forall>k<m. denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m
[PROOF STEP]
using matrix_sum_add[of m "(\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2))" d "(\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1)"
        "(\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2)"]
[PROOF STATE]
proof (prove)
using this:
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>1 \<in> carrier_mat d d
?k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) ?k \<rho>\<^sub>2 \<in> carrier_mat d d
\<forall>k<m. denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2
\<lbrakk>\<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) \<in> carrier_mat d d; \<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 \<in> carrier_mat d d; \<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2 \<in> carrier_mat d d; \<And>k. k < m \<Longrightarrow> denote_while_n (x1 0) (x1 1) (denote x2) k (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>1 + denote_while_n (x1 0) (x1 1) (denote x2) k \<rho>\<^sub>2\<rbrakk> \<Longrightarrow> matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) m

goal (1 subgoal):
 1. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) 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 (\<rho>\<^sub>1 + \<rho>\<^sub>2)) m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) 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 (\<rho>\<^sub>1 + \<rho>\<^sub>2)) ?m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) ?m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) ?m

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

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n)
[PROOF STEP]
using lladd
[PROOF STATE]
proof (prove)
using this:
matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2)) ?m = matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) ?m + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) ?m
matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) = matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1)) + matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))

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

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[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 (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) 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 (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n)

goal (1 subgoal):
 1. denote_while (x1 0) (x1 1) (denote x2) (\<rho>\<^sub>1 + \<rho>\<^sub>2) = denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>1 + denote_while (x1 0) (x1 1) (denote x2) \<rho>\<^sub>2
[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 (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n)

goal (1 subgoal):
 1. matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1)) + matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))
[PROOF STEP]
using lladd
[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 (\<rho>\<^sub>1 + \<rho>\<^sub>2))) = matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n)
matrix_seq.lowner_lub (\<lambda>n. matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1) n + matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2) n) = matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>1)) + matrix_seq.lowner_lub (matrix_sum d (\<lambda>n. denote_while_n (x1 0) (x1 1) (denote x2) n \<rho>\<^sub>2))

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

goal:
No subgoals!
[PROOF STEP]
qed