---

Step * 1 1 of Lemma d-conv_wf


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

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

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  two-factorizations(n)  \mmember{}  bag(\mBbbN{}  \mtimes{}  \mBbbN{})


By

---

Latex:
xxxSubsumeC  \mkleeneopen{}bag(\{p:\mBbbZ{}  \mtimes{}  \mBbbZ{}|  ((1  \mleq{}  (fst(p)))  \mwedge{}  ((fst(p))  \mleq{}  n))  \mwedge{}  (((fst(p))  *  (snd(p)))  =  n)\}  )\mkleeneclose{}\mcdot{}xxx

---

Home Index