---

Step * of Lemma pv11_p1_ldr_fun_state_adopted_pred

∀Cmd:ValueAllType. ∀f:pv11_p1_headers_type{i:l}(Cmd). ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ.
∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List. ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
  ((e1 <loc e2)
  ⇒ (<bnum, active, proposals>
     = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)
     ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))
  ⇒ (header(e1) = ``pv11_p1 adopted`` ∈ Name)
  ⇒ (<bnum, pvals> = msgval(e1) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
  ⇒ (∃e:{e:E| ¬↑first(e)} 
       ((e1 = pred(e) ∈ E)
       ∧ e ≤loc e2 
       ∧ (<bnum, tt, pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals)>
         = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)
         ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))))
BY
{ (((Unfold `vatype` 0 THEN RepeatFor 2 ((D 0 THENA Auto)) THEN AddMessageHeaderTypes)
    THEN skip{Repeat ((At ⌈𝕌{i''}⌉ (D 0)⋅ THENA Auto))}
    )
   THEN skip{(InstLemma `pv11_p1_ldr_state_adopted_pred` [⌈Cmd⌉;⌈f⌉;⌈es⌉;⌈e1⌉;⌈e2⌉;⌈ldrs_uid⌉;⌈bnum⌉;⌈active⌉;
              ⌈proposals⌉;⌈pvals⌉]⋅
              THEN Auto
              THEN Try (Complete ((BLemma `pv11_p1_LeaderState-classrel` THEN Auto)))
              THEN ParallelLast
              THEN Auto
              THEN FLemma `pv11_p1_LeaderState-classrel` [-1]
              THEN MaAuto)}
   ) }

1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. f : pv11_p1_headers_type{i:l}(Cmd)@i'
3. ((f [decision]) = (ℤ × Cmd) ∈ Type)
∧ ((f [propose]) = (ℤ × Cmd) ∈ Type)
∧ ((f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type)
∧ ((f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type)
∧ ((f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type)
∧ ((f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type)
∧ ((f ``pv11_p1 p1b``)
  = (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
  ∈ Type)
∧ ((f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type)
4. f ∈ Name ─→ Type
⊢ ∀es:EO+(Message(f)). ∀e1,e2:E. ∀ldrs_uid:Id ─→ ℤ. ∀bnum:pv11_p1_Ballot_Num(). ∀active:𝔹. ∀proposals:(ℤ × Cmd) List.
  ∀pvals:(pv11_p1_Ballot_Num() × ℤ × Cmd) List.
    ((e1 <loc e2)
    ⇒ (<bnum, active, proposals>
       = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e1)
       ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))
    ⇒ (header(e1) = ``pv11_p1 adopted`` ∈ Name)
    ⇒ (<bnum, pvals> = msgval(e1) ∈ (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)))
    ⇒ (∃e:{e:E| ¬↑first(e)} 
         ((e1 = pred(e) ∈ E)
         ∧ e ≤loc e2 
         ∧ (<bnum, tt, pv11_p1_update_proposals(Cmd) proposals (pv11_p1_pmax(Cmd;ldrs_uid) pvals)>
           = pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)
           ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))))

---

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{}bnum:pv11\_p1\_Ballot\_Num().  \mforall{}active:\mBbbB{}.  \mforall{}proposals:(\mBbbZ{}  \mtimes{}  Cm\000Cd)  List.
\mforall{}pvals:(pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List.
    ((e1  <loc  e2)
    {}\mRightarrow{}  (<bnum,  active,  proposals>  =  pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e\000C1))
    {}\mRightarrow{}  (header(e1)  =  ``pv11\_p1  adopted``)
    {}\mRightarrow{}  (<bnum,  pvals>  =  msgval(e1))
    {}\mRightarrow{}  (\mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\} 
              ((e1  =  pred(e))
              \mwedge{}  e  \mleq{}loc  e2 
              \mwedge{}  (<bnum,  tt,  pv11\_p1\_update\_proposals(Cmd)  proposals  (pv11\_p1\_pmax(Cmd;ldrs$_{ui\000Cd}$)  pvals)>
                  =  pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)))))


By

---

Latex:
(((Unfold  `vatype`  0  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  AddMessageHeaderTypes)
    THEN  skip\{Repeat  ((At  \mkleeneopen{}\mBbbU{}\{i''\}\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto))\}
    )
  THEN  skip\{(InstLemma  `pv11\_p1\_ldr\_state\_adopted\_pred`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}ldrs$_\mbackslash{}ff7\000Cbuid}$\mkleeneclose{};\mkleeneopen{}bnum\mkleeneclose{};
                        \mkleeneopen{}active\mkleeneclose{};\mkleeneopen{}proposals\mkleeneclose{};\mkleeneopen{}pvals\mkleeneclose{}]\mcdot{}
                        THEN  Auto
                        THEN  Try  (Complete  ((BLemma  `pv11\_p1\_LeaderState-classrel`  THEN  Auto)))
                        THEN  ParallelLast
                        THEN  Auto
                        THEN  FLemma  `pv11\_p1\_LeaderState-classrel`  [-1]
                        THEN  MaAuto)\}
  )

---

Home Index