| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cycles.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(cycles
(cycle?_TCC1 0 (cycle?_TCC1-1 nil 3312559967 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil cycles nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (pre_circuit? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" cycles nil)) nil)) (cycle?_TCC2 0 (cycle?_TCC2-1 nil 3312559967 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil cycles nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (pre_circuit? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" cycles nil)) nil)) (cycle_l_gt_3 0 (cycle_l_gt_3-1 nil 3312559967 ("" (skosimp*) (("" (expand "cycle?") (("" (flatten) (("" (expand "pre_circuit?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cycle? const-decl "bool" cycles nil) (pre_circuit? const-decl "bool" walks nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (cycle_has_path_TCC1 0 (cycle_has_path_TCC1-1 nil 3312559967 ("" (skosimp*) (("" (expand* "^" min empty_seq) (("" (typepred "j!1") (("" (assert) nil)))))) nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (< const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cycles nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil)) nil)) (cycle_has_path 0 (cycle_has_path-2 "Fewer" 3368782121 ("" (skosimp*) (("" (lemma "cycle_l_gt_3") (("" (inst?) (("" (assert) (("" (case "walk?(G!1, w!1)") (("1" (inst 1 "length(w!1)-2") (("1" (expand "path?") (("1" (expand "finseq_appl") (("1" (prop) (("1" (rewrite "walk?_caret") nil nil) ("2" (skosimp*) (("2" (expand "^") (("2" (typepred "j!1") (("2" (typepred "i!1") (("2" (expand* "^" min empty_seq) (("2" (expand "cycle?") (("2" (expand "finseq_appl") (("2" (flatten) (("2" (inst -7 "i!1" "j!1") (("2" (bddsimp) (("2" (install-rewrites "walks[T]") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cycle?") (("2" (expand "finseq_appl") (("2" (flatten) (("2" (expand "pre_circuit?") (("2" (expand "finseq_appl") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cycle_l_gt_3 formula-decl nil cycles nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (nil application-judgement "finite_set[T]" cycles nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (endpoint? const-decl "bool" paths nil) (pre_circuit? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (cycle? const-decl "bool" cycles nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (walk?_caret formula-decl nil walks nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals 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) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cycles nil)) shostak) (cycle_has_path-1 nil 3312559967 ("" (skosimp*) (("" (auto-rewrite "finseq_appl") (("" (lemma "cycle_l_gt_3") (("" (inst?) (("" (assert) (("" (case "walk?(G!1, w!1)") (("1" (inst 1 "length(w!1)-2") (("1" (expand "path?") (("1" (prop) (("1" (rewrite "walk?_caret") nil) ("2" (skosimp*) (("2" (expand* "^" min empty_seq) (("2" (typepred "j!1") (("2" (typepred "i!1") (("2" (expand* "^" min empty_seq) (("2" (expand "cycle?") (("2" (flatten) (("2" (inst -7 "i!1" "j!1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (assert) (("1" (flatten) (("1" (expand "endpoint?") (("1" (assert) nil))))))))))) ("2" (assert) nil) ("3" (assert) nil))))))))))))))))))))))) ("2" (hide 2) (("2" (expand "cycle?") (("2" (expand "pre_circuit?") (("2" (flatten) (("2" (propax) nil)))))))))))))))))))) nil) ((walk?_caret formula-decl nil walks nil) (endpoint? const-decl "bool" paths nil) (pre_circuit? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (prewalk type-eq-decl nil walks nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil)) nil)) (cycle_gt3 0 (cycle_gt3-1 nil 3312560646 ("" (skosimp*) (("" (expand "cycle?") (("" (expand "pre_circuit?") (("" (flatten) (("" (inst - "1" "(length(w!1) - 2)") (("1" (expand "endpoint?") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cycle? const-decl "bool" cycles nil) (endpoint? const-decl "bool" paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below 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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cycles nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (G!1 skolem-const-decl "graph[T]" cycles nil) (Seq type-eq-decl nil walks nil) (w!1 skolem-const-decl "Seq[T](G!1)" cycles nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pre_circuit? const-decl "bool" walks nil)) shostak)) (cycle_def 0 (cycle_def-1 nil 3312561988 ("" (skosimp*) (("" (expand "cycle?") (("" (expand "endpoint?") (("" (expand "pre_circuit?") (("" (ground) (("" (inst - "1" "(length(w!1) - 2)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cycle? const-decl "bool" cycles nil) (pre_circuit? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil cycles nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (endpoint? const-decl "bool" paths nil)) nil))) ¤ Dauer der Verarbeitung: 0.4 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.Bot Zugriff |
