---

Step * of Lemma prime-factors3

∀n:{2...}. (∃factors:{m:{2...}| prime(m)}  List [(n = Π(factors)  ∈ ℤ)])
BY
{ Extract of Obid: prime-factors2
  not unfolding  merge-int primrec natrec better-gcd iroot combinations_aux_rem
  finishing with Auto
  normalizes to:
  
  λn.(letrec rec(n)=if (5) < (n)
                       then eval m = iroot(4;n) + 1 in
                            case primrec(m;inr (λ%10.Ax) ;λi,x. case x
                                                                of inl(%) =>
                                                                inl %
                                                                | inr(%13) =>
                                                                case letrec %(i)=λj.eval p = combinations_aux_rem(1;(j 
                                                                                             - i)
                                                                                             + 1;j;n) in
                                                                                    eval g = better-gcd(n;p) in
                                                                                      if (1) < (g)
                                                                                         then if (g) < (n)
                                                                                                 then inl g
                                                                                                 else eval mid = i
                                                                                                      + (fst(divrem
                                                                                                               (j - i; 2
                                                                                                                ))) in
                                                                                                      case % i mid
                                                                                                       of inl(%29) =>
                                                                                                       inl %29
                                                                                                       | inr(%30) =>
                                                                                                       eval mid' = mid
                                                                                                       + 1 in
                                                                                                       case % mid' j
                                                                                                        of inl(%41) =>
                                                                                                        inl %41
                                                                                                        | inr(%42) =>
                                                                                                        inr (λ%45.Ax) 
                                                                                         else (inr (λ%12.Ax) ) in
                                                                      %((((i + 1) - 1) * m) + 1) 
                                                                     (((i + 1) * m) + 1)
                                                                 of inl(%14) =>
                                                                 inl %14
                                                                 | inr(%15) =>
                                                                 inr (λ%.Ax) )
                             of inl(%) =>
                             let q,r = divrem(n; %) 
                             in eval r = q in
                                merge-int(rec %;rec r)
                             | inr(%) =>
                             <n, Ax>
                       else if n=4 then let q,r = divrem(n; 2) in eval r = q in merge-int(rec 2;rec r) else <n, Ax> in
       rec 
      n) }

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  (\mexists{}factors:\{m:\{2...\}|  prime(m)\}    List  [(n  =  \mPi{}(factors)  )])


By

---

Latex:
Extract  of  Obid:  prime-factors2
not  unfolding    merge-int  primrec  natrec  better-gcd  iroot  combinations\_aux\_rem
finishing  with  Auto
normalizes  to:

\mlambda{}n.(letrec  rec(n)=if  (5)  <  (n)
                                          then  eval  m  =  iroot(4;n)  +  1  in
                                                    case  primrec(m;inr  (\mlambda{}\%10.Ax)  ;
                                                                              \mlambda{}i,x.  case  x
                                                                                          of  inl(\%)  =>
                                                                                          inl  \%
                                                                                          |  inr(\%13)  =>
                                                                                          case  letrec  \%(i)=\mlambda{}j.eval  p  =  combinations\_aux\_rem(1;(j 
                                                                                                                                                    -  i)
                                                                                                                                                    +  1;j;n)  in
                                                                                                                                  eval  g  =  better-gcd(n;p)  in
                                                                                                                                      if  (1)  <  (g)
                                                                                                                                            then  if  (g)  <  (n)
                                                                                                                                                            then  inl  g
                                                                                                                                                            else  eval  mid  =  i
                                                                                                                                                                      +  (fst(divrem
                                                                                                                                                                                        (j  -  i;
                                                                                                                                                                                          2)))  in
                                                                                                                                                                      case  \%  i  mid
                                                                                                                                                                        of  inl(\%29)  =>
                                                                                                                                                                        inl  \%29
                                                                                                                                                                        |  inr(\%30)  =>
                                                                                                                                                                        eval  mid'  =  mid
                                                                                                                                                                        +  1  in
                                                                                                                                                                        case  \%  mid'  j
                                                                                                                                                                          of  inl(\%41)  =>
                                                                                                                                                                          inl  \%41
                                                                                                                                                                          |  inr(\%42)  =>
                                                                                                                                                                          inr  (\mlambda{}\%45.Ax) 
                                                                                                                                            else  (inr  (\mlambda{}\%12.Ax)  )  in
                                                                                                      \%((((i  +  1)  -  1)  *  m)  +  1) 
                                                                                                    (((i  +  1)  *  m)  +  1)
                                                                                            of  inl(\%14)  =>
                                                                                            inl  \%14
                                                                                            |  inr(\%15)  =>
                                                                                            inr  (\mlambda{}\%.Ax)  )
                                                      of  inl(\%)  =>
                                                      let  q,r  =  divrem(n;  \%) 
                                                      in  eval  r  =  q  in
                                                            merge-int(rec  \%;rec  r)
                                                      |  inr(\%)  =>
                                                      <n,  Ax>
                                          else  if  n=4
                                                    then  let  q,r  =  divrem(n;  2) 
                                                              in  eval  r  =  q  in
                                                                    merge-int(rec  2;rec  r)
                                                    else  <n,  Ax>  in
          rec 
        n)

---

Home Index