From VLSM.Lib Require Import Itauto.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude finite fin_sets fin_maps nmap.
From Coq Require Import Streams FunctionalExtensionality Eqdep_dec.
From VLSM.Lib Require Import Preamble ListExtras FinSetExtras.
From VLSM.Core Require Import VLSM Plans VLSMProjections Composition Equivocation.
From VLSM.Core.Equivocation Require Import NoEquivocation.
From VLSM.Examples Require Import Voting.

Create HintDb list_simpl discriminated.
#[export] Hint Rewrite or_False @elem_of_cons @elem_of_nil @elem_of_app : list_simpl.

Ltac simpl_elem_of_list := rewrite_strat any (topdown (hints list_simpl)).
Ltac simpl_elem_of_list_in H := rewrite_strat any (topdown (hints list_simpl)) in H.

Variant AllOrFin VSet : Type :=
| any_value
| some_values (vs : VSet).

Arguments any_value   {VSet}.
Arguments some_values [VSet] vs.

#[export] Instance elem_of_all_or_fin `{ElemOf V VSet} : ElemOf V (AllOrFin VSet) :=
  fun v fv =>
  match fv with
  | any_value => True
  | some_values vs => v ∈ vs
  end.

#[export] Instance AllOrFin_eq_dec `{EqDecision VSet} : EqDecision (AllOrFin VSet).
VSet: Type
EqDecision0: EqDecision VSet
EqDecision (AllOrFin VSet)
Proof.
VSet: Type
EqDecision0: EqDecision VSet
EqDecision (AllOrFin VSet)
  intros [| xs] [| ys]; [by unfold Decision; auto.. |].
VSet: Type
EqDecision0: EqDecision VSet
xs, ys: VSet
Decision (some_values xs = some_values ys)
  by destruct (decide_rel eq xs ys); [left | right]; congruence.
Defined.

Section sec_paxos_spec.

Context
  `{FinSet Value VSet}
  `{EqDecision VSet}
  {VSDec : RelDecision (∈@{VSet})}
  `{FinMap Acceptor AMap}
  `{!finite.Finite Acceptor}
  .

Notation ASet := (mapset.mapset AMap).

#[export] Instance ASet_Dom {A:Type} : Dom (AMap A) ASet := mapset.mapset_dom.
#[export] Instance AMap_FinMapDom : fin_map_dom.FinMapDom Acceptor AMap ASet :=
  mapset.mapset_dom_spec.

Context
  (Quorum : ASet -> Prop)
  (QDec : forall Q, Decision (Quorum Q))
  (QClosed : Proper (subseteq ==> impl) Quorum)
  (QA : forall (Q1 Q2 : sig Quorum), exists a, a ∈ `Q1 ∩ `Q2)
  .

Inductive paxos_message_body : Type :=
| m_1a
| m_1b (a : Acceptor) (last_vote : option (Ballot * Value))
| m_1c (safe_v : AllOrFin VSet)
| m_2a (v : Value)
| m_2b (a : Acceptor) (v : Value).

Definition paxos_message : Type := Ballot * paxos_message_body.

#[export] Instance paxos_message_eq_dec : EqDecision paxos_message.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
EqDecision paxos_message
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
EqDecision paxos_message
  assert (EqDecision (option (Ballot * Value))) by typeclasses eauto.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
X: EqDecision (option (Ballot * Value))
EqDecision paxos_message
  assert (EqDecision (AllOrFin VSet)) by typeclasses eauto.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
X: EqDecision (option (Ballot * Value))
X0: EqDecision (AllOrFin VSet)
EqDecision paxos_message
  intros m1 m2.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
X: EqDecision (option (Ballot * Value))
X0: EqDecision (AllOrFin VSet)
m1, m2: paxos_message
Decision (m1 = m2)
  refine (prod_eq_dec _ _).
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
X: EqDecision (option (Ballot * Value))
X0: EqDecision (AllOrFin VSet)
m1, m2: paxos_message
EqDecision paxos_message_body
  unfold EqDecision, Decision in *.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: ∀ x y : Value, {x = y} + {x ≠ y}
H6: FinSet Value VSet
EqDecision1: ∀ x y : VSet, {x = y} + {x ≠ y}
VSDec: ∀ (x : Value) (y : VSet), {x ∈ y} + {x ∉ y}
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: ∀ x y : Acceptor, {x = y} + {x ≠ y}
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, {Quorum Q} + {¬ Quorum Q}
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
X: ∀ x y : option (Ballot * Value), {x = y} + {x ≠ y}
X0: ∀ x y : AllOrFin VSet, {x = y} + {x ≠ y}
m1, m2: paxos_message
∀ x y : paxos_message_body, {x = y} + {x ≠ y}
  decide equality.
Qed.

Section sec_paxos_acceptor_vlsm.

Context
  (self : Acceptor)
  .

Record paxos_acceptor_state :=
{
  paxos_maxBal : Ballot';
  lastVote : option (Ballot * Value);
  sent_messages : list paxos_message;
}.

Definition maxVBal (sa : paxos_acceptor_state) : Ballot' := fst <$> lastVote sa.
Definition maxVVal (sa : paxos_acceptor_state) : option Value := snd <$> lastVote sa.

Definition paxos_acceptor_initial : paxos_acceptor_state :=
{|
  paxos_maxBal := None;
  lastVote := None;
  sent_messages := [];
|}.

Inductive paxos_acceptor_label : Type :=
| A_send_1b
| A_send_2b.

Definition paxos_acceptor_type : VLSMType paxos_message :=
{|
  state := paxos_acceptor_state;
  label := paxos_acceptor_label;
|}.

Definition paxos_acceptor_valid :
 paxos_acceptor_label -> paxos_acceptor_state * option paxos_message -> Prop :=
  fun l som =>
    match l, som with
    | A_send_1b, (s, Some (b, m_1a)) => (paxos_maxBal s < b)%Z
    | A_send_2b, (s, Some (b, m_2a v)) => (paxos_maxBal s <= b)%Z
    | _, _ => False
    end.

Definition paxos_acceptor_transition
  (l : paxos_acceptor_label) (som : paxos_acceptor_state * option paxos_message)
  : paxos_acceptor_state * option paxos_message :=
  match l, som with
  | A_send_1b, (s, Some (b, m_1a)) =>
      let reply := (b, m_1b self (lastVote s)) in
      ({| paxos_maxBal := Some b; lastVote := lastVote s;
          sent_messages := reply :: sent_messages s; |},
        Some reply)
  | A_send_2b, (s, Some (b, m_2a v)) =>
      let reply := (b, m_2b self v) in
      ({| paxos_maxBal := Some b; lastVote := Some (b, v);
          sent_messages := reply::sent_messages s|},
        Some reply)
  | _, _ => (som.1, None) (* illegal inputs *)
  end.

Definition paxos_acceptor_machine : VLSMMachine paxos_acceptor_type :=
{|
  initial_state_prop := (.= paxos_acceptor_initial);
  s0 := populate (exist _ paxos_acceptor_initial eq_refl);
  initial_message_prop := (fun _ => False);
  valid := paxos_acceptor_valid;
  transition := paxos_acceptor_transition;
|}.

Definition paxos_acceptor_vlsm : VLSM paxos_message := mk_vlsm paxos_acceptor_machine.

Definition paxos_acceptor_has_been_sent
  (s : state paxos_acceptor_vlsm) (m : paxos_message) : Prop :=
    m ∈ sent_messages s.

#[export] Instance paxos_acceptor_has_been_sent_dec :
  RelDecision paxos_acceptor_has_been_sent :=
  fun s m => elem_of_list_dec m (sent_messages s).

Lemma paxos_acceptor_has_been_sent_stepwise_props :
  has_been_sent_stepwise_prop paxos_acceptor_has_been_sent.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
has_been_sent_stepwise_prop
  paxos_acceptor_has_been_sent
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
has_been_sent_stepwise_prop
  paxos_acceptor_has_been_sent
  constructor.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
∀ s : state paxos_acceptor_vlsm,
  initial_state_prop s
  → ∀ m : paxos_message,
      ¬ paxos_acceptor_has_been_sent s m
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
∀ (l : label
         (preloaded_with_all_messages_vlsm
            paxos_acceptor_vlsm)) 
  (s : state
         (preloaded_with_all_messages_vlsm
            paxos_acceptor_vlsm)) 
  (im : option paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             paxos_acceptor_vlsm)) 
  (om : option paxos_message),
  input_constrained_transition paxos_acceptor_vlsm l
    (s, im) (s', om)
  → ∀ msg : paxos_message,
      paxos_acceptor_has_been_sent s' msg
      ↔ field_selector output msg
          {|
            l := l;
            input := im;
            destination := s';
            output := om
          |} ∨ paxos_acceptor_has_been_sent s msg
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
∀ s : state paxos_acceptor_vlsm,
  initial_state_prop s
  → ∀ m : paxos_message,
      ¬ paxos_acceptor_has_been_sent s m intros s Hs m.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
s: state paxos_acceptor_vlsm
Hs: initial_state_prop s
m: paxos_message
¬ paxos_acceptor_has_been_sent s m
    unfold paxos_acceptor_has_been_sent.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
s: state paxos_acceptor_vlsm
Hs: initial_state_prop s
m: paxos_message
m ∉ sent_messages s
    simpl in Hs; subst s.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
m: paxos_message
m ∉ sent_messages paxos_acceptor_initial
    by apply not_elem_of_nil.
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
∀ (l : label
         (preloaded_with_all_messages_vlsm
            paxos_acceptor_vlsm)) (s : state
                                         (preloaded_with_all_messages_vlsm
                                            paxos_acceptor_vlsm)) 
  (im : option paxos_message) (s' : state
                                      (preloaded_with_all_messages_vlsm
                                         paxos_acceptor_vlsm)) 
  (om : option paxos_message),
  input_constrained_transition paxos_acceptor_vlsm l
    (s, im) (s', om)
  → ∀ msg : paxos_message,
      paxos_acceptor_has_been_sent s' msg
      ↔ field_selector output msg
          {|
            l := l;
            input := im;
            destination := s';
            output := om
          |} ∨ paxos_acceptor_has_been_sent s msg intros l s im s' om Htrans msg.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
paxos_acceptor_has_been_sent s' msg
↔ field_selector output msg
    {|
      l := l;
      input := im;
      destination := s';
      output := om
    |} ∨ paxos_acceptor_has_been_sent s msg
    simpl.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
paxos_acceptor_has_been_sent s' msg
↔ om = Some msg ∨ paxos_acceptor_has_been_sent s msg
    enough (H_hist : sent_messages s' =
      match om with Some m' => m' :: sent_messages s | None => sent_messages s end).
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
H_hist: sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
paxos_acceptor_has_been_sent s' msg
↔ om = Some msg ∨ paxos_acceptor_has_been_sent s msg
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
    {
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
H_hist: sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
paxos_acceptor_has_been_sent s' msg
↔ om = Some msg ∨ paxos_acceptor_has_been_sent s msg
      unfold paxos_acceptor_has_been_sent.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
H_hist: sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
msg ∈ sent_messages s'
↔ om = Some msg ∨ msg ∈ sent_messages s
      destruct om; rewrite H_hist, ?elem_of_cons; itauto congruence.
    }
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Htrans: input_constrained_transition
  paxos_acceptor_vlsm l (
  s, im) (s', om)
msg: paxos_message
sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
    destruct Htrans as [(_ & _ & Hvalid) Htran].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Hvalid: valid l (s, im)
Htran: transition l (s, im) = (s', om)
msg: paxos_message
sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
    change transition with paxos_acceptor_transition in Htran.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
self: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
s: state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     paxos_acceptor_vlsm)
om: option paxos_message
Hvalid: valid l (s, im)
Htran: paxos_acceptor_transition l (s, im) = (s', om)
msg: paxos_message
sent_messages s' =
match om with
| Some m' => m' :: sent_messages s
| None => sent_messages s
end
    by destruct l, im as [[? []] |]; simpl in Htran; inversion Htran.
Qed.

#[export] Instance paxos_acceptor_has_been_sent_inst :
  HasBeenSentCapability paxos_acceptor_vlsm :=
{|
  has_been_sent := paxos_acceptor_has_been_sent;
  has_been_sent_dec := paxos_acceptor_has_been_sent_dec;
  has_been_sent_stepwise_props := paxos_acceptor_has_been_sent_stepwise_props;
|}.

End sec_paxos_acceptor_vlsm.

Section sec_paxos_acceptor_vlsm_lem.

Lemma examine_paxos_acceptor_output :
  forall [a l s oim s' ob om],
    paxos_acceptor_transition a l (s, oim) = (s', Some (ob, om)) ->
    match om with
    | m_1b a' _ => l = A_send_1b /\ a' = a
    | m_2b a' _ => l = A_send_2b /\ a' = a
    | _ => False
    end.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : paxos_acceptor_label) (s : paxos_acceptor_state) 
  (oim : option paxos_message) (s' : paxos_acceptor_state) 
  (ob : Ballot) (om : paxos_message_body),
  paxos_acceptor_transition a l (s, oim) =
  (s', Some (ob, om))
  → match om with
    | m_1b a' _ => l = A_send_1b ∧ a' = a
    | m_2b a' _ => l = A_send_2b ∧ a' = a
    | _ => False
    end
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : paxos_acceptor_label) (s : paxos_acceptor_state) 
  (oim : option paxos_message) (s' : paxos_acceptor_state) 
  (ob : Ballot) (om : paxos_message_body),
  paxos_acceptor_transition a l (s, oim) =
  (s', Some (ob, om))
  → match om with
    | m_1b a' _ => l = A_send_1b ∧ a' = a
    | m_2b a' _ => l = A_send_2b ∧ a' = a
    | _ => False
    end
  by intros a [] s [[? []] |] * Ht; inversion Ht.
Qed.

Lemma paxos_maxBal_mono :
  forall a l s im s' om,
    input_constrained_transition (paxos_acceptor_vlsm a) l (s, im) (s', om) ->
    (paxos_maxBal s <= paxos_maxBal s')%Z.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (om : option
                                               paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', om)
  → (paxos_maxBal s ≤ paxos_maxBal s')%Z
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (om : option
                                               paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', om)
  → (paxos_maxBal s ≤ paxos_maxBal s')%Z
  intros * [(_ & _ & Hvalid) Htrans].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Hvalid: valid l (s, im)
Htrans: transition l (s, im) = (s', om)
(paxos_maxBal s ≤ paxos_maxBal s')%Z
  cbn in Hvalid, Htrans;
    unfold paxos_acceptor_valid, paxos_acceptor_transition in Hvalid, Htrans.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Hvalid: match l with
| A_send_1b =>
    match im with
    | Some (b, m_1a) =>
        (paxos_maxBal s < b)%Z
    | Some (b, m_1b _ _) | 
      Some (b, m_1c _) | 
      Some (b, m_2a _) |
      Some (b, m_2b _ _) => False
    | None => False
    end
| A_send_2b =>
    match im with
    | Some (b, m_2a _) =>
        (paxos_maxBal s ≤ b)%Z
    | Some (b, m_1a) | Some (b, m_1b _ _) |
      Some (b, m_1c _) |
      Some (b, m_2b _ _) => False
    | None => False
    end
end
Htrans: match l with
| A_send_1b =>
    match im with
    | Some (b, m_1a) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := lastVote s;
           sent_messages :=
             (b, m_1b a (lastVote s))
             :: sent_messages s
         |}, Some (b, m_1b a (lastVote s)))
    | Some (b, m_1b _ _) | 
      Some (b, m_1c _) | 
      Some (b, m_2a _) |
      Some (b, m_2b _ _) => (
        (s, im).1, None)
    | None => ((s, im).1, None)
    end
| A_send_2b =>
    match im with
    | Some (b, m_2a v) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := Some (b, v);
           sent_messages :=
             (b, m_2b a v) :: sent_messages s
         |}, Some (b, m_2b a v))
    | Some (b, m_1a) | Some (b, m_1b _ _) |
      Some (b, m_1c _) |
      Some (b, m_2b _ _) => (
        (s, im).1, None)
    | None => ((s, im).1, None)
    end
end = (s', om)
(paxos_maxBal s ≤ paxos_maxBal s')%Z
  by repeat case_match; injection Htrans as [= <- <-]; cbn -[Ballot'_to_Z];
    change (Ballot'_to_Z (Some ?b)) with (Ballot_to_Z b); lia.
Qed.

Lemma last_vote_was_sent :
  forall a s,
    constrained_state_prop (paxos_acceptor_vlsm a) s ->
    forall lv,
      lastVote s = Some lv -> has_been_sent (paxos_acceptor_vlsm a) s (lv.1, m_2b a lv.2).
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ lv : Ballot * Value,
      lastVote s = Some lv
      → has_been_sent (paxos_acceptor_vlsm a) s
          (lv.1, m_2b a lv.2)
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ lv : Ballot * Value,
      lastVote s = Some lv
      → has_been_sent (paxos_acceptor_vlsm a) s
          (lv.1, m_2b a lv.2)
  intros a s Hs.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
  induction Hs using valid_state_prop_ind; intros lv Hlv;
    [by rewrite Hs in Hlv |].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
has_been_sent (paxos_acceptor_vlsm a) s'
  (lv.1, m_2b a lv.2)
  rewrite has_been_sent_step_update with (1 := Ht).
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ has_been_sent (paxos_acceptor_vlsm a) s
    (lv.1, m_2b a lv.2)
  cut (om' = Some (lv.1, m_2b a lv.2) \/ lastVote s = lastVote s').
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
→ om' = Some (lv.1, m_2b a lv.2)
  ∨ has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
  {
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
→ om' = Some (lv.1, m_2b a lv.2)
  ∨ has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
    intros []; [by left |].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
H16: lastVote s = lastVote s'
om' = Some (lv.1, m_2b a lv.2)
∨ has_been_sent (paxos_acceptor_vlsm a) s
    (lv.1, m_2b a lv.2)
    by right; apply IHHs; congruence.
  }
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_valid_transition
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) l (
  s, om) (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
  destruct Ht as [_ Ht].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: transition l (s, om) = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
  change transition with (paxos_acceptor_transition a) in Ht.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: paxos_acceptor_transition a l (s, om) = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → has_been_sent (paxos_acceptor_vlsm a) s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
  destruct l; cbn in Ht, IHHs |- *.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: match om with
| Some (b, m_1a) =>
    ({|
       paxos_maxBal := Some b;
       lastVote := lastVote s;
       sent_messages :=
         (b, m_1b a (lastVote s))
         :: sent_messages s
     |}, Some (b, m_1b a (lastVote s)))
| Some (b, m_1b _ _) | Some (b, m_1c _) |
  Some (b, m_2a _) | Some (b, m_2b _ _) =>
    (s, None)
| None => (s, None)
end = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: match om with
| Some (b, m_2a v) =>
    ({|
       paxos_maxBal := Some b;
       lastVote := Some (b, v);
       sent_messages :=
         (b, m_2b a v) :: sent_messages s
     |}, Some (b, m_2b a v))
| Some (b, m_1a) | Some (b, m_1b _ _) |
  Some (b, m_1c _) | Some (b, m_2b _ _) =>
    (s, None)
| None => (s, None)
end = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s'
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: match om with
| Some (b, m_1a) =>
    ({|
       paxos_maxBal := Some b;
       lastVote := lastVote s;
       sent_messages :=
         (b, m_1b a (lastVote s))
         :: sent_messages s
     |}, Some (b, m_1b a (lastVote s)))
| Some (b, m_1b _ _) | Some (b, m_1c _) |
  Some (b, m_2a _) | Some (b, m_2b _ _) =>
    (s, None)
| None => (s, None)
end = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s' right.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: match om with
| Some (b, m_1a) =>
    ({|
       paxos_maxBal := Some b;
       lastVote := lastVote s;
       sent_messages :=
         (b, m_1b a (lastVote s))
         :: sent_messages s
     |}, Some (b, m_1b a (lastVote s)))
| Some (b, m_1b _ _) | Some (b, m_1c _) |
  Some (b, m_2a _) | Some (b, m_2b _ _) =>
    (s, None)
| None => (s, None)
end = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
lastVote s = lastVote s'
    apply (f_equal fst) in Ht; simpl in Ht; subst s'.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote
  match om with
  | Some (b, m_1a) =>
      ({|
         paxos_maxBal := Some b;
         lastVote := lastVote s;
         sent_messages :=
           (b, m_1b a (lastVote s))
           :: sent_messages s
       |}, Some (b, m_1b a (lastVote s)))
  | Some (b, m_1b _ _) | 
    Some (b, m_1c _) | Some (b, m_2a _) |
    Some (b, m_2b _ _) => (
      s, None)
  | None => (s, None)
  end.1 = Some lv
lastVote s =
lastVote
  match om with
  | Some (b, m_1a) =>
      ({|
         paxos_maxBal := Some b;
         lastVote := lastVote s;
         sent_messages :=
           (b, m_1b a (lastVote s)) :: sent_messages s
       |}, Some (b, m_1b a (lastVote s)))
  | Some (b, m_1b _ _) | Some (b, m_1c _) |
    Some (b, m_2a _) | Some (b, m_2b _ _) => (s, None)
  | None => (s, None)
  end.1
    by destruct om as [[? []] |]; simpl.
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om, om': option paxos_message
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: match om with
| Some (b, m_2a v) =>
    ({|
       paxos_maxBal := Some b;
       lastVote := Some (b, v);
       sent_messages :=
         (b, m_2b a v) :: sent_messages s
     |}, Some (b, m_2b a v))
| Some (b, m_1a) | Some (b, m_1b _ _) |
  Some (b, m_1c _) | Some (b, m_2b _ _) =>
    (s, None)
| None => (s, None)
end = (s', om')
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
lv: (Ballot * Value)%type
Hlv: lastVote s' = Some lv
om' = Some (lv.1, m_2b a lv.2)
∨ lastVote s = lastVote s' destruct lv as [b_lv v_lv], om as [[? []]|]; simpl in *;
      injection Ht as [= <- <-]; try (by right); [].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
s: paxos_acceptor_state
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
b_lv: Ballot
v_lv: Value
Hlv: lastVote
  {|
    paxos_maxBal := Some b;
    lastVote := Some (b, v);
    sent_messages :=
      (b, m_2b a v) :: sent_messages s
  |} = Some (b_lv, v_lv)
Some (b, m_2b a v) = Some (b_lv, m_2b a v_lv)
∨ lastVote s =
  lastVote
    {|
      paxos_maxBal := Some b;
      lastVote := Some (b, v);
      sent_messages :=
        (b, m_2b a v) :: sent_messages s
    |}
    left; simpl in Hlv.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
s: paxos_acceptor_state
IHHs: ∀ lv : Ballot * Value,
  lastVote s = Some lv
  → paxos_acceptor_has_been_sent a s
      (lv.1, m_2b a lv.2)
b_lv: Ballot
v_lv: Value
Hlv: Some (b, v) = Some (b_lv, v_lv)
Some (b, m_2b a v) = Some (b_lv, m_2b a v_lv)
    by congruence.
Qed.

Lemma paxos_acceptor_sent_bounds_maxBal :
  forall a s,
    constrained_state_prop (paxos_acceptor_vlsm a) s ->
  forall b mb,
    has_been_sent (paxos_acceptor_vlsm a) s (b, mb) ->
    (b <= paxos_maxBal s)%Z.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ (b : Ballot) (mb : paxos_message_body),
      has_been_sent (paxos_acceptor_vlsm a) s (b, mb)
      → (b ≤ paxos_maxBal s)%Z
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ (b : Ballot) (mb : paxos_message_body),
      has_been_sent (paxos_acceptor_vlsm a) s (b, mb)
      → (b ≤ paxos_maxBal s)%Z
  intros a s Hs b mb.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
has_been_sent (paxos_acceptor_vlsm a) s (b, mb)
→ (b ≤ paxos_maxBal s)%Z
  apply (from_send_to_from_sent_argument
    (paxos_acceptor_vlsm a) (fun s => b <= paxos_maxBal s)%Z); [.. | done].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
∀ (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (l : label
                                             (preloaded_with_all_messages_vlsm
                                                (paxos_acceptor_vlsm
                                                 a))) 
  (oim : option paxos_message) (s' : state
                                       (preloaded_with_all_messages_vlsm
                                          (paxos_acceptor_vlsm
                                             a))) 
  (oom : option paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, oim) (s', oom)
  → (b ≤ paxos_maxBal s)%Z → (b ≤ paxos_maxBal s')%Z
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
∀ (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) 
  (l : label
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) 
  (oim : option paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))),
  input_constrained_transition 
    (paxos_acceptor_vlsm a) l (
    s, oim) (s', Some (b, mb))
  → (b ≤ paxos_maxBal s')%Z
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
∀ (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (l : label
                                             (preloaded_with_all_messages_vlsm
                                                (paxos_acceptor_vlsm
                                                 a))) 
  (oim : option paxos_message) (s' : state
                                       (preloaded_with_all_messages_vlsm
                                          (paxos_acceptor_vlsm
                                             a))) 
  (oom : option paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, oim) (s', oom)
  → (b ≤ paxos_maxBal s)%Z → (b ≤ paxos_maxBal s')%Z by intros * Ht; apply paxos_maxBal_mono in Ht; lia.
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
∀ (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (l : label
                                             (preloaded_with_all_messages_vlsm
                                                (paxos_acceptor_vlsm
                                                 a))) 
  (oim : option paxos_message) (s' : state
                                       (preloaded_with_all_messages_vlsm
                                          (paxos_acceptor_vlsm
                                             a))),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, oim) (s', Some (b, mb))
  → (b ≤ paxos_maxBal s')%Z intros * [_ Htrans].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
s0: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
oim: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Htrans: transition l (s0, oim) = (s', Some (b, mb))
(b ≤ paxos_maxBal s')%Z
    cbn in Htrans; unfold paxos_acceptor_transition in Htrans.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b: Ballot
mb: paxos_message_body
s0: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
oim: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Htrans: match l with
| A_send_1b =>
    match oim with
    | Some (b, m_1a) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := lastVote s0;
           sent_messages :=
             (b, m_1b a (lastVote s0))
             :: sent_messages s0
         |}, Some (b, m_1b a (lastVote s0)))
    | Some (b, m_1b _ _) | 
      Some (b, m_1c _) | 
      Some (b, m_2a _) |
      Some (b, m_2b _ _) =>
        ((s0, oim).1, None)
    | None => ((s0, oim).1, None)
    end
| A_send_2b =>
    match oim with
    | Some (b, m_2a v) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := Some (b, v);
           sent_messages :=
             (b, m_2b a v)
             :: sent_messages s0
         |}, Some (b, m_2b a v))
    | Some (b, m_1a) | Some (b, m_1b _ _) |
      Some (b, m_1c _) |
      Some (b, m_2b _ _) =>
        ((s0, oim).1, None)
    | None => ((s0, oim).1, None)
    end
end = (s', Some (b, mb))
(b ≤ paxos_maxBal s')%Z
    by repeat case_match; inversion Htrans.
Qed.

Lemma maxVBal_le_paxos_maxBal :
  forall a s,
    constrained_state_prop (paxos_acceptor_vlsm a) s ->
      (maxVBal s <= paxos_maxBal s)%Z.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → (maxVBal s ≤ paxos_maxBal s)%Z
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → (maxVBal s ≤ paxos_maxBal s)%Z
  intros a s Hs.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
(maxVBal s ≤ paxos_maxBal s)%Z
  unfold maxVBal.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
(fst <$> lastVote s ≤ paxos_maxBal s)%Z
  destruct (lastVote s) as [[b_lv v_lv] |] eqn: Heq; simpl.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b_lv: Ballot
v_lv: Value
Heq: lastVote s = Some (b_lv, v_lv)
(Z.of_N b_lv ≤ paxos_maxBal s)%Z
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
Heq: lastVote s = None
(-1 ≤ paxos_maxBal s)%Z
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b_lv: Ballot
v_lv: Value
Heq: lastVote s = Some (b_lv, v_lv)
(Z.of_N b_lv ≤ paxos_maxBal s)%Z eapply paxos_acceptor_sent_bounds_maxBal; [done |].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
b_lv: Ballot
v_lv: Value
Heq: lastVote s = Some (b_lv, v_lv)
has_been_sent (paxos_acceptor_vlsm a) s (b_lv, ?mb)
    by apply (last_vote_was_sent a s Hs _ Heq).
  -
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Hs: constrained_state_prop (paxos_acceptor_vlsm a) s
Heq: lastVote s = None
(-1 ≤ paxos_maxBal s)%Z by destruct (paxos_maxBal s); simpl; lia.
Qed.

Lemma maxVBal_mono :
  forall a l s im s' om,
    input_constrained_transition (paxos_acceptor_vlsm a) l (s, im) (s', om) ->
    (maxVBal s <= maxVBal s')%Z.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (om : option
                                               paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', om) → (maxVBal s ≤ maxVBal s')%Z
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (om : option
                                               paxos_message),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', om) → (maxVBal s ≤ maxVBal s')%Z
  intros * Ht.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Ht: input_constrained_transition
  (paxos_acceptor_vlsm a) l (
  s, im) (s', om)
(maxVBal s ≤ maxVBal s')%Z
  destruct Ht as [(Hs & _ & Hvalid) Htrans].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) s
Hvalid: valid l (s, im)
Htrans: transition l (s, im) = (s', om)
(maxVBal s ≤ maxVBal s')%Z
  cbn in Hvalid, Htrans; unfold paxos_acceptor_valid, paxos_acceptor_transition in Hvalid, Htrans.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) s
Hvalid: match l with
| A_send_1b =>
    match im with
    | Some (b, m_1a) =>
        (paxos_maxBal s < b)%Z
    | Some (b, m_1b _ _) | 
      Some (b, m_1c _) | 
      Some (b, m_2a _) |
      Some (b, m_2b _ _) => False
    | None => False
    end
| A_send_2b =>
    match im with
    | Some (b, m_2a _) =>
        (paxos_maxBal s ≤ b)%Z
    | Some (b, m_1a) | Some (b, m_1b _ _) |
      Some (b, m_1c _) |
      Some (b, m_2b _ _) => False
    | None => False
    end
end
Htrans: match l with
| A_send_1b =>
    match im with
    | Some (b, m_1a) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := lastVote s;
           sent_messages :=
             (b, m_1b a (lastVote s))
             :: sent_messages s
         |}, Some (b, m_1b a (lastVote s)))
    | Some (b, m_1b _ _) | 
      Some (b, m_1c _) | 
      Some (b, m_2a _) |
      Some (b, m_2b _ _) => (
        (s, im).1, None)
    | None => ((s, im).1, None)
    end
| A_send_2b =>
    match im with
    | Some (b, m_2a v) =>
        ({|
           paxos_maxBal := Some b;
           lastVote := Some (b, v);
           sent_messages :=
             (b, m_2b a v) :: sent_messages s
         |}, Some (b, m_2b a v))
    | Some (b, m_1a) | Some (b, m_1b _ _) |
      Some (b, m_1c _) |
      Some (b, m_2b _ _) => (
        (s, im).1, None)
    | None => ((s, im).1, None)
    end
end = (s', om)
(maxVBal s ≤ maxVBal s')%Z
  repeat case_match; inversion Htrans; cbn; try done.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
om: option paxos_message
Hs: valid_state_prop
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a)) s
H16: l = A_send_2b
p: paxos_message
b: Ballot
p0: paxos_message_body
v: Value
H19: p0 = m_2a v
H18: p = (b, m_2a v)
H17: im = Some (b, m_2a v)
Hvalid: (paxos_maxBal s ≤ b)%Z
Htrans: ({|
   paxos_maxBal := Some b;
   lastVote := Some (b, v);
   sent_messages :=
     (b, m_2b a v) :: sent_messages s
 |}, Some (b, m_2b a v)) = (
s', om)
H21: {|
  paxos_maxBal := Some b;
  lastVote := Some (b, v);
  sent_messages :=
    (b, m_2b a v) :: sent_messages s
|} = s'
H22: Some (b, m_2b a v) = om
(maxVBal s ≤ Z.of_N b)%Z
  by transitivity (paxos_maxBal s); [apply maxVBal_le_paxos_maxBal |].
Qed.

Lemma sent_vote_le_maxVBal :
  forall a s,
    constrained_state_prop (paxos_acceptor_vlsm a) s ->
  forall b v,
    has_been_sent (paxos_acceptor_vlsm a) s (b, m_2b a v) ->
    (b <= maxVBal s)%Z.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ (b : Ballot) (v : Value),
      has_been_sent (paxos_acceptor_vlsm a) s
        (b, m_2b a v) → (b ≤ maxVBal s)%Z
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (s : state
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → ∀ (b : Ballot) (v : Value),
      has_been_sent (paxos_acceptor_vlsm a) s
        (b, m_2b a v) → (b ≤ maxVBal s)%Z
  intros a s Hs b v; revert s Hs.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
∀ s : state
        (preloaded_with_all_messages_vlsm
           (paxos_acceptor_vlsm a)),
  constrained_state_prop (paxos_acceptor_vlsm a) s
  → has_been_sent (paxos_acceptor_vlsm a) s
      (b, m_2b a v) → (b ≤ maxVBal s)%Z
  apply (from_send_to_from_sent_argument (paxos_acceptor_vlsm a) (fun s => b <= maxVBal s)%Z);
    intros * Ht; [by apply maxVBal_mono in Ht; lia |].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
oim: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Ht: input_constrained_transition
  (paxos_acceptor_vlsm a) l (
  s, oim) (s', Some (b, m_2b a v))
(b ≤ maxVBal s')%Z
  destruct Ht as [_ Htrans].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
oim: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Htrans: transition l (s, oim) =
(s', Some (b, m_2b a v))
(b ≤ maxVBal s')%Z
  destruct (examine_paxos_acceptor_output Htrans) as [-> _].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
b: Ballot
v: Value
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
oim: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
Htrans: transition A_send_2b (s, oim) =
(s', Some (b, m_2b a v))
(b ≤ maxVBal s')%Z
  by cbn in Htrans; repeat case_match; inversion Htrans.
Qed.

Lemma sending_1b_updates_maxBal :
  forall [a l s im s' b lv],
    input_constrained_transition (paxos_acceptor_vlsm a) l (s, im) (s', Some (b, m_1b a lv)) ->
    (paxos_maxBal s < b)%Z /\ (paxos_maxBal s' = Some b).
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (b : Ballot) 
  (lv : option (Ballot * Value)),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', Some (b, m_1b a lv))
  → (paxos_maxBal s < b)%Z ∧ paxos_maxBal s' = Some b
Proof.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
∀ (a : Acceptor) (l : label
                        (preloaded_with_all_messages_vlsm
                           (paxos_acceptor_vlsm a))) 
  (s : state
         (preloaded_with_all_messages_vlsm
            (paxos_acceptor_vlsm a))) (im : option
                                              paxos_message) 
  (s' : state
          (preloaded_with_all_messages_vlsm
             (paxos_acceptor_vlsm a))) (b : Ballot) 
  (lv : option (Ballot * Value)),
  input_constrained_transition (paxos_acceptor_vlsm a)
    l (s, im) (s', Some (b, m_1b a lv))
  → (paxos_maxBal s < b)%Z ∧ paxos_maxBal s' = Some b
  intros * [(_ & _ & Hvalid) Hstep]; cbn in Hstep.
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
l: label
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
b: Ballot
lv: option (Ballot * Value)
Hvalid: valid l (s, im)
Hstep: paxos_acceptor_transition a l (s, im) =
(s', Some (b, m_1b a lv))
(paxos_maxBal s < b)%Z ∧ paxos_maxBal s' = Some b
  apply examine_paxos_acceptor_output in Hstep as Hla; destruct Hla as [-> _].
Value, VSet: Type
H: ElemOf Value VSet
H0: Empty VSet
H1: Singleton Value VSet
H2: Union VSet
H3: Intersection VSet
H4: Difference VSet
H5: Elements Value VSet
EqDecision0: EqDecision Value
H6: FinSet Value VSet
EqDecision1: EqDecision VSet
VSDec: RelDecision elem_of
Acceptor: Type
AMap: Type → Type
H7: FMap AMap
H8: ∀ A : Type, Lookup Acceptor A (AMap A)
H9: ∀ A : Type, Empty (AMap A)
H10: ∀ A : Type, PartialAlter Acceptor A (AMap A)
H11: OMap AMap
H12: Merge AMap
H13: ∀ A : Type, MapFold Acceptor A (AMap A)
EqDecision2: EqDecision Acceptor
H14: FinMap Acceptor AMap
H15: finite.Finite Acceptor
Quorum: ASet → Prop
QDec: ∀ Q : ASet, Decision (Quorum Q)
QClosed: Proper (subseteq ==> impl) Quorum
QA: ∀ Q1 Q2 : {x : ASet | Quorum x},
  ∃ a : Acceptor, a ∈ `Q1 ∩ `Q2
a: Acceptor
s: state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
im: option paxos_message
s': state
  (preloaded_with_all_messages_vlsm
     (paxos_acceptor_vlsm a))
b: Ballot
lv: option (Ballot * Value)
Hstep: paxos_acceptor_transition a A_send_1b (s, im) =
(s', Some (b, m_1b a lv))
Hvalid: valid A_send_1b (s, im)
(paxos_maxBal s < b)%Z ∧ paxos_maxBal s' = Some b
  by destruct im as [[? []] |]; cbn in s, s', Hvalid; inversion Hstep; subst.
Qed.

End sec_paxos_acceptor_vlsm_lem.

Section sec_leaders_vlsm.