%% PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 22, 2008 3:35) %% 8.1 [Linux (x86)] (Jul 22, 2008 3:35) $$$arithsquare.pvs arithsquare: THEORY BEGIN n: VAR nat x: VAR real f(n): RECURSIVE int = IF n = 0 THEN 0 ELSE f(n-1) + 2*n-1 ENDIF MEASURE n % The sum of subsequent odd numbers is a square f_square: LEMMA f(n) = n*n power(n, x): RECURSIVE real = IF n = 0 THEN 1 ELSE x * power(n-1, x) ENDIF MEASURE n % geometric series geoseries(n, x): RECURSIVE real = IF n = 0 THEN 0 ELSE geoseries(n-1, x) + power(n-1, x) ENDIF MEASURE n geoseries_val: LEMMA (x - 1) * geoseries(n, x) = power(n, x) - 1 % The sum of a geometric series geoseries_val_again: LEMMA x /= 1 IMPLIES geoseries(n, x) = (power(n, x) - 1)/(x-1) END arithsquare $$$arithsquare.prf (arithsquare (f_TCC1 0 (f_TCC1-1 nil 3499085950 nil ("" (subtype-tcc) nil nil) unchecked nil nil nil nil nil)) (f_TCC2 0 (f_TCC2-1 nil 3499085950 nil ("" (termination-tcc) nil nil) unchecked nil nil nil nil nil)) (f_square 0 (f_square-1 nil 3499085951 3499087809 ("" (induct "n") (("1" (expand "f") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (expand "f" +) (("2" (assert) nil nil)) nil)) nil)) nil) unchecked ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (f def-decl "int" arithsquare 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)) 1858318 180 t shostak)) (geoseries_val 0 (geoseries_val-1 nil 3499092847 3499092945 ("" (induct "n") (("1" (expand "geoseries") (("1" (expand "power") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "x!1") (("2" (expand "power" +) (("2" (expand "geoseries" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (power def-decl "real" arithsquare nil) (geoseries def-decl "real" arithsquare 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 "[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)) 98364 200 t shostak)) (geoseries_val_again_TCC1 0 (geoseries_val_again_TCC1-1 nil 3499093072 nil ("" (subtype-tcc) nil nil) unchecked nil nil nil nil nil)) (geoseries_val_again 0 (geoseries_val_again-1 nil 3499093073 3499093095 ("" (skosimp) (("" (use "geoseries_val") (("" (assert) nil nil)) nil)) nil) unchecked ((geoseries_val formula-decl nil arithsquare 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) 21735 60 t shostak)))