%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:42) $$$newtop.pvs newtop : THEORY BEGIN IMPORTING fermat, prime_decomposition, chinese_remainder END newtop $$$posnat_induction.pvs posnat_induction : THEORY BEGIN n, m: VAR posnat P: VAR [posnat -> bool] posnat_induction: PROPOSITION P(1) AND (FORALL n: P(n) => P(n+1)) IMPLIES (FORALL n: P(n)) END posnat_induction $$$posnat_induction.prf (|posnat_induction| (|posnat_induction| "" (SKOSIMP) (("" (CASE "FORALL (i: nat): P!1(i+1)") (("1" (SKOLEM!) (("1" (INST - "n!1 - 1") (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (INDUCT "i") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (INST - "j!1+1") (("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))) $$$chinese_remainder.pvs chinese_remainder : THEORY BEGIN IMPORTING inverse_modulo, posnat_induction, products p, q: VAR nzint p1, q1: VAR posnat a, b, x, y: VAR int %------------------ % Simple version %------------------ chinese_remainder1: LEMMA prime(p, q) IMPLIES EXISTS x: divides(p, x - a) AND divides(q, x - b) chinese_remainder2: LEMMA prime(p1, q1) IMPLIES EXISTS x: rem(p1)(x) = rem(p1)(a) AND rem(q1)(x) = rem(q1)(b) chinese_remainder3: LEMMA prime(p1, q1) IMPLIES FORALL (a : mod(p1)), (b: mod(q1)): EXISTS (x: mod(p1 * q1)): rem(p1)(x) = a AND rem(q1)(x) = b equal_remainders: LEMMA prime(p1, q1) IMPLIES (rem(p1 * q1)(x) = rem(p1 * q1)(y) IFF rem(p1)(x) = rem(p1)(y) AND rem(q1)(x) = rem(q1)(y)) %--------------------------------------------- % Same property with p(0)...p(n-1) numbers %--------------------------------------------- n: VAR posnat mutual_primes(n): TYPE = { x: [below(n) -> posnat] | FORALL (i, j: below(n)): i /= j => prime(x(i), x(j)) } chinese_remainder0: PROPOSITION FORALL n, (p: mutual_primes(n)), (a: [below(n) -> int]): EXISTS (x: mod(prod(n)(p))): FORALL (i: below(n)): rem(p(i))(x) = rem(p(i))(a(i)) chinese_remainder: PROPOSITION FORALL n, (p: mutual_primes(n)), (a: [i:below(n) -> mod(p(i))]): EXISTS (x: mod(prod(n)(p))): FORALL (i: below(n)): rem(p(i))(x) = a(i) prime_partial_product: LEMMA FORALL n, (p: mutual_primes(n)): prime(prod(n-1)(lambda (i: below(n-1)): p(i)), p(n-1)) equal_remainders2: PROPOSITION FORALL n, (p: mutual_primes(n)): rem(prod(n)(p))(x) = rem(prod(n)(p))(y) IFF (FORALL (i: below(n)): rem(p(i))(x) = rem(p(i))(y)) END chinese_remainder $$$chinese_remainder.prf (chinese_remainder (chinese_remainder1 0 (chinese_remainder1-1 nil 3236363025 3236364181 ("" (skosimp) (("" (rewrite "mutual_primes_equiv") (("" (skolem!) (("" (case "divides(p!1, q!1 * m!1 - 1) AND divides(q!1, p!1 * n!1 - 1)") (("1" (ground) (("1" (name-replace "AA" "q!1 * m!1 - 1" :hide? nil) (("1" (name-replace "BB" "p!1 * n!1 - 1" :hide? nil) (("1" (auto-rewrite "divides_reflexive" "divides_prod1" "divides_prod2" "divides_sum") (("1" (inst + "a!1 * q!1 * m!1 + b!1 * p!1 * n!1") (("1" (split) (("1" (case-replace "a!1 * m!1 * q!1 - a!1 + b!1 * n!1 * p!1 = a!1 * AA + b!1 * n!1 * p!1") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (replace -2 + rl) (("2" (assert) nil nil)) nil)) nil) ("2" (case-replace "a!1 * m!1 * q!1 - b!1 + b!1 * n!1 * p!1 = a!1 * m!1 * q!1 + b!1 * BB") (("1" (assert) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (expand "divides") (("2" (ground) (("1" (inst + "-n!1") (("1" (assert) nil nil)) nil) ("2" (inst + "-m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (mutual_primes_equiv formula-decl nil mutual_primes nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) nil nil nil (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (divides_reflexive formula-decl nil divides nil) (divides_prod2 formula-decl nil divides nil) (divides_sum formula-decl nil divides nil) nil nil) 2693 2470 nil nil)) (chinese_remainder2 0 (chinese_remainder2-1 nil 3236363025 3243292366 ("" (skosimp) (("" (rewrite "mutual_primes_equiv") (("" (skolem!) (("" (auto-rewrite "rem_multiple1" "rem_multiple2" "rem_rem" "rem_zero") (("" (inst + "a!1 * (q1!1 * m!1) + b!1 * (p1!1 * n!1)") (("" (split) (("1" (case-replace "q1!1 * m!1 = 1 - p1!1 * n!1") (("1" (assert) (("1" (rewrite "rem_sum2" :dir rl) (("1" (rewrite "rem_sum2" :dir rl) (("1" (rewrite "rem_diff2" :dir rl) (("1" (rewrite "associative_mult") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (case-replace "p1!1 * n!1 = 1 - q1!1 * m!1") (("1" (assert) (("1" (rewrite "rem_sum2" :dir rl) (("1" (rewrite "rem_sum2" :dir rl) (("1" (rewrite "rem_diff2" :dir rl) (("1" (rewrite "associative_mult") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((mutual_primes_equiv formula-decl nil mutual_primes 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) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (associative_mult formula-decl nil number_fields nil) (rem_rem formula-decl nil modulo_arithmetic nil) (rem_multiple2 formula-decl nil modulo_arithmetic nil) (rem_diff2 formula-decl nil modulo_arithmetic nil) (rem_sum2 formula-decl nil modulo_arithmetic nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) 214666 8790 t nil)) (chinese_remainder3 0 (chinese_remainder3-1 nil 3236363025 3236364187 ("" (skosimp*) (("" (auto-rewrite "rem_mod") (("" (use "chinese_remainder2" ("a" "a!1" "b" "b!1")) (("" (ground) (("" (skosimp) (("" (name "y!1" "rem(p1!1 * q1!1)(x!1)") (("" (inst + "y!1") (("" (auto-rewrite "rem_def") (("" (ground) (("1" (delete -3 -4) (("1" (skosimp*) (("1" (inst + "q!2 - q!1 * q1!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (delete -2 -4) (("2" (skosimp*) (("2" (inst + "q!2 - q!1 * p1!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-incomplete ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (rem_mod formula-decl nil modulo_arithmetic nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) nil nil (= const-decl "[T, T -> boolean]" equalities nil) nil (rem_def formula-decl nil modulo_arithmetic nil) (mod nonempty-type-eq-decl nil euclidean_division 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) (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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (chinese_remainder2 formula-decl nil chinese_remainder nil)) 2335 2120 nil nil)) (equal_remainders 0 (equal_remainders-1 nil 3236363025 3236364188 ("" (skosimp) (("" (auto-rewrite "same_remainder" "divides_zero" "common_multiple_primes") (("" (ground) (("1" (expand "divides") (("1" (skolem!) (("1" (inst + "x!2 * q1!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "divides") (("2" (skolem!) (("2" (inst + "x!2 * p1!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (case-replace "x!1 - y!1 = 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) proved-complete ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) nil (common_multiple_primes formula-decl nil mutual_primes nil) (divides_zero formula-decl nil divides nil) nil (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) nil (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (same_remainder formula-decl nil modulo_arithmetic nil)) 1468 1350 nil nil)) (chinese_remainder0 0 (chinese_remainder0-1 nil 3236363025 3236364197 ("" (auto-rewrite "rem_mod" "rem_rem" "mutual_prime_prod") (("" (induct "n" :name "posnat_induction") (("1" (skosimp*) (("1" (inst + "rem(p!1(0))(a!1(0))") (("1" (skolem!) (("1" (assert) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "variant_prod_one") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "p!1") (("2" (inst-cp - "n!1" "n!1-1") (("2" (assert) (("2" (use "chinese_remainder2" ("a" "a!1(n!1)" "b" "a!1(n!1-1)")) (("2" (assert) (("2" (skosimp) (("2" (assert) (("2" (inst -5 "lambda (i: below(n!1)): IF i boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (prime const-decl "bool" mutual_primes nil) (mutual_primes type-eq-decl nil chinese_remainder nil) (prod def-decl "real" products nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (= const-decl "[T, T -> boolean]" equalities nil) nil nil (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (posnat_induction formula-decl nil posnat_induction nil) nil nil (rem_mod formula-decl nil modulo_arithmetic nil) (variant_prod_one formula-decl nil products nil) (NOT const-decl "[bool -> bool]" booleans nil) (mutual_prime_prod formula-decl nil mutual_primes nil) (mutual_primes_commutes formula-decl nil mutual_primes nil) nil (OR const-decl "[bool, bool -> bool]" booleans nil) (equal_remainders formula-decl nil chinese_remainder nil) nil (IF const-decl "[boolean, T, T -> T]" if_def nil) nil (chinese_remainder2 formula-decl nil chinese_remainder nil) (AND const-decl "[bool, bool -> bool]" booleans nil) nil) 8955 8150 nil nil)) (chinese_remainder 0 (chinese_remainder-1 nil 3236363025 3236364204 ("" (auto-rewrite "rem_mod" "mutual_prime_prod") (("" (induct "n" :name "posnat_induction") (("1" (skosimp*) (("1" (inst + "a!1(0)") (("1" (skolem!) (("1" (assert) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "variant_prod_one") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "p!1") (("2" (use "chinese_remainder3" ("p1" "p!1(n!1)" "q1" "p!1(n!1-1)")) (("2" (inst-cp -2 "n!1" "n!1-1") (("2" (ground) (("2" (inst - "a!1(n!1)" "a!1(n!1-1)") (("2" (skosimp) (("2" (assert) (("2" (inst -5 "lambda (i: below(n!1)): IF i boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (prime const-decl "bool" mutual_primes nil) (mutual_primes type-eq-decl nil chinese_remainder nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (prod def-decl "real" products nil) (= const-decl "[T, T -> boolean]" equalities nil) nil nil (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) (posnat_induction formula-decl nil posnat_induction nil) nil nil (rem_mod formula-decl nil modulo_arithmetic nil) (variant_prod_one formula-decl nil products nil) (NOT const-decl "[bool -> bool]" booleans nil) (mutual_prime_prod formula-decl nil mutual_primes nil) (mutual_primes_commutes formula-decl nil mutual_primes nil) nil (OR const-decl "[bool, bool -> bool]" booleans nil) (equal_remainders formula-decl nil chinese_remainder nil) nil nil nil (IF const-decl "[boolean, T, T -> T]" if_def nil) nil (chinese_remainder3 formula-decl nil chinese_remainder nil) nil (AND const-decl "[bool, bool -> bool]" booleans nil)) 6610 5790 nil nil)) (prime_partial_product_TCC1 0 (prime_partial_product_TCC1-1 nil 3236363025 3236364204 ("" (subtype-tcc) nil nil) proved-complete nil 51 50 nil nil)) (prime_partial_product_TCC2 0 (prime_partial_product_TCC2-1 nil 3236363025 3236364204 ("" (subtype-tcc) nil nil) proved-complete nil 119 30 nil nil)) (prime_partial_product_TCC3 0 (prime_partial_product_TCC3-1 nil 3236363025 3236364204 ("" (auto-rewrite "varprod_rat_seq" "varprod_int_seq" "variant_prod_null2") (("" (reduce) nil nil)) nil) proved-complete nil 38 40 nil nil)) (prime_partial_product 0 (prime_partial_product-1 nil 3236363025 3236364207 ("" (induct "n" :name "posnat_induction") (("1" (auto-rewrite "variant_prod_zero" "prime_with_one" "prime_with_one2") (("1" (skolem!) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "prod" +) (("2" (rewrite "mutual_prime_prod") (("2" (ground) (("1" (inst - "lambda (i: below(n!1)): IF i numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (mutual_prime_prod formula-decl nil mutual_primes nil) nil nil (IF const-decl "[boolean, T, T -> T]" if_def nil) nil (NOT const-decl "[bool -> bool]" booleans nil) (variant_prod_zero formula-decl nil products nil) (prime_with_one formula-decl nil mutual_primes nil) (posnat_induction formula-decl nil posnat_induction nil) nil (prod def-decl "real" products nil) (mutual_primes type-eq-decl nil chinese_remainder nil) (prime const-decl "bool" mutual_primes nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_field -> boolean]" reals nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 2792 2440 nil nil)) (equal_remainders2 0 (equal_remainders2-1 nil 3236363025 3236364214 ("" (auto-rewrite "varprod_rat_seq" "varprod_int_seq" "varprod_nat_seq") (("" (skolem + ("x!1" "y!1" _ _)) (("" (induct "n" :name "posnat_induction") (("1" (auto-rewrite "variant_prod_one") (("1" (skolem!) (("1" (ground) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "prod" +) (("2" (inst?) (("1" (use "equal_remainders" ("q1" "p!1(n!1)")) (("1" (use "prime_partial_product" ("n" "n!1+1")) (("1" (assert) (("1" (replace*) (("1" (delete -) (("1" (apply (then (reduce :if-match nil) (inst? :polarity? t))) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (typepred "p!1") (("2" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) nil nil (prime_partial_product formula-decl nil chinese_remainder nil) (NOT const-decl "[bool -> bool]" booleans nil) (equal_remainders formula-decl nil chinese_remainder nil) (variant_prod_one formula-decl nil products nil) (posnat_induction formula-decl nil posnat_induction nil) (prod def-decl "real" products nil) (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}" modulo_arithmetic nil) nil nil (mod nonempty-type-eq-decl nil euclidean_division nil) (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (mutual_primes type-eq-decl nil chinese_remainder nil) (prime const-decl "bool" mutual_primes nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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_field -> boolean]" reals nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 7132 6410 nil nil))) $$$bags.pvs bags [T: TYPE] : THEORY %------------------------------------------------------------------------ % % Fundamental definitions and properties of bags. % % Author: Rick Butler NASA Langley % % (everything not useful for inductive bags has been removed) %------------------------------------------------------------------------ BEGIN x,y,t: VAR T bag: NONEMPTY_TYPE = [T -> nat] a,b,c: VAR bag n: VAR nat insert(x,b) : bag = (LAMBDA t: IF x = t THEN b(t) + 1 ELSE b(t) ENDIF) purge(x,b) : bag = (LAMBDA t: IF x = t THEN 0 ELSE b(t) ENDIF) delete(x,b,n) : bag = (LAMBDA t: IF x = t THEN IF b(t) >= n THEN b(t) - n ELSE 0 ENDIF ELSE b(t) ENDIF) plus(a,b) : bag = (LAMBDA t: a(t) + b(t)) union(a,b) : bag = (LAMBDA t: max(a(t),b(t))) intersection(a,b): bag = (LAMBDA t: min(a(t),b(t))) % --------- some predicates over bags ------------ member(x,b) : bool = b(x) > 0 empty?(b) : bool = (FORALL x: b(x) = 0) nonempty_bag?(b) : bool = NOT empty?(b) eqmult(x,a,b) : bool = (a(x) = b(x)) subbag?(a,b) : bool = (FORALL x: a(x) <= b(x)) proper_subbag?(a,b): bool = subbag?(a, b) AND a /= b disjoint?(a, b) : bool = empty?(intersection(a, b)) END bags $$$bags.prf (|bags| (|delete_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|delete_TCC2| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL)) $$$inductive_bags.pvs inductive_bags [T : TYPE] : THEORY BEGIN IMPORTING bags S, U, V: VAR bag[T] x, y, z: VAR T i, j, n, m: VAR nat %------------------------------------- % Finite bags: inductive definition %------------------------------------- indbag(S): INDUCTIVE bool = empty?(S) OR (EXISTS x, U: indbag(U) AND S = insert(x, U)) finite_bag: NONEMPTY_TYPE = (indbag) A, B, C: VAR finite_bag P, Q: VAR [finite_bag -> bool] emptybag: finite_bag = LAMBDA x: 0 finite_insert_bag: JUDGEMENT insert(x, A) HAS_TYPE finite_bag %---------------------------- % Basic properties of bags %---------------------------- emptybag_is_empty: LEMMA empty?(S) IFF S = emptybag subbag_emptybag: LEMMA subbag?(S, emptybag) IFF S = emptybag subbag_insert: LEMMA subbag?(insert(x, S), insert(x, U)) IFF subbag?(S, U) subbag_insert2: LEMMA subbag?(S, U) IMPLIES subbag?(S, insert(x, U)) subbag_insert3: LEMMA subbag?(insert(x, S), U) IMPLIES subbag?(S, U) insert_not_empty: LEMMA not insert(x, S) = emptybag insert_or_empty: LEMMA empty?(S) OR (EXISTS x, U: S = insert(x, U)) insert_exchange: LEMMA insert(x, insert(y, S)) = insert(y, insert(x, S)) equal_insert: LEMMA insert(x, S) = insert(y, U) IFF (x = y AND S = U) OR (EXISTS V: S = insert(y, V) AND U = insert(x, V)) remove_element: LEMMA S(x) > 0 IFF EXISTS U: S = insert(x, U) %---------------------------- % Variants for finite bags %---------------------------- insert_finite: LEMMA indbag(insert(x, S)) IFF indbag(S) equal_insert_finite: LEMMA insert(x, A) = insert(y, B) IFF (x = y AND A = B) OR (EXISTS C: A = insert(y, C) AND B = insert(x, C)) insert_or_empty_finite: LEMMA A = emptybag OR (EXISTS x, B: A = insert(x, B)) remove_element_finite: LEMMA A(x) > 0 IFF EXISTS B: A = insert(x, B) %----------------------------- % Induction for finite bags %----------------------------- bag_induction: PROPOSITION P(emptybag) AND (FORALL x, A: P(A) IMPLIES P(insert(x, A))) IMPLIES FORALL A: P(A) %------------------------------------------- % Closure under intersection, union, etc. %------------------------------------------- finite_bag_subbag: LEMMA subbag?(S, A) IMPLIES indbag(S) finite_bag_plus: JUDGEMENT plus(A, B) HAS_TYPE finite_bag finite_bag_union: JUDGEMENT union(A, B) HAS_TYPE finite_bag finite_bag_inter1: JUDGEMENT intersection(A, S) HAS_TYPE finite_bag finite_bag_inter2: JUDGEMENT intersection(S, A) HAS_TYPE finite_bag finite_bag_purge: JUDGEMENT purge(x, A) HAS_TYPE finite_bag finite_bag_delete: JUDGEMENT delete(x, A, n) HAS_TYPE finite_bag %------------- % Cardinal %------------- Card(A, n): INDUCTIVE bool = (A = emptybag AND n = 0) OR (EXISTS x, B, m: Card(B, m) AND A = insert(x, B) AND n = m + 1) Card_emptybag: LEMMA Card(emptybag, n) IFF n = 0 Card_insert: LEMMA Card(insert(x, A), n) IFF n > 0 AND Card(A, n-1) Card_unique: LEMMA Card(A, n) AND Card(A, m) IMPLIES n = m Card_total: LEMMA FORALL A: EXISTS n: Card(A, n) %--------------------- % derived function %--------------------- card(A): { n | Card(A, n) } card_def: LEMMA card(A) = n IFF Card(A, n) card_emptybag: LEMMA card(emptybag) = 0 card_zero: LEMMA card(A) = 0 IFF A = emptybag card_insert: LEMMA card(insert(x, A)) = card(A) + 1 card_positive: LEMMA card(A) > 0 IFF EXISTS x, B: A = insert(x, B) %----------------------------------- % Lemma for induction on cardinal %----------------------------------- card_induction: LEMMA (FORALL n, A: card(A) = n IMPLIES P(A)) IMPLIES (FORALL A: P(A)) END inductive_bags $$$inductive_bags.prf (|inductive_bags| (|finite_bag_TCC1| "" (INST + "LAMBDA x: 0") (("" (EXPAND "indbag") (("" (EXPAND "empty?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|emptybag_TCC1| "" (EXPAND* "indbag" "empty?") NIL NIL) (|finite_insert_bag| "" (SKOLEM!) (("" (EXPAND "indbag") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|emptybag_is_empty| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) NIL NIL)) NIL)) NIL) (|subbag_emptybag| "" (GRIND) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|subbag_insert| "" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) NIL NIL)) NIL) (|subbag_insert2| "" (GRIND) NIL NIL) (|subbag_insert3| "" (GRIND) NIL NIL) (|insert_not_empty| "" (SKOLEM!) (("" (REWRITE "emptybag_is_empty" :DIR RL) (("" (GRIND) NIL NIL)) NIL)) NIL) (|insert_or_empty| "" (GRIND :IF-MATCH NIL) (("" (INST + "x!1" "lambda y: IF y=x!1 THEN S!1(x!1)-1 ELSE S!1(y) ENDIF") (("" (APPLY-EXTENSIONALITY :HIDE? T :FNUM 2) (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|insert_exchange| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|equal_insert| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (CASE "x!1 = y!1") (("1" (DELETE 2) (("1" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (DELETE -3) (("1" (GRIND) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (DELETE 2) (("2" (INST + "lambda z: IF z=y!1 THEN U!1(z) ELSE S!1(z) ENDIF") (("2" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (GRIND) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "insert(x!1, S!1)(x!2) = insert(y!1, U!1)(x!2)") (("1" (GRIND) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) (("2" (SKOSIMP) (("2" (REPLACE*) (("2" (REWRITE "insert_exchange") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|remove_element| "" (GRIND :IF-MATCH NIL) (("" (INST + "lambda x: IF x=x!1 THEN S!1(x!1)-1 ELSE S!1(x) ENDIF") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|insert_finite| "" (SKOLEM!) (("" (GROUND) (("1" (LEMMA "indbag_induction" ("P" "lambda S: FORALL x, U: S=insert(x, U) IMPLIES indbag(U)")) (("1" (AUTO-REWRITE "emptybag_is_empty" "insert_not_empty") (("1" (GROUND) (("1" (REDUCE) NIL NIL) ("2" (DELETE -1 2) (("2" (REDUCE :IF-MATCH NIL) (("2" (REWRITE "equal_insert") (("2" (EXPAND "indbag" +) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST?) (("2" (INST + "x!3" "V!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "indbag" +) (("2" (GROUND) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|equal_insert_finite| "" (SKOLEM!) (("" (GROUND) (("1" (REWRITE "equal_insert") (("1" (SKOLEM!) (("1" (INST?) (("1" (USE "insert_finite") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "equal_insert") (("2" (SKOLEM!) (("2" (INST?) (("2" (USE "insert_finite") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (REPLACE*) (("3" (REWRITE "insert_exchange") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|insert_or_empty_finite| "" (SKOSIMP) (("" (AUTO-REWRITE "emptybag_is_empty") (("" (USE "insert_or_empty") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (USE "insert_finite") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|remove_element_finite| "" (SKOLEM!) (("" (REWRITE "remove_element") (("" (APPLY (THEN (GROUND) (SKOLEM!) (INST?))) (("" (USE "insert_finite") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|bag_induction| "" (SKOSIMP) (("" (LEMMA "indbag_induction" ("P" "LAMBDA S: indbag(S) AND P!1(S)")) (("" (GROUND) (("1" (SKOLEM!) (("1" (INST - "A!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (AUTO-REWRITE "emptybag_is_empty" "insert_not_empty") (("2" (SPLIT -) (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (INST?) (("2" (GROUND) (("2" (REPLACE*) (("2" (REWRITE "finite_insert_bag") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_subbag| "" (INDUCT "A" :NAME "bag_induction") (("1" (AUTO-REWRITE "subbag_emptybag") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (CASE "S!1(x!1) > 0") (("1" (REWRITE "remove_element") (("1" (AUTO-REWRITE "subbag_insert") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST - "U!1") (("1" (EXPAND "indbag" +) (("1" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 3) (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_plus| "" (SKOLEM 1 ("A!1" _)) (("" (INDUCT "B" :NAME "bag_induction") (("1" (CASE-REPLACE "plus(A!1, emptybag) = A!1") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (CASE-REPLACE "plus(A!1, insert(x!1, A!2)) = insert(x!1, plus(A!1, A!2))") (("1" (REWRITE "insert_finite") NIL NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_union| "" (SKOLEM!) (("" (AUTO-REWRITE "finite_bag_plus") (("" (USE "finite_bag_subbag" ("A" "plus(A!1, B!1)")) (("" (GROUND) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_inter1| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_inter2| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_purge| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|finite_bag_delete| "" (SKOLEM!) (("" (USE "finite_bag_subbag") (("" (ASSERT) (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|Card_emptybag| "" (SKOLEM!) (("" (EXPAND "Card") (("" (GROUND) (("" (SKOSIMP) (("" (USE "insert_not_empty") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Card_insert_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|Card_insert| "" (CASE "FORALL A, n, x: Card(insert(x, A), n) IMPLIES n > 0 AND Card(A, n-1)") (("1" (SKOLEM!) (("1" (REDUCE) (("1" (EXPAND "Card" +) (("1" (INST + "x!1" "A!1" "n!1-1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE "equal_insert_finite" "insert_not_empty") (("2" (INDUCT "n") (("1" (EXPAND "Card") (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (EXPAND "Card" -2) (("2" (REDUCE :POLARITY? T) (("2" (EXPAND "Card" +) (("2" (INST + "x!2" "C!1" "j!1 - 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (SKOSIMP) (("3" (ASSERT) NIL NIL)) NIL)) NIL) (|Card_unique| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (GROUND) (("2" (INST - "n!1 - 1" "m!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|Card_total| "" (AUTO-REWRITE "Card_emptybag" "Card_insert") (("" (INDUCT "A" :NAME "bag_induction") (("1" (INST + "0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST + "n!1+1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_TCC1| "" (INST + "lambda A: epsilon! n: Card(A, n)") (("" (SKOLEM!) (("" (USE "epsilon_ax[nat]") (("" (USE "Card_total") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|card_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "Card_unique") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|card_emptybag| "" (AUTO-REWRITE "card_def" "Card_emptybag") (("" (ASSERT) NIL NIL)) NIL) (|card_zero| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (REWRITE "card_emptybag") NIL NIL)) NIL)) NIL)) NIL) (|card_insert| "" (SKOLEM!) (("" (AUTO-REWRITE "card_def" "Card_insert") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|card_positive| "" (SKOLEM!) (("" (GROUND) (("1" (TYPEPRED "card(A!1)") (("1" (EXPAND "Card") (("1" (SKOSIMP) (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REPLACE*) (("2" (REWRITE "card_insert") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|card_induction| "" (REDUCE) NIL NIL)) $$$inductive_bag_functions.pvs inductive_bag_functions [ T, U: TYPE] : THEORY BEGIN IMPORTING inductive_bags[T] %----------------------------- % Recursion for finite bags %----------------------------- f: VAR [T, U -> U] a: VAR U x, y: VAR T exchange?(f): bool = FORALL x, y, a: f(x, f(y, a)) = f(y, f(x, a)) g: VAR (exchange?) %---------------------------------------------- % Choice function: pick an arbitrary element %---------------------------------------------- A: VAR finite_bag B: VAR { A | not empty?(A) } choose(B): { x | B(x) > 0 } rest(B): finite_bag = delete(choose(B)::T, B, 1) insert_choose: LEMMA insert(choose(B)::T, rest(B)) = B card_rest: LEMMA card(rest(B)) = card(B) - 1 recur(a, g)(A): RECURSIVE U = IF empty?(A) THEN a ELSE g(choose(A), recur(a, g)(rest(A))) ENDIF MEASURE card(A) %--------------------------- % The two essential rules %--------------------------- recur_emptybag: LEMMA recur(a, g)(emptybag) = a recur_insert: LEMMA recur(a, g)(insert(x, A)) = g(x, recur(a, g)(A)) END inductive_bag_functions $$$inductive_bag_functions.prf (|inductive_bag_functions| (|choose_TCC1| "" (INST + "lambda B: epsilon! x: B(x) > 0") (("1" (SKOLEM-TYPEPRED) (("1" (DELETE -1) (("1" (EXPAND "empty?") (("1" (SKOLEM!) (("1" (USE "epsilon_ax[T]") (("1" (GROUND) (("1" (INST + "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST + "x!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL) (|insert_choose| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|card_rest| "" (SKOSIMP) (("" (USE "card_insert" ("x" "choose(B!1)" "A" "rest(B!1)")) (("" (REWRITE "insert_choose") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|recur_TCC1| "" (AUTO-REWRITE "card_rest") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|recur_emptybag| "" (AUTO-REWRITE "recur" "emptybag_is_empty") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|recur_insert| "" (SKOLEM + (_ "a!1" "g!1" _)) (("" (MEASURE-INDUCT "card(A)" "A") (("" (SKOSIMP*) (("" (AUTO-REWRITE "card_insert" "insert_not_empty" "emptybag_is_empty") (("" (EXPAND "recur" 1 1) (("" (ASSERT) (("" (USE "insert_choose") (("" (NAME-REPLACE "zzz" "choose(insert(x!2, x!1))") (("" (NAME-REPLACE "yyy" "rest(insert(x!2, x!1))") (("" (REWRITE "equal_insert_finite") (("" (GROUND) (("" (SKOSIMP) (("" (REPLACE*) (("" (INST - "C!1") (("" (ASSERT) (("" (INST? :COPY? T) (("" (INST - "zzz") (("" (REPLACE*) (("" (TYPEPRED "g!1") (("" (EXPAND "exchange?") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$prime_decomposition.pvs prime_decomposition : THEORY BEGIN IMPORTING prime_numbers, inductive_bag_functions[prime_nat, posnat] n, i, j: VAR nat x, y, z: VAR posnat p, p1, p2, q: VAR prime_nat A, B: VAR finite_bag[prime_nat] %-------------------------------------------------- % prime decompositions = finite bags of primes %-------------------------------------------------- prod: [finite_bag[prime_nat] -> posnat] = recur(1, lambda p, x: p * x) product_emptybag: LEMMA prod(emptybag) = 1 product_insert: LEMMA prod(insert(p, A)) = p * prod(A) product_plus: LEMMA prod(plus(A, B)) = prod(A) * prod(B) product_one: LEMMA prod(A) = 1 IFF A = emptybag %-------------------------------------------- % Existence of a prime decomposition of x %-------------------------------------------- decomposition_exists: LEMMA FORALL x: EXISTS A: prod(A) = x %---------------- % Uniqueness %---------------- product_prime: LEMMA A(p)=0 IMPLIES prime(p, prod(A)) division_product: LEMMA divides(prod(A), prod(B)) IFF subbag?(A, B) unique_decomposition: LEMMA prod(A) = prod(B) IFF A = B %------------------------------------------- % Function: posnat -> prime decomposition %------------------------------------------- prime_fact(x): { A | prod(A) = x } factorisation_def: LEMMA prime_fact(x) = A IFF prod(A) = x factors_prod: LEMMA prime_fact(prod(A)) = A factorisation_one: LEMMA prime_fact(1) = emptybag factorisation_empty: LEMMA prime_fact(x) = emptybag IFF x = 1 factorisation_prime: LEMMA prime_fact(p) = insert(p, emptybag) factorisation_prod: LEMMA prime_fact(x * y) = plus(prime_fact(x), prime_fact(y)) factorisation_divides: LEMMA divides(x, y) IFF subbag?(prime_fact(x), prime_fact(y)) factorisation_gcd: LEMMA prime_fact(gcd(x, y)) = intersection(prime_fact(x), prime_fact(y)) factorisation_primes: LEMMA prime(x, y) IFF disjoint?(prime_fact(x), prime_fact(y)) END prime_decomposition $$$prime_decomposition.prf (|prime_decomposition| (|prod_TCC1| "" (GRIND) NIL NIL) (|product_emptybag| "" (AUTO-REWRITE "recur_emptybag" "prod" "prod_TCC1") (("" (ASSERT) NIL NIL)) NIL) (|product_insert| "" (AUTO-REWRITE "recur_insert" "prod" "prod_TCC1") (("" (ASSERT) NIL NIL)) NIL) (|product_plus| "" (SKOLEM + ("A!1" _)) (("" (AUTO-REWRITE "product_emptybag" "product_insert") (("" (INDUCT "B" :NAME "bag_induction") (("1" (CASE-REPLACE "plus(A!1, emptybag) = A!1") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (AUTO-REWRITE "plus" "emptybag") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) (("2" (CASE-REPLACE "plus(A!1, insert(x!1, A!2)) = insert(x!1, plus(A!1, A!2))") (("1" (ASSERT) NIL NIL) ("2" (AUTO-REWRITE "plus" "insert") (("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (CASE "x!2 = x!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|product_one| "" (SKOLEM!) (("" (AUTO-REWRITE "product_emptybag" "product_insert" "product_one") (("" (GROUND) (("1" (USE "insert_or_empty_finite") (("1" (ASSERT) (("1" (SKOLEM!) (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|decomposition_exists| "" (MEASURE-INDUCT "x-1" "x") (("" (SKOSIMP) (("" (AUTO-REWRITE "product_insert" "product_emptybag" "divides") (("" (USE "prime_divisor" ("n" "x!1")) (("" (GROUND) (("1" (SKOSIMP*) (("1" (USE "pos_times_lt") (("1" (ASSERT) (("1" (LEMMA "both_sides_times_pos_le1" ("pz" "x!2" "x" "2" "y" "p!1")) (("1" (ASSERT) (("1" (INST - "x!2") (("1" (GROUND) (("1" (SKOLEM!) (("1" (INST + "insert(p!1, A!1)") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "emptybag") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|product_prime| "" (AUTO-REWRITE "product_emptybag" "product_insert") (("" (SKOLEM + (_ "p!1")) (("" (INDUCT "A" :NAME "bag_induction") (("1" (GROUND) (("1" (AUTO-REWRITE "prime" "gcd_one1" "gcd_one2") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (GROUND) (("1" (REWRITE "mutual_primes_commutes" +) (("1" (REWRITE "mutual_primes_commutes" -) (("1" (REWRITE "mutual_prime_prod") (("1" (ASSERT) (("1" (REWRITE "distinct_primes" +) (("1" (EXPAND "insert") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "insert") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|division_product| "" (AUTO-REWRITE "product_emptybag" "product_insert" "product_one" "one_divides" "one_div_one" "subbag_emptybag" "subbag_insert" "subbag_insert2" "divides_prod_elim1" "divides_prod2") (("" (INDUCT "B" :NAME "bag_induction") (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (GROUND) (("1" (USE "product_prime" ("p" "x!1" "A" "A!2")) (("1" (GROUND) (("1" (USE "divides_prod_prime1") (("1" (REDUCE) NIL NIL)) NIL) ("2" (USE "remove_element_finite" ("A" "A!2")) (("2" (REDUCE :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "A!2(x!1) > 0") (("1" (REWRITE "remove_element_finite") (("1" (REDUCE :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST?) (("2" (GROUND) (("2" (DELETE 2 4) (("2" (GRIND :DEFS NIL :REWRITES ("subbag?" "insert") :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|unique_decomposition| "" (SKOLEM!) (("" (GROUND) (("" (AUTO-REWRITE "divides_reflexive") (("" (USE "division_product" ("A" "A!1" "B" "B!1")) (("" (USE "division_product" ("A" "B!1" "B" "A!1")) (("" (REPLACE*) (("" (ASSERT) (("" (DELETE -3) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prime_fact_TCC1| "" (INST + "lambda x: epsilon! A: prod(A) = x") (("" (SKOLEM!) (("" (USE "epsilon_ax[finite_bag[prime_nat]]") (("" (ASSERT) (("" (USE "decomposition_exists") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|factorisation_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "unique_decomposition") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|factors_prod| "" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "factorisation_def") NIL NIL)) NIL)) NIL) (|factorisation_one| "" (AUTO-REWRITE "factorisation_def" "product_one") (("" (ASSERT) NIL NIL)) NIL) (|factorisation_empty| "" (SKOLEM!) (("" (AUTO-REWRITE "factorisation_def" "product_emptybag") (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|factorisation_prime| "" (AUTO-REWRITE "product_insert" "product_emptybag" "factorisation_def") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|factorisation_prod| "" (AUTO-REWRITE "factorisation_def" "product_plus") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|factorisation_divides| "" (SKOLEM!) (("" (REWRITE "division_product" :DIR RL) (("" (GROUND) NIL NIL)) NIL)) NIL) (|factorisation_gcd| "" (SKOLEM!) (("" (NAME-REPLACE "zzz" "gcd(x!1, y!1)" :HIDE? NIL) (("" (REWRITE "gcd_def") (("" (AUTO-REWRITE "factorisation_divides" "factorisation_prime" "factors_prod") (("" (GROUND) (("" (NAME-REPLACE "AA" "prime_fact(zzz)") (("" (NAME-REPLACE "BB" "prime_fact(x!1)") (("" (NAME-REPLACE "CC" "prime_fact(y!1)") (("" (INST - "prod(intersection(BB, CC))") (("" (ASSERT) (("" (AUTO-REWRITE "intersection" "subbag?") (("" (GROUND) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "min") (("1" (REDUCE) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL) ("3" (SKOLEM!) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|factorisation_primes| "" (SKOLEM!) (("" (EXPAND "prime") (("" (EXPAND "disjoint?") (("" (REWRITE "emptybag_is_empty") (("" (REWRITE "factorisation_gcd" :DIR RL) (("" (REWRITE "factorisation_empty") (("" (ASSERT) NIL NIL)) NIL)) 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))