---

Step * of Lemma pv11_p1_on_p2b_wf

pv11_p1_on_p2b() ∈ pv11_p1_Ballot_Num()
⟶ ℤ
⟶ Id
⟶ (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num())
⟶ bag(Id)
⟶ bag(Id)
BY
{ ProveEmlWfLemma }

---

Latex:

---

Latex:
pv11\_p1\_on\_p2b()  \mmember{}  pv11\_p1\_Ballot\_Num()
{}\mrightarrow{}  \mBbbZ{}
{}\mrightarrow{}  Id
{}\mrightarrow{}  (Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num())
{}\mrightarrow{}  bag(Id)
{}\mrightarrow{}  bag(Id)


By

---

Latex:
ProveEmlWfLemma

---

Home Index