|
(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.127 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.
|
