Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: finite_cyclic_groups.prf Sprache: Lisp

Original von: PVS^©

(finite_cyclic_groups
(IMP_finite_groups_TCC1 0
  (IMP_finite_groups_TCC1-1 nil 3408118121
   ("" (rewrite "fullset_is_group") nil nil)
   ((fullset_is_group formula-decl nil finite_cyclic_groups nil)) nil))
(prime_order_cycle 0
  (prime_order_cycle-2 nil 3407853657
   ("" (skosimp*)
    (("" (expand "cyclic?")
      (("" (expand "order")
        (("" (case "card(G!1) > 1")
          (("1" (case "(EXISTS (a: (G!1)): a /= one)")
            (("1" (skosimp*)
              (("1" (name "HH" "generated_by(a!1)")
                (("1" (inst + "a!1")
                  (("1" (assert)
                    (("1" (replace -1)
                      (("1" (case "subgroup?(HH,G!1)")
                        (("1" (lemma "Lagrange")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (expand "prime?")
                                (("1"
                                  (inst - "order(HH)")
                                  (("1"
                                    (expand "order")
                                    (("1"
                                      (split -5)
                                      (("1" (propax) nil nil)
                                       ("2"
                                        (assert)
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (lemma
                                             "generated_by_card_1")
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (inst - "G!1")
                                                (("2"
                                                  (expand "member")
                                                  (("2"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("3"
                                        (flatten)
                                        (("3"
                                          (assert)
                                          (("3"
                                            (hide -2 -4)
                                            (("3"
                                              (expand "subgroup?")
                                              (("3"
                                                (lemma
                                                 "same_card_subset[T]")
                                                (("3"
                                                  (inst - "HH" "G!1")
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (typepred "G!1")
                              (("2"
                                (lemma "finite_subgroups")
                                (("2"
                                  (inst?)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (lemma "generated_is_subgroup")
                          (("2" (inst?)
                            (("2" (inst - "G!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide -2 2)
              (("2" (lemma "card_2_has_2[T]")
                (("2" (inst - "G!1")
                  (("2" (assert)
                    (("2" (skosimp*)
                      (("2" (inst-cp + "x!1")
                        (("2" (inst + "y!1") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (expand "prime?") (("2" (flatten) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cyclic? const-decl "boolean" group nil)
    (finite_group nonempty-type-eq-decl nil group nil)
    (finite_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" finite_cyclic_groups nil)
    (* formal-const-decl "[T, T -> T]" finite_cyclic_groups nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil finite_cyclic_groups 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)
    (y!1 skolem-const-decl "T" finite_cyclic_groups nil)
    (x!1 skolem-const-decl "T" finite_cyclic_groups nil)
    (G!1 skolem-const-decl "finite_group[T, *, one]"
     finite_cyclic_groups nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (card_2_has_2 formula-decl nil finite_sets nil)
    (generated_is_subgroup formula-decl nil cyclic_group nil)
    (Lagrange formula-decl nil lagrange nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_subgroups formula-decl nil group nil)
    (finite_monad nonempty-type-eq-decl nil monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (member const-decl "bool" sets nil)
    (generated_by_card_1 formula-decl nil finite_groups nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (same_card_subset formula-decl nil finite_sets nil)
    (prime? const-decl "bool" primes "ints/")
    (HH skolem-const-decl "group[T, *, one]" finite_cyclic_groups nil)
    (subgroup? const-decl "bool" group_def nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (generated_by const-decl "group" group nil)
    (group nonempty-type-eq-decl nil group nil)
    (group? const-decl "bool" group_def nil)
    (/= const-decl "boolean" notequal nil)
    (order const-decl "posnat" monad nil))
   nil)
  (prime_order_cycle-1 nil 3407082460
   (";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
    (skosimp*)
    ((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
      (expand "cyclic?")
      ((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
        (expand "order")
        ((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
          (case "card(G!1) > 1")
          (("1" (case "(EXISTS (a: (G!1)): a /= one)")
            (("1" (skosimp*)
              (("1" (name "HH" "generated_by(a!1)")
                (("1" (inst + "a!1")
                  (("1" (assert)
                    (("1" (replace -1)
                      (("1" (case "subgroup?(HH,G!1)")
                        (("1" (lemma "Lagrange")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (expand "prime?")
                                (("1"
                                  (inst - "order(HH)")
                                  (("1"
                                    (expand "order")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (split -5)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "divides")
                                            (("1" (propax) nil)))))
                                         ("2"
                                          (flatten)
                                          (("2"
                                            (lemma
                                             "generated_by_card_1")
                                            (("2"
                                              (inst?)
                                              (("2"
                                                (inst - "G!1")
                                                (("2"
                                                  (expand "member")
                                                  (("2"
                                                    (assert)
                                                    nil)))))))))))
                                         ("3"
                                          (flatten)
                                          (("3"
                                            (assert)
                                            (("3"
                                              (hide -2 -4)
                                              (("3"
                                                (expand "subgroup?")
                                                (("3"
                                                  (lemma
                                                   "same_card_subset[T]")
                                                  (("3"
                                                    (inst - "HH" "G!1")
                                                    (("3"
                                                      (assert)
                                                      nil)))))))))))))))))))))))))
                             ("2" (typepred "G!1")
                              (("2"
                                (lemma "finite_subgroups")
                                (("2"
                                  (inst?)
                                  (("2" (assert) nil)))))))))))
                         ("2" (lemma "generated_is_subgroup")
                          (("2" (inst?)
                            (("2" (inst - "G!1")
                              (("2" (assert) nil)))))))))))))))))))
             ("2" (hide -2 2)
              (("2" (lemma "card_2_has_2[T]")
                (("2" (inst - "G!1")
                  (("2" (assert)
                    (("2" (skosimp*)
                      (("2" (inst-cp + "x!1")
                        (("2" (inst + "y!1")
                          (("2" (assert) nil)))))))))))))))))
           ("2" (expand "prime?") (("2" (flatten) nil))))))))))
    ";;; developed with shostak decision procedures")
   ((cyclic? const-decl "boolean" group nil)
    (finite_group nonempty-type-eq-decl nil group nil)
    (finite_group? const-decl "bool" group_def nil)
    (generated_is_subgroup formula-decl nil group nil)
    (Lagrange formula-decl nil lagrange nil)
    (finite_subgroups formula-decl nil group nil)
    (finite_monad nonempty-type-eq-decl nil monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (subgroup? const-decl "bool" group_def nil)
    (generated_by const-decl "group" group nil)
    (group nonempty-type-eq-decl nil group nil)
    (group? const-decl "bool" group_def nil)
    (order const-decl "posnat" monad nil))
   nil)))

¤ Dauer der Verarbeitung: 0.8 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.