---

Step * of 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)))
BY
{ (StartEmlProof
   THEN InstLemma `pv11_p1_ldr_mem_propose` [⌜Cmd⌝;⌜f⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;⌜ldrs_uid⌝;⌜<bnum1, active1, proposals1>⌝;
   ⌜<bnum2, active2, proposals2>⌝;⌜inl <s, c>⌝]⋅
   THEN Auto
   THEN All Reduce
   THEN Try (Complete ((D (-1) THEN Auto)))
   THEN MaUseClassRel 0
   THEN Reduce 0
   THEN OrLeft
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}f:pv11\_p1\_headers\_type\{i:l\}(Cmd).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.
\mforall{}ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}bnum1,bnum2:pv11\_p1\_Ballot\_Num().  \mforall{}active1,active2:\mBbbB{}.
\mforall{}proposals1,proposals2:(\mBbbZ{}  \mtimes{}  Cmd)  List.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  <s,  c>  \mmember{}  pv11\_p1\_propose'base(Cmd;f)(e1)
    {}\mRightarrow{}  <bnum1,  active1,  proposals1>  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e1)
    {}\mRightarrow{}  <bnum2,  active2,  proposals2>  \mmember{}  pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e2)
    {}\mRightarrow{}  (\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  proposals1))
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  proposals2)))


By

---

Latex:
(StartEmlProof
  THEN  InstLemma  `pv11\_p1\_ldr\_mem\_propose`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}\mbackslash{}ff2\000C4\mkleeneclose{};\mkleeneopen{}<bnum1
                                                                                                                                                              ,  active1
                                                                                                                                                              ,  proposals1>\mkleeneclose{};
  \mkleeneopen{}<bnum2,  active2,  proposals2>\mkleeneclose{};\mkleeneopen{}inl  <s,  c>\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  Reduce
  THEN  Try  (Complete  ((D  (-1)  THEN  Auto)))
  THEN  MaUseClassRel  0
  THEN  Reduce  0
  THEN  OrLeft
  THEN  Auto)

---

Home Index