2 (function n -> (function m -> (Matita_nat_compare.eqb (Matita_nat_div_and_mod.mod_ m n) Matita_nat_nat.O)))
8 Matita_nat_nat.O -> Matita_nat_nat.O
9 | Matita_nat_nat.S(p) ->
11 Matita_nat_nat.O -> (Matita_nat_nat.S(Matita_nat_nat.O))
12 | Matita_nat_nat.S(q) -> (Matita_nat_minimization.min_aux q (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) (function m -> (Matita_nat_compare.eqb (Matita_nat_div_and_mod.mod_ (Matita_nat_nat.S((Matita_nat_nat.S(q)))) m) Matita_nat_nat.O))))
20 Matita_nat_nat.O -> Matita_datatypes_bool.False
21 | Matita_nat_nat.S(p) ->
23 Matita_nat_nat.O -> Matita_datatypes_bool.False
24 | Matita_nat_nat.S(q) -> (Matita_nat_compare.eqb (smallest_factor (Matita_nat_nat.S((Matita_nat_nat.S(q))))) (Matita_nat_nat.S((Matita_nat_nat.S(q))))))