helm/software/matita/library/nat/factorization2.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/factorization.ma".
  16
  17 let rec factorize_aux2 i n b on b ≝
  18  match b with
  19   [ O ⇒ nfa_zero
  20   | S b' ⇒
  21      let p ≝ nth_prime i in
  22       match p_ord n p with
  23        [ pair q r ⇒
  24           match r with
  25           [ O ⇒ nfa_zero
  26           | S r' ⇒
  27              match r' with
  28              [ O ⇒
  29                match q with
  30                [ O ⇒ nfa_one
  31                | _ ⇒ nfa_proper (nf_last (pred q))]
  32              | S _ ⇒
  33                 let res ≝ factorize_aux2 (S i) r b' in
  34                  match res with
  35                  [ nfa_zero ⇒ nfa_zero (* impossible *)
  36                  | nfa_one ⇒ nfa_proper (nf_last q)
  37                  | nfa_proper l ⇒ nfa_proper (nf_cons q l)]]]]].
  38
  39 definition factorize2 ≝ λn.factorize_aux2 0 n n.