products/sources/formale Sprachen/PVS/orders/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: eq_mod.prf   Sprache: Unknown

(eq_mod
 (eq_mod_equiv 0
  (eq_mod_equiv-1 nil 3411734899
   ("" (skosimp*)
    (("" (expand "equivalence?")
      (("" (prop)
        (("1" (expand "reflexive?")
          (("1" (skosimp*)
            (("1" (expand "eq_mod")
              (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (expand "symmetric?")
          (("2" (skosimp*)
            (("2" (expand "eq_mod")
              (("2" (skosimp*)
                (("2" (inst + "-k!1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (expand "transitive?")
          (("3" (skosimp*)
            (("3" (expand "eq_mod")
              (("3" (skosimp*)
                (("3" (replaces -)
                  (("3" (assert)
                    (("3" (inst + "k!1+k!2") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((equivalence? const-decl "bool" relations nil)
    (transitive? const-decl "bool" relations nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (symmetric? const-decl "bool" relations nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (reflexive? const-decl "bool" relations nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (eq_mod const-decl "bool" eq_mod nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers 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))
 (eq_mod_mult 0
  (eq_mod_mult-2 nil 3411746929
   ("" (skosimp*)
    (("" (expand "eq_mod")
      (("" (skosimp*)
        (("" (replaces -)
          (("" (inst + "(k!1 * k!2 * p!1 + b!1 * k!2 + d!1 * k!1)")
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (eq_mod const-decl "bool" eq_mod nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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))
   nil)
  (eq_mod_mult-1 nil 3411734172
   ("" (skosimp*)
    (("" (expand "eq_mod")
      (("" (skosimp*)
        (("" (replaces -)
          (("" (assert)
            ((""
              (name "AA"
                    " k!1 * k!3 * p!1 * p!1 + k!2 * k!3 * p!1 * p!1 +
         k!3 * k!3 * p!1 * p!1
         + d!1 * k!1 * p!1
         + d!1 * k!3 * p!1
")
              (("" (factor -1)
                ((""
                  (inst +
                   " (k!1 * k!3 * p!1 + k!2 * k!3 * p!1 + k!3 * k!3 * p!1 + d!1 * k!1 +
         d!1 * k!3)")
                  (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (eq_mod_rem 0
  (eq_mod_rem-1 nil 3411813690
   ("" (skosimp*)
    (("" (expand "eq_mod")
      (("" (typepred "rem(p!1)(j!1)")
        (("1" (skosimp*)
          (("1" (inst + "q!1") (("1" (assert) nil nil)) nil)) nil)
         ("2" (propax) nil nil))
        nil))
      nil))
    nil)
   ((eq_mod const-decl "bool" eq_mod nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (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)
    (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)
    (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)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (rem const-decl "{r: mod(b) | EXISTS q: x = b * q + r}"
         modulo_arithmetic nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil))
   shostak))
 (gcd_is_1_TCC1 0
  (gcd_is_1_TCC1-1 nil 3411812631 ("" (subtype-tcc) 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)
    (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_ge_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)
    (divides const-decl "bool" divides nil)
    (/= const-decl "boolean" notequal nil)
    (prime? const-decl "bool" primes "ints/"))
   nil))
 (gcd_is_1 0
  (gcd_is_1-1 nil 3411812637
   ("" (skosimp*)
    (("" (lemma "gcd_def")
      (("" (inst?)
        (("" (assert)
          (("" (split -1)
            (("1" (expand "divides")
              (("1" (inst 1 "a!1") (("1" (assert) nil nil)) nil)) nil)
             ("2" (expand "divides")
              (("2" (inst 1 "p!1") (("2" (assert) nil nil)) nil)) nil)
             ("3" (skosimp*)
              (("3" (expand "divides")
                (("3" (skosimp*)
                  (("3" (expand "prime?")
                    (("3" (flatten)
                      (("3" (inst -3 "mm!1")
                        (("3" (typepred "mm!1")
                          (("3" (assert)
                            (("3" (split -4)
                              (("1"
                                (expand "divides")
                                (("1" (inst + "x!2") nil nil))
                                nil)
                               ("2"
                                (assert)
                                (("2"
                                  (flatten)
                                  (("2"
                                    (replace -1)
                                    (("2" (inst + "x!1") nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("4" (flatten)
              (("4" (replace -1)
                (("4" (expand "divides")
                  (("4" (inst + "0") (("4" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gcd_def formula-decl nil gcd "ints/")
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (prime? const-decl "bool" primes "ints/")
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (divides const-decl "bool" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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))
   shostak))
 (Euclids_30 0
  (Euclids_30-1 nil 3411755092
   ("" (skeep)
    (("" (expand "divides" -2)
      (("" (skosimp*)
        (("" (lemma "gcd_is_1")
          (("" (inst?)
            (("" (assert)
              (("" (lemma "rel_prime_lem")
                (("" (expand "rel_prime")
                  (("" (inst?)
                    (("" (assert)
                      (("" (expand "prime?")
                        (("" (flatten)
                          (("" (assert)
                            (("" (skosimp*)
                              ((""
                                (mult-by -1 "b")
                                ((""
                                  (assert)
                                  ((""
                                    (replace -5)
                                    ((""
                                      (assert)
                                      ((""
                                        (factor -1)
                                        ((""
                                          (expand "divides" 2)
                                          ((""
                                            (inst
                                             +
                                             "(b * n!1 + m!1 * x!1)")
                                            (("" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divides const-decl "bool" divides nil)
    (gcd_is_1 formula-decl nil eq_mod nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (rel_prime const-decl "bool" gcd "ints/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (prime? const-decl "bool" primes "ints/")
    (rel_prime_lem formula-decl nil gcd "ints/")
    (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))
   shostak))
 (eq_mod_cancel 0
  (eq_mod_cancel-1 nil 3411754307
   ("" (skeep)
    (("" (case "divides(p,a*c-b*c)")
      (("1" (case-replace "a * c - b * c = (a-b)*c")
        (("1" (hide -1)
          (("1" (lemma "Euclids_30")
            (("1" (inst?)
              (("1" (assert)
                (("1" (hide -2 -4 1)
                  (("1" (expand "eq_mod")
                    (("1" (expand "divides")
                      (("1" (skosimp*)
                        (("1" (assert)
                          (("1" (inst + "x!1") (("1" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil)
       ("2" (hide 2)
        (("2" (expand "eq_mod")
          (("2" (expand "divides")
            (("2" (skosimp*)
              (("2" (replace -2)
                (("2" (assert)
                  (("2" (inst + "k!1") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (divides const-decl "bool" divides 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (eq_mod const-decl "bool" eq_mod nil)
    (Euclids_30 formula-decl nil eq_mod nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   shostak)))

[ Dauer der Verarbeitung: 0.6 Sekunden  (vorverarbeitet)  ]