---

Step * of Lemma pv11_p1_ldr_state_fun_eq

∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
  (pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;e)
  = if first(e) then pv11_p1_init_leader(Cmd) loc(e)
    if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
      then pv11_p1_on_propose(Cmd) loc(e) pv11_p1_propose'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
      then pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) pv11_p1_adopted'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
      then pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) pv11_p1_preempted'base(Cmd;f)@pred(e) 
           pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    else pv11_p1_LeaderStateFun(Cmd;ldrs_uid;f;es;pred(e))
    fi 
  ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))
BY
{ (StartEmlProof
   THEN RepUR ``pv11_p1_LeaderStateFun pv11_p1_LeaderState`` 0
   THEN (RW (AddrC [2] (LemmaC `memory-class3-fun-eq`)) 0 THENA Auto)
   THEN ProveFunctional
   THEN Try (ProveEncodesMsgType)
   THEN Try (CpltAuto)
   THEN Fold `pv11_p1_LeaderState` 0
   THEN Fold `pv11_p1_LeaderStateFun` 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$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].
    (pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;e)
    =  if  first(e)  then  pv11\_p1\_init\_leader(Cmd)  loc(e)
        if  pred(e)  \mmember{}\msubb{}  pv11\_p1\_propose'base(Cmd;f)
            then  pv11\_p1\_on\_propose(Cmd)  loc(e)  pv11\_p1\_propose'base(Cmd;f)@pred(e) 
                      pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
        if  pred(e)  \mmember{}\msubb{}  pv11\_p1\_adopted'base(Cmd;f)
            then  pv11\_p1\_when\_adopted(Cmd;ldrs$_{uid}$)  loc(e)  pv11\_p1\_adopted'base(Cm\000Cd;f)@pred(e) 
                      pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
        if  pred(e)  \mmember{}\msubb{}  pv11\_p1\_preempted'base(Cmd;f)
            then  pv11\_p1\_when\_preempted(Cmd;ldrs$_{uid}$)  loc(e)  pv11\_p1\_preempted'bas\000Ce(Cmd;f)@pred(e) 
                      pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
        else  pv11\_p1\_LeaderStateFun(Cmd;ldrs$_{uid}$;f;es;pred(e))
        fi  )


By

---

Latex:
(StartEmlProof
  THEN  RepUR  ``pv11\_p1\_LeaderStateFun  pv11\_p1\_LeaderState``  0
  THEN  (RW  (AddrC  [2]  (LemmaC  `memory-class3-fun-eq`))  0  THENA  Auto)
  THEN  ProveFunctional
  THEN  Try  (ProveEncodesMsgType)
  THEN  Try  (CpltAuto)
  THEN  Fold  `pv11\_p1\_LeaderState`  0
  THEN  Fold  `pv11\_p1\_LeaderStateFun`  0
  THEN  Auto)

---

Home Index