|- ∀x. EVEN x ⇔ (x MOD 2 = 0)

|- ∀x. UNIT x = (λs. (x,s))

|- ∀g f x. BIND g f x = UNCURRY f (g x)

|- (∀c b a. prob_while_cut c b 0 a = UNIT a) ∧
   ∀c b n a.
     prob_while_cut c b (SUC n) a =
     if c a then BIND (b a) (prob_while_cut c b n) else UNIT a

|- K = (λx y. x)

|- ∀x. I x = x

|- ∀f n. many f n = prob_while_cut I (K f) n T

|- (log2 0 = 0) ∧ (log2 (SUC v) = SUC (log2 (SUC v DIV 2)))

|- factor_twos n =
   if 0 < n ∧ EVEN n then
     (let (r,s) = factor_twos (n DIV 2) in (SUC r,s))
   else
     (0,n)

|- modexp n a b =
   if b = 0 then
     1
   else
     (let r = modexp n a (b DIV 2) in
      let r2 = (r * r) MOD n
      in
        if EVEN b then r2 else (r2 * a) MOD n)

|- (∀n a. witness_tail n a 0 ⇔ a ≠ 1) ∧
   ∀n a r.
     witness_tail n a (SUC r) ⇔
     (let a2 = (a * a) MOD n
      in
        if a2 = 1 then a ≠ 1 ∧ a ≠ n − 1 else witness_tail n a2 r)

|- ∀n a.
     witness n a ⇔
     (let (r,s) = factor_twos (n − 1)
      in
        witness_tail n (modexp n a s) r)

|- ∀f. shd f = f 0

|- ∀f n. stl f n = f (SUC n)

|- (prob_unif 0 s = (0,s)) ∧
   (prob_unif (SUC v2) s =
    (let (m,s') = prob_unif (SUC v2 DIV 2) s
     in
       (if shd s' then 2 * m + 1 else 2 * m,stl s')))

|- (∀s n. prob_uniform_cut 0 (SUC n) s = (0,s)) ∧
   ∀t s n.
     prob_uniform_cut (SUC t) (SUC n) s =
     (let (res,s') = prob_unif n s
      in
        if res < SUC n then (res,s') else prob_uniform_cut t (SUC n) s')

|- ∀n s.
     miller_rabin_1 n s =
     if n = 2 then
       (T,s)
     else if (n = 1) ∨ EVEN n then
       (F,s)
     else
       (let (a,s') = prob_uniform_cut (2 * log2 (n − 1)) (n − 2) s
        in
          (¬witness n (a + 2),s'))

|- ∀n t. miller_rabin n t = many (miller_rabin_1 n) t