%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:42) $$$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| "" (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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (REWRITE "rem_def2") NIL NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL) ("2" (REWRITE "rem_def2") NIL NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 2) (("2" (USE "pos_times_le" ("x" "m" "y" "q!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 0 (rem_inverse-1 nil 3236363025 3236364000 ("" (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 :if-match nil) (("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) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_pred const-decl "[number -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (rem_zero formula-decl nil modulo_arithmetic nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (rem_def formula-decl nil modulo_arithmetic nil) (- const-decl "[real -> real]" reals nil) (mutual_primes_equiv formula-decl nil mutual_primes nil)) 311296 22120 t nil)) (rem_inverse2 0 (rem_inverse2-1 nil 3236363025 nil ("" (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) proved-incomplete ((rem_prod2 formula-decl nil modulo_arithmetic nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (+ const-decl "[real, real -> real]" reals nil) (* const-decl "[real, real -> real]" reals nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (rem_zero formula-decl nil modulo_arithmetic nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number -> boolean]" reals nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rem_inverse formula-decl nil inverse_modulo nil)) nil nil nil nil))) $$$product_modulo.pvs product_modulo : THEORY BEGIN IMPORTING products, mutual_primes 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)) equivalent_varprod: LEMMA FORALL (a, b: [below(n) -> nat]): (FORALL (i: below(n)): rem(p)(a(i)) = rem(p)(b(i))) IMPLIES rem(p)(prod(n)(a)) = rem(p)(prod(n)(b)) nz: VAR [nat -> nzint] x : VAR nzint mutual_prime_product: LEMMA n <= m IMPLIES (prime(prod(n, m)(nz), x) IFF FORALL (i: idx(n, m)): prime(nz(i), x)) mutual_prime_varprod: LEMMA FORALL (a: [below(n) -> nzint]): prime(prod(n)(a), x) IFF FORALL (i: below(n)): prime(a(i), x) END product_modulo $$$product_modulo.prf (|product_modulo| (|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) (|equivalent_varprod| "" (AUTO-REWRITE "prod") (("" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (REDUCE :IF-MATCH NIL) (("2" (REWRITE "rem_prod") (("1" (DELETE 2) (("1" (REDUCE :POLARITY? T) NIL NIL)) NIL) ("2" (INST? -4) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|mutual_prime_product| "" (SKOSIMP) (("" (ASSERT) (("" (CASE "FORALL (j: nat): j <= m!1 - n!1 IMPLIES (prime(prod(n!1, n!1+j)(nz!1), x!1) IFF FORALL (i: upto(j)): prime(nz!1(n!1 + i), x!1))") (("1" (INST - "m!1 - n!1") (("1" (ASSERT) (("1" (REPLACE*) (("1" (DELETE -1) (("1" (REDUCE :IF-MATCH NIL) (("1" (INST - "i!1 - n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "prod_once" "prod_step" "mutual_prime_prod") (("2" (INDUCT "j") (("1" (REDUCE) NIL NIL) ("2" (REDUCE :IF-MATCH NIL) (("1" (INST? :POLARITY? T) NIL NIL) ("2" (INST? -5) NIL NIL) ("3" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|mutual_prime_varprod| "" (AUTO-REWRITE "prod" "mutual_prime_prod" "prime_with_one") (("" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) (("2" (REPLACE*) (("2" (DELETE -) (("2" (REDUCE :POLARITY? T) NIL NIL)) NIL)) NIL)) 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_props2.pvs nat_fun_props2: THEORY BEGIN n, m: VAR nat injection_n_to_m: THEOREM (EXISTS (f: [below(n) -> below(m)]): injective?(f)) IMPLIES n <= m injection_n_to_m_var: THEOREM (EXISTS (f: [below(n) -> below(m)]): injective?(f)) IFF n <= m surjection_n_to_m: THEOREM (EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IMPLIES m <= n surjection_n_to_m_var: THEOREM (EXISTS (f: [below(n) -> below(m)]): surjective?(f)) IFF (m > 0 AND m <= n) OR (m = 0 AND n = 0) 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_props2 $$$nat_fun_props2.prf (|nat_fun_props2| (|injection_n_to_m| "" (INDUCT "n") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP*) (("2" (TYPEPRED "f!1(0)") (("2" (ASSERT) (("2" (INST - "m!1 - 1") (("2" (GROUND) (("2" (DELETE -1 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" (INST-CP - "x1!1" "j!1") (("1" (INST-CP - "x2!1" "j!1") (("1" (INST - "x1!1" "x2!1") (("1" (SMASH) 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) (|injection_n_to_m_var| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "injection_n_to_m") NIL NIL) ("2" (INST + "lambda (i: below(n!1)): i") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m| "" (SKOSIMP*) (("" (ASSERT) (("" (REWRITE "injection_n_to_m") (("" (EXPAND "surjective?" -1) (("" (INST -1 "0") (("" (SKOSIMP) (("" (ASSERT) (("" (INST + "inverse(f!1)") (("1" (REWRITE "inj_inv") (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|surjection_n_to_m_var| "" (SKOLEM!) (("" (APPLY (THEN (SPLIT) (FLATTEN))) (("1" (FORWARD-CHAIN "surjection_n_to_m") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (TYPEPRED "f!1(0)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "lambda (i: below(n!1)): IF i < m!1 THEN i ELSE 0 ENDIF") (("1" (GRIND) NIL NIL) ("2" (REDUCE) 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") (("2" (GRIND) 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") (("2" (GRIND) 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" (SMASH) 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" (SMASH) 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" (SMASH) (("1" (INST + "x2!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) 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_props2, 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) 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| "" (GRIND :IF-MATCH ALL) 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] %% New PVS3.0 version (10/10/2002): * is not of type [real, real -> real] anymore binprod(x, y): real = x * y times_assoc_commutes: JUDGEMENT binprod HAS_TYPE { f | associative?(f) AND commutative?(f) } prod(n, (m | n <= m))(u): real = iter(binprod, 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_permutation2: LEMMA n <= m AND permutation(u, n, m, v, p, q) IMPLIES prod(n, m)(u) = prod(p, q)(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 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_const: 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 0 (times_assoc_commutes-1 nil 3243291761 3243291766 ("" (grind) nil nil) proved ((associative? const-decl "bool" operator_defs nil) (commutative? const-decl "bool" operator_defs nil) (binprod const-decl "real" products nil)) 116 100 nil nil)) (prod_once_TCC1 0 (prod_once_TCC1-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete nil nil nil nil nil)) (prod_once 0 (prod_once-1 nil 3243291761 3243291766 ("" (grind) nil nil) proved ((iter def-decl "T" iterations nil) (prod const-decl "real" products nil)) 21 20 nil nil)) (prod_step_TCC1 0 (prod_step_TCC1-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (prod_step 0 (prod_step-1 nil 3243291761 3243291824 ("" (auto-rewrite "prod" "iter_induct[real]" "mult" "binprod") (("" (skosimp) (("" (assert) nil nil)) nil)) nil) proved ((binprod const-decl "real" products nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (iter_induct formula-decl nil iterations nil) (prod const-decl "real" products nil)) 12227 780 t nil)) (prod_same_elements 0 (prod_same_elements-1 nil 3243291761 3243291766 ("" (expand "prod") (("" (skosimp) (("" (rewrite "iter_same_elements") (("" (delete 2) (("" (skosimp) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((idx type-eq-decl nil index_range nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (m!1 skolem-const-decl "nat" products nil) (i!1 skolem-const-decl "nat" products nil) (n!1 skolem-const-decl "nat" products nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (binprod const-decl "real" products nil) (iter_same_elements formula-decl nil iterations nil) (prod const-decl "real" products nil)) 139 110 nil nil)) (prod_split_TCC1 0 (prod_split_TCC1-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (prod_split_TCC2 0 (prod_split_TCC2-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (prod_split 0 (prod_split-1 nil 3243291761 3243291865 ("" (skosimp) (("" (expand "prod") (("" (use "iter_assoc_split[real]") (("" (expand "binprod") (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((prod const-decl "real" products nil) (bool nonempty-type-eq-decl nil booleans nil) (associative? const-decl "bool" operator_defs nil) (binprod const-decl "real" products nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (iter_assoc_split formula-decl nil iterations nil)) 30416 1400 t nil)) (prod_split2 0 (prod_split2-1 nil 3243291761 3243291894 ("" (skosimp) (("" (auto-rewrite "prod" "binprod") (("" (assert) (("" (use "iter_split" ("u" "u!1" "v" "v!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((iter_split formula-decl nil iterations nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (binprod const-decl "real" products nil) (commutative? const-decl "bool" operator_defs nil) (associative? const-decl "bool" operator_defs nil) (prod const-decl "real" products nil)) 18645 1200 t nil)) (prod_permutation_TCC1 0 (prod_permutation_TCC1-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete ((permutation const-decl "bool" iterations nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil)) nil nil nil nil)) (prod_permutation_TCC2 0 (prod_permutation_TCC2-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete ((permutation const-decl "bool" iterations nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil)) nil nil nil nil)) (prod_permutation 0 (prod_permutation-1 nil 3243291761 3243291767 ("" (skosimp) (("" (expand "prod") (("" (rewrite "iter_permutation") nil nil)) nil)) nil) proved ((prod const-decl "real" products nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (binprod const-decl "real" products nil) (commutative? const-decl "bool" operator_defs nil) (associative? const-decl "bool" operator_defs nil) (bool nonempty-type-eq-decl nil booleans nil) (iter_permutation formula-decl nil iterations nil)) 142 130 nil nil)) (prod_permutation2_TCC1 0 (prod_permutation2_TCC1-1 nil 3243291761 nil ("" (grind :if-match all) nil nil) proved-complete ((permutation const-decl "bool" iterations nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (idx type-eq-decl nil index_range nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (prod_permutation2 0 (prod_permutation2-1 nil 3243291761 3243291767 ("" (expand "prod") (("" (skosimp) (("" (rewrite "iter_permutation2") nil nil)) nil)) nil) proved ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (binprod const-decl "real" products nil) (commutative? const-decl "bool" operator_defs nil) (associative? const-decl "bool" operator_defs nil) (bool nonempty-type-eq-decl nil booleans nil) (iter_permutation2 formula-decl nil iterations nil) (prod const-decl "real" products nil)) 76 70 nil nil)) (prod_const_TCC1 0 (prod_const_TCC1-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete nil nil nil nil nil)) (prod_const 0 (prod_const-1 nil 3243291761 3243291767 ("" (skolem + (_ "n!1" "x!1")) (("" (induct-and-rewrite "m" 1 "prod_once" "prod_step" "expt") nil nil)) nil) proved ((prod_step formula-decl nil products nil) (prod_once formula-decl nil products nil) (nat_induction formula-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (prod const-decl "real" products nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 511 480 nil nil)) (prod_closure 0 (prod_closure-1 nil 3243291761 3243291768 ("" (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) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (prod const-decl "real" products nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (n!1 skolem-const-decl "nat" products nil) (m!1 skolem-const-decl "nat" products nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (prod_once formula-decl nil products nil) (idx type-eq-decl nil index_range nil) (prod_step formula-decl nil products nil) (NOT const-decl "[bool -> bool]" booleans nil)) 673 630 nil nil)) (prod_positive 0 (prod_positive-1 nil 3243291761 3243291769 ("" (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) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (prod const-decl "real" products nil) (> const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (n!1 skolem-const-decl "nat" products nil) (m!1 skolem-const-decl "nat" products nil) (pos_times_gt formula-decl nil real_props nil) (prod_step formula-decl nil products nil) (idx type-eq-decl nil index_range nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (prod_once formula-decl nil products nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil)) 561 500 nil nil)) (prod_negative 0 (prod_negative-1 nil 3243291761 3243291770 ("" (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) proved ((pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (prod_once formula-decl nil products nil) (idx type-eq-decl nil index_range nil) (incr_even formula-decl nil parity nil) (prod_step formula-decl nil products nil) (neg_times_lt formula-decl nil real_props nil) (pos_times_gt formula-decl nil real_props nil) (j!1 skolem-const-decl "nat" products nil) (n!1 skolem-const-decl "nat" products nil) (odd_not_even formula-decl nil parity nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (even? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (prod const-decl "real" products nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) 987 950 nil nil)) (prod_negative1 0 (prod_negative1-1 nil 3243291761 3243291770 ("" (skosimp) (("" (use "prod_negative") (("" (assert) nil nil)) nil)) nil) proved ((prod_negative formula-decl nil products nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 122 110 nil nil)) (prod_negative2 0 (prod_negative2-1 nil 3243291761 3243291770 ("" (skosimp) (("" (rewrite "odd_not_even") (("" (use "prod_negative") (("" (assert) nil nil)) nil)) nil)) nil) proved ((odd_not_even formula-decl nil parity nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (prod_negative formula-decl nil products nil)) 132 120 nil nil)) (prod_null 0 (prod_null-1 nil 3243291761 3243291978 ("" (skosimp*) (("" (expand "prod") (("" (assert) (("" (use "iter_swap_last[real]" ("i" "i!1")) (("" (assert) (("" (replace -1 + rl) (("" (delete -1) (("" (auto-rewrite "iter" "swap" "binprod") (("" (case "n!1 = m!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((prod const-decl "real" products nil) (iter_swap_last formula-decl nil iterations nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (idx type-eq-decl nil index_range nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (associative? const-decl "bool" operator_defs nil) (commutative? const-decl "bool" operator_defs nil) (binprod const-decl "real" products nil) (swap const-decl "T" iterations nil) (iter def-decl "T" iterations nil) (= const-decl "[T, T -> boolean]" equalities nil)) 42048 2270 t nil)) (prod_null2 0 (prod_null2-1 nil 3243291761 3243291770 ("" (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) proved ((idx type-eq-decl nil index_range nil) (<= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (prod_closure formula-decl nil products nil) (prod_null formula-decl nil products nil)) 211 190 nil nil)) (prod_posreal_seq_is_posreal 0 (prod_posreal_seq_is_posreal-1 nil 3243291761 nil ("" (skolem!) (("" (use "prod_positive") (("" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (delete 2) (("3" (reduce) nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((idx type-eq-decl nil index_range nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (prod_positive formula-decl nil products nil)) nil nil nil nil)) (prod_nzreal_seq_is_nzreal 0 (prod_nzreal_seq_is_nzreal-1 nil 3243291761 nil ("" (skosimp) (("" (rewrite "prod_null2") (("" (reduce) nil nil)) nil)) nil) proved-incomplete ((NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (idx type-eq-decl nil index_range nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (prod_null2 formula-decl nil products nil)) nil nil nil nil)) (prod_nnreal_seq_is_nnreal 0 (prod_nnreal_seq_is_nnreal-1 nil 3243291761 nil ("" (skosimp) (("" (use* "prod_positive" "prod_null") (("" (ground) (("" (skolem!) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved-incomplete ((idx type-eq-decl nil index_range nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (prod_null formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (prod_positive formula-decl nil products nil)) nil nil nil nil)) (prod_rat_seq_is_rat 0 (prod_rat_seq_is_rat-1 nil 3243291761 nil ("" (skolem!) (("" (auto-rewrite "rationals.closed_times") (("" (rewrite "prod_closure") (("" (skosimp) (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((prod_closure formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_times formula-decl nil rationals nil)) nil nil nil nil)) (prod_posrat_seq_is_posrat 0 (prod_posrat_seq_is_posrat-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_rat_seq_is_rat" "prod_posreal_seq_is_posreal") (("" (assert) nil nil)) nil)) nil) proved-incomplete ((posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (prod_posreal_seq_is_posreal subtype-tcc nil products nil) (rat nonempty-type-eq-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (> const-decl "bool" reals nil) (posrat nonempty-type-eq-decl nil rationals nil) (<= const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (prod_rat_seq_is_rat subtype-tcc nil products nil)) nil nil nil nil)) (prod_nzrat_seq_is_nzrat 0 (prod_nzrat_seq_is_nzrat-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_rat_seq_is_rat" "prod_nzreal_seq_is_nzreal") nil nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rat nonempty-type-eq-decl nil rationals nil) (/= const-decl "boolean" notequal nil) (nzrat nonempty-type-eq-decl nil rationals nil) (prod_nzreal_seq_is_nzreal subtype-tcc nil products nil) (nzreal nonempty-type-eq-decl nil reals nil) (<= const-decl "bool" reals nil) (prod_rat_seq_is_rat subtype-tcc nil products nil)) nil nil nil nil)) (prod_nnrat_seq_is_nnrat 0 (prod_nnrat_seq_is_nnrat-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_rat_seq_is_rat" "prod_nnreal_seq_is_nnreal") nil nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (rat nonempty-type-eq-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (prod_nnreal_seq_is_nnreal subtype-tcc nil products nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (prod_rat_seq_is_rat subtype-tcc nil products nil)) nil nil nil nil)) (prod_int_seq_is_int 0 (prod_int_seq_is_int-1 nil 3243291761 nil ("" (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) proved-incomplete ((prod_closure formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (closed_times formula-decl nil integers nil) (closed_times formula-decl nil rationals nil)) nil nil nil nil)) (prod_posnat_seq_is_posnat 0 (prod_posnat_seq_is_posnat-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_int_seq_is_int" "prod_posreal_seq_is_posreal") (("" (ground) nil nil)) nil)) nil) proved-incomplete ((nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (prod_posreal_seq_is_posreal subtype-tcc nil products nil) (<= const-decl "bool" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (prod_int_seq_is_int subtype-tcc nil products nil)) nil nil nil nil)) (prod_nzint_seq_is_nzint 0 (prod_nzint_seq_is_nzint-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_int_seq_is_int" "prod_nzreal_seq_is_nzreal") nil nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (prod_nzreal_seq_is_nzreal subtype-tcc nil products nil) (nzreal nonempty-type-eq-decl nil reals nil) (prod_int_seq_is_int subtype-tcc nil products nil)) nil nil nil nil)) (prod_nat_seq_is_nat 0 (prod_nat_seq_is_nat-1 nil 3243291761 nil ("" (skolem!) (("" (use* "prod_int_seq_is_int" "prod_nnreal_seq_is_nnreal") nil nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (prod_nnreal_seq_is_nnreal subtype-tcc nil products nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (prod_int_seq_is_int subtype-tcc nil products nil)) nil nil nil nil)) (prod_TCC1 0 (prod_TCC1-1 nil 3243291761 3243291770 ("" (subtype-tcc) nil nil) proved nil 43 40 nil nil)) (prod_TCC2 0 (prod_TCC2-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete nil nil nil nil nil)) (prod_TCC3 0 (prod_TCC3-1 nil 3243291761 nil ("" (termination-tcc) nil nil) proved-complete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (prod_TCC4 0 (prod_TCC4-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-complete nil nil nil nil nil)) (variant_prod_zero 0 (variant_prod_zero-1 nil 3243291761 3243291770 ("" (grind) nil nil) proved ((prod def-decl "real" products nil)) 34 30 nil nil)) (variant_prod_one 0 (variant_prod_one-1 nil 3243291761 3243291770 ("" (grind) nil nil) proved ((prod def-decl "real" products nil)) 43 40 nil nil)) (variant_prod_two 0 (variant_prod_two-1 nil 3243291761 3243291770 ("" (grind) nil nil) proved ((prod def-decl "real" products nil)) 61 60 nil nil)) (variant_prod_equiv 0 (variant_prod_equiv-1 nil 3243291761 3243291771 ("" (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) proved ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (prod_same_elements formula-decl nil products nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (prod_step formula-decl nil products nil) (binprod const-decl "real" products nil) (iter def-decl "T" iterations nil) (nat_induction formula-decl nil naturalnumbers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (prod const-decl "real" products nil) (<= const-decl "bool" reals nil) (prod def-decl "real" products nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 781 750 nil nil)) (variant_prod_split 0 (variant_prod_split-1 nil 3243291761 3243291772 ("" (induct-and-rewrite "n" 1 "prod") nil nil) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (prod def-decl "real" products nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) 814 760 nil nil)) (variant_prod_permutation 0 (variant_prod_permutation-1 nil 3243291761 3243291773 ("" (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 boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (prod_permutation formula-decl nil products nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (h!1 skolem-const-decl "[below(n!1) -> below(n!1)]" products nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (idx type-eq-decl nil index_range nil) (n!1 skolem-const-decl "nat" products nil) (<= const-decl "bool" reals nil) (injective? const-decl "bool" functions nil) (O const-decl "T3" function_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (perm_equiv formula-decl nil iterations nil)) 1357 1270 nil nil)) (variant_prod_const 0 (variant_prod_const-1 nil 3243291761 3243291774 ("" (induct-and-rewrite "n" 1 "prod" "expt") nil nil) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (prod def-decl "real" products nil) (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil)) 444 410 nil nil)) (variant_prod_closure 0 (variant_prod_closure-1 nil 3243291761 3243291774 ("" (skolem + ("Q!1" _ _)) (("" (induct-and-rewrite "n" 1 "prod") (("" (typepred "Q!1") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved ((nat_induction formula-decl nil naturalnumbers nil) (prod def-decl "real" products nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil)) 615 560 nil nil)) (variant_prod_positive 0 (variant_prod_positive-1 nil 3243291761 3243291775 ("" (induct-and-rewrite "n" 1 "prod") (("" (rewrite "pos_times_gt") nil nil)) nil) proved ((pos_times_gt formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (prod def-decl "real" products nil) (nat_induction formula-decl nil naturalnumbers nil)) 571 520 nil nil)) (variant_prod_negative 0 (variant_prod_negative-1 nil 3243291761 3243291776 ("" (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) proved ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (even? const-decl "bool" integers nil) (> const-decl "bool" reals nil) (prod def-decl "real" products nil) (nat_induction formula-decl nil naturalnumbers nil) (incr_even formula-decl nil parity nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (pos_times_gt formula-decl nil real_props nil) (neg_times_lt formula-decl nil real_props nil) (odd_not_even formula-decl nil parity nil)) 573 540 nil nil)) (variant_prod_negative1 0 (variant_prod_negative1-1 nil 3243291761 3243291776 ("" (skosimp) (("" (use "variant_prod_negative") (("" (assert) nil nil)) nil)) nil) proved ((variant_prod_negative formula-decl nil products nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 96 90 nil nil)) (variant_prod_negative2 0 (variant_prod_negative2-1 nil 3243291761 3243291776 ("" (skosimp) (("" (rewrite "odd_not_even") (("" (use "variant_prod_negative") (("" (assert) nil nil)) nil)) nil)) nil) proved ((odd_not_even formula-decl nil parity nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (variant_prod_negative formula-decl nil products nil)) 104 100 nil nil)) (variant_prod_null 0 (variant_prod_null-1 nil 3243291761 3243291776 ("" (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) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (prod def-decl "real" products nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 290 260 nil nil)) (variant_prod_null2 0 (variant_prod_null2-1 nil 3243291761 3243291777 ("" (induct "n") (("1" (grind) nil nil) ("2" (skosimp*) (("2" (expand "prod" +) (("2" (inst?) (("2" (ground) (("1" (skolem!) (("1" (inst?) nil nil)) nil) ("2" (rewrite "zero_times3") (("2" (inst?) nil nil)) nil) ("3" (skolem!) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (i!1 skolem-const-decl "below(1 + j!1)" products nil) (j!1 skolem-const-decl "nat" products nil) (zero_times3 formula-decl nil real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (prod def-decl "real" products nil) (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 503 460 nil nil)) (varprod_posreal_seq 0 (varprod_posreal_seq-1 nil 3243291761 nil ("" (skolem!) (("" (use "variant_prod_positive") (("" (reduce) nil nil)) nil)) nil) proved-incomplete ((NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (variant_prod_positive formula-decl nil products nil)) nil nil nil nil)) (varprod_nzreal_seq 0 (varprod_nzreal_seq-1 nil 3243291761 nil ("" (skosimp) (("" (rewrite "variant_prod_null2") (("" (skolem!) (("" (assert) nil nil)) nil)) nil)) nil) proved-incomplete ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (variant_prod_null2 formula-decl nil products nil)) nil nil nil nil)) (varprod_nnreal_seq 0 (varprod_nnreal_seq-1 nil 3243291761 nil ("" (skolem!) (("" (use* "variant_prod_positive" "variant_prod_null") (("" (ground) (("" (skolem!) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) proved-incomplete ((variant_prod_null formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (variant_prod_positive formula-decl nil products nil)) nil nil nil nil)) (varprod_negreal_seq1 0 (varprod_negreal_seq1-1 nil 3243291761 nil ("" (skosimp) (("" (use "variant_prod_negative1") (("" (reduce) nil nil)) nil)) nil) proved-incomplete ((NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (even? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (variant_prod_negative1 formula-decl nil products nil)) nil nil nil nil)) (varprod_negreal_seq2 0 (varprod_negreal_seq2-1 nil 3243291761 nil ("" (skolem!) (("" (use "variant_prod_negative2") (("" (reduce) nil nil)) nil)) nil) proved-incomplete ((NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (odd? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (variant_prod_negative2 formula-decl nil products nil)) nil nil nil nil)) (varprod_rat_seq 0 (varprod_rat_seq-1 nil 3243291761 nil ("" (auto-rewrite "closed_times") (("" (skolem!) (("" (rewrite "variant_prod_closure") (("" (skosimp) (("" (assert) nil nil)) nil)) nil)) nil)) nil) proved-incomplete ((variant_prod_closure formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_times formula-decl nil rationals nil)) nil nil nil nil)) (varprod_posrat_seq 0 (varprod_posrat_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_nzrat_seq 0 (varprod_nzrat_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_nnrat_seq 0 (varprod_nnrat_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_negrat_seq1 0 (varprod_negrat_seq1-1 nil 3243291761 nil ("" (skolem!) (("" (use "varprod_negreal_seq1") (("" (skosimp) (("" (ground) nil nil)) nil)) nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (even? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_rat nonempty-type-eq-decl nil rationals nil) (negrat nonempty-type-eq-decl nil rationals nil) (varprod_negreal_seq1 subtype-tcc nil products nil)) nil nil nil nil)) (varprod_negrat_seq2 0 (varprod_negrat_seq2-1 nil 3243291761 nil ("" (skolem!) (("" (use "varprod_negreal_seq2") (("" (skosimp) (("" (ground) nil nil)) nil)) nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (odd? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_rat nonempty-type-eq-decl nil rationals nil) (negrat nonempty-type-eq-decl nil rationals nil) (varprod_negreal_seq2 subtype-tcc nil products nil)) nil nil nil nil)) (varprod_int_seq 0 (varprod_int_seq-1 nil 3243291761 nil ("" (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) proved-incomplete ((variant_prod_closure formula-decl nil products nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (closed_times formula-decl nil rationals nil) (closed_times formula-decl nil integers nil)) nil nil nil nil)) (varprod_posint_seq 0 (varprod_posint_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_nzint_seq 0 (varprod_nzint_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_nat_seq 0 (varprod_nat_seq-1 nil 3243291761 nil ("" (subtype-tcc) nil nil) proved-incomplete ((nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil nil nil nil)) (varprod_negint_seq1 0 (varprod_negint_seq1-1 nil 3243291761 nil ("" (skolem!) (("" (use "varprod_negreal_seq1") (("" (skosimp) (("" (ground) nil nil)) nil)) nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (even? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_int nonempty-type-eq-decl nil integers nil) (negint nonempty-type-eq-decl nil integers nil) (varprod_negreal_seq1 subtype-tcc nil products nil)) nil nil nil nil)) (varprod_negint_seq2 0 (varprod_negint_seq2-1 nil 3243291761 nil ("" (skolem!) (("" (use "varprod_negreal_seq2") (("" (skosimp) (("" (ground) nil nil)) nil)) nil)) nil) proved-incomplete ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (odd? const-decl "bool" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_int nonempty-type-eq-decl nil integers nil) (negint nonempty-type-eq-decl nil integers nil) (varprod_negreal_seq2 subtype-tcc nil products 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) (("2" (ASSERT) (("2" (ASSERT :FLUSH? T) NIL NIL)) 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 NIL)) NIL)) NIL)) NIL) (|mutual_primes_equiv| "" (SKOLEM!) (("" (EXPAND "prime") (("" (GROUND) (("1" (USE "gcd_decomp") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) 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" (REPLACE*) NIL NIL) ("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|common_div_of_primes| "" (AUTO-REWRITE "prime" "one_div_one") (("" (SKOSIMP) (("" (USE "greatest_common_divisor" ("b" "b!1")) (("" (ASSERT) (("" (REPLACE*) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|mutual_primes_equiv2| "" (AUTO-REWRITE "one_divides" "prime" "gcd_def" "one_div_one") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) 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 NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|divides_prod_prime2| "" (SKOSIMP) (("" (USE "divides_prod_prime1" ("a" "b!1" "b" "a!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|common_multiple_primes| "" (SKOSIMP) (("" (EXPAND "divides" -1) (("" (SKOLEM!) (("" (REPLACE*) (("" (ASSERT) (("" (FORWARD-CHAIN "divides_prod_prime1") (("1" (REWRITE "divides_prod_elim1") NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL) ("2" (AUTO-REWRITE "mutual_primes_equiv") (("2" (ASSERT) (("2" (SKOLEM!) (("2" (INST + "n!1 * a!1" "m!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) 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 NIL)) 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 NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prime_with_one| "" (SKOLEM!) (("" (REWRITE "mutual_primes_equiv") (("" (INST + "1" "0") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|prime_with_one2| "" (SKOLEM!) (("" (REWRITE "mutual_primes_commutes") (("" (REWRITE "prime_with_one") NIL NIL)) NIL)) 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| "" (EXPAND "prime") (("" (SKOSIMP) (("" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|three_is_prime| "" (EXPAND "prime") (("" (SKOSIMP) (("" (FORWARD-CHAIN "divisor_smaller") (("1" (ASSERT) NIL NIL) ("2" (CASE-REPLACE "d!1=2") (("1" (EXPAND "divides") (("1" (PROPAX) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|smallest_prime| "" (GRIND) NIL NIL) (|prime_nat_TCC1| "" (INST + "2") (("" (REWRITE "two_is_prime") NIL NIL)) NIL) (|divisors_of_prime| "" (AUTO-REWRITE "divides_reflexive" "one_divides" "prime") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|gcd_with_prime| "" (SKOSIMP) (("" (USE "gcd_divides2") (("" (REWRITE "divisors_of_prime") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|non_multiple_of_prime| "" (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| "" (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| "" (SKOSIMP) (("" (USE "non_multiple_of_prime") (("" (ASSERT) (("" (REWRITE "divisors_of_prime") NIL NIL)) NIL)) NIL)) NIL) (|prime_divisor| "" (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| "" (SUBTYPE-TCC) NIL NIL) (|factorial_TCC2| "" (SKOLEM!) (("" (REWRITE "prod_positive") NIL NIL)) NIL) (|divisor_factorial| "" (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)) NIL) (|unbounded_primes| "" (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") (("" (ASSERT) 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 = factorial(n - 1) 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's 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) (G_TCC1 "" (SUBTYPE-TCC) NIL NIL) (|decomp_G_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|decomp_G| "" (SKOLEM!) (("" (EXPAND* "F" "G") (("" (ASSERT) (("" (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 "factorial" :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) (|div_diff_mod| "" (SKOLEM!) (("" (GROUND) (("1" (APPLY (THEN (FORWARD-CHAIN "divisor_smaller") (ASSERT))) (("1" (REWRITE "divides_opposite" :DIR RL) (("1" (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" "factorial") (("" (ASSERT) (("" (REWRITE "prod_permutation2") (("" (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" (SMASH) 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!) (("" (AUTO-REWRITE "smaller_than_prime" "prod_same_elements" "F" "factorial") (("" (CASE-REPLACE "F(p!1) = prod(1, p!1 - 1)(lambda i: IF i=0 THEN 1 ELSE i ENDIF)") (("1" (DELETE -) (("1" (REWRITE "mutual_prime_product") (("1" (SKOSIMP) NIL NIL)) NIL)) NIL) ("2" (ASSERT) 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 :FNUMS +) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|fermat_theorem2| "" (AUTO-REWRITE "rem_one") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (FORWARD-CHAIN "fermat_theorem1") (("" (REWRITE "same_remainder" :DIR RL) 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))