|
(finite_sets_card_from
(card_extension 0
(card_extension-2 "How diff" 3389097530
("" (skosimp*)
(("" (expand "extend")
(("" (lemma "finite_sets_card_eq[T1,T2].card_eq_bij")
(("" (inst?)
(("1" (prop)
(("1" (hide 2 3)
(("1" (inst 1 "lambda (t:(F!1)):t")
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?") (("1" (grind) nil nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (inst 1 "y!1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (prop) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "extend_set_props[T1,T2].finite_extension")
(("2" (inst -1 "F!1")
(("2" (typepred "F!1")
(("2" (prop)
(("2" (hide -2 -3)
(("2" (expand "extend") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(F!1 skolem-const-decl "finite_set[T2]" finite_sets_card_from nil)
(finite_set type-eq-decl nil finite_sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(finite_extension formula-decl nil extend_set_props nil)
(card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
(T1 formal-type-decl nil finite_sets_card_from nil)
(boolean nonempty-type-decl nil booleans nil)
(T2_pred const-decl "[T1 -> boolean]" finite_sets_card_from nil)
(T2 formal-subtype-decl nil finite_sets_card_from nil))
shostak)
(card_extension-1 nil 3389097499
("" (skosimp*)
(("" (expand "extend")
(("" (lemma "finite_sets_card_eq[T1,T2].card_eq_bij")
(("" (inst?)
(("1" (prop)
(("1" (hide 2 3)
(("1" (inst 1 "lambda (t:(F!1)):t")
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?") (("1" (grind) nil)))
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (inst 1 "y!1") nil)))))))))))
("2" (skosimp*) (("2" (prop) nil)))))))))
("2" (hide 2)
(("2" (lemma "extend_set_props[T1,T2].finite_extension")
(("2" (inst -1 "F!1")
(("2" (typepred "F!1")
(("2" (prop)
(("2" (hide -2 -3)
(("2" (expand "extend")
(("2" (propax) nil))))))))))))))))))))))
nil)
((card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/"))
nil)))
¤ Dauer der Verarbeitung: 0.25 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.
|
