Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: sylow_theorems.prf Sprache: Lisp

Original von: PVS^©

(sylow_theorems
(IMP_finite_groups_TCC1 0
  (IMP_finite_groups_TCC1-1 nil 3531235292
   ("" (rewrite "T_is_group") nil nil)
   ((T_is_group formula-decl nil sylow_theorems nil)) nil))
(p_subgroup_sylow?_TCC1 0
  (p_subgroup_sylow?_TCC1-1 nil 3531141392
   ("" (skosimp*)
    (("" (typepred "P!1" "G!1")
      (("" (hide -1)
        (("" (lemma "finite_subgroups")
          (("" (inst?) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((subgroup type-eq-decl nil group "algebra/")
    (finite_group nonempty-type-eq-decl nil group "algebra/")
    (finite_group? const-decl "bool" group_def "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (one formal-const-decl "T" sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sylow_theorems nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_subgroups formula-decl nil group "algebra/"))
   nil))
(p_subgroup_sylow?_TCC2 0
  (p_subgroup_sylow?_TCC2-1 nil 3531141392
   ("" (skosimp*)
    (("" (hide -1)
      (("" (typepred "H!1" "G!1")
        (("" (hide -1)
          (("" (lemma "finite_subgroups")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_subgroups formula-decl nil group "algebra/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (one formal-const-decl "T" sylow_theorems nil)
    (group? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (finite_group? const-decl "bool" group_def "algebra/")
    (finite_group nonempty-type-eq-decl nil group "algebra/")
    (subgroup type-eq-decl nil group "algebra/"))
   nil))
(subgroup_is_factor_TCC1 0
  (subgroup_is_factor_TCC1-1 nil 3530954477
   ("" (skosimp)
    (("" (inst 1 "one")
      (("1" (rewrite "left_coset_one[T,*,one]") nil nil)
       ("2" (typepred "G!1")
        (("2" (expand* "group?" "monoid?" "monad?" "member")
          (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((G!1 skolem-const-decl "group[T, *, one]" sylow_theorems nil)
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (one formal-const-decl "T" sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil sylow_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))
(subgroup_is_factor_TCC2 0
  (subgroup_is_factor_TCC2-1 nil 3530954477
   ("" (skosimp*)
    (("" (rewrite "left_cosets_group[T, *, one]") nil nil)) nil)
   ((left_cosets_group formula-decl nil factor_groups "algebra/")
    (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 "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/")
    (T formal-type-decl nil sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (one formal-const-decl "T" sylow_theorems nil))
   nil))
(subgroup_is_factor_TCC3 0
  (subgroup_is_factor_TCC3-1 nil 3530954477
   ("" (skosimp*)
    (("" (typepred "N!1")
      (("" (hide -1)
        (("" (lemma "normal_subgroup_tran[T, *, one]")
          (("1" (inst -1 "G!1" "H!1" "N!1") (("1" (assert) nil nil))
            nil)
           ("2" (hide (-1 -2 2)) (("2" (rewrite "T_is_group") nil nil))
            nil))
          nil))
        nil))
      nil))
    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/")
    (one formal-const-decl "T" sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sylow_theorems nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (normal_subgroup_tran formula-decl nil groups_scaf nil)
    (fullset const-decl "set" sets nil)
    (subgroup type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (T_is_group formula-decl nil sylow_theorems nil))
   nil))
(subgroup_is_factor_TCC4 0
  (subgroup_is_factor_TCC4-1 nil 3530981159
   ("" (skosimp*)
    (("" (prop)
      (("1" (hide (-2 -3))
        (("1" (skosimp)
          (("1" (inst?)
            (("1" (hide -1)
              (("1" (typepred "a!1" "H!1")
                (("1" (expand* "subgroup?" "subset?" "member")
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide -1)
        (("2" (expand "/")
          (("2" (expand "restrict")
            (("2" (expand "left_cosets") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (G!1 skolem-const-decl "group[T, *, one]" sylow_theorems nil)
    (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" sylow_theorems
     nil)
    (a!1 skolem-const-decl "(H!1)" sylow_theorems nil)
    (subgroup type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (one formal-const-decl "T" sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil sylow_theorems nil)
    (/ const-decl "group[left_cosets(G, N), mult(G, N), N]"
       right_left_cosets nil)
    (left_cosets const-decl "setofsets[T]" right_left_cosets nil)
    (restrict const-decl "R" restrict nil))
   nil))
(subgroup_is_factor 0
  (subgroup_is_factor-1 nil 3530954523
   ("" (skosimp*)
    (("" (lemma "natural_homo[T, *, one,T, *, one]")
      (("1" (inst -1 "G!1" "N!1")
        (("1" (skosimp)
          (("1"
            (lemma
             "correspondence_theorem[T,*,one,left_cosets(G!1,N!1),mult(G!1,N!1),N!1]")
            (("1" (inst?)
              (("1" (assert)
                (("1" (skosimp)
                  (("1" (expand "bijective?")
                    (("1" (flatten)
                      (("1" (hide -7)
                        (("1" (expand "surjective?")
                          (("1" (inst -3 "S!1")
                            (("1" (skosimp)
                              (("1"
                                (inst 1 "x!1")
                                (("1"
                                  (prop)
                                  (("1"
                                    (typepred "x!1")
                                    (("1"
                                      (hide-all-but (-1 -3 -10 1))
                                      (("1"
                                        (replace -3 -2 rl)
                                        (("1"
                                          (hide -3)
                                          (("1"
                                            (expand "subgroup?")
                                            (("1" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide (-2 -4))
                                    (("2"
                                      (replaces -1)
                                      (("2"
                                        (replace -1 1 rl)
                                        (("2"
                                          (hide -1)
                                          (("2"
                                            (decompose-equality 1)
                                            (("1"
                                              (iff)
                                              (("1"
                                                (prop)
                                                (("1"
                                                  (expand "extend")
                                                  (("1"
                                                    (prop)
                                                    (("1"
                                                      (hide -1)
                                                      (("1"
                                                        (expand
                                                         "image")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (decompose-equality
                                                             -2)
                                                            (("1"
                                                              (inst
                                                               -1
                                                               "x!3")
                                                              (("1"
                                                                (expand
                                                                 "/")
                                                                (("1"
                                                                  (expand*
                                                                   "restrict"
                                                                   "left_cosets")
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (typepred
                                                                       "x!3")
                                                                      (("2"
                                                                        (expand
                                                                         "restrict")
                                                                        (("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "extend")
                                                  (("2"
                                                    (prop)
                                                    (("1"
                                                      (expand "image")
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (expand*
                                                           "/"
                                                           "restrict"
                                                           "left_cosets")
                                                          (("1"
                                                            (skosimp)
                                                            (("1"
                                                              (inst
                                                               1
                                                               "a!1")
                                                              (("1"
                                                                (decompose-equality
                                                                 -2)
                                                                (("1"
                                                                  (inst?)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (typepred
                                                                 "a!1"
                                                                 "x!1")
                                                                (("2"
                                                                  (hide
                                                                   (-2
                                                                    -4
                                                                    -5
                                                                    -6))
                                                                  (("2"
                                                                    (expand*
                                                                     "subgroup?"
                                                                     "subset?"
                                                                     "member")
                                                                    (("2"
                                                                      (inst?)
                                                                      (("2"
                                                                        (expand
                                                                         "restrict")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide -2)
                                                      (("2"
                                                        (expand*
                                                         "/"
                                                         "restrict"
                                                         "left_cosets")
                                                        (("2"
                                                          (skosimp)
                                                          (("2"
                                                            (typepred
                                                             "a!1"
                                                             "x!1")
                                                            (("2"
                                                              (hide
                                                               (-2 -4))
                                                              (("2"
                                                                (expand*
                                                                 "subgroup?"
                                                                 "subset?"
                                                                 "member")
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (inst?)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide (-1 2))
                                              (("2"
                                                (skosimp)
                                                (("2"
                                                  (rewrite
                                                   "T_is_group")
                                                  nil
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (hide-all-but 1)
                                              (("3"
                                                (rewrite "T_is_group")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide-all-but 1)
                (("2" (rewrite "T_is_group") nil nil)) nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (rewrite "left_cosets_group[T, *, one]") nil nil))
              nil)
             ("3" (hide-all-but 1)
              (("3" (inst 1 "one")
                (("1" (rewrite "left_coset_one[T, *, one]") nil nil)
                 ("2" (rewrite "one_in") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide-all-but 1) (("2" (rewrite "T_is_group") nil nil))
        nil))
      nil))
    nil)
   ((one formal-const-decl "T" sylow_theorems nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (T formal-type-decl nil sylow_theorems nil)
    (natural_homo formula-decl nil homomorphism_lemmas 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)
    (monad nonempty-type-eq-decl nil monad "algebra/")
    (monad? const-decl "bool" monad_def "algebra/")
    (one_in formula-decl nil monad "algebra/")
    (left_coset_one formula-decl nil cosets "algebra/")
    (left_cosets_group formula-decl nil factor_groups "algebra/")
    (/ const-decl "group[left_cosets(G, N), mult(G, N), N]"
       right_left_cosets nil)
    (homomorphism? const-decl "bool" homomorphisms "algebra/")
    (homomorphism type-eq-decl nil homomorphisms "algebra/")
    (surjective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T_is_group formula-decl nil sylow_theorems nil)
    (a!1 skolem-const-decl "(x!1)" sylow_theorems nil)
    (a!1 skolem-const-decl "(x!1)" sylow_theorems nil)
    (member const-decl "bool" sets nil)
    (left_cosets const-decl "setofsets[T]" right_left_cosets nil)
    (x!3 skolem-const-decl "(restrict[T, (G!1), bool](x!1))"
     sylow_theorems nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (image const-decl "set[R]" function_image nil)
    (restrict const-decl "R" restrict nil)
    (G!1 skolem-const-decl "group[T, *, one]" sylow_theorems nil)
    (N!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)"
     sylow_theorems nil)
    (pi!1 skolem-const-decl "[(G!1) -> (G!1 / N!1)]" sylow_theorems
     nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (x!1 skolem-const-decl
     "subgroup_contain[T, *, one](G!1, kernel(G!1, G!1 / N!1)(pi!1))"
     sylow_theorems nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subset? const-decl "bool" sets nil)
    (kernel const-decl "subgroup[T1, *, one1](G)" homomorphisms
     "algebra/")
    (subgroup_contain type-eq-decl nil groups_scaf nil)
    (subgroup? const-decl "bool" group_def "algebra/")
    (subgroup type-eq-decl nil group "algebra/")
    (bijective? const-decl "bool" functions nil)
    (correspondence_theorem formula-decl nil isomorphism_theorems nil)
    (= 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/")
    (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/"))
   shostak))
(First_Sylow_Theorem_TCC1 0
  (First_Sylow_Theorem_TCC1-1 nil 3531043400 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)
    (divides const-decl "bool" divides nil)
    (prime? const-decl "bool" primes "ints/"))
   nil))
(First_Sylow_Theorem_TCC2 0
  (First_Sylow_Theorem_TCC2-1 nil 3531043400 ("" (subtype-tcc) nil nil)
   ((order const-decl "posnat" monad "algebra/")
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (divides const-decl "bool" divides nil)
    (prime? const-decl "bool" primes "ints/")
    (posnat_expt application-judgement "posnat" exponentiation nil))
   nil))
(First_Sylow_Theorem_TCC3 0
  (First_Sylow_Theorem_TCC3-1 nil 3531043400
   ("" (skosimp*)
    (("" (hide -)
      (("" (typepred "G!1" "H!1")
        (("" (lemma "finite_subgroups[T, *, one]")
          (("" (inst?)
            (("" (assert)
              (("" (hide (-2 -4))
                (("" (expand* "group?" "finite_group?" "finite_monad?")
                  (("" (expand "monoid?")
                    (("" (flatten) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_subgroups formula-decl nil group "algebra/")
    (finite_monad? const-decl "bool" monad_def "algebra/")
    (monoid? const-decl "bool" monoid_def "algebra/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (one formal-const-decl "T" sylow_theorems nil)
    (finite_group? const-decl "bool" group_def "algebra/")
    (finite_group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (subgroup type-eq-decl nil group "algebra/"))
   nil))
(First_Sylow_Theorem_TCC4 0
  (First_Sylow_Theorem_TCC4-1 nil 3531043400 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)
    (divides const-decl "bool" divides nil)
    (prime? const-decl "bool" primes "ints/")
    (order const-decl "posnat" monad "algebra/")
    (^ const-decl "real" exponentiation nil)
    (gcd const-decl "{k: posnat | divides(k, i) AND divides(k, j)}" gcd
         "ints/")
    (posnat_expt application-judgement "posnat" exponentiation nil))
   nil))
(First_Sylow_Theorem_TCC5 0
  (First_Sylow_Theorem_TCC5-1 nil 3531043400
   ("" (skosimp*)
    (("" (hide -) (("" (typepred "i!1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   nil))
(First_Sylow_Theorem_TCC6 0
  (First_Sylow_Theorem_TCC6-1 nil 3531043400
   ("" (skosimp*)
    (("" (hide -)
      (("" (typepred "G!1" "K!1")
        (("" (lemma "finite_subgroups[T, *, one]")
          (("" (inst?)
            (("" (assert)
              (("" (hide (-2 -4))
                (("" (expand* "group?" "finite_group?" "finite_monad?")
                  (("" (expand "monoid?")
                    (("" (flatten) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_subgroups formula-decl nil group "algebra/")
    (finite_monad? const-decl "bool" monad_def "algebra/")
    (monoid? const-decl "bool" monoid_def "algebra/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil sylow_theorems nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" sylow_theorems nil)
    (one formal-const-decl "T" sylow_theorems nil)
    (finite_group? const-decl "bool" group_def "algebra/")
    (finite_group nonempty-type-eq-decl nil group "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (group nonempty-type-eq-decl nil group "algebra/")
    (subgroup? const-decl "bool" group_def "algebra/")
    (subgroup type-eq-decl nil group "algebra/"))
   nil))
(First_Sylow_Theorem 0
  (First_Sylow_Theorem-1 nil 3531043866
   ("" (induct "i")
    (("1" (hide 2)
      (("1" (typepred "i!1") (("1" (propax) nil nil)) nil)) nil)
     ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (case-replace "j!1 = 0" :hide? T)
        (("1" (hide (-1 -2 -5 -6))
          (("1" (lemma "cauchy_cor[T,*,one]")
            (("1" (inst -1 "G!1" "p!1")
              (("1" (prop)
                (("1" (rewrite "expt_x1") nil nil)
                 ("2" (skosimp*)
                  (("2" (assert)
                    (("2" (rewrite "expt_x1")
                      (("2" (rewrite "expt_x0")
                        (("2" (inst 1 "H!1")
                          (("2" (assert)
                            (("2" (lemma "one_is_subgroup")
                              (("2"
                                (inst -1 "H!1")
                                (("2"
                                  (lemma "order_is_1")
                                  (("2"
                                    (inst?)
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "one_group")
                                        (("2"
                                          (replace -1 -2 rl)
                                          (("2"
                                            (expand "normal_subgroup?")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (expand*
                                                   "subset?"
                                                   "member")
                                                  (("2"
                                                    (skosimp)
                                                    (("2"
                                                      (expand "*")
                                                      (("2"
                                                        (skosimp)
                                                        (("2"
                                                          (typepred
                                                           "h!1")
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (typepred
                                                               "h!2")
                                                              (("2"
                                                                (replaces
                                                                 -3)
                                                                (("2"
                                                                  (expand
                                                                   "singleton")
                                                                  (("2"
                                                                    (replaces
                                                                     -1)
                                                                    (("2"
                                                                      (replaces
                                                                       -1)
                                                                      (("2"
                                                                        (rewrite
                                                                         "one_right")
                                                                        (("2"
                                                                          (rewrite
                                                                           "inv_left")
                                                                          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)
                 ("3" (hide 1)
                  (("3" (lemma "divides_power")
                    (("3" (inst?)
                      (("3" (replaces -3)
                        (("3" (hide -2)
                          (("3" (rewrite "divides_prod1") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("4" (hide 1)
                  (("4" (lemma "divides_power")
                    (("4" (inst?)
                      (("4" (replaces -3)
                        (("4" (hide -2)
                          (("4" (rewrite "divides_prod1") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide (- 2)) (("2" (rewrite "T_is_group") nil nil))
              nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (prop)
            (("1" (inst -1 "m!1" "n!1" "p!1" "G!1")
              (("1" (assert)
                (("1" (flatten)
                  (("1" (hide -2)
                    (("1" (skosimp)
                      (("1" (lemma "normalizer_index[T,*,one]")
                        (("1" (inst -1 "p!1" "G!1" "H!1")
                          (("1" (prop)
                            (("1" (lemma "card_factor[T,*,one]")
                              (("1"
                                (inst?)
                                (("1"
                                  (prop)
                                  (("1"
                                    (rewrite
                                     "card_extend[set[T], left_cosets[T, *, one](normalizer(G!1, H!1), H!1)]")
                                    (("1"
                                      (replace -1 -2 rl)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (lemma
                                           "cauchy_cor[left_cosets(normalizer(G!1, H!1),H!1),mult(normalizer(G!1, H!1),H!1),H!1]")
                                          (("1"
                                            (inst
                                             -1
                                             "normalizer(G!1, H!1) / H!1"
                                             "p!1")
                                            (("1"
                                              (prop)
                                              (("1"
                                                (skosimp)
                                                (("1"
                                                  (lemma
                                                   "subgroup_is_factor")
                                                  (("1"
                                                    (inst
                                                     -1
                                                     "normalizer(G!1, H!1)"
                                                     "H!1"
                                                     "H!2")
                                                    (("1"
                                                      (skosimp)
                                                      (("1"
                                                        (hide -4)
                                                        (("1"
                                                          (replaces -2)
                                                          (("1"
                                                            (lemma
                                                             "Lagrange_index[T,*,one]")
                                                            (("1"
                                                              (inst
                                                               -1
                                                               "H!3"
                                                               "H!1")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "card_factor[T,*,one]")
                                                                  (("1"
                                                                    (inst
                                                                     -1
                                                                     "H!3"
                                                                     "H!1")
                                                                    (("1"
                                                                      (prop)
                                                                      (("1"
                                                                        (rewrite
                                                                         "card_extend[set[T], left_cosets[T, *, one](H!3, H!1)]")
                                                                        (("1"
                                                                          (replace
                                                                           -1
                                                                           -2
                                                                           rl)
                                                                          (("1"
                                                                            (hide
                                                                             -1)
                                                                            (("1"
                                                                              (replace
                                                                               -4
                                                                               -1)
                                                                              (("1"
                                                                                (case-replace
                                                                                 "card(H!3 / H!1) = p!1"
                                                                                 :hide?
                                                                                 T)
                                                                                (("1"
                                                                                  (inst
                                                                                   1
                                                                                   "H!3")
                                                                                  (("1"
                                                                                    (hide-all-but
                                                                                     (-1
                                                                                      1
                                                                                      2))
                                                                                    (("1"
                                                                                      (rewrite
                                                                                       "expt_plus")
                                                                                      (("1"
                                                                                        (rewrite
                                                                                         "expt_x1")
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide-all-but
                                                                                     1)
                                                                                    (("2"
                                                                                      (typepred
                                                                                       "H!3")
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("2"
                                                                                          (lemma
                                                                                           "normalizer_is_subgroup[T, *, one]")
                                                                                          (("2"
                                                                                            (inst?)
                                                                                            (("2"
                                                                                              (assert)
                                                                                              (("2"
                                                                                                (lemma
                                                                                                 "subgroup_transitive[T, *, one]")
                                                                                                (("2"
                                                                                                  (inst
                                                                                                   -1
                                                                                                   "G!1"
                                                                                                   "normalizer(G!1, H!1)"
                                                                                                   "H!3")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (hide-all-but
                                                                                                     1)
                                                                                                    (("2"
                                                                                                      (rewrite
                                                                                                       "T_is_group")
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   (-3
                                                                                    1))
                                                                                  (("2"
                                                                                    (expand
                                                                                     "order")
                                                                                    (("2"
                                                                                      (rewrite
                                                                                       "card_def[left_cosets(normalizer(G!1, H!1), H!1)]")
                                                                                      (("2"
                                                                                        (rewrite
                                                                                         "card_def[left_cosets[T, *, one](H!3, H!1)]")
                                                                                        (("2"
                                                                                          (replace
                                                                                           -1
                                                                                           1
                                                                                           rl)
                                                                                          (("2"
                                                                                            (hide
                                                                                             -1)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "Card")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "inj_set")
                                                                                                (("2"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           1)
                                                                          (("2"
                                                                            (expand
                                                                             "/")
                                                                            (("2"
                                                                              (lemma
                                                                               "restrict_finite[setof[T], left_cosets[T, *, one](H!3, H!1)]")
                                                                              (("2"
                                                                                (inst?)
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (hide
                                                                                     2)
                                                                                    (("1"
                                                                                      (lemma
                                                                                       "left_cosets_partition[T,*,one]")
                                                                                      (("1"
                                                                                        (inst?)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "finite_partition?")
                                                                                          (("1"
                                                                                            (propax)
                                                                                            nil
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (typepred
                                                                                           "H!3")
                                                                                          (("2"
                                                                                            (hide
                                                                                             (-1
                                                                                              2))
                                                                                            (("2"
                                                                                              (lemma
                                                                                               "normalizer_is_subgroup[T, *, one]")
                                                                                              (("2"
                                                                                                (inst?)
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "G!1")
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "finite_subgroups")
                                                                                                      (("2"
                                                                                                        (inst?)
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "finite_subgroups")
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -1
                                                                                                               "H!3"
                                                                                                               "normalizer(G!1, H!1)")
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                nil
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (hide-all-but
                                                                                                                 1)
                                                                                                                (("2"
                                                                                                                  (rewrite
                                                                                                                   "T_is_group")
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (hide-all-but
                                                                                                           1)
                                                                                                          (("2"
                                                                                                            (rewrite
                                                                                                             "T_is_group")
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (rewrite
                                                                                     "T_is_group")
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
--> --------------------

--> maximum size reached

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

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