| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 135 kB |
|
Quelle graph_complected.prfSprache: Lisp |
|||||||||||||||
|
(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 -1 -2 -3 -4 -5 -7 -8 -9 -11 -12 -13 2 3 4 5) (("2" (replace -2 * rl) (("2" (hide -2) (("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -5 -6 -7 -9 -10 -11 2 3 4 5) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (replace -2 * rl) (("2" (hide -2) (("2" (expand "del_edge") (("2" (expand "size") (("2" (expand "del_vert") (("2" (rewrite "card_remove") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "del_vert_edge_comm") (("2" (replace -3 * rl) (("2" (replace -8 * rl) (("2" (replace -2 * rl) (("2" (hide -2 -3 -5 -6 -7 -8 -9 -11 2 3 4 5) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (expand "connected?" -5) (("2" (split -5) (("1" (hide -2 -4 1 2 3 4) (("1" (replace -2 * rl) (("1" (lemma "del_edge_singleton") (("1" (inst?) (("1" (assert) (("1" (hide -2 -3) (("1" (lemma "edge_in_card_gt_1") (("1" (inst?) (("1" (assert) (("1" (expand "singleton?") (("1" (expand "size") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst 1 "v!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst 2 "v!1") (("2" (inst -3 "v!1") (("2" (replace -2 * rl) (("2" (expand "del_edge" -1) (("2" (assert) (("2" (lemma "deg_del_edge_le") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (case "deg(v!1, G!1) = 0") (("1" (case "vert(del_edge(G!1, e!1))(v!1)") (("1" (case "card(vert(del_edge(G!1,e!1))) > 1") (("1" (case "NOT empty?(vert(del_vert(del_edge(G!1, e!1), v!1)))") (("1" (lemma "sub_T") (("1" (inst -1 "del_edge(G!1, e!1)" "v!1") (("1" (assert) (("1" (hide -1 -6 2 3 4 5) (("1" (lemma "deg_del_edge3") (("1" (inst?) (("1" (assert) (("1" (expand "deg") (("1" (lemma "empty_card[doubleton[T]]") (("1" (inst -1 "incident_edges(v!1, G!1)") (("1" (assert) (("1" (hide -3 -4 -5 1) (("1" (expand "incident_edges") (("1" (expand "empty?") (("1" (inst?) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -4 -7 1 2 3) (("2" (lemma "empty_card[T]") (("2" (inst?) (("2" (assert) (("2" (hide -2 -5 -6) (("2" (grind) (("2" (rewrite "card_remove[T]") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "edge_in_card_gt_1") (("2" (inst -1 "G!1" "e!1") (("2" (assert) (("2" (hide -2 -3 -4 -5 -6 2 3 4) (("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "del_edge") (("2" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "del_edge_lem5") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((del_edge_lem5 formula-decl nil graph_ops nil) (> const-decl "bool" reals nil) (del_vert_edge formula-decl nil graph_ops nil) (deg_del_edge_ge formula-decl nil graph_deg nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (u!1 skolem-const-decl "T" graph_complected nil) (H skolem-const-decl "graph[T]" graph_complected nil) (edges_vert formula-decl nil graphs nil) (edge_has_2_verts formula-decl nil graphs nil) (deg_del_edge_le formula-decl nil graph_deg nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (z!1 skolem-const-decl "T" graph_complected nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (edge_in_card_gt_1 formula-decl nil graphs nil) (singleton? const-decl "bool" graphs nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (finite_remove application-judgement "finite_set" finite_sets nil) (remove const-decl "set" sets nil) (empty_card formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (v!1 skolem-const-decl "T" graph_complected nil) (empty? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" graph_complected nil) (deg_del_edge formula-decl nil graph_deg nil) (sub_T formula-decl nil graph_complected nil) (H skolem-const-decl "graph[T]" graph_complected nil) (del_edge_singleton formula-decl nil graph_ops nil) (del_vert_empty? formula-decl nil graph_ops nil) (v!1 skolem-const-decl "T" graph_complected nil) (e!1 skolem-const-decl "doubleton[T]" graph_complected nil) (G!1 skolem-const-decl "graph[T]" graph_complected nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (del_vert_edge_comm formula-decl nil graph_ops nil) (size const-decl "nat" graphs nil) (is_finite const-decl "bool" finite_sets nil) (card_remove formula-decl nil finite_sets 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) (other_vert formula-decl nil graphs nil) (deg_del_edge3 formula-decl nil graph_deg nil) (rev_lem2 formula-decl nil graph_complected nil) (del_vert const-decl "graph[T]" graph_ops 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) (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) (deg const-decl "nat" graph_deg nil) (graph_induction_vert formula-decl nil graph_inductions nil) (T formal-type-decl nil graph_complected nil) (del_edge const-decl "graph[T]" graph_ops 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_lem6 0 (conn_lem6-1 nil 3262679921 ("" (skosimp*) (("" (lemma "BIG") (("" (inst?) (("" (assert) nil)))))) nil) ((BIG 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)) (conn_eq_compl 0 (conn_eq_compl-1 nil 3262679921 ("" (skosimp*) (("" (prop) (("1" (expand "connected?") (("1" (assert) (("1" (expand "singleton?") (("1" (skosimp*) (("1" (expand "isolated?") (("1" (lemma "deg_edge_exists") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "empty?") (("1" (inst?) (("1" (expand "member") (("1" (propax) nil))))))))))))))))))))))))) ("2" (skosimp*) (("2" (lemma "conn_lem2") (("2" (inst?) (("2" (assert) nil))))))) ("3" (rewrite "conn_lem3") nil) ("4" (expand "connected?") (("4" (assert) nil))) ("5" (skosimp*) (("5" (expand "connected?" 2) (("5" (flatten) (("5" (inst 3 "x!1") (("5" (assert) nil))))))))) ("6" (skosimp*) (("6" (lemma "conn_lem6") (("6" (inst?) (("6" (assert) nil)))))))))) nil) ((deg_edge_exists formula-decl nil graph_deg nil) (T formal-type-decl nil graph_complected nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (isolated? const-decl "bool" graphs nil) (singleton? const-decl "bool" graphs nil) (connected? def-decl "bool" graph_conn_defs nil) (conn_lem2 formula-decl nil graph_complected nil) (conn_lem3 formula-decl nil graph_complected nil) (conn_lem6 formula-decl nil graph_complected nil)) nil)) (conn_del_vert 0 (conn_del_vert-1 nil 3262679921 ("" (skosimp*) (("" (lemma "conn_eq_compl") (("" (inst?) (("" (flatten) (("" (hide -2) (("" (assert) (("" (split -1) (("1" (flatten) (("1" (expand "connected?") (("1" (flatten) (("1" (inst 2 "v!1") (("1" (assert) nil))))))))) ("2" (flatten) (("2" (split -1) (("1" (flatten) (("1" (skosimp*) (("1" (expand "connected?") (("1" (assert) (("1" (flatten) (("1" (inst?) (("1" (assert) nil))))))))))))) ("2" (flatten) (("2" (expand "connected?" 3) (("2" (flatten) (("2" (inst 4 "v!1") (("2" (assert) nil)))))))))))))))))))))))))) nil) ((conn_eq_compl formula-decl nil graph_complected nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (connected? def-decl "bool" graph_conn_defs 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) (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)) (connected_not_empty 0 (connected_not_empty-1 nil 3262679921 ("" (skosimp*) (("" (expand "empty?") (("" (expand "connected?") (("" (lemma " card_empty?[T]") (("" (inst?) (("" (iff) (("" (assert) (("" (prop) (("1" (expand "singleton?") (("1" (expand "size") (("1" (assert) nil))))) ("2" (skosimp*) (("2" (expand "empty?") (("2" (inst -4 "v!1") (("2" (expand "member") (("2" (propax) nil)))))))))))))))))))))))) nil) ((empty? const-decl "bool" graphs nil) (T formal-type-decl nil graph_complected nil) (card_empty? formula-decl nil finite_sets nil) (size const-decl "nat" graphs nil) (singleton? const-decl "bool" graphs nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (connected? def-decl "bool" graph_conn_defs nil)) nil)) (connect_deg_0 0 (connect_deg_0-1 nil 3262679921 ("" (lemma "size_prep") (("" (inst -1 "LAMBDA G:(FORALL v:( connected?(G) AND vert(G)(v) AND deg(v, G) = 0 IMPLIES G = singleton_gra (("" (flatten) (("" (bddsimp) (("1" (hide -2) (("1" (assert) (("1" (skosimp*) (("1" (inst -1 "G!1") (("1" (inst -1 "v!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1 3) (("2" (induct "n" 1 "nat_induction") (("1" (skosimp*) (("1" (lemma "empty?_rew") (("1" (inst -1 "G!1") (("1" (iff -1) (("1" (bddsimp) (("1" (expand "deg" -6) (("1" (hide -2 -3) (("1" (expand "empty?" -1) (("1" (expand "empty?" -1) (("1" (inst -1 "v!1") (("1" (expand "member" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal -1) (("2" (lemma "connected_not_empty") (("2" (inst -1 "G!1") (("2" (bddsimp -1 -4) (("1" (hide -1 -3 -4 -5 1 2 4) (("1" (grind) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "connected?" -3) (("2" (split -3) (("1" (hide -2 -3) (("1" (grind) (("1" (apply-extensionality 1) (("1" (hide 2) (("1" (lemma "finite_sets[T].card_one") (("1" (inst -1 "vert(G!1)") (("1" (bddsimp -1 -2) (("1" (skosimp*) (("1" (hide -1 -3) (("1" (lemma "finite_sets[doubleton[T]].empty_card") (("1" (inst -1 "incident_edges(v!1, G!1)") (("1" (bddsimp) (("1" (hide -2) (("1" (replace -2 -3) (("1" (expand "singleton" -3) (("1" (replace -3 -2 rl) (("1" (hide -3) (("1" (expand "empty?" -1) (("1" (expand "emptyset" 1) (("1" (apply-extensionality 1) (("1" (inst -2 "x!2") (("1" (typepred "G!1") (("1" (inst -1 "x!2") (("1" (bddsimp -1 -2) (("1" (typepred "x!2") (("1" (skosimp*) (("1" (hide -3 3) (("1" (inst-cp -2 "x!3") (("1" (inst -2 "y!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (grind) (("2" (lemma "finite_sets[T].card_one") (("2" (inst -1 "vert(G!1)") (("2" (bddsimp -1 -2) (("1" (hide -1 -3) (("1" (grind) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "v!1=v!2") (("1" (replace -1 -7) (("1" (hide -3 -4 -5) (("1" (assert) nil nil)) nil)) nil) ("2" (inst -3 "del_vert(G!1, v!2)") (("2" (lemma "graph_ops[T].size_del_vert") (("2" (inst -1 "G!1" "v!2") (("2" (replace -5 -1) (("2" (assert -1) (("2" (bddsimp (-1 -4)) (("2" (lemma "graph_ops[T].del_vert_still_in") (("2" (lemma "graph_deg[T].del_vert_not_incident") (("2" (inst -4 "v!1") (("2" (inst -2 "G!1" "v!2" "v!1") (("2" (bddsimp (-2 1)) (("1" (inst -2 "G!1" "v!2" "v!1") (("1" (bddsimp (-2 1)) (("1" (hide -3 -4 -6 -7 2) (("1" (grind) (("1" (expand "incident_edges" -4) (("1" (lemma "finite_sets[doubleton[T]].empty_card") (("1" (inst -1 "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}") (("1" (bddsimp (-1 -5)) (("1" (expand "empty?" -1) (("1" (inst -1 "dbl[T](v!1, v!2)") (("1" (expand "member" 1) (("1" (hide -1 -2 -3 -4) (("1" (grind) nil nil)) nil)) nil) ("2" (hide -1 -2 -3 -4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "graph_deg[T].incident_edges_TCC1") (("2" (inst -1 "G!1" "v!1") (("2" (hide -2 -4 -5 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9 -1) (("2" (bddsimp (-1 -2 -4 -6)) (("2" (hide -3 -5 -7) (("2" (expand "deg" -4) (("2" (lemma "finite_sets[doubleton[T]].nonempty_card") (("2" (inst -1 "incident_edges(v!2, G!1)") (("2" (bddsimp (-1 -5)) (("2" (expand "nonempty?" -1) (("2" (expand "empty?" 1) (("2" (skosimp*) (("2" (expand "member" -1) (("2" (hide -2) (("2" (expand "incident_edges" -1) (("2" (lemma "graphs[T].other_vert") (("2" (inst -1 "G!1" "x!1" "v!2") (("2" (bddsimp (-1 -2)) (("2" (skosimp*) (("2" (lemma "graph_ops[T].del_vert_still_in") (("2" (inst -1 "G!1" "v!2" "u!1") (("2" (bddsimp (-1 1)) (("1" (typepred "G!1") (("1" (inst -1 "x!1") (("1" (bddsimp (-1 -4)) (("1" (inst -2 "v!2") (("1" (bddsimp (-2 -4)) (("1" (case "deg(u!1,G!1)=0") (("1" (expand "deg" -1) (("1" (lemma "finite_sets[doubleton[T]].empty_card") (("1" (inst -1 "incident_edges(u!1, G!1)") (("1" (bddsimp (-1 -2)) (("1" (expand "empty?" -1) (("1" (inst -1 "x!1") (("1" (expand "member" 1) (("1" (expand "incident_edges" 1) (("1" (hide -1 -3 -5 -8 -9 -10 -12 4) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton_graph" -9) (("2" (replace -9 -8) (("2" (beta -8) (("2" (replace -9 -4) (("2" (beta -4) (("2" (hide -9 4) (("2" (hide -7) (("2" (hide -6) (("2" (expand "singleton" -4) (("2" (replace -4 -8 rl) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("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) ((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) (pred type-eq-decl nil defined_types nil) (connected? def-decl "bool" graph_conn_defs 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) (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) (deg const-decl "nat" graph_deg nil) (singleton? const-decl "bool" graphs nil) (singleton_graph const-decl "(singleton?)" graphs nil) (size const-decl "nat" graphs nil) (nat_induction formula-decl nil naturalnumbers nil) (empty?_rew formula-decl nil graphs nil) (connected_not_empty formula-decl nil graph_complected nil) (empty? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (del_vert const-decl "graph[T]" graph_ops nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (del_vert_still_in formula-decl nil graph_ops nil) (remove const-decl "set" sets nil) (finite_remove application-judgement "finite_set" finite_sets nil) (incident_edges_TCC1 subtype-tcc nil graph_deg nil) (injective? const-decl "bool" functions nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nonempty? const-decl "bool" sets nil) (other_vert formula-decl nil graphs nil) (u!1 skolem-const-decl "T" graph_complected nil) (nonempty_card formula-decl nil finite_sets nil) (v!1 skolem-const-decl "T" graph_complected nil) (G!1 skolem-const-decl "graph[T]" graph_complected nil) (del_vert_not_incident formula-decl nil graph_deg nil) (size_del_vert formula-decl nil graph_ops nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (emptyset const-decl "set" sets nil) (card_one formula-decl nil finite_sets nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (nil application-judgement "finite_set[T]" graph_complected nil) (NOT const-decl "[bool -> bool]" booleans nil) (FALSE const-decl "bool" booleans nil) (empty_card formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (size_prep formula-decl nil graph_inductions nil) (T formal-type-decl nil graph_complected nil)) nil)))
¤ Dauer der Verarbeitung: 0.77 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26