---

Step * of 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)))))
BY
{ (StartEmlProof
   THEN (InstLemma `pv11_p1_ldr_pos` [⌜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 BLemma `pv11_p1_LeaderState-classrel`
                THEN Auto
                THEN RepeatFor 2 ((RWO "pair-eta<" 0 THEN Auto)))
         )
   THEN Reduce (-1)
   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{}.
    (\muparrow{}(pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  (pv11\_p1\_init\_ballot\_num()  loc(e)) 
          (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))))


By

---

Latex:
(StartEmlProof
  THEN  (InstLemma  `pv11\_p1\_ldr\_pos`  [\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  BLemma  `pv11\_p1\_LeaderState-classrel`
                            THEN  Auto
                            THEN  RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto)))
              )
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index