---

Step * of 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)) ∈ pv11_p1_Ballot_Num())
BY
{ (StartEmlProof
   THEN (InstLemma `pv11_p1_ldr_loc_bnum` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e⌉;⌈ldrs_uid⌉;
         ⌈<fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e))
          , fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))
          , snd(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))>⌉]⋅
         THENA (Auto
                THEN RepeatFor 2 ((RWO "pair-eta<" 0 THEN Auto))
                THEN BLemma `pv11_p1_LeaderState-classrel`
                THEN Auto)
         )
   THEN All Reduce
   THEN Auto) }

---

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{}.
    \mexists{}n:\mBbbZ{}.  ((fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))  =  (pv11\_p1\_mk\_bn\000Cum()  n  loc(e)))


By

---

Latex:
(StartEmlProof
  THEN  (InstLemma  `pv11\_p1\_ldr\_loc\_bnum`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};
              \mkleeneopen{}<fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e))
                ,  fst(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
                ,  snd(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))>\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto))
                            THEN  BLemma  `pv11\_p1\_LeaderState-classrel`
                            THEN  Auto)
              )
  THEN  All  Reduce
  THEN  Auto)

---

Home Index