---

Step * 1 1 2 1 1 of Lemma d-conv_wf

.....subterm..... T:t
1:n
1. n : ℕ
2. two-factorizations(n)
= two-factorizations(n)
∈ bag({p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} )
3. x : {p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} 
⊢ x ∈ ℕ × ℕ
BY
{ xxx(D -1 THEN D -2 THEN All Reduce)xxx }

1
1. n : ℕ
2. two-factorizations(n)
= two-factorizations(n)
∈ bag({p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} )
3. x1 : ℤ
4. x2 : ℤ
5. ((1 ≤ x1) ∧ (x1 ≤ n)) ∧ ((x1 * x2) = n ∈ ℤ)
⊢ <x1, x2> ∈ ℕ × ℕ

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  n  :  \mBbbN{}
2.  two-factorizations(n)  =  two-factorizations(n)
3.  x  :  \{p:\mBbbZ{}  \mtimes{}  \mBbbZ{}|  ((1  \mleq{}  (fst(p)))  \mwedge{}  ((fst(p))  \mleq{}  n))  \mwedge{}  (((fst(p))  *  (snd(p)))  =  n)\} 
\mvdash{}  x  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}


By

---

Latex:
xxx(D  -1  THEN  D  -2  THEN  All  Reduce)xxx

---

Home Index