products/sources/formale sprachen/PVS/groups/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: real_lebesgue_scaf.prf   Sprache: Lisp

Original von: PVS©
(isomorphism_theorems
 (G_TCC1 0
  (G_TCC1-1 nil 3530909168 ("" (rewrite "T1_is_group") nil nil)
   ((T1_is_group formula-decl nil isomorphism_theorems nil)) nil))
 (GP_TCC1 0
  (GP_TCC1-1 nil 3530909168 ("" (rewrite "T2_is_group") nil nil)
   ((T2_is_group formula-decl nil isomorphism_theorems nil)) nil))
 (quotient_subgroup_TCC1 0
  (quotient_subgroup_TCC1-1 nil 3524781199
   ("" (skosimp*)
    (("" (lemma "normal_subgroup_tran[T1, *, one1]")
      (("1" (inst -1 "G!1" "M!1" "N!1")
        (("1" (assert)
          (("1" (typepred "M!1")
            (("1" (expand "normal_subgroup?") (("1" (propax) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "G_TCC1") nil nil))
      nil))
    nil)
   ((one1 formal-const-decl "T1" isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (normal_subgroup_tran formula-decl nil groups_scaf nil)
    (fullset const-decl "set" sets nil)
    (group? const-decl "bool" group_def "algebra/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (G_TCC1 assuming-tcc nil isomorphism_theorems nil))
   nil))
 (quotient_subgroup_TCC2 0
  (quotient_subgroup_TCC2-1 nil 3524781199
   ("" (skosimp*)
    (("" (prop)
      (("1" (skosimp)
        (("1" (inst 1 "a!1")
          (("1" (hide -)
            (("1" (typepred "a!1" "M!1")
              (("1" (expand* "normal_subgroup?" "subgroup?")
                (("1" (flatten)
                  (("1" (expand* "subset?" "member")
                    (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide -1)
        (("2" (inst 1 "lc_gen(M!1, N!1, x!1)") (("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((T1 formal-type-decl nil isomorphism_theorems nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (one1 formal-const-decl "T1" isomorphism_theorems nil)
    (group? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subgroup? const-decl "bool" group_def "algebra/")
    (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (subgroup type-eq-decl nil group "algebra/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "set[T]" cosets "algebra/")
    (left_cosets type-eq-decl nil cosets "algebra/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets
     "algebra/"))
   nil))
 (quotient_subgroup_TCC3 0
  (quotient_subgroup_TCC3-1 nil 3524781199
   ("" (skosimp*)
    (("" (inst 1 "one1")
      (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil)
       ("2" (typepred "G!1")
        (("2" (expand* "group?" "monoid?" "monad?" "member")
          (("2" (flatten) nil nil)) nil))
        nil))
      nil))
    nil)
   ((G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (one1 formal-const-decl "T1" isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (left_coset_one formula-decl nil cosets "algebra/")
    (monoid? const-decl "bool" monoid_def "algebra/")
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def "algebra/")
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
 (quotient_subgroup_TCC4 0
  (quotient_subgroup_TCC4-1 nil 3524781199
   ("" (skosimp*)
    (("" (inst 1 "N!1")
      (("" (inst 1 "one1")
        (("1" (rewrite "left_coset_one[T1,*,one1]") nil nil)
         ("2" (typepred "G!1")
          (("2" (expand* "group?" "monoid?" "monad?" "member")
            (("2" (flatten) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T1 formal-type-decl nil isomorphism_theorems nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (one1 formal-const-decl "T1" isomorphism_theorems nil)
    (group? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "set[T]" cosets "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (left_cosets type-eq-decl nil cosets "algebra/")
    (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (monad? const-decl "bool" monad_def "algebra/")
    (member const-decl "bool" sets nil)
    (monoid? const-decl "bool" monoid_def "algebra/")
    (left_coset_one formula-decl nil cosets "algebra/"))
   nil))
 (quotient_subgroup 0
  (quotient_subgroup-1 nil 3524784283
   ("" (skosimp*)
    (("" (expand "subgroup?")
      (("" (prop)
        (("1" (hide -1)
          (("1" (expand* "subset?" "member")
            (("1" (skosimp*)
              (("1" (expand "/")
                (("1" (expand "restrict")
                  (("1" (expand "left_cosets")
                    (("1" (skosimp)
                      (("1" (inst?)
                        (("1" (hide -1)
                          (("1" (typepred "a!1" "M!1")
                            (("1"
                              (expand* "normal_subgroup?" "subgroup?"
                               "subset?" "member")
                              (("1"
                                (flatten)
                                (("1"
                                  (hide (-2 -4))
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide -1)
          (("2" (expand "group?")
            (("2" (prop)
              (("1" (expand "monoid?")
                (("1" (prop)
                  (("1" (expand "monad?")
                    (("1" (prop)
                      (("1" (expand "star_closed?")
                        (("1" (skosimp*)
                          (("1" (expand "member")
                            (("1" (expand "/")
                              (("1"
                                (expand "restrict")
                                (("1"
                                  (expand "left_cosets")
                                  (("1"
                                    (typepred "x!1" "y!1")
                                    (("1"
                                      (hide (-2 -4))
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst 1 "a!1 * a!2")
                                          (("1"
                                            (replaces -1)
                                            (("1"
                                              (replaces -1)
                                              (("1"
                                                (lemma
                                                 "mult_lem[T1, *, one1]")
                                                (("1"
                                                  (inst?)
                                                  (("1"
                                                    (hide 2)
                                                    (("1"
                                                      (typepred
                                                       "a!2"
                                                       "M!1")
                                                      (("1"
                                                        (expand*
                                                         "normal_subgroup?"
                                                         "subgroup?"
                                                         "subset?"
                                                         "member")
                                                        (("1"
                                                          (flatten)
                                                          (("1"
                                                            (hide
                                                             (-2 -4))
                                                            (("1"
                                                              (inst?)
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (typepred
                                                       "a!1"
                                                       "M!1")
                                                      (("2"
                                                        (expand*
                                                         "normal_subgroup?"
                                                         "subgroup?"
                                                         "subset?"
                                                         "member")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (hide
                                                             (-2 -4))
                                                            (("2"
                                                              (inst?)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide (-1 -2))
                                            (("2"
                                              (rewrite
                                               "product_in[T1, *, one1]")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand* "member" "/" "left_cosets")
                        (("2" (expand "restrict")
                          (("2" (typepred "M!1")
                            (("2"
                              (expand* "group?" "monoid?" "monad?"
                               "member")
                              (("2"
                                (flatten)
                                (("2"
                                  (hide-all-but (-2 1))
                                  (("2"
                                    (inst 1 "one1")
                                    (("2"
                                      (rewrite "left_coset_one")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (expand "identity?")
                        (("3" (skosimp*)
                          (("3" (expand "restrict")
                            (("3" (lemma "N_is_identity[T1, *, one1]")
                              (("3"
                                (inst?)
                                (("1"
                                  (flatten)
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (typepred "x!1")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (hide -)
                                          (("2"
                                            (typepred "a!1" "M!1")
                                            (("2"
                                              (expand*
                                               "normal_subgroup?"
                                               "subgroup?"
                                               "subset?"
                                               "member")
                                              (("2"
                                                (flatten)
                                                (("2"
                                                  (inst?)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "associative?")
                    (("2" (expand "restrict")
                      (("2" (skosimp*)
                        (("2" (typepred "z!1")
                          (("2" (typepred "y!1")
                            (("2" (typepred "x!1")
                              (("2"
                                (skosimp*)
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (hide -1)
                                    (("2"
                                      (replace -2)
                                      (("2"
                                        (hide -2)
                                        (("2"
                                          (replace -3)
                                          (("2"
                                            (hide -3)
                                            (("2"
                                              (rewrite
                                               "mult_lem[T1, *, one1]")
                                              (("1"
                                                (rewrite
                                                 "mult_lem[T1, *, one1]")
                                                (("1"
                                                  (rewrite
                                                   "mult_lem[T1, *, one1]")
                                                  (("1"
                                                    (rewrite
                                                     "mult_lem[T1, *, one1]")
                                                    (("1"
                                                      (rewrite
                                                       "assoc[T1, *, one1]")
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (hide-all-but 1)
                                                      (("2"
                                                        (typepred
                                                         "a!2"
                                                         "a!3"
                                                         "G!1"
                                                         "M!1")
                                                        (("2"
                                                          (expand
                                                           "normal_subgroup?")
                                                          (("2"
                                                            (flatten)
                                                            (("2"
                                                              (expand
                                                               "subgroup?")
                                                              (("2"
                                                                (expand
                                                                 "subset?")
                                                                (("2"
                                                                  (hide
                                                                   (-4
                                                                    -6))
                                                                  (("2"
                                                                    (copy
                                                                     -4)
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "a!2")
                                                                      (("2"
                                                                        (inst
                                                                         -5
                                                                         "a!3")
                                                                        (("2"
                                                                          (expand
                                                                           "member")
                                                                          (("2"
                                                                            (expand*
                                                                             "group?"
                                                                             "monoid?"
                                                                             "monad?")
                                                                            (("2"
                                                                              (flatten)
                                                                              (("2"
                                                                                (hide-all-but
                                                                                 (-1
                                                                                  -4
                                                                                  -9
                                                                                  1))
                                                                                (("2"
                                                                                  (expand
                                                                                   "star_closed?")
                                                                                  (("2"
                                                                                    (inst?)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "member")
                                                                                      (("2"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("3"
                                                      (hide-all-but 1)
                                                      (("3"
                                                        (typepred
                                                         "a!1"
                                                         "M!1")
                                                        (("3"
                                                          (expand*
                                                           "normal_subgroup?"
                                                           "subgroup?"
                                                           "subset?"
                                                           "member")
                                                          (("3"
                                                            (flatten)
                                                            (("3"
                                                              (hide
                                                               (-2 -4))
                                                              (("3"
                                                                (inst?)
                                                                (("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (typepred
                                                       "a!3"
                                                       "M!1")
                                                      (("2"
                                                        (expand*
                                                         "normal_subgroup?"
                                                         "subgroup?"
                                                         "subset?"
                                                         "member")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (hide
                                                             (-2 -4))
                                                            (("2"
                                                              (inst?)
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("3"
                                                    (hide-all-but 1)
                                                    (("3"
                                                      (typepred
                                                       "a!2"
                                                       "M!1")
                                                      (("3"
                                                        (expand*
                                                         "normal_subgroup?"
                                                         "subgroup?"
                                                         "subset?"
                                                         "member")
                                                        (("3"
                                                          (flatten)
                                                          (("3"
                                                            (hide
                                                             (-2 -4))
                                                            (("3"
                                                              (inst?)
                                                              (("3"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide-all-but 1)
                                                  (("2"
                                                    (typepred
                                                     "a!3"
                                                     "M!1")
                                                    (("2"
                                                      (expand*
                                                       "normal_subgroup?"
                                                       "subgroup?"
                                                       "subset?"
                                                       "member")
                                                      (("2"
                                                        (flatten)
                                                        (("2"
                                                          (hide
                                                           (-2 -4))
                                                          (("2"
                                                            (inst?)
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (hide-all-but 1)
                                                  (("3"
                                                    (typepred
                                                     "a!1"
                                                     "a!2"
                                                     "G!1"
                                                     "M!1")
                                                    (("3"
                                                      (expand
                                                       "normal_subgroup?")
                                                      (("3"
                                                        (flatten)
                                                        (("3"
                                                          (expand
                                                           "subgroup?")
                                                          (("3"
                                                            (expand
                                                             "subset?")
                                                            (("3"
                                                              (hide
                                                               (-4 -6))
                                                              (("3"
                                                                (copy
                                                                 -4)
                                                                (("3"
                                                                  (inst
                                                                   -1
                                                                   "a!1")
                                                                  (("3"
                                                                    (inst
                                                                     -5
                                                                     "a!2")
                                                                    (("3"
                                                                      (expand
                                                                       "member")
                                                                      (("3"
                                                                        (expand*
                                                                         "group?"
                                                                         "monoid?"
                                                                         "monad?")
                                                                        (("3"
                                                                          (flatten)
                                                                          (("3"
                                                                            (hide-all-but
                                                                             (-1
                                                                              -4
                                                                              -9
                                                                              1))
                                                                            (("3"
                                                                              (expand
                                                                               "star_closed?")
                                                                              (("3"
                                                                                (inst?)
                                                                                (("3"
                                                                                  (expand
                                                                                   "member")
                                                                                  (("3"
                                                                                    (propax)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide-all-but 1)
                                                (("2"
                                                  (typepred
                                                   "a!2"
                                                   "M!1")
                                                  (("2"
                                                    (expand*
                                                     "normal_subgroup?"
                                                     "subgroup?"
                                                     "subset?"
                                                     "member")
                                                    (("2"
                                                      (flatten)
                                                      (("2"
                                                        (hide (-2 -4))
                                                        (("2"
                                                          (inst?)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (hide-all-but 1)
                                                (("3"
                                                  (typepred
                                                   "a!1"
                                                   "M!1")
                                                  (("3"
                                                    (expand*
                                                     "normal_subgroup?"
                                                     "subgroup?"
                                                     "subset?"
                                                     "member")
                                                    (("3"
                                                      (flatten)
                                                      (("3"
                                                        (hide (-2 -4))
                                                        (("3"
                                                          (inst?)
                                                          (("3"
                                                            (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)
               ("2" (expand "inv_exists?")
                (("2" (skosimp*)
                  (("2" (typepred "x!1")
                    (("2" (skosimp*)
                      (("2"
                        (inst 1
                         "*[T1, *, one1](inv[T1, *, one1](a!1), N!1)")
                        (("1" (replace -1)
                          (("1" (hide -1)
                            (("1" (rewrite "mult_lem[T1, *, one1]")
                              (("1"
                                (rewrite "mult_lem[T1, *, one1]")
                                (("1"
                                  (rewrite "inv_right[T1, *, one1]")
                                  (("1"
                                    (rewrite "inv_left[T1, *, one1]")
                                    (("1"
                                      (rewrite "left_coset_one")
                                      nil
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2"
                                    (typepred "a!1" "M!1")
                                    (("2"
                                      (expand*
                                       "normal_subgroup?"
                                       "subgroup?"
                                       "subset?"
                                       "member")
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (hide (-2 -4))
                                          (("2"
                                            (inst?)
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide-all-but 1)
                                  (("3"
                                    (typepred "a!1" "M!1")
                                    (("3"
                                      (expand*
                                       "normal_subgroup?"
                                       "subgroup?"
                                       "subset?"
                                       "member")
                                      (("3"
                                        (flatten)
                                        (("3"
                                          (hide (-2 -4))
                                          (("3"
                                            (inst?)
                                            (("3"
                                              (assert)
                                              (("3"
                                                (rewrite
                                                 "inv_in[T1, *, one1]")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (typepred "a!1" "M!1")
                                  (("2"
                                    (expand*
                                     "normal_subgroup?"
                                     "subgroup?"
                                     "subset?"
                                     "member")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (hide (-2 -4))
                                        (("2"
                                          (inst?)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (rewrite
                                               "inv_in[T1, *, one1]")
                                              nil
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (hide-all-but 1)
                                (("3"
                                  (typepred "a!1" "M!1")
                                  (("3"
                                    (expand*
                                     "normal_subgroup?"
                                     "subgroup?"
                                     "subset?"
                                     "member")
                                    (("3"
                                      (flatten)
                                      (("3"
                                        (hide (-2 -4))
                                        (("3"
                                          (inst?)
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (prop)
                          (("1" (expand "*")
                            (("1" (inst + "inv[T1, *, one1](a!1)")
                              (("1"
                                (rewrite "inv_in[T1, *, one1]")
                                nil
                                nil))
                              nil))
                            nil)
                           ("2" (expand "/")
                            (("2" (hide -2)
                              (("2"
                                (expand "restrict")
                                (("2"
                                  (expand "left_cosets")
                                  (("2"
                                    (inst 1 "inv[T1, *, one1](a!1)")
                                    (("2"
                                      (rewrite "inv_in[T1, *, one1]")
                                      nil
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subgroup? const-decl "bool" group_def "algebra/")
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (a!2 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (mult_lem formula-decl nil factor_groups "algebra/")
    (product_in formula-decl nil group "algebra/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "set[T]" cosets "algebra/")
    (left_cosets type-eq-decl nil cosets "algebra/")
    (mult const-decl "left_cosets(G, H)" factor_groups "algebra/")
    (star_closed? const-decl "bool" groupoid_def "algebra/")
    (left_coset_one formula-decl nil cosets "algebra/")
    (N_is_identity formula-decl nil factor_groups "algebra/")
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (x!1 skolem-const-decl "(M!1 / N!1)" isomorphism_theorems nil)
    (identity? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def "algebra/")
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (a!3 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (a!2 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (assoc formula-decl nil group "algebra/")
    (associative? const-decl "bool" operator_defs nil)
    (monoid? const-decl "bool" monoid_def "algebra/")
    (inv_in formula-decl nil group "algebra/")
    (inv_right formula-decl nil group "algebra/")
    (inv_left formula-decl nil group "algebra/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (inv const-decl "{y | x * y = one AND y * x = one}" group
     "algebra/")
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (inv_exists? const-decl "bool" group_def "algebra/")
    (restrict const-decl "R" restrict nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (M!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (a!1 skolem-const-decl "(M!1)" isomorphism_theorems nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (one1 formal-const-decl "T1" isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (left_cosets const-decl "setofsets[T]" right_left_cosets nil)
    (/ const-decl "group[left_cosets(G, N), mult(G, N), N]"
       right_left_cosets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   shostak))
 (second_isomorphism_th_aux_TCC1 0
  (second_isomorphism_th_aux_TCC1-1 nil 3524841142
   ("" (skosimp*)
    (("" (replaces -1)
      (("" (lemma "HK_subgroup[T1, *, one1]")
        (("" (inst -1 "G!1" "H!1" "N!1")
          (("1" (assert)
            (("1" (lemma "HK_subgroup_permute[T1, *, one1]")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (expand "subgroup?") (("1" (propax) nil nil))
                    nil))
                  nil)
                 ("2" (hide (-1 2))
                  (("2" (typepred "N!1")
                    (("2" (expand "normal_subgroup?")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (typepred "N!1")
            (("2" (expand "normal_subgroup?") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subgroup type-eq-decl nil group "algebra/")
    (HK_subgroup_permute formula-decl nil products_subgroups nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (HK_subgroup formula-decl nil products_subgroups nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (one1 formal-const-decl "T1" isomorphism_theorems nil))
   nil))
 (second_isomorphism_th_aux_TCC2 0
  (second_isomorphism_th_aux_TCC2-1 nil 3524841142
   ("" (skosimp*)
    (("" (replaces -2)
      (("" (replaces -1)
        (("" (lemma "HK_subgroup[T1, *, one1]")
          (("" (inst -1 "G!1" "H!1" "N!1")
            (("1" (assert)
              (("1" (lemma "HK_subgroup_permute[T1, *, one1]")
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (replaces -1)
                      (("1" (lemma "H_K_are_subgroups[T1, *, one1]")
                        (("1" (inst?)
                          (("1" (prop)
                            (("1" (hide -2)
                              (("1"
                                (lemma
                                 "normal_subgroup_tran[T1, *, one1]")
                                (("1"
                                  (inst
                                   -1
                                   "G!1"
                                   "prod[T1, *, one1](N!1, H!1)"
                                   "N!1")
                                  (("1" (assert) nil nil))
                                  nil)
                                 ("2" (rewrite "G_TCC1") nil nil))
                                nil))
                              nil)
                             ("2" (expand "subgroup?")
                              (("2" (assert) nil nil)) nil))
                            nil)
                           ("2" (typepred "N!1")
                            (("2" (expand "normal_subgroup?" -2)
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (typepred "N!1")
                      (("2" (expand "normal_subgroup?")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (typepred "N!1")
                (("2" (expand "normal_subgroup?")
                  (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (subgroup type-eq-decl nil group "algebra/")
    (HK_subgroup_permute formula-decl nil products_subgroups nil)
    (H_K_are_subgroups formula-decl nil products_subgroups nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (normal_subgroup_tran formula-decl nil groups_scaf nil)
    (fullset const-decl "set" sets nil)
    (prod const-decl "set[T]" products_subgroups nil)
    (G_TCC1 assuming-tcc nil isomorphism_theorems nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (HK_subgroup formula-decl nil products_subgroups nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (one1 formal-const-decl "T1" isomorphism_theorems nil))
   nil))
 (second_isomorphism_th_aux_TCC3 0
  (second_isomorphism_th_aux_TCC3-1 nil 3524841142
   ("" (skosimp*)
    (("" (inst 1 "one1")
      (("1" (rewrite "left_coset_one") nil nil)
       ("2" (replaces -1)
        (("2" (lemma "HK_subgroup[T1, *, one1]")
          (("2" (inst -1 "G!1" "H!1" "N!1")
            (("1" (assert)
              (("1" (lemma "HK_subgroup_permute[T1, *, one1]")
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (replaces -1)
                      (("1"
                        (expand* "subgroup?" "group?" "monoid?"
                         "monad?" "member")
                        nil nil))
                      nil))
                    nil)
                   ("2" (typepred "N!1")
                    (("2" (expand "normal_subgroup?")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (typepred "N!1")
              (("2" (expand "normal_subgroup?")
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((one1 formal-const-decl "T1" isomorphism_theorems nil)
    (NH!1 skolem-const-decl "set[T1]" isomorphism_theorems nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil isomorphism_theorems nil)
    (* formal-const-decl "[T1, T1 -> T1]" isomorphism_theorems nil)
    (normal_subgroup type-eq-decl nil normal_subgroups "algebra/")
    (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (left_coset_one formula-decl nil cosets "algebra/")
    (HK_subgroup formula-decl nil products_subgroups nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def "algebra/")
    (monoid? const-decl "bool" monoid_def "algebra/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (HK_subgroup_permute formula-decl nil products_subgroups nil)
    (subgroup type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (G!1 skolem-const-decl "group[T1, *, one1]" isomorphism_theorems
     nil)
    (N!1 skolem-const-decl "normal_subgroup[T1, *, one1](G!1)"
     isomorphism_theorems nil))
   nil))
 (second_isomorphism_th_aux_TCC4 0
  (second_isomorphism_th_aux_TCC4-1 nil 3524841142
   ("" (skosimp*)
    (("" (rewrite "left_cosets_group[T1, *, one1]")
      (("1" (hide 2)
        (("1" (replaces -1)
          (("1" (lemma "HK_subgroup[T1, *, one1]")
            (("1" (inst -1 "G!1" "H!1" "N!1")
              (("1" (assert)
                (("1" (lemma "HK_subgroup_permute[T1, *, one1]")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (replaces -1)
                        (("1" (lemma "H_K_are_subgroups[T1, *, one1]")
                          (("1" (inst?)
                            (("1" (prop)
                              (("1"
                                (hide -2)
                                (("1"
                                  (lemma
                                   "normal_subgroup_tran[T1, *, one1]")
                                  (("1"
                                    (inst
                                     -1
                                     "G!1"
                                     "prod[T1, *, one1](N!1, H!1)"
                                     "N!1")
                                    (("1" (assert) nil nil))
                                    nil)
                                   ("2" (rewrite "G_TCC1") nil nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "subgroup?")
                                (("2" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (typepred "N!1")
                                (("2"
                                  (expand "normal_subgroup?")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2)
                      (("2" (typepred "N!1")
                        (("2" (expand "normal_subgroup?")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (typepred "N!1")
                  (("2" (expand "normal_subgroup?")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (replaces -1)
          (("2" (lemma "HK_subgroup[T1, *, one1]")
            (("2" (inst -1 "G!1" "H!1" "N!1")
              (("1" (assert)
                (("1" (lemma "HK_subgroup_permute[T1, *, one1]")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (replaces -1)
                        (("1"
                          (expand* "subgroup?" "group?" "monoid?"
                           "monad?" "member" -1)
                          nil nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1)
--> --------------------

--> maximum size reached

--> --------------------

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