Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: number_fields_bis.prf Sprache: Lisp

Original von: PVS^©

(cyclic_monoid_def
  (power_TCC1 0
  (power_TCC1-1 nil 3292925562 3293621498 ("" (grind) nil nil)
   proved-complete
   ((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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   121 110 t shostak))
(power_TCC2 0
  (power_TCC2-1 nil 3292925568 3293621498 ("" (grind) nil nil)
   proved-complete nil 29 30 t shostak))
(power_0 0
  (power_0-1 nil 3292925609 3293638300 ("" (grind) nil nil) proved
   ((power def-decl "T" groups nil)) 22 20 t shostak))
(power_1 0
  (power_1-1 nil 3292925615 3293638300 ("" (grind) nil nil) proved
   ((power def-decl "T" groups nil)
    (one formal-const-decl "T" groups nil)
    (* formal-const-decl "[T, T -> T]" groups nil)
    (T formal-nonempty-type-decl nil groups nil)
    (right_identity formula-decl nil monoids nil))
   42 30 t shostak))
(one_power 0
  (one_power-1 nil 3292925621 3293638300
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skosimp*)
      (("2" (expand "power" 1) (("2" (assert) nil nil)) nil)) nil))
    nil)
   proved
   ((* formal-const-decl "[T, T -> T]" groups nil)
    (left_identity formula-decl nil monoids nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (one formal-const-decl "T" groups nil)
    (power def-decl "T" groups nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil groups 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))
   60 50 t shostak))
(power_def 0
  (power_def-1 nil 3292925779 3293638301
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skosimp*)
      (("2" (inst - "a!1")
        (("2" (expand "power" 1)
          (("2"
            (lemma "cancel_left"
             ("z" "a!1" "x" "power(a!1, j!1 + 1)" "y"
              "power(a!1, j!1) * a!1"))
            (("2" (rewrite "associative") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((associative formula-decl nil monoids nil)
    (cancel_left formula-decl nil groups nil)
    (one formal-const-decl "T" groups nil)
    (right_identity formula-decl nil monoids nil)
    (left_identity formula-decl nil monoids nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (* formal-const-decl "[T, T -> T]" groups nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (power def-decl "T" groups nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil groups 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))
   385 350 t shostak))
(power_mult 0
  (power_mult-1 nil 3292925654 3293638301
   ("" (induct "m")
    (("1" (skolem!)
      (("1" (rewrite "power_0") (("1" (assert) nil nil)) nil)) nil)
     ("2" (skosimp*)
      (("2" (inst - "a!1" "n!1+1")
        (("2" (rewrite "power_def" -1)
          (("2" (expand "power" 1 2)
            (("2" (rewrite "associative" -1) (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((power_def formula-decl nil groups nil)
    (associative formula-decl nil monoids nil)
    (one formal-const-decl "T" groups nil)
    (right_identity formula-decl nil monoids nil)
    (power_0 formula-decl nil groups 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)
    (power def-decl "T" groups nil)
    (* formal-const-decl "[T, T -> T]" groups nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil groups 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))
   514 480 t shostak))
(power_power 0
  (power_power-1 nil 3292926190 3293638302
   ("" (induct "m")
    (("1" (skolem!)
      (("1" (rewrite "power_0") (("1" (rewrite "power_0") nil nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "power" 1 1)
        (("2" (inst - "a!1" "n!1")
          (("2" (replace -1)
            (("2" (rewrite "power_mult") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((power_mult formula-decl nil groups nil)
    (power_0 formula-decl nil groups 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)
    (power def-decl "T" groups nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil groups 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))
   601 570 t shostak))
(power_commutes 0
  (power_commutes-1 nil 3292926297 3293638302
   ("" (skolem!)
    (("" (rewrite "power_mult") (("" (rewrite "power_mult") nil nil))
      nil))
    nil)
   proved
   ((power_mult formula-decl nil groups nil)
    (T formal-nonempty-type-decl nil groups 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   229 220 t shostak))
(inv_power 0
  (inv_power-1 nil 3292926316 3293638302
   ("" (induct "m")
    (("1" (grind) nil nil)
     ("2" (skosimp*)
      (("2" (expand "power" 1 1)
        (("2" (rewrite "inv_star")
          (("2" (rewrite "power_def")
            (("2" (inst - "a!1")
              (("2"
                (lemma "cancel_right"
                 ("z" "inv(a!1)" "x" "inv(power(a!1, j!1))" "y"
                  "power(inv(a!1), j!1)"))
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((inv_star formula-decl nil groups nil)
    (cancel_right formula-decl nil groups 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)
    (power_def formula-decl nil groups nil)
    (inv_one formula-decl nil groups nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (power def-decl "T" groups nil)
    (inv const-decl "{y | x * y = one AND y * x = one}" groups nil)
    (one formal-const-decl "T" groups nil)
    (* formal-const-decl "[T, T -> T]" groups nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil groups 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))
   412 410 t shostak))
(power_inv_right 0
  (power_inv_right-1 nil 3292926510 3293638302
   ("" (skolem!)
    (("" (rewrite "inv_power" :dir rl) (("" (assert) nil nil))
      nil))
    nil)
   proved
   ((inv_power formula-decl nil groups nil)
    (T formal-nonempty-type-decl nil groups 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (inv_right formula-decl nil groups nil))
   46 50 t shostak))
(power_inv_left 0
  (power_inv_left-1 nil 3292926554 3293638303
   ("" (skolem!)
    (("" (rewrite "inv_power" :dir rl) (("" (assert) nil nil))
      nil))
    nil)
   proved
   ((inv_power formula-decl nil groups nil)
    (T formal-nonempty-type-decl nil groups 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (inv_left formula-decl nil groups nil))
   39 40 t shostak))
(cyclic_group_is_abelian 0
  (cyclic_group_is_abelian-1 nil 3293272131 3293621505
   ("" (skolem 1 ("G!1"))
    (("" (typepred "G!1")
      (("" (expand "cyclic_group?")
        (("" (flatten)
          (("" (expand "abelian_group?")
            (("" (assert)
              (("" (expand "cyclic?")
                (("" (skolem!)
                  (("" (replace -1 -2)
                    (("" (expand "commutative_over?")
                      (("" (skosimp*)
                        (("" (replace -1)
                          (("" (assert)
                            (("" (expand "generated_by")
                              ((""
                                (skosimp*)
                                ((""
                                  (lemma
                                   "expt_mult"
                                   ("a" "a!1" "i" "i!1" "j" "i!2"))
                                  ((""
                                    (lemma
                                     "expt_mult"
                                     ("a" "a!1" "i" "i!2" "j" "i!1"))
                                    (("" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved-incomplete
   ((cyclic_group nonempty-type-eq-decl nil groups nil)
    (cyclic_group? const-decl "bool" groups nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil groups nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (commutative_over? const-decl "bool" operator_defs_more nil)
    (generated_by const-decl "group" groups 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)
    (number nonempty-type-decl nil numbers nil)
    (expt_mult formula-decl nil groups nil)
    (member const-decl "bool" sets nil)
    (cyclic? const-decl "bool" groups nil)
    (abelian_group? const-decl "bool" groups_def nil))
   290 250 t shostak)))

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.