[STATEMENT]
lemma next_free_weak_until [simp]:
  "next_free (\<phi> W\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. next_free (\<phi> W\<^sub>p \<psi>) = (next_free \<phi> \<and> next_free \<psi>)
[PROOF STEP]
by (auto simp: WeakUntil_ltlp_def)


[STATEMENT]
lemma step1_ref:
  "{ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} \<Union>r d_f o_f. tso_round1 r d_f o_f,
    BenOr_trans_step HOs HOs next1 send1 (Suc 0) {> ref_rel}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ref_rel \<inter> (TSO_inv1 \<inter> TSO_inv2) \<times> UNIV} \<Union>r d_f. \<Union> (range (tso_round1 r d_f)), BenOr_trans_step HOs HOs next1 send1 (Suc 0) {> ref_rel}
[PROOF STEP]
proof(clarsimp simp add: PO_rhoare_defs BenOr_trans_step_def all_conj_distrib)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
fix sa r cfg \<mu> and cfg' :: "process \<Rightarrow> val pstate"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
assume
    R: "(sa, (r, cfg)) \<in> ref_rel"
    and step_r: "two_step r = Suc 0"
    and send: "\<forall>p. \<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p"
    and step: "\<forall>p. next1 r p (cfg p) (\<mu> p) (cfg' p)"
    and ainv: "sa \<in> TSO_inv1"
    and ainv2: "sa \<in> TSO_inv2"
[PROOF STATE]
proof (state)
this:
(sa, r, cfg) \<in> ref_rel
two_step r = Suc 0
\<forall>p. \<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p
\<forall>p. next1 r p (cfg p) (\<mu> p) (cfg' p)
sa \<in> TSO_inv1
sa \<in> TSO_inv2

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
(sa, r, cfg) \<in> ref_rel
[PROOF STEP]
have next_r: "next_round sa = r"
[PROOF STATE]
proof (prove)
using this:
(sa, r, cfg) \<in> ref_rel

goal (1 subgoal):
 1. opt_obsv_state.next_round sa = r
[PROOF STEP]
by(simp add: ref_rel_def)
[PROOF STATE]
proof (state)
this:
opt_obsv_state.next_round sa = r

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define S where "S = {p. \<exists>v. vote (cfg p) = Some v}"
[PROOF STATE]
proof (state)
this:
S = {p. \<exists>v. vote (cfg p) = Some v}

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
(sa, r, cfg) \<in> ref_rel
[PROOF STEP]
obtain v where v: "\<forall>p \<in> S. vote (cfg p) = Some v"
[PROOF STATE]
proof (prove)
using this:
(sa, r, cfg) \<in> ref_rel

goal (1 subgoal):
 1. (\<And>v. \<forall>p\<in>S. vote (cfg p) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ainv step_r
[PROOF STATE]
proof (prove)
using this:
(sa, r, cfg) \<in> ref_rel
sa \<in> TSO_inv1
two_step r = Suc 0

goal (1 subgoal):
 1. (\<And>v. \<forall>p\<in>S. vote (cfg p) = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: ref_rel_def TSO_inv1_def S_def)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>S. vote (cfg p) = Some v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define Ob where "Ob = {p. x (cfg' p) = v}"
[PROOF STATE]
proof (state)
this:
Ob = {p. x (cfg' p) = v}

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define o_f where "o_f p = (if S \<in> Quorum then Some v else None)" for p :: process
[PROOF STATE]
proof (state)
this:
o_f ?p = (if S \<in> Quorum then Some v else None)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define dec_f where "dec_f p = (if p \<in> D cfg cfg' then decide (cfg' p) else None)" for p
[PROOF STATE]
proof (state)
this:
dec_f ?p = (if ?p \<in> D cfg cfg' then decide (cfg' ?p) else None)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dec_f ?p = (if ?p \<in> D cfg cfg' then decide (cfg' ?p) else None)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
fix p w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
assume "vote (cfg p) = Some w"
[PROOF STATE]
proof (state)
this:
vote (cfg p) = Some w

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
hence "w = v"
[PROOF STATE]
proof (prove)
using this:
vote (cfg p) = Some w

goal (1 subgoal):
 1. w = v
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
vote (cfg p) = Some w
\<forall>p\<in>S. vote (cfg p) = Some v

goal (1 subgoal):
 1. w = v
[PROOF STEP]
by(unfold S_def, auto)
[PROOF STATE]
proof (state)
this:
w = v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
vote (cfg ?p4) = Some ?w4 \<Longrightarrow> ?w4 = v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
note v'=this
[PROOF STATE]
proof (state)
this:
vote (cfg ?p4) = Some ?w4 \<Longrightarrow> ?w4 = v

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have d_guard: "d_guard dec_f (vote \<circ> cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_guard dec_f (vote \<circ> cfg)
[PROOF STEP]
using per_rd[THEN spec, of r]
[PROOF STATE]
proof (prove)
using this:
BenOr_commPerRd (HOs r)

goal (1 subgoal):
 1. d_guard dec_f (vote \<circ> cfg)
[PROOF STEP]
by(fastforce simp add: d_guard_def locked_in_vf_def quorum_for_def dec_f_def
      BenOr_commPerRd_def dest!: decide_origin[OF send step step_r, THEN subsetD])
[PROOF STATE]
proof (state)
this:
d_guard dec_f (vote \<circ> cfg)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have "dom (vote \<circ> cfg) \<in> Quorum \<longrightarrow> Ob = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (vote \<circ> cfg) \<in> Quorum \<longrightarrow> Ob = UNIV
[PROOF STEP]
proof(auto simp add: Ob_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
assume Q: "dom (vote \<circ> cfg) \<in> Quorum" (is "?Q \<in> Quorum")
[PROOF STATE]
proof (state)
this:
dom (vote \<circ> cfg) \<in> Quorum

goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
hence "?Q \<inter> HOs r p \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
dom (vote \<circ> cfg) \<in> Quorum

goal (1 subgoal):
 1. dom (vote \<circ> cfg) \<inter> HOs r p \<noteq> {}
[PROOF STEP]
using per_rd[THEN spec, of r]
[PROOF STATE]
proof (prove)
using this:
dom (vote \<circ> cfg) \<in> Quorum
BenOr_commPerRd (HOs r)

goal (1 subgoal):
 1. dom (vote \<circ> cfg) \<inter> HOs r p \<noteq> {}
[PROOF STEP]
by(auto simp add: BenOr_commPerRd_def dest: qintersect)
[PROOF STATE]
proof (state)
this:
dom (vote \<circ> cfg) \<inter> HOs r p \<noteq> {}

goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
hence "someVoteRcvd (\<mu> p) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
dom (vote \<circ> cfg) \<inter> HOs r p \<noteq> {}

goal (1 subgoal):
 1. someVoteRcvd (\<mu> p) \<noteq> {}
[PROOF STEP]
using send[THEN spec, of p]
[PROOF STATE]
proof (prove)
using this:
dom (vote \<circ> cfg) \<inter> HOs r p \<noteq> {}
\<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p

goal (1 subgoal):
 1. someVoteRcvd (\<mu> p) \<noteq> {}
[PROOF STEP]
by(force simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def
        isVote_def send1_def)
[PROOF STATE]
proof (state)
this:
someVoteRcvd (\<mu> p) \<noteq> {}

goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
someVoteRcvd (\<mu> p) \<noteq> {}

goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
have "\<forall>q \<in> someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))
[PROOF STEP]
using send[THEN spec, of p]
[PROOF STATE]
proof (prove)
using this:
\<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p

goal (1 subgoal):
 1. \<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))
[PROOF STEP]
by(auto simp add: someVoteRcvd_def get_msgs_benign msgRcvd_def restrict_map_def
        isVote_def send1_def dest: v')
[PROOF STATE]
proof (state)
this:
\<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))

goal (1 subgoal):
 1. \<And>xa. dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> x (cfg' xa) = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
someVoteRcvd (\<mu> p) \<noteq> {}
\<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))
[PROOF STEP]
show "x (cfg' p) = v"
[PROOF STATE]
proof (prove)
using this:
someVoteRcvd (\<mu> p) \<noteq> {}
\<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))

goal (1 subgoal):
 1. x (cfg' p) = v
[PROOF STEP]
using step[THEN spec, of p]
[PROOF STATE]
proof (prove)
using this:
someVoteRcvd (\<mu> p) \<noteq> {}
\<forall>q\<in>someVoteRcvd (\<mu> p). \<exists>x'. \<mu> p q = Some (Vote (Some v))
next1 r p (cfg p) (\<mu> p) (cfg' p)

goal (1 subgoal):
 1. x (cfg' p) = v
[PROOF STEP]
by(auto simp add: next1_def x_update_def)
[PROOF STATE]
proof (state)
this:
x (cfg' p) = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dom (vote \<circ> cfg) \<in> Quorum \<longrightarrow> Ob = UNIV

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
note Ob_UNIV=this[rule_format]
[PROOF STATE]
proof (state)
this:
dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> Ob = UNIV

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have obs_guard: "obs_guard o_f (vote \<circ> cfg)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_guard o_f (vote \<circ> cfg)
[PROOF STEP]
apply(auto simp add: obs_guard_def o_f_def S_def dom_def
      dest: v' Ob_UNIV quorum_non_empty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. \<exists>v. vote (cfg p) = Some v} \<in> Quorum \<Longrightarrow> \<exists>q. (\<exists>y. vote (cfg q) = Some y) \<and> Some v = vote (cfg q)
[PROOF STEP]
apply (metis S_def all_not_in_conv  empty_not_quorum v)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
obs_guard o_f (vote \<circ> cfg)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
define sa' where "sa' = sa\<lparr>
    next_round := Suc (next_round sa)
    , decisions := decisions sa ++ dec_f
    , last_obs := last_obs sa ++ o_f
    \<rparr>"

  \<comment> \<open>Abstract step\<close>
[PROOF STATE]
proof (state)
this:
sa' = sa\<lparr>opt_obsv_state.next_round := Suc (opt_obsv_state.next_round sa), opt_obsv_state.decisions := opt_obsv_state.decisions sa ++ dec_f, last_obs := last_obs sa ++ o_f\<rparr>

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have abs_step: "(sa, sa') \<in> tso_round1 r dec_f o_f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sa, sa') \<in> tso_round1 r dec_f o_f
[PROOF STEP]
using next_r step_r R d_guard obs_guard
[PROOF STATE]
proof (prove)
using this:
opt_obsv_state.next_round sa = r
two_step r = Suc 0
(sa, r, cfg) \<in> ref_rel
d_guard dec_f (vote \<circ> cfg)
obs_guard o_f (vote \<circ> cfg)

goal (1 subgoal):
 1. (sa, sa') \<in> tso_round1 r dec_f o_f
[PROOF STEP]
by(auto simp add: tso_round1_def sa'_def ref_rel_def)

  \<comment> \<open>Relation preserved\<close>
[PROOF STATE]
proof (state)
this:
(sa, sa') \<in> tso_round1 r dec_f o_f

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have "\<forall>p. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)
[PROOF STEP]
show "((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)
[PROOF STEP]
using step[THEN spec, of p]
[PROOF STATE]
proof (prove)
using this:
next1 r p (cfg p) (\<mu> p) (cfg' p)

goal (1 subgoal):
 1. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)
[PROOF STEP]
by(auto simp add: dec_f_def D_def next1_def dec_update_def map_add_def)
[PROOF STATE]
proof (state)
this:
((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p. ((decide \<circ> cfg) ++ dec_f) p = decide (cfg' p)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
note dec_rel=this[rule_format]
[PROOF STATE]
proof (state)
this:
((decide \<circ> cfg) ++ dec_f) ?p = decide (cfg' ?p)

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have "\<forall>p. (\<exists>q. o_f q = None \<and> opt_obsv_state.last_obs sa q = None
        \<or> (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
proof(intro allI impI, cases "S \<in> Quorum")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. S \<in> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
 2. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. S \<in> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
 2. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S \<in> Quorum

goal (2 subgoals):
 1. \<And>p. S \<in> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
 2. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
hence "x (cfg' p) = v"
[PROOF STATE]
proof (prove)
using this:
S \<in> Quorum

goal (1 subgoal):
 1. x (cfg' p) = v
[PROOF STEP]
using Ob_UNIV
[PROOF STATE]
proof (prove)
using this:
S \<in> Quorum
dom (vote \<circ> cfg) \<in> Quorum \<Longrightarrow> Ob = UNIV

goal (1 subgoal):
 1. x (cfg' p) = v
[PROOF STEP]
by(auto simp add: S_def Ob_def dom_def)
[PROOF STATE]
proof (state)
this:
x (cfg' p) = v

goal (2 subgoals):
 1. \<And>p. S \<in> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
 2. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
thus "(\<exists>q. o_f q = None \<and> opt_obsv_state.last_obs sa q = None
        \<or> (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))"
[PROOF STATE]
proof (prove)
using this:
x (cfg' p) = v

goal (1 subgoal):
 1. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x (cfg' p) = v
S \<in> Quorum

goal (1 subgoal):
 1. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
by(auto simp add: o_f_def)
[PROOF STATE]
proof (state)
this:
\<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S \<notin> Quorum

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
hence empty: "o_f = Map.empty"
[PROOF STATE]
proof (prove)
using this:
S \<notin> Quorum

goal (1 subgoal):
 1. o_f = Map.empty
[PROOF STEP]
by(auto simp add: o_f_def)
[PROOF STATE]
proof (state)
this:
o_f = Map.empty

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
S \<notin> Quorum
[PROOF STEP]
have "S \<noteq> UNIV"
[PROOF STATE]
proof (prove)
using this:
S \<notin> Quorum

goal (1 subgoal):
 1. S \<noteq> UNIV
[PROOF STEP]
using UNIV_quorum
[PROOF STATE]
proof (prove)
using this:
S \<notin> Quorum
UNIV \<in> Quorum

goal (1 subgoal):
 1. S \<noteq> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<noteq> UNIV

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> UNIV
[PROOF STEP]
obtain q where q: "vote (cfg q) = None"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> UNIV

goal (1 subgoal):
 1. (\<And>q. vote (cfg q) = None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
S \<noteq> UNIV
S \<notin> Quorum

goal (1 subgoal):
 1. (\<And>q. vote (cfg q) = None \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: o_f_def S_def)
[PROOF STATE]
proof (state)
this:
vote (cfg q) = None

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vote (cfg q) = None
[PROOF STEP]
obtain q1 q2 where
      "x (cfg q1) \<noteq> x (cfg q2)"
[PROOF STATE]
proof (prove)
using this:
vote (cfg q) = None

goal (1 subgoal):
 1. (\<And>q1 q2. x (cfg q1) \<noteq> x (cfg q2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using R step_r
[PROOF STATE]
proof (prove)
using this:
vote (cfg q) = None
(sa, r, cfg) \<in> ref_rel
two_step r = Suc 0

goal (1 subgoal):
 1. (\<And>q1 q2. x (cfg q1) \<noteq> x (cfg q2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: ref_rel_def no_vote_diff_def)
[PROOF STATE]
proof (state)
this:
x (cfg q1) \<noteq> x (cfg q2)

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x (cfg q1) \<noteq> x (cfg q2)
[PROOF STEP]
obtain q1' q2' where
      "x (cfg q1') = val0"
      "x (cfg q2') = val1"
[PROOF STATE]
proof (prove)
using this:
x (cfg q1) \<noteq> x (cfg q2)

goal (1 subgoal):
 1. (\<And>q1' q2'. \<lbrakk>x (cfg q1') = val0; x (cfg q2') = val1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (poly_guards_query) val_exhaust)
[PROOF STATE]
proof (state)
this:
x (cfg q1') = val0
x (cfg q2') = val1

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
hence "\<forall>v. \<exists>q. opt_obsv_state.last_obs sa q \<in> {None, Some v}"
[PROOF STATE]
proof (prove)
using this:
x (cfg q1') = val0
x (cfg q2') = val1

goal (1 subgoal):
 1. \<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}
[PROOF STEP]
using R step_r
[PROOF STATE]
proof (prove)
using this:
x (cfg q1') = val0
x (cfg q2') = val1
(sa, r, cfg) \<in> ref_rel
two_step r = Suc 0

goal (1 subgoal):
 1. \<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}
[PROOF STEP]
apply(auto simp add: ref_rel_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>x (cfg q1') = val0; x (cfg q2') = val1; two_step (opt_obsv_state.next_round sa) = Suc 0; r = opt_obsv_state.next_round sa; r_votes sa = vote \<circ> cfg; All (no_vote_diff cfg); \<forall>p. \<exists>q. last_obs sa q = None \<or> last_obs sa q = Some (x (cfg p)); opt_obsv_state.decisions sa = decide \<circ> cfg\<rbrakk> \<Longrightarrow> \<exists>q. last_obs sa q = None \<or> last_obs sa q = Some v
[PROOF STEP]
by (metis (poly_guards_query) val_exhaust)
[PROOF STATE]
proof (state)
this:
\<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
(* note x = x_origin2[OF send step step_r refl, of p] *)
[PROOF STATE]
proof (state)
this:
\<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}

goal (1 subgoal):
 1. \<And>p. S \<notin> Quorum \<Longrightarrow> \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
thus "(\<exists>q. o_f q = None \<and> opt_obsv_state.last_obs sa q = None
        \<or> (opt_obsv_state.last_obs sa ++ o_f) q = Some (x (cfg' p)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}

goal (1 subgoal):
 1. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
using empty
[PROOF STATE]
proof (prove)
using this:
\<forall>v. \<exists>q. last_obs sa q \<in> {None, Some v}
o_f = Map.empty

goal (1 subgoal):
 1. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p. \<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' p))

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
note obs_rel=this[rule_format]
[PROOF STATE]
proof (state)
this:
\<exists>q. o_f q = None \<and> last_obs sa q = None \<or> (last_obs sa ++ o_f) q = Some (x (cfg' ?p))

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
have post_rel:
    "(sa', Suc r, cfg') \<in> ref_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
using step send next_r R step_r
[PROOF STATE]
proof (prove)
using this:
\<forall>p. next1 r p (cfg p) (\<mu> p) (cfg' p)
\<forall>p. \<mu> p \<in> get_msgs (send1 r) cfg (HOs r) (HOs r) p
opt_obsv_state.next_round sa = r
(sa, r, cfg) \<in> ref_rel
two_step r = Suc 0

goal (1 subgoal):
 1. (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
by(auto simp add: sa'_def ref_rel_def
      two_step_phase_Suc dec_rel obs_rel)
[PROOF STATE]
proof (state)
this:
(sa', Suc r, cfg') \<in> ref_rel

goal (1 subgoal):
 1. \<And>a ab ba x cfg'. \<lbrakk>(a, ab, ba) \<in> ref_rel; a \<in> TSO_inv1; a \<in> TSO_inv2; two_step ab = Suc 0; \<forall>p. x p \<in> get_msgs (send1 ab) ba (HOs ab) (HOs ab) p; \<forall>p. next1 ab p (ba p) (x p) (cfg' p)\<rbrakk> \<Longrightarrow> \<exists>y. (\<exists>x xa xb. (a, y) \<in> tso_round1 x xa xb) \<and> (y, Suc ab, cfg') \<in> ref_rel
[PROOF STEP]
from abs_step post_rel
[PROOF STATE]
proof (chain)
picking this:
(sa, sa') \<in> tso_round1 r dec_f o_f
(sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
show
    "\<exists>sa'. (\<exists>r d_f o_f. (sa, sa') \<in> tso_round1 r d_f o_f) \<and> (sa', Suc r, cfg') \<in> ref_rel"
[PROOF STATE]
proof (prove)
using this:
(sa, sa') \<in> tso_round1 r dec_f o_f
(sa', Suc r, cfg') \<in> ref_rel

goal (1 subgoal):
 1. \<exists>sa'. (\<exists>r d_f o_f. (sa, sa') \<in> tso_round1 r d_f o_f) \<and> (sa', Suc r, cfg') \<in> ref_rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>sa'. (\<exists>r d_f o_f. (sa, sa') \<in> tso_round1 r d_f o_f) \<and> (sa', Suc r, cfg') \<in> ref_rel

goal:
No subgoals!
[PROOF STEP]
qed