| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 554 kB |
|
Quelle cycle_deg.prf Sprache: Lisp |
|||||||||
|
(cycle_deg
(reachable_TCC1 0 (reachable_TCC1-2 nil 3312297543 ("" (skosimp*) (("" (typepred "vert(G!1)") (("" (lemma "finite_subset[T]") (("" (inst -1 "vert(G!1)" "{y: T | vert(G!1)(y) AND (EXISTS (w: Seq[T](G!1)): walk_from?[T](G!1, w, x!1, y))}") (("" (bddsimp) (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil cycle_deg nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (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) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (finite_subset formula-decl nil finite_sets nil)) nil) (reachable_TCC1-1 nil 3312285093 ("" (subtype-tcc) nil nil) nil nil)) (reachable_subset 0 (reachable_subset-1 nil 3312297501 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil cycle_deg 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (reachable const-decl "finite_set[T]" cycle_deg nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" cycle_deg nil)) shostak)) (reachable_conn 0 (reachable_conn-5 nil 3559571065 ("" (skosimp*) (("" (lemma "conn_eq_path") (("" (inst -1 "subgraph(G!1, reachable(G!1, x!1))") (("" (iff -1) (("" (bddsimp) (("" (hide 1) (("" (expand "path_connected?") (("" (bddsimp) (("1" (install-rewrites "subgraphs") (("1" (assert) (("1" (inst -1 "x!1") (("1" (bddsimp) (("1" (inst 1 "(#length := 1, seq :=(LAMBDA (i:below(1)): x!1)#)") (("1" (assert) nil nil)) nil) ("2" (typepred "x!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!2") (("2" (typepred "y!1") (("2" (expand "subgraph" -) (("2" (flatten) (("2" (expand "reachable" -) (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk?_reverse") (("2" (inst-cp -1 "G!1" "x!1" "y!1" "w!1") (("2" (inst -1 "G!1" "x!1" "x!2" "w!2") (("2" (bddsimp) (("2" (skosimp*) (("2" (lemma "walk_merge") (("2" (inst -1 "G!1" "w!4" "w!3" "x!2" "y!1" "x!1") (("2" (bddsimp) (("2" (skosimp*) (("2" (inst 1 "p!1") (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) nil nil)) nil)) nil) ("2" (assert) (("2" (install-rewrites "walks") (("2" (assert) (("2" (skosimp*) (("2" (bddsimp) (("1" (skosimp*) (("1" (bddsimp) (("1" (typepred "p!1") (("1" (inst -11 "n!1") (("1" (bddsimp) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst-cp -9 "n!1") (("1" (inst -9 "1+n!1") (("1" (hide -3 -4 -5 -6) (("1" (bddsimp (-2 -5 -6 1)) (("1" (hide -8 -9 -11 -12) (("1" (reveal -10 -11) (("1" (reveal (-1 -2 -7 -8)) (("1" (lemma "walk?_caret") (("1" (inst -1 "G!1" "0" "n!1" "p!1") (("1" (stop-rewrite) (("1" (assert) (("1" (case "walk?(G!1,p!1)") (("1" (bddsimp) (("1" (inst -8 "G!1" "x!2" "x!3" "p!1 ^ (0, n!1)") (("1" (expand "walk_from?" -8) (("1" (expand "^" -8 (1 2 3)) (("1" (bddsimp (-2 -8)) (("1" (skosimp*) (("1" (inst -9 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (expand "walk_from?" -9 (1 2)) (("1" (typepred "w!2") (("1" (case "walk?(G!1,w!2)") (("1" (bddsimp) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (expand "walk_from?" -12) (("1" (flatten) (("1" (expand "walk?" -14) (("1" (flatten) (("1" (hide-all-but (-4 -7 -12 -13 -14 -15 -25 -26) -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -12 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -7 -8 -19) -) (("2" (hide 2) (("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand min) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal -10) (("2" (hide (-16 -17)) (("2" (hide-all-but (-1 -9 -12 -13 -14 -15) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -3) -) (("2" (assert) nil nil)) nil) ("3" (reveal -6 -7) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "1+n!1" "p!1") (("3" (inst -3 "G!1" "x!2" "x!3" "p!1 ^ (0, 1 + n!1)") (("1" (typepred "n!1") (("1" (bddsimp (-1 -2 -4 -5 -8)) (("1" (skosimp*) (("1" (inst -6 "G!1" "w!5" "w!2" "x!1" "x!3" "x!2") (("1" (hide-all-but (-3 -6 -12 -13 -14) -) (("1" (typepred "w!2") (("1" (case "walk_from?(G!1, w!2, x!1, x!2)") (("1" (bddsimp (-1 -4 -5)) (("1" (skosimp*) (("1" (inst 1 "p!2") (("1" (hide-all-but -3 -) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but -3 -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -5 -6 -7) -) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide (-5 -11 -12 -13 -14 -15 -16 -17 -18)) (("2" (assert) (("2" (bddsimp) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -2 -5 -11 -12 -13 -14 -15 -16) (("3" (assert) (("3" (bddsimp) (("3" (typepred "p!1") (("3" (reveal -13) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -4 -12 -15 3) (("4" (reveal -8) (("4" (hide 2) (("4" (assert) (("4" (bddsimp) nil nil)) nil)) nil)) nil)) nil) ("5" (assert) nil nil) ("6" (assert) nil nil) ("7" (assert) nil nil) ("8" (assert) nil nil)) nil)) nil) ("2" (hide -2 -9 -12 -15 2) (("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert (-1 -2 1)) nil nil)) nil)) nil) ("2" (assert (-1 1)) nil nil)) nil) ("2" (assert (-1 1)) nil nil)) nil)) nil) ("3" (inst -9 "n!1") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -7 "i!1") (("2" (bddsimp) (("2" (lemma "walk?_caret") (("2" (inst -1 "G!1" "0" "i!1" "p!1") (("2" (typepred "i!1") (("2" (reveal -4) (("2" (inst -1 "G!1" "x!2" "seq(p!1)(i!1)" "p!1 ^ (0, i!1)") (("1" (case --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.38Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28