|
(finite_sets_aux
(is_finite_exists_N 0
(is_finite_exists_N-1 nil 3460199813
("" (skosimp*)
(("" (lemma "is_finite_surj[T]")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (inst + "N!1" "(LAMBDA (n: below(N!1)): g!1(n))")
(("1" (expand "surjective?")
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1" (skosimp*)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil finite_sets_aux nil)
(is_finite_surj formula-decl nil finite_sets nil)
(g!1 skolem-const-decl "[below[N!1] -> T]" finite_sets_aux nil)
(below type-eq-decl nil naturalnumbers nil)
(N!1 skolem-const-decl "nat" finite_sets_aux nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(surjective? const-decl "bool" functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals 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)
(number nonempty-type-decl nil numbers nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
