|
(abelian_group
(IMP_group_TCC1 0
(IMP_group_TCC1-1 nil 3293976868
("" (lemma "fullset_is_abelian_group")
(("" (expand "abelian_group?") (("" (flatten) nil nil)) nil)) nil)
((abelian_group? const-decl "bool" group_def nil)
(fullset_is_abelian_group formula-decl nil abelian_group nil))
shostak))
(abelian_group_TCC1 0
(abelian_group_TCC1-1 nil 3293976891
("" (lemma "fullset_is_abelian_group") (("" (propax) nil nil)) nil)
((fullset_is_abelian_group formula-decl nil abelian_group nil))
shostak))
(abelian_group_is_group 0
(abelian_group_is_group-1 nil 3293976699
("" (skolem!)
(("" (typepred "x!1")
(("" (expand "abelian_group?") (("" (flatten) nil nil)) nil))
nil))
nil)
((abelian_group nonempty-type-eq-decl nil abelian_group nil)
(abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil abelian_group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(abelian_group_is_commutative_monoid 0
(abelian_group_is_commutative_monoid-1 nil 3294086816
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "abelian_group?")
(("" (expand "group?")
(("" (expand "commutative_monoid?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((abelian_group nonempty-type-eq-decl nil abelian_group nil)
(abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil abelian_group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(group? const-decl "bool" group_def nil)
(commutative_monoid? const-decl "bool" monoid_def nil))
shostak))
(abelian_subgroups 0
(abelian_subgroups-1 nil 3293976722
("" (skolem!)
(("" (flatten)
(("" (typepred "A!1")
(("" (expand "abelian_group?")
(("" (flatten)
(("" (expand "subgroup?")
(("" (flatten)
(("" (assert)
(("" (hide -1 -4)
(("" (expand "commutative_over?")
(("" (skosimp*)
(("" (inst - "x!1" "y!1")
(("" (expand "subset?")
(("" (inst-cp - "x!1")
((""
(inst - "y!1")
(("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subgroup? const-decl "bool" group_def nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(A!1 skolem-const-decl "abelian_group" abelian_group nil)
(S!1 skolem-const-decl "set[T]" abelian_group nil)
(x!1 skolem-const-decl "(S!1)" abelian_group nil)
(y!1 skolem-const-decl "(S!1)" abelian_group nil)
(member const-decl "bool" sets nil)
(commutative? const-decl "bool" operator_defs nil)
(restrict const-decl "R" restrict nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-nonempty-type-decl nil abelian_group nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" abelian_group nil)
(one formal-const-decl "T" abelian_group nil)
(abelian_group? const-decl "bool" group_def nil)
(abelian_group nonempty-type-eq-decl nil abelian_group nil))
shostak))
(finite_abelian_group_TCC1 0
(finite_abelian_group_TCC1-1 nil 3407081659
("" (inst + "singleton[T](one)")
(("" (expand "finite_abelian_group?")
(("" (assert)
(("" (expand "commutative?")
(("" (skosimp*)
(("" (grind)
(("" (typepred "y!1")
(("" (typepred "x!1")
(("" (expand "singleton")
(("" (replace -1)
(("" (hide -1)
(("" (replace -1) (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((commutative? const-decl "bool" operator_defs nil)
(restrict const-decl "R" restrict nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(one_finite_group formula-decl nil group nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(finite_abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group 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-nonempty-type-decl nil abelian_group nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
nil))
(finite_abelian_group_is_abelian_group 0
(finite_abelian_group_is_abelian_group-2 nil 3426244950
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "finite_abelian_group?")
(("" (flatten)
(("" (expand "abelian_group?")
(("" (expand "finite_group?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
(finite_abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil abelian_group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_group? const-decl "bool" group_def nil)
(abelian_group? const-decl "bool" group_def nil))
nil)
(finite_abelian_group_is_abelian_group-1 nil 3407081659
("" (skosimp*)
(("" (typepred "x!1")
(("" (expand "finite_abelian_group?")
(("" (flatten)
(("" (assert)
(("" (expand "abelian_group?")
(("" (assert)
(("" (expand "finite_group?") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_abelian_group? const-decl "bool" group_def nil)
(abelian_group? const-decl "bool" group_def nil)
(finite_group? const-decl "bool" group_def nil))
nil))
(finite_abelian_group_is_finite_group 0
(finite_abelian_group_is_finite_group-1 nil 3407081659
("" (skosimp*)
(("" (typepred "x!1")
(("" (assert)
(("" (expand "finite_group?")
(("" (expand "finite_abelian_group?") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
(finite_abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil abelian_group nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(finite_group? const-decl "bool" group_def nil))
nil))
(finite_abelian_subgroups 0
(finite_abelian_subgroups-1 nil 3407081668
("" (skosimp)
(("" (lemma "abelian_subgroups" ("S" "S!1" "A" "G!1"))
(("" (expand "finite_abelian_group?")
(("" (expand "abelian_group?")
(("" (assert)
(("" (flatten)
(("" (assert)
(("" (expand "finite_group?")
(("" (lemma "finite_subgroups")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_abelian_group nonempty-type-eq-decl nil abelian_group nil)
(finite_abelian_group? const-decl "bool" group_def nil)
(abelian_group nonempty-type-eq-decl nil abelian_group nil)
(abelian_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" abelian_group nil)
(* formal-const-decl "[T, T -> T]" abelian_group 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-nonempty-type-decl nil abelian_group nil)
(abelian_subgroups formula-decl nil abelian_group nil)
(finite_group? const-decl "bool" group_def nil)
(finite_group nonempty-type-eq-decl nil group nil)
(finite_subgroups formula-decl nil group nil))
nil)))
¤ Dauer der Verarbeitung: 0.3 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.
|
