---

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