---

Step * 1 2 2 2 1 1 2 of Lemma factorit_wf


1. d : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x - b * b < d
       ⇒ (2 ≤ b)
       ⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
           ∀[facs:{p:ℕ| prime(p)}  List].
             (factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)}  List| 
                                          reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))
3. x : ℕ+
4. b : ℕ
5. x - b * b < d
6. 2 ≤ b
7. tried : {L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} 
8. ¬(∃p∈tried. (b rem p) = 0 ∈ ℤ)
9. facs : {p:ℕ| prime(p)}  List
10. (b * b) ≤ x
11. ∀p:{p:ℕ| prime(p)} . p ≠ 0
12. prime(b)
13. x = (((x ÷ b) * b) + 0) ∈ ℤ
14. (x rem b) = 0 ∈ ℤ
⊢ factorit(x ÷ b;b;tried;[b / facs]) ∈ {L:{p:ℕ| prime(p)}  List| 
                                        reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} 
BY
{ (InstHyp [⌜d - 1⌝;⌜x ÷ b⌝;⌜b⌝] 2⋅ THEN Auto') }

1
.....wf..... 
1. d : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x - b * b < d
       ⇒ (2 ≤ b)
       ⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
           ∀[facs:{p:ℕ| prime(p)}  List].
             (factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)}  List| 
                                          reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))
3. x : ℕ+
4. b : ℕ
5. x - b * b < d
6. 2 ≤ b
7. tried : {L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} 
8. ¬(∃p∈tried. (b rem p) = 0 ∈ ℤ)
9. facs : {p:ℕ| prime(p)}  List
10. (b * b) ≤ x
11. ∀p:{p:ℕ| prime(p)} . p ≠ 0
12. prime(b)
13. x = (((x ÷ b) * b) + 0) ∈ ℤ
14. (x rem b) = 0 ∈ ℤ
⊢ x ÷ b ∈ ℕ+

2
.....antecedent..... 
1. d : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x - b * b < d
       ⇒ (2 ≤ b)
       ⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
           ∀[facs:{p:ℕ| prime(p)}  List].
             (factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)}  List| 
                                          reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))
3. x : ℕ+
4. b : ℕ
5. x - b * b < d
6. 2 ≤ b
7. tried : {L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} 
8. ¬(∃p∈tried. (b rem p) = 0 ∈ ℤ)
9. facs : {p:ℕ| prime(p)}  List
10. (b * b) ≤ x
11. ∀p:{p:ℕ| prime(p)} . p ≠ 0
12. prime(b)
13. x = (((x ÷ b) * b) + 0) ∈ ℤ
14. (x rem b) = 0 ∈ ℤ
⊢ (x ÷ b) - b * b < d - 1

3
1. d : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x - b * b < d
       ⇒ (2 ≤ b)
       ⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
           ∀[facs:{p:ℕ| prime(p)}  List].
             (factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)}  List| 
                                          reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))
3. x : ℕ+
4. b : ℕ
5. x - b * b < d
6. 2 ≤ b
7. tried : {L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | x))))} 
8. ¬(∃p∈tried. (b rem p) = 0 ∈ ℤ)
9. facs : {p:ℕ| prime(p)}  List
10. (b * b) ≤ x
11. ∀p:{p:ℕ| prime(p)} . p ≠ 0
12. prime(b)
13. x = (((x ÷ b) * b) + 0) ∈ ℤ
14. (x rem b) = 0 ∈ ℤ
15. ∀[tried:{L:{p:ℕ| prime(p) ∧ p < b}  List| ∀p:{p:ℕ| prime(p)} . (p < b ⇒ ((p ∈ L) ∧ (¬(p | (x ÷ b)))))} ].
    ∀[facs:{p:ℕ| prime(p)}  List].
      (factorit(x ÷ b;b;tried;facs) ∈ {L:{p:ℕ| prime(p)}  List| 
                                       reduce(λp,q. (p * q);1;L) = ((x ÷ b) * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )
⊢ factorit(x ÷ b;b;tried;[b / facs]) ∈ {L:{p:ℕ| prime(p)}  List| 
                                        reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} 

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d
          \mforall{}[x:\mBbbN{}\msupplus{}].  \mforall{}[b:\mBbbN{}].
              (x  -  b  *  b  <  d
              {}\mRightarrow{}  (2  \mleq{}  b)
              {}\mRightarrow{}  (\mforall{}[tried:\{L:\{p:\mBbbN{}|  prime(p)  \mwedge{}  p  <  b\}    List| 
                                        \mforall{}p:\{p:\mBbbN{}|  prime(p)\}  .  (p  <  b  {}\mRightarrow{}  ((p  \mmember{}  L)  \mwedge{}  (\mneg{}(p  |  x))))\}  ].
                      \mforall{}[facs:\{p:\mBbbN{}|  prime(p)\}    List].
                          (factorit(x;b;tried;facs)  \mmember{}  \{L:\{p:\mBbbN{}|  prime(p)\}    List| 
                                                                                    reduce(\mlambda{}p,q.  (p  *  q);1;L)  =  (x  *  reduce(\mlambda{}p,q.  (p  *  q);1;fa\000Ccs))\}  )))
3.  x  :  \mBbbN{}\msupplus{}
4.  b  :  \mBbbN{}
5.  x  -  b  *  b  <  d
6.  2  \mleq{}  b
7.  tried  :  \{L:\{p:\mBbbN{}|  prime(p)  \mwedge{}  p  <  b\}    List|  \mforall{}p:\{p:\mBbbN{}|  prime(p)\}  .  (p  <  b  {}\mRightarrow{}  ((p  \mmember{}  L)  \mwedge{}  (\mneg{}(p  |  x))))\}\000C 
8.  \mneg{}(\mexists{}p\mmember{}tried.  (b  rem  p)  =  0)
9.  facs  :  \{p:\mBbbN{}|  prime(p)\}    List
10.  (b  *  b)  \mleq{}  x
11.  \mforall{}p:\{p:\mBbbN{}|  prime(p)\}  .  p  \mneq{}  0
12.  prime(b)
13.  x  =  (((x  \mdiv{}  b)  *  b)  +  0)
14.  (x  rem  b)  =  0
\mvdash{}  factorit(x  \mdiv{}  b;b;tried;[b  /  facs])  \mmember{}  \{L:\{p:\mBbbN{}|  prime(p)\}    List| 
                                                                                reduce(\mlambda{}p,q.  (p  *  q);1;L)  =  (x  *  reduce(\mlambda{}p,q.  (p  *  q);1;facs\000C))\} 


By

---

Latex:
(InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}x  \mdiv{}  b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  2\mcdot{}  THEN  Auto')

---

Home Index