Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


SSL A_group.prf   Interaktion und
PortierbarkeitLisp

 
(A_group
 (op_TCC1 0
  (op_TCC1-1 nil 3397569694 ("" (subtype-tcc) nil nil)
   ((composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil))
   nil))
 (A_is_group_TCC1 0
  (A_is_group_TCC1-1 nil 3397569250
   ("" (skosimp*) (("" (inst + "id(S!1)"nil nil)) nil)
   ((T formal-type-decl nil A_group nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (bijective? const-decl "bool" functions nil)
    (maps type-eq-decl nil A_group nil)
    (id const-decl "maps(S)" A_group nil))
   nil))
 (A_is_group 0
  (A_is_group-1 nil 3397569259
   ("" (skosimp*)
    (("" (expand "group?")
      (("" (prop)
        (("1" (expand "monoid?")
          (("1" (prop)
            (("1" (expand "monad?")
              (("1" (prop)
                (("1" (expand "groupoid?")
                  (("1" (expand "star_closed?")
                    (("1" (assert)
                      (("1" (skosimp*) (("1" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (grind) nil nil)
                 ("3" (grind)
                  (("1" (expand "identity")
                    (("1" (apply-extensionality 1 :hide? t) nil nil))
                    nil)
                   ("2" (apply-extensionality 1 :hide? t) nil nil))
                  nil))
                nil))
              nil)
             ("2" (grind)
              (("2" (apply-extensionality 1 :hide? t) nil nil)) nil))
            nil))
          nil)
         ("2" (expand "inv_exists?")
          (("2" (skosimp*)
            (("2" (typepred "x!1")
              (("2" (inst + "(inverse(x!1))")
                (("1" (grind)
                  (("1" (apply-extensionality 1 :hide? t)
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "epsilon_ax[(S!1)]")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1" (inst + "x!2"nil nil)) nil))
                            nil)
                           ("2" (typepred "S!1")
                            (("2" (expand "nonempty?")
                              (("2" (inst?) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "S!1")
                        (("2" (expand "nonempty?")
                          (("2" (typepred "S!1")
                            (("2" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (typepred "S!1")
                      (("2" (expand "nonempty?")
                        (("2" (expand "empty?")
                          (("2" (skosimp*)
                            (("2" (expand "member")
                              (("2" (inst + "x!2"nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (apply-extensionality 1 :hide? t)
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "epsilon_ax[(S!1)]")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1" (inst - "x!2"nil nil)) nil))
                            nil)
                           ("2" (typepred "S!1")
                            (("2" (expand "nonempty?")
                              (("2"
                                (expand "empty?")
                                (("2"
                                  (skosimp*)
                                  (("2"
                                    (assert)
                                    (("2" (inst + "x!3"nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "S!1")
                        (("2" (expand "nonempty?")
                          (("2" (expand "empty?")
                            (("2" (skosimp*)
                              (("2"
                                (assert)
                                (("2" (inst + "x!3"nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (typepred "S!1")
                      (("2" (expand "nonempty?")
                        (("2" (expand "empty?")
                          (("2" (skosimp*)
                            (("2" (assert)
                              (("2" (inst + "x!2"nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (grind) nil nil)
                 ("3" (typepred "S!1")
                  (("3" (expand "nonempty?")
                    (("3" (expand "empty?")
                      (("3" (assert)
                        (("3" (skosimp*) (("3" (inst + "x!2"nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((group? const-decl "bool" group_def nil)
    (inv_exists? const-decl "bool" group_def nil)
    (x!2 skolem-const-decl "T" A_group nil)
    (empty? const-decl "bool" sets nil)
    (x!2 skolem-const-decl "T" A_group nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (unique_bijective_inverse application-judgement "{x: D | f(x) = y}"
     function_inverse nil)
    (x!1 skolem-const-decl "(fullset[maps(S!1)])" A_group nil)
    (inverse const-decl "D" function_inverse nil)
    (TRUE const-decl "bool" booleans nil)
    (S!1 skolem-const-decl "(nonempty?[T])" A_group nil)
    (bijective_inverse_is_bijective application-judgement
     "(bijective?[R, D])" function_inverse nil)
    (monoid? const-decl "bool" monoid_def nil)
    (associative? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (identity? const-decl "bool" operator_defs nil)
    (maps type-eq-decl nil A_group nil)
    (bijective? const-decl "bool" functions nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil A_group nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (O const-decl "T3" function_props nil)
    (identity const-decl "(bijective?[T, T])" identity nil)
    (id const-decl "maps(S)" A_group nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (composition_bijective application-judgement "(bijective?[T1, T3])"
     function_props nil)
    (composition_surjective application-judgement
     "(surjective?[T1, T3])" function_props nil)
    (composition_injective application-judgement "(injective?[T1, T3])"
     function_props nil)
    (fullset const-decl "set" sets nil)
    (restrict const-decl "R" restrict nil)
    (op const-decl "[maps(S), maps(S) -> maps(S)]" A_group nil)
    (member const-decl "bool" sets nil))
   nil)))

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge