%Patch files loaded: patch2 version 1.2.2.11

$$$rsa.pvs
rsa : THEORY

  BEGIN

  IMPORTING fermat, inverse_modulo

  p: prime_nat

  q: { x: prime_nat | p /= x }

  p1: posnat = p - 1

  q1: posnat = q - 1


  %------------------
  %  public modulus
  %------------------

  N: posnat = p * q

  N_not_one: LEMMA  N /= 1

  m: posnat = p1 * q1

  m_not_one: LEMMA  m /= 1


  %--------------------------------
  %  private and public exponents
  %--------------------------------

  a: { x: posnat | prime(x, m) }

  b: { x: posnat | rem(m)(a * x) = 1}


  %---------------
  %  Main lemmas
  %---------------  

  x: VAR posnat

  prime_with_N: LEMMA prime(x, N) IFF prime(x, p) AND prime(x, q)

  fermat_p: LEMMA
     prime(x, p) IMPLIES rem(p)(expt(x, p1 * q1)) = 1

  fermat_q: LEMMA 
     prime(x, q) IMPLIES rem(q)(expt(x, p1 * q1)) = 1


  rsa_aux1: LEMMA rem(p)(expt(x, a * b)) = rem(p)(x)

  rsa_aux2: LEMMA rem(q)(expt(x, a * b)) = rem(q)(x)

  rsa_prop: LEMMA rem(N)(expt(x, a * b)) = rem(N)(x)


  %-------------------
  %  Encrypt/Decrypt
  %-------------------

  y: VAR mod(N)

  private(y): mod(N) = rem(N)(expt(y, a))
 
  public(y): mod(N) = rem(N)(expt(y, b))


  private_zero: LEMMA private(0) = 0

  public_zero: LEMMA public(0) = 0


  inverse_rsa1: LEMMA public(private(y)) = y

  inverse_rsa2: LEMMA private(public(y)) = y

  END rsa


$$$rsa.prf
(|rsa|
 (|q_TCC1| "" (LEMMA "unbounded_primes" ("x" "p"))
  (("" (SKOLEM!) (("" (INST + "p!1") (("" (ASSERT) NIL)))))))
 (|p1_TCC1| "" (SUBTYPE-TCC) NIL) (|q1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|N_not_one| "" (FLATTEN)
  (("" (EXPAND "N") (("" (REWRITE "product_one") (("" (GROUND) NIL)))))))
 (|m_not_one| "" (FLATTEN)
  (("" (EXPAND "m")
    (("" (REWRITE "product_one")
      (("" (EXPAND* "p1" "q1") (("" (GROUND) NIL)))))))))
 (|a_TCC1| "" (INST + "1 + m")
  (("" (REWRITE "mutual_primes_equiv")
    (("" (INST + "1" "-1") (("" (ASSERT) NIL)))))))
 (|b_TCC1| "" (LEMMA "rem_inverse2")
  (("" (INST - "m" "a")
    (("" (LEMMA "m_not_one")
      (("" (ASSERT)
        (("" (GROUND) (("" (SKOLEM!) (("" (INST + "py!1") NIL)))))))))))))
 (|prime_with_N_TCC1| "" (ASSERT) (("" (SKOSIMP) (("" (ASSERT) NIL)))))
 (|prime_with_N| "" (SKOLEM!)
  (("" (EXPAND "N")
    (("" (REWRITE "mutual_primes_commutes")
      (("" (REWRITE "mutual_prime_prod")
        (("" (USE "mutual_primes_commutes" ("a" "p"))
          (("" (USE "mutual_primes_commutes" ("a" "q"))
            (("" (REPLACE*) (("" (GROUND) NIL)))))))))))))))
 (|fermat_p| "" (SKOSIMP)
  (("" (AUTO-REWRITE "expt_times_aux" "rem_one" "expt_1n_aux")
    (("" (FORWARD-CHAIN "fermat_theorem2")
      (("" (REWRITE "p1" :DIR RL)
        (("" (ASSERT)
          (("" (REWRITE "rem_expt1" 1 :DIR RL)
            (("" (REPLACE*) (("" (ASSERT) NIL)))))))))))))))
 (|fermat_q_TCC1| "" (ASSERT) NIL)
 (|fermat_q| "" (SKOSIMP)
  (("" (AUTO-REWRITE "rem_one" "expt_1n_aux")
    (("" (FORWARD-CHAIN "fermat_theorem2")
      (("" (REWRITE "q1" :DIR RL)
        (("" (USE "expt_times_aux" ("m" "q1" "n" "p1"))
          (("" (REPLACE -1)
            (("" (REWRITE "rem_expt1" 1 :DIR RL)
              (("" (REPLACE*) (("" (ASSERT) NIL)))))))))))))))))
 (|rsa_aux1| "" (SKOSIMP)
  (("" (USE "non_multiple_of_prime" ("p" "p" "a" "x!1"))
    (("" (GROUND)
      (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero")
        (("1" (REWRITE "rem_expt1" :DIR RL)
          (("1" (CASE-REPLACE "rem(p)(x!1) = 0")
            (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL)))))))
       ("2" (REWRITE "mutual_primes_commutes")
        (("2" (TYPEPRED "b")
          (("2" (ASSERT)
            (("2" (REWRITE "rem_def")
              (("2" (SKOLEM!)
                (("2" (CASE "q!1 >= 0")
                  (("1" (ASSERT)
                    (("1" (REPLACE*)
                      (("1" (DELETE -1 -2 -3)
                        (("1"
                          (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_p")
                          (("1" (EXPAND "expt")
                            (("1" (REWRITE "expt_times_aux")
                              (("1" (REWRITE "rem_prod2" :DIR RL)
                                (("1" (REWRITE "rem_expt1" :DIR RL)
                                  (("1" (EXPAND "m")
                                    (("1" (ASSERT) NIL)))))))))))))))))))
                   ("2" (DELETE -3 2)
                    (("2" (USE "pos_times_le" ("x" "m" "y" "q!1"))
                      (("2" (GROUND) NIL)))))))))))))))))))))))
 (|rsa_aux2| "" (SKOSIMP)
  (("" (USE "non_multiple_of_prime" ("p" "q" "a" "x!1"))
    (("" (GROUND)
      (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero")
        (("1" (REWRITE "rem_expt1" :DIR RL)
          (("1" (CASE-REPLACE "rem(q)(x!1) = 0")
            (("1" (ASSERT) NIL) ("2" (REWRITE "rem_def2") NIL)))))))
       ("2" (REWRITE "mutual_primes_commutes")
        (("2" (TYPEPRED "b")
          (("2" (ASSERT)
            (("2" (REWRITE "rem_def")
              (("2" (SKOLEM!)
                (("2" (CASE "q!1 >= 0")
                  (("1" (ASSERT)
                    (("1" (REPLACE*)
                      (("1" (DELETE -1 -2 -3)
                        (("1"
                          (AUTO-REWRITE "expt_1n_aux" "rem_one" "fermat_q")
                          (("1" (EXPAND "expt")
                            (("1" (REWRITE "expt_times_aux")
                              (("1" (REWRITE "rem_prod2" :DIR RL)
                                (("1" (REWRITE "rem_expt1" :DIR RL)
                                  (("1" (EXPAND "m")
                                    (("1" (ASSERT) NIL)))))))))))))))))))
                   ("2" (DELETE -3 2)
                    (("2" (USE "pos_times_le" ("x" "m" "y" "q!1"))
                      (("2" (GROUND) NIL)))))))))))))))))))))))
 (|rsa_prop| "" (SKOLEM!)
  (("" (AUTO-REWRITE "same_remainder" "distinct_primes" "divides_zero")
    (("" (USE* "rsa_aux1" "rsa_aux2")
      (("" (ASSERT)
        (("" (EXPAND "N")
          (("" (REWRITE "common_multiple_primes")
            (("" (FLATTEN) (("" (REPLACE*) (("" (ASSERT) NIL)))))))))))))))))
 (|private_zero_TCC1| "" (SUBTYPE-TCC) NIL)
 (|private_zero| "" (AUTO-REWRITE "private" "expt" "zero_times1" "rem_zero")
  (("" (ASSERT) (("" (ASSERT) NIL)))))
 (|public_zero| "" (AUTO-REWRITE "public" "expt" "zero_times1" "rem_zero")
  (("" (ASSERT) (("" (ASSERT) NIL)))))
 (|inverse_rsa1| ""
  (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop")
  (("" (SKOLEM!)
    (("" (CASE-REPLACE "y!1 = 0")
      (("1" (ASSERT) NIL)
       ("2" (EXPAND "public")
        (("2" (EXPAND "private")
          (("2" (ASSERT)
            (("2" (REWRITE "expt_times_aux" :DIR RL)
              (("2" (ASSERT) NIL)))))))))))))))
 (|inverse_rsa2| ""
  (AUTO-REWRITE "private_zero" "public_zero" "rem_expt1" "rem_mod" "rsa_prop")
  (("" (SKOLEM!)
    (("" (CASE-REPLACE "y!1 = 0")
      (("1" (ASSERT) NIL)
       ("2" (EXPAND "public")
        (("2" (EXPAND "private")
          (("2" (ASSERT)
            (("2" (REWRITE "expt_times_aux" :DIR RL)
              (("2" (REWRITE "commutative_mult")
                (("2" (ASSERT) NIL))))))))))))))))))
$$$inverse_modulo.pvs
inverse_modulo : THEORY

  BEGIN

  IMPORTING mutual_primes

  x, y: VAR int

  py, b: VAR posnat


  %------------------------------------
  %  Existence of an inverse modulo b
  %------------------------------------

  rem_inverse: LEMMA 
     (EXISTS y : rem(b)(x * y) = 1) IFF x /= 0 AND b /= 1 AND prime(x, b)

  rem_inverse2: LEMMA
     (EXISTS py: rem(b)(x * py) = 1) IFF  x /= 0 AND b /= 1 AND prime(x, b)

  END inverse_modulo

$$$inverse_modulo.prf
(|inverse_modulo|
 (|rem_inverse| "" (SKOLEM!)
  (("" (CASE-REPLACE "x!1=0")
    (("1" (AUTO-REWRITE "rem_zero") (("1" (ASSERT) NIL NIL)) NIL)
     ("2" (ASSERT)
      (("2" (AUTO-REWRITE "mutual_primes_equiv" "rem_def")
        (("2" (ASSERT)
          (("2" (REDUCE :INSTANTIATOR INST!)
            (("1" (INST + "y!1" "-q!1") (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (INST + "n!1")
              (("2" (INST + "- m!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|rem_inverse2| "" (SKOLEM!)
  (("" (REWRITE "rem_inverse" :DIR RL)
    (("" (PROP)
      (("1" (SKOLEM!) (("1" (INST?) NIL NIL)) NIL)
       ("2" (SKOLEM!)
        (("2" (REWRITE "rem_prod2" :DIR RL)
          (("2" (AUTO-REWRITE "rem_zero")
            (("2" (CASE-REPLACE "rem(b!1)(y!1) = 0")
              (("1" (ASSERT) NIL NIL)
               ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$product_modulo.pvs
product_modulo : THEORY

  BEGIN

  IMPORTING products

  u, v: VAR [nat -> nat]

  n, m: VAR nat

  p: VAR posnat

  equivalent_product: LEMMA
     n <= m AND (FORALL (i: idx(n, m)): rem(p)(u(i)) = rem(p)(v(i)))
 	IMPLIES rem(p)(prod(n, m)(u)) = rem(p)(prod(n, m)(v))

  END product_modulo

$$$product_modulo.prf
(|product_modulo| (|equivalent_product_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|equivalent_product| "" (SKOSIMP)
  (("" (ASSERT)
    ((""
      (CASE "FORALL (j : nat): j <= m!1 - n!1 IMPLIES
                                         rem(p!1)(prod(n!1, n!1 + j)(u!1)) = rem(p!1)(prod(n!1, n!1+j)(v!1))")
      (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (DELETE 2)
        (("2" (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "rem_prod")
          NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$parity.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  A few lemmas about odd or even numbers  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

parity : THEORY

  BEGIN

  i : VAR int


  incr_odd : LEMMA  odd?(i + 1) IFF even?(i)

  incr_even : LEMMA  even?(i + 1) IFF odd?(i)


  opposite_odd : LEMMA  odd?(- i) IFF odd?(i)

  opposite_even : LEMMA  even?(- i) IFF even?(i)


  parity1 : LEMMA odd?(i) OR odd?(i + 1)

  parity2 : LEMMA even?(i) OR even?(i + 1)


  odd_not_even : LEMMA  odd?(i) IFF not even?(i)

  even_not_odd : LEMMA  even?(i) IFF not odd?(i)


  even_2i : LEMMA  even?(2 * i)

  odd_2i_plus1 : LEMMA  odd?(2 * i + 1)

  odd_2i_minus1 : LEMMA odd?(2 * i - 1)


  %-------------------------------------
  %  Rewrite rules for small constants
  %-------------------------------------

  parity_zero: LEMMA even?(0)

  parity_one: LEMMA odd?(1)

  parity_two: LEMMA even?(2)

  parity_three: LEMMA odd?(3)

  parity_minus_one: LEMMA odd?(-1)

  parity_minus_two: LEMMA even?(-2)

  parity_minus_three: LEMMA odd?(-3)


  END parity

$$$parity.prf
(|parity| (|incr_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) NIL NIL)
 (|incr_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL)
  (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL NIL)) NIL)
   ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|opposite_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL)
  (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL NIL)) NIL)
   ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|opposite_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL)
  (("1" (INST + "-j!1") (("1" (ASSERT) NIL NIL)) NIL)
   ("2" (INST + "-j!1") (("2" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|parity1| (:NEW-GROUND? NIL) ""
  (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)")
  (("1" (SKOSIMP)
    (("1" (CASE "i!1 >= 0")
      (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT)
        (("2" (INST - "- (1 + i!1)")
          (("2" (REWRITE "opposite_odd" 2 :DIR RL)
            (("2" (REWRITE "opposite_odd" 3 :DIR RL) (("2" (GROUND) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   ("2" (DELETE 2)
    (("2" (INDUCT "n")
      (("1" (GRIND) NIL NIL)
       ("2" (SKOLEM!)
        (("2" (GROUND)
          (("2" (DELETE 1)
            (("2" (EXPAND "odd?")
              (("2" (SKOLEM!)
                (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|parity2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "incr_even")
  (("" (SKOSIMP)
    (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|odd_not_even| (:NEW-GROUND? NIL) "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND) NIL NIL)
     ("2" (USE "parity1")
      (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|even_not_odd| (:NEW-GROUND? NIL) "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND) NIL NIL)
     ("2" (USE "parity1")
      (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|even_2i| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL)
 (|odd_2i_plus1| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL)
 (|odd_2i_minus1| (:NEW-GROUND? NIL) "" (SKOLEM!)
  (("" (REWRITE "incr_even" :DIR RL) (("" (REWRITE "even_2i") NIL NIL)) NIL))
  NIL)
 (|parity_zero| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL)
 (|parity_one| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd")
  (("" (REWRITE "parity_zero") NIL NIL)) NIL)
 (|parity_two| (:NEW-GROUND? NIL) "" (REWRITE "incr_even")
  (("" (REWRITE "parity_one") NIL NIL)) NIL)
 (|parity_three| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd")
  (("" (REWRITE "parity_two") NIL NIL)) NIL)
 (|parity_minus_one_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL)
 (|parity_minus_one| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd")
  (("" (REWRITE "parity_one") NIL NIL)) NIL)
 (|parity_minus_two_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL)
 (|parity_minus_two| (:NEW-GROUND? NIL) "" (REWRITE "opposite_even")
  (("" (REWRITE "parity_two") NIL NIL)) NIL)
 (|parity_minus_three_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL)
 (|parity_minus_three| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd")
  (("" (REWRITE "parity_three") NIL NIL)) NIL))


$$$index_range.pvs
index_range : THEORY

  BEGIN

  i, n, m: VAR nat

  idx(n, m): TYPE = {i | n <= i AND i <= m}

  END index_range

$$$nat_fun_props.pvs
nat_fun_props : THEORY

  BEGIN

  n, m : VAR nat

  injection_n_to_m : THEOREM
	(EXISTS (f : [below(n) -> below(m)]) : injective?(f)) IMPLIES n <= m

  surjection_n_to_m : THEOREM
	(EXISTS (f : [below(n) -> below(m)]) : surjective?(f)) IMPLIES m <= n

  bijection_n_to_m : THEOREM
	(EXISTS (f : [below(n) -> below(m)]) : bijective?(f)) IFF n = m


  injection_n_to_m2: THEOREM
	(EXISTS (f : [upto(n) -> upto(m)]) : injective?(f)) IFF n <= m

  surjection_n_to_m2: THEOREM
	(EXISTS (f : [upto(n) -> upto(m)]) : surjective?(f)) IFF m <= n

  bijection_n_to_m2: THEOREM
	(EXISTS (f : [upto(n) -> upto(m)]) : bijective?(f)) IFF n = m


  surj_equiv_inj: THEOREM
	FORALL (f : [below(n) -> below(n)]) : surjective?(f) IFF injective?(f)
	
  inj_equiv_bij: THEOREM
	FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF injective?(f)

  surj_equiv_bij: THEOREM
	FORALL (f : [below(n) -> below(n)]) : bijective?(f) IFF surjective?(f)


  surj_equiv_inj2: THEOREM
	FORALL (f : [upto(n) -> upto(n)]) : surjective?(f) IFF injective?(f)
	
  inj_equiv_bij2: THEOREM
	FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF injective?(f)

  surj_equiv_bij2: THEOREM
	FORALL (f : [upto(n) -> upto(n)]) : bijective?(f) IFF surjective?(f)


  END nat_fun_props

$$$nat_fun_props.prf
(|nat_fun_props|
 (|injection_n_to_m| "" (INDUCT "n")
  (("1" (ASSERT) NIL NIL)
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "f!1(0)")
      (("2" (ASSERT)
        (("2" (HIDE -1)
          (("2" (INST -1 "m!1 - 1")
            (("2" (ASSERT)
              (("2" (DELETE 2)
                (("2"
                  (INST +
                   "LAMBDA (x : below(j!1)) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF")
                  (("1" (EXPAND "injective?")
                    (("1" (SKOSIMP)
                      (("1" (LIFT-IF)
                        (("1" (LIFT-IF)
                          (("1" (INST-CP -2 "x1!1" "j!1")
                            (("1" (INST-CP -2 "x2!1" "j!1")
                              (("1" (INST -2 "x1!1" "x2!1")
                                (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)
                   ("3" (SKOSIMP)
                    (("3" (EXPAND "injective?")
                      (("3" (INST - "x!1" "j!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|surjection_n_to_m| "" (SKOSIMP*)
  (("" (COPY -1)
    (("" (REWRITE "injection_n_to_m")
      (("" (EXPAND "surjective?" -1)
        (("" (INST -1 "0")
          (("1" (SKOSIMP)
            (("1" (ASSERT)
              (("1" (INST + "inverse(f!1)")
                (("1" (REWRITE "inj_inv") (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL))
                NIL))
              NIL))
            NIL)
           ("2" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bijection_n_to_m| "" (SKOLEM!)
  (("" (PROP)
    (("1" (EXPAND "bijective?")
      (("1" (SKOSIMP)
        (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1"))
          (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1"))
            (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST 1 "LAMBDA (x : below(n!1)) : x")
      (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|injection_n_to_m2| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (LEMMA "injection_n_to_m" ("n" "n!1+1" "m" "m!1+1"))
      (("1" (ASSERT)
        (("1" (SKOLEM!)
          (("1" (INST + "lambda (i : below(1 + n!1)) : f!1(i)")
            (("1" (GRIND :IF-MATCH NIL) (("1" (INST? :WHERE +) (("1" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST + "lambda (i : upto(n!1)): i")
      (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|surjection_n_to_m2| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (LEMMA "surjection_n_to_m" ("n" "n!1+1" "m" "m!1+1"))
      (("1" (ASSERT)
        (("1" (SKOLEM!)
          (("1" (INST + "lambda (i: below(1 + n!1)): f!1(i)")
            (("1" (GRIND :IF-MATCH NIL)
              (("1" (INST? -) (("1" (SKOLEM!) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)
             ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST + "lambda (i : upto(n!1)): IF i <= m!1 THEN i ELSE 0 ENDIF")
      (("2" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|bijection_n_to_m2| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (EXPAND "bijective?")
      (("1" (SKOSIMP)
        (("1" (LEMMA "injection_n_to_m2" ("n" "n!1" "m" "m!1"))
          (("1" (LEMMA "surjection_n_to_m2" ("n" "n!1" "m" "m!1"))
            (("1" (GROUND) (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("2" (INST + "lambda (i : upto(n!1)): i")
      (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|surj_equiv_inj| "" (SKOLEM!)
  (("" (CASE "n!1 = 0")
    (("1" (GRIND) NIL NIL)
     ("2" (GROUND)
      (("1" (USE "surjection_n_to_m" ("n" "n!1 - 1" "m" "n!1"))
        (("1" (ASSERT)
          (("1" (EXPAND* "surjective?" "injective?")
            (("1" (SKOSIMP)
              (("1"
                (INST +
                 "lambda (i : below(n!1 - 1)): IF i < x1!1 THEN f!1(i) ELSE f!1(i+1) ENDIF")
                (("1" (ASSERT)
                  (("1" (SKOLEM!)
                    (("1" (INST - "y!1")
                      (("1" (SKOLEM!)
                        (("1" (CASE "x!1 = x1!1")
                          (("1" (INST + "IF x2!1 < x!1 THEN x2!1 ELSE x2!1-1 ENDIF")
                            (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)
                             ("3" (GROUND) NIL NIL))
                            NIL)
                           ("2" (INST + "IF x!1 < x1!1 THEN x!1 ELSE x!1 - 1 ENDIF")
                            (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)
                             ("3" (GROUND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (USE "injection_n_to_m" ("n" "n!1" "m" "n!1-1"))
        (("2" (ASSERT)
          (("2" (EXPAND* "injective?" "surjective?")
            (("2" (SKOLEM!)
              (("2"
                (INST +
                 "lambda (i : below(n!1)) : IF f!1(i) = n!1 - 1 THEN y!1 ELSE f!1(i) ENDIF")
                (("1" (ASSERT)
                  (("1" (SKOSIMP)
                    (("1" (INST? - :WHERE +)
                      (("1" (LIFT-IF)
                        (("1" (LIFT-IF)
                          (("1" (GROUND)
                            (("1" (INST?) NIL NIL)
                             ("2" (INST + "x2!1") (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)
                 ("3" (SKOSIMP) (("3" (INST? +) (("3" (ASSERT) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|inj_equiv_bij| "" (SKOLEM!)
  (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL))
  NIL)
 (|surj_equiv_bij| "" (SKOLEM!)
  (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj") NIL NIL)) NIL)) NIL))
  NIL)
 (|surj_equiv_inj2| "" (SKOLEM!)
  (("" (LEMMA "surj_equiv_inj" ("n" "n!1+1" "f" "lambda (i : below(n!1 + 1)): f!1(i)"))
    (("1" (EXPAND* "surjective?" "injective?")
      (("1" (REDUCE :IF-MATCH NIL)
        (("1" (INST? -4 :WHERE +) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (INST? -2) (("2" (SKOLEM!) (("2" (INST? +) NIL NIL)) NIL)) NIL)
         ("3" (INST - "y!1") (("3" (SKOLEM!) (("3" (INST + "x!1") NIL NIL)) NIL)) NIL)
         ("4" (INST? - :WHERE +) (("4" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL)
     ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|inj_equiv_bij2| "" (SKOLEM!)
  (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL))
    NIL))
  NIL)
 (|surj_equiv_bij2| "" (SKOLEM!)
  (("" (EXPAND "bijective?") (("" (GROUND) (("" (REWRITE "surj_equiv_inj2") NIL NIL)) NIL))
    NIL))
  NIL))


$$$iterations.pvs
iterations [ T : TYPE ] : THEORY

  BEGIN

  IMPORTING nat_fun_props, index_range

  f : VAR [T, T -> T]

  u, v: VAR [nat -> T]

  n, m, p, q, i, j, k: VAR nat

  x, y, z, t: VAR T


  %--------------------------------------------
  %  Iterated application of f to u(n)...u(m)
  %--------------------------------------------

  iter(f, n, (m | n <= m), u): RECURSIVE T =
      IF n=m THEN  u(n) ELSE f(iter(f, n, m-1, u), u(m)) ENDIF
    MEASURE m

  iter_once: LEMMA iter(f, n, n, u) = u(n)

  iter_induct: LEMMA  
     FORALL n, (m | n <= m): 
	iter(f, n, m + 1, u) = f(iter(f, n, m, u), u(m + 1))

  iter_same_elements: LEMMA
     FORALL n, (m | n <= m):
	(FORALL i: n <= i AND i <= m IMPLIES u(i) = v(i))
	    IMPLIES iter(f, n, m, u) = iter(f, n, m, v)



  %----------------------------------------
  %  Iteration of an associative function
  %----------------------------------------

  g : VAR { f | associative?(f) }

  associativity: LEMMA  g(x, g(y, z)) = g(g(x, y), z)

  iter_assoc_split: LEMMA 
     n <= m AND m < p IMPLIES 
	g(iter(g, n, m, u), iter(g, m + 1, p, u)) = iter(g, n, p, u)



  %--------------------------------------------------------
  %  Iteration of an associative and commutative function
  %--------------------------------------------------------

  h : VAR { g | commutative?(g) }

  commutativity: LEMMA h(x, y) = h(y, x)

  commut_assoc1: LEMMA h(h(x, y), h(z, t)) = h(h(x, z), h(y, t))

  commut_assoc2: LEMMA h(h(x, y), z) = h(h(z, y), x)


  %--------------------------------------------
  %  iteration on h(u(n),v(n))...h(u(m),v(m))
  %--------------------------------------------

  iter_split: LEMMA
     FORALL n, (m | n <= m):
       iter(h, n, m, lambda i: h(u(i), v(i))) = h(iter(h, n, m, u), iter(h, n, m, v))



  %-------------------------------------------
  %  Invariance if two elements are swapped
  %-------------------------------------------

  swap(u, n, m)(i): T = IF i=m THEN u(n) ELSIF i=n THEN u(m) ELSE u(i) ENDIF


  swap_unchanged: LEMMA swap(u, n, n) = u

  swap_commutes: LEMMA swap(u, n, m) = swap(u, m, n)

  swap_inverse: LEMMA swap(swap(u, n, m), n, m) = u


  iter_swap_first_last: LEMMA  n <= m IMPLIES
	iter(h, n, m, swap(u, n, m)) = iter(h, n, m, u)

  iter_swap_last: LEMMA  n <= i AND i <= m IMPLIES
	iter(h, n, m, swap(u, i, m)) = iter(h, n, m, u)

  iter_swap: LEMMA n <= i AND i <= j AND j <= m IMPLIES
	iter(h, n, m, swap(u, i, j)) = iter(h, n, m, u)



  %--------------------------------------------
  % IF u[n..m] is a permutation of v[p..q] 
  % then iter(h, n, m, u) = iter(h, p, q, v)
  %--------------------------------------------

  permutation(u, n, m, v, p, q): bool =
    EXISTS (a: [idx(n, m) -> idx(p, q)]): bijective?(a)
	AND FORALL (i: idx(n, m)): u(i) = v(a(i))

  perm_range: LEMMA
     n <= m AND permutation(u, n, m, v, p, q) IMPLIES  m - n = q - p

  perm_equiv: LEMMA
    permutation(u, n, n+m, v, p, p+m) IFF
      EXISTS (a: [idx(n, n+m) -> idx(p, p+m)]): injective?(a)
	AND FORALL (i: idx(n, n+m)): u(i) = v(a(i))


  iter_permutation: LEMMA 
     permutation(u, n, n + m, v, p, p + m) IMPLIES
	iter(h, n, n + m, u) = iter(h, p, p + m, v)

  iter_permutation2: LEMMA
     n <= m AND permutation(u, n, m, v, p, q) IMPLIES 
	iter(h, n, m, u) = iter(h, p, q, v)

  iter_permutation3: LEMMA
     FORALL (a : [idx(n, n + m) -> idx(p, p + m)]):
        injective?(a) AND (FORALL (i: idx(n, n + m)): u(i) = v(a(i)))
            IMPLIES iter(h, n, n + m, u) = iter(h, p, p + m, v)


  END iterations



$$$iterations.prf
(|iterations| (|iter_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|iter_once_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_once| "" (GRIND) NIL NIL)
 (|iter_induct_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_induct| "" (GRIND) NIL NIL)
 (|iter_same_elements| "" (SKOSIMP)
  ((""
    (CASE "FORALL (x: nat): n!1 + x <= m!1 IMPLIES iter(f!1, n!1, n!1 + x, u!1) = iter(f!1, n!1, n!1 + x, v!1)")
    (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)
     ("2" (DELETE 2) (("2" (INDUCT-AND-SIMPLIFY "x") NIL NIL)) NIL))
    NIL))
  NIL)
 (|associativity| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "associative?")
    (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|iter_assoc_split_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_assoc_split_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_assoc_split| "" (SKOLEM + ("g!1" "m!1" "n!1" _ "u!1"))
  (("" (INDUCT-AND-REWRITE "p" 1 "iter")
    (("" (CASE "m!1 < j!1")
      (("1" (ASSERT)
        (("1" (REWRITE "associativity" 1) (("1" (ASSERT) NIL NIL))
          NIL))
        NIL)
       ("2" (STOP-REWRITE "iter")
        (("2" (CASE-REPLACE "m!1 = j!1")
          (("1" (REWRITE "iter_once") NIL NIL) ("2" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|commutativity| "" (GRIND) NIL NIL)
 (|commut_assoc1| "" (SKOLEM!)
  ((""
    (NAME-REPLACE "x!2" "h!1(h!1(x!1, z!1), h!1(y!1, t!1))" :HIDE? NIL)
    (("" (REWRITE "associativity")
      (("" (REWRITE "associativity")
        (("" (REWRITE "associativity" :DIR RL)
          (("" (REWRITE "associativity" :DIR RL +)
            (("" (USE "commutativity" ("x" "z!1" "y" "y!1"))
              (("" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|commut_assoc2| "" (SKOLEM!)
  (("" (USE "commutativity" ("x" "z!1" "y" "y!1"))
    (("" (USE "commutativity" ("x" "x!1" "y" "y!1"))
      (("" (REPLACE*)
        (("" (DELETE -)
          (("" (REWRITE "associativity" :DIR RL)
            (("" (REWRITE "associativity" :DIR RL)
              (("" (USE "commutativity" ("x" "x!1" "y" "z!1"))
                (("" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|iter_split| "" (SKOSIMP)
  ((""
    (CASE "FORALL (x: nat): iter(h!1, n!1, n!1 + x, lambda i: h!1(u!1(i), v!1(i))) = h!1(iter(h!1, n!1, n!1 + x, u!1), iter(h!1, n!1, n!1 + x, v!1))")
    (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)
     ("2" (DELETE 2)
      (("2" (AUTO-REWRITE "iter")
        (("2" (INDUCT "x")
          (("1" (ASSERT) NIL NIL)
           ("2" (SKOSIMP)
            (("2" (ASSERT)
              (("2" (REPLACE*)
                (("2" (REWRITE "commut_assoc1") NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|swap_unchanged| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
  NIL)
 (|swap_commutes| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
  NIL)
 (|swap_inverse| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
  NIL)
 (|iter_swap_first_last| "" (SKOSIMP)
  (("" (CASE-REPLACE "m!1 = n!1")
    (("1" (REWRITE "swap_unchanged") NIL NIL)
     ("2" (AUTO-REWRITE "iter_once" "iter" "swap")
      (("2" (ASSERT)
        (("2" (CASE-REPLACE "m!1 - 1 = n!1")
          (("1" (ASSERT) (("1" (REWRITE "commutativity") NIL NIL)) NIL)
           ("2" (STOP-REWRITE "iter")
            (("2" (USE "iter_assoc_split" ("m" "n!1" "u" "u!1"))
              (("2"
                (USE "iter_assoc_split"
                     ("m" "n!1" "u" "swap(u!1, n!1, m!1)"))
                (("2" (ASSERT)
                  (("2" (REPLACE -1 + RL)
                    (("2" (REPLACE -2 + RL)
                      (("2" (DELETE -1 -2)
                        (("2"
                          (CASE-REPLACE
                           "iter(h!1, 1 + n!1, m!1 - 1, swap(u!1, n!1, m!1)) = iter(h!1, 1 + n!1, m!1 - 1, u!1)")
                          (("1" (REWRITE "commut_assoc2") NIL NIL)
                           ("2" (REWRITE "iter_same_elements")
                            (("2" (DELETE 2 5) (("2" (REDUCE) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|iter_swap_last_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_swap_last| "" (SKOSIMP)
  (("" (AUTO-REWRITE "iter_swap_first_last")
    (("" (CASE-REPLACE "i!1 = n!1")
      (("1" (ASSERT) NIL NIL)
       ("2"
        (USE "iter_assoc_split"
             ("m" "i!1 - 1" "u" "swap(u!1, i!1, m!1)"))
        (("1" (USE "iter_assoc_split" ("m" "i!1 - 1" "u" "u!1"))
          (("1" (ASSERT)
            (("1"
              (CASE-REPLACE
               "iter(h!1, n!1, i!1 - 1, swap(u!1, i!1, m!1)) = iter(h!1, n!1, i!1 - 1, u!1)")
              (("1" (ASSERT) NIL NIL)
               ("2" (REWRITE "iter_same_elements")
                (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (ASSERT) NIL NIL))
          NIL)
         ("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|iter_swap_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_swap| "" (SKOSIMP)
  (("" (AUTO-REWRITE "iter_swap_last")
    (("" (CASE-REPLACE "j!1 = m!1")
      (("1" (ASSERT) NIL NIL)
       ("2"
        (USE "iter_assoc_split" ("m" "j!1" "u" "swap(u!1, i!1, j!1)"))
        (("2" (USE "iter_assoc_split" ("m" "j!1" "u" "u!1"))
          (("2" (ASSERT)
            (("2"
              (CASE-REPLACE
               "iter(h!1, 1 + j!1, m!1, swap(u!1, i!1, j!1)) = iter(h!1, 1+j!1, m!1, u!1)")
              (("1" (ASSERT) NIL NIL)
               ("2" (REWRITE "iter_same_elements")
                (("2" (DELETE -1 -2 2 4) (("2" (GRIND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|perm_range| "" (EXPAND "permutation")
  (("" (SKOSIMP*)
    (("" (ASSERT)
      (("" (TYPEPRED "a!1(n!1)")
        (("" (ASSERT)
          (("" (DELETE -1 -2 -3 -5)
            (("" (REWRITE "bijection_n_to_m2" :DIR RL)
              ((""
                (INST +
                 "lambda (i : upto(m!1 - n!1)): a!1(n!1 + i) - p!1")
                (("1" (GRIND :IF-MATCH NIL)
                  (("1" (INST -3 "p!1 + y!1")
                    (("1" (SKOLEM!)
                      (("1" (INST + "x!1 - n!1")
                        (("1" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL)
                   ("2" (INST -3 "n!1 + x1!1" "n!1 + x2!1")
                    (("2" (ASSERT) NIL NIL)) NIL))
                  NIL)
                 ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|perm_equiv| "" (SKOSIMP)
  (("" (EXPAND "permutation")
    (("" (EXPAND "bijective?")
      (("" (GROUND)
        (("1" (SKOSIMP)
          (("1" (INST?) (("1" (ASSERT) (("1" (GROUND) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (SKOSIMP)
          (("2" (INST?)
            (("2" (GROUND)
              (("2" (DELETE -2)
                (("2"
                  (USE "surj_equiv_inj2"
                       ("n" "m!1" "f"
                        "lambda (i : upto(m!1)): a!1(i + n!1) - p!1"))
                  (("1" (GRIND :IF-MATCH NIL)
                    (("1" (INST - "y!1 - p!1")
                      (("1" (SKOLEM!)
                        (("1" (INST? +) (("1" (ASSERT) NIL NIL)) NIL))
                        NIL))
                      NIL)
                     ("2" (INST - "n!1 + x1!1" "n!1 + x2!1")
                      (("2" (ASSERT) NIL NIL)) NIL))
                    NIL)
                   ("2" (SKOSIMP) (("2" (GROUND) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|iter_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_permutation_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_permutation| "" (SKOLEM 1 ("h!1" _ "n!1" "p!1" _ _))
  (("" (AUTO-REWRITE "iter" "swap")
    (("" (INDUCT "m")
      (("1" (SKOSIMP)
        (("1" (EXPAND "permutation")
          (("1" (SKOSIMP)
            (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL)
       ("2" (AUTO-REWRITE "perm_equiv")
        (("2" (SKOSIMP*)
          (("2" (ASSERT)
            (("2" (SKOSIMP)
              (("2"
                (INST - "u!1"
                 "swap(v!1, a!1(1 + j!1 + n!1), j!1 + 1 + p!1)")
                (("2" (GROUND)
                  (("1"
                    (USE "iter_swap_last"
                         ("n" "p!1" "i" "a!1(1 + j!1 + n!1)" "m"
                          "1 + j!1 + p!1"))
                    (("1" (ASSERT)
                      (("1" (REPLACE -1 + RL)
                        (("1" (DELETE -1)
                          (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (DELETE 2)
                    (("2"
                      (INST + "lambda (i : idx(n!1, j!1+n!1)):
                        IF a!1(i) = 1 + j!1 + p!1 THEN a!1(1 + j!1 + n!1) ELSE a!1(i) ENDIF")
                      (("1" (GROUND)
                        (("1" (DELETE -2)
                          (("1" (EXPAND "injective?")
                            (("1" (SKOSIMP)
                              (("1"
                                (INST-CP - "x1!1" "x2!1")
                                (("1"
                                  (INST-CP - "x1!1" "1+j!1+n!1")
                                  (("1"
                                    (INST - "x2!1" "1+j!1+n!1")
                                    (("1"
                                      (ASSERT)
                                      (("1"
                                        (LIFT-IF)
                                        (("1"
                                          (LIFT-IF)
                                          (("1" (GROUND) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (SKOLEM!)
                          (("2" (LIFT-IF)
                            (("2" (GROUND)
                              (("1"
                                (INST?)
                                (("1"
                                  (EXPAND "swap")
                                  (("1"
                                    (LIFT-IF)
                                    (("1" (GROUND) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2"
                                (INST?)
                                (("2"
                                  (EXPAND "injective?")
                                  (("2"
                                    (INST - "i!1" "1 + j!1 + n!1")
                                    (("2"
                                      (ASSERT)
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)
                       ("3" (SKOSIMP)
                        (("3" (GROUND)
                          (("3" (EXPAND "injective?")
                            (("3" (INST - "i!1" "1 + j!1 + n!1")
                              (("3" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|iter_permutation2_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_permutation2| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "perm_range")
    (("" (ASSERT)
      ((""
        (USE "iter_permutation" ("m" "m!1 - n!1" "p" "p!1" "v" "v!1"))
        (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|iter_permutation3_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_permutation3_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|iter_permutation3| "" (SKOSIMP)
  (("" (REWRITE "iter_permutation")
    (("" (REWRITE "perm_equiv")
      (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL))
    NIL))
  NIL))


$$$products.pvs
products : THEORY

  BEGIN

  IMPORTING iterations, parity

  i, j, n, m, p, q: VAR nat

  u, v : VAR [nat -> real]

  x, y, z: VAR real


  %--------------------------------------------------
  %  prod(n, m)(u) = u(n) * u(n+1) * ... * u(m)
  %  (requires n <= m AND u: [nat -> real])
  %--------------------------------------------------
  
  f: VAR [real, real -> real]

  times_assoc_commutes: JUDGEMENT * HAS_TYPE 
	{ f | associative?(f) AND commutative?(f) }

  prod(n, (m | n <= m))(u): real = iter(*, n, m, u)


  prod_once: LEMMA prod(n, n)(u) = u(n)

  prod_step: LEMMA
       n <= m IMPLIES prod(n, m+1)(u) = prod(n, m)(u) * u(m+1)

  prod_same_elements: LEMMA
	n <= m AND (FORALL (i : idx(n, m)) : u(i) = v(i))
	   IMPLIES prod(n, m)(u) = prod(n, m)(v)

  prod_split: LEMMA
        n <= m AND m < p IMPLIES prod(n, m)(u) * prod(m+1, p)(u) = prod(n, p)(u)

  prod_split2: LEMMA
	n <= m IMPLIES
            prod(n, m)(lambda i : u(i) * v(i)) = prod(n, m)(u) * prod(n, m)(v)

  prod_permutation: LEMMA
	permutation(u, n, n + m, v, p, p + m)
	   IMPLIES prod(n, n + m)(u) = prod(p, p + m)(v)

  prod_const: LEMMA  prod(n, n + m)(lambda i: x) = expt(x, m + 1)



  %-----------------------
  %  Sign of the product
  %-----------------------

  P: VAR { R: [real -> bool] | FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) }

  prod_closure: LEMMA 
	n <= m AND (FORALL (i: idx(n, m)): P(u(i))) IMPLIES P(prod(n, m)(u))

  prod_positive: LEMMA
        n <= m AND (FORALL (i: idx(n, m)): u(i) > 0) IMPLIES prod(n, m)(u) > 0

  prod_negative: LEMMA
	n <= m AND (FORALL (i: idx(n, m)): u(i) < 0) 
	    IMPLIES IF even?(m - n) THEN prod(n, m)(u) < 0 ELSE prod(n, m)(u) > 0 ENDIF

  prod_negative1: LEMMA
        n <= m AND even?(m - n) AND (FORALL (i: idx(n, m)): u(i) < 0) 
           IMPLIES prod(n, m)(u) < 0

  prod_negative2: LEMMA
        n <= m AND odd?(m - n) AND (FORALL (i: idx(n, m)): u(i) < 0) 
           IMPLIES prod(n, m)(u) >  0

  prod_null: LEMMA
        n <= m AND (EXISTS (i: idx(n, m)): u(i) = 0) IMPLIES prod(n, m)(u) = 0

  prod_null2: LEMMA
	n <= m IMPLIES (prod(n, m)(u) = 0 IFF EXISTS (i: idx(n, m)): u(i) = 0)


  posu:  VAR [nat -> posreal]
  nzu:   VAR [nat -> nzreal]
  nnu:   VAR [nat -> nonneg_real]

  prod_posreal_seq_is_posreal: JUDGEMENT prod(n, (m | n <= m))(posu) HAS_TYPE posreal
  prod_nzreal_seq_is_nzreal:   JUDGEMENT prod(n, (m | n <= m))(nzu)  HAS_TYPE nzreal
  prod_nnreal_seq_is_nnreal:   JUDGEMENT prod(n, (m | n <= m))(nnu)  HAS_TYPE nonneg_real

  ru:    VAR [nat -> rat]
  posru: VAR [nat -> posrat]
  nzru:  VAR [nat -> nzrat]
  nnru:  VAR [nat -> nonneg_rat]

  prod_rat_seq_is_rat:       JUDGEMENT prod(n, (m | n <= m))(ru)    HAS_TYPE rat
  prod_posrat_seq_is_posrat: JUDGEMENT prod(n, (m | n <= m))(posru) HAS_TYPE posrat
  prod_nzrat_seq_is_nzrat:   JUDGEMENT prod(n, (m | n <= m))(nzru)  HAS_TYPE nzrat
  prod_nnrat_seq_is_nnrat:   JUDGEMENT prod(n, (m | n <= m))(nnru)  HAS_TYPE nonneg_rat

  iu:    VAR [nat -> int]
  nu:    VAR [nat -> nat]
  posnu: VAR [nat -> posnat]
  nziu:  VAR [nat -> nzint]
  
  prod_int_seq_is_int:       JUDGEMENT prod(n, (m | n <= m))(iu)    HAS_TYPE int
  prod_posnat_seq_is_posnat: JUDGEMENT prod(n, (m | n <= m))(posnu) HAS_TYPE posnat
  prod_nzint_seq_is_nzint:   JUDGEMENT prod(n, (m | n <= m))(nziu)  HAS_TYPE nzint
  prod_nat_seq_is_nat:       JUDGEMENT prod(n, (m | n <= m))(nu)    HAS_TYPE nat



  %------------------------------------
  %  prod(n)(a) = a(0) * ... * a(n-1)
  %  requires a : [below(n) -> real]
  %------------------------------------

  prod(n)(a:[below(n) -> real]): RECURSIVE real =
     IF n=0 THEN 1 ELSE prod(n-1)(lambda (i: below(n-1)): a(i)) * a(n-1) ENDIF
   MEASURE n


  variant_prod_zero: LEMMA
	FORALL (a: [below(0) -> real]): prod(0)(a) = 1  

  variant_prod_one: LEMMA
	FORALL (a: [below(1) -> real]): prod(1)(a) = a(0)

  variant_prod_two: LEMMA
	FORALL (a: [below(2) -> real]): prod(2)(a) = a(0) * a(1)


  variant_prod_equiv: LEMMA
	FORALL (a: [below(n) -> real]): 
	    prod(n)(a) = prod(0, n)(lambda i: IF i<n THEN a(i) ELSE 1 ENDIF)

  variant_prod_split: LEMMA
	FORALL (a, b: [below(n) -> real]):
	    prod(n)(lambda (i: below(n)): a(i) * b(i)) = prod(n)(a) * prod(n)(b)

  variant_prod_permutation: LEMMA
        FORALL (a, b: [below(n) -> real]), (h: [below(n) -> below(n)]): 
	    injective?(h) AND a = b o h IMPLIES prod(n)(a) = prod(n)(b)

  variant_prod_cont: LEMMA
        prod(n)(lambda (i: below(n)): x) = expt(x, n)
	

  %--------
  %  Sign
  %--------

  Q: VAR { R: [real -> bool] | R(1) AND FORALL x, y: R(x) AND R(y) IMPLIES R(x * y) }

  variant_prod_closure: LEMMA
	FORALL (a: [below(n) -> real]):
	   (FORALL (i: below(n)): Q(a(i))) IMPLIES Q(prod(n)(a))

  variant_prod_positive: LEMMA
	FORALL (a: [below(n) -> real]):
	   (FORALL (i: below(n)): a(i) > 0) IMPLIES prod(n)(a) > 0

  variant_prod_negative: LEMMA
	FORALL (a: [below(n) -> real]):
	   (FORALL (i: below(n)): a(i) < 0) IMPLIES 
		IF even?(n) THEN prod(n)(a) > 0 ELSE prod(n)(a) < 0 ENDIF

  variant_prod_negative1: LEMMA
	FORALL (a: [below(n) -> real]):
           even?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) > 0

  variant_prod_negative2: LEMMA
	FORALL (a: [below(n) -> real]):
           odd?(n) AND (FORALL (i: below(n)): a(i) < 0) IMPLIES prod(n)(a) <  0

  variant_prod_null: LEMMA
	FORALL (a: [below(n) -> real]):
	   (EXISTS (i: below(n)): a(i) = 0) IMPLIES prod(n)(a) = 0

  variant_prod_null2: LEMMA
	FORALL (a: [below(n) -> real]):
	   prod(n)(a) = 0 IFF EXISTS (i: below(n)): a(i) = 0



  on: VAR { n | odd?(n) }
  en: VAR { n | even?(n) }
  pn: VAR posnat

  varprod_posreal_seq:  JUDGEMENT prod(n)(a: [below(n) -> posreal])     HAS_TYPE posreal
  varprod_nzreal_seq:   JUDGEMENT prod(n)(a: [below(n) -> nzreal])      HAS_TYPE nzreal
  varprod_nnreal_seq:   JUDGEMENT prod(n)(a: [below(n) -> nonneg_real]) HAS_TYPE nonneg_real

  varprod_negreal_seq1: JUDGEMENT prod(en)(a: [below(en) -> negreal]) HAS_TYPE posreal
  varprod_negreal_seq2: JUDGEMENT prod(on)(a: [below(on) -> negreal]) HAS_TYPE negreal

  varprod_rat_seq:     JUDGEMENT prod(n)(a: [below(n) -> rat])        HAS_TYPE rat
  varprod_posrat_seq:  JUDGEMENT prod(n)(a: [below(n) -> posrat])     HAS_TYPE posrat
  varprod_nzrat_seq:   JUDGEMENT prod(n)(a: [below(n) -> nzrat])      HAS_TYPE nzrat
  varprod_nnrat_seq:   JUDGEMENT prod(n)(a: [below(n) -> nonneg_rat]) HAS_TYPE nonneg_rat

  varprod_negrat_seq1: JUDGEMENT prod(en)(a: [below(en) -> negrat]) HAS_TYPE posrat
  varprod_negrat_seq2: JUDGEMENT prod(on)(a: [below(on) -> negrat]) HAS_TYPE negrat

  varprod_int_seq:     JUDGEMENT prod(n)(a: [below(n) -> int])    HAS_TYPE int
  varprod_posint_seq:  JUDGEMENT prod(n)(a: [below(n) -> posint]) HAS_TYPE posint
  varprod_nzint_seq:   JUDGEMENT prod(n)(a: [below(n) -> nzint])  HAS_TYPE nzint
  varprod_nat_seq:     JUDGEMENT prod(n)(a: [below(n) -> nat])    HAS_TYPE nat

  varprod_negint_seq1: JUDGEMENT prod(en)(a: [below(en) -> negint]) HAS_TYPE posint
  varprod_negint_seq2: JUDGEMENT prod(on)(a: [below(on) -> negint]) HAS_TYPE negint


  END products

$$$products.prf
(|products| (|times_assoc_commutes| "" (GRIND) NIL NIL)
 (|prod_once_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_once| "" (GRIND) NIL NIL)
 (|prod_step_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_step| "" (AUTO-REWRITE "prod" "iter_induct[real]" "mult")
  (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|prod_same_elements| "" (EXPAND "prod")
  (("" (SKOSIMP)
    (("" (REWRITE "iter_same_elements")
      (("" (DELETE 2)
        (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|prod_split_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_split_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_split| "" (SKOSIMP)
  (("" (EXPAND "prod")
    (("" (USE "iter_assoc_split[real]") (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|prod_split2| "" (SKOSIMP)
  (("" (AUTO-REWRITE "prod")
    (("" (ASSERT) (("" (USE "iter_split" ("u" "u!1" "v" "v!1")) NIL NIL))
      NIL))
    NIL))
  NIL)
 (|prod_permutation_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_permutation_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_permutation| "" (SKOSIMP)
  (("" (EXPAND "prod") (("" (REWRITE "iter_permutation") NIL NIL)) NIL)) NIL)
 (|prod_const_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_const| "" (SKOLEM + (_ "n!1" "x!1"))
  (("" (INDUCT-AND-REWRITE "m" 1 "prod_once" "prod_step" "expt") NIL NIL))
  NIL)
 (|prod_closure| "" (SKOSIMP)
  (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES P!1(prod(n!1, n!1+i)(u!1))")
    (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL))
      NIL)
     ("2" (DELETE 2)
      (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step")
        (("2" (TYPEPRED "P!1") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|prod_positive| "" (SKOSIMP)
  (("" (CASE "FORALL i: i <= m!1 - n!1 IMPLIES prod(n!1, n!1 + i)(u!1) > 0")
    (("1" (INST - "m!1 -n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL))
      NIL)
     ("2" (DELETE 2)
      (("2" (INDUCT-AND-REWRITE "i" 1 "prod_once" "prod_step" "pos_times_gt")
        NIL NIL))
      NIL))
    NIL))
  NIL)
 (|prod_negative| "" (SKOSIMP)
  (("" (ASSERT)
    ((""
      (CASE "FORALL i: i <= m!1 - n!1 IMPLIES IF even?(i) THEN prod(n!1, n!1 + i)(u!1) < 0 ELSE prod(n!1, n!1 + i)(u!1) > 0 ENDIF")
      (("1" (INST - "m!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (DELETE 2)
        (("2"
          (AUTO-REWRITE "prod_once" "prod_step" "pos_times_gt" "neg_times_lt"
                        "parity_zero")
          (("2" (INDUCT "i")
            (("1" (REDUCE) NIL NIL)
             ("2" (SKOSIMP)
              (("2" (REWRITE "incr_even" +)
                (("2" (REWRITE "odd_not_even" +)
                  (("2" (ASSERT)
                    (("2" (STOP-REWRITE "prod_step") (("2" (REDUCE) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|prod_negative1| "" (SKOSIMP)
  (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|prod_negative2| "" (SKOSIMP)
  (("" (REWRITE "odd_not_even")
    (("" (USE "prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|prod_null| "" (SKOSIMP*)
  (("" (EXPAND "prod")
    (("" (ASSERT)
      (("" (USE "iter_swap_last[real]" ("i" "i!1"))
        (("" (ASSERT)
          (("" (REPLACE -1 + RL)
            (("" (DELETE -1)
              (("" (AUTO-REWRITE "iter" "swap")
                (("" (CASE "n!1 = m!1")
                  (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|prod_null2| "" (SKOSIMP)
  (("" (GROUND)
    (("1" (USE "prod_closure" ("P" "lambda x: x /= 0"))
      (("1" (GROUND)
        (("1" (DELETE -) (("1" (SKOSIMP) (("1" (INST?) NIL NIL)) NIL)) NIL))
        NIL)
       ("2" (SKOSIMP)
        (("2" (ASSERT) (("2" (REWRITE "zero_times3") NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (FORWARD-CHAIN "prod_null") NIL NIL))
    NIL))
  NIL)
 (|prod_posreal_seq_is_posreal| "" (SKOLEM!)
  (("" (USE "prod_positive")
    (("" (SPLIT -)
      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)
       ("3" (DELETE 2) (("3" (REDUCE) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|prod_nzreal_seq_is_nzreal| "" (SKOSIMP)
  (("" (REWRITE "prod_null2") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|prod_nnreal_seq_is_nnreal| "" (SKOSIMP)
  (("" (USE* "prod_positive" "prod_null")
    (("" (GROUND)
      (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|prod_rat_seq_is_rat| "" (SKOLEM!)
  (("" (AUTO-REWRITE "rationals.closed_times")
    (("" (REWRITE "prod_closure") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|prod_posrat_seq_is_posrat| "" (SKOLEM!)
  (("" (USE* "prod_rat_seq_is_rat" "prod_posreal_seq_is_posreal")
    (("" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|prod_nzrat_seq_is_nzrat| "" (SKOLEM!)
  (("" (USE* "prod_rat_seq_is_rat" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL)
 (|prod_nnrat_seq_is_nnrat| "" (SKOLEM!)
  (("" (USE* "prod_rat_seq_is_rat" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL)
 (|prod_int_seq_is_int| "" (SKOLEM!)
  (("" (ASSERT)
    ((""
      (USE "prod_closure"
           ("P" "lambda x: rational_pred(x) AND integer_pred(x)"))
      (("1" (ASSERT) NIL NIL)
       ("2" (AUTO-REWRITE "closed_times")
        (("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|prod_posnat_seq_is_posnat| "" (SKOLEM!)
  (("" (USE* "prod_int_seq_is_int" "prod_posreal_seq_is_posreal")
    (("" (GROUND) NIL NIL)) NIL))
  NIL)
 (|prod_nzint_seq_is_nzint| "" (SKOLEM!)
  (("" (USE* "prod_int_seq_is_int" "prod_nzreal_seq_is_nzreal") NIL NIL)) NIL)
 (|prod_nat_seq_is_nat| "" (SKOLEM!)
  (("" (USE* "prod_int_seq_is_int" "prod_nnreal_seq_is_nnreal") NIL NIL)) NIL)
 (|prod_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|prod_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|prod_TCC3| "" (TERMINATION-TCC) NIL NIL)
 (|prod_TCC4| "" (SUBTYPE-TCC) NIL NIL)
 (|variant_prod_zero| "" (GRIND) NIL NIL)
 (|variant_prod_one_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|variant_prod_one| "" (GRIND) NIL NIL)
 (|variant_prod_two_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|variant_prod_two_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|variant_prod_two| "" (GRIND) NIL NIL)
 (|variant_prod_equiv| "" (INDUCT "n")
  (("1" (GRIND) NIL NIL)
   ("2" (SKOSIMP*)
    (("2" (CASE-REPLACE "j!1 = 0")
      (("1" (DELETE -) (("1" (GRIND) NIL NIL)) NIL)
       ("2" (AUTO-REWRITE "prod_step")
        (("2" (ASSERT)
          (("2" (EXPAND "prod" 2 1)
            (("2" (INST?)
              (("2"
                (CASE "prod(0, j!1 - 1)((LAMBDA (i: nat): IF i < j!1 THEN a!1(i) ELSE 1 ENDIF)) = prod(0, j!1 - 1)(LAMBDA (i: nat): IF i < 1 + j!1 THEN a!1(i) ELSE 1 ENDIF)")
                (("1" (ASSERT) NIL NIL)
                 ("2" (DELETE -1 3)
                  (("2" (REWRITE "prod_same_elements") NIL NIL)) NIL)
                 ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|variant_prod_split| "" (INDUCT-AND-REWRITE "n" 1 "prod") NIL NIL)
 (|variant_prod_permutation| "" (SKOSIMP)
  (("" (REWRITE "variant_prod_equiv")
    (("" (REWRITE "variant_prod_equiv")
      (("" (USE "prod_permutation" ("n" "0" "m" "n!1"))
        (("" (GROUND)
          (("" (DELETE 2)
            (("" (USE "perm_equiv[real]")
              (("" (ASSERT)
                (("" (DELETE 2)
                  ((""
                    (INST +
                     "lambda (i: idx(0, n!1)): IF i<n!1 THEN h!1(i) ELSE n!1 ENDIF")
                    (("1" (GRIND :IF-MATCH NIL)
                      (("1" (INST? :WHERE +) (("1" (ASSERT) NIL NIL)) NIL))
                      NIL)
                     ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|variant_prod_cont| "" (INDUCT-AND-REWRITE "n" 1 "prod" "expt") NIL NIL)
 (|variant_prod_closure| "" (SKOLEM + ("Q!1" _ _))
  (("" (INDUCT-AND-REWRITE "n" 1 "prod")
    (("" (TYPEPRED "Q!1") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|variant_prod_positive| "" (INDUCT-AND-REWRITE "n" 1 "prod")
  (("" (REWRITE "pos_times_gt") NIL NIL)) NIL)
 (|variant_prod_negative| ""
  (AUTO-REWRITE "pos_times_gt" "neg_times_lt" "parity_zero")
  (("" (INDUCT "n")
    (("1" (AUTO-REWRITE "prod") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL))
      NIL)
     ("2" (SKOSIMP*)
      (("2" (REWRITE "incr_even" +)
        (("2" (REWRITE "odd_not_even" +)
          (("2" (EXPAND "prod" +)
            (("2" (GROUND)
              (("1" (INST?)
                (("1" (SPLIT -)
                  (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
                   ("2" (DELETE 2 3)
                    (("2" (SKOLEM!)
                      (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (INST?)
                (("2" (SPLIT -)
                  (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
                   ("2" (DELETE -1 2)
                    (("2" (SKOLEM!)
                      (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|variant_prod_negative1| "" (SKOSIMP)
  (("" (USE "variant_prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|variant_prod_negative2| "" (SKOSIMP)
  (("" (REWRITE "odd_not_even")
    (("" (USE "variant_prod_negative") (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|variant_prod_null| "" (INDUCT "n")
  (("1" (EXPAND "prod") (("1" (REDUCE) NIL NIL)) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "prod" +)
      (("2" (INST?) (("2" (GROUND) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|variant_prod_null2| "" (INDUCT-AND-REWRITE "n" 1 "prod")
  (("" (REWRITE "zero_times3" -) (("" (INST? 3) NIL NIL)) NIL)) NIL)
 (|varprod_posreal_seq| "" (SKOLEM!)
  (("" (USE "variant_prod_positive") (("" (REDUCE) NIL NIL)) NIL)) NIL)
 (|varprod_nzreal_seq| "" (SKOSIMP)
  (("" (REWRITE "variant_prod_null2")
    (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|varprod_nnreal_seq| "" (SKOLEM!)
  (("" (USE* "variant_prod_positive" "variant_prod_null")
    (("" (GROUND)
      (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|varprod_negreal_seq1| "" (SKOSIMP)
  (("" (USE "variant_prod_negative1") (("" (REDUCE) NIL NIL)) NIL)) NIL)
 (|varprod_negreal_seq2| "" (SKOLEM!)
  (("" (USE "variant_prod_negative2") (("" (REDUCE) NIL NIL)) NIL)) NIL)
 (|varprod_rat_seq| "" (AUTO-REWRITE "closed_times")
  (("" (SKOLEM!)
    (("" (REWRITE "variant_prod_closure")
      (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|varprod_posrat_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_nzrat_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_nnrat_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_negrat_seq1| "" (SKOLEM!)
  (("" (USE "varprod_negreal_seq1")
    (("" (SKOSIMP) (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL)
 (|varprod_negrat_seq2| "" (SKOLEM!)
  (("" (USE "varprod_negreal_seq2")
    (("" (SKOSIMP) (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL)
 (|varprod_int_seq| "" (AUTO-REWRITE "closed_times")
  (("" (SKOLEM!)
    ((""
      (USE "variant_prod_closure"
           ("Q" "lambda x: rational_pred(x) AND integer_pred(x)"))
      (("1" (GROUND) NIL NIL)
       ("2" (SKOSIMP)
        (("2" (GROUND) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|varprod_posint_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_nzint_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_nat_seq| "" (SUBTYPE-TCC) NIL NIL)
 (|varprod_negint_seq1| "" (SKOLEM!)
  (("" (USE "varprod_negreal_seq1")
    (("" (SKOSIMP) (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL)
 (|varprod_negint_seq2| "" (SKOLEM!)
  (("" (USE "varprod_negreal_seq2")
    (("" (SKOSIMP) (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL))


$$$common_divisor.pvs
common_divisor : THEORY

  BEGIN

  a, b: VAR nzint

  c, d, x: VAR posnat

  n, m: VAR int


  E(a, b) : (nonempty?[posnat]) = { x | EXISTS n, m: x = a * n + b * m }

  gcd(a, b): posnat = min(E(a, b))


  gcd_decomp: LEMMA  EXISTS n, m: gcd(a, b) = a * n + b * m

  gcd_commutes: LEMMA gcd(b, a) = gcd(a, b)

  gcd_divides1: LEMMA divides(gcd(a, b), a)

  gcd_divides2: LEMMA divides(gcd(a, b), b)

  greatest_common_divisor: LEMMA
     divides(x, a) AND divides(x, b) IMPLIES divides(x, gcd(a, b))


  gcd_def: LEMMA
     gcd(a, b) = d IFF (divides(d, a) AND divides(d, b) AND 
        (FORALL x: divides(x, a) AND divides(x, b) IMPLIES divides(x, d)))


  gcd_self: LEMMA gcd(c, c) = c

  gcd_opp1: LEMMA  gcd(-a, b) = gcd(a, b)

  gcd_opp2: LEMMA  gcd(a, -b) = gcd(a, b)

  gcd_one1: LEMMA  gcd(1, a) = 1

  gcd_one2: LEMMA  gcd(a, 1) = 1

  gcd_rule1: LEMMA  a + b * x /= 0 IMPLIES gcd(a + b * x, b) = gcd(a, b)

  gcd_rule2: LEMMA  b + a * x /= 0 IMPLIES gcd(a, b + a * x) = gcd(a, b)

  gcd_multiple1: LEMMA gcd(c * a, c) = c

  gcd_multiple2: LEMMA gcd(c, c * a) = c

  gcd_multiple3: LEMMA gcd(c, b) = c IFF divides(c, b)

  gcd_multiple4: LEMMA gcd(a, c) = c IFF divides(c, a)

  gcd_bound1: LEMMA gcd(c, b) <= c

  gcd_bound2: LEMMA gcd(a, c) <= c

  END common_divisor

$$$common_divisor.prf
(|common_divisor|
 (E_TCC1 "" (GRIND :IF-MATCH NIL)
  (("" (CASE "a!1 < 0")
    (("1" (INST - "- a!1")
      (("1" (INST + "-1" "0") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT) NIL NIL))
      NIL)
     ("2" (INST - "a!1")
      (("1" (INST + "1" "0") (("1" (ASSERT) NIL NIL)) NIL)
       ("2" (ASSERT) NIL NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_decomp| "" (SKOLEM!)
  (("" (EXPAND "gcd")
    (("" (TYPEPRED "min(E(a!1, b!1))")
      (("" (EXPAND "E" -2 1) (("" (PROPAX) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|gcd_commutes| "" (SKOLEM!)
  (("" (EXPAND "gcd")
    (("" (CASE-REPLACE "E(b!1, a!1) = E(a!1, b!1)")
      (("" (APPLY-EXTENSIONALITY :HIDE? T)
        (("" (GRIND :IF-MATCH NIL)
          (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_divides1| "" (SKOLEM!)
  (("" (LEMMA "euclid_int" ("n" "a!1" "b" "gcd(a!1, b!1)"))
    (("" (SKOLEM!)
      (("" (CASE-REPLACE "r!1 = 0")
        (("1" (EXPAND "divides") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
          NIL)
         ("2" (DELETE 2)
          (("2" (ASSERT)
            (("2" (CASE "E(a!1, b!1)(r!1)")
              (("1" (TYPEPRED "r!1")
                (("1" (DELETE -3 1)
                  (("1" (EXPAND "gcd")
                    (("1" (TYPEPRED "min(E(a!1, b!1))")
                      (("1" (INST? :WHERE -5) (("1" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (USE "gcd_decomp")
                (("2" (SKOLEM!)
                  (("2" (REPLACE -1)
                    (("2" (EXPAND "E")
                      (("2" (INST + "1 - n!1 * q!1" "-m!1 * q!1")
                        (("2" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_divides2| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_divides1") NIL NIL)) NIL))
  NIL)
 (|greatest_common_divisor| "" (SKOSIMP)
  (("" (AUTO-REWRITE "divides_sum" "divides_prod1" "divides_prod2")
    (("" (USE "gcd_decomp")
      (("" (SKOLEM!) (("" (REPLACE*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|gcd_def| "" (SKOLEM!)
  (("" (AUTO-REWRITE "gcd_divides1" "gcd_divides2" "mutual_divisors_nat")
    (("" (LEMMA "greatest_common_divisor" ("a" "a!1" "b" "b!1"))
      (("" (GROUND)
        (("1" (REPLACE -1 + RL) (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (REPLACE -1 + RL) (("2" (ASSERT) NIL NIL)) NIL)
         ("3" (REPLACE*) NIL NIL)
         ("4" (INST - "gcd(a!1, b!1)")
          (("4" (INST - "d!1") (("4" (ASSERT) (("4" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_self| "" (SKOLEM!)
  (("" (AUTO-REWRITE "divides_reflexive")
    (("" (REWRITE "gcd_def") (("" (SKOSIMP) NIL NIL)) NIL)) NIL))
  NIL)
 (|gcd_opp1| ""
  (AUTO-REWRITE "opposite_divides" "divides_opposite" "gcd_divides1"
                "gcd_divides2" "greatest_common_divisor")
  (("" (SKOLEM!)
    (("" (REWRITE "gcd_def") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_opp2| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes")
    (("" (REWRITE "gcd_opp1") (("" (REWRITE "gcd_commutes") NIL NIL)) NIL))
    NIL))
  NIL)
 (|gcd_one1| "" (AUTO-REWRITE "one_divides" "one_div_one" "gcd_def")
  (("" (SKOLEM!) (("" (ASSERT) (("" (SKOSIMP) NIL NIL)) NIL)) NIL)) NIL)
 (|gcd_one2| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_one1") NIL NIL)) NIL)) NIL)
 (|gcd_rule1| ""
  (AUTO-REWRITE "gcd_divides1" "gcd_divides2" "divides_sum" "divides_prod1"
                "divides_prod2")
  (("" (SKOSIMP)
    (("" (ASSERT)
      (("" (REWRITE "gcd_def")
        (("" (SKOSIMP)
          (("" (USE "gcd_decomp")
            (("" (SKOLEM!)
              (("" (REPLACE*)
                (("" (CASE "divides(x!2, (b!1 * x!1 + a!1) - b!1 * x!1)")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (REWRITE "divides_diff") (("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_rule2| "" (SKOSIMP)
  (("" (NAME-REPLACE "d!1" "gcd(a!1, b!1)" :HIDE? NIL)
    (("" (REWRITE "gcd_commutes" +)
      (("" (USE "gcd_rule1")
        (("" (REWRITE "gcd_commutes" -2) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_multiple1| ""
  (AUTO-REWRITE "divides_reflexive" "divides_prod1" "divides_prod2" "gcd_def")
  (("" (SKOLEM!) (("" (ASSERT) (("" (SKOSIMP) NIL NIL)) NIL)) NIL)) NIL)
 (|gcd_multiple2| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_multiple1") NIL NIL)) NIL))
  NIL)
 (|gcd_multiple3| "" (AUTO-REWRITE "divides_reflexive")
  (("" (SKOLEM!)
    (("" (REWRITE "gcd_def") (("" (GROUND) (("" (SKOSIMP) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|gcd_multiple4| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_multiple3") NIL NIL)) NIL))
  NIL)
 (|gcd_bound1| "" (SKOLEM!)
  (("" (USE "gcd_divides1")
    (("" (FORWARD-CHAIN "divisor_smaller") (("" (ASSERT) NIL NIL)) NIL)) NIL))
  NIL)
 (|gcd_bound2| "" (SKOLEM!)
  (("" (REWRITE "gcd_commutes") (("" (REWRITE "gcd_bound1") NIL NIL)) NIL))
  NIL))


$$$mutual_primes.pvs
mutual_primes : THEORY

  BEGIN

  IMPORTING common_divisor

  a, b, c: VAR nzint

  d: VAR posnat

  n, m: VAR int


  prime(a, b): bool = gcd(a, b) = 1

  mutual_primes_commutes: LEMMA  prime(a, b) IFF prime(b, a)

  mutual_primes_equiv: LEMMA
      prime(a, b) IFF EXISTS n, m: a * n + b * m = 1

  common_div_of_primes: LEMMA
      prime(a, b) AND divides(d, a) AND divides(d, b) IMPLIES d=1

  mutual_primes_equiv2: LEMMA
      prime(a, b) IFF (FORALL d: divides(d, a) AND divides(d, b) IMPLIES d=1)

  divides_prod_prime1: LEMMA
      divides(c, a * b) AND prime(a, c) IMPLIES divides(c, b)

  divides_prod_prime2: LEMMA
      divides(c, a * b) AND prime(b, c) IMPLIES divides(c, a)

  common_multiple_primes: LEMMA
      divides(a, c) AND divides(b, c) AND prime(a, b) 
          IMPLIES divides(a * b, c)  

  mutual_prime_prod: LEMMA
      prime(a * b, c) IFF prime(a, c) AND prime(b, c)


  prime_with_one: LEMMA  prime(1, a)

  prime_with_one2: LEMMA  prime(a, 1)

  END mutual_primes


$$$mutual_primes.prf
(|mutual_primes|
 (|mutual_primes_commutes| "" (SKOLEM!)
  (("" (EXPAND "prime") (("" (REWRITE "gcd_commutes") (("" (ASSERT) NIL)))))))
 (|mutual_primes_equiv| "" (SKOLEM!)
  (("" (EXPAND "prime")
    (("" (GROUND)
      (("1" (USE "gcd_decomp")
        (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL)))))))
       ("2" (REWRITE "gcd_def")
        (("2"
          (AUTO-REWRITE "one_divides" "divides_sum" "divides_prod1"
                        "divides_prod2")
          (("2" (ASSERT)
            (("2" (SKOSIMP*)
              (("2" (CASE "divides(x!1, a!1 * n!1 + b!1 * m!1)")
                (("1" (ASSERT) NIL)
                 ("2" (ASSERT) (("2" (ASSERT) NIL)))))))))))))))))))
 (|common_div_of_primes| "" (AUTO-REWRITE "prime" "one_div_one")
  (("" (SKOSIMP)
    (("" (USE "greatest_common_divisor" ("b" "b!1"))
      (("" (ASSERT) (("" (REPLACE*) (("" (ASSERT) NIL)))))))))))
 (|mutual_primes_equiv2| ""
  (AUTO-REWRITE "one_divides" "prime" "gcd_def" "one_div_one")
  (("" (SKOLEM!) (("" (ASSERT) NIL)))))
 (|divides_prod_prime1| ""
  (AUTO-REWRITE "mutual_primes_equiv" "divides_sum" "divides_diff"
                "divides_prod1" "divides_prod2" "divides_reflexive")
  (("" (SKOSIMP)
    (("" (ASSERT)
      (("" (SKOLEM!)
        (("" (CASE "divides(c!1, b!1 * (a!1 * n!1 + c!1 * m!1))")
          (("1" (REPLACE*) NIL) ("2" (ASSERT) NIL)))))))))))
 (|divides_prod_prime2| "" (SKOSIMP)
  (("" (USE "divides_prod_prime1" ("a" "b!1" "b" "a!1"))
    (("" (ASSERT) NIL)))))
 (|common_multiple_primes| "" (SKOSIMP)
  (("" (EXPAND "divides" -1)
    (("" (SKOLEM!)
      (("" (REPLACE*)
        (("" (ASSERT)
          (("" (FORWARD-CHAIN "divides_prod_prime1")
            (("" (REWRITE "divides_prod_elim1") NIL)))))))))))))
 (|mutual_prime_prod| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (AUTO-REWRITE "mutual_primes_equiv")
      (("1" (ASSERT)
        (("1" (SKOLEM!)
          (("1" (INST + "n!1 * b!1" "m!1") (("1" (ASSERT) NIL)))))))))
     ("2" (AUTO-REWRITE "mutual_primes_equiv")
      (("2" (ASSERT)
        (("2" (SKOLEM!)
          (("2" (INST + "n!1 * a!1" "m!1") (("2" (ASSERT) NIL)))))))))
     ("3" (REWRITE "mutual_primes_equiv2" +)
      (("3" (SKOSIMP)
        (("3" (CASE "prime(a!1, d!1)")
          (("1" (FORWARD-CHAIN "divides_prod_prime1")
            (("1" (FORWARD-CHAIN "common_div_of_primes") NIL)))
           ("2" (EXPAND "prime" +)
            (("2" (DELETE -2 -3)
              (("2" (AUTO-REWRITE "gcd_divides1" "gcd_divides2")
                (("2" (USE "common_div_of_primes" ("d" "gcd(a!1, d!1)"))
                  (("2" (ASSERT)
                    (("2" (USE "divides_transitive" ("m" "d!1"))
                      (("2" (ASSERT) NIL)))))))))))))))))))))))
 (|prime_with_one| "" (SKOLEM!)
  (("" (REWRITE "mutual_primes_equiv")
    (("" (INST + "1" "0") (("" (ASSERT) NIL)))))))
 (|prime_with_one2| "" (SKOLEM!)
  (("" (REWRITE "mutual_primes_commutes")
    (("" (REWRITE "prime_with_one") NIL))))))

$$$prime_numbers.pvs
prime_numbers : THEORY

  BEGIN

  IMPORTING mutual_primes

  a: VAR nzint

  x, d: VAR posnat

  i, n: VAR nat



  %--------------------------------------
  %  Definition and first prime numbers
  %--------------------------------------

  prime(x): bool =
     x /= 1 AND FORALL d: divides(d, x) IMPLIES d=x OR d=1

  two_is_prime: LEMMA prime(2)

  three_is_prime: LEMMA prime(3)  

  smallest_prime: LEMMA prime(x) IMPLIES 2 <= x


  %-------------------------
  %  Type of prime numbers
  %-------------------------

  prime_nat: NONEMPTY_TYPE = { x | 2 <= x AND prime(x) }

  p, q: VAR prime_nat

  

  %-----------------
  %  Simple lemmas
  %-----------------

  divisors_of_prime: LEMMA divides(d, p) IFF d=p OR d=1

  gcd_with_prime: LEMMA gcd(a, p) = 1 OR gcd(a, p) = p

  non_multiple_of_prime: LEMMA divides(p, a) OR prime(p, a)

  smaller_than_prime: LEMMA x < p IMPLIES prime(x, p)

  distinct_primes: LEMMA p /= q IMPLIES prime(p, q)


  %--------------------------------------------
  %  There are infinitely many prime numbers
  %--------------------------------------------

  IMPORTING products

  prime_divisor: LEMMA
     FORALL n: 2 <= n IMPLIES EXISTS p: divides(p, n)

  factorial(x): posnat = prod(1, x)(lambda i: i)

  divisor_factorial: LEMMA
     d <= x IMPLIES divides(d, factorial(x))  

  unbounded_primes: LEMMA FORALL x: EXISTS p: x < p

  END prime_numbers


$$$prime_numbers.prf
(|prime_numbers|
 (|two_is_prime| (:NEW-GROUND? T) "" (EXPAND "prime")
  (("" (SKOSIMP)
    (("" (FORWARD-CHAIN "divisor_smaller")
      (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|three_is_prime| (:NEW-GROUND? T) "" (EXPAND "prime")
  (("" (SKOSIMP)
    (("" (FORWARD-CHAIN "divisor_smaller")
      (("1" (ASSERT) NIL NIL)
       ("2" (CASE-REPLACE "d!1=2")
        (("1" (EXPAND "divides")
          (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|smallest_prime| (:NEW-GROUND? T) "" (GRIND) NIL NIL)
 (|prime_nat_TCC1| (:NEW-GROUND? T) "" (INST + "2")
  (("" (REWRITE "two_is_prime") NIL NIL)) NIL)
 (|divisors_of_prime| (:NEW-GROUND? T) ""
  (AUTO-REWRITE "divides_reflexive" "one_divides" "prime")
  (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REDUCE) NIL NIL)) NIL)) NIL))
  NIL)
 (|gcd_with_prime| (:NEW-GROUND? T) "" (SKOSIMP)
  (("" (USE "gcd_divides2")
    (("" (REWRITE "divisors_of_prime") (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL)
 (|non_multiple_of_prime| (:NEW-GROUND? T) "" (SKOSIMP)
  (("" (AUTO-REWRITE "gcd_multiple4" "prime")
    (("" (LEMMA "gcd_with_prime" ("a" "a!1" "p" "p!1"))
      (("" (GROUND) (("" (REWRITE "gcd_commutes") NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|smaller_than_prime| (:NEW-GROUND? T) "" (SKOSIMP)
  (("" (REWRITE "mutual_primes_commutes")
    (("" (USE "non_multiple_of_prime")
      (("" (ASSERT)
        (("" (FORWARD-CHAIN "divisor_smaller")
          (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|distinct_primes| (:NEW-GROUND? T) "" (SKOSIMP)
  (("" (USE "non_multiple_of_prime")
    (("" (ASSERT) (("" (REWRITE "divisors_of_prime") NIL NIL)) NIL)) NIL))
  NIL)
 (|prime_divisor| (:NEW-GROUND? T) "" (INDUCT "n" :NAME "NAT_induction")
  (("" (SKOSIMP)
    (("" (AUTO-REWRITE "divides_reflexive")
      (("" (ASSERT)
        (("" (CASE "prime(j!1)")
          (("1" (INST? +) (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (EXPAND "prime")
            (("2" (SKOSIMP)
              (("2" (FORWARD-CHAIN "divisor_smaller")
                (("1" (ASSERT) NIL NIL)
                 ("2" (INST - "d!1")
                  (("2" (ASSERT)
                    (("2" (SKOLEM!)
                      (("2" (INST + "p!1")
                        (("2" (FORWARD-CHAIN "divides_transitive") NIL NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|factorial_TCC1| (:NEW-GROUND? T) "" (SUBTYPE-TCC) NIL NIL)
 (|factorial_TCC2| (:NEW-GROUND? T) "" (SKOLEM!)
  (("" (REWRITE "prod_positive") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|divisor_factorial| (:NEW-GROUND? T) ""
  (CASE "FORALL d, n: d <= n+1  IMPLIES divides(d, factorial(n+1))")
  (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)
   ("2" (DELETE 2)
    (("2" (EXPAND "factorial")
      (("2" (NAME-REPLACE "u!1" "lambda i:i" :HIDE? NIL)
        (("2"
          (INDUCT-AND-REWRITE "n" 1 "prod_once" "prod_step" "divides_prod1"
           "divides_prod2" "divides_reflexive" "one_div_one")
          (("1" (REPLACE -2 + RL) (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (CASE-REPLACE "d!1 = u!1(2 + j!1)")
            (("1" (ASSERT) NIL NIL)
             ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL))
  NIL)
 (|unbounded_primes| (:NEW-GROUND? T) "" (SKOLEM!)
  (("" (USE "prime_divisor" ("n" "factorial(x!1) + 1"))
    (("" (GROUND)
      (("" (SKOLEM!)
        (("" (INST?)
          (("" (USE "divisor_factorial")
            (("" (ASSERT)
              ((""
                (USE "divides_diff"
                     ("n" "1 + factorial(x!1)" "m" "factorial(x!1)"))
                (("" (AUTO-REWRITE "one_div_one")
                  (("" (USE "smallest_prime") (("" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$fermat.pvs
fermat : THEORY

  BEGIN

  IMPORTING prime_numbers, product_modulo

  a : VAR posnat

  n : VAR {a | 2 <= a}

  i, j: VAR nat

  p: VAR prime_nat


  F(n): posnat = prod(1, n - 1)(lambda i: i)

  G(n, a): nat = prod(1, n - 1)(lambda i: rem(n)(a * i))



  %---------------------
  %  G(n, a) modulo n
  %---------------------

  decomp_G: LEMMA rem(n)(G(n, a)) = rem(n)(expt(a, n - 1) * F(n))


  %------------------------------------------------
  %  G(n, a) = F(n) if n and a are mutually prime
  %------------------------------------------------

  div_diff_mod: LEMMA
     FORALL (x, y: mod(n)): divides(n, x - y) IFF x= y

  aux_prop: LEMMA   prime(a, n) IMPLIES
     FORALL (x, y: mod(n)): rem(n)(a * x) = rem(n)(a * y) IFF x=y

  equal_products: LEMMA  prime(a, n) IMPLIES G(n, a) = F(n)


  %-------------------------------------
  %  (p - 1)! and p are mutually prime
  %-------------------------------------

  fact_prime: LEMMA prime(F(p), p)


  %--------------------------
  %  Fermat little theorem
  %--------------------------

  fermat_theorem1: LEMMA
     prime(a, p) IMPLIES divides(p, expt(a, p - 1) - 1)

  fermat_theorem2: LEMMA
     prime(a, p) IMPLIES rem(p)(expt(a, p - 1)) = 1

  fermat_theorem3: LEMMA rem(p)(expt(a, p)) = rem(p)(a)

  END fermat

$$$fermat.prf
(|fermat| (F_TCC1 "" (SUBTYPE-TCC) NIL NIL)
 (F_TCC2 "" (AUTO-REWRITE "prod_rat_seq_is_rat" "prod_int_seq_is_int")
  (("" (SKOLEM!)
    (("" (ASSERT) (("" (USE "prod_positive") (("" (ASSERT) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (G_TCC1 ""
  (AUTO-REWRITE "prod_rat_seq_is_rat" "prod_int_seq_is_int"
                "prod_nat_seq_is_nat")
  (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|decomp_G_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|decomp_G| "" (SKOLEM!)
  (("" (EXPAND "G")
    (("" (ASSERT)
      (("" (AUTO-REWRITE "prod_rat_seq_is_rat" "prod_int_seq_is_int")
        ((""
          (CASE-REPLACE
           "rem(n!1)(prod(1, n!1 - 1)(LAMBDA (i: nat): rem(n!1)(a!1 * i))) = rem(n!1)(prod(1, n!1 -1)(lambda i: a!1 * i))")
          (("1" (REWRITE "prod_split2")
            (("1" (REWRITE "F" :DIR RL)
              (("1" (USE "prod_const" ("m" "n!1 - 2"))
                (("1" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("2" (DELETE 2)
            (("2" (REWRITE "equivalent_product")
              (("2" (AUTO-REWRITE "rem_rem")
                (("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|div_diff_mod| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (CASE "x!1 > y!1")
      (("1" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL NIL)
       ("2" (REWRITE "divides_opposite" :DIR RL)
        (("2" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) NIL
          NIL))
        NIL))
      NIL)
     ("2" (AUTO-REWRITE "divides_zero")
      (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|aux_prop| "" (SKOSIMP*)
  (("" (GROUND)
    (("" (REWRITE "same_remainder")
      (("" (USE "divides_prod_prime1" ("b" "x!1 - y!1"))
        (("" (ASSERT) (("" (REWRITE "div_diff_mod") NIL NIL)) NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|equal_products| "" (SKOSIMP)
  (("" (EXPAND* "G" "F")
    (("" (ASSERT)
      (("" (USE "prod_permutation" ("m" "n!1 - 2"))
        (("" (GROUND)
          (("" (DELETE 2)
            (("" (USE "perm_equiv[real]" ("m" "n!1 - 2"))
              (("" (ASSERT)
                (("" (DELETE 2)
                  (("" (FORWARD-CHAIN "aux_prop")
                    ((""
                      (INST +
                       "lambda (i: idx(1, n!1 - 1)): rem(n!1)(a!1 * i)")
                      (("1" (GROUND)
                        (("1" (EXPAND "injective?")
                          (("1" (SKOSIMP)
                            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                          NIL))
                        NIL)
                       ("2" (SKOLEM!)
                        (("2" (INST - "0" "i!1")
                          (("2" (AUTO-REWRITE "rem_zero")
                            (("2" (ASSERT) (("2" (GROUND) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|fact_prime_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|fact_prime| "" (SKOLEM!)
  (("" (EXPAND "F")
    (("" (NAME-REPLACE "u!1" "lambda i: i" :HIDE? NIL)
      ((""
        (CASE "FORALL (j: nat): j <= p!1 - 2 IMPLIES prod(1, 1 + j)(u!1) > 0 AND prime(prod(1, 1 + j)(u!1), p!1)")
        (("1" (INST - "p!1-2") (("1" (ASSERT) NIL NIL)) NIL)
         ("2" (DELETE 2)
          (("2"
            (INDUCT-AND-REWRITE "j" 1 "prod_once" "prod_step" "pos_times_gt"
             "smaller_than_prime")
            (("1" (REPLACE -2 + RL) (("1" (ASSERT) NIL NIL)) NIL)
             ("2" (REPLACE -2 + RL) (("2" (ASSERT) NIL NIL)) NIL)
             ("3" (REWRITE "mutual_prime_prod")
              (("1" (REPLACE -4 + RL) (("1" (ASSERT) NIL NIL)) NIL)
               ("2" (REPLACE -4 + RL) (("2" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("4" (REPLACE -4 + RL) (("4" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL)
         ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|fermat_theorem1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|fermat_theorem1| ""
  (AUTO-REWRITE "fact_prime" "equal_products" "fact_prime_TCC1")
  (("" (SKOSIMP)
    (("" (USE "decomp_G" ("n" "p!1"))
      (("" (ASSERT)
        (("" (ASSERT)
          (("" (REWRITE "same_remainder")
            ((""
              (USE "divides_prod_prime1"
                   ("a" "F(p!1)" "b" "1 - expt(a!1, p!1 - 1)"))
              (("1" (ASSERT)
                (("1" (REWRITE "divides_opposite" :DIR RL +) NIL NIL)) NIL)
               ("2" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|fermat_theorem2| "" (AUTO-REWRITE "rem_one")
  (("" (SKOSIMP :PREDS? T)
    (("" (GROUND)
      (("" (DELETE -1 -2 -3 1)
        (("" (FORWARD-CHAIN "fermat_theorem1")
          (("" (REWRITE "same_remainder" :DIR RL) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|fermat_theorem3| "" (SKOLEM!)
  (("" (USE "non_multiple_of_prime" ("p" "p!1" "a" "a!1"))
    (("" (GROUND)
      (("1" (REWRITE "rem_expt1" :DIR RL)
        (("1" (AUTO-REWRITE "expt" "zero_times1" "rem_zero")
          (("1" (CASE-REPLACE "rem(p!1)(a!1) = 0")
            (("1" (ASSERT) NIL NIL) ("2" (REWRITE "rem_def2") NIL NIL)) NIL))
          NIL))
        NIL)
       ("2" (REWRITE "mutual_primes_commutes")
        (("2" (EXPAND "expt")
          (("2" (REWRITE "rem_prod2" :DIR RL)
            (("2" (REWRITE "fermat_theorem2") (("2" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))