---

Lemma: test
True

Comment: EventML spec properties
exports:                 []
prefix:                  pv11_p1:s
name:                    paxos-v11-part1.esh:s

Comment: ------ pv11_p1 - types ------
⋅

Definition: pv11_p1_Ballot_Num
pv11_p1_Ballot_Num() ==  ℤ × Id?

Lemma: pv11_p1_Ballot_Num_wf
pv11_p1_Ballot_Num() ∈ Type

Definition: pv11_p1_abs_Ballot_Num
pv11_p1_abs_Ballot_Num() ==  λx.x

Lemma: pv11_p1_abs_Ballot_Num_wf
pv11_p1_abs_Ballot_Num() ∈ (ℤ × Id?) ─→ pv11_p1_Ballot_Num()

Definition: pv11_p1_rep_Ballot_Num
pv11_p1_rep_Ballot_Num() ==  λx.x

Lemma: pv11_p1_rep_Ballot_Num_wf
pv11_p1_rep_Ballot_Num() ∈ pv11_p1_Ballot_Num() ─→ (ℤ × Id?)

Definition: pv11_p1_mk_bnum
pv11_p1_mk_bnum() ==  λn,loc. (inl <n, loc>)

Lemma: pv11_p1_mk_bnum_wf
pv11_p1_mk_bnum() ∈ ℤ ─→ Id ─→ pv11_p1_Ballot_Num()

Definition: pv11_p1_is_bnum
pv11_p1_is_bnum() ==  λbnum.isl(bnum)

Lemma: pv11_p1_is_bnum_wf
pv11_p1_is_bnum() ∈ pv11_p1_Ballot_Num() ─→ 𝔹

Definition: pv11_p1_upd_bnum
pv11_p1_upd_bnum() ==  λbnum,loc. case bnum of inl(z) => let r,l = z in pv11_p1_mk_bnum() (r + 1) loc | inr(z) => bnum

Lemma: pv11_p1_upd_bnum_wf
pv11_p1_upd_bnum() ∈ pv11_p1_Ballot_Num() ─→ Id ─→ pv11_p1_Ballot_Num()

Definition: pv11_p1_dummy_ballot
pv11_p1_dummy_ballot() ==  inr ⋅ 

Lemma: pv11_p1_dummy_ballot_wf
pv11_p1_dummy_ballot() ∈ pv11_p1_Ballot_Num()

Definition: pv11_p1_leq_bnum'
pv11_p1_leq_bnum'(ldrs_uid) ==
  λza,z. let i1,l1 = za in let i2,l2 = z in i1 <z i2 ∨b((i1 =z i2) ∧b ldrs_uid l1 ≤z ldrs_uid l2)

Lemma: pv11_p1_leq_bnum'_wf
∀[ldrs_uid:Id ─→ ℤ]. (pv11_p1_leq_bnum'(ldrs_uid) ∈ (ℤ × Id) ─→ (ℤ × Id) ─→ 𝔹)

Definition: pv11_p1_leq_bnum
pv11_p1_leq_bnum(ldrs_uid) ==
  λbn1,bn2. case bn1
            of inl(x1) =>
            case bn2 of inl(x2) => pv11_p1_leq_bnum'(ldrs_uid) x1 x2 | inr(z) => ff
            | inr(z) =>
            tt

Lemma: pv11_p1_leq_bnum_wf
∀[ldrs_uid:Id ─→ ℤ]. (pv11_p1_leq_bnum(ldrs_uid) ∈ pv11_p1_Ballot_Num() ─→ pv11_p1_Ballot_Num() ─→ 𝔹)

Definition: pv11_p1_lt_bnum'
pv11_p1_lt_bnum'(ldrs_uid) ==
  λzb,z. let i1,l1 = zb in let i2,l2 = z in i1 <z i2 ∨b((i1 =z i2) ∧b ldrs_uid l1 <z ldrs_uid l2)

Lemma: pv11_p1_lt_bnum'_wf
∀[ldrs_uid:Id ─→ ℤ]. (pv11_p1_lt_bnum'(ldrs_uid) ∈ (ℤ × Id) ─→ (ℤ × Id) ─→ 𝔹)

Definition: pv11_p1_lt_bnum
pv11_p1_lt_bnum{ABS:q, paxos-v11-part1.esh:o}(ldrs_uid) ==
  λbn1,bn2. case bn1
            of inl(x1) =>
            case bn2 of inl(x2) => pv11_p1_lt_bnum'(ldrs_uid) x1 x2 | inr(z) => ff
            | inr(z) =>
            isl(bn2)

Lemma: pv11_p1_lt_bnum_wf
∀[ldrs_uid:Id ─→ ℤ]. (pv11_p1_lt_bnum(ldrs_uid) ∈ pv11_p1_Ballot_Num() ─→ pv11_p1_Ballot_Num() ─→ 𝔹)

Definition: pv11_p1_eq_bnums
pv11_p1_eq_bnums() ==  λbn1,bn2. (union-deq(ℤ × Id;Unit;product-deq(ℤ;Id;IntDeq;IdDeq);UnitDeq) bn1 bn2)

Lemma: pv11_p1_eq_bnums_wf
pv11_p1_eq_bnums() ∈ pv11_p1_Ballot_Num() ─→ pv11_p1_Ballot_Num() ─→ 𝔹

Lemma: pv11_p1_eq_bnums-assert
∀[x,y:pv11_p1_Ballot_Num()].  uiff(↑(pv11_p1_eq_bnums() x y);x = y)

Comment: ------ pv11_p1 - headers ------
⋅

Definition: pv11_p1_headers
pv11_p1_headers() ==
  [``pv11_p1 p1a``;
   ``pv11_p1 p1b``;
   ``pv11_p1 p2a``;
   ``pv11_p1 p2b``;
   ``pv11_p1 preempted``;
   ``pv11_p1 adopted``;
   [propose];
   [decision]]

Lemma: pv11_p1_headers_wf
pv11_p1_headers() ∈ Name List

Definition: pv11_p1_headers_no_rep
pv11_p1_headers_no_rep() ==  no_repeats(Name;pv11_p1_headers())

Lemma: pv11_p1_headers_no_rep_wf
pv11_p1_headers_no_rep() ∈ ℙ

Definition: pv11_p1_headers_fun
pv11_p1_headers_fun(Cmd) ==
  λhdr.if name_eq(hdr;``pv11_p1 p1a``) then Id × pv11_p1_Ballot_Num()
       if name_eq(hdr;``pv11_p1 p1b``)
         then Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
       if name_eq(hdr;``pv11_p1 p2a``) then Id × pv11_p1_Ballot_Num() × ℤ × Cmd
       if name_eq(hdr;``pv11_p1 p2b``) then Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()
       if name_eq(hdr;``pv11_p1 preempted``) then pv11_p1_Ballot_Num()
       if name_eq(hdr;``pv11_p1 adopted``) then pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
       if name_eq(hdr;[propose]) then ℤ × Cmd
       if name_eq(hdr;[decision]) then ℤ × Cmd
       else Top
       fi 

Lemma: pv11_p1_headers_fun_wf
∀[Cmd:ValueAllType]. (pv11_p1_headers_fun(Cmd) ∈ Name ─→ Type)

Definition: pv11_p1_headers_type
pv11_p1_headers_type{i:l}(Cmd) ==
  {mf:Name ─→ ValueAllType| 
   pv11_p1_headers_no_rep() ∧ (∀hdr∈pv11_p1_headers().(mf hdr) = (pv11_p1_headers_fun(Cmd) hdr))} 

Lemma: pv11_p1_headers_type_wf
∀[Cmd:ValueAllType]. (pv11_p1_headers_type{i:l}(Cmd) ∈ ℙ')

Comment: ------ pv11_p1 - specification ------
⋅

Definition: pv11_p1_max_bnum
pv11_p1_max_bnum(ldrs_uid) ==  λbn1,bn2. if pv11_p1_leq_bnum(ldrs_uid) bn1 bn2 then bn2 else bn1 fi 

Lemma: pv11_p1_max_bnum_wf
∀[ldrs_uid:Id ─→ ℤ]. (pv11_p1_max_bnum(ldrs_uid) ∈ pv11_p1_Ballot_Num() ─→ pv11_p1_Ballot_Num() ─→ pv11_p1_Ballot_Num())

Definition: pv11_p1_pmax
pv11_p1_pmax(Cmd;ldrs_uid) ==
  λpvals.let g = λbn,slt,z. let bn',z = z in let s',z = z in (slt =z s') ∧b (bn  < bn') in
          let P = λz.let bn,z = z 
                     in let s,c = z 
                        in ¬b(∃zw∈pvals.g bn s zw)_b in
          mapfilter(λx.(snd(x));P;pvals)

Lemma: pv11_p1_pmax_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_pmax(Cmd;ldrs_uid) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) ─→ ((ℤ × Cmd) List))

Definition: pv11_p1_update_proposals
pv11_p1_update_proposals(Cmd) ==
  λproposals1,proposals2. (filter(λprp.(¬b(∃prp'∈proposals2.(fst(prp) =z fst(prp')))_b);proposals1) @ proposals2)

Lemma: pv11_p1_update_proposals_wf
∀[Cmd:ValueAllType]. (pv11_p1_update_proposals(Cmd) ∈ ((ℤ × Cmd) List) ─→ ((ℤ × Cmd) List) ─→ ((ℤ × Cmd) List))

Definition: pv11_p1_in_domain
pv11_p1_in_domain(Cmd) ==  λx,xys. x ∈b map(λx.(fst(x));xys))

Lemma: pv11_p1_in_domain_wf
∀[Cmd:ValueAllType]. (pv11_p1_in_domain(Cmd) ∈ ℤ ─→ ((ℤ × Cmd) List) ─→ 𝔹)

Definition: pv11_p1_same_proposal
pv11_p1_same_proposal(Cmd) ==  λzc,z. let slt1,cmd1 = zc in let slt2,cmd2 = z in (slt1 =z slt2)

Lemma: pv11_p1_same_proposal_wf
∀[Cmd:ValueAllType]. (pv11_p1_same_proposal(Cmd) ∈ (ℤ × Cmd) ─→ (ℤ × Cmd) ─→ 𝔹)

Definition: pv11_p1_same_pvalue
pv11_p1_same_pvalue(Cmd) ==
  λzd,z. let bnum1,prp1 = zd 
         in let bnum2,prp2 = z 
            in (pv11_p1_eq_bnums() bnum1 bnum2) ∧b (pv11_p1_same_proposal(Cmd) prp1 prp2)

Lemma: pv11_p1_same_pvalue_wf
∀[Cmd:ValueAllType]
  (pv11_p1_same_pvalue(Cmd) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ 𝔹)

Definition: pv11_p1_add_if_new
pv11_p1_add_if_new() ==  λtest,val,lst. if (∃zzc∈lst.test val zzc)_b then lst else lst @ [val] fi 

Lemma: pv11_p1_add_if_new_wf
pv11_p1_add_if_new() ∈ ∩A:𝕌'. ((A ─→ A ─→ 𝔹) ─→ A ─→ (A List) ─→ (A List))

Definition: pv11_p1_append_news
pv11_p1_append_news(Cmd) ==
  λtest,zzg,zzh. accumulate (with value a and list item x):
                  pv11_p1_add_if_new() test x a
                 over list:
                   zzh
                 with starting value:
                  zzg)

Lemma: pv11_p1_append_news_wf
∀[Cmd:ValueAllType]
  (pv11_p1_append_news(Cmd) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ 𝔹)
   ─→ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
   ─→ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
   ─→ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

Definition: pv11_p1_threshold
pv11_p1_threshold(accpts) ==  (#(accpts) + 1) ÷ 2

Lemma: pv11_p1_threshold_wf
∀[accpts:bag(Id)]. (pv11_p1_threshold(accpts) ∈ ℤ)

Definition: pv11_p1_p1a'base
pv11_p1_p1a'base(Cmd;mf) ==  Base(``pv11_p1 p1a``)

Lemma: pv11_p1_p1a'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1a'base(Cmd;mf) ∈ EClass(Id × pv11_p1_Ballot_Num()))

Definition: pv11_p1_p1a'base-program
pv11_p1_p1a'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 p1a``)

Lemma: pv11_p1_p1a'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1a'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_p1a'base(Cmd;mf)))

Definition: pv11_p1_p1a'broadcast
pv11_p1_p1a'broadcast(Cmd;mf) ==  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``pv11_p1 p1a``;z));locs)

Lemma: pv11_p1_p1a'broadcast_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1a'broadcast(Cmd;mf) ∈ bag(Id) ─→ (Id × pv11_p1_Ballot_Num()) ─→ bag(Interface))

Definition: pv11_p1_p1b'base
pv11_p1_p1b'base(Cmd;mf) ==  Base(``pv11_p1 p1b``)

Lemma: pv11_p1_p1b'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1b'base(Cmd;mf) ∈ EClass(Id
   × pv11_p1_Ballot_Num()
   × pv11_p1_Ballot_Num()
   × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Definition: pv11_p1_p1b'base-program
pv11_p1_p1b'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 p1b``)

Lemma: pv11_p1_p1b'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1b'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_p1b'base(Cmd;mf)))

Definition: pv11_p1_p1b'send
pv11_p1_p1b'send(Cmd;mf) ==  λl,z. mk-msg-interface(l;make-Msg(``pv11_p1 p1b``;z))

Lemma: pv11_p1_p1b'send_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p1b'send(Cmd;mf) ∈ Id
   ─→ (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ Interface)

Definition: pv11_p1_p2a'base
pv11_p1_p2a'base(Cmd;mf) ==  Base(``pv11_p1 p2a``)

Lemma: pv11_p1_p2a'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2a'base(Cmd;mf) ∈ EClass(Id × pv11_p1_Ballot_Num() × ℤ × Cmd))

Definition: pv11_p1_p2a'base-program
pv11_p1_p2a'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 p2a``)

Lemma: pv11_p1_p2a'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2a'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_p2a'base(Cmd;mf)))

Definition: pv11_p1_p2a'broadcast
pv11_p1_p2a'broadcast(Cmd;mf) ==  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg(``pv11_p1 p2a``;z));locs)

Lemma: pv11_p1_p2a'broadcast_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2a'broadcast(Cmd;mf) ∈ bag(Id) ─→ (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ bag(Interface))

Definition: pv11_p1_p2b'base
pv11_p1_p2b'base(Cmd;mf) ==  Base(``pv11_p1 p2b``)

Lemma: pv11_p1_p2b'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2b'base(Cmd;mf) ∈ EClass(Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()))

Definition: pv11_p1_p2b'base-program
pv11_p1_p2b'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 p2b``)

Lemma: pv11_p1_p2b'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2b'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_p2b'base(Cmd;mf)))

Definition: pv11_p1_p2b'send
pv11_p1_p2b'send(Cmd;mf) ==  λl,z. mk-msg-interface(l;make-Msg(``pv11_p1 p2b``;z))

Lemma: pv11_p1_p2b'send_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2b'send(Cmd;mf) ∈ Id ─→ (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ─→ Interface)

Definition: pv11_p1_preempted'base
pv11_p1_preempted'base(Cmd;mf) ==  Base(``pv11_p1 preempted``)

Lemma: pv11_p1_preempted'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_preempted'base(Cmd;mf) ∈ EClass(pv11_p1_Ballot_Num()))

Definition: pv11_p1_preempted'base-program
pv11_p1_preempted'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 preempted``)

Lemma: pv11_p1_preempted'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_preempted'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_preempted'base(Cmd;mf)))

Definition: pv11_p1_preempted'send
pv11_p1_preempted'send(Cmd;mf) ==  λl,z. mk-msg-interface(l;make-Msg(``pv11_p1 preempted``;z))

Lemma: pv11_p1_preempted'send_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_preempted'send(Cmd;mf) ∈ Id ─→ pv11_p1_Ballot_Num() ─→ Interface)

Definition: pv11_p1_adopted'base
pv11_p1_adopted'base(Cmd;mf) ==  Base(``pv11_p1 adopted``)

Lemma: pv11_p1_adopted'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_adopted'base(Cmd;mf) ∈ EClass(pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Definition: pv11_p1_adopted'base-program
pv11_p1_adopted'base-program(Cmd;mf) ==  base-class-program(``pv11_p1 adopted``)

Lemma: pv11_p1_adopted'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_adopted'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_adopted'base(Cmd;mf)))

Definition: pv11_p1_adopted'send
pv11_p1_adopted'send(Cmd;mf) ==  λl,z. mk-msg-interface(l;make-Msg(``pv11_p1 adopted``;z))

Lemma: pv11_p1_adopted'send_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_adopted'send(Cmd;mf) ∈ Id ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ─→ Interface)

Definition: pv11_p1_propose'base
pv11_p1_propose'base(Cmd;mf) ==  Base([propose])

Lemma: pv11_p1_propose'base_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].  (pv11_p1_propose'base(Cmd;mf) ∈ EClass(ℤ × Cmd))

Definition: pv11_p1_propose'base-program
pv11_p1_propose'base-program(Cmd;mf) ==  base-class-program([propose])

Lemma: pv11_p1_propose'base-program_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_propose'base-program(Cmd;mf) ∈ LocalClass(pv11_p1_propose'base(Cmd;mf)))

Definition: pv11_p1_decision'broadcast
pv11_p1_decision'broadcast(Cmd;mf) ==  λlocs,z. bag-map(λl.mk-msg-interface(l;make-Msg([decision];z));locs)

Lemma: pv11_p1_decision'broadcast_wf
∀[Cmd:ValueAllType]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_decision'broadcast(Cmd;mf) ∈ bag(Id) ─→ (ℤ × Cmd) ─→ bag(Interface))

Definition: pv11_p1_init_accepted
pv11_p1_init_accepted(Cmd) ==  []

Lemma: pv11_p1_init_accepted_wf
∀[Cmd:ValueAllType]. (pv11_p1_init_accepted(Cmd) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) List)

Definition: pv11_p1_init_acceptor
pv11_p1_init_acceptor(Cmd) ==  <pv11_p1_dummy_ballot(), pv11_p1_init_accepted(Cmd)>

Lemma: pv11_p1_init_acceptor_wf
∀[Cmd:ValueAllType]. (pv11_p1_init_acceptor(Cmd) ∈ pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

Definition: pv11_p1_init_slot_num
pv11_p1_init_slot_num() ==  1

Lemma: pv11_p1_init_slot_num_wf
pv11_p1_init_slot_num() ∈ ℤ

Definition: pv11_p1_init_proposals
pv11_p1_init_proposals(Cmd) ==  []

Lemma: pv11_p1_init_proposals_wf
∀[Cmd:ValueAllType]. (pv11_p1_init_proposals(Cmd) ∈ (ℤ × Cmd) List)

Definition: pv11_p1_init_pvalues
pv11_p1_init_pvalues(Cmd) ==  []

Lemma: pv11_p1_init_pvalues_wf
∀[Cmd:ValueAllType]. (pv11_p1_init_pvalues(Cmd) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) List)

Definition: pv11_p1_init_scout
pv11_p1_init_scout(Cmd;accpts) ==  <accpts, pv11_p1_init_pvalues(Cmd)>

Lemma: pv11_p1_init_scout_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)].
  (pv11_p1_init_scout(Cmd;accpts) ∈ bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

Definition: pv11_p1_init_ballot_num
pv11_p1_init_ballot_num() ==  λloc.(pv11_p1_mk_bnum() 0 loc)

Lemma: pv11_p1_init_ballot_num_wf
pv11_p1_init_ballot_num() ∈ Id ─→ pv11_p1_Ballot_Num()

Definition: pv11_p1_init_active
pv11_p1_init_active() ==  ff

Lemma: pv11_p1_init_active_wf
pv11_p1_init_active() ∈ 𝔹

Definition: pv11_p1_init_leader
pv11_p1_init_leader(Cmd) ==  λloc.<pv11_p1_init_ballot_num() loc, pv11_p1_init_active(), pv11_p1_init_proposals(Cmd)>

Lemma: pv11_p1_init_leader_wf
∀[Cmd:ValueAllType]. (pv11_p1_init_leader(Cmd) ∈ Id ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))

Definition: pv11_p1_on_p1a
pv11_p1_on_p1a(Cmd;ldrs_uid) ==
  λloc,ze,z. let loc,bnum = ze in let ballot_num,accepted = z in <pv11_p1_max_bnum(ldrs_uid) bnum ballot_num, accepted>

Lemma: pv11_p1_on_p1a_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_on_p1a(Cmd;ldrs_uid) ∈ Id
   ─→ (Id × pv11_p1_Ballot_Num())
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Definition: pv11_p1_on_p2a
pv11_p1_on_p2a(Cmd;ldrs_uid) ==
  λloc,zf,z. let loc,zg = zf 
             in let b,sp = zg 
                in let ballot_num,accepted = z 
                   in let ballot_num' = pv11_p1_max_bnum(ldrs_uid) b ballot_num in
                       let accepted' = if pv11_p1_leq_bnum(ldrs_uid) ballot_num b
                                       then pv11_p1_add_if_new() pv11_p1_same_pvalue(Cmd) <b, sp> accepted
                                       else accepted
                                       fi  in
                       <ballot_num', accepted'>

Lemma: pv11_p1_on_p2a_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_on_p2a(Cmd;ldrs_uid) ∈ Id
   ─→ (Id × pv11_p1_Ballot_Num() × ℤ × Cmd)
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Definition: pv11_p1_AcceptorState
pv11_p1_AcceptorState(Cmd;ldrs_uid;mf) ==
  state-class2(λloc.pv11_p1_init_acceptor(Cmd);pv11_p1_on_p1a(Cmd;ldrs_uid);pv11_p1_p1a'base(Cmd;mf);
               pv11_p1_on_p2a(Cmd;ldrs_uid);pv11_p1_p2a'base(Cmd;mf))

Lemma: pv11_p1_AcceptorState_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorState(Cmd;ldrs_uid;mf) ∈ EClass(pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Lemma: pv11_p1_AcceptorState-functional
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))].
  pv11_p1_AcceptorState(Cmd;ldrs_uid;mf) is functional

Definition: pv11_p1_AcceptorStateFun
pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e) ==  pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e)

Lemma: pv11_p1_AcceptorStateFun_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E].
  (pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e) ∈ pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

Lemma: pv11_p1_AcceptorState-classrel
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  ∀es:EO+(Message(mf)). ∀e:E. ∀v:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
    (v ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e) ⇐⇒ v = pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e))

Definition: pv11_p1_AcceptorState-program
pv11_p1_AcceptorState-program(Cmd;ldrs_uid;mf) ==
  state-class2-program(λloc.pv11_p1_init_acceptor(Cmd);pv11_p1_on_p1a(Cmd;ldrs_uid);pv11_p1_p1a'base-program(Cmd;mf);
                       pv11_p1_on_p2a(Cmd;ldrs_uid);pv11_p1_p2a'base-program(Cmd;mf))

Lemma: pv11_p1_AcceptorState-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorState-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)))

Lemma: pv11_p1_inv_acc
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀z:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  (z ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e1)
  ⇒ let ballot_num,accepted = z 
     in (∀bnum:pv11_p1_Ballot_Num(). ∀p:ℤ × Cmd.
           ((<bnum, p> ∈ accepted) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) bnum ballot_num))))
        ∧ l-ordered(pv11_p1_Ballot_Num() × ℤ × Cmd;pv1,pv2.↑(pv11_p1_leq_bnum(ldrs_uid) (fst(pv1)) (fst(pv2)));accepted)
        ∧ no_repeats(pv11_p1_Ballot_Num() × ℤ × Cmd;accepted))

Lemma: pv11_p1_inc_acc
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀zh,z:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zh ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e1)
  ⇒ z ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;mf)(e2)
  ⇒ let ballot_num1,accepted1 = zh 
     in let ballot_num2,accepted2 = z 
        in (↑(pv11_p1_leq_bnum(ldrs_uid) ballot_num1 ballot_num2)) ∧ accepted1 ≤ accepted2)

Definition: pv11_p1_AcceptorsP1a
pv11_p1_AcceptorsP1a(Cmd;ldrs_uid;mf) ==
  let f = λloc,zi,z. let ldr,b = zi in let bnum,pvals = z in {pv11_p1_p1b'send(Cmd;mf) ldr <loc, b, bnum, pvals>} in
      ((f o pv11_p1_p1a'base(Cmd;mf)) o pv11_p1_AcceptorState(Cmd;ldrs_uid;mf))

Lemma: pv11_p1_AcceptorsP1a_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorsP1a(Cmd;ldrs_uid;mf) ∈ EClass(Interface))

Definition: pv11_p1_AcceptorsP1a-program
pv11_p1_AcceptorsP1a-program(Cmd;ldrs_uid;mf) ==
  let f = λloc,zi,z. let ldr,b = zi in let bnum,pvals = z in {pv11_p1_p1b'send(Cmd;mf) ldr <loc, b, bnum, pvals>} in
      eclass1-program(f;pv11_p1_p1a'base-program(Cmd;mf)) o pv11_p1_AcceptorState-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_AcceptorsP1a-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorsP1a-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_AcceptorsP1a(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_AcceptorsP2a
pv11_p1_AcceptorsP2a(Cmd;ldrs_uid;mf) ==
  let f = λloc,zj,z. let ldr,zk = zj 
                     in let b,s,zl = zk in 
                        let bnum,z = z 
                        in {pv11_p1_p2b'send(Cmd;mf) ldr <loc, b, s, bnum>} in
      ((f o pv11_p1_p2a'base(Cmd;mf)) o pv11_p1_AcceptorState(Cmd;ldrs_uid;mf))

Lemma: pv11_p1_AcceptorsP2a_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorsP2a(Cmd;ldrs_uid;mf) ∈ EClass(Interface))

Definition: pv11_p1_AcceptorsP2a-program
pv11_p1_AcceptorsP2a-program(Cmd;ldrs_uid;mf) ==
  let f = λloc,zj,z. let ldr,zk = zj 
                     in let b,s,zl = zk in 
                        let bnum,z = z 
                        in {pv11_p1_p2b'send(Cmd;mf) ldr <loc, b, s, bnum>} in
      eclass1-program(f;pv11_p1_p2a'base-program(Cmd;mf)) o pv11_p1_AcceptorState-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_AcceptorsP2a-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_AcceptorsP2a-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_AcceptorsP2a(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_Acceptor
pv11_p1_Acceptor(Cmd;ldrs_uid;mf) ==  pv11_p1_AcceptorsP1a(Cmd;ldrs_uid;mf) || pv11_p1_AcceptorsP2a(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_Acceptor_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Acceptor(Cmd;ldrs_uid;mf) ∈ EClass(Interface))

Definition: pv11_p1_Acceptor-program
pv11_p1_Acceptor-program(Cmd;ldrs_uid;mf) ==
  pv11_p1_AcceptorsP1a-program(Cmd;ldrs_uid;mf) || pv11_p1_AcceptorsP2a-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_Acceptor-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Acceptor-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_Acceptor(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_CommanderNotify
pv11_p1_CommanderNotify(Cmd;accpts;mf) ==
  λbsp.return-loc-bag-class(λldr.(pv11_p1_p2a'broadcast(Cmd;mf) accpts <ldr, bsp>))

Lemma: pv11_p1_CommanderNotify_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderNotify(Cmd;accpts;mf) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ EClass(Interface))

Definition: pv11_p1_CommanderNotify-program
pv11_p1_CommanderNotify-program(Cmd;accpts;mf) ==
  λbsp.return-loc-bag-class-program(λldr.(pv11_p1_p2a'broadcast(Cmd;mf) accpts <ldr, bsp>))

Lemma: pv11_p1_CommanderNotify-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderNotify-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num() × ℤ × Cmd
                                                      LocalClass(pv11_p1_CommanderNotify(Cmd;accpts;mf) x))

Definition: pv11_p1_on_p2b
pv11_p1_on_p2b() ==
  λbnum,slt,loc,z,waitfor. let acloc,b,s,b' = z 
                           in if (pv11_p1_eq_bnums() bnum b) ∧b (slt =z s) ∧b (pv11_p1_eq_bnums() bnum b')
                              then waitfor - acloc
                              else waitfor
                              fi   

Lemma: pv11_p1_on_p2b_wf
pv11_p1_on_p2b() ∈ pv11_p1_Ballot_Num()
─→ ℤ
─→ Id
─→ (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
─→ bag(Id)
─→ bag(Id)

Definition: pv11_p1_CommanderState
pv11_p1_CommanderState(Cmd;accpts;mf) ==  λb,s. state-class1(λloc.accpts;pv11_p1_on_p2b() b s;pv11_p1_p2b'base(Cmd;mf))

Lemma: pv11_p1_CommanderState_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderState(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num() ─→ ℤ ─→ EClass(bag(Id)))

Lemma: pv11_p1_CommanderState-functional
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))].
∀[x:pv11_p1_Ballot_Num()]. ∀[zzs:ℤ].
  pv11_p1_CommanderState(Cmd;accpts;mf) x zzs is functional

Definition: pv11_p1_CommanderStateFun
pv11_p1_CommanderStateFun(Cmd;accpts;mf;x;zzs;es;e) ==  pv11_p1_CommanderState(Cmd;accpts;mf) x zzs(e)

Lemma: pv11_p1_CommanderStateFun_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E].
∀[x:pv11_p1_Ballot_Num()]. ∀[zzs:ℤ].
  (pv11_p1_CommanderStateFun(Cmd;accpts;mf;x;zzs;es;e) ∈ bag(Id))

Lemma: pv11_p1_CommanderState-classrel
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  ∀es:EO+(Message(mf)). ∀e:E. ∀x:pv11_p1_Ballot_Num(). ∀zzs:ℤ. ∀v:bag(Id).
    (v ∈ pv11_p1_CommanderState(Cmd;accpts;mf) x zzs(e) ⇐⇒ v = pv11_p1_CommanderStateFun(Cmd;accpts;mf;x;zzs;es;e))

Definition: pv11_p1_CommanderState-program
pv11_p1_CommanderState-program(Cmd;accpts;mf) ==
  λb,s. state-class1-program(λloc.accpts;pv11_p1_on_p2b() b s;pv11_p1_p2b'base-program(Cmd;mf))

Lemma: pv11_p1_CommanderState-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderState-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num(). ∀zzt:ℤ.
                                                     LocalClass(pv11_p1_CommanderState(Cmd;accpts;mf) x zzt))

Lemma: pv11_p1_inv_comm
∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀waitfor:bag(Id).
  (waitfor ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e1) ⇒ sub-bag(Id;waitfor;accpts))

Lemma: pv11_p1_ord_comm
∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀waitfor1,waitfor2:bag(Id).
  ((e1 <loc e2)
  ⇒ waitfor1 ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e1)
  ⇒ waitfor2 ∈ pv11_p1_CommanderState(Cmd;accpts;mf) b s(e2)
  ⇒ sub-bag(Id;waitfor2;waitfor1))

Definition: pv11_p1_commander_output
pv11_p1_commander_output(Cmd;accpts;reps;mf) ==
  λzm,ldr,z,waitfor. let bnum,slt,cmd = zm in 
                    let acloc,b,s,b' = z 
                    in if (pv11_p1_eq_bnums() bnum b) ∧b (slt =z s)
                       then if pv11_p1_eq_bnums() bnum b'
                            then if #(waitfor) <z pv11_p1_threshold(accpts)
                                 then pv11_p1_decision'broadcast(Cmd;mf) reps <slt, cmd>
                                 else {}
                                 fi 
                            else {pv11_p1_preempted'send(Cmd;mf) ldr b'}
                            fi 
                       else {}
                       fi   

Lemma: pv11_p1_commander_output_wf
∀[Cmd:ValueAllType]. ∀[accpts,reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_commander_output(Cmd;accpts;reps;mf) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd)
   ─→ Id
   ─→ (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
   ─→ bag(Id)
   ─→ bag(Interface))

Definition: pv11_p1_CommanderOutput
pv11_p1_CommanderOutput(Cmd;accpts;reps;mf) ==
  λz.let bnum,slt,cmd = z in 
     (((pv11_p1_commander_output(Cmd;accpts;reps;mf) <bnum, slt, cmd> o pv11_p1_p2b'base(Cmd;mf)) o pv11_p1_CommanderSta\000Cte(Cmd;accpts;mf) bnum slt) once)

Lemma: pv11_p1_CommanderOutput_wf
∀[Cmd:ValueAllType]. ∀[accpts,reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderOutput(Cmd;accpts;reps;mf) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ EClass(Interface))

Definition: pv11_p1_CommanderOutput-program
pv11_p1_CommanderOutput-program(Cmd;accpts;reps;mf) ==
  λz.let bnum,slt,cmd = z in 
     once-class-program(eclass1-program(pv11_p1_commander_output(Cmd;accpts;reps;mf) <bnum, slt, cmd>;pv11_p1_p2b'base-p\000Crogram(Cmd;mf))
                        o pv11_p1_CommanderState-program(Cmd;accpts;mf) bnum slt)

Lemma: pv11_p1_CommanderOutput-program_wf
∀[Cmd:ValueAllType]. ∀[accpts,reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_CommanderOutput-program(Cmd;accpts;reps;mf) ∈ ∀x:pv11_p1_Ballot_Num() × ℤ × Cmd
                                                           LocalClass(pv11_p1_CommanderOutput(Cmd;accpts;reps;mf) x))

Definition: pv11_p1_Commander
pv11_p1_Commander(Cmd;accpts;reps;mf) ==
  λbp.pv11_p1_CommanderNotify(Cmd;accpts;mf) bp || pv11_p1_CommanderOutput(Cmd;accpts;reps;mf) bp

Lemma: pv11_p1_Commander_wf
∀[Cmd:ValueAllType]. ∀[accpts,reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Commander(Cmd;accpts;reps;mf) ∈ (pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ EClass(Interface))

Definition: pv11_p1_Commander-program
pv11_p1_Commander-program(Cmd;accpts;reps;mf) ==
  λbp.pv11_p1_CommanderNotify-program(Cmd;accpts;mf) bp || pv11_p1_CommanderOutput-program(Cmd;accpts;reps;mf) bp

Lemma: pv11_p1_Commander-program_wf
∀[Cmd:ValueAllType]. ∀[accpts,reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Commander-program(Cmd;accpts;reps;mf) ∈ ∀x:pv11_p1_Ballot_Num() × ℤ × Cmd
                                                     LocalClass(pv11_p1_Commander(Cmd;accpts;reps;mf) x))

Definition: pv11_p1_ScoutNotify
pv11_p1_ScoutNotify(Cmd;accpts;mf) ==  λb.return-loc-bag-class(λldr.(pv11_p1_p1a'broadcast(Cmd;mf) accpts <ldr, b>))

Lemma: pv11_p1_ScoutNotify_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutNotify(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num() ─→ EClass(Interface))

Definition: pv11_p1_ScoutNotify-program
pv11_p1_ScoutNotify-program(Cmd;accpts;mf) ==
  λb.return-loc-bag-class-program(λldr.(pv11_p1_p1a'broadcast(Cmd;mf) accpts <ldr, b>))

Lemma: pv11_p1_ScoutNotify-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutNotify-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num()
                                                  LocalClass(pv11_p1_ScoutNotify(Cmd;accpts;mf) x))

Definition: pv11_p1_on_p1b
pv11_p1_on_p1b(Cmd) ==
  λbnum,loc,zn,z. let acloc,b,b',pvals = zn 
                  in let waitfor,pvalues = z 
                     in if (pv11_p1_eq_bnums() bnum b) ∧b (pv11_p1_eq_bnums() bnum b')
                        then let waitfor' = waitfor - acloc in
                              let pvalues' = pv11_p1_append_news(Cmd) pv11_p1_same_pvalue(Cmd) pvalues pvals in
                              <waitfor', pvalues'>
                        else <waitfor, pvalues>
                        fi   

Lemma: pv11_p1_on_p1b_wf
∀[Cmd:ValueAllType]
  (pv11_p1_on_p1b(Cmd) ∈ pv11_p1_Ballot_Num()
   ─→ Id
   ─→ (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Definition: pv11_p1_ScoutState
pv11_p1_ScoutState(Cmd;accpts;mf) ==
  λb.state-class1(λloc.pv11_p1_init_scout(Cmd;accpts);pv11_p1_on_p1b(Cmd) b;pv11_p1_p1b'base(Cmd;mf))

Lemma: pv11_p1_ScoutState_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutState(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num()
   ─→ EClass(bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))

Lemma: pv11_p1_ScoutState-functional
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))].
∀[x:pv11_p1_Ballot_Num()].
  pv11_p1_ScoutState(Cmd;accpts;mf) x is functional

Definition: pv11_p1_ScoutStateFun
pv11_p1_ScoutStateFun(Cmd;accpts;mf;x;es;e) ==  pv11_p1_ScoutState(Cmd;accpts;mf) x(e)

Lemma: pv11_p1_ScoutStateFun_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E].
∀[x:pv11_p1_Ballot_Num()].
  (pv11_p1_ScoutStateFun(Cmd;accpts;mf;x;es;e) ∈ bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))

Lemma: pv11_p1_ScoutState-classrel
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  ∀es:EO+(Message(mf)). ∀e:E. ∀x:pv11_p1_Ballot_Num(). ∀v:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
    (v ∈ pv11_p1_ScoutState(Cmd;accpts;mf) x(e) ⇐⇒ v = pv11_p1_ScoutStateFun(Cmd;accpts;mf;x;es;e))

Definition: pv11_p1_ScoutState-program
pv11_p1_ScoutState-program(Cmd;accpts;mf) ==
  λb.state-class1-program(λloc.pv11_p1_init_scout(Cmd;accpts);pv11_p1_on_p1b(Cmd) b;pv11_p1_p1b'base-program(Cmd;mf))

Lemma: pv11_p1_ScoutState-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutState-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num(). LocalClass(pv11_p1_ScoutState(Cmd;accpts;mf) x))

Lemma: pv11_p1_inv_scout
∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1:E.
∀b:pv11_p1_Ballot_Num(). ∀z:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  (z ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e1) ⇒ let waitfor,pvalues = z in sub-bag(Id;waitfor;accpts))

Lemma: pv11_p1_ord_scout
∀Cmd:ValueAllType. ∀accpts:bag(Id). ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀b:pv11_p1_Ballot_Num(). ∀zo,z:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zo ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e1)
  ⇒ z ∈ pv11_p1_ScoutState(Cmd;accpts;mf) b(e2)
  ⇒ let waitfor1,pvalues1 = zo 
     in let waitfor2,pvalues2 = z 
        in sub-bag(Id;waitfor2;waitfor1) ∧ pvalues1 ⊆ pvalues2)

Definition: pv11_p1_scout_output
pv11_p1_scout_output(Cmd;accpts;mf) ==
  λbnum,ldr,zp,z. let a,b,b',pvals = zp 
                  in let waitfor,pvalues = z 
                     in if pv11_p1_eq_bnums() bnum b
                        then if pv11_p1_eq_bnums() bnum b'
                             then if #(waitfor) <z pv11_p1_threshold(accpts)
                                  then {pv11_p1_adopted'send(Cmd;mf) ldr <bnum, pvalues>}
                                  else {}
                                  fi 
                             else {pv11_p1_preempted'send(Cmd;mf) ldr b'}
                             fi 
                        else {}
                        fi   

Lemma: pv11_p1_scout_output_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_scout_output(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num()
   ─→ Id
   ─→ (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ bag(Interface))

Definition: pv11_p1_ScoutOutput
pv11_p1_ScoutOutput(Cmd;accpts;mf) ==
  λb.(((pv11_p1_scout_output(Cmd;accpts;mf) b o pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) b) once)

Lemma: pv11_p1_ScoutOutput_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutOutput(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num() ─→ EClass(Interface))

Definition: pv11_p1_ScoutOutput-program
pv11_p1_ScoutOutput-program(Cmd;accpts;mf) ==
  λb.once-class-program(eclass1-program(pv11_p1_scout_output(Cmd;accpts;mf) b;pv11_p1_p1b'base-program(Cmd;mf))
                        o pv11_p1_ScoutState-program(Cmd;accpts;mf) b)

Lemma: pv11_p1_ScoutOutput-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_ScoutOutput-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num()
                                                  LocalClass(pv11_p1_ScoutOutput(Cmd;accpts;mf) x))

Definition: pv11_p1_Scout
pv11_p1_Scout(Cmd;accpts;mf) ==  λb.pv11_p1_ScoutNotify(Cmd;accpts;mf) b || pv11_p1_ScoutOutput(Cmd;accpts;mf) b

Lemma: pv11_p1_Scout_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Scout(Cmd;accpts;mf) ∈ pv11_p1_Ballot_Num() ─→ EClass(Interface))

Definition: pv11_p1_Scout-program
pv11_p1_Scout-program(Cmd;accpts;mf) ==
  λb.pv11_p1_ScoutNotify-program(Cmd;accpts;mf) b || pv11_p1_ScoutOutput-program(Cmd;accpts;mf) b

Lemma: pv11_p1_Scout-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Scout-program(Cmd;accpts;mf) ∈ ∀x:pv11_p1_Ballot_Num(). LocalClass(pv11_p1_Scout(Cmd;accpts;mf) x))

Definition: pv11_p1_on_propose
pv11_p1_on_propose(Cmd) ==
  λloc,zq,z. let s,p = zq 
             in let ballot_num,active,proposals = z in 
                let proposals' = if pv11_p1_in_domain(Cmd) s proposals
                                 then proposals
                                 else pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) <s, p> proposals
                                 fi  in
                    <ballot_num, active, proposals'>

Lemma: pv11_p1_on_propose_wf
∀[Cmd:ValueAllType]
  (pv11_p1_on_propose(Cmd) ∈ Id
   ─→ (ℤ × Cmd)
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))

Definition: pv11_p1_when_adopted
pv11_p1_when_adopted(Cmd;ldrs_uid) ==
  λloc,zr,z. let bnum,pvals = zr 
             in let ballot_num,active,proposals = z in 
                if pv11_p1_eq_bnums() bnum ballot_num
                then let proposals' = pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals) in
                         <ballot_num, tt, proposals'>
                else <ballot_num, active, proposals>
                fi 

Lemma: pv11_p1_when_adopted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_when_adopted(Cmd;ldrs_uid) ∈ Id
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))

Definition: pv11_p1_when_preempted
pv11_p1_when_preempted(Cmd;ldrs_uid) ==
  λldr,bnum,z. let ballot_num,active,proposals = z in 
              if (pv11_p1_is_bnum() bnum) ∧b (ballot_num  < bnum)
              then <pv11_p1_upd_bnum() bnum ldr, ff, proposals>
              else <ballot_num, active, proposals>
              fi 

Lemma: pv11_p1_when_preempted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_when_preempted(Cmd;ldrs_uid) ∈ Id
   ─→ pv11_p1_Ballot_Num()
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))

Definition: pv11_p1_LeaderState
pv11_p1_LeaderState(Cmd;ldrs_uid;mf) ==
  memory-class3(pv11_p1_init_leader(Cmd);pv11_p1_on_propose(Cmd);pv11_p1_propose'base(Cmd;mf);
                pv11_p1_when_adopted(Cmd;ldrs_uid);pv11_p1_adopted'base(Cmd;mf);pv11_p1_when_preempted(Cmd;ldrs_uid)
                ;pv11_p1_preempted'base(Cmd;mf))

Lemma: pv11_p1_LeaderState_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderState(Cmd;ldrs_uid;mf) ∈ EClass(pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))

Lemma: pv11_p1_LeaderState-functional
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))].
  pv11_p1_LeaderState(Cmd;ldrs_uid;mf) is functional

Definition: pv11_p1_LeaderStateFun
pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e) ==  pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e)

Lemma: pv11_p1_LeaderStateFun_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E].
  (pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e) ∈ pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))

Lemma: pv11_p1_LeaderState-classrel
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  ∀es:EO+(Message(mf)). ∀e:E. ∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
    (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e) ⇐⇒ v = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e))

Definition: pv11_p1_LeaderState-program
pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf) ==
  memory-class3-program(pv11_p1_init_leader(Cmd);pv11_p1_on_propose(Cmd);pv11_p1_propose'base-program(Cmd;mf);
                        pv11_p1_when_adopted(Cmd;ldrs_uid);pv11_p1_adopted'base-program(Cmd;mf);
                        pv11_p1_when_preempted(Cmd;ldrs_uid);pv11_p1_preempted'base-program(Cmd;mf))

Lemma: pv11_p1_LeaderState-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_LeaderState(Cmd;ldrs_uid;mf)))

Lemma: pv11_p1_ldr_ord
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀mf:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(mf)). ∀e1,e2:E.
∀zs,z:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  ((e1 <loc e2)
  ⇒ zs ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e1)
  ⇒ z ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;mf)(e2)
  ⇒ let bnum1,active1,proposals1 = zs in 
     let bnum2,active2,proposals2 = z in 
     ↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2))

Definition: pv11_p1_leader_propose
pv11_p1_leader_propose(Cmd) ==
  λloc,zt,z. let slt,p = zt 
             in let ballot_num,active,proposals = z in 
                if active ∧b (¬b(pv11_p1_in_domain(Cmd) slt proposals)) then {<ballot_num, slt, p>} else {} fi 

Lemma: pv11_p1_leader_propose_wf
∀[Cmd:ValueAllType]
  (pv11_p1_leader_propose(Cmd) ∈ Id
   ─→ (ℤ × Cmd)
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ bag(pv11_p1_Ballot_Num() × ℤ × Cmd))

Definition: pv11_p1_LeaderPropose
pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf) ==
  ((pv11_p1_leader_propose(Cmd) o pv11_p1_propose'base(Cmd;mf)) o pv11_p1_LeaderState(Cmd;ldrs_uid;mf))

Lemma: pv11_p1_LeaderPropose_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf) ∈ EClass(pv11_p1_Ballot_Num() × ℤ × Cmd))

Definition: pv11_p1_LeaderPropose-program
pv11_p1_LeaderPropose-program(Cmd;ldrs_uid;mf) ==
  eclass1-program(pv11_p1_leader_propose(Cmd);pv11_p1_propose'base-program(Cmd;mf))
  o pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_LeaderPropose-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderPropose-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_leader_adopted
pv11_p1_leader_adopted(Cmd;ldrs_uid) ==
  λloc,zu,z. let bnum,pvals = zu 
             in let ballot_num,active,proposals = z in 
                if pv11_p1_eq_bnums() bnum ballot_num
                then map(λsp.<bnum, sp>;pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals))
                else {}
                fi 

Lemma: pv11_p1_leader_adopted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_leader_adopted(Cmd;ldrs_uid) ∈ Id
   ─→ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ bag(pv11_p1_Ballot_Num() × ℤ × Cmd))

Definition: pv11_p1_LeaderAdopted
pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf) ==
  ((pv11_p1_leader_adopted(Cmd;ldrs_uid) o pv11_p1_adopted'base(Cmd;mf)) o pv11_p1_LeaderState(Cmd;ldrs_uid;mf))

Lemma: pv11_p1_LeaderAdopted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf) ∈ EClass(pv11_p1_Ballot_Num() × ℤ × Cmd))

Definition: pv11_p1_LeaderAdopted-program
pv11_p1_LeaderAdopted-program(Cmd;ldrs_uid;mf) ==
  eclass1-program(pv11_p1_leader_adopted(Cmd;ldrs_uid);pv11_p1_adopted'base-program(Cmd;mf))
  o pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_LeaderAdopted-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderAdopted-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_leader_preempted
pv11_p1_leader_preempted(Cmd;ldrs_uid) ==
  λldr,bnum,z. let ballot_num,zv,z = z in 
              if (pv11_p1_is_bnum() bnum) ∧b (ballot_num  < bnum) then {pv11_p1_upd_bnum() bnum ldr} else {} fi 

Lemma: pv11_p1_leader_preempted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_leader_preempted(Cmd;ldrs_uid) ∈ Id
   ─→ pv11_p1_Ballot_Num()
   ─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
   ─→ bag(pv11_p1_Ballot_Num()))

Definition: pv11_p1_LeaderPreempted
pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf) ==
  ((pv11_p1_leader_preempted(Cmd;ldrs_uid) o pv11_p1_preempted'base(Cmd;mf)) o pv11_p1_LeaderState(Cmd;ldrs_uid;mf))

Lemma: pv11_p1_LeaderPreempted_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf) ∈ EClass(pv11_p1_Ballot_Num()))

Definition: pv11_p1_LeaderPreempted-program
pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf) ==
  eclass1-program(pv11_p1_leader_preempted(Cmd;ldrs_uid);pv11_p1_preempted'base-program(Cmd;mf))
  o pv11_p1_LeaderState-program(Cmd;ldrs_uid;mf)

Lemma: pv11_p1_LeaderPreempted-program_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf) ∈ LocalClass(pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf)))

Definition: pv11_p1_SpawnFirstScout
pv11_p1_SpawnFirstScout(Cmd;accpts;mf) ==  on-loc-class(λldr.(pv11_p1_Scout(Cmd;accpts;mf) (pv11_p1_mk_bnum() 0 ldr)))

Lemma: pv11_p1_SpawnFirstScout_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_SpawnFirstScout(Cmd;accpts;mf) ∈ EClass(Interface))

Definition: pv11_p1_SpawnFirstScout-program
pv11_p1_SpawnFirstScout-program(Cmd;accpts;mf) ==
  on-loc-class-program(λldr.(pv11_p1_Scout-program(Cmd;accpts;mf) (pv11_p1_mk_bnum() 0 ldr)))

Lemma: pv11_p1_SpawnFirstScout-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_SpawnFirstScout-program(Cmd;accpts;mf) ∈ LocalClass(pv11_p1_SpawnFirstScout(Cmd;accpts;mf)))

Definition: pv11_p1_Leader
pv11_p1_Leader(Cmd;accpts;ldrs_uid;reps;mf) ==
  pv11_p1_SpawnFirstScout(Cmd;accpts;mf) || pv11_p1_LeaderPropose(Cmd;ldrs_uid;mf)
                                            || pv11_p1_LeaderAdopted(Cmd;ldrs_uid;mf)
                                             >z> pv11_p1_Commander(Cmd;accpts;reps;mf) z
  || pv11_p1_LeaderPreempted(Cmd;ldrs_uid;mf) >z> pv11_p1_Scout(Cmd;accpts;mf) z

Lemma: pv11_p1_Leader_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Leader(Cmd;accpts;ldrs_uid;reps;mf) ∈ EClass(Interface))

Definition: pv11_p1_Leader-program
pv11_p1_Leader-program(Cmd;accpts;ldrs_uid;reps;mf) ==
  pv11_p1_SpawnFirstScout-program(Cmd;accpts;mf) || pv11_p1_LeaderPropose-program(Cmd;ldrs_uid;mf)
                                                    || pv11_p1_LeaderAdopted-program(Cmd;ldrs_uid;mf)
                                                     >>= λz.(pv11_p1_Commander-program(Cmd;accpts;reps;mf) z)
  || pv11_p1_LeaderPreempted-program(Cmd;ldrs_uid;mf) >>= λz.(pv11_p1_Scout-program(Cmd;accpts;mf) z)

Lemma: pv11_p1_Leader-program_wf
∀[Cmd:ValueAllType]. ∀[accpts:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_Leader-program(Cmd;accpts;ldrs_uid;reps;mf) ∈ LocalClass(pv11_p1_Leader(Cmd;accpts;ldrs_uid;reps;mf)))

Definition: pv11_p1_main
pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf) ==
  pv11_p1_Leader(Cmd;accpts;ldrs_uid;reps;mf)@ldrs || pv11_p1_Acceptor(Cmd;ldrs_uid;mf)@accpts

Lemma: pv11_p1_main_wf
∀[Cmd:ValueAllType]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf) ∈ EClass(Interface))

Definition: pv11_p1_main-program
pv11_p1_main-program(Cmd;accpts;ldrs;ldrs_uid;reps;mf) ==
  (pv11_p1_Leader-program(Cmd;accpts;ldrs_uid;reps;mf))@ldrs || (pv11_p1_Acceptor-program(Cmd;ldrs_uid;mf))@accpts

Lemma: pv11_p1_main-program_wf
∀[Cmd:ValueAllType]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_main-program(Cmd;accpts;ldrs;ldrs_uid;reps;mf) ∈ LocalClass(pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)))

Comment: ------ pv11_p1 - extra ------
⋅

Definition: pv11_p1_headers_internal
pv11_p1_headers_internal() ==
  [``pv11_p1 p1a``; ``pv11_p1 p1b``; ``pv11_p1 p2a``; ``pv11_p1 p2b``; ``pv11_p1 preempted``; ``pv11_p1 adopted``]

Lemma: pv11_p1_headers_internal_wf
pv11_p1_headers_internal() ∈ Name List

Definition: pv11_p1_headers_no_inputs
pv11_p1_headers_no_inputs() ==
  [``pv11_p1 p1a``;
   ``pv11_p1 p1b``;
   ``pv11_p1 p2a``;
   ``pv11_p1 p2b``;
   ``pv11_p1 preempted``;
   ``pv11_p1 adopted``;
   [decision]]

Lemma: pv11_p1_headers_no_inputs_wf
pv11_p1_headers_no_inputs() ∈ Name List

Definition: pv11_p1_headers_no_inputs_types
pv11_p1_headers_no_inputs_types(Cmd) ==
  [<``pv11_p1 p1a``, Id × pv11_p1_Ballot_Num()>;
   <``pv11_p1 p1b``, Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)>;
   <``pv11_p1 p2a``, Id × pv11_p1_Ballot_Num() × ℤ × Cmd>;
   <``pv11_p1 p2b``, Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()>;
   <``pv11_p1 preempted``, pv11_p1_Ballot_Num()>;
   <``pv11_p1 adopted``, pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)>;
   <[decision], ℤ × Cmd>]

Lemma: pv11_p1_headers_no_inputs_types_wf
∀[Cmd:ValueAllType]. (pv11_p1_headers_no_inputs_types(Cmd) ∈ (Name × Type) List)

Definition: pv11_p1_message-constraint
pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; mf; es) ==
  eo-msg-interface-constraint(es;pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf);pv11_p1_headers_no_inputs();mf)

Lemma: pv11_p1_message-constraint_wf
∀[Cmd:ValueAllType]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
∀[es:EO+(Message(mf))].
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; mf; es) ∈ ℙ)

Definition: pv11_p1_messages-delivered
pv11_p1_messages-delivered{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; mf; es) ==
  eo-msgs-interface-delivered(es;pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf);mf)

Lemma: pv11_p1_messages-delivered_wf
∀[Cmd:ValueAllType]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
∀[es:EO+(Message(mf))].
  (pv11_p1_messages-delivered{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; mf; es) ∈ ℙ)

Lemma: pv11_p1-ilf
(∀[loc:Id]. ∀[accpts:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[mf:pv11_p1_headers_type{i:l}(Cmd)].
 ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(mf)].
   {<d, i, m> ∈ ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc) o pv11_p1_p1b'base(Cmd;mf)) o
                pv11_p1_ScoutState(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc))(e)
   ⇐⇒ ((header(e) = ``pv11_p1 p1b``)
       ∧ has-es-info-type(es;e;mf;Id
         × pv11_p1_Ballot_Num()
         × pv11_p1_Ballot_Num()
         × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
       ∧ ((pv11_p1_init_ballot_num() loc) = (fst(snd(msgval(e)))))
       ∧ (d = 0)
       ∧ (i = loc(e))
       ∧ (↓(((pv11_p1_init_ballot_num() loc) = (fst(snd(snd(msgval(e))))))
           ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() loc;es;e))) < pv11_p1_threshold(accpts)
           ∧ (m
             = make-Msg(``pv11_p1 adopted``;<pv11_p1_init_ballot_num() loc
                                            , snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() 
                                                                                      loc;es;e))
                                            >)))
           ∨ ((¬((pv11_p1_init_ballot_num() loc) = (fst(snd(snd(msgval(e)))))))
             ∧ (m = make-Msg(``pv11_p1 preempted``;fst(snd(snd(msgval(e))))))))})
∧ (∀[z3:ℤ]. ∀[z1:pv11_p1_Ballot_Num()]. ∀[reps,accpts:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[z4:Cmd].
   ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(mf)].
     {<d, i, m> ∈ ((pv11_p1_commander_output(Cmd;accpts;reps;mf) <z1, z3, z4> o pv11_p1_p2b'base(Cmd;mf)) o pv11_p1_Comm\000CanderState(Cmd;accpts;mf) z1 z3)(e)
     ⇐⇒ ((header(e) = ``pv11_p1 p2b``)
         ∧ has-es-info-type(es;e;mf;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()))
         ∧ ((z1 = (fst(snd(msgval(e))))) ∧ (z3 = (fst(snd(snd(msgval(e)))))))
         ∧ (d = 0)
         ∧ (↓((z1 = (snd(snd(snd(msgval(e))))))
             ∧ #(pv11_p1_CommanderStateFun(Cmd;accpts;mf;z1;z3;es;e)) < pv11_p1_threshold(accpts)
             ∧ i ↓∈ reps
             ∧ (m = make-Msg([decision];<z3, z4>)))
             ∨ ((¬(z1 = (snd(snd(snd(msgval(e)))))))
               ∧ (i = loc(e))
               ∧ (m = make-Msg(``pv11_p1 preempted``;snd(snd(snd(msgval(e))))))))})
∧ (∀[loc:Id]. ∀[param:pv11_p1_Ballot_Num()]. ∀[accpts:bag(Id)]. ∀[Cmd:{T:Type| valueall-type(T)} ].
   ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(mf)].
     {<d, i, m> ∈ ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_upd_bnum() param loc) o pv11_p1_p1b'base(Cmd;mf)) o
                  pv11_p1_ScoutState(Cmd;accpts;mf) (pv11_p1_upd_bnum() param loc))(e)
     ⇐⇒ ((header(e) = ``pv11_p1 p1b``)
         ∧ has-es-info-type(es;e;mf;Id
           × pv11_p1_Ballot_Num()
           × pv11_p1_Ballot_Num()
           × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
         ∧ ((pv11_p1_upd_bnum() param loc) = (fst(snd(msgval(e)))))
         ∧ (d = 0)
         ∧ (i = loc(e))
         ∧ (↓(((pv11_p1_upd_bnum() param loc) = (fst(snd(snd(msgval(e))))))
             ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() param 
                                                         loc;es;e))) < pv11_p1_threshold(accpts)
             ∧ (m
               = make-Msg(``pv11_p1 adopted``;<pv11_p1_upd_bnum() param loc
                                              , snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() param 
                                                                                        loc;es;e))
                                              >)))
             ∨ ((¬((pv11_p1_upd_bnum() param loc) = (fst(snd(snd(msgval(e)))))))
               ∧ (m = make-Msg(``pv11_p1 preempted``;fst(snd(snd(msgval(e))))))))})
∧ (∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
   ∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[m:Message(mf)].
     {<d, i, m> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
     ⇐⇒ ↓(loc(e) ↓∈ ldrs
          ∧ ((((((d = 0) ∧ (m = make-Msg(``pv11_p1 p1a``;<loc(e), pv11_p1_init_ballot_num() loc(e)>)) ∧ i ↓∈ accpts) ∧ (\000C↑first(e)))
            ∨ ((no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e)) o
                    pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) 
                                                (pv11_p1_init_ballot_num() loc(e))) prior to e)
              ∧ <d, i, m> ∈ {((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e)) o
                              pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) 
                                                          (pv11_p1_init_ballot_num() loc(e)))}(e)))
            ∨ (∃e':{e':E| e' ≤loc e } 
                ∃z1:pv11_p1_Ballot_Num()
                 ∃z3:ℤ
                  ∃z4:Cmd
                   (((((header(e') = [propose]) ∧ has-es-info-type(es;e';mf;ℤ × Cmd))
                   ∧ ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))
                     ∧ (¬↑(pv11_p1_in_domain(Cmd) (fst(msgval(e'))) 
                           (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))))
                   ∧ (z1 = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
                   ∧ (<z3, z4> = msgval(e')))
                   ∨ (((header(e') = ``pv11_p1 adopted``)
                      ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
                     ∧ ((fst(msgval(e'))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
                     ∧ ((<z3, z4> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))
                       ∧ (¬(∃p2:Cmd. (<z3, p2> ∈ pv11_p1_pmax(Cmd;ldrs_uid) (snd(msgval(e')))))))
                       ∨ (∃v2:pv11_p1_Ballot_Num()
                           (<v2, z3, z4> ↓∈ snd(msgval(e'))
                           ∧ (¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2 ... ...)) ∧ ...))))))
                     ∧ ...))
                   ∧ ...)))
            ∨ ...))
          ∨ ...})

Lemma: pv11_p1-p1a
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[i1:Id].
∀[p:pv11_p1_Ballot_Num()].
  (<d, i, mk-msg(auth;``pv11_p1 p1a``;<i1, p>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ i ↓∈ accpts
      ∧ (d = 0)
      ∧ auth = pv11_p1_init_active()
      ∧ (i1 = loc(e))
      ∧ (↓((p = (pv11_p1_init_ballot_num() loc(e))) ∧ (↑first(e)))
          ∨ ((header(e) = ``pv11_p1 preempted``)
            ∧ has-es-info-type(es;e;mf;pv11_p1_Ballot_Num())
            ∧ (↑(pv11_p1_is_bnum() msgval(e)))
            ∧ (↑(fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e))  < msgval(e)))
            ∧ (p = (pv11_p1_upd_bnum() msgval(e) loc(e))))))

Lemma: pv11_p1-p1b
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[i1:Id].
∀[p,p1:pv11_p1_Ballot_Num()]. ∀[L:(pv11_p1_Ballot_Num() × ℤ × Cmd) List].
  (<d, i, mk-msg(auth;``pv11_p1 p1b``;<i1, p, p1, L>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ accpts
      ∧ ((header(e) = ``pv11_p1 p1a``) ∧ has-es-info-type(es;e;mf;Id × pv11_p1_Ballot_Num()))
      ∧ (d = 0)
      ∧ (i = (fst(msgval(e))))
      ∧ auth = pv11_p1_init_active()
      ∧ (i1 = loc(e))
      ∧ (p = (snd(msgval(e))))
      ∧ (<p1, L> = pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e)))

Lemma: pv11_p1-p2a
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[i1:Id].
∀[p:pv11_p1_Ballot_Num()]. ∀[k:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;``pv11_p1 p2a``;<i1, p, k, v>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ i ↓∈ accpts
      ∧ (d = 0)
      ∧ auth = pv11_p1_init_active()
      ∧ (i1 = loc(e))
      ∧ (↓(((header(e) = [propose]) ∧ has-es-info-type(es;e;mf;ℤ × Cmd))
          ∧ ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e)))))
            ∧ (¬↑(pv11_p1_in_domain(Cmd) (fst(msgval(e))) (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e)))))))
          ∧ (p = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e))))
          ∧ (<k, v> = msgval(e)))
          ∨ (((header(e) = ``pv11_p1 adopted``)
             ∧ has-es-info-type(es;e;mf;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
            ∧ ((fst(msgval(e))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e))))
            ∧ ((<k, v> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e)))
              ∧ (¬(∃p2:Cmd. (<k, p2> ∈ pv11_p1_pmax(Cmd;ldrs_uid) (snd(msgval(e)))))))
              ∨ (∃v2:pv11_p1_Ballot_Num()
                  (<v2, k, v> ↓∈ snd(msgval(e))
                  ∧ (¬(∃z5:pv11_p1_Ballot_Num(). ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, k, z8> ∈ snd(msgval(e)))))))))
            ∧ (p = (fst(msgval(e)))))))

Lemma: pv11_p1-p2b
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[i1:Id].
∀[p:pv11_p1_Ballot_Num()]. ∀[k:ℤ]. ∀[p1:pv11_p1_Ballot_Num()].
  (<d, i, mk-msg(auth;``pv11_p1 p2b``;<i1, p, k, p1>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ accpts
      ∧ ((header(e) = ``pv11_p1 p2a``) ∧ has-es-info-type(es;e;mf;Id × pv11_p1_Ballot_Num() × ℤ × Cmd))
      ∧ (d = 0)
      ∧ (i = (fst(msgval(e))))
      ∧ auth = pv11_p1_init_active()
      ∧ (i1 = loc(e))
      ∧ (p = (fst(snd(msgval(e)))))
      ∧ (k = (fst(snd(snd(msgval(e))))))
      ∧ (p1 = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;mf;es;e)))))

Lemma: pv11_p1-preempted
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[p:pv11_p1_Ballot_Num()].
  (<d, i, mk-msg(auth;``pv11_p1 preempted``;p)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ (↓(((no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e)) o pv11_p1_p1b'base(Cmd;mf)) o
                pv11_p1_ScoutState(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e))) prior to e)
          ∧ ((header(e) = ``pv11_p1 p1b``)
            ∧ has-es-info-type(es;e;mf;Id
              × pv11_p1_Ballot_Num()
              × pv11_p1_Ballot_Num()
              × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
          ∧ ((pv11_p1_init_ballot_num() loc(e)) = (fst(snd(msgval(e)))))
          ∧ (d = 0)
          ∧ (i = loc(e))
          ∧ (¬((pv11_p1_init_ballot_num() loc(e)) = (fst(snd(snd(msgval(e)))))))
          ∧ auth = pv11_p1_init_active()
          ∧ (p = (fst(snd(snd(msgval(e)))))))
          ∨ (∃z4:Cmd
              ∃e':{e':E| e' ≤loc e } 
               ((header(e) = ``pv11_p1 p2b``)
               ∧ has-es-info-type(es;e;mf;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
               ∧ (d = 0)
               ∧ (¬((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e)))))))
               ∧ (i = loc(e))
               ∧ auth = pv11_p1_init_active()
               ∧ (p = (snd(snd(snd(msgval(e))))))
               ∧ ((((header(e') = [propose]) ∧ has-es-info-type(es;e';mf;ℤ × Cmd))
                 ∧ ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))
                   ∧ (¬↑(pv11_p1_in_domain(Cmd) (fst(msgval(e'))) 
                         (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))))
                 ∧ ((fst(snd(msgval(e)))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
                 ∧ (<fst(snd(snd(msgval(e)))), z4> = msgval(e')))
                 ∨ (((header(e') = ``pv11_p1 adopted``)
                    ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
                   ∧ ((fst(msgval(e'))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
                   ∧ ((<fst(snd(snd(msgval(e)))), z4> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))
                     ∧ (¬(∃p2:Cmd. (<fst(snd(snd(msgval(e)))), p2> ∈ pv11_p1_pmax(Cmd;ldrs_uid) (snd(msgval(e')))))))
                     ∨ (∃v2:pv11_p1_Ballot_Num()
                         (<v2, fst(snd(snd(msgval(e)))), z4> ↓∈ snd(msgval(e'))
                         ∧ (¬(∃z5:pv11_p1_Ballot_Num()
                               ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, fst(snd(snd(msgval(e)))), z8> ∈ snd(msgval(e')))))))))
                   ∧ ((fst(snd(msgval(e)))) = (fst(msgval(e'))))))
               ∧ (no ((pv11_p1_commander_output(Cmd;accpts;reps;mf) <fst(snd(msgval(e))), fst(snd(snd(msgval(e)))), z4> \000Co pv11_p1_p2b'base(Cmd;mf)) o
                     pv11_p1_CommanderState(Cmd;accpts;mf) (fst(snd(msgval(e)))) (fst(snd(snd(msgval(e)))))) between e'
                  and e))))
          ∨ (∃e':{e':E| e' ≤loc e } 
              ((((header(e') = ``pv11_p1 preempted``) ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num()))
               ∧ (↑(pv11_p1_is_bnum() msgval(e')))
               ∧ (↑(fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))  < msgval(e'))))
              ∧ (no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_upd_bnum() msgval(e') loc(e')) o
                     pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) 
                                                 (pv11_p1_upd_bnum() msgval(e') loc(e'))) between e' and e)
              ∧ ((header(e) = ``pv11_p1 p1b``)
                ∧ has-es-info-type(es;e;mf;Id
                  × pv11_p1_Ballot_Num()
                  × pv11_p1_Ballot_Num()
                  × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
              ∧ ((pv11_p1_upd_bnum() msgval(e') loc(e')) = (fst(snd(msgval(e)))))
              ∧ (d = 0)
              ∧ (i = loc(e))
              ∧ (¬((pv11_p1_upd_bnum() msgval(e') loc(e')) = (fst(snd(snd(msgval(e)))))))
              ∧ auth = pv11_p1_init_active()
              ∧ (p = (fst(snd(snd(msgval(e))))))))))

Lemma: pv11_p1-adopted
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹].
∀[p:pv11_p1_Ballot_Num()]. ∀[L:(pv11_p1_Ballot_Num() × ℤ × Cmd) List].
  (<d, i, mk-msg(auth;``pv11_p1 adopted``;<p, L>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ (↓((no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e)) o pv11_p1_p1b'base(Cmd;mf)) o
               pv11_p1_ScoutState(Cmd;accpts;mf) (pv11_p1_init_ballot_num() loc(e))) prior to e)
          ∧ ((header(e) = ``pv11_p1 p1b``)
            ∧ has-es-info-type(es;e;mf;Id
              × pv11_p1_Ballot_Num()
              × pv11_p1_Ballot_Num()
              × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
          ∧ ((pv11_p1_init_ballot_num() loc(e)) = (fst(snd(msgval(e)))))
          ∧ (d = 0)
          ∧ (i = loc(e))
          ∧ ((pv11_p1_init_ballot_num() loc(e)) = (fst(snd(snd(msgval(e))))))
          ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() 
                                                      loc(e);es;e))) < pv11_p1_threshold(accpts)
          ∧ auth = pv11_p1_init_active()
          ∧ (p = (pv11_p1_init_ballot_num() loc(e)))
          ∧ (L = (snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_init_ballot_num() loc(e);es;e)))))
          ∨ (∃e':{e':E| e' ≤loc e } 
              ((((header(e') = ``pv11_p1 preempted``) ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num()))
               ∧ (↑(pv11_p1_is_bnum() msgval(e')))
               ∧ (↑(fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))  < msgval(e'))))
              ∧ (no ((pv11_p1_scout_output(Cmd;accpts;mf) (pv11_p1_upd_bnum() msgval(e') loc(e')) o
                     pv11_p1_p1b'base(Cmd;mf)) o pv11_p1_ScoutState(Cmd;accpts;mf) 
                                                 (pv11_p1_upd_bnum() msgval(e') loc(e'))) between e' and e)
              ∧ ((header(e) = ``pv11_p1 p1b``)
                ∧ has-es-info-type(es;e;mf;Id
                  × pv11_p1_Ballot_Num()
                  × pv11_p1_Ballot_Num()
                  × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
              ∧ ((pv11_p1_upd_bnum() msgval(e') loc(e')) = (fst(snd(msgval(e)))))
              ∧ (d = 0)
              ∧ (i = loc(e))
              ∧ ((pv11_p1_upd_bnum() msgval(e') loc(e')) = (fst(snd(snd(msgval(e))))))
              ∧ #(fst(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() msgval(e') 
                                                          loc(e');es.e';e))) < pv11_p1_threshold(accpts)
              ∧ auth = pv11_p1_init_active()
              ∧ (p = (pv11_p1_upd_bnum() msgval(e') loc(e')))
              ∧ (L = (snd(pv11_p1_ScoutStateFun(Cmd;accpts;mf;pv11_p1_upd_bnum() msgval(e') loc(e');es.e';e))))))))

Lemma: pv11_p1-decision
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[accpts,ldrs:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)].
∀[mf:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(mf))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[k:ℤ]. ∀[v:Cmd].
  (<d, i, mk-msg(auth;[decision];<k, v>)> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;mf)(e)
  ⇐⇒ loc(e) ↓∈ ldrs
      ∧ (↓∃e':{e':E| e' ≤loc e } 
           ((header(e) = ``pv11_p1 p2b``)
           ∧ has-es-info-type(es;e;mf;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
           ∧ (d = 0)
           ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))))
           ∧ #(pv11_p1_CommanderStateFun(Cmd;accpts;mf;fst(snd(msgval(e)));fst(snd(snd(msgval(e))));es.e';e)) < ...
           ∧ i ↓∈ reps
           ∧ auth = pv11_p1_init_active()
           ∧ (k = (fst(snd(snd(msgval(e))))))
           ∧ ((((header(e') = [propose]) ∧ has-es-info-type(es;e';mf;ℤ × Cmd))
             ∧ ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))
               ∧ (¬↑(pv11_p1_in_domain(Cmd) (fst(msgval(e'))) 
                     (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))))))
             ∧ ((fst(snd(msgval(e)))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
             ∧ (<fst(snd(snd(msgval(e)))), v> = msgval(e')))
             ∨ (((header(e') = ``pv11_p1 adopted``)
                ∧ has-es-info-type(es;e';mf;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
               ∧ ((fst(msgval(e'))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e'))))
               ∧ ((<fst(snd(snd(msgval(e)))), v> ↓∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;mf;es;e')))
                 ∧ (¬(∃p2:Cmd. (<fst(snd(snd(msgval(e)))), p2> ∈ pv11_p1_pmax(Cmd;ldrs_uid) (snd(msgval(e')))))))
                 ∨ (∃v2:pv11_p1_Ballot_Num()
                     (<v2, fst(snd(snd(msgval(e)))), v> ↓∈ snd(msgval(e'))
                     ∧ (¬(∃z5:pv11_p1_Ballot_Num()
                           ∃z8:Cmd. ((↑(v2  < z5)) ∧ (<z5, fst(snd(snd(msgval(e)))), z8> ∈ snd(msgval(e')))))))))
               ∧ ((fst(snd(msgval(e)))) = (fst(msgval(e'))))))
           ∧ (no ((pv11_p1_commander_output(Cmd;accpts;reps;mf) <fst(snd(msgval(e))), fst(snd(snd(msgval(e)))), v> o pv1\000C1_p1_p2b'base(Cmd;mf)) o
                 pv11_p1_CommanderState(Cmd;accpts;mf) (fst(snd(msgval(e)))) (fst(snd(snd(msgval(e)))))) between e' and
              e))))

Lemma: pv11_p1_pmax_wf
∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_pmax(Cmd;ldrs_uid) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) ─→ ((ℤ × Cmd) List))

Lemma: pv11_p1_in_domain_wf
∀[Cmd:ValueAllType]. (pv11_p1_in_domain(Cmd) ∈ ℤ ─→ ((ℤ × Cmd) List) ─→ 𝔹)

Comment: ----- header property --------------------
Shouldn't we generated this automatically ?

Lemma: pv11_p1_headers-property
∀[Cmd:ValueAllType]
  ∀f:pv11_p1_headers_type{i:l}(Cmd)
    (((f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()))
    ∧ ((f ``pv11_p1 p1b``)
      = (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
    ∧ ((f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd))
    ∧ ((f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()))
    ∧ ((f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num())
    ∧ ((f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
    ∧ ((f [propose]) = (ℤ × Cmd))
    ∧ ((f [decision]) = (ℤ × Cmd)))

Lemma: pv11_p1_lt_bnum_trans
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2,b3:pv11_p1_Ballot_Num().  ((↑(b1  < b2)) ⇒ (↑(b2  < b3)) ⇒ (↑(b1  < b3)))

Lemma: pv11_p1_lt_bnum_trans1
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2,b3:pv11_p1_Ballot_Num().
  ((↑(b1  < b2)) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b3)) ⇒ (↑(b1  < b3)))

Lemma: pv11_p1_lt_bnum_trans2
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2,b3:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ⇒ (↑(b2  < b3)) ⇒ (↑(b1  < b3)))

Lemma: pv11_p1_lt_bnum_irrefl
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  (¬↑(b  < b))

Lemma: pv11_p1_lt_bnum_irrefl2
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  ((↑(b  < b)) ⇒ False)

Lemma: pv11_p1_lt_bnum_implies_not
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(b1  < b2)) ⇒ (¬↑(b2  < b1)))

Lemma: pv11_p1_lt_bnum_implies_not2
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(b1  < b2)) ⇒ (↑(b2  < b1)) ⇒ False)

Lemma: pv11_p1_lt_bnum_implies_not3
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().  ((↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)) ⇒ (↑(b1  < b2)) ⇒ False)

Lemma: pv11_p1_lt_bnum_upd
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num(). ∀l:Id.  ((↑(pv11_p1_is_bnum() b)) ⇒ (↑(b  < (pv11_p1_upd_bnum() b l))))

Lemma: pv11_p1_leq_bnum_implies_eq
∀ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b b')) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b)) ⇒ (b = b'))

Lemma: pv11_p1_leq_bnum_implies_eq_or_lt
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ⇒ ((b1 = b2) ∨ (↑(b1  < b2))))

Lemma: pv11_p1_leq_bnum_linorder
∀ldrs_uid:Id ─→ ℤ. (Inj(Id;ℤ;ldrs_uid) ⇒ Linorder(pv11_p1_Ballot_Num();b1,b2.↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)))

Lemma: not-pv11_p1_leq_bnum
∀ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().
  (Inj(Id;ℤ;ldrs_uid) ⇒ (¬↑(pv11_p1_leq_bnum(ldrs_uid) b b')) ⇒ (↑(b'  < b)))

Lemma: pv11_p1_leq_bnum_refl
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) b b))

Lemma: pv11_p1_leq_bnum_dummy
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) pv11_p1_dummy_ballot() b))

Lemma: pv11_p1_leq_bnum_dummy_eq
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  (pv11_p1_leq_bnum(ldrs_uid) pv11_p1_dummy_ballot() b ~ tt)

Lemma: pv11_p1_leq_bnum_max
∀ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) b (pv11_p1_max_bnum(ldrs_uid) b' b)))

Lemma: pv11_p1_leq_bnum_max2
∀ldrs_uid:Id ─→ ℤ. ∀b,b':pv11_p1_Ballot_Num().  (↑(pv11_p1_leq_bnum(ldrs_uid) b (pv11_p1_max_bnum(ldrs_uid) b b')))

Lemma: pv11_p1_leq_bnum_or
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ∨ (↑(pv11_p1_leq_bnum(ldrs_uid) b2 b1)))

Lemma: pv11_p1_max_bnum_dummy
∀ldrs_uid:Id ─→ ℤ. ∀b:pv11_p1_Ballot_Num().  ((pv11_p1_max_bnum(ldrs_uid) b pv11_p1_dummy_ballot()) = b)

Lemma: pv11_p1_max_bnum_if_leq
∀ldrs_uid:Id ─→ ℤ. ∀b1,b2:pv11_p1_Ballot_Num().
  ((↑(pv11_p1_leq_bnum(ldrs_uid) b1 b2)) ⇒ ((pv11_p1_max_bnum(ldrs_uid) b1 b2) = b2))

Lemma: pv11_p1_max_bnum_comm
∀[ldrs_uid:Id ─→ ℤ]. ∀[b1,b2:pv11_p1_Ballot_Num()].
  (pv11_p1_max_bnum(ldrs_uid) b1 b2) = (pv11_p1_max_bnum(ldrs_uid) b2 b1) supposing Inj(Id;ℤ;ldrs_uid)

Lemma: pv11_p1_add_if_new_iff
∀Cmd:ValueAllType. ∀p,x:ℤ × Cmd. ∀proposals:(ℤ × Cmd) List.
  ((p ∈ pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) x proposals)
  ⇐⇒ (p ∈ proposals) ∨ if (∃z∈proposals.pv11_p1_same_proposal(Cmd) x z)_b then False else p = x fi )

Lemma: pv11_p1_add_if_new_iff2
∀A:Type. ∀p,x:A. ∀L:A List. ∀test:A ─→ A ─→ 𝔹.
  ((p ∈ pv11_p1_add_if_new() test x L) ⇐⇒ (p ∈ L) ∨ if (∃z∈L.test x z)_b then False else p = x fi )

Lemma: pv11_p1_add_if_new_if
∀Cmd:ValueAllType. ∀p:ℤ × Cmd. ∀proposals:(ℤ × Cmd) List.
  ((¬↑(pv11_p1_in_domain(Cmd) (fst(p)) proposals)) ⇒ (p ∈ pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) p proposals))

Lemma: pv11_p1_pmax_desc
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_pmax(Cmd;ldrs_uid) pvals)
  ⇒ (∃b:pv11_p1_Ballot_Num()
       ((<b, s, c> ∈ pvals)
       ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b)))))))

Lemma: pv11_p1_pmax_desc_iff
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_pmax(Cmd;ldrs_uid) pvals)
  ⇐⇒ ∃b:pv11_p1_Ballot_Num()
       ((<b, s, c> ∈ pvals)
       ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.  ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))

Lemma: pv11_p1_pmax_desc_implies
∀Cmd:ValueAllType. ∀ldrs_uid:Id ─→ ℤ. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ.
∀c:Cmd.
  ((<b, s, c> ∈ pvals) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_pmax(Cmd;ldrs_uid) pvals)))

Lemma: pv11_p1_upd_desc
∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)
  ⇒ ((<s, c> ∈ proposals2) ∨ ((<s, c> ∈ proposals1) ∧ (¬(∃c':Cmd. (<s, c'> ∈ proposals2))))))

Lemma: pv11_p1_upd_desc_iff
∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)
  ⇐⇒ (<s, c> ∈ proposals2) ∨ ((<s, c> ∈ proposals1) ∧ (¬(∃c':Cmd. (<s, c'> ∈ proposals2)))))

Lemma: pv11_p1_upd_left
∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ proposals1) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)))

Lemma: pv11_p1_upd_right
∀Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ proposals2) ⇒ (∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)))

Lemma: pv11_p1_acc_p2a
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (v ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,accepted = v 
     in (<b, s, c> ∈ accepted) ⇒ (∃e':E. ∃l:Id. (e' ≤loc e  ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))

Lemma: pv11_p1_acc_fun_p2a
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  ((<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (∃e':E. ∃l:Id. (e' ≤loc e  ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))

Lemma: pv11_p1_acc_fun_p2a_pv
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
  ((p ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (∃e':E. ∃l:Id. (e' ≤loc e  ∧ <l, p> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))

Lemma: pv11_p1_ldr_loc_bnum
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,active,proposals = v in 
     ∃n:ℤ. (bnum = (pv11_p1_mk_bnum() n loc(e))))

Lemma: pv11_p1_ldr_fun_loc_bnum
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
  ∃n:ℤ. ((fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e))) = (pv11_p1_mk_bnum() n loc(e)))

Lemma: pv11_p1_ldr_mem_propose
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀v1,v2:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
∀p:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ((e1 <loc e2)
  ⇒ p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)
  ⇒ v1 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ v2 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ case p
      of inl(x) =>
      let s,c = x 
      in let bnum1,active1,proposals1 = v1 in 
         let bnum2,active2,proposals2 = v2 in 
         (¬↑(pv11_p1_in_domain(Cmd) s proposals1)) ⇒ (↑(pv11_p1_in_domain(Cmd) s proposals2))
      | inr(x) =>
      True)

Lemma: pv11_p1_ldr_mem_propose2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀active1,active2:𝔹. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <s, c> ∈ pv11_p1_propose'base(Cmd;f)(e1)
  ⇒ <bnum1, active1, proposals1> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ <bnum2, active2, proposals2> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ (¬↑(pv11_p1_in_domain(Cmd) s proposals1))
  ⇒ (↑(pv11_p1_in_domain(Cmd) s proposals2)))

Lemma: pv11_p1_ldr_fun_mem_propose
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀p:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ((e1 <loc e2)
  ⇒ p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)
  ⇒ case p
      of inl(x) =>
      (¬↑(pv11_p1_in_domain(Cmd) (fst(x)) (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))))))
      ⇒ (↑(pv11_p1_in_domain(Cmd) (fst(x)) (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))))))
      | inr(x) =>
      True)

Lemma: pv11_p1_ldr_fun_mem_propose2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <s, c> ∈ pv11_p1_propose'base(Cmd;f)(e1)
  ⇒ (¬↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))))))
  ⇒ (↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))))))

Lemma: pv11_p1_ldr_mem_preempted
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀v1,v2:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
∀p:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ((e1 <loc e2)
  ⇒ p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)
  ⇒ v1 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ v2 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ let bnum1,active1,proposals1 = v1 in 
     let bnum2,active2,proposals2 = v2 in 
     case p
      of inl(x) =>
      True
      | inr(x) =>
      case x
       of inl(x) =>
       True
       | inr(bnum) =>
       (↑(bnum1  < bnum)) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) (pv11_p1_upd_bnum() bnum loc(e1)) bnum2)))

Lemma: pv11_p1_ldr_active
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,active,proposals1 = v in 
     (↑active)
     ⇒ (∃e':E
          ∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. (e' ≤loc e  ∧ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e'))))

Lemma: pv11_p1_ldr_active2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,active,proposals1 = v in 
     (↑active)
     ⇒ (↓∃e':E
           ∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
            ∃proposals:(ℤ × Cmd) List
             ∃b:𝔹
              ((e' <loc e)
              ∧ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
              ∧ <bnum, b, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'))))

Lemma: pv11_p1_ldr_active_fun
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
  ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))))
  ⇒ (↓∃e':E
        ∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
         ((e' <loc e)
         ∧ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
         ∧ ((fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e))) = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e')))))))

Lemma: pv11_p1_ldr_pos
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,active,proposals1 = v in 
     ↑(pv11_p1_leq_bnum(ldrs_uid) (pv11_p1_init_ballot_num() loc(e)) bnum))

Lemma: pv11_p1_ldr_fun_pos
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
  (↑(pv11_p1_leq_bnum(ldrs_uid) (pv11_p1_init_ballot_num() loc(e)) (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))))

Lemma: pv11_p1_ldr_fun_ord
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
  ((e1 <loc e2)
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))) 
        (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))))))

Lemma: pv11_p1_scout_from_acc
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts:bag(Id).
∀s:bag(Id) × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀bnum:pv11_p1_Ballot_Num().
  (s ∈ pv11_p1_ScoutState(Cmd;accpts;f) bnum(e)
  ⇒ let waitfor,pvalues = s 
     in ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd
          ((p ∈ pvalues)
          ⇒ (∃e':E
               ∃l:Id
                ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
                 (e' ≤loc e  ∧ <l, bnum, bnum, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r)))))

Lemma: pv11_p1_scout_fun_from_acc
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts:bag(Id).
∀b:pv11_p1_Ballot_Num(). ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
  ((p ∈ snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es;e)))
  ⇒ (∃e':E
       ∃l:Id
        ∃r:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. (e' ≤loc e  ∧ <l, b, b, r> ∈ pv11_p1_p1b'base(Cmd;f)(e') ∧ (p ∈ r))))

Lemma: pv11_p1_scout_fun_from_acc2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (p ∈ snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es;e)))
  ⇒ (↓∃e':E. ((e' < e) ∧ (p ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))))

Lemma: pv11_p1_acc_state_fun_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)
  = if e ∈b pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p1a(Cmd;ldrs_uid) + pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) 
                pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)@e 
                pv11_p1_init_acceptor(Cmd)
           else pv11_p1_on_p1a(Cmd;ldrs_uid) + pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) 
                pv11_p1_p1a'base(Cmd;f) (+) pv11_p1_p2a'base(Cmd;f)@e 
                pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
           fi 
    if first(e) then pv11_p1_init_acceptor(Cmd)
    else pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
    fi )

Lemma: pv11_p1_acc_state_fun_eq2
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)
  = if e ∈b pv11_p1_p1a'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p1a(Cmd;ldrs_uid) loc(e) pv11_p1_p1a'base(Cmd;f)@e pv11_p1_init_acceptor(Cmd)
           else pv11_p1_on_p1a(Cmd;ldrs_uid) loc(e) pv11_p1_p1a'base(Cmd;f)@e 
                pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
           fi 
    if e ∈b pv11_p1_p2a'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) pv11_p1_p2a'base(Cmd;f)@e pv11_p1_init_acceptor(Cmd)
           else pv11_p1_on_p2a(Cmd;ldrs_uid) loc(e) pv11_p1_p2a'base(Cmd;f)@e 
                pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
           fi 
    if first(e) then pv11_p1_init_acceptor(Cmd)
    else pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;pred(e))
    fi )

Lemma: pv11_p1_ldr_state_fun_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)
  = if first(e) then pv11_p1_init_leader(Cmd) loc(e)
    if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
      then pv11_p1_on_propose(Cmd) loc(e) pv11_p1_propose'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
      then pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) pv11_p1_adopted'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
      then pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) pv11_p1_preempted'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    else pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    fi )

Lemma: pv11_p1_ldr_state_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
∀[v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)].
  uiff(v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e);↓if first(e) then v = (pv11_p1_init_leader(Cmd) loc(e))
                                                   if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
                                                     then ∃x:ℤ × Cmd
                                                           ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
                                                            (x ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
                                                            ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
                                                            ∧ (v = (pv11_p1_on_propose(Cmd) loc(e) x s)))
                                                   if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
                                                     then ∃x:pv11_p1_Ballot_Num()
                                                             × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
                                                           ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
                                                            (x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
                                                            ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
                                                            ∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s)))
                                                   if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
                                                     then ∃x:pv11_p1_Ballot_Num()
                                                           ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
                                                            (x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
                                                            ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
                                                            ∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s)))
                                                   else v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
                                                   fi )

Lemma: pv11_p1_ldr_state_eq2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
  uiff(v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e);if first(e) then v = (pv11_p1_init_leader(Cmd) loc(e))
  if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
    then ∃x:ℤ × Cmd
          ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
           (x ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
           ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
           ∧ (v = (pv11_p1_on_propose(Cmd) loc(e) x s)))
  if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
    then ∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
          ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
           (x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
           ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
           ∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s)))
  if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
    then ∃x:pv11_p1_Ballot_Num()
          ∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
           (x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
           ∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
           ∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s)))
  else v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
  fi )

Lemma: pv11_p1_ldr_mem_adopted
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀v1,v2:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
∀p:ℤ × Cmd + pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) + pv11_p1_Ballot_Num().
  ((e1 <loc e2)
  ⇒ p ∈ pv11_p1_propose'base(Cmd;f) (+) pv11_p1_adopted'base(Cmd;f) (+) pv11_p1_preempted'base(Cmd;f)(e1)
  ⇒ v1 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ v2 ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ case p
      of inl(x) =>
      True
      | inr(x) =>
      case x
       of inl(x) =>
       let bnum,pvals = x 
       in let bnum1,active1,proposals1 = v1 in 
          let bnum2,active2,proposals2 = v2 in 
          (bnum1 = bnum)
          ⇒ (∀s:ℤ. ∀b:pv11_p1_Ballot_Num(). ∀c:Cmd.
                (((<s, c> ∈ proposals1) ∨ (<b, s, c> ∈ pvals)) ⇒ (↑(pv11_p1_in_domain(Cmd) s proposals2))))
       | inr(x) =>
       True)

Lemma: pv11_p1_ldr_fun_mem_adopted
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
  ⇒ ((↓(<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)))))
     ∨ (∃b:pv11_p1_Ballot_Num(). (↓(<b, s, c> ∈ pvals))))
  ⇒ (↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2)))))))

Lemma: pv11_p1_ldr_proposal3
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List). ∀s:ℤ. ∀c:Cmd.
  (v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ (<s, c> ∈ snd(snd(v)))
  ⇒ (∃e':E
       ∃bnum:pv11_p1_Ballot_Num()
        ∃active:𝔹
         ∃proposals:(ℤ × Cmd) List
          ((e' <loc e)
          ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
          ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
               ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ x ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e'') ⇒ (<s, c> ∈ snd(snd(x)))))
          ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e') ∧ (¬↑(pv11_p1_in_domain(Cmd) s proposals)))
            ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
                ∃b:pv11_p1_Ballot_Num()
                 (<bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
                 ∧ (<b, s, c> ∈ pvals)
                 ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
                      ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))))

Lemma: pv11_p1_ldr_fun_proposal3
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e))))
  ⇒ (∃e':E
       ((e' <loc e)
       ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (<s, c> ∈ snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e''))))))
       ∧ ((<s, c> ∈ pv11_p1_propose'base(Cmd;f)(e')
         ∧ (¬↑(pv11_p1_in_domain(Cmd) s (snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e')))))))
         ∨ (∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
             ∃b:pv11_p1_Ballot_Num()
              (<fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e')), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
              ∧ (<b, s, c> ∈ pvals)
              ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
                   ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))))

Lemma: pv11_p1_adopted_from_init_or_preempted
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e)
  ⇒ (↓(bnum = (pv11_p1_init_ballot_num() loc(e)))
       ∨ (∃e':E
           ∃bnum1,bnum2:pv11_p1_Ballot_Num()
            ∃b:𝔹
             ∃proposals:(ℤ × Cmd) List
              ((e' <loc e)
              ∧ bnum1 ∈ pv11_p1_preempted'base(Cmd;f)(e')
              ∧ <bnum2, b, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
              ∧ (↑(bnum2  < bnum1))
              ∧ (bnum = (pv11_p1_upd_bnum() bnum1 loc(e)))))))

Lemma: pv11_p1_adopted_from_acceptor
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e)
  ⇒ (<b, s, c> ∈ pvals)
  ⇒ (↓∃e':E
        ∃accepted:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
         ((e' < e) ∧ <bnum, accepted> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e') ∧ (<b, s, c> ∈ accepted))))

Lemma: pv11_p1_scout_state_fun_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[bnum:pv11_p1_Ballot_Num()].
∀[accpts:bag(Id)].
  (pv11_p1_ScoutStateFun(Cmd;accpts;f;bnum;es;e)
  = if e ∈b pv11_p1_p1b'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p1b(Cmd) bnum loc(e) pv11_p1_p1b'base(Cmd;f)@e pv11_p1_init_scout(Cmd;accpts)
           else pv11_p1_on_p1b(Cmd) bnum loc(e) pv11_p1_p1b'base(Cmd;f)@e 
                pv11_p1_ScoutStateFun(Cmd;accpts;f;bnum;es;pred(e))
           fi 
    if first(e) then pv11_p1_init_scout(Cmd;accpts)
    else pv11_p1_ScoutStateFun(Cmd;accpts;f;bnum;es;pred(e))
    fi )

Lemma: pv11_p1_commander_state_fun_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[accpts:bag(Id)].
∀[b:pv11_p1_Ballot_Num()]. ∀[s:ℤ].
  (pv11_p1_CommanderStateFun(Cmd;accpts;f;b;s;es;e)
  = if e ∈b pv11_p1_p2b'base(Cmd;f)
      then if first(e)
           then pv11_p1_on_p2b() b s loc(e) pv11_p1_p2b'base(Cmd;f)@e accpts
           else pv11_p1_on_p2b() b s loc(e) pv11_p1_p2b'base(Cmd;f)@e 
                pv11_p1_CommanderStateFun(Cmd;accpts;f;b;s;es;pred(e))
           fi 
    if first(e) then accpts
    else pv11_p1_CommanderStateFun(Cmd;accpts;f;b;s;es;pred(e))
    fi )

Lemma: pv11_p1_unique_adopted
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals1,pvals2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
∀proposals1,proposals2:(ℤ × Cmd) List. ∀b1,b2:𝔹.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals1> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
  ⇒ <bnum, pvals2> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
  ⇒ <bnum, b1, proposals1> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ <bnum, b2, proposals2> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e2)
  ⇒ e1 ≤loc e2 
  ⇒ (pvals1 = pvals2))

Lemma: pv11_p1_unique_adopted_fun
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals1,pvals2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals1> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
  ⇒ <bnum, pvals2> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
  ⇒ (bnum = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))))
  ⇒ (bnum = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))))
  ⇒ e1 ≤loc e2 
  ⇒ (pvals1 = pvals2))

Lemma: pv11_p1_unique_adopted_fun2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals1,pvals2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals1> ∈ pv11_p1_adopted'base(Cmd;f)(e1)
  ⇒ <bnum, pvals2> ∈ pv11_p1_adopted'base(Cmd;f)(e2)
  ⇒ (bnum = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))))
  ⇒ (bnum = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e2))))
  ⇒ (loc(e1) = loc(e2))
  ⇒ (pvals1 = pvals2))

Lemma: pv11_p1_adopted_prior
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
∀b':pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c,c':Cmd.
  ((¬↑first(e))
  ⇒ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)
  ⇒ (<s, c> ∈ proposals)
  ⇒ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
  ⇒ (<b', s, c'> ∈ pvals)
  ⇒ (↓∃b:pv11_p1_Ballot_Num(). ((<b, s, c> ∈ pvals) ∧ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b)))))

Lemma: pv11_p1_ldr_state_propose_pred
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ (header(e1) = [propose])
  ⇒ has-es-info-type(es;e1;f;ℤ × Cmd)
  ⇒ (<s, c> = msgval(e1))
  ⇒ (¬↑(pv11_p1_in_domain(Cmd) s proposals))
  ⇒ (∃e:{e:E| ¬↑first(e)} 
       ((e1 = pred(e)) ∧ e ≤loc e2  ∧ <bnum, active, pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) <s, c> proposals> ∈\000C pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e))))

Lemma: pv11_p1_ldr_fun_state_propose_pred
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((e1 <loc e2)
  ⇒ (<bnum, active, proposals> = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))
  ⇒ (header(e1) = [propose])
  ⇒ has-es-info-type(es;e1;f;ℤ × Cmd)
  ⇒ (<s, c> = msgval(e1))
  ⇒ (¬↑(pv11_p1_in_domain(Cmd) s proposals))
  ⇒ (∃e:{e:E| ¬↑first(e)} 
       ((e1 = pred(e)) ∧ e ≤loc e2  ∧ (<bnum, active, pv11_p1_add_if_new() pv11_p1_same_proposal(Cmd) <s, c> proposals> \000C= pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))))

Lemma: pv11_p1_ldr_state_adopted_pred
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  ((e1 <loc e2)
  ⇒ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
  ⇒ (header(e1) = ``pv11_p1 adopted``)
  ⇒ (<bnum, pvals> = msgval(e1))
  ⇒ (∃e:{e:E| ¬↑first(e)} 
       ((e1 = pred(e))
       ∧ e ≤loc e2 
       ∧ <bnum, tt, pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals)> ∈
          pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e))))

Lemma: pv11_p1_ldr_fun_state_adopted_pred
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  ((e1 <loc e2)
  ⇒ (<bnum, active, proposals> = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1))
  ⇒ (header(e1) = ``pv11_p1 adopted``)
  ⇒ (<bnum, pvals> = msgval(e1))
  ⇒ (∃e:{e:E| ¬↑first(e)} 
       ((e1 = pred(e))
       ∧ e ≤loc e2 
       ∧ (<bnum, tt, pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals)>
         = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))))

Definition: pv11_p1_p2a'send
pv11_p1_p2a'send(Cmd;f) ==  λl,z. mk-msg-interface(l;make-Msg(``pv11_p1 p2a``;z))

Lemma: pv11_p1_p2a'send_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)].
  (pv11_p1_p2a'send(Cmd;f) ∈ Id ─→ (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ─→ Interface)

Definition: pv11_p1_decision'send
pv11_p1_decision'send(Cmd;f) ==  λl,z. mk-msg-interface(l;make-Msg([decision];z))

Lemma: pv11_p1_decision'send_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)].  (pv11_p1_decision'send(Cmd;f) ∈ Id ─→ (ℤ × Cmd) ─→ Interface)

Lemma: pv11_p1_bnum_p2a
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀accpts,ldrs,reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀i,l:Id. ∀s:ℤ. ∀c:Cmd.
  (pv11_p1_p2a'send(Cmd;f) i <l, b, s, c> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e)
  ⇒ (∃n:ℤ. (↑(pv11_p1_eq_bnums() b (pv11_p1_mk_bnum() n l)))))

Lemma: pv11_p1_bnum_p2a_loc
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀accpts,ldrs,reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀i,l:Id. ∀s:ℤ. ∀c:Cmd.
  (pv11_p1_p2a'send(Cmd;f) i <l, b, s, c> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e)
  ⇒ (∃n:ℤ. (↑(pv11_p1_eq_bnums() b (pv11_p1_mk_bnum() n loc(e))))))

Lemma: pv11_p1_about_threshold
∀[T:Type]. ∀[as,bs:bag(T)].  (#(as) < (#(as + bs) + 1) ÷ 2 ⇒ #(as) < #(bs))

Lemma: pv11_p1_inc_acc_pvals_fun
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bsp:pv11_p1_Ballot_Num() × ℤ × Cmd.
  (e1 ≤loc e2 
  ⇒ (bsp ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1)))
  ⇒ (bsp ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2))))

Lemma: pv11_p1_inc_acc_bnum_fun
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
  (e1 ≤loc e2 
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1))) 
        (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2))))))

Lemma: pv11_p1_acc_state_from_p2a
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀v:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ v ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e)
  ⇒ let bnum,accepted = v 
     in (<b, s, c> ∈ accepted)
        ⇒ (↓∃e':E
              ∃l:Id
               (e' ≤loc e 
               ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e')
               ∧ (b = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))
               ∧ (∀e'':E
                    (e' ≤loc e'' 
                    ⇒ e'' ≤loc e 
                    ⇒ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e''))))))))

Lemma: pv11_p1_acc_state_from_p2a_fun
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ⇒ (↓∃e':E
        ∃l:Id
         (e' ≤loc e 
         ∧ <l, b, s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e')
         ∧ (b = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))
         ∧ (∀e'':E
              (e' ≤loc e''  ⇒ e'' ≤loc e  ⇒ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e''))))))))

Lemma: pv11_p1_A1
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  ((e1 <loc e2)
  ⇒ <bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
  ⇒ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e2)
  ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) bnum1 bnum2)))

Lemma: pv11_p1_A2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List. ∀b:pv11_p1_Ballot_Num().
∀pv:ℤ × Cmd. ∀loc:Id.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ (¬↑first(e))
  ⇒ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e)
  ⇒ <bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(pred(e))
  ⇒ (<b, pv> ∈ accepted2)
  ⇒ (¬(<b, pv> ∈ accepted1))
  ⇒ (b = bnum2))

Lemma: pv11_p1_A3
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  ((e1 <loc e2)
  ⇒ <bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
  ⇒ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e2)
  ⇒ (∀pv:pv11_p1_Ballot_Num() × ℤ × Cmd. ((pv ∈ accepted1) ⇒ (pv ∈ accepted2))))

Lemma: pv11_p1_A4_C1
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum1,bnum2:pv11_p1_Ballot_Num(). ∀accepted1,accepted2:(pv11_p1_Ballot_Num()
                                                                                          × ℤ
                                                                                          × Cmd) List. ∀i1,i2,l:Id.
∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ ((<bnum1, accepted1> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e1)
     ∧ <bnum2, accepted2> ∈ pv11_p1_AcceptorState(Cmd;ldrs_uid;f)(e2)
     ∧ (<b, s, p1> ∈ accepted1)
     ∧ (<b, s, p2> ∈ accepted2))
     ∨ (pv11_p1_p2a'send(Cmd;f) i1 <l, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
       ∧ pv11_p1_p2a'send(Cmd;f) i2 <l, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e2)))
  ⇒ (p1 = p2))

Lemma: pv11_p1_A4_C1_funA
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (<b, s, p1> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e1)))
  ⇒ (<b, s, p2> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e2)))
  ⇒ (p1 = p2))

Lemma: pv11_p1_A4_C1_funC
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀i1,i2,l1,l2:Id. ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p1,p2:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ pv11_p1_p2a'send(Cmd;f) i1 <l1, b, s, p1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
  ⇒ pv11_p1_p2a'send(Cmd;f) i2 <l2, b, s, p2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e2)
  ⇒ (p1 = p2))

Lemma: pv11_p1_append_news_iff
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ.
∀reps:bag(Id). ∀pv:pv11_p1_Ballot_Num() × ℤ × Cmd. ∀L1,L2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (∀x∈L1 @ L2.∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))
  ⇒ ((pv ∈ pv11_p1_append_news(Cmd) pv11_p1_same_pvalue(Cmd) L1 L2) ⇐⇒ (pv ∈ L1) ∨ (pv ∈ L2)))

Lemma: pv11_p1_append_news_iff2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ.
∀reps:bag(Id). ∀pv:pv11_p1_Ballot_Num() × ℤ × Cmd. ∀L1,L2:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (∀x∈L1 @ L2.↓∃e:E. (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))))
  ⇒ ((pv ∈ pv11_p1_append_news(Cmd) pv11_p1_same_pvalue(Cmd) L1 L2) ⇐⇒ (pv ∈ L1) ∨ (pv ∈ L2)))

Lemma: pv11_p1_scout_state_subset_pvals
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀bnum:pv11_p1_Ballot_Num().
∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id).
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (header(e) = ``pv11_p1 p1b``)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
  ⇒ ((fst(snd(msgval(e)))) = bnum)
  ⇒ ((fst(snd(snd(msgval(e))))) = bnum)
  ⇒ (↓l_subset(pv11_p1_Ballot_Num()
       × ℤ
       × Cmd;snd(snd(snd(msgval(e))));snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;bnum;es;e)))))

Lemma: pv11_p1_scout_state_from_p1bs
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀start,e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀waitfor:bag(Id).
∀pvalues:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (start ≤loc e 
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (<waitfor, pvalues> = pv11_p1_ScoutStateFun(Cmd;accpts;f;bnum;es.start;e))
  ⇒ (↓∃L:E List
        ((waitfor = [i∈accpts|¬bi ∈b map(λe.loc(e);L))])
        ∧ (∀pv:pv11_p1_Ballot_Num() × ℤ × Cmd
             ((pv ∈ pvalues) ⇐⇒ (pv ∈ concat(map(λe.(snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)));L)))))
        ∧ (∀e':E
             ((e' ∈ L)
             ⇒ ((e' < e) ∧ loc(e') ↓∈ accpts ∧ (bnum = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))))))))

Lemma: pv11_p1_acc_rcv_p2a
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (header(e) = ``pv11_p1 p2a``)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × Cmd)
  ⇒ (∃e':E. ∃i,l:Id. pv11_p1_p2a'send(Cmd;f) i <l, snd(msgval(e))> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e'))
  ⇒ ((fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))) = (fst(snd(msgval(e)))))
  ⇒ (↓(snd(msgval(e)) ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))))

Lemma: pv11_p1_acc_rcv_p2a2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (header(e) = ``pv11_p1 p2a``)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × Cmd)
  ⇒ ((fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e))) = (fst(snd(msgval(e)))))
  ⇒ (↓(snd(msgval(e)) ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))))

Lemma: pv11_p1_commander_state_from_p2bs
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀start,e,e0:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd. ∀waitfor:bag(Id). ∀i,l:Id.
  (start ≤loc e 
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ pv11_p1_p2a'send(Cmd;f) i <l, b, s, c> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e0)
  ⇒ (waitfor = pv11_p1_CommanderStateFun(Cmd;accpts;f;b;s;es.start;e))
  ⇒ (↓∃L:E List
        ((waitfor = [i∈accpts|¬bi ∈b map(λe.loc(e);L))])
        ∧ (∀e':E
             ((e' ∈ L)
             ⇒ ((e' < e)
                ∧ loc(e') ↓∈ accpts
                ∧ (b = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))
                ∧ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e')))))))))

Lemma: pv11_p1_adopted_from_maj_acceptors
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀bnum:pv11_p1_Ballot_Num(). ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ <bnum, pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e)
  ⇒ (↓∃L:E List
        (#([i∈accpts|¬bi ∈b map(λe.loc(e);L))]) < pv11_p1_threshold(accpts)
        ∧ (∀pv:pv11_p1_Ballot_Num() × ℤ × Cmd
             ((pv ∈ pvals) ⇐⇒ (pv ∈ concat(map(λe.(snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)));L)))))
        ∧ (∀e':E
             ((e' ∈ L)
             ⇒ ((e' < e) ∧ loc(e') ↓∈ accpts ∧ (bnum = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))))))))

Lemma: pv11_p1_decision_from_maj_acceptors
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀s:ℤ. ∀c:Cmd. ∀i:Id.
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ 0 < #(accpts)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
  ⇒ (b = (snd(snd(snd(msgval(e))))))
  ⇒ pv11_p1_decision'send(Cmd;f) i <s, c> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e)
  ⇒ (↓∃L:E List
        (#([i∈accpts|¬bi ∈b map(λe.loc(e);L))]) < pv11_p1_threshold(accpts)
        ∧ (∀e':E
             ((e' ∈ L)
             ⇒ ((e' < e)
                ∧ loc(e') ↓∈ accpts
                ∧ (b = (fst(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e'))))
                ∧ (<b, s, c> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e')))))))))

Lemma: pv11_p1_overlapping_accs
∀[accpts,as,bs,cs:bag(Id)].
  (↓∃i:Id. (i ↓∈ bs ∧ i ↓∈ cs)) supposing 
     (#([i∈accpts|¬bbag-deq-member(IdDeq;i;bs)]) < pv11_p1_threshold(accpts) and 
     #(as) < pv11_p1_threshold(accpts) and 
     (accpts = (as + cs)))

Lemma: pv11_p1_A5_C2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀i,l:Id. ∀b,b':pv11_p1_Ballot_Num(). ∀s:ℤ. ∀p,p':Cmd. ∀as,cs:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ (accpts = (as + cs))
  ⇒ #(as) < pv11_p1_threshold(accpts)
  ⇒ (∀a:Id. (a ↓∈ cs ⇒ (↓∃e':E. ((a = loc(e')) ∧ (<b, s, p> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e')))))))
  ⇒ ((<b', s, p'> ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
     ∨ pv11_p1_p2a'send(Cmd;f) i <l, b', s, p'> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e))
  ⇒ (↑(b  < b'))
  ⇒ (p = p'))

Definition: pv11_p1_valid-proposal
pv11_p1_valid-proposal(Cmd;es;e;p;f) ==  ↓∃e':E. (e' c≤ e ∧ p ∈ pv11_p1_propose'base(Cmd;f)(e'))

Lemma: pv11_p1_valid-proposal_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀p:ℤ × Cmd.  (pv11_p1_valid-proposal(Cmd;es;e;p;f) ∈ ℙ)

Definition: pv11_p1_valid-proposals
pv11_p1_valid-proposals(Cmd;es;e;L;f) ==  (∀p∈L.pv11_p1_valid-proposal(Cmd;es;e;p;f))

Lemma: pv11_p1_valid-proposals_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ps:(ℤ × Cmd) List.
    (pv11_p1_valid-proposals(Cmd;es;e;ps;f) ∈ ℙ)

Definition: pv11_p1_valid-LeaderState
pv11_p1_valid-LeaderState(Cmd;ldrs_uid;es;e;f) ==
  pv11_p1_valid-proposals(Cmd;es;e;snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)));f)

Lemma: pv11_p1_valid-LeaderState_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀ldrs_uid:Id ─→ ℤ. ∀e:E.
    (pv11_p1_valid-LeaderState(Cmd;ldrs_uid;es;e;f) ∈ ℙ)

Definition: pv11_p1_valid-AcceptorState
pv11_p1_valid-AcceptorState(Cmd;ldrs_uid;es;e;f) ==
  pv11_p1_valid-proposals(Cmd;es;e;map(λp.(snd(p));snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)));f)

Lemma: pv11_p1_valid-AcceptorState_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀ldrs_uid:Id ─→ ℤ. ∀e:E.
    (pv11_p1_valid-AcceptorState(Cmd;ldrs_uid;es;e;f) ∈ ℙ)

Definition: pv11_p1_valid-ScoutState
pv11_p1_valid-ScoutState(Cmd;accpts;b;start;es;e;f) ==
  pv11_p1_valid-proposals(Cmd;es;e;map(λp.(snd(p));snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es.start;e)));f)

Lemma: pv11_p1_valid-ScoutState_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts:bag(Id). ∀b:pv11_p1_Ballot_Num(). ∀e,start:E.
    (((loc(e) = loc(start)) ⇒ start ≤loc e ) ⇒ (pv11_p1_valid-ScoutState(Cmd;accpts;b;start;es;e;f) ∈ ℙ))

Definition: pv11_p1_valid-adopted-message
pv11_p1_valid-adopted-message(Cmd;es;e;f) ==  pv11_p1_valid-proposals(Cmd;es;e;map(λp.(snd(p));snd(msgval(e)));f)

Lemma: pv11_p1_valid-adopted-message_wf
∀Cmd:{T:Type| valueall-type(T)} . ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E.
  (has-es-info-type(es;e;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
  ⇒ (pv11_p1_valid-adopted-message(Cmd;es;e;f) ∈ ℙ))

Definition: pv11_p1_valid-p1b-message
pv11_p1_valid-p1b-message(Cmd;es;e;f) ==  pv11_p1_valid-proposals(Cmd;es;e;map(λp.(snd(p));snd(snd(snd(msgval(e)))));f)

Lemma: pv11_p1_valid-p1b-message_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E.
    ((header(e) = ``pv11_p1 p1b``) ⇒ (pv11_p1_valid-p1b-message(Cmd;es;e;f) ∈ ℙ))

Definition: pv11_p1_valid-p2a-message
pv11_p1_valid-p2a-message(Cmd;es;e;f) ==  pv11_p1_valid-proposal(Cmd;es;e;snd(snd(msgval(e)));f)

Lemma: pv11_p1_valid-p2a-message_wf
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E.
    ((header(e) = ``pv11_p1 p2a``) ⇒ (pv11_p1_valid-p2a-message(Cmd;es;e;f) ∈ ℙ))

Lemma: pv11_p1_valid-proposal-transitivity
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀p:ℤ × Cmd.
    (pv11_p1_valid-proposal(Cmd;es;e;p;f) ⇒ (∀e':E. (e c≤ e' ⇒ pv11_p1_valid-proposal(Cmd;es;e';p;f))))

Lemma: pv11_p1_valid-proposal-forward
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀e':{e':E| e' ≤loc e } . ∀p:ℤ × Cmd.
    (pv11_p1_valid-proposal(Cmd;es.e';e;p;f) ⇒ pv11_p1_valid-proposal(Cmd;es;e;p;f))

Lemma: pv11_p1_valid-proposal-transitivity-forward
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀p:ℤ × Cmd. ∀e':{e':E| e' ≤loc e } . ∀e1:{e1:E| 
                                                                                                         e1 ≤loc e' } .
    (pv11_p1_valid-proposal(Cmd;es.e1;e';p;f) ⇒ pv11_p1_valid-proposal(Cmd;es;e;p;f))

Lemma: pv11_p1_validity-lemma
∀[Cmd:{T:Type| valueall-type(T)} ]
  ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id).
    (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
    ⇒ (∀e:E
          (pv11_p1_valid-AcceptorState(Cmd;ldrs_uid;es;e;f)
          ∧ pv11_p1_valid-LeaderState(Cmd;ldrs_uid;es;e;f)
          ∧ (∀b:pv11_p1_Ballot_Num(). ∀start:E.  (start ≤loc e  ⇒ pv11_p1_valid-ScoutState(Cmd;accpts;b;start;es;e;f)))
          ∧ ((header(e) = ``pv11_p1 adopted``)
            ⇒ has-es-info-type(es;e;f;pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
            ⇒ pv11_p1_valid-adopted-message(Cmd;es;e;f))
          ∧ ((header(e) = ``pv11_p1 p1b``)
            ⇒ has-es-info-type(es;e;f;Id
               × pv11_p1_Ballot_Num()
               × pv11_p1_Ballot_Num()
               × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
            ⇒ pv11_p1_valid-p1b-message(Cmd;es;e;f))
          ∧ ((header(e) = ``pv11_p1 p2a``)
            ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × Cmd)
            ⇒ pv11_p1_valid-p2a-message(Cmd;es;e;f)))))

Definition: pv11_p1_consistent-pvalues
pv11_p1_consistent-pvalues(Cmd;x;y) ==  ((fst(x)) = (fst(y))) ⇒ ((fst(snd(x))) = (fst(snd(y)))) ⇒ (x = y)

Lemma: pv11_p1_consistent-pvalues_wf
∀[Cmd:Type]. ∀[x,y:pv11_p1_Ballot_Num() × ℤ × Cmd].  (pv11_p1_consistent-pvalues(Cmd;x;y) ∈ ℙ)

Definition: pv11_p1_from-p2a
pv11_p1_from-p2a{i:l}(Cmd;es;e;x) ==  (header(e) = ``pv11_p1 p2a``) ∧ (x = (snd(msgval(e))))

Lemma: pv11_p1_from-p2a_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[x:pv11_p1_Ballot_Num()
                                                                                             × ℤ
                                                                                             × Cmd].
  (pv11_p1_from-p2a{i:l}(Cmd;es;e;x) ∈ ℙ')

Definition: pv11_p1_pvalue
pv11_p1_pvalue{i:l}(Cmd;ldrs_uid;accpts;es;e;x;f) ==
  (x ∈ snd(pv11_p1_AcceptorStateFun(Cmd;ldrs_uid;f;es;e)))
  ∨ (∃b:pv11_p1_Ballot_Num(). ∃start:E. (start ≤loc e  ∧ (x ∈ snd(pv11_p1_ScoutStateFun(Cmd;accpts;f;b;es.start;e)))))
  ∨ ((header(e) = ``pv11_p1 p1b``) ∧ (x ∈ snd(snd(snd(msgval(e))))))
  ∨ ((header(e) = ``pv11_p1 p2a``) ∧ (x = (snd(msgval(e)))))
  ∨ ((header(e) = ``pv11_p1 adopted``) ∧ (x ∈ snd(msgval(e))))

Lemma: pv11_p1_pvalue_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts:bag(Id)]. ∀[ldrs_uid:Id ─→ ℤ].
∀[e:E]. ∀[x:pv11_p1_Ballot_Num() × ℤ × Cmd].
  (pv11_p1_pvalue{i:l}(Cmd;ldrs_uid;accpts;es;e;x;f) ∈ ℙ')

Lemma: pv11_p1_pvalue_from_p2a
∀Cmd:{T:Type| valueall-type(T)} . ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (∀e:E. ∀p:pv11_p1_Ballot_Num() × ℤ × Cmd.
        (pv11_p1_pvalue{i:l}(Cmd;ldrs_uid;accpts;es;e;p;f)
        ⇒ (↓∃e':E. (e' c≤ e ∧ pv11_p1_from-p2a{i:l}(Cmd;es;e';p))))))

Definition: pv11_p1_decision
pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v) ==
  ∃delay:ℤ. ∃client:Id. make-msg-interface(delay;client;make-Msg([decision];<k, v>)) ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs\000C_uid;reps;f)(e)

Lemma: pv11_p1_decision_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[e:E]. ∀[k:ℤ]. ∀[v:Cmd].
  (pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v) ∈ ℙ')

Lemma: pv11_p1_decision_from_p2a
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[e:E]. ∀[k:ℤ]. ∀[v:Cmd].
  ∀a:Id
    (pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;k;v)
    ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
    ⇒ a ↓∈ accpts
    ⇒ (↓∃e':E
          (e' ≤loc e 
          ∧ (k = (fst(snd(snd(msgval(e))))))
          ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))))
          ∧ pv11_p1_p2a'send(Cmd;f) a <loc(e), fst(snd(msgval(e))), k, v> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f\000C)(e'))))

Lemma: pv11_p1_decision_from_p2a_acc
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[e:E]. ∀[s:ℤ]. ∀[c:Cmd]. ∀[a:Id].
  (Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e;s;c)
  ⇒ has-es-info-type(es;e;f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
  ⇒ a ↓∈ accpts
  ⇒ (↓∃e':E
        ((e' < e)
        ∧ loc(e') ↓∈ accpts
        ∧ (s = (fst(snd(snd(msgval(e))))))
        ∧ ((fst(snd(msgval(e)))) = (snd(snd(snd(msgval(e))))))
        ∧ <loc(e), snd(snd(snd(msgval(e)))), s, c> ∈ pv11_p1_p2a'base(Cmd;f)(e'))))

Lemma: pv11_p1_consistency_lemma
∀Cmd:{T:Type| valueall-type(T)} . ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ (∀e:E. ∀b:pv11_p1_Ballot_Num(). ∀k:ℤ. ∀v:Cmd.
        (pv11_p1_pvalue{i:l}(Cmd;ldrs_uid;accpts;es;e;<b, k, v>;f)
        ⇒ (∀e':E. ∀w:Cmd.
              (pv11_p1_decision{i:l}(Cmd;f;accpts;ldrs;ldrs_uid;reps;es;e';k;w)
              ⇒ has-es-info-type(es;e';f;Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
              ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) (snd(snd(snd(msgval(e'))))) b))
              ⇒ (w = v))))))

Definition: pv11_p1_messages-delivered-w-omissions-accpts
pv11_p1_messages-delivered-w-omissions-accpts{i:l}(es;flrs;Cmd;accpts;ldrs;ldrs_uid;reps;f) ==
  msgs-interface-with-omissions-sub{i:l}(pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f);flrs;accpts;f)

Lemma: pv11_p1_messages-delivered-w-omissions-accpts_wf
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[flrs:ℤ].
  (pv11_p1_messages-delivered-w-omissions-accpts{i:l}(es;flrs;Cmd;accpts;ldrs;ldrs_uid;reps;f) ∈ ℙ')

Definition: pv11_p1_messages-delivered-w-omissions-ldrs
pv11_p1_messages-delivered-w-omissions-ldrs{i:l}(es;flrs;Cmd;accpts;ldrs;ldrs_uid;reps;f) ==
  msgs-interface-with-omissions-sub{i:l}(pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f);flrs;ldrs;f)

Lemma: pv11_p1_messages-delivered-w-omissions-ldrs_wf
∀[Cmd:{T:Type| valueall-type(T)} ]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[accpts,ldrs:bag(Id)].
∀[ldrs_uid:Id ─→ ℤ]. ∀[reps:bag(Id)]. ∀[flrs:ℤ].
  (pv11_p1_messages-delivered-w-omissions-ldrs{i:l}(es;flrs;Cmd;accpts;ldrs;ldrs_uid;reps;f) ∈ ℙ')

Definition: pv11_p1_decision'base
pv11_p1_decision'base(Cmd;f) ==  Base([decision])

Lemma: pv11_p1_decision'base_wf
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)].  (pv11_p1_decision'base(Cmd;f) ∈ EClass(ℤ × Cmd))

Lemma: pv11_p1-validity
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ.
∀reps:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ (∀e:E. ∀i:Id. ∀p:ℤ × Cmd.
        (pv11_p1_decision'send(Cmd;f) i p ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e)
        ⇒ pv11_p1_valid-proposal(Cmd;es;e;p;f))))

Lemma: pv11_p1-validity2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ.
∀reps:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ for every p1 in pv11_p1_decision'base(Cmd;f) there is an
     earlier event  with info=m such that
     (msg-header(m) = [propose]) ∧ (p1 = msg-body(m)))

Lemma: pv11_p1-agreement
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀accpts,ldrs:bag(Id).
∀ldrs_uid:Id ─→ ℤ. ∀reps:bag(Id). ∀i1,i2:Id. ∀s:ℤ. ∀c1,c2:Cmd.
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ pv11_p1_decision'send(Cmd;f) i1 <s, c1> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e1)
  ⇒ pv11_p1_decision'send(Cmd;f) i2 <s, c2> ∈ pv11_p1_main(Cmd;accpts;ldrs;ldrs_uid;reps;f)(e2)
  ⇒ (c1 = c2))

Lemma: pv11_p1-agreement2
∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀accpts,ldrs:bag(Id). ∀ldrs_uid:Id ─→ ℤ.
∀reps:bag(Id).
  (pv11_p1_message-constraint{paxos-v11-part1.esh:o}(Cmd; accpts; ldrs; ldrs_uid; reps; f; es)
  ⇒ Inj(Id;ℤ;ldrs_uid)
  ⇒ any p1,p2 from pv11_p1_decision'base(Cmd;f) satisfy
     ((fst(p1)) = (fst(p2))) ⇒ ((snd(p1)) = (snd(p2))))



Home Index