val EVEN = 
  (fn v1 => ((v1 mod 2) <= 0)) ;

datatype ('a, 'b) prod = 
    Pair of 'a * 'b ;

val UNIT = 
  (fn v2 => 
    (fn v1 => (Pair (v2, v1)))) ;

val BIND = 
  (fn v4 => 
    (fn v3 => 
      (fn v5 => 
        (case (v4 v5) of 
            (Pair (v2, v1)) => ((v3 v2) v1))))) ;

fun prob_while_cut v2 = 
  (fn v3 => 
    (fn v4 => 
      (fn v5 => 
        (if (v4 <= 0) 
        then (UNIT v5) 
        else 
          (if (v2 v5) 
          then ((BIND (v3 v5)) 
            (fn v1 => ((((prob_while_cut v2) v3) 
              let val k = (v4 - 1) 
              in 
                (if (k < 0) 
                then 0 
                else k) 
              end ) v1))) 
          else (UNIT v5)))))) ;

val K = 
  (fn v2 => 
    (fn v1 => v2)) ;

val I = 
  (fn v1 => v1) ;

val many = 
  (fn v1 => 
    (fn v2 => ((((prob_while_cut I) (K v1)) v2) true))) ;

fun log2 v1 = 
  (if (v1 <= 0) 
  then 0 
  else ((log2 (v1 div 2)) + 1)) ;

fun factor_twos v4 = 
  (if ((0 < v4) andalso (EVEN v4)) 
  then 
    let val v3 = (factor_twos (v4 div 2)) 
    in 
      (case v3 of 
          (Pair (v2, v1)) => (Pair ((v2 + 1), v1))) 
    end 
  else (Pair (0, v4))) ;

fun modexp v5 = 
  (fn v3 => 
    (fn v4 => 
      (if (v4 <= 0) 
      then 1 
      else 
        let val v2 = (((modexp v5) v3) (v4 div 2)) 
        in 
          let val v1 = ((v2 * v2) mod v5) 
          in 
            (if (EVEN v4) 
            then v1 
            else ((v1 * v3) mod v5)) 
          end 
        end ))) ;

fun witness_tail v2 = 
  (fn v3 => 
    (fn v4 => 
      (if (v4 <= 0) 
      then ((v3 = 1) = false) 
      else 
        let val v1 = ((v3 * v3) mod v2) 
        in 
          (if (v1 = 1) 
          then (((v3 = 1) = false) andalso ((v3 = 
            let val k = (v2 - 1) 
            in 
              (if (k < 0) 
              then 0 
              else k) 
            end ) = false)) 
          else (((witness_tail v2) v1) (v4 - 1))) 
        end ))) ;

val witness = 
  (fn v5 => 
    (fn v4 => 
      let val v3 = (factor_twos 
      let val k = (v5 - 1) 
      in 
        (if (k < 0) 
        then 0 
        else k) 
      end ) 
      in 
        (case v3 of 
            (Pair (v2, v1)) => (((witness_tail v5) (((modexp v5) v4) v1)) v2)) 
      end )) ;

val shd = 
  (fn v1 => (v1 0)) ;

val stl = 
  (fn v1 => 
    (fn v2 => (v1 (v2 + 1)))) ;

fun prob_unif v4 = 
  (fn v5 => 
    (if (v4 <= 0) 
    then (Pair (0, v5)) 
    else 
      let val v3 = ((prob_unif (v4 div 2)) v5) 
      in 
        (case v3 of 
            (Pair (v2, v1)) => (Pair (
              (if (shd v1) 
              then ((2 * v2) + 1) 
              else (2 * v2)), (stl v1)))) 
      end )) ;

fun prob_uniform_cut x = 
  (fn x1 => 
    (fn x2 => 
      (if (x <= 0) 
      then 
        (if (x1 <= 0) 
        then (raise Bind) 
        else (Pair (0, x2))) 
      else 
        (if (x1 <= 0) 
        then (raise Bind) 
        else 
          let val v3 = ((prob_unif (x1 - 1)) x2) 
          in 
            (case v3 of 
                (Pair (v2, v1)) => 
                  (if (v2 < x1) 
                  then (Pair (v2, v1)) 
                  else (((prob_uniform_cut (x - 1)) x1) v1))) 
          end )))) ;

val miller_rabin_1 = 
  (fn v4 => 
    (fn v5 => 
      (if (v4 = 2) 
      then (Pair (true, v5)) 
      else 
        (if ((v4 = 1) orelse (EVEN v4)) 
        then (Pair (false, v5)) 
        else 
          let val v3 = (((prob_uniform_cut (2 * (log2 
          let val k = (v4 - 1) 
          in 
            (if (k < 0) 
            then 0 
            else k) 
          end ))) 
          let val k = (v4 - 2) 
          in 
            (if (k < 0) 
            then 0 
            else k) 
          end ) v5) 
          in 
            (case v3 of 
                (Pair (v2, v1)) => (Pair ((((witness v4) (v2 + 2)) = false), v1))) 
          end )))) ;

val miller_rabin = 
  (fn v1 => 
    (fn v2 => ((many (miller_rabin_1 v1)) v2))) ;