Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: complex_field.prf Sprache: Lisp

Original von: PVS^©

(complex_field
(fullset_is_field 0
  (fullset_is_field-2 nil 3408269025
   ("" (expand "fullset")
    (("" (expand "field?")
      (("" (expand "division_ring?")
        (("" (expand "ring_with_one?")
          (("" (expand "ring?")
            (("" (expand "restrict")
              (("" (expand "left_distributive?")
                (("" (expand "right_distributive?")
                  (("" (expand "abelian_group?")
                    (("" (expand "group?")
                      (("" (expand "monoid?")
                        (("" (expand "monad?")
                          (("" (expand "restrict")
                            (("" (expand "groupoid?")
                              ((""
                                (expand "commutative?")
                                ((""
                                  (expand "associative?")
                                  ((""
                                    (expand "semigroup?")
                                    ((""
                                      (expand "restrict")
                                      ((""
                                        (expand "associative?")
                                        ((""
                                          (expand "groupoid?")
                                          ((""
                                            (expand "remove")
                                            ((""
                                              (expand "identity?")
                                              ((""
                                                (expand "member")
                                                ((""
                                                  (expand
                                                   "star_closed?")
                                                  ((""
                                                    (expand "member")
                                                    ((""
                                                      (split)
                                                      (("1"
                                                        (expand
                                                         "inv_exists?")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "-x!1")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (lemma
                                                                   "number_fields_negate_is_right_inverse"
                                                                   ("x"
                                                                    "x!1"))
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (skosimp)
                                                        (("3"
                                                          (rewrite
                                                           "number_fields_left_identity_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("4"
                                                        (skosimp)
                                                        (("4"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("5"
                                                        (skosimp)
                                                        (("5"
                                                          (typepred
                                                           "x!1")
                                                          (("5"
                                                            (typepred
                                                             "y!1")
                                                            (("5"
                                                              (lemma
                                                               "nznum_times_nznum_is_nznum"
                                                               ("nzx"
                                                                "x!1"
                                                                "nzy"
                                                                "y!1"))
                                                              (("5"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("6"
                                                        (skosimp)
                                                        (("6"
                                                          (rewrite
                                                           "number_fields_left_identity_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("7"
                                                        (skosimp)
                                                        (("7"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("8"
                                                        (expand
                                                         "inv_exists?")
                                                        (("8"
                                                          (skosimp)
                                                          (("8"
                                                            (typepred
                                                             "x!1")
                                                            (("8"
                                                              (lemma
                                                               "inv_ne_0"
                                                               ("n0x"
                                                                "x!1"))
                                                              (("8"
                                                                (lemma
                                                                 "closed_divides"
                                                                 ("z"
                                                                  "1"
                                                                  "n0z"
                                                                  "x!1"))
                                                                (("8"
                                                                  (inst
                                                                   +
                                                                   "1/x!1")
                                                                  (("1"
                                                                    (rewrite
                                                                     "div_cancel1")
                                                                    (("1"
                                                                      (rewrite
                                                                       "div_cancel2")
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("9"
                                                        (skosimp)
                                                        (("9"
                                                          (rewrite
                                                           "commutative_mult")
                                                          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)
   ((field? const-decl "bool" field_def "algebra/")
    (ring_with_one? const-decl "bool" ring_with_one_def "algebra/")
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (restrict const-decl "R" restrict nil)
    (right_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (monad? const-decl "bool" monad_def "algebra/")
    (commutative? const-decl "bool" operator_defs nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (commutative_mult formula-decl nil number_fields nil)
    (closed_divides formula-decl nil complex_types nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (div_cancel1 formula-decl nil number_fields_bis nil)
    (div_cancel2 formula-decl nil number_fields_bis nil)
    (x!1 skolem-const-decl "({y | 0 /= y})" complex_field nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum_div_nznum_is_nznum application-judgement "nznum"
     number_fields_bis nil)
    (complex_div_nzcomplex_is_complex application-judgement "complex"
     complex_types nil)
    (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
     "nzcomplex" complex_types nil)
    (inv_ne_0 formula-decl nil number_fields_bis nil)
    (set type-eq-decl nil sets nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis
     nil)
    (/= const-decl "boolean" notequal nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number_fields_left_identity_mult formula-decl nil
     number_fields_bis nil)
    (associative_mult formula-decl nil number_fields nil)
    (inv_exists? const-decl "bool" group_def "algebra/")
    (minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (TRUE const-decl "bool" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_fields_negate_is_right_inverse formula-decl nil
     number_fields_bis nil)
    (star_closed? const-decl "bool" groupoid_def "algebra/")
    (identity? const-decl "bool" operator_defs nil)
    (associative? const-decl "bool" operator_defs nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (monoid? const-decl "bool" monoid_def "algebra/")
    (abelian_group? const-decl "bool" group_def "algebra/")
    (left_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (ring? const-decl "bool" ring_def "algebra/")
    (division_ring? const-decl "bool" division_ring_def "algebra/")
    (fullset const-decl "set" sets nil))
   nil)
  (fullset_is_field-1 nil 3385139699
   ("" (expand "fullset")
    (("" (expand "field?")
      (("" (expand "division_ring?")
        (("" (expand "ring_with_one?")
          (("" (expand "ring?")
            (("" (expand "restrict")
              (("" (expand "left_distributive?")
                (("" (expand "right_distributive?")
                  (("" (expand "abelian_group?")
                    (("" (expand "group?")
                      (("" (expand "monoid?")
                        (("" (expand "monad?")
                          (("" (expand "restrict")
                            (("" (expand "groupoid?")
                              ((""
                                (expand "commutative?")
                                ((""
                                  (expand "associative?")
                                  ((""
                                    (expand "semigroup?")
                                    ((""
                                      (expand "restrict")
                                      ((""
                                        (expand "associative?")
                                        ((""
                                          (expand "groupoid?")
                                          ((""
                                            (expand "remove")
                                            ((""
                                              (expand "identity?")
                                              ((""
                                                (expand "member")
                                                ((""
                                                  (expand
                                                   "star_closed?")
                                                  ((""
                                                    (expand "member")
                                                    ((""
                                                      (split)
                                                      (("1"
                                                        (expand
                                                         "inverse_exists?")
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (inst
                                                             +
                                                             "-x!1")
                                                            (("1"
                                                              (lemma
                                                               "number_fields_negate_is_right_inverse"
                                                               ("x"
                                                                "x!1"))
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (skosimp)
                                                        (("3"
                                                          (rewrite
                                                           "number_fields_left_identity_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("4"
                                                        (skosimp)
                                                        (("4"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("5"
                                                        (skosimp)
                                                        (("5"
                                                          (typepred
                                                           "x!1")
                                                          (("5"
                                                            (typepred
                                                             "y!1")
                                                            (("5"
                                                              (lemma
                                                               "nznum_times_nznum_is_nznum"
                                                               ("nzx"
                                                                "x!1"
                                                                "nzy"
                                                                "y!1"))
                                                              (("5"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("6"
                                                        (skosimp)
                                                        (("6"
                                                          (rewrite
                                                           "number_fields_left_identity_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("7"
                                                        (skosimp)
                                                        (("7"
                                                          (rewrite
                                                           "associative_mult")
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("8"
                                                        (expand
                                                         "inverse_exists?")
                                                        (("8"
                                                          (skosimp)
                                                          (("8"
                                                            (typepred
                                                             "x!1")
                                                            (("8"
                                                              (lemma
                                                               "inv_ne_0"
                                                               ("n0x"
                                                                "x!1"))
                                                              (("8"
                                                                (lemma
                                                                 "closed_divides"
                                                                 ("z"
                                                                  "1"
                                                                  "n0z"
                                                                  "x!1"))
                                                                (("1"
                                                                  (inst
                                                                   +
                                                                   "1/x!1")
                                                                  (("1"
                                                                    (rewrite
                                                                     "div_cancel1")
                                                                    (("1"
                                                                      (rewrite
                                                                       "div_cancel2")
                                                                      nil
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (lemma
                                                                   "real_complex"
                                                                   ("x"
                                                                    "1"))
                                                                  (("2"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("9"
                                                        (skosimp)
                                                        (("9"
                                                          (rewrite
                                                           "commutative_mult")
                                                          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)
   ((field? const-decl "bool" field_def "algebra/")
    (ring_with_one? const-decl "bool" ring_with_one_def "algebra/")
    (right_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (group? const-decl "bool" group_def "algebra/")
    (monad? const-decl "bool" monad_def "algebra/")
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (star_closed? const-decl "bool" groupoid_def "algebra/")
    (number_fields_negate_is_right_inverse formula-decl nil
     number_fields_bis nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (number_fields_left_identity_mult formula-decl nil
     number_fields_bis nil)
    (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis
     nil)
    (inv_ne_0 formula-decl nil number_fields_bis nil)
    (real_complex formula-decl nil complex_types nil)
    (nznum_div_nznum_is_nznum application-judgement "nznum"
     number_fields_bis nil)
    (div_cancel2 formula-decl nil number_fields_bis nil)
    (div_cancel1 formula-decl nil number_fields_bis nil)
    (nzcomplex nonempty-type-eq-decl nil complex_types nil)
    (closed_divides formula-decl nil complex_types nil)
    (monoid? const-decl "bool" monoid_def "algebra/")
    (abelian_group? const-decl "bool" group_def "algebra/")
    (left_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (ring? const-decl "bool" ring_def "algebra/")
    (division_ring? const-decl "bool" division_ring_def "algebra/"))
   shostak))
(IMP_field_TCC1 0
  (IMP_field_TCC1-1 nil 3385121716
   ("" (expand "fullset")
    (("" (expand "field?")
      (("" (expand "division_ring?")
        (("" (expand "ring_with_one?")
          (("" (expand "ring?")
            (("" (expand "abelian_group?")
              (("" (expand "left_distributive?")
                (("" (expand "right_distributive?")
                  (("" (expand "restrict")
                    (("" (expand "commutative?")
                      (("" (assert)
                        (("" (expand "group?")
                          (("" (expand "remove")
                            (("" (expand "monoid?")
                              ((""
                                (expand "restrict")
                                ((""
                                  (expand "associative?")
                                  ((""
                                    (expand "monad?")
                                    ((""
                                      (expand "groupoid?")
                                      ((""
                                        (expand "member")
                                        ((""
                                          (expand "restrict")
                                          ((""
                                            (expand "identity?")
                                            ((""
                                              (expand "semigroup?")
                                              ((""
                                                (expand "groupoid?")
                                                ((""
                                                  (expand "restrict")
                                                  ((""
                                                    (expand
                                                     "associative?")
                                                    ((""
                                                      (expand
                                                       "star_closed?")
                                                      ((""
                                                        (expand
                                                         "member")
                                                        ((""
                                                          (split)
                                                          (("1"
                                                            (expand
                                                             "inv_exists?")
                                                            (("1"
                                                              (skosimp)
                                                              (("1"
                                                                (inst
                                                                 +
                                                                 "-x!1")
                                                                (("1"
                                                                  (rewrite
                                                                   "number_fields_negate_is_right_inverse")
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (skosimp)
                                                            (("2"
                                                              (rewrite
                                                               "associative_mult")
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("3"
                                                            (skosimp)
                                                            (("3"
                                                              (rewrite
                                                               "number_fields_left_identity_mult")
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("4"
                                                            (skosimp)
                                                            (("4"
                                                              (rewrite
                                                               "associative_mult")
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("5"
                                                            (skosimp)
                                                            (("5"
                                                              (typepred
                                                               "x!1")
                                                              (("5"
                                                                (typepred
                                                                 "y!1")
                                                                (("5"
                                                                  (lemma
                                                                   "nznum_times_nznum_is_nznum"
                                                                   ("nzx"
                                                                    "x!1"
                                                                    "nzy"
                                                                    "y!1"))
                                                                  (("5"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("6"
                                                            (skosimp)
                                                            (("6"
                                                              (rewrite
                                                               "number_fields_left_identity_mult")
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("7"
                                                            (skosimp)
                                                            (("7"
                                                              (rewrite
                                                               "associative_mult")
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("8"
                                                            (expand
                                                             "inv_exists?")
                                                            (("8"
                                                              (skosimp)
                                                              (("8"
                                                                (typepred
                                                                 "x!1")
                                                                (("8"
                                                                  (lemma
                                                                   "inv_ne_0"
                                                                   ("n0x"
                                                                    "x!1"))
                                                                  (("8"
                                                                    (inst
                                                                     +
                                                                     "1/x!1")
                                                                    (("1"
                                                                      (assert)
                                                                      (("1"
                                                                        (rewrite
                                                                         "div_cancel1")
                                                                        (("1"
                                                                          (rewrite
                                                                           "div_cancel2")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("9"
                                                            (skosimp)
                                                            (("9"
                                                              (rewrite
                                                               "commutative_mult")
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((field? const-decl "bool" field_def "algebra/")
    (ring_with_one? const-decl "bool" ring_with_one_def "algebra/")
    (abelian_group? const-decl "bool" group_def "algebra/")
    (right_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (commutative? const-decl "bool" operator_defs nil)
    (group? const-decl "bool" group_def "algebra/")
    (monoid? const-decl "bool" monoid_def "algebra/")
    (associative? const-decl "bool" operator_defs nil)
    (member const-decl "bool" sets nil)
    (identity? const-decl "bool" operator_defs nil)
    (commutative_mult formula-decl nil number_fields nil)
    (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
     "nzcomplex" complex_types nil)
    (complex_div_nzcomplex_is_complex application-judgement "complex"
     complex_types nil)
    (nznum_div_nznum_is_nznum application-judgement "nznum"
     number_fields_bis nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (x!1 skolem-const-decl "({y | 0 /= y})" complex_field nil)
    (div_cancel1 formula-decl nil number_fields_bis nil)
    (div_cancel2 formula-decl nil number_fields_bis nil)
    (inv_ne_0 formula-decl nil number_fields_bis nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (nznum_times_nznum_is_nznum judgement-tcc nil number_fields_bis
     nil)
    (/= const-decl "boolean" notequal nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number_fields_left_identity_mult formula-decl nil
     number_fields_bis nil)
    (associative_mult formula-decl nil number_fields nil)
    (inv_exists? const-decl "bool" group_def "algebra/")
    (minus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (TRUE const-decl "bool" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (complex nonempty-type-from-decl nil complex_types nil)
    (complex_pred const-decl "[number_field -> boolean]" complex_types
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_fields_negate_is_right_inverse formula-decl nil
     number_fields_bis nil)
    (star_closed? const-decl "bool" groupoid_def "algebra/")
    (monad? const-decl "bool" monad_def "algebra/")
    (remove const-decl "set" sets nil)
    (restrict const-decl "R" restrict nil)
    (complex_times_complex_is_complex application-judgement "complex"
     complex_types nil)
    (complex_plus_complex_is_complex application-judgement "complex"
     complex_types nil)
    (left_distributive? const-decl "bool" operator_defs_more
     "algebra/")
    (ring? const-decl "bool" ring_def "algebra/")
    (division_ring? const-decl "bool" division_ring_def "algebra/")
    (fullset const-decl "set" sets nil))
   nil)))

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