Step * 1 1 of Lemma factorit_wf

.....truecase..... 
1. : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x b < d
        (2 ≤ b)
        (∀[tried:{L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((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. : ℕ+
4. : ℕ
5. b < d
6. 2 ≤ b
7. tried {L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((p ∈ L) ∧ (p x))))} 
8. facs {p:ℕprime(p)}  List
9. x < b
⊢ if x <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)) ∈ ℤ
BY
(CaseNat `x' THEN Reduce 0) }

1
1. : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x b < d
        (2 ≤ b)
        (∀[tried:{L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((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. : ℕ+
4. : ℕ
5. b < d
6. 2 ≤ b
7. tried {L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((p ∈ L) ∧ (p x))))} 
8. facs {p:ℕprime(p)}  List
9. x < b
10. 1 ∈ ℤ
⊢ facs ∈ {L:{p:ℕprime(p)}  List| reduce(λp,q. (p q);1;L) (1 reduce(λp,q. (p q);1;facs)) ∈ ℤ

2
1. : ℕ
2. ∀d:ℕd
     ∀[x:ℕ+]. ∀[b:ℕ].
       (x b < d
        (2 ≤ b)
        (∀[tried:{L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((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. : ℕ+
4. : ℕ
5. b < d
6. 2 ≤ b
7. tried {L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((p ∈ L) ∧ (p x))))} 
8. facs {p:ℕprime(p)}  List
9. x < b
10. ¬(x 1 ∈ ℤ)
⊢ if x <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)) ∈ ℤ


Latex:


Latex:
.....truecase..... 
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.  facs  :  \{p:\mBbbN{}|  prime(p)\}    List
9.  x  <  b  *  b
\mvdash{}  if  x  <z  2  then  facs  else  [x  /  facs]  fi    \mmember{}  \{L:\{p:\mBbbN{}|  prime(p)\}    List| 
                                                                                          reduce(\mlambda{}p,q.  (p  *  q);1;L)
                                                                                          =  (x  *  reduce(\mlambda{}p,q.  (p  *  q);1;facs))\} 


By


Latex:
(CaseNat  1  `x'  THEN  Reduce  0)




Home Index