| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/examples/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 245 B |
|
Quellcode-Bibliothek round.prf Sprache: Lisp |
|||||||||
|
(round (round_to_even0 0
(round_to_even0-1 nil 3507032123 ("" (grind) nil nil) ((round_to_even const-decl "integer" round nil) (nonneg_ceiling_is_nat application-judgement "nat" floor_ceil nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (round_to_even1 0 (round_to_even1-1 nil 3507032123 ("" (skosimp*) (("" (expand "abs") (("" (lift-if) (("" (prop) (("1" (expand "round_to_even") (("1" (lift-if) (("1" (ground) nil))))) ("2" (expand "round_to_even") (("2" (lift-if) (("2" (ground) nil)))))))))))) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (round_to_even const-decl "integer" round nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (round_to_even2 0 (round_to_even2-1 nil 3507032123 ("" (skosimp*) (("" (expand "abs") (("" (lift-if) (("" (prop) (("1" (expand "round_to_even") (("1" (lift-if) (("1" (ground) (("1" (expand "integer?") (("1" (propax) nil))))))))) ("2" (expand "round_to_even") (("2" (lift-if) (("2" (ground) (("2" (expand "integer?") (("2" (propax) nil)))))))))))))))) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (integer? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (round_to_even const-decl "integer" round nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (round1 0 (round1-1 nil 3507032123 ("" (skosimp*) (("" (expand "round") (("" (lift-if) (("" (prop) (("1" (lemma "round_to_even1") (("1" (inst?) (("1" (assert) nil))))) ("2" (grind) nil) ("3" (grind) nil) ("4" (grind) nil)))))))) nil) ((nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (round const-decl "integer" round 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (round_to_even1 formula-decl nil round nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (round_int 0 (round_int-1 nil 3507032123 ("" (skosimp*) (("" (expand "round") (("" (lift-if) (("" (ground) (("1" (expand "round_to_even") (("1" (lift-if) (("1" (ground) nil))))) ("2" (expand "abs") (("2" (lift-if) (("2" (expand "sgn") (("2" (ground) nil)))))))))))))) nil) ((round const-decl "integer" round nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (round_to_even const-decl "integer" round nil) (minus_int_is_int application-judgement "int" integers nil) (sgn const-decl "int" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) nil))) ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.13Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28