| products/Sources/formale Sprachen/PVS/ACCoRD/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: util.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(util
(eq_correct_1 0 (eq_correct_1-1 nil 3470478491 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "eq") (("1" (flatten) (("1" (mult-cases -1) (("1" (case-replace "sq(a) = sq(-a)") (("1" (case-replace "sq(e) = sq(-e)") (("1" (hide (-1 -2)) (("1" (case "sqrt(sq(-a)*b) = sqrt(sq(-e))") (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil) ("2" (replaces -3) nil nil)) nil)) nil) ("2" (rewrite "sq_neg") nil nil)) nil) ("2" (rewrite "sq_neg") nil nil)) nil) ("2" (case "sqrt(sq(a)*b) = sqrt(sq(e))") (("1" (rewrite "sqrt_times") (("1" (assert) nil nil)) nil) ("2" (replaces -3) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "eq") (("2" (copy -1) (("2" (both-sides-f -1 "sq") (("2" (rewrite "sq_times") (("2" (assert) (("2" (hide -1) (("2" (replaces -1 :dir rl) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq const-decl "bool" util nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (pos_times_ge formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_times formula-decl nil sqrt "reals/") (sq_neg formula-decl nil sq "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (neg_times_ge formula-decl nil real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_times formula-decl nil sq "reals/")) shostak)) (eq_neg 0 (eq_neg-1 nil 3470499696 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (eq const-decl "bool" util nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (gt_correct_1 0 (gt_correct_1-1 nil 3460570945 ("" (skeep) (("" (expand "gt") (("" (case "a>=0") (("1" (assert) (("1" (split 1) (("1" (flatten) (("1" (mult-by -2 "sqrt(b)") (("1" (case "e < 0") (("1" (assert) nil nil) ("2" (assert) (("2" (real-props) (("2" (both-sides-f 2 "sq") (("1" (rewrite "sq_times") nil nil) ("2" (rewrite "sq_gt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (both-sides-f -1 "sq") (("1" (rewrite "sq_times") nil nil) ("2" (rewrite "sq_gt") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split) (("1" (flatten) (("1" (neg-formula 1) (("1" (both-sides-f 1 "sq") (("1" (sq-simp) (("1" (assert) nil nil)) nil) ("2" (rewrite "sq_gt") nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "e < 0") (("1" (assert) (("1" (neg-formula -2) (("1" (both-sides-f -2 "sq") (("1" (sq-simp) (("1" (assert) nil nil)) nil) ("2" (rewrite "sq_gt") (("2" (neg-formula 1) (("2" (grind-reals) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (mult-by 2 "sqrt(b)") (("2" (real-props) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((gt const-decl "bool" util nil) (b skolem-const-decl "nnreal" util nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (neg_neg formula-decl nil extra_tegies 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) (both_sides_times_neg_ge1 formula-decl nil real_props nil) (neg_times_ge formula-decl nil real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_gt1 formula-decl nil real_props nil) (sq_neg formula-decl nil sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_le1_imp formula-decl nil extra_real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (mult_neg formula-decl nil extra_tegies nil) (neg_one_times formula-decl nil extra_tegies nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (pos_times_ge formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (sq_gt formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_times formula-decl nil sq "reals/") (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props 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) (>= const-decl "bool" reals nil)) shostak)) (lt_correct_1 0 (lt_correct_1-1 nil 3460645954 ("" (skeep) (("" (expand "lt") (("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil)) nil) ((lt const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gt_correct_1 formula-decl nil util nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (ge_correct_1 0 (ge_correct_1-1 nil 3460646107 ("" (skeep) (("" (expand "ge") (("" (rewrite "lt_correct_1") (("" (ground) nil nil)) nil)) nil)) nil) ((ge const-decl "bool" util nil) (real_ge_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) (real_times_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (lt_correct_1 formula-decl nil util nil)) shostak)) (le_correct_1 0 (le_correct_1-1 nil 3460646250 ("" (skeep) (("" (expand "le") (("" (rewrite "gt_correct_1") (("" (ground) nil nil)) nil)) nil)) nil) ((le const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (gt_correct_1 formula-decl nil util nil)) shostak)) (gt_correct_2 0 (gt_correct_2-1 nil 3460646699 ("" (skeep) (("" (expand "gt") (("" (rewrite "lt_correct_1") (("" (rewrite "lt_correct_1") (("" (rewrite "gt_correct_1") (("" (lemma "gt_correct_1") (("" (inst -1 "a" "b" "c*sqrt(d) + e") (("" (replaces -1 :dir rl) (("" (expand "gt") (("" (rewrite "sq_plus") (("" (rewrite "sq_times") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (gt const-decl "bool" util nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq_plus formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_times formula-decl nil sq "reals/") (gt const-decl "bool" util nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_correct_1 formula-decl nil util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (lt_correct_1 formula-decl nil util nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (lt_correct_2 0 (lt_correct_2-1 nil 3460648253 ("" (skeep) (("" (expand "lt") (("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (lt const-decl "bool" util nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (gt_correct_2 formula-decl nil util nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (ge_correct_2 0 (ge_correct_2-1 nil 3460648277 ("" (skeep) (("" (expand "ge") (("" (rewrite "lt_correct_2") (("" (ground) nil nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (ge const-decl "bool" util nil) (real_ge_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) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (lt_correct_2 formula-decl nil util nil)) shostak)) (le_correct_2 0 (le_correct_2-1 nil 3460648299 ("" (skeep) (("" (expand "le") (("" (rewrite "gt_correct_2") (("" (ground) nil nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (le const-decl "bool" util nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (gt_correct_2 formula-decl nil util nil)) shostak))) ¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
