|
(homomorphisms
(IMP_group_TCC1 0
(IMP_group_TCC1-1 nil 3406458542 ("" (rewrite "T1_is_group") nil nil)
((T1_is_group formula-decl nil homomorphisms nil)) nil))
(IMP_group_TCC2 0
(IMP_group_TCC2-1 nil 3406458542 ("" (rewrite "T2_is_group") nil nil)
((T2_is_group formula-decl nil homomorphisms nil)) nil))
(homomorphism?_TCC1 0
(homomorphism?_TCC1-1 nil 3397908305 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T1 formal-type-decl nil homomorphisms nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphisms nil)
(one1 formal-const-decl "T1" homomorphisms nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(T2 formal-type-decl nil homomorphisms nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphisms nil)
(one2 formal-const-decl "T2" homomorphisms nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(one_member formula-decl nil monad nil)
(right_identity formula-decl nil monad nil)
(restrict const-decl "R" restrict nil)
(left_identity formula-decl nil monad 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))
nil))
(homo_one_TCC1 0
(homo_one_TCC1-1 nil 3406465849
("" (skosimp*)
(("" (typepred "G!1")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (flatten)
(("" (expand "monad?")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one1 formal-const-decl "T1" homomorphisms nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphisms nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil homomorphisms nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(monoid? const-decl "bool" monoid_def nil)
(monad? const-decl "bool" monad_def nil)
(member const-decl "bool" sets nil))
nil))
(homo_one 0
(homo_one-1 nil 3406465854
("" (skosimp*)
(("" (typepred "phi!1")
(("" (expand "homomorphism?")
(("" (inst - "one1" "one1")
(("" (rewrite "one_left")
(("" (lemma "divby[T2,o,one2]")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((homomorphism type-eq-decl nil homomorphisms nil)
(homomorphism? const-decl "bool" homomorphisms nil)
(group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(one2 formal-const-decl "T2" homomorphisms nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphisms nil)
(T2 formal-type-decl nil homomorphisms nil)
(group nonempty-type-eq-decl nil group nil)
(one1 formal-const-decl "T1" homomorphisms nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphisms nil)
(T1 formal-type-decl nil homomorphisms nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(divby formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(one_left formula-decl nil group nil))
shostak))
(kernel_TCC1 0
(kernel_TCC1-1 nil 3406458542
("" (skosimp*)
((""
(case-replace
"subgroup?[T1, *, one1]({a: T1 | G!1(a) AND phi!1(a) = one2}, G!1)")
(("1" (expand "subgroup?") (("1" (flatten) nil nil)) nil)
("2" (hide 2)
(("2" (expand "subgroup?")
(("2" (prop)
(("1" (expand "subset?")
(("1" (skosimp*)
(("1" (assert) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (expand "group?")
(("2" (prop)
(("1" (expand "monoid?")
(("1" (prop)
(("1" (expand "monad?")
(("1" (prop)
(("1" (expand "groupoid?")
(("1" (expand "star_closed?")
(("1" (skosimp*)
(("1"
(expand "member")
(("1"
(prop)
(("1"
(rewrite "star_closed")
nil
nil)
("2"
(typepred "x!1")
(("2"
(typepred "y!1")
(("2"
(typepred "phi!1")
(("2"
(expand "homomorphism?")
(("2"
(inst?)
(("2"
(assert)
(("2"
(replace -1)
(("2"
(replace -3)
(("2"
(replace -5)
(("2"
(rewrite
"one_left")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member")
(("2" (rewrite "one_in")
(("2" (typepred "phi!1")
(("2"
(expand "homomorphism?")
(("2"
(inst?)
(("2" (rewrite "homo_one") nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "restrict")
(("3" (expand "identity?")
(("3" (skosimp*)
(("3"
(rewrite "one_left")
(("3" (rewrite "one_right") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "restrict")
(("2" (expand "associative?")
(("2" (skosimp*)
(("2" (rewrite "associative") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "inv(x!1)")
(("1" (assert)
(("1" (rewrite "inv_right")
(("1" (rewrite "inv_left") nil nil)) nil))
nil)
("2" (prop)
(("1" (expand "inv")
(("1" (assert)
(("1" (rewrite "inv_in") nil nil)) nil))
nil)
("2" (typepred "x!1")
(("2" (typepred "phi!1")
(("2" (expand "homomorphism?")
(("2"
(inst - "x!1" "inv(x!1)")
(("2"
(assert)
(("2"
(rewrite "inv_right")
(("2"
(rewrite "homo_one")
(("2"
(replace -3)
(("2"
(rewrite "one_left")
(("2"
(assert)
(("2"
(expand "inv")
(("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)
((T1 formal-type-decl nil homomorphisms nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T1, T1 -> T1]" homomorphisms nil)
(one1 formal-const-decl "T1" homomorphisms nil)
(group? const-decl "bool" group_def nil)
(subgroup? const-decl "bool" group_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(group nonempty-type-eq-decl nil group nil)
(T2 formal-type-decl nil homomorphisms nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(O formal-const-decl "[T2, T2 -> T2]" homomorphisms nil)
(one2 formal-const-decl "T2" homomorphisms nil)
(homomorphism? const-decl "bool" homomorphisms nil)
(homomorphism type-eq-decl nil homomorphisms nil)
(inv_exists? const-decl "bool" group_def nil)
(x!1 skolem-const-decl "({a: T1 | G!1(a) AND phi!1(a) = one2})"
homomorphisms nil)
(phi!1 skolem-const-decl "homomorphism(G!1, GP!1)" homomorphisms
nil)
(GP!1 skolem-const-decl "group[T2, o, one2]" homomorphisms nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(G!1 skolem-const-decl "group[T1, *, one1]" homomorphisms nil)
(inv_left formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(inv_in formula-decl nil group nil)
(monoid? const-decl "bool" monoid_def nil)
(associative formula-decl nil semigroup nil)
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(restrict const-decl "R" restrict nil)
(one_right formula-decl nil group nil)
(identity? const-decl "bool" operator_defs nil)
(homo_one formula-decl nil homomorphisms nil)
(one_in formula-decl nil monad nil)
(monad nonempty-type-eq-decl nil monad nil)
(star_closed? const-decl "bool" groupoid_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(one_left formula-decl nil group nil)
(groupoid nonempty-type-eq-decl nil groupoid nil)
(star_closed formula-decl nil groupoid nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil))
nil)))
¤ Dauer der Verarbeitung: 0.16 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.
|
