|
(subgroups
(G_TCC1 0
(G_TCC1-1 nil 3459006169
("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
((fullset_is_group formula-decl nil subgroups nil)) nil))
(pg64_1 0
(pg64_1-1 nil 3459009709
("" (skeep)
(("" (lemma "subgroup_def[T,*,one]")
(("" (inst - "G" "intersection(A, B)")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (expand "intersection")
(("1" (expand "member")
(("1" (inst - "one") (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subgroup?")
(("2" (flatten)
(("2" (auto-rewrite-theory "sets[T]")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst?)
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "subgroup?")
(("3" (expand "star_closed?")
(("3" (expand "intersection")
(("3" (assert)
(("3" (skosimp*)
(("3" (typepred "x!1")
(("3" (typepred "y!1")
(("3" (expand "intersection")
(("3"
(assert)
(("3"
(flatten)
(("3"
(expand "group?")
(("3"
(expand "monoid?")
(("3"
(expand "monad?")
(("3"
(flatten)
(("3"
(expand "star_closed?")
(("3"
(assert)
(("3"
(inst?)
(("3"
(inst?)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "inv_closed?")
(("4" (expand "intersection")
(("4" (expand "subgroup?")
(("4" (expand "subset?")
(("4" (expand "member")
(("4" (flatten)
(("4" (expand "group?")
(("4" (flatten)
(("4"
(expand "inv_exists?")
(("4"
(skosimp*)
(("4"
(inst -3 "x!1")
(("1"
(inst -6 "x!1")
(("1"
(skosimp*)
(("1"
(replace -3 -7 rl)
(("1"
(rewrite
"cancel_left[T,*,one]")
(("1"
(lemma
"unique_inv[T,*,one]")
(("1"
(inst-cp
-1
"x!1"
"y!1")
(("1"
(inst -1 "x!1" "y!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "x!1")
(("2"
(expand "intersection")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(typepred "x!1")
(("2"
(expand "intersection")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((one formal-const-decl "T" subgroups nil)
(* formal-const-decl "[T, T -> T]" subgroups nil)
(T formal-nonempty-type-decl nil subgroups nil)
(subgroup_def formula-decl nil group nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(empty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict nil)
(identity? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(inv_exists? const-decl "bool" group_def nil)
(subgroup? const-decl "bool" group_def nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(unique_inv formula-decl nil group nil)
(cancel_left formula-decl nil group nil)
(x!1 skolem-const-decl "(intersection(A, B))" subgroups nil)
(B skolem-const-decl "set[T]" subgroups nil)
(A skolem-const-decl "set[T]" subgroups nil)
(inv_closed? const-decl "bool" group nil)
(intersection const-decl "set" sets nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(center_normal_TCC1 0
(center_normal_TCC1-1 nil 3459175283
("" (skeep)
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (expand "subgroup?") (("" (flatten) nil nil)) nil)) nil))
nil))
nil)
((one formal-const-decl "T" subgroups nil)
(* formal-const-decl "[T, T -> T]" subgroups nil)
(T formal-nonempty-type-decl nil subgroups nil)
(center_subgroup formula-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(center_normal 0
(center_normal-1 nil 3459175396
("" (skeep)
(("" (expand "normal_subgroup?")
(("" (lemma "center_subgroup")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (typepred "h!1")
(("" (skosimp*)
((""
(typepred "h!2")
((""
(rewrite "center_def" +)
((""
(prop)
(("1"
(replace -5)
(("1"
(replace -2)
(("1"
(typepred "center(G)")
(("1"
(expand "subset?")
(("1"
(assert)
(("1"
(inst - "h!2")
(("1"
(assert)
(("1"
(hide -2 -3 -5 -6)
(("1"
(lemma
"inv_member")
(("1"
(inst?)
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma
"product_in")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
2)
(("1"
(lemma
"product_in")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -5)
(("2"
(skeep)
(("2"
(hide -5)
(("2"
(replace -2)
(("2"
(hide -2)
(("2"
(name
"w"
"inv[T, *, one](a!1)")
(("2"
(replace -1)
(("2"
(hide -4)
(("2"
(rewrite
"center_def")
(("2"
(flatten)
(("2"
(inst-cp
-3
"w")
(("1"
(replace
-4)
(("1"
(lemma
"assoc")
(("1"
(inst
-
"h!2"
"w"
"a!1")
(("1"
(replace
-1
+
rl)
(("1"
(replace
-2
+
rl)
(("1"
(rewrite
"inv_left")
(("1"
(assert)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"inv_in")
(("2"
(inst?)
(("2"
(assert)
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))
nil)
((normal_subgroup? const-decl "boolean" normal_subgroups nil)
(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 nil)
(group nonempty-type-eq-decl nil group nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(center_def formula-decl nil group nil)
(G skolem-const-decl "group[T, *, one]" subgroups nil)
(w skolem-const-decl "T" subgroups nil)
(assoc formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(right_identity formula-decl nil monad nil)
(inv_in formula-decl nil group nil)
(inv_member formula-decl nil group nil)
(product_in formula-decl nil group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(center const-decl "{s: set[T] | subset?(s, G)}" group nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(center_subgroup formula-decl nil group nil)
(T formal-nonempty-type-decl nil subgroups nil)
(* formal-const-decl "[T, T -> T]" subgroups nil)
(one formal-const-decl "T" subgroups nil))
shostak)))
¤ Dauer der Verarbeitung: 0.15 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.
|
