---

Step * of 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))))))))))
BY
{ (StartEmlProof
   THEN DProdsAndUnions
   THEN AllReduce
   THEN RepeatFor 7 (MoveToConcl (-1))
   THEN MoveToConcl (-2)
   THEN VrCausalInd'
   THEN (UnivCD THENA Auto)) }

1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ⟶ Type
12. es : EO+(Message(f))@i'
13. ldrs_uid : Id ⟶ ℤ@i
14. e : E@i
15. ∀e':E
      ((e' < e)
      ⇒ (∀v1:pv11_p1_Ballot_Num(). ∀v3:𝔹. ∀v4:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
            (<v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e')
            ⇒ (<s, c> ∈ v4)
            ⇒ (∃e1:E
                 ∃bnum:pv11_p1_Ballot_Num()
                  ∃active:𝔹
                   ∃proposals:(ℤ × Cmd) List
                    ((e1 <loc e')
                    ∧ <bnum, active, proposals> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e1)
                    ∧ (∀e'':E. ∀x:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List).
                         ((e1 <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)(e1) ∧ (¬↑(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)(e1)
                           ∧ (<b, s, c> ∈ pvals)
                           ∧ (∀b':pv11_p1_Ballot_Num(). ∀c':Cmd.
                                ((<b', s, c'> ∈ pvals) ⇒ (↑(pv11_p1_leq_bnum(ldrs_uid) b' b))))))))))))
16. v1 : pv11_p1_Ballot_Num()@i
17. v3 : 𝔹@i
18. v4 : (ℤ × Cmd) List@i
19. s : ℤ@i
20. c : Cmd@i
21. <v1, v3, v4> ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e)@i
22. (<s, c> ∈ v4)@i
⊢ ∃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))))))))

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ldrs$_\mbackslash{}ff7\000Cbuid}$:Id  {}\mrightarrow{}  \mBbbZ{}.
\mforall{}v:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    (v  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e)
    {}\mRightarrow{}  (<s,  c>  \mmember{}  snd(snd(v)))
    {}\mRightarrow{}  (\mexists{}e':E
              \mexists{}bnum:pv11\_p1\_Ballot\_Num()
                \mexists{}active:\mBbbB{}
                  \mexists{}proposals:(\mBbbZ{}  \mtimes{}  Cmd)  List
                    ((e'  <loc  e)
                    \mwedge{}  <bnum,  active,  proposals>  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(\000Ce')
                    \mwedge{}  (\mforall{}e'':E.  \mforall{}x:pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbB{}  \mtimes{}  ((\mBbbZ{}  \mtimes{}  Cmd)  List).
                              ((e'  <loc  e'')
                              {}\mRightarrow{}  e''  \mleq{}loc  e 
                              {}\mRightarrow{}  x  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e'')
                              {}\mRightarrow{}  (<s,  c>  \mmember{}  snd(snd(x)))))
                    \mwedge{}  ((<s,  c>  \mmember{}  pv11\_p1\_propose'base(Cmd;f)(e')  \mwedge{}  (\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  proposals)))
                        \mvee{}  (\mexists{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                                \mexists{}b:pv11\_p1\_Ballot\_Num()
                                  (<bnum,  pvals>  \mmember{}  pv11\_p1\_adopted'base(Cmd;f)(e')
                                  \mwedge{}  (<b,  s,  c>  \mmember{}  pvals)
                                  \mwedge{}  (\mforall{}b':pv11\_p1\_Ballot\_Num().  \mforall{}c':Cmd.
                                            ((<b',  s,  c'>  \mmember{}  pvals)  {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$\000C)  b'  b))))))))))


By

---

Latex:
(StartEmlProof
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  RepeatFor  7  (MoveToConcl  (-1))
  THEN  MoveToConcl  (-2)
  THEN  VrCausalInd'
  THEN  (UnivCD  THENA  Auto))

---

Home Index