Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: abelian_group.prf   Sprache: Lisp

Original von: PVS©

(abelian_group
 (IMP_group_TCC1 0
  (IMP_group_TCC1-1 nil 3293976868
   ("" (lemma "fullset_is_abelian_group")
    (("" (expand "abelian_group?") (("" (flatten) nil nil)) nil)) nil)
   ((abelian_group? const-decl "bool" group_def nil)
    (fullset_is_abelian_group formula-decl nil abelian_group nil))
   shostak))
 (abelian_group_TCC1 0
  (abelian_group_TCC1-1 nil 3293976891
   ("" (lemma "fullset_is_abelian_group") (("" (propax) nil nil)) nil)
   ((fullset_is_abelian_group formula-decl nil abelian_group nil))
   shostak))
 (abelian_group_is_group 0
  (abelian_group_is_group-1 nil 3293976699
   ("" (skolem!)
    (("" (typepred "x!1")
      (("" (expand "abelian_group?") (("" (flatten) nil nil)) nil))
      nil))
    nil)
   ((abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (abelian_group_is_commutative_monoid 0
  (abelian_group_is_commutative_monoid-1 nil 3294086816
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "abelian_group?")
        (("" (expand "group?")
          (("" (expand "commutative_monoid?")
            (("" (flatten) (("" (assertnil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (group? const-decl "bool" group_def nil)
    (commutative_monoid? const-decl "bool" monoid_def nil))
   shostak))
 (abelian_subgroups 0
  (abelian_subgroups-1 nil 3293976722
   ("" (skolem!)
    (("" (flatten)
      (("" (typepred "A!1")
        (("" (expand "abelian_group?")
          (("" (flatten)
            (("" (expand "subgroup?")
              (("" (flatten)
                (("" (assert)
                  (("" (hide -1 -4)
                    (("" (expand "commutative_over?")
                      (("" (skosimp*)
                        (("" (inst - "x!1" "y!1")
                          (("" (expand "subset?")
                            (("" (inst-cp - "x!1")
                              ((""
                                (inst - "y!1")
                                (("" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subgroup? const-decl "bool" group_def nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (subset? const-decl "bool" sets nil)
    (A!1 skolem-const-decl "abelian_group" abelian_group nil)
    (S!1 skolem-const-decl "set[T]" abelian_group nil)
    (x!1 skolem-const-decl "(S!1)" abelian_group nil)
    (y!1 skolem-const-decl "(S!1)" abelian_group nil)
    (member const-decl "bool" sets nil)
    (commutative? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (one formal-const-decl "T" abelian_group nil)
    (abelian_group? const-decl "bool" group_def nil)
    (abelian_group nonempty-type-eq-decl nil abelian_group nil))
   shostak))
 (finite_abelian_group_TCC1 0
  (finite_abelian_group_TCC1-1 nil 3407081659
   ("" (inst + "singleton[T](one)")
    (("" (expand "finite_abelian_group?")
      (("" (assert)
        (("" (expand "commutative?")
          (("" (skosimp*)
            (("" (grind)
              (("" (typepred "y!1")
                (("" (typepred "x!1")
                  (("" (expand "singleton")
                    (("" (replace -1)
                      (("" (hide -1)
                        (("" (replace -1) (("" (propax) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((commutative? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (one_finite_group formula-decl nil group nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (finite_abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
 (finite_abelian_group_is_abelian_group 0
  (finite_abelian_group_is_abelian_group-2 nil 3426244950
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "finite_abelian_group?")
        (("" (flatten)
          (("" (expand "abelian_group?")
            (("" (expand "finite_group?")
              (("" (flatten) (("" (assertnil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (finite_abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_group? const-decl "bool" group_def nil)
    (abelian_group? const-decl "bool" group_def nil))
   nil)
  (finite_abelian_group_is_abelian_group-1 nil 3407081659
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "finite_abelian_group?")
        (("" (flatten)
          (("" (assert)
            (("" (expand "abelian_group?")
              (("" (assert)
                (("" (expand "finite_group?") (("" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_abelian_group? const-decl "bool" group_def nil)
    (abelian_group? const-decl "bool" group_def nil)
    (finite_group? const-decl "bool" group_def nil))
   nil))
 (finite_abelian_group_is_finite_group 0
  (finite_abelian_group_is_finite_group-1 nil 3407081659
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (assert)
        (("" (expand "finite_group?")
          (("" (expand "finite_abelian_group?") (("" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (finite_abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_group? const-decl "bool" group_def nil))
   nil))
 (finite_abelian_subgroups 0
  (finite_abelian_subgroups-1 nil 3407081668
   ("" (skosimp)
    (("" (lemma "abelian_subgroups" ("S" "S!1" "A" "G!1"))
      (("" (expand "finite_abelian_group?")
        (("" (expand "abelian_group?")
          (("" (assert)
            (("" (flatten)
              (("" (assert)
                (("" (expand "finite_group?")
                  (("" (lemma "finite_subgroups")
                    (("" (inst?) (("" (assertnil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (finite_abelian_group? const-decl "bool" group_def nil)
    (abelian_group nonempty-type-eq-decl nil abelian_group nil)
    (abelian_group? const-decl "bool" group_def nil)
    (one formal-const-decl "T" abelian_group nil)
    (* formal-const-decl "[T, T -> T]" abelian_group nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil abelian_group nil)
    (abelian_subgroups formula-decl nil abelian_group nil)
    (finite_group? const-decl "bool" group_def nil)
    (finite_group nonempty-type-eq-decl nil group nil)
    (finite_subgroups formula-decl nil group nil))
   nil)))


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


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik