Quelle  UteProof.thy

theory UteProof
imports UteDefs "../Majorities" "../Reduction"
begin

context ute_parameters
begin

subsection ‹Preliminary Lemmas›

text ‹Processes can make a vote only at first round of each phase.›

lemma vote_step:
  assumes  nxt: "nextState Ute_M r p (rho r p) μ (rho (Suc r) p)"
  and "vote (rho (Suc r) p) ≠ None"
  shows "step r = 0"
proof (rule ccontr)
  assume "step r ≠ 0"
  with assms have "vote (rho (Suc r) p) = None"
    by (auto simp:Ute_SHOMachine_def nextState_def Ute_nextState_def next1_def)
  with assms show False by auto
qed

text ‹Processes can make a new decision only at second round of each phase.›

lemma decide_step:
  assumes run: "SHORun Ute_M rho HOs SHOs"
  and d1: "decide (rho r p) ≠ Some v"
  and d2: "decide (rho (Suc r) p) = Some v"
  shows "step r ≠ 0"
proof
  assume sr:"step r = 0"
  from run obtain μ where "Ute_nextState r p (rho r p) μ (rho (Suc r) p)"
    unfolding Ute_SHOMachine_def nextState_def SHORun_eq SHOnextConfig_eq 
    by force
  with sr have "next0 r p (rho r p) μ (rho (Suc r) p)"
    unfolding Ute_nextState_def by auto
  hence "decide (rho r p) = decide (rho (Suc r) p)" 
    by (auto simp:next0_def)
  with d1 d2 show False by auto
qed

lemma unique_majority_E:
  assumes majv: "card {qq::Proc. F qq = Some m} > E"
  and majw: "card {qq::Proc. F qq = Some m'} > E"
  shows "m = m'"
proof -
  from majv majw majE 
  have "card {qq::Proc. F qq = Some m} > N div 2"
    and "card {qq::Proc. F qq = Some m'} > N div 2"
    by auto
  then obtain qq
    where "qq ∈ {qq::Proc. F qq = Some m}"
      and "qq ∈ {qq::Proc. F qq = Some m'}"
    by (rule majoritiesE')
  thus ?thesis by auto
qed

lemma unique_majority_E_α:
  assumes majv: "card {qq::Proc. F qq = m} > E - α"
  and majw: "card {qq::Proc. F qq = m'} > E - α"
  shows "m = m'"
proof -
  from majE alpha_lt_N majv majw
  have "card {qq::Proc. F qq = m} > N div 2"
    and "card {qq::Proc. F qq = m'} > N div 2"
    by auto
  then obtain qq
    where "qq ∈ {qq::Proc. F qq = m}"
      and "qq ∈ {qq::Proc. F qq = m'}"
    by (rule majoritiesE')
  thus ?thesis by auto
qed

lemma unique_majority_T:
  assumes majv: "card {qq::Proc. F qq = Some m} > T"
  and majw: "card {qq::Proc. F qq = Some m'} > T"
  shows "m = m'"
proof -
  from majT majv majw
  have "card {qq::Proc. F qq = Some m} > N div 2"
    and "card {qq::Proc. F qq = Some m'} > N div 2"
    by auto
  then obtain qq
    where "qq ∈ {qq::Proc. F qq = Some m}"
      and "qq ∈ {qq::Proc. F qq = Some m'}"
    by (rule majoritiesE')
  thus ?thesis by auto
qed

text ‹No two processes may vote for different values in the same round.›

lemma common_vote:
  assumes usafe: "SHOcommPerRd Ute_M HO SHO"
  and nxtp: "nextState Ute_M r p (rho r p) μp (rho (Suc r) p)"
  and mup: "μp ∈ SHOmsgVectors Ute_M r p (rho r) (HO p) (SHO p)"
  and nxtq: "nextState Ute_M r q (rho r q) μq (rho (Suc r) q)"
  and muq: "μq ∈ SHOmsgVectors Ute_M r q (rho r) (HO q) (SHO q)"
  and vp: "vote (rho (Suc r) p) = Some vp"
  and vq: "vote (rho (Suc r) q) = Some vq"
  shows "vp = vq"
using assms proof -
  have gtn: "card {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
           + card {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} > N"
  proof -
    have "card {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp} > T - α
        ∧ card {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} > T - α"
      (is "card ?vsentp > _ ∧ card ?vsentq > _")
    proof -
      from nxtp vp have stp:"step r = 0" by (auto simp: vote_step)
      from mup
      have "{qq. μp qq = Some (Val vp)} - (HO p - SHO p)
             ⊆ {qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}"
             (is "?vrcvdp - ?ahop ⊆ ?vsentp") 
         by (auto simp: SHOmsgVectors_def)
      hence "card (?vrcvdp - ?ahop) ≤ card ?vsentp"
        and "card (?vrcvdp - ?ahop) ≥ card ?vrcvdp - card ?ahop"
        by (auto simp: card_mono diff_card_le_card_Diff)
      hence "card ?vsentp ≥ card ?vrcvdp - card ?ahop" by auto
      moreover
      from nxtp stp have "next0 r p (rho r p) μp (rho (Suc r) p)"
        by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
      with vp have "card ?vrcvdp > T"
        unfolding next0_def by auto
      moreover
      from muq
      have "{qq. μq qq = Some (Val vq)} - (HO q - SHO q)
             ⊆ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}"
             (is "?vrcvdq - ?ahoq ⊆ ?vsentq") 
        by (auto simp: SHOmsgVectors_def)
      hence "card (?vrcvdq - ?ahoq) ≤ card ?vsentq"
        and "card (?vrcvdq - ?ahoq) ≥ card ?vrcvdq - card ?ahoq"
        by (auto simp: card_mono diff_card_le_card_Diff)
      hence "card ?vsentq ≥ card ?vrcvdq - card ?ahoq" by auto
      moreover
      from nxtq stp have "next0 r q (rho r q) μq (rho (Suc r) q)"
        by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
      with vq have "card {qq. μq qq = Some (Val vq)} > T" 
        by (unfold next0_def, auto)
      moreover
      from usafe have "card ?ahop ≤ α" and "card ?ahoq ≤ α"
        by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
      ultimately
      show ?thesis using alpha_lt_T by auto
    qed
    thus ?thesis using majT by auto
  qed

  show ?thesis
  proof (rule ccontr)
    assume vpq:"vp ≠ vq"
    have "∀qq. sendMsg Ute_M r qq p (rho r qq)
               = sendMsg Ute_M r qq q (rho r qq)"
      by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def 
                     step_def send0_def send1_def)
    with vpq 
    have "{qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
           ∩ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq} = {}" 
      by auto
    with gtn
    have "card ({qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
                  ∪ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}) > N"
      by (auto simp: card_Un_Int)
    moreover
    have "card ({qq. sendMsg Ute_M r qq p (rho r qq) = Val vp}
                  ∪ {qq. sendMsg Ute_M r qq q (rho r qq) = Val vq}) ≤ N"
      by (auto simp: card_mono)
    ultimately
    show "False" by auto
  qed
qed

text ‹
 No decision may be taken by a process unless it received enough messages
 holding the same value.
 ›
(*
  The proof mainly relies on lemma @{text decide_step}
  and the @{text Ute_commPerRound} predicate. 
*)

lemma decide_with_threshold_E:
  assumes run: "SHORun Ute_M rho HOs SHOs" 
  and usafe: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and d1: "decide (rho r p) ≠ Some v"
  and d2: "decide (rho (Suc r) p) = Some v"
  shows "card {q. sendMsg Ute_M r q p (rho r q) = Vote (Some v)}
           > E - α"
proof -
  from run obtain μp
    where nxt:"nextState Ute_M r p (rho r p) μp (rho (Suc r) p)"
      and "∀qq. qq ∈ HOs r p ⟷ μp qq ≠ None"
      and "∀qq. qq ∈ SHOs r p ∩ HOs r p
                ⟶ μp qq = Some (sendMsg Ute_M r qq p (rho r qq))"
    unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq SHOmsgVectors_def
    by blast
  hence "{qq. μp qq = Some (Vote (Some v))} - (HOs r p - SHOs r p)
          ⊆ {qq. sendMsg Ute_M r qq p (rho r qq) = Vote (Some v)}"
         (is "?vrcvdp - ?ahop ⊆ ?vsentp") by auto
  hence "card (?vrcvdp - ?ahop) ≤ card ?vsentp"
    and "card (?vrcvdp - ?ahop) ≥ card ?vrcvdp - card ?ahop"
    by (auto simp: card_mono diff_card_le_card_Diff)
  hence "card ?vsentp ≥ card ?vrcvdp - card ?ahop" by auto
  moreover
  from usafe have "card (HOs r p - SHOs r p) ≤ α"
    by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
  moreover
  from run d1 d2 have "step r ≠ 0" by (rule decide_step)
  with nxt have "next1 r p (rho r p) μp (rho (Suc r) p)"
    by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
  with run d1 d2 have "card {qq. μp qq = Some (Vote (Some v))} > E"
    unfolding next1_def by auto
  ultimately
  show ?thesis using alpha_lt_E by auto
qed

subsection ‹Proof of Agreement and Validity›

text ‹
 If more than ‹E - α› messages holding ‹v› are sent to
 some process ‹p› at round ‹r›, then every process ‹pp›
 correctly receives more than ‹α› such messages.
 ›
(*
  The proof mainly relies on the @{text Ute_commPerRound} predicate. 
*)

lemma common_x_argument_1:
  assumes usafe:"SHOcommPerRd Ute_M (HOs (Suc r)) (SHOs (Suc r))"
  and threshold: "card {q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
                            = Vote (Some v)} > E - α"
                 (is "card (?msgs p v) > _")
  shows "card (?msgs pp v ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) > α"
proof -
  have "card (?msgs pp v) + card (SHOs (Suc r) pp ∩ HOs (Suc r) pp) > N + α"
  proof -
    have "∀q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
                = sendMsg Ute_M (Suc r) q pp (rho (Suc r) q)"
      by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def 
                     step_def send0_def send1_def)
    moreover
    from usafe
    have "card (SHOs (Suc r) pp ∩ HOs (Suc r) pp) > N + 2*α - E - 1"
      by (auto simp: Ute_SHOMachine_def step_def Ute_commPerRd_def)
    ultimately
    show ?thesis using threshold by auto
  qed
  moreover
  have "card (?msgs pp v) + card (SHOs (Suc r) pp ∩ HOs (Suc r) pp)
        = card (?msgs pp v ∪ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))
          + card (?msgs pp v ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))"
    by (auto intro: card_Un_Int)
  moreover
  have "card (?msgs pp v ∪ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) ≤ N"
    by (auto simp: card_mono)
  ultimately
  show ?thesis by auto
qed

text ‹
 If more than ‹E - α› messages holding ‹v› are sent to ‹p›
 at some round ‹r›, then any process ‹pp› will set its ‹x› to
 value ‹v› in ‹r›.
 ›
(*
  The proof relies on previous lemmas @{text common_x_argument_1}
  and @{text common_vote} and the @{text Ute_commPerRound} predicate. 
*)

lemma common_x_argument_2:
  assumes run: "SHORun Ute_M rho HOs SHOs" 
  and usafe: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and nxtpp: "nextState Ute_M (Suc r) pp (rho (Suc r) pp)
                        μpp (rho (Suc (Suc r)) pp)"
  and mupp: "μpp ∈ SHOmsgVectors Ute_M (Suc r) pp (rho (Suc r))
                                 (HOs (Suc r) pp) (SHOs (Suc r) pp)"
  and threshold: "card {q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
                             = Vote (Some v)} > E - α"
                 (is "card (?sent p v) > _")
  shows "x (rho (Suc (Suc r)) pp) = v"
proof -
  have stp:"step (Suc r) ≠ 0"
  proof
    assume sr: "step (Suc r) = 0"
    hence "∀q. sendMsg Ute_M (Suc r) q p (rho (Suc r) q)
                 = Val (x (rho (Suc r) q))"
      by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send0_def)
    moreover
    from threshold obtain qq where
      "sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq) = Vote (Some v)"
      by force
    ultimately
    show False by simp
  qed

  have va: "card {qq. μpp qq = Some (Vote (Some v))} > α"
       (is "card (?msgs v) > α")
  proof -
    from mupp
    have "SHOs (Suc r) pp ∩ HOs (Suc r) pp
          ⊆ {qq. μpp qq = Some (sendMsg Ute_M (Suc r) qq pp (rho (Suc r) qq))}"
      unfolding SHOmsgVectors_def by auto
    moreover
    hence "(?msgs v) 🪙 (?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)" 
      by auto
    hence "card (?msgs v)
             ≥ card ((?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp))"
      by (auto intro: card_mono)
    moreover
    from usafe threshold 
    have alph:"card ((?sent pp v) ∩ (SHOs (Suc r) pp ∩ HOs (Suc r) pp)) > α"
      by (blast dest: common_x_argument_1)
    ultimately
    show ?thesis by auto
  qed
  moreover
  from nxtpp stp
  have "next1 (Suc r) pp (rho (Suc r) pp) μpp (rho (Suc (Suc r)) pp)"
    by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
  ultimately
  obtain w where wa:"card (?msgs w) > α" and xw:"x (rho (Suc (Suc r)) pp) = w"
    unfolding next1_def by auto

  have "v = w"
  proof -
    note usafe
    moreover
    obtain qv where "qv ∈ SHOs (Suc r) pp" and "μpp qv = Some (Vote (Some v))"
    proof -
      have "¬ (?msgs v ⊆ HOs (Suc r) pp - SHOs (Suc r) pp)"
      proof
        assume "?msgs v ⊆ HOs (Suc r) pp - SHOs (Suc r) pp"
        hence "card (?msgs v) ≤ card ((HOs (Suc r) pp) - (SHOs (Suc r) pp))"
          by (auto simp: card_mono)
        moreover
        from usafe
        have "card (HOs (Suc r) pp - SHOs (Suc r) pp) ≤ α"
          by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
        moreover
        note va
        ultimately
        show False by auto
      qed
      then obtain qv
        where "qv ∉ HOs (Suc r) pp - SHOs (Suc r) pp"
          and qsv:"μpp qv = Some (Vote (Some v))" 
        by auto
      with mupp have "qv ∈ SHOs (Suc r) pp"
        unfolding SHOmsgVectors_def by auto
      with qsv that show ?thesis by auto
    qed
    with stp mupp have "vote (rho (Suc r) qv) = Some v"
      by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def 
                     Ute_sendMsg_def send1_def)
    moreover
    obtain qw where
      "qw ∈ SHOs (Suc r) pp" and "μpp qw = Some (Vote (Some w))"
    proof -
      have "¬ (?msgs w ⊆ HOs (Suc r) pp - SHOs (Suc r) pp)"
      proof
        assume "?msgs w ⊆ HOs (Suc r) pp - SHOs (Suc r) pp"
        hence "card (?msgs w) ≤ card ((HOs (Suc r) pp) - (SHOs (Suc r) pp))"
          by (auto simp: card_mono)
        moreover
        from usafe
        have "card (HOs (Suc r) pp - SHOs (Suc r) pp) ≤ α"
          by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
        moreover
        note wa
        ultimately
        show False by auto
      qed
      then obtain qw
        where "qw ∉ HOs (Suc r) pp - SHOs (Suc r) pp"
          and qsw: "μpp qw = Some (Vote (Some w))" 
        by auto
      with mupp have "qw ∈ SHOs (Suc r) pp" 
        unfolding SHOmsgVectors_def by auto
      with qsw that show ?thesis by auto
    qed
    with stp mupp have "vote (rho (Suc r) qw) = Some w"
      by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def
                     Ute_sendMsg_def send1_def)
    moreover
    from run obtain μqv μqw
      where "nextState Ute_M r qv ((rho r) qv) μqv (rho (Suc r) qv)"
        and "μqv ∈ SHOmsgVectors Ute_M r qv (rho r) (HOs r qv) (SHOs r qv)"
        and "nextState Ute_M r qw ((rho r) qw) μqw (rho (Suc r) qw)"
        and "μqw ∈ SHOmsgVectors Ute_M r qw (rho r) (HOs r qw) (SHOs r qw)"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq) blast
    ultimately
    show ?thesis using usafe by (auto dest: common_vote)
  qed
  with xw show "x (rho (Suc (Suc r)) pp) = v" by auto
qed

text ‹
 Inductive argument for the agreement and validity theorems.
 ›
(*
  The proof relies on previous lemmas @{text common_x_argument_2}
  and @{text unique_majority_T} and the @{text Ute_commPerRound} predicate.
*)

lemma safety_inductive_argument:
  assumes run: "SHORun Ute_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and ih: "E - α < card {q. sendMsg Ute_M r' q p (rho r' q) = Vote (Some v)}"
  and stp1: "step r' = Suc 0"
  shows "E - α <
         card {q. sendMsg Ute_M (Suc (Suc r')) q p (rho (Suc (Suc r')) q)
                     = Vote (Some v)}"
proof -
  from stp1 have "r' > 0" by (auto simp: step_def)
  with stp1 obtain r where rr':"r' = Suc r" and stpr:"step (Suc r) = Suc 0"
    by (auto dest: gr0_implies_Suc)

  have "∀pp. x (rho (Suc (Suc r)) pp) = v"
  proof 
    fix pp
    from run obtain μpp
      where "μpp ∈ SHOmsgVectors Ute_M r' pp (rho r') (HOs r' pp) (SHOs r' pp)"
        and "nextState Ute_M r' pp (rho r' pp) μpp (rho (Suc r') pp)"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
    with run comm ih rr' show "x (rho (Suc (Suc r)) pp) = v" 
      by (auto dest: common_x_argument_2)
  qed
  with run stpr
  have "∀pp p. sendMsg Ute_M (Suc (Suc r)) pp p (rho (Suc (Suc r)) pp) = Val v"
    by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
                   Ute_sendMsg_def send0_def mod_Suc step_def)
  with rr'
  have "∧p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
                                     (HOs (Suc r') p) (SHOs (Suc r') p)
             ==> SHOs (Suc r') p ∩ HOs (Suc r') p
                   ⊆ {q. μp' q = Some (Val v)}"
    by (auto simp: SHOmsgVectors_def)
  hence "∧p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
                                       (HOs (Suc r') p) (SHOs (Suc r') p)
             ==> card (SHOs (Suc r') p ∩ HOs (Suc r') p)
                   ≤ card {q. μp' q = Some (Val v)}" 
    by (auto simp: card_mono)
  moreover
  from comm have "∧p. T < card (SHOs (Suc r') p ∩ HOs (Suc r') p)"
    by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
  ultimately 
  have vT:"∧p μp'. μp' ∈ SHOmsgVectors Ute_M (Suc r') p (rho (Suc r'))
                                         (HOs (Suc r') p) (SHOs (Suc r') p)
                ==> T < card {q. μp' q = Some (Val v)}"
    by (auto dest: less_le_trans)

  show ?thesis
  proof -
    have "∀pp. vote ((rho (Suc (Suc r'))) pp) = Some v"
    proof
      fix pp
      from run obtain μpp
        where nxtpp: "nextState Ute_M (Suc r') pp (rho (Suc r') pp) μpp
                                      (rho (Suc (Suc r')) pp)"
          and mupp: "μpp ∈ SHOmsgVectors Ute_M (Suc r') pp (rho (Suc r'))
                                     (HOs (Suc r') pp) (SHOs (Suc r') pp)"
        by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
      with vT have vT':"card {q. μpp q = Some (Val v)} > T" 
        by auto
      moreover
      from stpr rr' have "step (Suc r') = 0"
        by (auto simp: mod_Suc step_def)
      with nxtpp
      have "next0 (Suc r') pp (rho (Suc r') pp) μpp (rho (Suc (Suc r')) pp)"
        by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
      ultimately
      obtain w
        where wT:"card {q. μpp q = Some (Val w)} > T"
          and votew:"vote (rho (Suc (Suc r')) pp) = Some w" 
        by (auto simp: next0_def)
      from vT' wT have "v = w"
        by (auto dest: unique_majority_T)
      with votew show "vote (rho (Suc (Suc r')) pp) = Some v" by simp
    qed
    with run stpr rr'
    have "∀p. N = card {q. sendMsg Ute_M (Suc (Suc (Suc r))) q p
                                  ((rho (Suc (Suc (Suc r)))) q) = Vote (Some v)}"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq 
                     Ute_sendMsg_def send1_def step_def mod_Suc)
    with rr' majE EltN show ?thesis by auto
  qed
qed

text ‹
 A process that holds some decision ‹v› has decided ‹v›
 sometime in the past.
 ›

lemma decisionNonNullThenDecided:
  assumes run:"SHORun Ute_M rho HOs SHOs" and dec: "decide (rho n p) = Some v"
  shows "∃m<n. decide (rho (Suc m) p) ≠ decide (rho m p)
             ∧ decide (rho (Suc m) p) = Some v"
proof -
  let "?dec k" = "decide ((rho k) p)"
  have "(∀m<n. ?dec (Suc m) ≠ ?dec m ⟶ ?dec (Suc m) ≠ Some v)
        ⟶ ?dec n ≠ Some v"
    (is "?P n" is "?A n ⟶ _")
  proof (induct n)
    from run show "?P 0"
      by (auto simp: Ute_SHOMachine_def SHORun_eq HOinitConfig_eq
                     initState_def Ute_initState_def)
  next
    fix n
    assume ih: "?P n" thus "?P (Suc n)" by force
  qed
  with dec show ?thesis by auto
qed


text ‹
 If process ‹p1› has decided value ‹v1› and process
 ‹p2› later decides, then ‹p2› must decide ‹v1›.
 ›
(*
  The proof relies on previous lemmas @{text decide_step},
  @{text decide_with_threshold_E}, @{text unique_majority_E_\<alpha>},
  @{text decisionNonNullThenDecided} and @{text safety_inductive_argument}.
*)

lemma laterProcessDecidesSameValue:
  assumes run:"SHORun Ute_M rho HOs SHOs"
  and comm:"∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and dv1:"decide (rho (Suc r) p1) = Some v1"
  and dn2:"decide (rho (r + k) p2) ≠ Some v2"
  and dv2:"decide (rho (Suc (r + k)) p2) = Some v2"
  shows "v2 = v1"
proof -
  from run dv1 obtain r1
    where r1r:"r1 < Suc r"
      and dn1:"decide (rho r1 p1) ≠ Some v1"
      and dv1':"decide (rho (Suc r1) p1) = Some v1"
    by (auto dest: decisionNonNullThenDecided)

  from r1r obtain s where rr1:"Suc r = Suc (r1 + s)"
    by (auto dest: less_imp_Suc_add)
  then obtain k' where kk':"r + k = r1 + k'" 
    by auto
  with dn2 dv2 
  have dn2': "decide (rho (r1 + k') p2) ≠ Some v2"
    and dv2': "decide (rho (Suc (r1 + k')) p2) = Some v2"
    by auto

  from run dn1 dv1' dn2' dv2' 
  have rs0:"step r1 = Suc 0" and  rks0:"step (r1 + k') = Suc 0"
    by (auto simp: mod_Suc step_def dest: decide_step)

  have "step (r1 + k') = step (step r1 + k')"
    unfolding step_def by (simp add: mod_add_left_eq)
  with rs0 rks0 have "step k' = 0" by (auto simp: step_def mod_Suc)
  then obtain k'' where "k' = k''*nSteps" by (auto simp: step_def)
  with dn2' dv2' 
  have dn2'':"decide (rho (r1 + k''*nSteps) p2) ≠ Some v2"
    and dv2'':"decide (rho (Suc (r1 + k''*nSteps)) p2) = Some v2" 
    by auto

  from rs0 have stp:"step (r1 + k''*nSteps) = Suc 0" 
    unfolding step_def by auto

  have inv:"card {q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
                         = Vote (Some v1)} > E - α"
  proof (induct k'')
    from stp have "step (r1 + 0*nSteps) = Suc 0" 
      by (auto simp: step_def)
    from run comm dn1 dv1'
    show "card {q. sendMsg Ute_M (r1 + 0*nSteps) q p1 (rho (r1 + 0*nSteps) q)
                      = Vote (Some v1)} > E - α"
      by (intro decide_with_threshold_E) auto
  next
    fix k''
    assume ih: "E - α <
          card {q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
                       = Vote (Some v1)}"
    from rs0 have stps: "step (r1 + k''*nSteps) = Suc 0" 
      by (auto simp: step_def)
    with run comm ih
    have "E - α <
       card {q. sendMsg Ute_M (Suc (Suc (r1 + k''*nSteps))) q p1
                              (rho (Suc (Suc (r1 + k''*nSteps))) q)
                   = Vote (Some v1)}"
      by (rule safety_inductive_argument)
    thus "E - α <
       card {q. sendMsg Ute_M (r1 + Suc k'' * nSteps) q p1
                              (rho (r1 + Suc k'' * nSteps) q)
                     = Vote (Some v1)}"
      by auto
  qed
  moreover
  from run
  have "∀q. sendMsg Ute_M (r1 + k''*nSteps) q p1 (rho (r1 + k''*nSteps) q)
          = sendMsg Ute_M (r1 + k''*nSteps) q p2 (rho (r1 + k''*nSteps) q)"
    by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def 
                   step_def send0_def send1_def)
  moreover
  from run comm dn2'' dv2''
  have "E - α <
      card {q. sendMsg Ute_M (r1 + k''*nSteps) q p2 (rho (r1 + k''*nSteps) q)
                  = Vote (Some v2)}"
    by (auto dest: decide_with_threshold_E)
  ultimately
  show "v2 = v1" by (auto dest: unique_majority_E_α)
qed

text ‹
 The Agreement property is an immediate consequence of the two
 preceding lemmas.
 ›

theorem ute_agreement:
  assumes run: "SHORun Ute_M rho HOs SHOs" 
  and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and p: "decide (rho m p) = Some v"
  and q: "decide (rho n q) = Some w"
  shows "v = w"
proof -
  from run p obtain k 
    where k1: "decide (rho (Suc k) p) ≠ decide (rho k p)"
      and k2: "decide (rho (Suc k) p) = Some v"
    by (auto dest: decisionNonNullThenDecided)
  from run q obtain l 
    where l1: "decide (rho (Suc l) q) ≠ decide (rho l q)"
      and l2: "decide (rho (Suc l) q) = Some w"
    by (auto dest: decisionNonNullThenDecided)
  show ?thesis
  proof (cases "k ≤ l")
    case True
    then obtain m where m: "l = k+m" by (auto simp add: le_iff_add)
    from run comm k2 l1 l2 m have "w = v"
      by (auto elim!: laterProcessDecidesSameValue)
    thus ?thesis by simp
  next
    case False
    hence "l ≤ k" by simp
    then obtain m where m: "k = l+m" by (auto simp add: le_iff_add)
    from run comm l2 k1 k2 m show ?thesis
      by (auto elim!: laterProcessDecidesSameValue)
  qed
qed

text ‹
 Main lemma for the proof of the Validity property.
 ›
(*
  The proof relies on previous lemmas @{text safety_inductive_argument},
  @{text unique_majority_T} and the @{text Ute_commPerRound} predicate.
*)

lemma validity_argument:
  assumes run: "SHORun Ute_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and init: "∀p. x ((rho 0) p) = v"
  and dw: "decide (rho r p) = Some w"
  and stp: "step r' = Suc 0"
  shows "card {q. sendMsg Ute_M r' q p (rho r' q) = Vote (Some v)} > E - α"
proof -
  define k where "k = r' div nSteps"
  with stp have stp: "r' = Suc 0 + k * nSteps"
    using div_mult_mod_eq [of r' nSteps]
    by (simp add: step_def)
  moreover
  have "E - α <
        card {q. sendMsg Ute_M (Suc 0 + k*nSteps) q p ((rho (Suc 0 + k*nSteps)) q)
                   = Vote (Some v)}"
  proof (induct k)
    have "∀pp. vote ((rho (Suc 0)) pp) = Some v"
    proof
      fix pp
      from run obtain μpp
        where nxtpp:"nextState Ute_M 0 pp (rho 0 pp) μpp (rho (Suc 0) pp)"
          and mupp:"μpp ∈ SHOmsgVectors Ute_M 0 pp (rho 0) (HOs 0 pp) (SHOs 0 pp)"
        by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
      have majv:"card {q. μpp q = Some (Val v)} > T"
      proof -
        from run init have "∀q. sendMsg Ute_M 0 q pp (rho 0 q) = Val v"
          by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq 
                         Ute_sendMsg_def send0_def step_def)
        moreover
        from comm have shoT:"card (SHOs 0 pp ∩ HOs 0 pp) > T"
          by (auto simp: Ute_SHOMachine_def Ute_commPerRd_def)
        moreover
        from mupp
        have "SHOs 0 pp ∩ HOs 0 pp
               ⊆ {q. μpp q = Some (sendMsg Ute_M 0 q pp (rho 0 q))}"
          by (auto simp: SHOmsgVectors_def)
        hence "card (SHOs 0 pp ∩ HOs 0 pp)
                 ≤ card {q. μpp q = Some (sendMsg Ute_M 0 q pp (rho 0 q))}"
          by (auto simp: card_mono)
        ultimately
        show ?thesis by (auto simp: less_le_trans)
      qed
      moreover
      from nxtpp have "next0 0 pp ((rho 0) pp) μpp (rho (Suc 0) pp)"
        by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def step_def)
      ultimately
      obtain w where majw:"card {q. μpp q = Some (Val w)} > T"
                 and votew:"vote (rho (Suc 0) pp) = Some w"
        by (auto simp: next0_def)

      from majv majw have "v = w" by (auto dest: unique_majority_T)
      with votew show "vote ((rho (Suc 0)) pp) = Some v" by simp
    qed
    with run
    have "card {q. sendMsg Ute_M (Suc 0) q p (rho (Suc 0) q) = Vote (Some v)} = N"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq
                     Ute_nextState_def step_def Ute_sendMsg_def send1_def)
    thus "E - α <
      card {q. sendMsg Ute_M (Suc 0 + 0 * nSteps) q p (rho (Suc 0 + 0 * nSteps) q)
                   = Vote (Some v)}"
      using majE EltN by auto
  next
    fix k
    assume ih:"E - α <
        card {q. sendMsg Ute_M (Suc 0 + k * nSteps) q p (rho (Suc 0 + k * nSteps) q)
                     = Vote (Some v)}"
    have "step (Suc 0 + k * nSteps) = Suc 0"
      by (auto simp: mod_Suc step_def)
    from run comm ih this
    have "E - α <
      card {q. sendMsg Ute_M (Suc (Suc (Suc 0 + k * nSteps))) q p
                             (rho (Suc (Suc (Suc 0 + k * nSteps))) q)
                  = Vote (Some v)}"
      by (rule safety_inductive_argument)
    thus "E - α <
       card {q. sendMsg Ute_M (Suc 0 + Suc k * nSteps) q p
                              (rho (Suc 0 + Suc k * nSteps) q)
                 = Vote (Some v)}" by simp
  qed
  ultimately
  show ?thesis by simp
qed

text ‹
 The following theorem shows the Validity property of algorithm \ute{}.
 ›
(*
 The proof relies on previous lemmas @{text decisionNonNullThenDecided},
 @{text decide_step}, @{text decide_with_threshold_E},  @{text unique_majority_E_\<alpha>},
 and the @{text Validity_argument}. 
*)

theorem ute_validity:
  assumes run: "SHORun Ute_M rho HOs SHOs"
  and comm: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and init: "∀p. x (rho 0 p) = v"
  and dw: "decide (rho r p) = Some w"
  shows "v = w"
proof -
  from run dw obtain r1
    where dnr1:"decide ((rho r1) p) ≠ Some w"
      and dwr1:"decide ((rho (Suc r1)) p) = Some w"
    by (force dest: decisionNonNullThenDecided)
  with run have "step r1 ≠ 0" by (rule decide_step)
  hence "step r1 = Suc 0" by (simp add: step_def mod_Suc)
  with assms
  have "E - α <
        card {q. sendMsg Ute_M r1 q p (rho r1 q) = Vote (Some v)}"
    by (rule validity_argument)
  moreover
  from run comm dnr1 dwr1
  have "card {q. sendMsg Ute_M r1 q p (rho r1 q) = Vote (Some w)} > E - α"
    by (auto dest: decide_with_threshold_E)
  ultimately
  show "v = w" by (auto dest: unique_majority_E_α)
qed


subsection ‹Proof of Termination›

text ‹
 At the second round of a phase that satisfies the conditions expressed in
 the global communication predicate, processes update their ‹x› variable
 with the value ‹v› they receive in more than ‹α› messages.
 ›
(* The proof relies on @{text common_vote}. *)

lemma set_x_from_vote:
  assumes run: "SHORun Ute_M rho HOs SHOs" 
  and comm: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and stp: "step (Suc r) = Suc 0"
  and π: "∀p. HOs (Suc r) p = SHOs (Suc r) p"
  and nxt: "nextState Ute_M (Suc r) p (rho (Suc r) p) μ (rho (Suc (Suc r)) p)"
  and mu: "μ ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
                                   (HOs (Suc r) p) (SHOs (Suc r) p)"
  and vp: "α < card {qq. μ qq = Some (Vote (Some v))}"
  shows "x ((rho (Suc (Suc r))) p) = v"
proof -
  from nxt stp vp obtain wp
    where xwp:"α < card {qq. μ qq = Some (Vote (Some wp))}"
      and xp:"x (rho (Suc (Suc r)) p) = wp"
    by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def next1_def)

  have "wp = v"
  proof -
    from xwp obtain pp where smw:"μ pp = Some (Vote (Some wp))"
      by force
    have "vote (rho (Suc r) pp) = Some wp"
    proof -
      from smw mu π 
      have "μ pp = Some (sendMsg Ute_M (Suc r) pp p (rho (Suc r) pp))"
        unfolding SHOmsgVectors_def by force
      with stp have "μ pp = Some (Vote (vote (rho (Suc r) pp)))"
        by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send1_def)
      with smw show ?thesis by auto
    qed
    moreover
    from vp obtain qq where smv:"μ qq = Some (Vote (Some v))" 
      by force
    have "vote (rho (Suc r) qq) = Some v"
    proof -
      from smv mu π
      have "μ qq = Some (sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq))"
        unfolding SHOmsgVectors_def by force
      with stp have "μ qq = Some (Vote (vote (rho (Suc r) qq)))"
        by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def send1_def)
      with smv show ?thesis by auto
    qed
    moreover
    from run obtain μpp μqq
      where "nextState Ute_M r pp (rho r pp) μpp (rho (Suc r) pp)"
        and "μpp ∈ SHOmsgVectors Ute_M r pp (rho r) (HOs r pp) (SHOs r pp)"
        and "nextState Ute_M r qq ((rho r) qq) μqq (rho (Suc r) qq)"
        and "μqq ∈ SHOmsgVectors Ute_M r qq (rho r) (HOs r qq) (SHOs r qq)"
      unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq by blast
    ultimately
    show ?thesis using comm by (auto dest: common_vote)
  qed
  with xp show ?thesis by simp
qed

text ‹
 Assume that HO and SHO sets are uniform at the second step of some
 phase. Then at the subsequent round there exists some value ‹v›
 such that any received message which is not corrupted holds ‹v›.
 ›
(* The proof relies on lemma @{text set_x_from_vote}. *)

lemma termination_argument_1:
  assumes run: "SHORun Ute_M rho HOs SHOs" 
  and comm: "SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and stp: "step (Suc r) = Suc 0"
  and π: "∀p. π0 = HOs (Suc r) p ∧ π0 = SHOs (Suc r) p"
  obtains v where 
    "∧p μp' q.
       [ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
         μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
                             (HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
       ] ==> μp' q = (Some (Val v))"
proof -
  from π have hosho:"∀p. SHOs (Suc r) p = SHOs (Suc r) p ∩ HOs (Suc r) p"
    by simp

  have "∧p q. x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)"
  proof -
    fix p q
    from run obtain μp
      where nxt: "nextState Ute_M (Suc r) p (rho (Suc r) p)
                                  μp (rho (Suc (Suc r)) p)"
        and mu: "μp ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
                                          (HOs (Suc r) p) (SHOs (Suc r) p)"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)

    from run obtain μq
      where nxtq: "nextState Ute_M (Suc r) q (rho (Suc r) q)
                                   μq (rho (Suc (Suc r)) q)"
       and muq: "μq ∈ SHOmsgVectors Ute_M (Suc r) q (rho (Suc r))
                                          (HOs (Suc r) q) (SHOs (Suc r) q)"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
       
    have "∀qq. μp qq = μq qq"
    proof
      fix qq
      show "μp qq = μq qq"
      proof (cases "μp qq = None")
        case False
        with mu π have 1:"qq ∈ SHOs (Suc r) p" and 2:"qq ∈ SHOs (Suc r) q"
          unfolding SHOmsgVectors_def by auto
        from mu π 1
        have "μp qq = Some (sendMsg Ute_M (Suc r) qq p (rho (Suc r) qq))"
          unfolding SHOmsgVectors_def by auto
        moreover
        from muq π 2 
        have "μq qq = Some (sendMsg Ute_M (Suc r) qq q (rho (Suc r) qq))"
          unfolding SHOmsgVectors_def by auto
        ultimately
        show ?thesis
          by (auto simp: Ute_SHOMachine_def Ute_sendMsg_def step_def 
                         send0_def send1_def)
      next
        case True
        with mu have "qq ∉ HOs (Suc r) p" unfolding SHOmsgVectors_def by auto
        with π muq have "μq qq = None" unfolding SHOmsgVectors_def by auto
        with True show ?thesis by simp
      qed
    qed
    hence vsets:"∧v. {qq. μp qq = Some (Vote (Some v))}
                    = {qq. μq qq = Some (Vote (Some v))}"
      by auto
    (* NB: due to the Global predicate (HO = SHO), we do not need \<alpha> + 1 msgs
       holding a true vote, only 1. We might also prefer to invoke only the
       @{text Ute_commPerRound} predicate to obtain qq :
       since "card (HOs (Suc r) p - SHOs (Suc r) p) < \<alpha>", there should be one
       "correct" message holding a vote and this vote should be common according
       to previous (Suc r)esults. *)

    show "x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)"
    proof (cases "∃v. α < card {qq. μp qq = Some (Vote (Some v))}", clarify)
      fix v
      assume vp: "α < card {qq. μp qq = Some (Vote (Some v))}"
      with run comm stp π nxt mu have "x (rho (Suc (Suc r)) p) = v" 
        by (auto dest: set_x_from_vote)
      moreover
      from vsets vp
      have "α < card {qq. μq qq = Some (Vote (Some v))}" by auto
      with run comm stp π nxtq muq have "x (rho (Suc (Suc r)) q) = v" 
        by (auto dest: set_x_from_vote)
      ultimately
      show "x (rho (Suc (Suc r)) p) = x (rho (Suc (Suc r)) q)" 
        by auto
    next
      assume nov: "¬ (∃v. α < card {qq. μp qq = Some (Vote (Some v))})"
      with nxt stp have "x (rho (Suc (Suc r)) p) = undefined"
        by (auto simp: Ute_SHOMachine_def nextState_def 
                       Ute_nextState_def next1_def)
      moreover
      from vsets nov
      have "¬ (∃v. α < card {qq. μq qq = Some (Vote (Some v))})" by auto
      with nxtq stp have "x (rho (Suc (Suc r)) q) = undefined" 
        by (auto simp: Ute_SHOMachine_def nextState_def 
                       Ute_nextState_def next1_def)
      ultimately
      show ?thesis by simp
    qed
  qed
  then obtain v where "∧q. x (rho (Suc (Suc r)) q) = v" by blast
  moreover
  from stp have "step (Suc (Suc r)) = 0" 
    by (auto simp: step_def mod_Suc)
  hence "∧p μp' q.
    [ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
      μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
                          (HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
    ] ==> μp' q = Some (Val (x (rho (Suc (Suc r)) q)))"
    by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def Ute_sendMsg_def send0_def)
  ultimately
  have "∧p μp' q.
    [ q ∈ SHOs (Suc (Suc r)) p ∩ HOs (Suc (Suc r)) p;
      μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r)) p (rho (Suc (Suc r)))
                                (HOs (Suc (Suc r)) p) (SHOs (Suc (Suc r)) p)
    ] ==> μp' q = (Some (Val v))" 
    by auto
  with that show thesis by blast
qed

text ‹
 If a process ‹p› votes ‹v› at some round ‹r›,
 then all messages received by ‹p› in ‹r› that are not
 corrupted hold ‹v›.
 ›
(* immediate from lemma @{text vote_step} and the algorithm definition. *)

lemma termination_argument_2:
  assumes mup: "μp ∈ SHOmsgVectors Ute_M (Suc r) p (rho (Suc r))
                                     (HOs (Suc r) p) (SHOs (Suc r) p)"
  and nxtq: "nextState Ute_M r q (rho r q) μq (rho (Suc r) q)"
  and vq: "vote (rho (Suc r) q) = Some v"
  and qsho: "q ∈ SHOs (Suc r) p ∩ HOs (Suc r) p"
  shows "μp q = Some (Vote (Some v))"
proof -
  from nxtq vq have "step r = 0" by (auto simp: vote_step)
  with mup qsho have "μp q = Some (Vote (vote (rho (Suc r) q)))"
    by (auto simp: Ute_SHOMachine_def SHOmsgVectors_def Ute_sendMsg_def
                   step_def send1_def mod_Suc)
  with vq show "μp q = Some (Vote (Some v))" by auto
qed

text‹
 We now prove the Termination property.
 ›
(*
  The proof relies on previous lemmas @{text termination_argument_1},
  @{text termination_argument_2}, @{text common_vote}, @{text unique_majority_E},
  and the @{text Ute_commGlobal} predicate.
*)

theorem ute_termination:
  assumes run: "SHORun Ute_M rho HOs SHOs"
  and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
  and commG: "SHOcommGlobal Ute_M HOs SHOs"
  shows "∃r v. decide (rho r p) = Some v"
proof -
  from commG
  obtain Φ π r0
    where rr: "r0 = Suc (nSteps * Φ)"
      and π: "∀p. π = HOs r0 p ∧ π = SHOs r0 p"
      and t: "∀p. card (SHOs (Suc r0) p ∩ HOs (Suc r0) p) > T"
      and e: "∀p. card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p) > E"
    by (auto simp: Ute_SHOMachine_def Ute_commGlobal_def Let_def)
  from rr have stp:"step r0 = Suc 0" by (auto simp: step_def)

  obtain w where votew:"∀p. (vote (rho (Suc (Suc r0)) p)) = Some w"
  proof -    
    have abc:"∀p. ∃w. vote (rho (Suc (Suc r0)) p) = Some w"
    proof
      fix p
      from run stp obtain μp
        where nxt:"nextState Ute_M (Suc r0) p (rho (Suc r0) p) μp
                                   (rho (Suc (Suc r0)) p)"
          and mup:"μp ∈ SHOmsgVectors Ute_M (Suc r0) p (rho (Suc r0))
                                      (HOs (Suc r0) p) (SHOs (Suc r0) p)"
        by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)

      have "∃v. T < card {qq. μp qq = Some (Val v)}"
      proof -
        from t have "card (SHOs (Suc r0) p ∩ HOs (Suc r0) p) > T" .. 
        moreover
        from run commR stp π rr
        obtain v where
          "∧p μp' q.
              [ q ∈ SHOs (Suc r0) p ∩ HOs (Suc r0) p;
                μp' ∈ SHOmsgVectors Ute_M (Suc r0) p (rho (Suc r0))
                                          (HOs (Suc r0) p) (SHOs (Suc r0) p)
              ] ==> μp' q = Some (Val v)" 
          using termination_argument_1 by blast

        with mup obtain v where
          "∧qq. qq ∈ SHOs (Suc r0) p ∩ HOs (Suc r0) p ==> μp qq = Some (Val v)" 
          by auto
        hence "SHOs (Suc r0) p ∩ HOs (Suc r0) p ⊆ {qq. μp qq = Some (Val v)}" 
          by auto
        hence "card (SHOs (Suc r0) p ∩ HOs (Suc r0) p)
                 ≤ card {qq. μp qq = Some (Val v)}"
          by (auto intro: card_mono)
        ultimately
        have "T < card {qq. μp qq = Some (Val v)}" by auto
        thus ?thesis by auto
      qed
      with stp nxt show "∃w. vote ((rho (Suc (Suc r0))) p) = Some w"
        by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def 
                       step_def mod_Suc next0_def)
    qed
    then obtain qq w where qqw:"vote (rho (Suc (Suc r0)) qq) = Some w" 
      by blast
    have "∀pp. vote (rho (Suc (Suc r0)) pp) = Some w"
    proof
      fix pp
      from abc obtain wp where pwp:"vote ((rho (Suc (Suc r0))) pp) = Some wp" 
        by blast
      from run obtain μpp μqq
        where nxtp: "nextState Ute_M (Suc r0) pp (rho (Suc r0) pp)
                                     μpp (rho (Suc (Suc r0)) pp)"
          and mup: "μpp ∈ SHOmsgVectors Ute_M (Suc r0) pp (rho (Suc r0))
                                          (HOs (Suc r0) pp) (SHOs (Suc r0) pp)"
          and nxtq: "nextState Ute_M (Suc r0) qq (rho (Suc r0) qq)
                                     μqq (rho (Suc (Suc r0)) qq)"
          and muq: "μqq ∈ SHOmsgVectors Ute_M (Suc r0) qq (rho (Suc r0))
                                          (HOs (Suc r0) qq) (SHOs (Suc r0) qq)"
        unfolding Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq by blast
      from commR this pwp qqw have "wp = w"
        by (auto dest: common_vote)
      with pwp show "vote ((rho (Suc (Suc r0))) pp) = Some w" 
        by auto
    qed
    with that show ?thesis by auto
  qed

  from run obtain μp'
    where nxtp: "nextState Ute_M (Suc (Suc r0)) p (rho (Suc (Suc r0)) p)
                                 μp' (rho (Suc (Suc (Suc r0))) p)"
      and mup': "μp' ∈ SHOmsgVectors Ute_M (Suc (Suc r0)) p (rho (Suc (Suc r0)))
                                     (HOs (Suc (Suc r0)) p) (SHOs (Suc (Suc r0)) p)"
    by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
  have "∧qq. qq ∈ SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p
              ==> μp' qq = Some (Vote (Some w))"
  proof -
    fix qq
    assume qqsho:"qq ∈ SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p"
    from run obtain μqq where
      nxtqq:"nextState Ute_M (Suc r0) qq (rho (Suc r0) qq)
                             μqq (rho (Suc (Suc r0)) qq)"
      by (auto simp: Ute_SHOMachine_def SHORun_eq SHOnextConfig_eq)
    from commR mup' nxtqq votew qqsho show "μp' qq = Some (Vote (Some w))"
      by (auto dest: termination_argument_2)
  qed
  hence "SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p
           ⊆ {qq. μp' qq = Some (Vote (Some w))}" 
    by auto
  hence wsho: "card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p)
                 ≤ card {qq. μp' qq = Some (Vote (Some w))}"
    by (auto simp: card_mono)
   
  from stp have "step (Suc (Suc r0)) = Suc 0" 
    unfolding step_def by auto
  with nxtp have "next1 (Suc (Suc r0)) p (rho (Suc (Suc r0)) p) μp'
                        (rho (Suc (Suc (Suc r0))) p)"
    by (auto simp: Ute_SHOMachine_def nextState_def Ute_nextState_def)
  moreover
  from e have "E < card (SHOs (Suc (Suc r0)) p ∩ HOs (Suc (Suc r0)) p)" 
    by auto
  with wsho have majv:"card {qq. μp' qq = Some (Vote (Some w))} > E" 
    by auto
  ultimately
  show ?thesis by (auto simp: next1_def)
qed


subsection ‹\ute{} Solves Weak Consensus›

text ‹
 Summing up, all (coarse-grained) runs of \ute{} for
 HO and SHO collections that satisfy the communication predicate
 satisfy the Weak Consensus property.
 ›

theorem ute_weak_consensus:
  assumes run: "SHORun Ute_M rho HOs SHOs"
      and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ute_M HOs SHOs"
  shows "weak_consensus (x ∘ (rho 0)) decide rho"
  unfolding weak_consensus_def
  using ute_validity[OF run commR]
        ute_agreement[OF run commR]
        ute_termination[OF run commR commG]
  by auto

text ‹
 By the reduction theorem, the correctness of the algorithm carries over
 to the fine-grained model of runs.
 ›

theorem ute_weak_consensus_fg:
  assumes run: "fg_run Ute_M rho HOs SHOs (λr q. undefined)"
      and commR: "∀r. SHOcommPerRd Ute_M (HOs r) (SHOs r)"
      and commG: "SHOcommGlobal Ute_M HOs SHOs"
  shows "weak_consensus (λp. x (state (rho 0) p)) decide (state ∘ rho)"
    (is "weak_consensus ?inits _ _")
proof (rule local_property_reduction[OF run weak_consensus_is_local])
  fix crun
  assume crun: "CSHORun Ute_M crun HOs SHOs (λr q. undefined)"
     and init: "crun 0 = state (rho 0)"
  from crun have "SHORun Ute_M crun HOs SHOs" by (unfold SHORun_def)
  from this commR commG 
  have "weak_consensus (x ∘ (crun 0)) decide crun" 
    by (rule ute_weak_consensus)
  with init show "weak_consensus ?inits decide crun"
    by (simp add: o_def)
qed

end    ― ‹context @{text "ute_parameters"}›

end    (* theory UteProof *)