Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: gcd_fractions.prf Sprache: Lisp

Original von: PVS^©

(gcd_fractions
(div_by_gcd_prep_TCC1 0
  (div_by_gcd_prep_TCC1-1 nil 3453735869 ("" (subtype-tcc) nil nil) nil
   nil))
(div_by_gcd_prep 0
  (div_by_gcd_prep-1 nil 3453735879
   ("" (skosimp)
    (("" (case "p!1 / gcd(p!1, q!1) > 0")
      (("1" (assert)
        (("1" (typepred "gcd(p!1, q!1)")
          (("1" (hide -1 -3)
            (("1" (expand "divides")
              (("1" (skosimp)
                (("1" (div-by -1 "gcd(p!1, q!1)")
                  (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (rewrite "pos_div_gt")
          (("2" (typepred "gcd(p!1, q!1)") (("2" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd
         nil)
    (divides const-decl "bool" divides nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_div1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (times_div_cancel1 formula-decl nil extra_real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_div_gt formula-decl nil real_props nil))
   nil))
(div_by_gcd_TCC1 0
  (div_by_gcd_TCC1-1 nil 3451974213
   ("" (lemma "div_by_gcd_prep") (("" (propax) nil nil)) nil)
   ((div_by_gcd_prep formula-decl nil gcd_fractions nil)) nil))
(gcd_div_by_gcd_TCC1 0
  (gcd_div_by_gcd_TCC1-1 nil 3453642317 ("" (subtype-tcc) nil nil)
   ((divides const-decl "bool" divides nil)
    (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd
         nil)
    (div_by_gcd const-decl "posint" gcd_fractions nil))
   nil))
(gcd_div_by_gcd 0
  (gcd_div_by_gcd-1 nil 3451974878
   ("" (skosimp)
    (("" (lemma "gcd_times")
      ((""
        (inst - "gcd(p!1, q!1)" "div_by_gcd(p!1, q!1)"
         "div_by_gcd(q!1, p!1)")
        ((""
          (case "div_by_gcd(p!1, q!1) * gcd(p!1, q!1) = p!1 AND div_by_gcd(q!1, p!1) * gcd(p!1, q!1) = q!1")
          (("1" (flatten)
            (("1" (replace*)
              (("1" (hide -2 -1)
                (("1" (cancel-by -1 "gcd(p!1, q!1)") nil nil)) nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (prop)
              (("1" (expand "div_by_gcd") (("1" (assert) nil nil)) nil)
               ("2" (expand "div_by_gcd")
                (("2" (rewrite "gcd_sym") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gcd_times formula-decl nil gcd nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (gcd_sym formula-decl nil gcd nil)
    (div_by_gcd const-decl "posint" gcd_fractions nil)
    (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd
         nil)
    (divides const-decl "bool" divides nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (posint 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)
    (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))
   shostak))
(quotient_fully_cancelled 0
  (quotient_fully_cancelled-1 nil 3451974081
   ("" (skosimp*)
    (("" (lemma "rational_pred_ax2")
      (("" (inst - "r!1")
        (("" (skosimp*)
          (("" (case "i!1 > 0")
            (("1"
              (inst + "div_by_gcd(i!1, p!1)" "div_by_gcd(p!1, i!1)")
              (("1" (rewrite "gcd_div_by_gcd")
                (("1" (expand "div_by_gcd")
                  (("1" (rewrite "gcd_sym") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil)
             ("2" (assert) (("2" (cross-mult -1) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rational_pred_ax2 formula-decl nil rational_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (div_cancel4 formula-decl nil real_props nil)
    (real_gt_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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (i!1 skolem-const-decl "int" gcd_fractions nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (div_by_gcd const-decl "posint" gcd_fractions nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (gcd_sym formula-decl nil gcd nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (gcd_div_by_gcd formula-decl nil gcd_fractions nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rat nonempty-type-eq-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))
   nil)))

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.