Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: synch_protocol_invariants.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) (("" (assert) nil 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) (("" (assert) 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)
    (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?) (("" (assert) nil 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.16 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.