Step
*
of Lemma
pv11_p1_leader_propose_wf
∀[Cmd:ValueAllType]
(pv11_p1_leader_propose(Cmd) ∈ Id
─→ (ℤ × Cmd)
─→ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
─→ bag(pv11_p1_Ballot_Num() × ℤ × Cmd))
BY
{ ProveEmlWfLemma }
Latex:
Latex:
\mforall{}[Cmd:ValueAllType]
(pv11\_p1\_leader\_propose(Cmd) \mmember{} Id
{}\mrightarrow{} (\mBbbZ{} \mtimes{} Cmd)
{}\mrightarrow{} (pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List))
{}\mrightarrow{} bag(pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd))
By
Latex:
ProveEmlWfLemma
Home
Index