---

Step * of Lemma d-conv_wf

∀[r:CRng]. ∀[f,g:ℕ ⟶ |r|].  (d-conv(r;f;g) ∈ ℕ ⟶ |r|)
BY
{ xxxAssert ⌜∀n:ℕ. (two-factorizations(n) ∈ bag(ℕ × ℕ))⌝⋅xxx }

1
.....assertion..... 
∀n:ℕ. (two-factorizations(n) ∈ bag(ℕ × ℕ))

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

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[f,g:\mBbbN{}  {}\mrightarrow{}  |r|].    (d-conv(r;f;g)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  |r|)


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  (two-factorizations(n)  \mmember{}  bag(\mBbbN{}  \mtimes{}  \mBbbN{}))\mkleeneclose{}\mcdot{}xxx

---

Home Index