---

Step * of 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)))))))
BY
{ (StartEmlProof
   THEN InstLemma `pv11_p1_ldr_fun_mem_propose` [⌜Cmd⌝;⌜f⌝;⌜es⌝;⌜e1⌝;⌜e2⌝;⌜ldrs_uid⌝;⌜inl <s, c>⌝]⋅
   THEN Auto
   THEN All Reduce
   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{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((e1  <loc  e2)
    {}\mRightarrow{}  <s,  c>  \mmember{}  pv11\_p1\_propose'base(Cmd;f)(e1)
    {}\mRightarrow{}  (\mneg{}\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  (snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}\mbackslash{}ff\000C24;f;es;e1))))))
    {}\mRightarrow{}  (\muparrow{}(pv11\_p1\_in\_domain(Cmd)  s  (snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}\mbackslash{}ff2\000C4;f;es;e2)))))))


By

---

Latex:
(StartEmlProof
  THEN  InstLemma  `pv11\_p1\_ldr\_fun\_mem\_propose`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}\000C$\mkleeneclose{};\mkleeneopen{}inl  <s,  c>\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  Reduce
  THEN  Auto
  THEN  MaUseClassRel  0
  THEN  Reduce  0
  THEN  OrLeft
  THEN  Auto)

---

Home Index