products/sources/formale sprachen/Coq/dev/ci/nix/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sort_fseq_lems.prf   Sprache: Unknown

(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.28 Sekunden  (vorverarbeitet)  ]