---

Step * 1 of Lemma factorit_wf

.....assertion..... 
∀[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;fa\000Ccs)) ∈ ℤ} )))
BY
{ (CompleteInductionOnNat THEN Auto THEN RecUnfold `factorit` 0 THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
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. facs : {p:ℕ| prime(p)}  List
9. x < b * b
⊢ if x <z 2 then facs else [x / facs] fi  ∈ {L:{p:ℕ| prime(p)}  List| 
                                             reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} 

2
.....falsecase..... 
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. facs : {p:ℕ| prime(p)}  List
9. (b * b) ≤ x
⊢ if (∃p∈tried.(b rem p =z 0))_b then eval b' = b + 1 in factorit(x;b';tried;facs)
  if (x rem b =z 0) then eval x' = x ÷ b in factorit(x';b;tried;[b / facs])
  else eval b' = b + 1 in
       factorit(x;b';[b / tried];facs)
  fi  ∈ {L:{p:ℕ| prime(p)}  List| reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} 

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}[d:\mBbbN{}].  \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;facs))\}\000C  )))


By

---

Latex:
(CompleteInductionOnNat  THEN  Auto  THEN  RecUnfold  `factorit`  0  THEN  (SplitOnConclITE  THENA  Auto))

---

Home Index