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