[STATEMENT]
lemma wlp_mono_and_close:
  shows "well_com S \<Longrightarrow> is_quantum_predicate P \<Longrightarrow> is_quantum_predicate Q \<Longrightarrow> P \<le>\<^sub>L Q
        \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q
[PROOF STEP]
proof (induct S arbitrary: P Q)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>well_com SKIP; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp SKIP P) \<and> wlp SKIP P \<le>\<^sub>L wlp SKIP Q
 2. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 3. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 4. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 5. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
case SKIP
[PROOF STATE]
proof (state)
this:
well_com SKIP
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (5 subgoals):
 1. \<And>P Q. \<lbrakk>well_com SKIP; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp SKIP P) \<and> wlp SKIP P \<le>\<^sub>L wlp SKIP Q
 2. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 3. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 4. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 5. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com SKIP
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
well_com SKIP
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. is_quantum_predicate (wlp SKIP P) \<and> wlp SKIP P \<le>\<^sub>L wlp SKIP Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp SKIP P) \<and> wlp SKIP P \<le>\<^sub>L wlp SKIP Q

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
case (Utrans U)
[PROOF STATE]
proof (state)
this:
well_com (Utrans U)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
well_com (Utrans U)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
[PROOF STEP]
have dU: "U \<in> carrier_mat d d" and u: "unitary U" and qp: "is_quantum_predicate P"  and le: "P \<le>\<^sub>L Q"
    and dP: "P \<in> carrier_mat d d" and dQ: "Q \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans U)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. (U \<in> carrier_mat d d &&& unitary U &&& is_quantum_predicate P) &&& P \<le>\<^sub>L Q &&& P \<in> carrier_mat d d &&& Q \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
well_com (Utrans U)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. (U \<in> carrier_mat d d &&& unitary U &&& is_quantum_predicate P) &&& P \<le>\<^sub>L Q &&& P \<in> carrier_mat d d &&& Q \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U \<in> carrier_mat d d
unitary U
is_quantum_predicate P
P \<le>\<^sub>L Q
P \<in> carrier_mat d d
Q \<in> carrier_mat d d

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U \<in> carrier_mat d d
unitary U
is_quantum_predicate P
P \<le>\<^sub>L Q
P \<in> carrier_mat d d
Q \<in> carrier_mat d d
[PROOF STEP]
have qp': "is_quantum_predicate (wlp (Utrans U) P)"
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat d d
unitary U
is_quantum_predicate P
P \<le>\<^sub>L Q
P \<in> carrier_mat d d
Q \<in> carrier_mat d d

goal (1 subgoal):
 1. is_quantum_predicate (wlp (Utrans U) P)
[PROOF STEP]
using qp_close_under_unitary_operator
[PROOF STATE]
proof (prove)
using this:
U \<in> carrier_mat d d
unitary U
is_quantum_predicate P
P \<le>\<^sub>L Q
P \<in> carrier_mat d d
Q \<in> carrier_mat d d
\<lbrakk>?U \<in> carrier_mat d d; unitary ?U; is_quantum_predicate ?P\<rbrakk> \<Longrightarrow> is_quantum_predicate (adjoint ?U * ?P * ?U)

goal (1 subgoal):
 1. is_quantum_predicate (wlp (Utrans U) P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (Utrans U) P)

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (Utrans U) P)

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dU dP dQ le]
[PROOF STATE]
proof (prove)
using this:
adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U

goal (1 subgoal):
 1. adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U

goal (4 subgoals):
 1. \<And>x P Q. \<lbrakk>well_com (Utrans x); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Utrans x) P) \<and> wlp (Utrans x) P \<le>\<^sub>L wlp (Utrans x) Q
 2. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 3. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 4. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp (Utrans U) P)
adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (Utrans U) P)
adjoint U * P * U \<le>\<^sub>L adjoint U * Q * U

goal (1 subgoal):
 1. is_quantum_predicate (wlp (Utrans U) P) \<and> wlp (Utrans U) P \<le>\<^sub>L wlp (Utrans U) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (Utrans U) P) \<and> wlp (Utrans U) P \<le>\<^sub>L wlp (Utrans U) Q

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
case (Seq S1 S2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com (S1;; S2)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com (S1;; S2)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
[PROOF STEP]
have qpP: "is_quantum_predicate P" and qpQ: "is_quantum_predicate Q" and wc1: "well_com S1" and wc2: "well_com S2"
    and dP: "P \<in> carrier_mat d d" and dQ: "Q \<in> carrier_mat d d" and le: "P \<le>\<^sub>L Q"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com (S1;; S2)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. (is_quantum_predicate P &&& is_quantum_predicate Q &&& well_com S1) &&& (well_com S2 &&& P \<in> carrier_mat d d) &&& Q \<in> carrier_mat d d &&& P \<le>\<^sub>L Q
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com (S1;; S2)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. (is_quantum_predicate P &&& is_quantum_predicate Q &&& well_com S1) &&& (well_com S2 &&& P \<in> carrier_mat d d) &&& Q \<in> carrier_mat d d &&& P \<le>\<^sub>L Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate P
is_quantum_predicate Q
well_com S1
well_com S2
P \<in> carrier_mat d d
Q \<in> carrier_mat d d
P \<le>\<^sub>L Q

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have qpP2: "is_quantum_predicate (wlp S2 P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S2 P)
[PROOF STEP]
using Seq qpP wc2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com (S1;; S2)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
is_quantum_predicate P
well_com S2

goal (1 subgoal):
 1. is_quantum_predicate (wlp S2 P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S2 P)

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have qpQ2: "is_quantum_predicate (wlp S2 Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S2 Q)
[PROOF STEP]
using Seq(2)[OF wc2 qpQ qpQ] lowner_le_refl dQ
[PROOF STATE]
proof (prove)
using this:
Q \<le>\<^sub>L Q \<Longrightarrow> is_quantum_predicate (wlp S2 Q) \<and> wlp S2 Q \<le>\<^sub>L wlp S2 Q
?A \<in> carrier_mat ?n ?n \<Longrightarrow> ?A \<le>\<^sub>L ?A
Q \<in> carrier_mat d d

goal (1 subgoal):
 1. is_quantum_predicate (wlp S2 Q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S2 Q)

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have qpP1: "is_quantum_predicate (wlp S1 (wlp S2 P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S1 (wlp S2 P))
[PROOF STEP]
using Seq(1)[OF wc1 qpP2 qpP2] qpP2 is_quantum_predicate_def[of "wlp S2 P"] lowner_le_refl
[PROOF STATE]
proof (prove)
using this:
wlp S2 P \<le>\<^sub>L wlp S2 P \<Longrightarrow> is_quantum_predicate (wlp S1 (wlp S2 P)) \<and> wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 P)
is_quantum_predicate (wlp S2 P)
is_quantum_predicate (wlp S2 P) = (wlp S2 P \<in> carrier_mat d d \<and> positive (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L 1\<^sub>m d)
?A \<in> carrier_mat ?n ?n \<Longrightarrow> ?A \<le>\<^sub>L ?A

goal (1 subgoal):
 1. is_quantum_predicate (wlp S1 (wlp S2 P))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S1 (wlp S2 P))

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "wlp S2 P \<le>\<^sub>L wlp S2 Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp S2 P \<le>\<^sub>L wlp S2 Q
[PROOF STEP]
using Seq(2) wc2 qpP qpQ le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S2; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 ?P) \<and> wlp S2 ?P \<le>\<^sub>L wlp S2 ?Q
well_com S2
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. wlp S2 P \<le>\<^sub>L wlp S2 Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp S2 P \<le>\<^sub>L wlp S2 Q

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wlp S2 P \<le>\<^sub>L wlp S2 Q
[PROOF STEP]
have "wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)"
[PROOF STATE]
proof (prove)
using this:
wlp S2 P \<le>\<^sub>L wlp S2 Q

goal (1 subgoal):
 1. wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)
[PROOF STEP]
using Seq(1) wc1 qpP2 qpQ2
[PROOF STATE]
proof (prove)
using this:
wlp S2 P \<le>\<^sub>L wlp S2 Q
\<lbrakk>well_com S1; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 ?P) \<and> wlp S1 ?P \<le>\<^sub>L wlp S1 ?Q
well_com S1
is_quantum_predicate (wlp S2 P)
is_quantum_predicate (wlp S2 Q)

goal (1 subgoal):
 1. wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)

goal (3 subgoals):
 1. \<And>S1 S2 P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S1; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S1 P) \<and> wlp S1 P \<le>\<^sub>L wlp S1 Q; \<And>P Q. \<lbrakk>well_com S2; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S2 P) \<and> wlp S2 P \<le>\<^sub>L wlp S2 Q; well_com (S1;; S2); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
 2. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 3. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)

goal (1 subgoal):
 1. is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
[PROOF STEP]
using qpP1
[PROOF STATE]
proof (prove)
using this:
wlp S1 (wlp S2 P) \<le>\<^sub>L wlp S1 (wlp S2 Q)
is_quantum_predicate (wlp S1 (wlp S2 P))

goal (1 subgoal):
 1. is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (S1;; S2) P) \<and> wlp (S1;; S2) P \<le>\<^sub>L wlp (S1;; S2) Q

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
case (Measure n M S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?x3a ?P) \<and> wlp ?x3a ?P \<le>\<^sub>L wlp ?x3a ?Q
well_com (Measure n M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?x3a ?P) \<and> wlp ?x3a ?P \<le>\<^sub>L wlp ?x3a ?Q
well_com (Measure n M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
[PROOF STEP]
have wc: "well_com (Measure n M S)" and wck: "k < n \<Longrightarrow> well_com (S!k)" and l: "length S = n"
    and m: "measurement d n M" and le: "P \<le>\<^sub>L Q"
    and qpP: "is_quantum_predicate P" and dP: "P \<in> carrier_mat d d"
    and qpQ: "is_quantum_predicate Q" and dQ: "Q \<in> carrier_mat d d"
    for k
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?x3a ?P) \<and> wlp ?x3a ?P \<le>\<^sub>L wlp ?x3a ?Q
well_com (Measure n M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. ((well_com (Measure n M S) &&& (k < n \<Longrightarrow> well_com (S ! k))) &&& length S = n &&& measurement d n M) &&& (P \<le>\<^sub>L Q &&& is_quantum_predicate P) &&& P \<in> carrier_mat d d &&& is_quantum_predicate Q &&& Q \<in> carrier_mat d d
[PROOF STEP]
using measure_well_com is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3a \<in> set S; well_com ?x3a; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp ?x3a ?P) \<and> wlp ?x3a ?P \<le>\<^sub>L wlp ?x3a ?Q
well_com (Measure n M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
\<lbrakk>well_com (Measure ?n ?M ?S); ?k < ?n\<rbrakk> \<Longrightarrow> well_com (?S ! ?k)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. ((well_com (Measure n M S) &&& (k < n \<Longrightarrow> well_com (S ! k))) &&& length S = n &&& measurement d n M) &&& (P \<le>\<^sub>L Q &&& is_quantum_predicate P) &&& P \<in> carrier_mat d d &&& is_quantum_predicate Q &&& Q \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_com (Measure n M S)
?k < n \<Longrightarrow> well_com (S ! ?k)
length S = n
measurement d n M
P \<le>\<^sub>L Q
is_quantum_predicate P
P \<in> carrier_mat d d
is_quantum_predicate Q
Q \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have dMk: "k < n \<Longrightarrow> M k \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> M k \<in> carrier_mat d d
[PROOF STEP]
using m measurement_def
[PROOF STATE]
proof (prove)
using this:
measurement d n M
measurement ?d ?n ?M = ((\<forall>j<?n. ?M j \<in> carrier_mat ?d ?d) \<and> matrix_sum ?d (\<lambda>j. adjoint (?M j) * ?M j) ?n = 1\<^sub>m ?d)

goal (1 subgoal):
 1. k < n \<Longrightarrow> M k \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have set: "k < n \<Longrightarrow> S!k \<in> set S" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> S ! k \<in> set S
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
length S = n

goal (1 subgoal):
 1. k < n \<Longrightarrow> S ! k \<in> set S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> S ! ?k \<in> set S

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have qpk: "k < n \<Longrightarrow> is_quantum_predicate (wlp (S!k) P)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! k) P)
[PROOF STEP]
using Measure(1)[OF set wck qpP qpP] lowner_le_refl[of P] dP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k1 < n; ?k1 < n; P \<le>\<^sub>L P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k1) P) \<and> wlp (S ! ?k1) P \<le>\<^sub>L wlp (S ! ?k1) P
P \<in> carrier_mat ?n ?n \<Longrightarrow> P \<le>\<^sub>L P
P \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! k) P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)
[PROOF STEP]
have dWkP: "k < n \<Longrightarrow> wlp (S!k) P \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)

goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) P \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) P \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<in> carrier_mat d d
[PROOF STEP]
have dMkP: "k < n \<Longrightarrow> adjoint (M k) * (wlp (S!k) P) * (M k) \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) P * M k \<in> carrier_mat d d
[PROOF STEP]
using dMk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<in> carrier_mat d d
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) P * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "k < n \<Longrightarrow> is_quantum_predicate (wlp (S!k) Q)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! k) Q)
[PROOF STEP]
using Measure(1)[OF set wck qpQ qpQ] lowner_le_refl[of Q] dQ
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k1 < n; ?k1 < n; Q \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k1) Q) \<and> wlp (S ! ?k1) Q \<le>\<^sub>L wlp (S ! ?k1) Q
Q \<in> carrier_mat ?n ?n \<Longrightarrow> Q \<le>\<^sub>L Q
Q \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! k) Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) Q)

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) Q)
[PROOF STEP]
have dWkQ: "k < n \<Longrightarrow> wlp (S!k) Q \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) Q)

goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) Q \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) Q)
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) Q \<in> carrier_mat d d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> wlp (S ! ?k) Q \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> wlp (S ! ?k) Q \<in> carrier_mat d d
[PROOF STEP]
have dMkQ: "k < n \<Longrightarrow> adjoint (M k) * (wlp (S!k) Q) * (M k) \<in> carrier_mat d d" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) Q \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) Q * M k \<in> carrier_mat d d
[PROOF STEP]
using dMk
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) Q \<in> carrier_mat d d
?k < n \<Longrightarrow> M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) Q * M k \<in> carrier_mat d d
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) Q * M ?k \<in> carrier_mat d d

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "k < n \<Longrightarrow> wlp (S!k) P \<le>\<^sub>L wlp (S!k) Q" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) P \<le>\<^sub>L wlp (S ! k) Q
[PROOF STEP]
using Measure(1)[OF set wck qpP qpQ le]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?k1 < n; ?k1 < n\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k1) P) \<and> wlp (S ! ?k1) P \<le>\<^sub>L wlp (S ! ?k1) Q

goal (1 subgoal):
 1. k < n \<Longrightarrow> wlp (S ! k) P \<le>\<^sub>L wlp (S ! k) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<le>\<^sub>L wlp (S ! ?k) Q

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<le>\<^sub>L wlp (S ! ?k) Q
[PROOF STEP]
have "k < n \<Longrightarrow> adjoint (M k) * (wlp (S!k) P) * (M k) \<le>\<^sub>L adjoint (M k) * (wlp (S!k) Q) * (M k)" for k
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<le>\<^sub>L wlp (S ! ?k) Q

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) P * M k \<le>\<^sub>L adjoint (M k) * wlp (S ! k) Q * M k
[PROOF STEP]
using lowner_le_keep_under_measurement[OF dMk dWkP dWkQ]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> wlp (S ! ?k) P \<le>\<^sub>L wlp (S ! ?k) Q
\<lbrakk>?k3 < n; ?k2 < n; ?k1 < n; wlp (S ! ?k2) P \<le>\<^sub>L wlp (S ! ?k1) Q\<rbrakk> \<Longrightarrow> adjoint (M ?k3) * wlp (S ! ?k2) P * M ?k3 \<le>\<^sub>L adjoint (M ?k3) * wlp (S ! ?k1) Q * M ?k3

goal (1 subgoal):
 1. k < n \<Longrightarrow> adjoint (M k) * wlp (S ! k) P * M k \<le>\<^sub>L adjoint (M k) * wlp (S ! k) Q * M k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<le>\<^sub>L adjoint (M ?k) * wlp (S ! ?k) Q * M ?k

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<le>\<^sub>L adjoint (M ?k) * wlp (S ! ?k) Q * M ?k
[PROOF STEP]
have le': "wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q"
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<le>\<^sub>L adjoint (M ?k) * wlp (S ! ?k) Q * M ?k

goal (1 subgoal):
 1. wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q
[PROOF STEP]
unfolding wlp_measure_expand[OF wc]
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<le>\<^sub>L adjoint (M ?k) * wlp (S ! ?k) Q * M ?k

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n \<le>\<^sub>L matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) Q * M k) n
[PROOF STEP]
using lowner_le_matrix_sum dMkP dMkQ
[PROOF STATE]
proof (prove)
using this:
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<le>\<^sub>L adjoint (M ?k) * wlp (S ! ?k) Q * M ?k
\<lbrakk>\<And>k. k < ?n \<Longrightarrow> ?f k \<in> carrier_mat ?d ?d; \<And>k. k < ?n \<Longrightarrow> ?g k \<in> carrier_mat ?d ?d; \<And>k. k < ?n \<Longrightarrow> ?f k \<le>\<^sub>L ?g k\<rbrakk> \<Longrightarrow> matrix_sum ?d ?f ?n \<le>\<^sub>L matrix_sum ?d ?g ?n
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) P * M ?k \<in> carrier_mat d d
?k < n \<Longrightarrow> adjoint (M ?k) * wlp (S ! ?k) Q * M ?k \<in> carrier_mat d d

goal (1 subgoal):
 1. matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n \<le>\<^sub>L matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) Q * M k) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have qp': "is_quantum_predicate (wlp (Measure n M S) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp (Measure n M S) P)
[PROOF STEP]
unfolding wlp_measure_expand[OF wc]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n)
[PROOF STEP]
using qps_after_measure_is_qp[OF m] qpk
[PROOF STATE]
proof (prove)
using this:
(\<And>k. k < n \<Longrightarrow> is_quantum_predicate (?P k)) \<Longrightarrow> is_quantum_predicate (matrix_sum d (\<lambda>k. adjoint (M k) * ?P k * M k) n)
?k < n \<Longrightarrow> is_quantum_predicate (wlp (S ! ?k) P)

goal (1 subgoal):
 1. is_quantum_predicate (matrix_sum d (\<lambda>k. adjoint (M k) * wlp (S ! k) P * M k) n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (Measure n M S) P)

goal (2 subgoals):
 1. \<And>x1 x2a x3 P Q. \<lbrakk>\<And>x3a P Q. \<lbrakk>x3a \<in> set x3; well_com x3a; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp x3a P) \<and> wlp x3a P \<le>\<^sub>L wlp x3a Q; well_com (Measure x1 x2a x3); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (Measure x1 x2a x3) P) \<and> wlp (Measure x1 x2a x3) P \<le>\<^sub>L wlp (Measure x1 x2a x3) Q
 2. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp (Measure n M S) P) \<and> wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q
[PROOF STEP]
using le' qp'
[PROOF STATE]
proof (prove)
using this:
wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q
is_quantum_predicate (wlp (Measure n M S) P)

goal (1 subgoal):
 1. is_quantum_predicate (wlp (Measure n M S) P) \<and> wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (Measure n M S) P) \<and> wlp (Measure n M S) P \<le>\<^sub>L wlp (Measure n M S) Q

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
case (While M S)
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_com S; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S ?P) \<and> wlp S ?P \<le>\<^sub>L wlp S ?Q
well_com (While M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_com S; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S ?P) \<and> wlp S ?P \<le>\<^sub>L wlp S ?Q
well_com (While M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q
[PROOF STEP]
have m: "measurement d 2 M" and wcs: "well_com S"
    and qpP: "is_quantum_predicate P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_com S; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S ?P) \<and> wlp S ?P \<le>\<^sub>L wlp S ?Q
well_com (While M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. measurement d 2 M &&& well_com S &&& is_quantum_predicate P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
measurement d 2 M
well_com S
is_quantum_predicate P

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have closeWS: "is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P)" for P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P)
[PROOF STEP]
assume asm: "is_quantum_predicate P"
[PROOF STATE]
proof (state)
this:
is_quantum_predicate P

goal (1 subgoal):
 1. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate P
[PROOF STEP]
have dP: "P \<in> carrier_mat d d"
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P

goal (1 subgoal):
 1. P \<in> carrier_mat d d
[PROOF STEP]
using is_quantum_predicate_def
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate P
is_quantum_predicate ?P = (?P \<in> carrier_mat d d \<and> positive ?P \<and> ?P \<le>\<^sub>L 1\<^sub>m d)

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

goal (1 subgoal):
 1. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<in> carrier_mat d d
[PROOF STEP]
show "is_quantum_predicate (wlp S P)"
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat d d

goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
using While(1)[OF wcs asm asm lowner_le_refl] dP
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat d d
P \<in> carrier_mat ?n1 ?n1 \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S P
P \<in> carrier_mat d d

goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp S P)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (wlp S ?P)

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have monoWS: "is_quantum_predicate P \<Longrightarrow> is_quantum_predicate Q \<Longrightarrow> P \<le>\<^sub>L Q \<Longrightarrow> wlp S P \<le>\<^sub>L wlp S Q" for P Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> wlp S P \<le>\<^sub>L wlp S Q
[PROOF STEP]
using While(1)[OF wcs]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S ?P) \<and> wlp S ?P \<le>\<^sub>L wlp S ?Q

goal (1 subgoal):
 1. \<lbrakk>is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> wlp S P \<le>\<^sub>L wlp S Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> wlp S ?P \<le>\<^sub>L wlp S ?Q

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "is_quantum_predicate (wlp (While M S) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
using wlp_while_exists[of "wlp S" M P] closeWS monoWS m qpP
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P); \<And>P Q. \<lbrakk>is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> wlp S P \<le>\<^sub>L wlp S Q; measurement d 2 M; is_quantum_predicate P\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp_while (M 0) (M 1) (wlp S) P) \<and> (\<forall>n. wlp_while (M 0) (M 1) (wlp S) P \<le>\<^sub>L wlp_while_n (M 0) (M 1) (wlp S) n P) \<and> (\<forall>W'. (\<forall>n. W' \<le>\<^sub>L wlp_while_n (M 0) (M 1) (wlp S) n P) \<longrightarrow> W' \<le>\<^sub>L wlp_while (M 0) (M 1) (wlp S) P) \<and> limit_mat (\<lambda>n. wlp_while_n (M 0) (M 1) (wlp S) n P) (wlp_while (M 0) (M 1) (wlp S) P) d
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (wlp S ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> wlp S ?P \<le>\<^sub>L wlp S ?Q
measurement d 2 M
is_quantum_predicate P

goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (While M S) P)

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (While M S) P)

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
have "wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q
[PROOF STEP]
using wlp_while_mono[of "wlp S" M P Q] closeWS monoWS m While
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>P. is_quantum_predicate P \<Longrightarrow> is_quantum_predicate (wlp S P); \<And>P Q. \<lbrakk>is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> wlp S P \<le>\<^sub>L wlp S Q; measurement d 2 M; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> wlp_while (M 0) (M 1) (wlp S) P \<le>\<^sub>L wlp_while (M 0) (M 1) (wlp S) Q
is_quantum_predicate ?P \<Longrightarrow> is_quantum_predicate (wlp S ?P)
\<lbrakk>is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> wlp S ?P \<le>\<^sub>L wlp S ?Q
measurement d 2 M
\<lbrakk>well_com S; is_quantum_predicate ?P; is_quantum_predicate ?Q; ?P \<le>\<^sub>L ?Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S ?P) \<and> wlp S ?P \<le>\<^sub>L wlp S ?Q
well_com (While M S)
is_quantum_predicate P
is_quantum_predicate Q
P \<le>\<^sub>L Q

goal (1 subgoal):
 1. wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q

goal (1 subgoal):
 1. \<And>x1 S P Q. \<lbrakk>\<And>P Q. \<lbrakk>well_com S; is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S Q; well_com (While x1 S); is_quantum_predicate P; is_quantum_predicate Q; P \<le>\<^sub>L Q\<rbrakk> \<Longrightarrow> is_quantum_predicate (wlp (While x1 S) P) \<and> wlp (While x1 S) P \<le>\<^sub>L wlp (While x1 S) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_quantum_predicate (wlp (While M S) P)
wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
is_quantum_predicate (wlp (While M S) P)
wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q

goal (1 subgoal):
 1. is_quantum_predicate (wlp (While M S) P) \<and> wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_quantum_predicate (wlp (While M S) P) \<and> wlp (While M S) P \<le>\<^sub>L wlp (While M S) Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wlp_close:
  assumes wc: "well_com S" and qp: "is_quantum_predicate P"
  shows "is_quantum_predicate (wlp S P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
using wlp_mono_and_close[OF wc qp qp] is_quantum_predicate_def[of P] qp lowner_le_refl
[PROOF STATE]
proof (prove)
using this:
P \<le>\<^sub>L P \<Longrightarrow> is_quantum_predicate (wlp S P) \<and> wlp S P \<le>\<^sub>L wlp S P
is_quantum_predicate P = (P \<in> carrier_mat d d \<and> positive P \<and> P \<le>\<^sub>L 1\<^sub>m d)
is_quantum_predicate P
?A \<in> carrier_mat ?n ?n \<Longrightarrow> ?A \<le>\<^sub>L ?A

goal (1 subgoal):
 1. is_quantum_predicate (wlp S P)
[PROOF STEP]
by auto