---

Step * 1 1 1 of Lemma d-conv_wf


1. n : ℕ
⊢ two-factorizations(n) ∈ bag({p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} )
BY
{ xxxAutoxxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  two-factorizations(n)  \mmember{}  bag(\{p:\mBbbZ{}  \mtimes{}  \mBbbZ{}| 
                                                              ((1  \mleq{}  (fst(p)))  \mwedge{}  ((fst(p))  \mleq{}  n))  \mwedge{}  (((fst(p))  *  (snd(p)))  =  n)\}  )


By

---

Latex:
xxxAutoxxx

---

Home Index