|
(graph_deg
(incident_edges_TCC1 0
(incident_edges_TCC1-1 nil 3507100590
("" (skosimp*)
(("" (lemma "finite_subset[doubleton[T]]")
(("" (inst?)
(("" (inst -1 "edges(G!1)")
(("" (assert) (("" (hide 2) (("" (grind) nil))))))))))))
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_deg nil)
(finite_subset formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas 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))
nil))
(incident_edges_subset 0
(incident_edges_subset-1 nil 3507100590 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil graph_deg 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(incident_edges_emptyset 0
(incident_edges_emptyset-1 nil 3507100590
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (expand "emptyset")
(("" (expand "incident_edges") (("" (ground) nil))))))))
nil)
((T formal-type-decl nil graph_deg 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)
(emptyset const-decl "set" sets nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(is_finite const-decl "bool" finite_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)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(deg_del_edge 0
(deg_del_edge-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
((""
(case-replace "incident_edges(y!1, del_edge(G!1,e!1)) =
remove(e!1,incident_edges(y!1, G!1))")
(("1" (rewrite "card_remove[doubleton[T]]")
(("1" (lift-if)
(("1" (ground)
(("1" (hide -1 2)
(("1" (hide -2) (("1" (grind) nil)))))))))))
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (iff 1)
(("2" (prop)
(("1" (expand "incident_edges")
(("1" (ground)
(("1" (expand "remove")
(("1" (expand "member")
(("1" (ground)
(("1" (replace -1)
(("1" (hide -1)
(("1"
(lemma "del_edge_lem[T]")
(("1"
(inst?)
(("1"
(expand "member")
(("1" (propax) nil)))))))))))
("2" (lemma "del_edge_lem2[T]")
(("2" (inst?)
(("2" (assert) nil)))))))))))))))
("2" (expand "incident_edges")
(("2" (expand "remove")
(("2" (flatten)
(("2" (expand "member")
(("2" (ground)
(("2" (rewrite "del_edge_lem3")
nil))))))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(del_edge_lem3 formula-decl nil graph_ops nil)
(del_edge_lem formula-decl nil graph_ops nil)
(del_edge_lem2 formula-decl nil graph_ops nil)
(member const-decl "bool" sets nil)
(card_remove formula-decl nil finite_sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "finite_set[T]" graph_deg nil)
(remove const-decl "set" sets nil)
(del_edge const-decl "graph[T]" graph_ops nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(is_finite const-decl "bool" finite_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)
(T formal-type-decl nil graph_deg nil)
(finite_remove application-judgement "finite_set" finite_sets nil))
nil))
(deg_del_edge2 0
(deg_del_edge2-1 nil 3507100590
("" (skosimp*)
(("" (lemma "deg_del_edge")
(("" (inst?)
(("" (typepred "e!1")
(("" (skosimp*)
(("" (case "x!1=y!1")
(("1" (replace -1)
(("1" (hide -1)
(("1" (inst -2 "y!2")
(("1" (split -2)
(("1" (propax) nil)
("2" (replace -1)
(("2" (hide -1)
(("2" (hide -1 -2 3)
(("2" (expand "dbl")
(("2"
(apply-extensionality :hide? t)
(("2"
(iff 1)
(("2" (ground) nil)))))))))))))
("3" (propax) nil)))))))))
("2" (case "y!2 = y!1")
(("1" (replace -1)
(("1" (hide -1)
(("1" (inst -2 "x!1") (("1" (assert) nil)))))))
("2" (hide -2 -4 4)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "dbl")
(("2" (ground) nil))))))))))))))))))))))
nil)
((deg_del_edge formula-decl nil graph_deg nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nil application-judgement "finite_set[T]" graph_deg nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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_deg nil))
nil))
(deg_del_edge3 0
(deg_del_edge3-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
((""
(case "incident_edges(y!1, G!1) = incident_edges(y!1, del_edge(G!1, e!1))")
(("1" (assert) nil)
("2" (hide 3)
(("2" (apply-extensionality 1 :hide? t)
(("2" (expand "incident_edges")
(("2" (iff 1)
(("2" (ground)
(("1" (lemma "del_edge_lem3[T]")
(("1" (inst?) (("1" (assert) nil)))))
("2" (lemma "del_edge_lem2[T]")
(("2" (inst?)
(("2" (assert) nil))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(del_edge_lem3 formula-decl nil graph_ops nil)
(del_edge_lem2 formula-decl nil graph_ops nil)
(T formal-type-decl nil graph_deg 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)
(is_finite const-decl "bool" finite_sets nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(del_edge const-decl "graph[T]" graph_ops nil))
nil))
(deg_del_edge_ge 0
(deg_del_edge_ge-1 nil 3507100590
("" (skosimp*)
(("" (case "e!1(y!1)")
(("1" (lemma "deg_del_edge2")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "del_edge_lem5[T]")
(("1" (inst?) (("1" (assert) nil)))))))))))
("2" (lemma "deg_del_edge3")
(("2" (inst?) (("2" (assert) nil))))))))
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_deg nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(del_edge_lem5 formula-decl nil graph_ops nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(deg_del_edge2 formula-decl nil graph_deg nil)
(deg_del_edge3 formula-decl nil graph_deg nil))
nil))
(deg_del_edge_le 0
(deg_del_edge_le-1 nil 3507100590
("" (skosimp*)
(("" (case "e!1(y!1)")
(("1" (lemma "deg_del_edge2")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "del_edge_lem5[T]")
(("1" (inst?) (("1" (assert) nil)))))))))))
("2" (lemma "deg_del_edge3")
(("2" (inst?) (("2" (assert) nil))))))))
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_deg nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(del_edge_lem5 formula-decl nil graph_ops nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(deg_del_edge2 formula-decl nil graph_deg nil)
(deg_del_edge3 formula-decl nil graph_deg nil))
nil))
(deg_edge_exists 0
(deg_edge_exists-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
(("" (rewrite "nonempty_card[doubleton[T]]" :dir rl)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "incident_edges")
(("" (skosimp*)
(("" (expand "member")
(("" (inst?)
(("" (flatten)
(("" (assert) nil))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" 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_deg nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
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)
(is_finite const-decl "bool" finite_sets nil)
(nonempty_card formula-decl nil finite_sets nil))
nil))
(deg_to_card 0
(deg_to_card-1 nil 3507100590
("" (skosimp*)
(("" (lemma "deg_edge_exists")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (hide -1 -3)
(("" (typepred "G!1")
(("" (inst?)
(("" (assert)
(("" (typepred "e!1")
(("" (skosimp*)
(("" (inst-cp -2 "x!1")
(("" (inst -2 "y!1")
(("" (replace -1)
((""
(hide -1)
((""
(hide -3)
((""
(expand "dbl")
((""
(expand "size")
((""
(case
"subset?(add[T](x!1,singleton(y!1)),vert(G!1))")
(("1"
(lemma "card_subset[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide -2)
(("1"
(lemma "card_add[T]")
(("1"
(inst?)
(("1"
(lemma
"card_singleton[T]")
(("1"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"singleton")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(assert)
nil)))))))))))))))))))))))
("2"
(rewrite "finite_add[T]")
nil)))))
("2"
(hide 3)
(("2"
(grind)
nil))))))))))))))))))))))))))))))))))))))))
nil)
((deg_edge_exists formula-decl nil graph_deg nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(size const-decl "nat" graphs nil)
(member const-decl "bool" sets nil)
(card_subset formula-decl nil finite_sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(card_add formula-decl nil finite_sets nil)
(card_singleton formula-decl nil finite_sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(is_finite const-decl "bool" finite_sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(nonempty_add_finite application-judgement "non_empty_finite_set"
finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans 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_deg nil))
nil))
(del_vert_deg_0 0
(del_vert_deg_0-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
(("" (lemma "card_empty?[doubleton[T]]")
(("" (inst?)
(("" (iff)
(("" (assert)
(("" (hide -2)
(("" (expand "incident_edges")
(("" (expand "empty?")
(("" (expand "member")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "del_vert")
(("" (inst?)
(("" (iff 1)
((""
(ground)
nil))))))))))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(is_finite const-decl "bool" finite_sets 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)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(member const-decl "bool" sets nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(empty? const-decl "bool" sets nil)
(card_empty? formula-decl nil finite_sets nil)
(T formal-type-decl nil graph_deg 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))
nil))
(deg_del_vert_TCC1 0
(deg_del_vert_TCC1-1 nil 3507100590 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil graph_deg nil)
(/= const-decl "boolean" notequal nil))
nil))
(deg_del_vert 0
(deg_del_vert-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
((""
(case-replace "incident_edges(v!1, del_vert(G!1, x!1)) =
incident_edges(v!1, del_edge(G!1,dbl[T](x!1,v!1)))")
(("1" (hide -1)
(("1" (lemma "deg_del_edge")
(("1" (inst?)
(("1" (inst -1 "x!1" "v!1")
(("1" (prop)
(("1" (expand "deg") (("1" (assert) nil)))))))
("2" (inst?) (("2" (assert) nil)))))))))
("2" (hide 3)
(("2" (apply-extensionality 1 :hide? t)
(("1" (expand "incident_edges")
(("1" (grind)
(("1" (hide -3)
(("1" (replace -2 * rl) (("1" (grind) nil)))))
("2" (hide -1 -4)
(("2" (lemma "edge_has_2_verts[T]")
(("2" (inst?)
(("2" (inst?) (("2" (assert) nil)))))))))))))
("2" (inst?) (("2" (assert) nil)))))))
("3" (inst?) (("3" (assert) nil))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(edge_has_2_verts formula-decl nil graphs nil)
(finite_remove application-judgement "finite_set" finite_sets nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(deg_del_edge formula-decl nil graph_deg nil)
(del_edge const-decl "graph[T]" graph_ops nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(is_finite const-decl "bool" finite_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)
(T formal-type-decl nil graph_deg nil)
(nil application-judgement "finite_set[T]" graph_deg nil))
nil))
(del_vert_not_incident 0
(del_vert_not_incident-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
((""
(case-replace
"incident_edges(x!1, G!1) = incident_edges(x!1, del_vert(G!1, v!1))")
(("" (hide 4)
(("" (apply-extensionality 1 :hide? t)
(("" (expand "incident_edges")
(("" (iff 1)
(("" (prop)
(("1" (lemma "edge_in_del_vert")
(("1" (inst?)
(("1" (assert)
(("1" (lemma "edge_has_2_verts")
(("1" (inst?)
(("1" (inst?)
(("1" (assert) nil)))))))))))))
("2" (expand "del_vert")
(("2" (flatten)
(("2" (propax) nil))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(edge_has_2_verts formula-decl nil graphs nil)
(edge_in_del_vert formula-decl nil graph_ops nil)
(nil application-judgement "finite_set[T]" graph_deg nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(is_finite const-decl "bool" finite_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)
(T formal-type-decl nil graph_deg nil))
nil))
(singleton_deg 0
(singleton_deg-1 nil 3507100590
("" (skosimp*)
(("" (expand "singleton?")
(("" (expand "deg")
(("" (rewrite "card_is_0[doubleton[T]]")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "incident_edges")
(("" (expand "emptyset")
(("" (flatten)
(("" (lemma "edge_in_card_gt_1[T]")
(("" (inst?)
(("" (split -1)
(("1" (assert)
(("1" (expand "size") (("1" (assert) nil)))))
("2" (propax) nil))))))))))))))))))))))
nil)
((singleton? const-decl "bool" graphs nil)
(card_is_0 formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets 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)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(T formal-type-decl nil graph_deg 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_emptyset name-judgement "finite_set" finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(size const-decl "nat" graphs nil)
(edge_in_card_gt_1 formula-decl nil graphs nil)
(emptyset const-decl "set" sets nil)
(deg const-decl "nat" graph_deg nil))
nil))
(deg_1_sing 0
(deg_1_sing-1 nil 3507100590
("" (skosimp*)
(("" (expand "deg")
(("" (lemma "card_one[Dbl]")
(("" (inst?)
(("" (flatten)
(("" (assert)
(("" (hide -2)
(("" (skosimp*)
(("" (inst?)
(("" (assert)
((""
(case-replace
"incident_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)")
(("1" (hide -2)
(("1" (expand "incident_edges")
(("1" (expand "singleton")
(("1"
(flatten)
(("1" (assert) nil)))))))))
("2" (assert) nil))))))))))))))))))))))
nil)
((deg const-decl "nat" graph_deg nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(pregraph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(graph type-eq-decl nil graphs nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(card_one formula-decl nil finite_sets nil)
(T formal-type-decl nil graph_deg 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)
(Dbl type-eq-decl nil doubletons nil))
nil)))
¤ Dauer der Verarbeitung: 0.983 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.
|
