---

Step * 2 of Lemma d-conv_wf


1. ∀n:ℕ. (two-factorizations(n) ∈ bag(ℕ × ℕ))
⊢ ∀[r:CRng]. ∀[f,g:ℕ ⟶ |r|].  (d-conv(r;f;g) ∈ ℕ ⟶ |r|)
BY
{ xxxProveWfLemmaxxx }

---

Latex:

---

Latex:

1.  \mforall{}n:\mBbbN{}.  (two-factorizations(n)  \mmember{}  bag(\mBbbN{}  \mtimes{}  \mBbbN{}))
\mvdash{}  \mforall{}[r:CRng].  \mforall{}[f,g:\mBbbN{}  {}\mrightarrow{}  |r|].    (d-conv(r;f;g)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  |r|)


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index