(scott_composition_continuity
(IMP_composition_continuity_TCC1 0
(IMP_composition_continuity_TCC1-1 nil 3353641502 3353641645
("" (assert) nil nil) proved nil 4548 280 t nil))
(IMP_composition_continuity_TCC2 0
(IMP_composition_continuity_TCC2-1 nil 3353641502 3353641655
("" (assert) nil nil) proved nil 3733 290 t nil))
(IMP_composition_continuity_TCC3 0
(IMP_composition_continuity_TCC3-1 nil 3353641502 3353641664
("" (assert) nil nil) proved nil 4352 280 t nil))
(composition_scott_continuous 0
(composition_scott_continuous-1 nil 3353641502 3353641627
("" (skosimp)
(("" (typepred "f!1")
(("" (typepred "g!1")
(("" (rewrite "scott_continuous_def" -1 :dir rl)
(("" (rewrite "scott_continuous_def" -2 :dir rl)
(("" (rewrite "scott_continuous_def" 1 :dir rl)
((""
(lemma "composition_continuous" ("f" "f!1" "g" "g!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved
((scott_continuous? const-decl "bool" scott_continuity nil)
(le3 formal-const-decl "(directed_complete_partial_order?[T3])"
scott_composition_continuity nil)
(le2 formal-const-decl "(directed_complete_partial_order?[T2])"
scott_composition_continuity nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(pred type-eq-decl nil defined_types nil)
(T3 formal-type-decl nil scott_composition_continuity nil)
(T2 formal-type-decl nil scott_composition_continuity nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(scott_continuous_def formula-decl nil scott_continuity nil)
(O const-decl "T3" function_props nil)
(composition_continuous formula-decl nil composition_continuity
"topology/")
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(scott_open_sets const-decl "setofsets[T]" scott nil)
(T1 formal-type-decl nil scott_composition_continuity nil)
(le1 formal-const-decl "(directed_complete_partial_order?[T1])"
scott_composition_continuity nil))
120165 2310 t 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.
|