|
(group_test
(integer_plus_TCC1 0
(integer_plus_TCC1-1 nil 3293317341
("" (expand "fullset")
(("" (expand "abelian_group?")
(("" (expand "group?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "-x!1") (("2" (grind) nil nil)) nil)) nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil)
((abelian_group? const-decl "bool" group_def nil)
(member 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_int_is_int application-judgement "int" integers nil)
(inv_exists? const-decl "bool" group_def nil)
(commutative? const-decl "bool" operator_defs nil)
(group? const-decl "bool" group_def nil)
(fullset const-decl "set" sets nil))
shostak))
(nz_rational_mult_TCC1 0
(nz_rational_mult_TCC1-1 nil 3293317603
("" (expand "abelian_group?")
(("" (expand "group?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (typepred "x!1")
(("2" (inst + "1/x!1")
(("1" (assert) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(commutative? const-decl "bool" operator_defs nil)
(inv_exists? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(nzrat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(x!1 skolem-const-decl "(fullset[nzrat])" group_test nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
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)
(restrict const-decl "R" restrict nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(abelian_group? const-decl "bool" group_def nil))
shostak))
(pos_rational_mult_TCC1 0
(pos_rational_mult_TCC1-1 nil 3293317482
("" (expand "abelian_group?")
(("" (expand "group?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "inv_exists?")
(("2" (skosimp*)
(("2" (inst + "1/x!1")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil))
nil)
("3" (grind) nil nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(commutative? const-decl "bool" operator_defs nil)
(inv_exists? const-decl "bool" group_def nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(x!1 skolem-const-decl "(fullset[posrat])" group_test nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(set type-eq-decl nil sets nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(> const-decl "bool" reals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals 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)
(restrict const-decl "R" restrict nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(abelian_group? const-decl "bool" group_def nil))
shostak)))
¤ Dauer der Verarbeitung: 0.24 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.
|
