---

Step * of Lemma pv11_p1_pmax_wf

∀[Cmd:ValueAllType]. ∀[ldrs_uid:Id ⟶ ℤ].
  (pv11_p1_pmax(Cmd;ldrs_uid) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) ⟶ ((ℤ × Cmd) List))
BY
{ ((UnivCD THENA Auto) THEN Unfold `pv11_p1_pmax` 0⋅) }

1
1. Cmd : ValueAllType
2. ldrs_uid : Id ⟶ ℤ
⊢ λpvals.let g = λbn,slt,z. let bn',z = z in let s',z = z in (slt =z s') ∧b (bn  < bn') in
          let P = λz.let bn,z = z 
                     in let s,c = z 
                        in ¬b(∃zw∈pvals.g bn s zw)_b in
          mapfilter(λx.(snd(x));P;pvals) ∈ ((pv11_p1_Ballot_Num() × ℤ × Cmd) List) ⟶ ((ℤ × Cmd) List)

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[ldrs$_{uid}$:Id  {}\mrightarrow{}  \mBbbZ{}].
    (pv11\_p1\_pmax(Cmd;ldrs$_{uid}$)  \mmember{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)  {}\mrightarrow{}  (\000C(\mBbbZ{}  \mtimes{}  Cmd)  List))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `pv11\_p1\_pmax`  0\mcdot{})

---

Home Index