Quelle trees.prf
Sprache: Lisp
(treesnil 3262616780"" (skosimp*)"" (expand "size" )"" (expand "del_vert" )"" (rewrite "card_remove" ) (("" (assert ) nil ))))))))nil )"nat" graphs nil )nil finite_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil trees nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"graph[T]" graph_ops nil ))nil ))nil 3262616780"" (skosimp*)"" (expand "empty?" )"" (use "card_empty?[T]" )"" (assert )"" (iff)"" (assert )"" (expand "tree?" )"" (skosimp*)"" (use "deg_to_card" )"" (assert )"" (expand "size" )"" (assert ) nil ))))))))))))))))))))))nil )"bool" graphs nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nat" graphs nil )nil graph_deg nil )"bool" trees nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil trees nil )nil finite_sets nil ))nil ))nil 3262616780"" (induct "G" 1 "graph_induction_vert" )"" (skosimp*)"" (expand "tree?" -2)"" (bddsimp)"1" (lemma "singleton_edges" )"1" (inst -1 "G!1" )"1" (expand "singleton?" -1)"1" (expand "size" -1)"1" (assert )"1" "finite_sets[doubleton[T]].empty_card" )"1" (inst -1 "edges(G!1)" )"1" (bddsimp)"1" (assert )"1" (expand "size" 1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "size_del_vert" )"2" (inst -1 "G!1" "v!1" )"2" (inst -2 "del_vert(G!1,v!1)" )"2" (assert )"2" (replace -1 -2)"2" (expand "deg" -3)"2" (expand "incident_edges" -3)"2" "finite_sets[doubleton[T]].card_one" )"2" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" )"1" "1" "1" "1" expand "del_vert" -4)"1" "finite_sets[doubleton[T]].card_disj_union" )"1" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}" )"1" "1" "finite_sets[doubleton[T]].card_singleton" )"1" "x!1" )"1" replace -4 -1 rl)"1" replace -1 -2)"1" assert -6)"1" replace "1" expand "union" "1" expand "member" "1" assert "1" "1" case "{x: doubleton[T] | AND x(v!1) OR edges(G!1)(x) AND NOT x(v!1)}=edges(G!1)") "1" replace "1" assert )nil nil ))nil )"2" "2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint?" )"2" "finite_sets[doubleton[T]]" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_subset[doubleton[T]]" )"2" "edges(G!1)" "{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}" )"2" assert )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "finite_subset[doubleton[T]]" )"3" "edges(G!1)" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "finite_subset[doubleton[T]]" )"2" "edges(G!1)" "{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}" )"2" assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil finite_sets nil )"posint" nil )"posint" nil )"bool" graphs nil )nil graphs nil )nil graph_ops nil )"graph[T]" graph_ops nil )"finite_set[doubleton[T]]" graph_degnil )"graph[T]" trees nil )"(vert(G!1))" trees nil )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )"set" sets nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil )"non_empty_finite_set" finite_sets nil )"(partial_order?[set[T]])" nil )nil finite_sets nil )nil finite_sets nil )nil finite_sets nil )"nat" graph_deg nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil graph_inductions nil )nil trees nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" finite_sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" graphs nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" trees nil )nil defined_types nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3262616780"" (skosimp*)"" (inst? -1)"" (inst -1 "size(G!1)-2" )"1" (lemma "tree_nonempty" )"1" (inst? -1)"1" (bddsimp) (("1" (assert 2) nil nil )) nil )) nil ))nil )"2" (expand "size" 1)"2" (assert 1)"2" (case "card[T](vert(G!1)) > 0" )"1" (hide -2 -3 2) (("1" (grind) nil nil )) nil )"2" (lemma "tree_nonempty" )"2" (inst? -1)"2" (bddsimp)"2" (expand "empty?" 1)"2" (lemma "finite_sets[T].empty_card" )"2" (inst -1 "vert(G!1)" )"2" (bddsimp)"2" (hide -1 -2 1 4 5 6)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trees nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil ) (> const-decl "bool" reals nil )"bool" finite_sets nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" graphs nil )nil finite_sets nil )nil trees nil )"int" integers nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" graphs nil )"graph[T]" trees nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3262616780"" (induct "k" 1 "nat_induction" )"1" (skosimp*)"1" (copy -2)"1" (expand "size" -1)"1" (expand "tree?" -2)"1" (case "card[T](vert(G!1)) = 1" )"1" (propax) nil nil )"2" (split)"1" (propax) nil nil )"2" (hide -3 1 3)"2" (skosimp*)"2" (case "v!2=v!1" )"1" (replace -1 -2) (("1" (assert ) nil nil ))nil )"2" (lemma "size_del_vert" )"2" (inst -1 "G!1" "v!2" )"2" (reveal -2)"2" (replace -1 -2)"2" assert -2)"2" expand "size" -2)"2" "finite_sets[T].card_one" )"2" "vert(del_vert(G!1, v!2))" )"2" "2" "2" "2" "HH" "del_vert(G!1, v!2)" )"2" replace -1 -2)"2" "HH" )"2" expand "del_vert" "2" case "vert(HH)= remove[T](v!2, vert(G!1))" )"1" "1" expand "deg" "1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!2, G!1)" )"1" "1" "1" "1" expand "incident_edges" "1" replace "1" "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})(x!2) = singleton(x!2)(x!2)" )"1" "1" "1" case "singleton(x!2)(x!2)" )"1" "1" "1" "other_vert" )"1" "G!1" "x!2" "v!2" )"1" "1" "1" "1" case " ({y: T | v!2 /= y AND member(y, vert(G!1))})(x!1) = singleton(x!1)(x!1)" )"1" case " ({y: T | v!2 /= y AND member(y, vert(G!1))})(u!1) = singleton(x!1)(u!1)" )"1" case " ({y: T | v!2 /= y AND member(y, vert(G!1))})(v!1) = singleton(x!1)(v!1)" )"1" case " ({y: T | v!2 /= y AND member(y, vert(G!1))})(v!2) = singleton(x!1)(v!2)" )"1" "1" "1" "1" "1" "1" expand "member" "1" expand "singleton" "1" "1" "1" assert )"1" replace "1" "1" replace "1" "1" "1" expand "deg" "1" "finite_sets[doubleton[T]].nonempty_card" )"1" "incident_edges(v!1, G!1)" )"1" "1" expand "nonempty?" "1" expand "empty?" "1" "x!2" )"1" "1" expand "member" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "member" )"2" expand "singleton" )"2" expand "remove" )"2" expand "member" )"2" "2" "2" "2" "v!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "hh" "({y: T | v!2 /= y AND member(y, vert(G!1))})" )"2" replace "2" "1" expand "remove" )"1" expand "member" )"1" expand "singleton" )"1" "1" replace "1" "1" assert )"1" "1" "u!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "remove" )"2" expand "member" )"2" expand "singleton" )"2" "2" replace "2" assert )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "hh" "({y: T | v!2 /= y AND member(y, vert(G!1))})" )"2" replace "2" "2" expand "singleton" )"2" expand "remove" )"2" expand "member" )"2" replace "2" assert )"2" "2" "u!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "singleton" "2" nil nil ))nil ))nil ))nil ))nil )"2" "bb" "({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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 ))nil ))nil )"2" (skosimp*)"2" (expand "tree?" -2)"2" (bddsimp)"2" (copy -3)"2" (expand "size" -1)"2" (typepred "j!1" )"2" (skosimp*)"2" (case "v!1=v!2" )"1" (replace -1 -5 rl)"1" (hide-all-but -5 -)"1" (assert ) nil nil )) nil ))nil )"2" (inst -3 "del_vert[T](G!1, v!2)" "v!1" )"2" (bddsimp)"1" (expand "deg" -4)"1" "finite_sets[doubleton[T]].nonempty_card" )"1" "incident_edges(v!1, del_vert[T](G!1, v!2))" )"1" "1" "1" expand "nonempty?" -2)"1" expand "empty?" 1)"1" "1" expand "member" -2)"1" expand "deg" 3)"1" "incident_edges(v!1, G!1)" )"1" "1" expand "nonempty?" "1" expand "empty?" "1" "x!1" )"1" expand "member" "1" "1" expand "incident_edges" "1" expand "del_vert" "1" assert )"1" "1" "1" 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 )"2" (lemma "finite_sets[T].card_one" )"2" (inst -1 "vert(del_vert[T](G!1, v!2))" )"2" (bddsimp)"2" "2" "2" "2" expand "del_vert" -1)"2" "2" expand "deg" -2)"2" "finite_sets[doubleton[T]].card_one" )"2" "incident_edges(v!2, G!1)" )"2" "2" "2" "2" expand "incident_edges" "2" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})(x!2) = ") "1" "1" case "({y: T | v!2 /= y AND vert(G!1)(y)})(x!1) = singleton(x!1)(x!1)" )"1" case "({y: T | v!2 /= y AND vert(G!1)(y)})(v!1) = singleton(x!1)(v!1)" )"1" case "({y: T | v!2 /= y AND vert(G!1)(y)})(v!2) = singleton(x!1)(v!2)" )"1" "1" "1" "1" "1" assert "1" expand "singleton" "1" "1" "1" "other_vert" )"1" "G!1" "x!2" "v!2" )"1" "1" "1" "1" case "({y: T | v!2 /= y AND vert(G!1)(y)})(u!1) = singleton(x!1)(u!1)" )"1" "1" "1" expand "singleton" "1" "1" "1" replace "1" replace "1" "1" expand "deg" "1" "finite_sets[doubleton[T]].nonempty_card" )"1" "incident_edges(v!1, G!1)" )"1" "1" "1" expand "nonempty?" "1" expand "empty?" )"1" "x!2" )"1" expand "member" )"1" expand "incident_edges" "1" assert )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "jj" "({y: T | v!2 /= y AND vert(G!1)(y)})" )"2" replace "2" "1" expand "remove" )"1" expand "member" )"1" expand "singleton" )"1" replace "1" assert )"1" "1" "u!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "remove" )"2" expand "member" )"2" expand "singleton" )"2" "2" "u!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "jj" "({y: T | v!2 /= y AND vert(G!1)(y)})" )"2" replace "2" "1" expand "remove" )"1" expand "member" )"1" expand "singleton" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "remove" )"2" expand "member" )"2" expand "singleton" )"2" assert )"2" "2" "v!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "jj" "({y: T | v!2 /= y AND vert(G!1)(y)})" )"2" replace "2" "1" expand "remove" )"1" expand "member" )"1" expand "singleton" )"1" replace "1" assert )"1" "1" "v!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "remove" )"2" expand "member" )"2" expand "singleton" )"2" replace "2" assert )"2" "2" "v!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "jj" "({y: T | v!2 /= y AND vert(G!1)(y)})" )"2" replace "2" "2" expand "singleton" )"2" expand "remove" )"2" expand "member" )"2" replace "2" assert )"2" "2" assert )"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cc" "({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -2 -3 -5 3 4)"3" (grind) nil nil )) nil )"4" (lemma "size_del_vert" )"4" (inst -1 "G!1" "v!2" )"4" (replace -6 -1)"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"graph[T]" graph_ops nil )NOT const-decl "[bool -> bool]" booleans nil )"finite_set" finite_sets nil )"set" sets nil )"finite_set[doubleton[T]]" graph_degnil )"bool" sets nil )"non_empty_finite_set" finite_sets nil )nil finite_sets nil )"bool" sets nil )"bool" sets nil )nil application-judgement "finite_set[T]" trees nil )nil graphs nil )"(singleton?)" sets nil )"bool" sets nil )nil finite_sets nil )"odd_int" integersnil )"posint" nil )"even_int" integersnil )nil graph_ops nil )nil naturalnumbers nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" finite_sets nil )"nat" graph_deg nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" graphs nil )"bool" trees nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (T formal-type-decl nil trees nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3262616780"" (lemma "tree_edge_k" )"" (lemma "tree_edge" )"" (assert ) (("" (bddsimp) nil nil )) nil )) nil ))nil )nil trees nil )nil trees nil ))nil ))nil 3312289508"" (skosimp*)"" (inst? -1)"" (inst -1 "size(G!1) -1" )"1" (assert ) nil nil )"2" (lemma "tree_nonempty" )"2" (inst? -1)"2" (bddsimp)"2" (expand "empty?" )"2" (expand "size" 2)"2" (assert 2)"2" (lemma "finite_sets[T].nonempty_card" )"2" (inst -1 "vert(G!1)" )"2" (bddsimp)"1" (assert ) nil nil )"2" (hide -1 -2 -3 2 4 5)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trees nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil trees nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" finite_sets nil )"bool" graphs nil )"int" integers nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" graphs nil )"graph[T]" trees nil )"int" integers nil )"(total_order?[real])" nil ))nil )nil 3262616780"" (skosimp*)"" (inst? -1)"" (inst -1 "size(G!1) -1" )"1" (assert ) nil nil )"2" (lemma "tree_nonempty" )"2" (inst? -1)"2" (bddsimp)"2" (expand "empty?" )"2" (expand "size[T]" 2)"2" (assert 2)"2" (lemma "finite_sets[T].nonempty_card" )"2" (inst -1 "vert(G!1)" )"2" (bddsimp)"1" (assert ) nil nil )"2" (hide -1 -2 -3 2 4 5)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )nil graphs nil )"bool" graphs nil )"nat" graphs nil ))nil ))nil 3312294681"" (induct "k" 1 "nat_induction" )"1" (skosimp*)"1" (name "H!1" "del_vert(G!1,v!1)" )"1" (assert -3)"1" (copy 1)"1" (replace -1 1)"1" (expand "tree?" -2)"1" (bddsimp)"1" (hide -3)"1" (lemma "finite_sets[T].card_one" )"1" (inst -1 "vert(G!1)" )"1" (bddsimp)"1" (expand "deg" -5)"1" (reveal -1)"1" "finite_sets[doubleton[T]].card_one" )"1" "1" "incident_edges(v!1,G!1)" )"1" "1" "1" "1" "x!1" )"1" "1" case "x!1(x!2)" )"1" "1" "1" expand "singleton" "1" expand "dbl" "1" case "vert(G!1)(y!1)" )"1" nil nil )"2" case "edges(G!1)(x!1)" )"1" "G!1" )"1" "x!1" )"1" "1" "x!3" )"1" "y!1" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" expand "incident_edges" "2" expand "dbl" "2" replace "2" "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!1)" )"1" nil nil )"2" "2" "1" expand "singleton" "1" "functions[doubleton[T],bool].extensionality_postulate" )"1" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" "({y: doubleton[T] | y = x!1})" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "functions[doubleton[T],bool].extensionality_postulate" )"2" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" "({y: doubleton[T] | y = x!1})" )"2" "1" "x!1" )"1" assert )nil nil ))nil )"2" assert )"2" "2" expand "singleton" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "vert(G!1)(x!3)" )"1" nil nil )"2" replace "2" expand "incident_edges" "2" case "singleton(x!1)(x!1)" )"1" replace "1" case "edges(G!1)(x!1)" )"1" "G!1" )"1" "x!1" )"1" "1" case "x!1(x!3)" )"1" "x!3" )"1" assert )nil nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "graphs" )"2" assert )"2" expand "incident_edges" "2" expand "singleton" "2" expand "singleton" "2" replace "2" "2" replace "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(x!2)})(x!1) = ({y: doubleton[T] | y = x!1})(x!1)" )"1" assert nil nil )"2" "2" 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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "finite_sets[T].card_one" )"2" (inst -1 "vert(G!1)" )"2" (bddsimp)"1" (hide -4)"1" (skosimp*)"1" (hide -4)"1" expand "deg" -5)"1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!1,G!1)" )"1" "1" "1" "1" "x!2" )"1" "1" case "x!2(x!1)" )"1" expand "incident_edges" "1" case "singleton(x!2)(x!2)" )"1" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) = singleton(x!2)(x!2)" )"1" "1" "G!1" )"1" "x!2" )"1" "1" "1" "x!3" )"1" "y!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ff" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "incident_edges" "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) = singleton(x!2)(x!2)" )"1" "1" "G!1" )"1" "x!2" )"1" "1" "x!3" )"1" "y!1" )"1" case "x!2(y!1) AND x!2(x!3)" )"1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil )"2" "2" "ff" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "size" -3)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (copy 1)"2" (name "H!1" "del_vert(G!1, v!1)" )"2" (replace -1 1)"2" (expand "tree?" -3)"2" (expand "size" -4)"2" (typepred "j!1" )"2" (case "NOT card[T](vert(G!1)) = 1" )"1" (bddsimp)"1" (skosimp*)"1" (name "W!1" "del_vert[T](G!1, v!2)" )"1" (copy -6)"1" (replace -2 -1)"1" "1" "del_vert_comm" )"1" "G!1" "v!1" "v!2" )"1" replace -3 -1)"1" replace -4 -1)"1" "size_del_vert" )"1" "G!1" "v!1" )"1" "G!1" "v!2" )"1" "H!1" "v!2" )"1" "W!1" "v!1" )"1" replace -8 -4)"1" replace -9 -5)"1" "U!1" "del_vert(W!1, v!1)" )"1" "1" "W!1" "v!1" )"1" case "v!1=v!2" )"1" replace "1" replace "1" replace "1" nil nil ))nil ))nil ))nil )"2" case "size(G!1) = j!1+2" )"1" case "vert(W!1)(v!1) AND deg(v!1,W!1)=1" )"1" replace "1" assert "1" "1" "1" case "tree?(W!1) AND vert(W!1)(v!1) AND deg(v!1, W!1) = 1" )"1" "1" case "tree?(del_vert(W!1, v!1))" )"1" replace "1" replace "1" case "deg(v!2,H!1)=1" )"1" expand "tree?" "1" "1" "v!2" )"1" replace "1" assert )nil nil ))nil )"2" "2" expand "del_vert" "2" "2" "2" case "remove[T](v!1, vert(G!1))=vert(H!1)" )"1" case "remove[T](v!1, vert(G!1))(v!2)=vert(H!1)(v!2)" )"1" "1" expand "remove" "1" expand "member" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "gg" "remove[T](v!1, vert(G!1))" )"2" replace "2" replace "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "del_vert" "2" case "remove[T](v!1, vert(G!1))=vert(H!1)" )"1" "1" case "remove[T](v!1, vert(G!1))(v!2)=vert(H!1)(v!2)" )"1" "1" expand "remove" "1" "1" "1" expand "deg" "1" expand "deg" "1" expand "member" "1" "1" expand "del_vert" "1" "finite_sets[T].card_one" )"1" "1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!2, G!1)" )"1" "incident_edges(v!2, H!1)" )"1" "1" "1" "1" "x!1" )"1" expand "incident_edges" )"1" case "j!1>0" )"1" case "edges(H!1)=({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)})" )"1" "1" "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})(x!2) ") "1" "1" assert )"1" replace "1" "1" "1" replace "1" "1" "1" "1" expand "deg" "1" "1" "incident_edges(v!1, W!1)" )"1" "1" "1" expand "incident_edges" "1" "1" expand "del_vert" "1" case "edges(W!1)=({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!2)})" )"1" replace "1" "1" case " ({e: doubleton[T] | (edges(G!1)(e) AND NOT e(v!2)) AND e(v!1)})(x!3) = singleton(x!3)(x!3)" )"1" "1" "1" case "singleton(x!3)(x!3)" )"1" "1" "1" expand "deg" "1" "1" "incident_edges(v!1, G!1)" )"1" "1" "1" expand "incident_edges" "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) ") "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!3) ") "1" "1" "1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "ww" "({e: doubleton[T] | (edges(G!1)(e) AND NOT e(v!2)) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mm" "({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" "j!1" )"2" case "j!1=0" )"1" replace "1" replace "1" assert "1" expand "size" "1" "1" expand "tree?" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "kk" "remove[T](v!1, vert(G!1))" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "j!1>0" )"1" "1" expand "del_vert" "1" case "vert(W!1)=remove[T](v!2, vert(G!1))" )"1" case "edges(W!1)=({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!2)})" )"1" expand "remove" "1" case "vert(W!1)(v!1) = ({y: T | v!2 /= y AND member(y, vert(G!1))})(v!1)" )"1" "1" expand "member" "1" "1" "1" expand "deg" "1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!1, W!1)" )"1" "1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!1, G!1)" )"1" expand "deg" "1" "1" "1" "x!1" )"1" "1" expand "incident_edges" )"1" "tree_edge_all" )"1" "1" "W!1" "v!1" )"1" "1" "1" expand "deg" "1" "finite_sets[doubleton[T]].nonempty_card" )"1" "incident_edges(v!1, W!1)" )"1" "1" expand "nonempty?" "1" expand "empty?" "1" "1" expand "member" )"1" expand "incident_edges" "1" "1" "1" "1" replace "1" "1" "1" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!1) ") "1" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) ") "1" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!3) ") "1" "1" "1" "1" "1" "1" "1" "1" "1" "1" "1" case "edges(W!1)(x!1) = ({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!2)})(x!1)" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil )"4" "4" "4" nil nil ))nil ))nil )"5" nil nil )"6" nil nil )"7" "7" "7" case "edges(W!1)(x!2) = ({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!2)})(x!2)" )"1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"8" nil nil )"9" replace "9" "9" nil nil ))nil ))nil )"10" nil nil )"11" nil nil )"12" nil nil )"13" "13" nil nil ))nil )"14" nil nil )"15" "15" "15" "15" assert )nil nil ))nil ))nil ))nil )"16" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "2" assert "2" expand "size" "2" "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 )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "jj" "({y: T | v!2 /= y AND member(y, vert(G!1))})" )"2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "j!1" )"2" case "j!1=0" )"1" replace "1" replace "1" assert "1" expand "size" "1" expand "tree?" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "size" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v!1=v!2" )"1" replace "1" replace -7 -8)"1" replace "1" nil nil ))nil ))nil ))nil )"2" "2" expand "del_vert" "2" "2" "2" "2" case "remove[T](v!2,vert(G!1))=vert(W!1)" )"1" "1" case " remove[T](v!2, vert(G!1))(v!1) = vert(W!1)(v!1)" )"1" "1" expand "remove" "1" expand "member" "1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v!1=v!2" )"1" replace -1 -6 rl)"1" replace -6 -7)"1" replace -7 -5)"1" nil nil ))nil ))nil ))nil )"2" "2" expand "del_vert" "2" "2" "2" "2" case "remove[T](v!1,vert(G!1))=vert(H!1)" )"1" case " remove[T](v!1, vert(G!1))(v!2) = vert(H!1)(v!2)" )"1" "1" expand "remove" "1" expand "member" "1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 -6 -8) -)"2" (typepred "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_ops nil )nil graph_ops nil )"graph[T]" trees nil )"int" integers nil )"posint" nil )"finite_set" finite_sets nil )"set" sets nil )"bool" sets nil )"(total_order?[real])" nil )"even_int" integersnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil trees nil )nil finite_sets nil )"bool" sets nil )"bool" sets nil )"(vert(G!1))" trees nil )"graph[T]" trees nil )"T" trees nil )"graph[T]" trees nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"odd_int" integers nil )"posint" nil )nil finite_sets nil )"bool" sets nil )"(singleton?)" sets nil )nil functions nil )"non_empty_finite_set" finite_sets nil )nil application-judgement "finite_set[T]" trees nil )NOT const-decl "[bool -> bool]" booleans nil )"finite_set[doubleton[T]]" graph_degnil )"bool" finite_sets nil )nil naturalnumbers nil )"graph[T]" graph_ops nil )"nat" graph_deg nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" graphs nil )"bool" trees nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil ) (T formal-type-decl nil trees nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3312294198"" (induct "k" 1 "nat_induction" )"1" (skosimp*)"1" (name "H!1" "del_vert(G!1,v!1)" )"1" (assert -3)"1" (copy 1)"1" (replace -1 1)"1" (expand "tree?" -2)"1" (bddsimp)"1" (hide -3)"1" (lemma "finite_sets[T].card_one" )"1" (inst -1 "vert(G!1)" )"1" (bddsimp)"1" (expand "deg" -5)"1" (reveal -1)"1" "finite_sets[doubleton[T]].card_one" )"1" "1" "incident_edges(v!1,G!1)" )"1" "1" "1" "1" "x!1" )"1" "1" case "x!1(x!2)" )"1" "1" "1" expand "singleton" "1" expand "dbl" "1" case "vert(G!1)(y!1)" )"1" nil )"2" case "edges(G!1)(x!1)" )"1" "G!1" )"1" "x!1" )"1" "1" "x!3" )"1" "y!1" )"1" assert )"1" "1" "1" nil )))))))))))"2" nil )))))))"2" expand "incident_edges" "2" expand "dbl" "2" replace "2" "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!1)" )"1" nil )"2" "2" "1" expand "singleton" "1" "functions[doubleton[T],bool].extensionality_postulate" )"1" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" "({y: doubleton[T] | y = x!1})" )"1" "1" "x!1" )"1" assert )nil )))))))))))"2" "functions[doubleton[T],bool].extensionality_postulate" )"2" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" "({y: doubleton[T] | y = x!1})" )"2" "1" "x!1" )"1" assert )nil )))"2" assert )"2" "2" expand "singleton" "2" nil )))))))))))))))))))))))))))))))))))"2" case "vert(G!1)(x!3)" )"1" nil )"2" replace "2" expand "incident_edges" "2" case "singleton(x!1)(x!1)" )"1" replace "1" case "edges(G!1)(x!1)" )"1" "G!1" )"1" "x!1" )"1" "1" case "x!1(x!3)" )"1" "x!3" )"1" assert )nil )))"2" assert )"2" "2" nil )))))))"2" nil )))))))"2" "2" nil )))))))"2" nil )))))))))))))"2" "2" "graphs" )"2" assert )"2" expand "incident_edges" "2" expand "singleton" "2" expand "singleton" "2" replace "2" "2" replace "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(x!2)})(x!1) = ({y: doubleton[T] | y = x!1})(x!1)" )"1" assert nil )"2" "2" nil )))))))))))))))))))))))))))))))))"2" nil )))))))))))))))))))))"2" (lemma "finite_sets[T].card_one" )"2" (inst -1 "vert(G!1)" )"2" (bddsimp)"1" (hide -4)"1" (skosimp*)"1" (hide -4)"1" expand "deg" -5)"1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!1,G!1)" )"1" "1" "1" "1" "x!2" )"1" "1" case "x!2(x!1)" )"1" expand "incident_edges" "1" case "singleton(x!2)(x!2)" )"1" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) = singleton(x!2)(x!2)" )"1" "1" "G!1" )"1" "x!2" )"1" "1" "1" "x!3" )"1" "y!1" )"1" nil )))))))))))))))"2" "2" "2" "ff" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" "2" nil )))))))))))))))"2" "2" "2" nil )))))))))"2" "2" expand "incident_edges" "2" case "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) = singleton(x!2)(x!2)" )"1" "1" "G!1" )"1" "x!2" )"1" "1" "x!3" )"1" "y!1" )"1" case "x!2(y!1) AND x!2(x!3)" )"1" "1" "1" nil )))))"2" "2" nil )))))))))"2" nil )"3" nil )))))))))"2" "2" "ff" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" "2" nil )))))))))))))))))))))))))))"2" (propax) nil )))))))))))))))"2" (expand "size" -3)"2" (propax) nil )))))))))))))))))))))))"2" (skosimp*)"2" (copy 1)"2" (name "H!1" "del_vert(G!1, v!1)" )"2" (replace -1 1)"2" (expand "tree?" -3)"2" (expand "size" -4)"2" (typepred "j!1" )"2" (case "NOT card[T](vert(G!1)) = 1" )"1" (bddsimp)"1" (skosimp*)"1" (name "W!1" "del_vert[T](G!1, v!2)" )"1" (copy -6)"1" (replace -2 -1)"1" "1" "del_vert_comm" )"1" "G!1" "v!1" "v!2" )"1" replace -3 -1)"1" replace -4 -1)"1" "size_del_vert" )"1" "G!1" "v!1" )"1" "G!1" "v!2" )"1" "H!1" "v!2" )"1" "W!1" "v!1" )"1" replace -8 -4)"1" replace -9 -5)"1" "U!1" "del_vert(W!1, v!1)" )"1" "1" "W!1" "v!1" )"1" case "v!1=v!2" )"1" replace "1" replace "1" replace "1" nil )))))))"2" case "size(G!1) = j!1+2" )"1" case "vert(W!1)(v!1) AND deg(v!1,W!1)=1" )"1" replace "1" assert "1" "1" "1" case "tree?(W!1) AND vert(W!1)(v!1) AND deg(v!1, W!1) = 1" )"1" "1" case "tree?(del_vert(W!1, v!1))" )"1" replace "1" replace "1" case "deg(v!2,H!1)=1" )"1" expand "tree?" "1" "1" "v!2" )"1" replace "1" assert )nil )))"2" "2" expand "del_vert" "2" "2" "2" case "remove[T](v!1, vert(G!1))=vert(H!1)" )"1" case "remove[T](v!1, vert(G!1))(v!2)=vert(H!1)(v!2)" )"1" "1" expand "remove" "1" expand "member" "1" assert )"1" "1" assert )nil )))))))))))"2" "2" "2" "gg" "remove[T](v!1, vert(G!1))" )"2" replace "2" replace "2" "2" assert )nil )))))))))))))))"2" "2" "2" nil )))))))))))))))))))))"2" "2" expand "del_vert" "2" case "remove[T](v!1, vert(G!1))=vert(H!1)" )"1" "1" case "remove[T](v!1, vert(G!1))(v!2)=vert(H!1)(v!2)" )"1" "1" expand "remove[T]" "1" "1" "1" expand "deg" "1" expand "deg" "1" expand "member" "1" "1" expand "del_vert" "1" "finite_sets[T].card_one" )"1" "1" "finite_sets[doubleton[T]].card_one" )"1" "incident_edges(v!2, G!1)" )"1" "incident_edges(v!2, H!1)" )"1" "1" "1" "1" "x!1" )"1" expand "incident_edges" )"1" case "j!1>0" )"1" case "edges(H!1)=({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)})" )"1" "1" "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})(x!2) ") "1" "1" assert )"1" replace "1" "1" "1" replace "1" "1" "1" "1" expand "deg" "1" "1" "incident_edges(v!1, W!1)" )"1" "1" "1" expand "incident_edges" "1" "1" expand "del_vert" "1" case "edges(W!1)=({e: doubleton[T] | edges(G!1)(e) AND NOT e(v!2)})" )"1" replace "1" "1" case " ({e: doubleton[T] | (edges(G!1)(e) AND NOT e(v!2)) AND e(v!1)})(x!3) = singleton(x!3)(x!3)" )"1" "1" "1" case "singleton(x!3)(x!3)" )"1" "1" "1" expand "deg" "1" "1" "incident_edges(v!1, G!1)" )"1" "1" "1" expand "incident_edges" "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!2) ") "1" case " ({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})(x!3) ") "1" "1" "1" "1" "1" "1" "1" "1" nil )))))))))))))))"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil )))))))))))"2" "2" "kkk" "({e: doubleton[T] | edges(G!1)(e) AND e(v!1)})" )"2" replace "2" replace "2" nil )))))))))))))))))))))))))))"2" "2" nil )))))))))"2" "2" "ww" "({e: doubleton[T] | (edges(G!1)(e) AND NOT e(v!2)) AND e(v!1)})" )"2" replace "2" replace "2" nil )))))))))))))))"2" "2" nil )))))))))))))))))))))))))))))))))))))))"2" "2" "mm" "({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})" )"2" replace "2" replace "2" nil )))))))))))))))"2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.735Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
