Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Delphi/Autor 0.7/   (Columbo Version 0.7©)  Datei vom 4.1.2008 mit Größe 109 B image not shown  

 subgroups.prf   Interaktion und
PortierbarkeitLisp

 
(subgroups
 (G_TCC1 0
  (G_TCC1-1 nil 3459006169
   ("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
   ((fullset_is_group formula-decl nil subgroups nil)) nil))
 (pg64_1 0
  (pg64_1-1 nil 3459009709
   ("" (skeep)
    (("" (lemma "subgroup_def[T,*,one]")
      (("" (inst - "G" "intersection(A, B)")
        (("" (assert)
          (("" (hide 2)
            (("" (prop)
              (("1" (expand "nonempty?")
                (("1" (expand "empty?")
                  (("1" (expand "member")
                    (("1" (expand "intersection")
                      (("1" (expand "member")
                        (("1" (inst - "one") (("1" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "subgroup?")
                (("2" (flatten)
                  (("2" (auto-rewrite-theory "sets[T]")
                    (("2" (assert)
                      (("2" (skosimp*)
                        (("2" (inst?)
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "subgroup?")
                (("3" (expand "star_closed?")
                  (("3" (expand "intersection")
                    (("3" (assert)
                      (("3" (skosimp*)
                        (("3" (typepred "x!1")
                          (("3" (typepred "y!1")
                            (("3" (expand "intersection")
                              (("3"
                                (assert)
                                (("3"
                                  (flatten)
                                  (("3"
                                    (expand "group?")
                                    (("3"
                                      (expand "monoid?")
                                      (("3"
                                        (expand "monad?")
                                        (("3"
                                          (flatten)
                                          (("3"
                                            (expand "star_closed?")
                                            (("3"
                                              (assert)
                                              (("3"
                                                (inst?)
                                                (("3"
                                                  (inst?)
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("4" (expand "inv_closed?")
                (("4" (expand "intersection")
                  (("4" (expand "subgroup?")
                    (("4" (expand "subset?")
                      (("4" (expand "member")
                        (("4" (flatten)
                          (("4" (expand "group?")
                            (("4" (flatten)
                              (("4"
                                (expand "inv_exists?")
                                (("4"
                                  (skosimp*)
                                  (("4"
                                    (inst -3 "x!1")
                                    (("1"
                                      (inst -6 "x!1")
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (replace -3 -7 rl)
                                          (("1"
                                            (rewrite
                                             "cancel_left[T,*,one]")
                                            (("1"
                                              (lemma
                                               "unique_inv[T,*,one]")
                                              (("1"
                                                (inst-cp
                                                 -1
                                                 "x!1"
                                                 "y!1")
                                                (("1"
                                                  (inst -1 "x!1" "y!2")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (typepred "x!1")
                                        (("2"
                                          (expand "intersection")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (typepred "x!1")
                                      (("2"
                                        (expand "intersection")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((one formal-const-decl "T" subgroups nil)
    (* formal-const-decl "[T, T -> T]" subgroups nil)
    (T formal-nonempty-type-decl nil subgroups nil)
    (subgroup_def formula-decl nil group nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (empty? const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (associative? const-decl "bool" operator_defs nil)
    (monoid? const-decl "bool" monoid_def nil)
    (inv_exists? const-decl "bool" group_def nil)
    (subgroup? const-decl "bool" group_def nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (unique_inv formula-decl nil group nil)
    (cancel_left formula-decl nil group nil)
    (x!1 skolem-const-decl "(intersection(A, B))" subgroups nil)
    (B skolem-const-decl "set[T]" subgroups nil)
    (A skolem-const-decl "set[T]" subgroups nil)
    (inv_closed? const-decl "bool" group nil)
    (intersection const-decl "set" sets nil)
    (group nonempty-type-eq-decl nil group nil)
    (group? const-decl "bool" group_def nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (center_normal_TCC1 0
  (center_normal_TCC1-1 nil 3459175283
   ("" (skeep)
    (("" (lemma "center_subgroup")
      (("" (inst?)
        (("" (expand "subgroup?") (("" (flatten) nil nil)) nil)) nil))
      nil))
    nil)
   ((one formal-const-decl "T" subgroups nil)
    (* formal-const-decl "[T, T -> T]" subgroups nil)
    (T formal-nonempty-type-decl nil subgroups nil)
    (center_subgroup formula-decl nil group nil)
    (subgroup? const-decl "bool" group_def nil)
    (group nonempty-type-eq-decl nil group nil)
    (group? const-decl "bool" group_def nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (center_normal 0
  (center_normal-1 nil 3459175396
   ("" (skeep)
    (("" (expand "normal_subgroup?")
      (("" (lemma "center_subgroup")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (typepred "a!1")
                (("" (expand "subset?")
                  (("" (skosimp*)
                    (("" (expand "member")
                      (("" (expand "*")
                        (("" (skosimp*)
                          (("" (typepred "h!1")
                            (("" (skosimp*)
                              ((""
                                (typepred "h!2")
                                ((""
                                  (rewrite "center_def" +)
                                  ((""
                                    (prop)
                                    (("1"
                                      (replace -5)
                                      (("1"
                                        (replace -2)
                                        (("1"
                                          (typepred "center(G)")
                                          (("1"
                                            (expand "subset?")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (inst - "h!2")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (hide -2 -3 -5 -6)
                                                    (("1"
                                                      (lemma
                                                       "inv_member")
                                                      (("1"
                                                        (inst?)
                                                        (("1"
                                                          (inst?)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "product_in")
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (hide
                                                                     2)
                                                                    (("1"
                                                                      (lemma
                                                                       "product_in")
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace -5)
                                      (("2"
                                        (skeep)
                                        (("2"
                                          (hide -5)
                                          (("2"
                                            (replace -2)
                                            (("2"
                                              (hide -2)
                                              (("2"
                                                (name
                                                 "w"
                                                 "inv[T, *, one](a!1)")
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (hide -4)
                                                    (("2"
                                                      (rewrite
                                                       "center_def")
                                                      (("2"
                                                        (flatten)
                                                        (("2"
                                                          (inst-cp
                                                           -3
                                                           "w")
                                                          (("1"
                                                            (replace
                                                             -4)
                                                            (("1"
                                                              (lemma
                                                               "assoc")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "h!2"
                                                                 "w"
                                                                 "a!1")
                                                                (("1"
                                                                  (replace
                                                                   -1
                                                                   +
                                                                   rl)
                                                                  (("1"
                                                                    (replace
                                                                     -2
                                                                     +
                                                                     rl)
                                                                    (("1"
                                                                      (rewrite
                                                                       "inv_left")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (inst?)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (lemma
                                                             "inv_in")
                                                            (("2"
                                                              (inst?)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((normal_subgroup? const-decl "boolean" normal_subgroups nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (group? const-decl "bool" group_def nil)
    (group nonempty-type-eq-decl nil group nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (center_def formula-decl nil group nil)
    (G skolem-const-decl "group[T, *, one]" subgroups nil)
    (w skolem-const-decl "T" subgroups nil)
    (assoc formula-decl nil group nil)
    (inv_left formula-decl nil group nil)
    (right_identity formula-decl nil monad nil)
    (inv_in formula-decl nil group nil)
    (inv_member formula-decl nil group nil)
    (product_in formula-decl nil group nil)
    (inv const-decl "{y | x * y = one AND y * x = one}" group nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (center const-decl "{s: set[T] | subset?(s, G)}" group nil)
    (* const-decl "set[T]" cosets nil)
    (* const-decl "set[T]" cosets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (center_subgroup formula-decl nil group nil)
    (T formal-nonempty-type-decl nil subgroups nil)
    (* formal-const-decl "[T, T -> T]" subgroups nil)
    (one formal-const-decl "T" subgroups nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.