| products/sources/formale Sprachen/Isabelle/Pure/System/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 18 kB |
|
Quelle graph_conn_defs.prf Sprache: Lisp |
|||||||||
|
(graph_conn_defs
(connected?_TCC1 0 (connected?_TCC1-1 nil 3507100595 ("" (skosimp*) (("" (rewrite "size_del_vert") (("" (assert) nil)))) nil) ((size_del_vert formula-decl nil graph_ops nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (T formal-type-decl nil graph_conn_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (path_connected?_TCC1 0 (path_connected?_TCC1-1 nil 3507100595 ("" (subtype-tcc) nil nil) ((member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (T formal-type-decl nil graph_conn_defs nil) (empty? const-decl "bool" graphs nil)) nil)) (path_connected?_TCC2 0 (path_connected?_TCC2-1 nil 3507100595 ("" (subtype-tcc) nil nil) ((member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (T formal-type-decl nil graph_conn_defs nil) (empty? const-decl "bool" graphs nil)) nil))) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28