Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
scott_identity_continuity.prf
Sprache: Lisp
|
(scott_identity_continuity
(IMP_identity_continuity_TCC1 0
(IMP_identity_continuity_TCC1-1 nil 3353640334 3353640425
("" (lemma "scott_topology[T,le]") (("" (propax) nil nil)) nil)
proved
((scott_topology formula-decl nil scott nil)
(T formal-type-decl nil scott_identity_continuity nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(le formal-const-decl "(directed_complete_partial_order?)"
scott_identity_continuity nil))
35142 420 t nil))
(id_scott_continuous 0
(id_scott_continuous-1 nil 3353640334 3353640363
("" (lemma "id_continuous")
(("" (rewrite "scott_continuous_def") nil nil)) nil)
proved
((I const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(scott_continuous_def formula-decl nil scott_continuity nil)
(id_continuous formula-decl nil identity_continuity "topology/")
(T formal-type-decl nil scott_identity_continuity nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
nil)
(le formal-const-decl "(directed_complete_partial_order?)"
scott_identity_continuity nil)
(scott_open_sets const-decl "setofsets[T]" scott nil))
26579 440 t nil)))
[ zur Elbe Produktseite wechseln0.31Quellennavigators
Analyse erneut starten
]
|
|
