| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: min_walk_reduced.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(graph_complected
(two_vertices 0 (two_vertices-1 nil 3262679921 ("" (skosimp*) (("" (typepred "e!1") (("" (skosimp*) (("" (typepred "G!1") (("" (inst?) (("" (assert) (("" (inst-cp -1 "x!1") (("" (inst -1 "y!1") (("" (replace -3 -1) (("" (replace -3 -2) (("" (expand "dbl" -1) (("" (expand "dbl" -2) (("" (replace -6) (("" (expand "dbl" -1) (("" (expand "dbl" -2) (("" (ground) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (expand "dbl") (("1" (propax) nil))))))))))))) ("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (replace -1) (("2" (hide -1) (("2" (expand "dbl") (("2" (propax) nil)))))))))))))))))))))))))))))))))))))))))))))) nil) ((doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil graph_complected nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" graph_complected nil)) nil)) (sub_T 0 (sub_T-1 nil 3262679921 ("" (induct "G" 1 "graph_induction_vert") (("" (skosimp*) (("" (expand "connected?" -3) (("" (prop) (("1" (hide -2) (("1" (typepred "v!1") (("1" (expand "singleton?") (("1" (expand "size") (("1" (assert) (("1" (expand "del_vert") (("1" (rewrite "empty_card[T]") (("1" (rewrite "card_remove") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -3 "del_vert(G!1, v!2)") (("2" (rewrite "size_del_vert") (("2" (assert) (("2" (inst -3 "v!1") (("1" (prop) (("1" (case "vert(G!1) = dbl[T](v!1,v!2)") (("1" (hide -2 -4 1) (("1" (expand "deg") (("1" (rewrite "card_is_0[doubleton[T]]") (("1" (lemma "nonempty_card[doubleton[T]]") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (skosimp*) (("1" (hide -3) (("1" (case "incident_edges(v!1, G!1)(x!1) = emptyset(x!1)") (("1" (hide -4) (("1" (expand "incident_edges") (("1" (expand "emptyset") (("1" (flatten) (("1" (assert) (("1" (lemma "two_vertices") (("1" (inst?) (("1" (inst -1 "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 -4 2) (("2" (expand "del_vert") (("2" (expand "remove") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "dbl") (("2" (apply-extensionality 1 :hide? t) (("2" (inst -1 "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (case "v!1 = v!2") (("1" (assert) nil nil) ("2" (lemma "del_vert_not_incident") (("2" (inst?) (("2" (assert) (("2" (hide -2 2) (("2" (expand "deg") (("2" (rewrite "card_empty?[doubleton[T]]") (("2" (expand "empty?") (("2" (expand "member") (("2" (expand "incident_edges") (("2" (inst?) (("2" (assert) (("2" (expand "dbl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "v!1") (("2" (hide -2 -3 -4 2) (("2" (rewrite "del_vert_still_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((size const-decl "nat" graphs nil) (finite_remove application-judgement "finite_set" finite_sets nil) (card_remove formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (empty_card formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (remove const-decl "set" sets nil) (singleton? const-decl "bool" graphs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (del_vert_still_in formula-decl nil graph_ops nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (card_is_0 formula-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (two_vertices formula-decl nil graph_complected nil) (emptyset const-decl "set" sets nil) (nonempty_card formula-decl nil finite_sets nil) (nil application-judgement "finite_set[T]" graph_complected nil) (card_empty? formula-decl nil finite_sets nil) (del_vert_not_incident formula-decl nil graph_deg nil) (v!1 skolem-const-decl "(vert(G!1))" graph_complected nil) (v!2 skolem-const-decl "(vert(G!1))" graph_complected nil) (G!1 skolem-const-decl "graph[T]" graph_complected nil) (size_del_vert formula-decl nil graph_ops nil) (graph_induction_vert formula-decl nil graph_inductions nil) (T formal-type-decl nil graph_complected nil) (connected? def-decl "bool" graph_conn_defs nil) (deg const-decl "nat" graph_deg nil) (nat nonempty-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) (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) (del_vert const-decl "graph[T]" graph_ops nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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)) nil)) (rev_lem2 0 (rev_lem2-1 nil 3262679921 ("" (induct "G" 1 "graph_induction_vert") (("" (skosimp*) (("" (lemma "singleton_deg") (("" (inst?) (("" (assert) (("" (case "(EXISTS (x: (vert(G!1))): deg(x,G!1) > 0 AND connected?(del_vert(G!1, x)))") (("1" (skosimp*) (("1" (case-replace "x!1 = v!1") (("1" (case "edges(G!1)(dbl[T](x!1,v!1))") (("1" (case "vert(del_vert(del_vert(G!1, x!1), v!1)) = emptyset[T]") (("1" (hide -5) (("1" (expand "connected?" 3) (("1" (flatten) (("1" (hide -2 -3 -4 -5 -6 2 4) (("1" (expand "singleton?") (("1" (expand "size") (("1" (lemma "card_is_0[T]") (("1" (inst -1 "vert(del_vert(del_vert(G!1, x!1), v!1))") (("1" (iff -1) (("1" (flatten) (("1" (assert) (("1" (lemma "size_del_vert ") (("1" (inst -1 "del_vert(G!1, v!1)" "x!1") (("1" (rewrite "del_vert_comm") (("1" (expand "size") (("1" (assert) nil))))) ("2" (rewrite "del_vert_still_in") nil))))))))))))))))))))))))))) ("2" (hide -4) (("2" (lemma "sub_T") (("2" (inst -1 "del_vert(G!1,x!1)" "v!1") (("1" (assert) (("1" (prop) (("1" (hide -2 -3 -4 -5 -6 3 4) (("1" (lemma "emptyset_is_empty?[T]") (("1" (inst?) (("1" (assert) nil))))))) ("2" (hide -2 -3 -4 2 4 5 6) (("2" (assert) (("2" (lemma "deg_del_vert") (("2" (inst?) (("2" (assert) nil))))))))))))) ("2" (rewrite "del_vert_still_in") nil))))))))) ("2" (inst -3 "del_vert(G!1,x!1)") (("2" (prop) (("1" (inst -1 "v!1") (("1" (expand "connected?" 4) (("1" (prop) (("1" (inst?) (("1" (rewrite "del_vert_comm") (("1" (assert) (("1" (rewrite "del_vert_not_incident") nil))))) ("2" (rewrite "del_vert_still_in") nil))) ("2" (lemma "del_vert_not_incident") (("2" (inst?) (("2" (rewrite "dbl_comm") (("2" (assert) nil))))))))))) ("2" (rewrite "del_vert_still_in") nil))) ("2" (rewrite "size_del_vert") (("2" (assert) nil))))))) ("3" (inst 1 "x!1" "v!1") (("3" (assert) nil))))))))) ("2" (hide -1) (("2" (expand "connected?" -1) (("2" (propax) nil)))))))))))))))) nil) ((> const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (del_vert_not_incident formula-decl nil graph_deg nil) (dbl_comm formula-decl nil doubletons nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (size const-decl "nat" graphs nil) (is_finite const-decl "bool" finite_sets nil) (size_del_vert formula-decl nil graph_ops nil) (del_vert_still_in formula-decl nil graph_ops nil) (del_vert_comm formula-decl nil graph_ops nil) (int_minus_int_is_int application-judgement "int" integers nil) (x!1 skolem-const-decl "(vert(G!1))" graph_complected nil) (v!1 skolem-const-decl "(vert(G!1))" graph_complected nil) (G!1 skolem-const-decl "graph[T]" graph_complected nil) (card_is_0 formula-decl nil finite_sets nil) (singleton? const-decl "bool" graphs nil) (sub_T formula-decl nil graph_complected nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deg_del_vert formula-decl nil graph_deg nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (nil application-judgement "finite_set[T]" graph_complected nil) (singleton_deg formula-decl nil graph_deg nil) (graph_induction_vert formula-decl nil graph_inductions nil) (T formal-type-decl nil graph_complected nil) (del_vert const-decl "graph[T]" graph_ops nil) (deg const-decl "nat" graph_deg nil) (nat nonempty-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) (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) (connected? def-decl "bool" graph_conn_defs nil) (pred type-eq-decl nil defined_types 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)) nil)) (conn_lem2 0 (conn_lem2-1 nil 3262679921 ("" (skosimp*) (("" (lemma "rev_lem2") (("" (inst?) (("" (assert) (("" (inst 2 "v!1") (("" (assert) nil)))))))))) nil) ((rev_lem2 formula-decl nil graph_complected 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 graph_complected nil)) nil)) (del_rem_lem 0 (del_rem_lem-1 nil 3262679921 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (expand "del_vert") (("1" (expand "del_edge") (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil))))))) ("2" (grind) nil)))) nil) ((T formal-type-decl nil graph_complected 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) (del_edge const-decl "graph[T]" graph_ops nil) (del_vert const-decl "graph[T]" graph_ops nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (finite_remove application-judgement "finite_set" finite_sets nil) (remove const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (conn_lem3 0 (conn_lem3-1 nil 3262679921 ("" (skosimp*) (("" (expand "connected?" -1) (("" (prop) (("1" (hide 2 3) (("1" (expand "isolated?") (("1" (rewrite "singleton_edges") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (case "(EXISTS (e: doubleton[T], y:T): e = dbl(y,v!1) AND edges(G!1)(e))") (("1" (skosimp*) (("1" (inst 3 "e!1") (("1" (name "HH" "del_edge(G!1,e!1)") (("1" (name "KK" "del_vert(G!1,v!1)") (("1" (replace -1) (("1" (replace -2) (("1" (expand "connected?" +) (("1" (flatten) (("1" (inst 2 "v!1") (("1" (inst 4 "v!1") (("1" (prop) (("1" (replace -2 * rl) (("1" (hide -2) (("1" (lemma "deg_del_edge") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "del_vert(HH,v!1) = KK") (("1" (assert) nil nil) ("2" (replace -2 * rl) (("2" (hide -2) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (hide -3 -4 2 3 4 5) (("2" (lemma "del_rem_lem") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (replace -1) (("2" (hide -1) (("2" (expand "dbl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "v!1") (("2" (replace -3 * rl) (("2" (rewrite "vert_del_edge") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2 3 4) (("2" (expand "deg") (("2" (lemma "empty_card[doubleton[T]]") (("2" (inst?) (("2" (flatten) (("2" (assert) (("2" (hide -1) (("2" (expand "empty?") (("2" (expand "incident_edges") (("2" (skosimp*) (("2" (expand "member") (("2" (flatten) (("2" (lemma "other_vert") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (inst + "x!1" "u!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((connected? def-decl "bool" graph_conn_defs nil) (empty_card formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (other_vert formula-decl nil graphs nil) (empty? const-decl "bool" sets nil) (is_finite const-decl "bool" finite_sets nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (deg const-decl "nat" graph_deg nil) (del_edge const-decl "graph[T]" graph_ops nil) (NOT const-decl "[bool -> bool]" booleans nil) (vert_del_edge formula-decl nil graph_ops nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deg_del_edge formula-decl nil graph_deg nil) (del_rem_lem formula-decl nil graph_complected nil) (v!1 skolem-const-decl "(vert(G!1))" graph_complected nil) (HH skolem-const-decl "graph[T]" graph_complected nil) (del_vert const-decl "graph[T]" graph_ops nil) (G!1 skolem-const-decl "graph[T]" graph_complected nil) (e!1 skolem-const-decl "doubleton[T]" graph_complected nil) (nil application-judgement "finite_set[T]" graph_complected nil) (singleton_edges formula-decl nil graphs 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_complected nil) (isolated? const-decl "bool" graphs nil)) nil)) (BIG 0 (BIG-1 nil 3262679921 ("" (induct "G" 1 "graph_induction_vert") (("" (skosimp*) (("" (case "edges(G!1)(e!1)") (("1" (hide -2) (("1" (case "(EXISTS (v: T): vert(G!1)(v) AND deg(v,G!1) = 1)") (("1" (name "H" "del_edge(G!1,e!1)") (("1" (skosimp*) (("1" (case "(EXISTS (u: T): vert(G!1)(u) AND e!1 = dbl[T](u,v!1))") (("1" (skosimp*) (("1" (lemma "deg_del_edge") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (replace -6) (("1" (assert) (("1" (lemma "sub_T") (("1" (inst?) (("1" (assert) (("1" (lemma " del_vert_empty?") (("1" (inst -1 "H" "v!1") (("1" (assert) (("1" (replace -6) (("1" (expand "connected?" 1) (("1" (flatten) (("1" (lemma "del_edge_singleton") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -5 + rl) (("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "GP" "del_vert(G!1,v!1)") (("2" (name "K" "del_vert(H,v!1)") (("2" (case "K = del_edge(GP,e!1)") (("1" (case "connected?(K)") (("1" (reveal -1) (("1" (inst -1 "GP") (("1" (split -1) (("1" (inst?) (("1" (assert) (("1" (expand "connected?" 2) (("1" (flatten) (("1" (inst 3 "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "size") (("2" (replace -4 + rl) (("2" (hide -1 -2 -3 -4 -5 -7 -8 -9 2 3) (("2" (expand "del_vert") (("2" (rewrite "card_remove[T]") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "rev_lem2") (("2" (inst?) (("1" (assert) (("1" (replace -4 + rl) (("1" (lemma "deg_del_edge3") (("1" (inst?) (("1" (assert) (("1" (hide -2 -3 -4 -5 -7 -9 1 2 4) (("1" (lemma "other_vert") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -4 + rl) (("2" (expand "del_edge" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -7 2 3) (("2" (replace -2 + rl) (("2" (replace -1 + rl) (("2" (replace -3 + rl) (("2" (hide -1 -2 -3) (("2" (rewrite "del_vert_edge_comm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(FORALL (v: T): vert(G!1)(v) IMPLIES deg(v, G!1) > 1)") (("1" (name "H" "del_edge(G!1,e!1)") (("1" (case "(EXISTS (u: T): vert(G!1)(u) AND deg(u,H) = 1)") (("1" (skosimp*) (("1" (case "(EXISTS (z: T): vert(H)(z) AND e!1 = dbl[T](u!1,z))") (("1" (skosimp*) (("1" (name "K" "del_vert(G!1,u!1)") (("1" (case "K = del_vert(H,u!1)") (("1" (case "connected?(K)") (("1" (expand "connected?" 2) (("1" (flatten) (("1" (inst 3 "u!1") (("1" (assert) (("1" (hide -1 -2 -3 -4 -5 -9 -11 1 2) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (lemma "deg_del_edge_ge") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -7) (("2" (lemma "rev_lem2") (("2" (inst?) (("1" (assert) nil nil) ("2" (hide -1 -2 -3 -4 -6 -8 -9 -10 2 3 4) (("2" (replace -2 * rl) (("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "del_vert_edge") (("2" (inst?) (("2" (inst -1 "u!1") (("2" (assert) (("2" (replace -3) (("2" (expand "dbl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -4 "u!1") (("2" (assert) (("2" (replace -3 * rl) (("2" (hide -3) (("2" (case "e!1(u!1)") (("1" (lemma "edges_vert") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst 2 "y!1") (("1" (lemma "edge_has_2_verts") (("1" (inst?) (("1" (assert) (("1" (expand "del_edge") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 2 3 4) (("2" (lemma "deg_del_edge3") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(FORALL (v: T): vert(H)(v) IMPLIES deg(v,H) > 1)") (("1" (case "(EXISTS (z: T): vert(H)(z) AND deg(z,H) > 0 AND connected?(del_vert(H,z)))") (("1" (skosimp*) (("1" (case "(EXISTS (p: T): p /= z!1 AND vert(H)(p) AND e!1 = dbl[T](z!1,p))") (("1" (skosimp*) (("1" (case "del_vert(H,z!1) = del_vert(G!1,z!1)") (("1" (expand "connected?" 4) (("1" (flatten) (("1" (replace -1) (("1" (inst 5 "z!1") (("1" (assert) (("1" (hide -2 -3 -4 -5 -6 -8 -10 2 3 4) (("1" (lemma "deg_del_edge_ge") (("1" (inst?) (("1" (assert) (("1" (inst -4 "z!1") (("1" (assert) (("1" (reveal -5 -8) (("1" (hide -3 -5) (("1" (replace -2 * rl) (("1" (expand "del_edge" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 -5 -6 -7 -9 3 4 5) (("2" (replace -1) (("2" (hide -1) (("2" (typepred "G!1") (("2" (inst?) (("1" (assert) (("1" (inst -1 "z!1") (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "del_vert_edge") (("2" (inst?) (("2" (inst -1 "z!1") (("2" (assert) (("2" (hide -1 -4 -5 -6 -8 -10 2 4 5 6) (("2" (replace -1) (("2" (hide -1) (("2" (expand "dbl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "K" "del_vert(H,z!1)") (("2" (replace -1) (("2" (replace -6) (("2" (name "GP" "del_vert(G!1,z!1)") (("2" (case "K = del_edge(GP,e!1)") (("1" (case "size(GP) < size(G!1)") (("1" (reveal -1) (("1" (inst -1 "GP") (("1" (assert) (("1" (inst -1 "e!1") (("1" (assert) (("1" (expand "connected?" 4) (("1" (flatten) (("1" (inst 5 "z!1") (("1" (assert) (("1" (hide -1 -2 -3 -4 -5 -8 -9 -11 -12 -13 1 2 3 4) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (expand "del_edge" -1) (("1" (lemma "deg_del_edge_ge") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.129 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 |
