| products/Sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: A_group.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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))) ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
