---

Step * of Lemma pv11_p1_ldr_active_fun

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e:E. ∀ldrs_uid:Id ⟶ ℤ.
  ((↑(fst(snd(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))))
  ⇒ (↓∃e':E
        ∃pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List
         ((e' <loc e)
         ∧ <fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)), pvals> ∈ pv11_p1_adopted'base(Cmd;f)(e')
         ∧ ((fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)))
           = (fst(pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e')))
           ∈ pv11_p1_Ballot_Num()))))
BY
{ (StartEmlProof
   THEN InstLemma `pv11_p1_ldr_active2` [⌜Cmd⌝;⌜f⌝;⌜es⌝;⌜e⌝;⌜ldrs_uid⌝;⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)⌝]⋅
   THEN Auto
   THEN Try (Complete ((BLemma `pv11_p1_LeaderState-classrel` THEN Auto)))
   THEN (Subst ⌜pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e) ~ <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)))>⌝ \000C(-1)⋅
         THENA RepeatFor 2 ((RWO "pair-eta<" 0 THEN Auto))
         )
   THEN Reduce (-1)
   THEN D (-1)
   THEN Auto
   THEN SquashExRepD
   THEN D 0
   THEN (InstConcl [⌜e'⌝;⌜pvals⌝]⋅ THENA Auto)
   THEN Auto
   THEN (FLemma `pv11_p1_LeaderState-classrel` [-3] THENA Auto)
   THEN (RevHypSubst' (-1) 0 THENA Auto)
   THEN Reduce 0
   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{}(fst(snd(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))))
    {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                \mexists{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List
                  ((e'  <loc  e)
                  \mwedge{}  <fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)),  pvals>  \mmember{}
                        pv11\_p1\_adopted'base(Cmd;f)(e')
                  \mwedge{}  ((fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))
                      =  (fst(pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e')))))))


By

---

Latex:
(StartEmlProof
  THEN  InstLemma  `pv11\_p1\_ldr\_active2`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}ldrs$_{uid}$\mkleeneclose{};
  \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `pv11\_p1\_LeaderState-classrel`  THEN  Auto)))
  THEN  (Subst  \mkleeneopen{}pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e) 
                            \msim{}  <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{}  (-\000C1)\mcdot{}
              THENA  RepeatFor  2  ((RWO  "pair-eta<"  0  THEN  Auto))
              )
  THEN  Reduce  (-1)
  THEN  D  (-1)
  THEN  Auto
  THEN  SquashExRepD
  THEN  D  0
  THEN  (InstConcl  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}pvals\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  (FLemma  `pv11\_p1\_LeaderState-classrel`  [-3]  THENA  Auto)
  THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index