Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
monoid_def.prf
Sprache: Unknown
|
(monoid_def
(power_TCC1 0
(power_TCC1-1 nil 3296995136 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(power_TCC2 0
(power_TCC2-1 nil 3296995136 ("" (grind) nil nil) nil shostak))
(generated_set_lem 0
(generated_set_lem-1 nil 3396972577
("" (skosimp*)
(("" (expand "generated_set") (("" (inst?) nil nil)) nil)) nil)
((generated_set const-decl "set[T]" monoid_def nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(monoid?_TCC1 0
(monoid?_TCC1-1 nil 3301141924
("" (expand "monad?")
(("" (expand "groupoid?")
(("" (expand "star_closed?")
(("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
nil))
nil)
((star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(monad? const-decl "bool" monad_def nil))
shostak))
(commutative_monoid?_TCC1 0
(commutative_monoid?_TCC1-1 nil 3301141924
("" (expand "monoid?")
(("" (expand "monad?")
(("" (expand "groupoid?")
(("" (expand "star_closed?")
(("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
nil))
nil))
nil)
((monad? const-decl "bool" monad_def nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(monoid? const-decl "bool" monoid_def nil))
shostak))
(finite_commutative_monoid?_TCC1 0
(finite_commutative_monoid?_TCC1-1 nil 3301141924
("" (expand "finite_monoid?")
(("" (expand "monoid?")
(("" (expand "monad?")
(("" (expand "groupoid?")
(("" (expand "star_closed?")
(("" (expand "member") (("" (skosimp*) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((monoid? const-decl "bool" monoid_def nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(monad? const-decl "bool" monad_def nil)
(finite_monoid? const-decl "bool" monoid_def nil))
shostak)))
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
|
