Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: symmetric_groups.prf Sprache: Lisp

Original von: PVS^©

(symmetric_groups
(op_TCC1 0
  (op_TCC1-1 nil 3251123754 ("" (grind) nil nil)
   ((composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil))
   nil))
(Sym_is_group 0
  (Sym_is_group-3 nil 3407237323
   ("" (expand "group?")
    (("" (prop)
      (("1" (expand "monoid?")
        (("1" (prop)
          (("1" (expand "monad?")
            (("1" (prop)
              (("1" (expand "groupoid?")
                (("1" (expand "Sym")
                  (("1" (expand "fullset")
                    (("1" (expand "star_closed?")
                      (("1" (skosimp*)
                        (("1" (expand "op")
                          (("1" (expand "member")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "identity")
                (("2" (expand "member")
                  (("2" (expand "Sym")
                    (("2" (expand "fullset") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "restrict")
                (("3" (expand "identity?")
                  (("3" (skosimp*)
                    (("3" (expand "op")
                      (("3" (expand "restrict")
                        (("3" (expand "identity")
                          (("3" (expand "o")
                            (("3" (prop)
                              (("1"
                                (apply-extensionality :hide? t)
                                nil
                                nil)
                               ("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (grind)
            (("2" (expand "o" 1 1)
              (("2" (expand "o" 1 1)
                (("2" (expand "o" 1 1)
                  (("2" (expand "o" 1 1) (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "comp_inverse_right[(S),(S)]")
        (("1" (expand "inv_exists?")
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (assert)
                (("1" (expand "op")
                  (("1" (expand "restrict")
                    (("1" (expand "O")
                      (("1" (assert)
                        (("1" (typepred "x!1")
                          (("1" (inst + "inverse(x!1)")
                            (("1" (expand "identity")
                              (("1"
                                (lemma "comp_inverse_right[(S),(S)]")
                                (("1"
                                  (inst?)
                                  (("1"
                                    (prop)
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst + "1")
                                          (("1"
                                            (hide -)
                                            (("1" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (lemma
                                         "comp_inverse_left[(S),(S)]")
                                        (("1" (inst?) nil nil))
                                        nil)
                                       ("2"
                                        (skosimp*)
                                        (("2"
                                          (inst + "1")
                                          (("2"
                                            (hide -)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "Sym")
                              (("2"
                                (expand "fullset")
                                (("2" (propax) nil nil))
                                nil))
                              nil)
                             ("3" (inst + "1")
                              (("3"
                                (hide -)
                                (("3" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (inst + "1") (("2" (hide 2) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (op const-decl "[perm, perm -> perm]" symmetric_groups nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (Sym const-decl "set[perm]" symmetric_groups nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (identity? const-decl "bool" operator_defs nil)
    (S const-decl "set[posnat]" symmetric_groups nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (bijective? const-decl "bool" functions nil)
    (perm type-eq-decl nil symmetric_groups nil)
    (O const-decl "T3" function_props nil)
    (restrict const-decl "R" restrict nil)
    (monad? const-decl "bool" monad_def nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (associative? const-decl "bool" operator_defs nil)
    (monoid? const-decl "bool" monoid_def nil)
    (inv_exists? const-decl "bool" group_def nil)
    (unique_bijective_inverse application-judgement "{x: D | f(x) = y}"
     function_inverse nil)
    (comp_inverse_left formula-decl nil function_inverse nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (extend const-decl "R" extend nil)
    (x!1 skolem-const-decl "(Sym)" symmetric_groups nil)
    (inverse const-decl "D" function_inverse nil)
    (bijective_inverse_is_bijective application-judgement
     "(bijective?[R, D])" function_inverse nil)
    (TRUE const-decl "bool" booleans nil)
    (comp_inverse_right formula-decl nil function_inverse nil)
    (group? const-decl "bool" group_def nil))
   nil)
  (Sym_is_group-2 nil 3374416353
   ("" (expand "group?")
    (("" (prop)
      (("1" (expand "monoid?")
        (("1" (prop)
          (("1" (expand "monad?")
            (("1" (prop)
              (("1" (expand "groupoid?")
                (("1" (expand "Sym")
                  (("1" (expand "fullset")
                    (("1" (expand "star_closed?")
                      (("1" (skosimp*)
                        (("1" (expand "op")
                          (("1" (expand "member")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "identity")
                (("2" (expand "member")
                  (("2" (expand "Sym")
                    (("2" (expand "fullset") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "restrict")
                (("3" (expand "identity?")
                  (("3" (skosimp*)
                    (("3" (expand "op")
                      (("3" (expand "restrict")
                        (("3" (expand "identity")
                          (("3" (expand "o")
                            (("3" (prop)
                              (("1"
                                (apply-extensionality :hide? t)
                                nil
                                nil)
                               ("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (grind)
            (("2" (expand "o" 1 1)
              (("2" (expand "o" 1 1)
                (("2" (expand "o" 1 1)
                  (("2" (expand "o" 1 1) (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "comp_inv_right[(S),(S)]")
        (("1" (expand "inv_exists?")
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (assert)
                (("1" (expand "op")
                  (("1" (expand "restrict")
                    (("1" (expand "O")
                      (("1" (assert)
                        (("1" (typepred "x!1")
                          (("1" (inst + "inv(x!1)")
                            (("1" (expand "identity")
                              (("1"
                                (lemma "comp_inv_right[(S),(S)]")
                                (("1"
                                  (inst?)
                                  (("1"
                                    (prop)
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst + "1")
                                          (("1"
                                            (hide -)
                                            (("1" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (lemma
                                         "comp_inv_left[(S),(S)]")
                                        (("1" (inst?) nil nil))
                                        nil)
                                       ("2"
                                        (skosimp*)
                                        (("2"
                                          (inst + "1")
                                          (("2"
                                            (hide -)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "Sym")
                              (("2"
                                (expand "fullset")
                                (("2" (propax) nil nil))
                                nil))
                              nil)
                             ("3" (inst + "1")
                              (("3"
                                (hide -)
                                (("3" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (inst + "1") (("2" (hide 2) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((group? const-decl "bool" group_def nil)
    (inv_exists? const-decl "bool" group_def nil)
    (monoid? const-decl "bool" monoid_def nil)
    (monad? const-decl "bool" monad_def nil)
    (star_closed? const-decl "bool" groupoid_def nil))
   nil)
  (Sym_is_group-1 nil 3251123754
   ("" (expand "group?")
    (("" (prop)
      (("1" (expand "monoid?")
        (("1" (prop)
          (("1" (expand "monad?")
            (("1" (prop)
              (("1" (expand "groupoid?")
                (("1" (expand "Sym")
                  (("1" (expand "fullset")
                    (("1" (expand "star_closed?")
                      (("1" (skosimp*)
                        (("1" (expand "op")
                          (("1" (expand "member")
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "identity")
                (("2" (expand "member")
                  (("2" (expand "Sym")
                    (("2" (expand "fullset") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (expand "restrict")
                (("3" (expand "identity?")
                  (("3" (skosimp*)
                    (("3" (expand "op")
                      (("3" (expand "restrict")
                        (("3" (expand "identity")
                          (("3" (expand "o")
                            (("3" (prop)
                              (("1"
                                (apply-extensionality :hide? t)
                                nil
                                nil)
                               ("2"
                                (apply-extensionality 1 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (grind)
            (("2" (expand "o") (("2" (propax) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (lemma "comp_inv_right[(S),(S)]")
        (("1" (expand "inv_exists?")
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (assert)
                (("1" (expand "op")
                  (("1" (expand "restrict")
                    (("1" (expand "O")
                      (("1" (assert)
                        (("1" (typepred "x!1")
                          (("1" (inst + "inv(x!1)")
                            (("1" (expand "identity")
                              (("1"
                                (lemma "comp_inv_right[(S),(S)]")
                                (("1"
                                  (inst?)
                                  (("1"
                                    (prop)
                                    (("1"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst + "1")
                                          (("1"
                                            (hide -)
                                            (("1" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (apply-extensionality 1 :hide? t)
                                      (("1"
                                        (lemma
                                         "comp_inv_left[(S),(S)]")
                                        (("1" (inst?) nil nil))
                                        nil)
                                       ("2"
                                        (skosimp*)
                                        (("2"
                                          (inst + "1")
                                          (("2"
                                            (hide -)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "Sym")
                              (("2"
                                (expand "fullset")
                                (("2" (propax) nil nil))
                                nil))
                              nil)
                             ("3" (inst + "1")
                              (("3"
                                (hide -)
                                (("3" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (inst + "1") (("2" (hide 2) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((star_closed? const-decl "bool" groupoid_def nil)
    (monad? const-decl "bool" monad_def nil)
    (monoid? const-decl "bool" monoid_def nil)
    (inv_exists? const-decl "bool" group_def nil)
    (group? const-decl "bool" group_def nil))
   nil)))

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