| products/sources/formale Sprachen/PVS/digraphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: digraph_deg.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(digraph_deg
(incoming_edges_TCC1 0 (incoming_edges_TCC1-1 nil 3298281553 ("" (skosimp*) (("" (lemma "finite_subset[edgetype[T]]") (("" (inst?) (("" (inst -1 "edges(G!1)") (("" (assert) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_subset formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets 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)) shostak)) (outgoing_edges_TCC1 0 (outgoing_edges_TCC1-1 nil 3298281553 ("" (skosimp*) (("" (lemma "finite_subset[edgetype[T]]") (("" (inst?) (("" (inst -1 "edges(G!1)") (("" (assert) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_subset formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (= const-decl "[T, T -> boolean]" equalities nil) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets 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)) shostak)) (incident_edges_TCC1 0 (incident_edges_TCC1-1 nil 3298819375 ("" (skosimp*) (("" (lemma "finite_subset[edgetype[T]]") (("" (inst?) (("" (inst -1 "edges(G!1)") (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_subset formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets 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) (in? const-decl "bool" pairs nil) (pair type-eq-decl nil pairs nil) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets 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)) shostak)) (incoming_edges_subset 0 (incoming_edges_subset-1 nil 3298476069 ("" (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 digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (outgoing_edges_subset 0 (outgoing_edges_subset-1 nil 3298476076 ("" (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 digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (incident_edges_subset 0 (incident_edges_subset-1 nil 3298734919 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (in? const-decl "bool" pairs nil) (incident_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (incoming_edges_emptyset 0 (incoming_edges_emptyset-1 nil 3298476249 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "emptyset") (("" (expand "incoming_edges") (("" (flatten) (("" (replace -3) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (emptyset const-decl "set" sets nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (outgoing_edges_emptyset 0 (outgoing_edges_emptyset-1 nil 3298476557 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "emptyset") (("" (expand "outgoing_edges") (("" (flatten) (("" (replace -3) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (emptyset const-decl "set" sets nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (incident_edges_emptyset 0 (incident_edges_emptyset-1 nil 3298734972 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "emptyset") (("" (expand "incident_edges") (("" (flatten) (("" (replace -3) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (emptyset const-decl "set" sets nil) (incident_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (deg_del_edge_incoming 0 (deg_del_edge_incoming-1 nil 3298474440 ("" (skosimp*) (("" (expand "in_deg") (("" (case-replace "incoming_edges(y!1, del_edge(G!1,e!1)) = remove(e!1,incoming_edges(y!1, G!1))") (("1" (rewrite "card_remove[edgetype[T]]") (("1" (lift-if) (("1" (ground) (("1" (hide -1 2) (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (iff 1) (("2" (prop) (("1" (expand "incoming_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 nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "incoming_edges") (("2" (expand "remove") (("2" (flatten) (("2" (expand "member") (("2" (ground) (("2" (rewrite "del_edge_lem3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in_deg const-decl "nat" digraph_deg nil) (del_edge_lem3 formula-decl nil digraph_ops nil) (del_edge_lem formula-decl nil digraph_ops nil) (del_edge_lem2 formula-decl nil digraph_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) (remove const-decl "set" sets nil) (del_edge const-decl "digraph[T]" digraph_ops nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_remove application-judgement "finite_set" finite_sets nil)) shostak)) (deg_del_edge_outgoing 0 (deg_del_edge_outgoing-1 nil 3298475399 ("" (skosimp*) (("" (expand "out_deg") (("" (case-replace "outgoing_edges(x!1, del_edge(G!1,e!1)) = remove(e!1,outgoing_edges(x!1, G!1))") (("1" (rewrite "card_remove[edgetype[T]]") (("1" (lift-if) (("1" (ground) (("1" (hide -1 2) (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (iff 1) (("2" (prop) (("1" (expand "outgoing_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 nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "outgoing_edges") (("2" (expand "remove") (("2" (flatten) (("2" (expand "member") (("2" (ground) (("2" (rewrite "del_edge_lem3") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((out_deg const-decl "nat" digraph_deg nil) (del_edge_lem3 formula-decl nil digraph_ops nil) (del_edge_lem formula-decl nil digraph_ops nil) (del_edge_lem2 formula-decl nil digraph_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) (remove const-decl "set" sets nil) (del_edge const-decl "digraph[T]" digraph_ops nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_remove application-judgement "finite_set" finite_sets nil)) shostak)) (deg_del_non_edge 0 (deg_del_non_edge-1 nil 3298484996 ("" (skosimp*) (("" (expand "deg") (("" (expand "in_deg") (("" (expand "out_deg") (("" (case "incoming_edges(y!1, G!1) = incoming_edges(y!1, del_edge(G!1, e!1)) AND out (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (split) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "incoming_edges") (("1" (iff 1) (("1" (ground) (("1" (lemma "del_edge_lem3[T]") (("1" (inst?) (("1" (assert) (("1" (case "e!1 = (x!1,x!2)") (("1" (expand "in?") (("1" (propax) nil nil)) nil) ("2" (expand "in?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "in?") (("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "outgoing_edges") (("2" (iff 1) (("2" (ground) (("1" (lemma "del_edge_lem3[T]") (("1" (inst?) (("1" (assert) (("1" (case "e!1 = (x!1,x!2)") (("1" (expand "in?") (("1" (propax) nil nil)) nil) ("2" (expand "in?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "in?") (("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deg const-decl "nat" digraph_deg nil) (out_deg const-decl "nat" digraph_deg nil) (del_edge_lem2 formula-decl nil digraph_ops nil) (del_edge_lem3 formula-decl nil digraph_ops nil) (in? const-decl "bool" pairs nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (is_finite const-decl "bool" finite_sets nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (del_edge const-decl "digraph[T]" digraph_ops nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (in_deg const-decl "nat" digraph_deg nil)) shostak)) (deg_del_non_edge_incoming 0 (deg_del_non_edge_incoming-1 nil 3298488119 ("" (assert) (("" (skosimp*) (("" (expand "in_deg") (("" (case "incoming_edges(y!1, G!1) = incoming_edges(y!1, del_edge(G!1, e!1))") (("1" (assert) nil nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "incoming_edges") (("2" (iff 1) (("2" (ground) (("1" (lemma "del_edge_lem3[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((del_edge const-decl "digraph[T]" digraph_ops nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (del_edge_lem2 formula-decl nil digraph_ops nil) (del_edge_lem3 formula-decl nil digraph_ops nil) (in_deg const-decl "nat" digraph_deg nil)) shostak)) (deg_del_non_edge_outgoing 0 (deg_del_non_edge_outgoing-1 nil 3298488293 ("" (skosimp*) (("" (expand "out_deg") (("" (case "outgoing_edges(y!1, G!1) = outgoing_edges(y!1, del_edge(G!1, e!1))") (("1" (assert) nil nil) ("2" (hide 3) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "outgoing_edges") (("2" (iff 1) (("2" (ground) (("1" (lemma "del_edge_lem3[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "del_edge_lem2[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((out_deg const-decl "nat" digraph_deg nil) (del_edge_lem3 formula-decl nil digraph_ops nil) (del_edge_lem2 formula-decl nil digraph_ops nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (is_finite const-decl "bool" finite_sets nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (del_edge const-decl "digraph[T]" digraph_ops nil)) shostak)) (deg_del_edge 0 (deg_del_edge-1 nil 3298478034 ("" (skosimp*) (("" (expand "in?") (("" (split) (("1" (expand "self_loop?") (("1" (lemma "deg_del_edge_outgoing") (("1" (inst - "G!1" "e!1" "e!1`1" "e!1`2") (("1" (expand "deg") (("1" (lemma "deg_del_non_edge_incoming") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "self_loop?") (("2" (lemma "deg_del_edge_incoming") (("2" (inst - "G!1" "e!1" "e!1`1" "e!1`2") (("2" (expand "deg") (("2" (lemma "deg_del_non_edge_outgoing") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in? const-decl "bool" pairs nil) (deg_del_non_edge_outgoing formula-decl nil digraph_deg nil) (deg_del_edge_incoming formula-decl nil digraph_deg nil) (self_loop? const-decl "bool" digraph_deg nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (deg_del_non_edge_incoming formula-decl nil digraph_deg nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (deg const-decl "nat" digraph_deg nil) (deg_del_edge_outgoing formula-decl nil digraph_deg nil)) shostak)) (deg_del_self_loop 0 (deg_del_self_loop-1 nil 3298491682 ("" (skosimp*) (("" (expand "in?") (("" (expand "deg") (("" (lemma "deg_del_edge_incoming") (("" (inst - "G!1" "e!1" "e!1`1" "y!1") (("" (lemma "deg_del_edge_outgoing") (("" (inst - "G!1" "e!1" "y!1" "e!1`2") (("" (expand "self_loop?") (("" (copy -3) (("" (replace -6 -1) (("" (replace -6 -4 :dir rl) (("" (bddsimp -1) (("" (bddsimp -4) (("" (replace -1 -3) (("" (replace -2 -4) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in? const-decl "bool" pairs nil) (deg_del_edge_incoming formula-decl nil digraph_deg nil) (deg_del_edge_outgoing formula-decl nil digraph_deg nil) (self_loop? const-decl "bool" digraph_deg nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (deg const-decl "nat" digraph_deg nil)) shostak)) (deg_del_edge_ge_incoming 0 (deg_del_edge_ge_incoming-1 nil 3298490074 ("" (skosimp*) (("" (case "e!1 = (e!1`1, y!1)") (("1" (lemma "deg_del_edge_incoming") (("1" (inst - "G!1" "e!1" "e!1`1" "y!1") (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge_incoming") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deg_del_edge_incoming formula-decl nil digraph_deg nil) (deg_del_non_edge_incoming formula-decl nil digraph_deg nil)) shostak)) (deg_del_edge_ge_outgoing 0 (deg_del_edge_ge_outgoing-1 nil 3298491281 ("" (skosimp*) (("" (case "e!1 = (y!1, e!1`2)") (("1" (lemma "deg_del_edge_outgoing") (("1" (inst - "G!1" "e!1" "y!1" "e!1`2") (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge_outgoing") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deg_del_edge_outgoing formula-decl nil digraph_deg nil) (deg_del_non_edge_outgoing formula-decl nil digraph_deg nil)) shostak)) (deg_del_edge_ge 0 (deg_del_edge_ge-1 nil 3298281514 ("" (skosimp*) (("" (case "in?(y!1,e!1)") (("1" (lemma "deg_del_edge") (("1" (inst?) (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) (("1" (lemma "deg_del_self_loop") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (in? const-decl "bool" pairs nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pair type-eq-decl nil pairs nil) (T formal-type-decl nil digraph_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) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (deg_del_self_loop formula-decl nil digraph_deg nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deg_del_edge formula-decl nil digraph_deg nil) (deg_del_non_edge formula-decl nil digraph_deg nil)) nil)) (deg_del_edge_le_incoming 0 (deg_del_edge_le_incoming-1 nil 3298636487 ("" (skosimp*) (("" (case "e!1 = (e!1`1, y!1)") (("1" (lemma "deg_del_edge_incoming") (("1" (inst - "G!1" "e!1" "e!1`1" "y!1") (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge_incoming") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (deg_del_edge_incoming formula-decl nil digraph_deg nil) (deg_del_non_edge_incoming formula-decl nil digraph_deg nil)) shostak)) (deg_del_edge_le_outgoing 0 (deg_del_edge_le_outgoing-1 nil 3298636605 ("" (skosimp*) (("" (case "e!1 = (y!1, e!1`2)") (("1" (lemma "deg_del_edge_outgoing") (("1" (inst - "G!1" "e!1" "y!1" "e!1`2") (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge_outgoing") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (deg_del_edge_outgoing formula-decl nil digraph_deg nil) (deg_del_non_edge_outgoing formula-decl nil digraph_deg nil)) shostak)) (deg_del_edge_le 0 (deg_del_edge_le-1 nil 3298281514 ("" (skosimp*) (("" (case "in?(y!1,e!1)") (("1" (lemma "deg_del_edge") (("1" (inst?) (("1" (assert) (("1" (lemma "del_edge_lem5[T]") (("1" (inst?) (("1" (assert) (("1" (lemma "deg_del_self_loop") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deg_del_non_edge") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (in? const-decl "bool" pairs nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pair type-eq-decl nil pairs nil) (T formal-type-decl nil digraph_deg nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (del_edge_lem5 formula-decl nil digraph_ops nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (deg_del_self_loop formula-decl nil digraph_deg nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (deg_del_edge formula-decl nil digraph_deg nil) (deg_del_non_edge formula-decl nil digraph_deg nil)) nil)) (in_deg_edge_exists 0 (in_deg_edge_exists-1 nil 3298636784 ("" (skosimp*) (("" (expand "in_deg") (("" (rewrite "nonempty_card[edgetype[T]]" :dir rl) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "incoming_edges") (("" (skosimp*) (("" (expand "member") (("" (inst?) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in_deg const-decl "nat" digraph_deg nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs 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) (nonempty_card formula-decl nil finite_sets nil)) shostak)) (out_deg_edge_exists 0 (out_deg_edge_exists-1 nil 3298640405 ("" (skosimp*) (("" (expand "out_deg") (("" (rewrite "nonempty_card[edgetype[T]]" :dir rl) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "outgoing_edges") (("" (skosimp*) (("" (expand "member") (("" (inst?) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((out_deg const-decl "nat" digraph_deg nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs 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) (nonempty_card formula-decl nil finite_sets nil)) shostak)) (deg_edge_exists 0 (deg_edge_exists-1 nil 3298281514 ("" (skosimp*) (("" (expand "deg") (("" (lemma "in_deg_edge_exists") (("" (inst?) (("" (lemma "out_deg_edge_exists") (("" (inst?) (("" (assert) (("" (ground) (("1" (expand "in?") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (prop) (("2" (expand "in?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst?) (("3" (expand "in?") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deg const-decl "nat" digraph_deg nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (in? const-decl "bool" pairs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (out_deg_edge_exists formula-decl nil digraph_deg nil) (in_deg_edge_exists formula-decl nil digraph_deg nil)) nil)) (deg_to_card 0 (deg_to_card-1 nil 3298281514 ("" (skosimp*) (("" (lemma "deg_edge_exists") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (hide -1 -3) (("" (typepred "SG!1") (("" (inst?) (("" (assert) (("" (flatten) (("" (case "subset?(add[T](proj_1(e!1),singleton(proj_2(e!1))),vert(SG!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" (replace -1) (("1" (hide -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)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deg_edge_exists formula-decl nil digraph_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) (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) (size const-decl "nat" digraphs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (is_finite const-decl "bool" finite_sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set" finite_sets nil) (set type-eq-decl nil sets nil) (subset? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (simple_digraph type-eq-decl nil digraphs nil) (/= const-decl "boolean" notequal nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil)) nil)) (del_vert_deg_0 0 (del_vert_deg_0-1 nil 3298281514 ("" (skosimp*) (("" (expand "deg") (("" (expand "in_deg") (("" (expand "out_deg") (("" (lemma "card_empty?[edgetype[T]]") (("" (inst?) (("" (iff) (("" (assert) (("" (lemma "card_empty?[edgetype[T]]") (("" (inst - "outgoing_edges(v!1, G!1)") (("" (iff) (("" (assert) (("" (hide -3) (("" (expand "outgoing_edges") (("" (expand "incoming_edges") (("" (expand "empty?") (("" (expand "member") (("" (apply-extensionality 1 :hide? t) (("" (expand "del_vert") (("" (inst?) (("" (inst?) (("" (iff 1) (("" (expand "in?") (("" (ground) 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) ((deg const-decl "nat" digraph_deg nil) (out_deg const-decl "nat" digraph_deg nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (empty? const-decl "bool" sets nil) (del_vert const-decl "digraph[T]" digraph_ops nil) (in? const-decl "bool" pairs nil) (member const-decl "bool" sets nil) (card_empty? formula-decl nil finite_sets nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (in_deg const-decl "nat" digraph_deg nil)) nil)) (singleton_loops 0 (singleton_loops-1 nil 3298653367 ("" (skosimp*) (("" (expand "singleton?") (("" (expand "self_loop?") (("" (expand "size") (("" (typepred! "e!1") (("" (lemma "edge_in_card_gt_1") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton? const-decl "bool" digraphs nil) (size const-decl "nat" digraphs nil) (edge_in_card_gt_1 formula-decl nil digraphs 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 digraph_deg nil) (edgetype type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (/= const-decl "boolean" notequal nil) (simple_digraph type-eq-decl nil digraphs nil) (self_loop? const-decl "bool" digraph_deg nil)) shostak)) (singleton_edges 0 (singleton_edges-1 nil 3298651751 ("" (skosimp*) (("" (lemma "singleton_loops") (("" (inst?) (("" (assert) (("" (expand "self_loop?") (("" (apply-extensionality 1 :hide? t) (("" (inst -1 "(x!1, x!2)") (("1" (expand "incoming_edges") (("1" (expand "outgoing_edges") (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton_loops formula-decl nil digraph_deg nil) (set type-eq-decl nil sets nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (is_finite const-decl "bool" finite_sets nil) (x!2 skolem-const-decl "T" digraph_deg nil) (x!1 skolem-const-decl "T" digraph_deg nil) (SG!1 skolem-const-decl "simple_digraph[T]" digraph_deg nil) (self_loop? const-decl "bool" digraph_deg nil) (simple_digraph type-eq-decl nil digraphs nil) (/= const-decl "boolean" notequal nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil)) shostak)) (singleton_deg 0 (singleton_deg-1 nil 3298281514 ("" (skosimp*) (("" (lemma "singleton_edges") (("" (inst - "v!1" "SG!1") (("" (assert) (("" (expand "in_deg") (("" (expand "out_deg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton_edges formula-decl nil digraph_deg nil) (out_deg const-decl "nat" digraph_deg nil) (in_deg const-decl "nat" digraph_deg nil) (simple_digraph type-eq-decl nil digraphs nil) (/= const-decl "boolean" notequal nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil digraph_deg nil)) nil)) (in_deg_1_sing 0 (in_deg_1_sing-1 nil 3298727916 ("" (skosimp*) (("" (expand "in_deg") (("" (lemma "card_one[edgetype[T]]") (("" (inst?) (("" (flatten) (("" (assert) (("" (hide -2) (("" (skosimp*) (("" (inst?) (("" (assert) (("" (case-replace "incoming_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)") (("1" (hide -2) (("1" (expand "incoming_edges") (("1" (expand "singleton") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in_deg const-decl "nat" digraph_deg nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (incoming_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (card_one formula-decl nil finite_sets nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil)) shostak)) (out_deg_1_sing 0 (out_deg_1_sing-1 nil 3298728100 ("" (skosimp*) (("" (expand "out_deg") (("" (lemma "card_one[edgetype[T]]") (("" (inst?) (("" (flatten) (("" (assert) (("" (hide -2) (("" (skosimp*) (("" (inst?) (("" (assert) (("" (case-replace "outgoing_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)") (("1" (hide -2) (("1" (expand "outgoing_edges") (("1" (expand "singleton") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((out_deg const-decl "nat" digraph_deg nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (outgoing_edges const-decl "finite_set[edgetype[T]]" digraph_deg nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (card_one formula-decl nil finite_sets nil) (T formal-type-decl nil digraph_deg nil) (edgetype type-eq-decl nil digraphs nil)) shostak)) (deg_1_sing 0 (deg_1_sing-1 nil 3298735089 ("" (skosimp*) (("" (expand "deg") (("" (case "in_deg(v!1, G!1) = 1 AND out_deg(v!1, G!1) = 0") (("1" (flatten) (("1" (lemma "in_deg_1_sing") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "in_deg") (("1" (lemma "card_one[edgetype[T]]") (("1" (inst?) (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (case "incoming_edges(v!1, G!1) = incident_edges(v!1, G!1)") (("1" (case-replace "incident_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)") (("1" (assert) (("1" (expand "incident_edges") (("1" (expand "singleton") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "out_deg") (("2" (apply-extensionality 1 :hide? t) (("2" (bddsimp 2) (("2" (expand "incoming_edges" 1) (("2" (expand "incident_edges" 1) (("2" (expand "in?") (("2" (rewrite "card_empty?") (("2" (expand "outgoing_edges") (("2" (expand "empty?") (("2" (inst -6 "(x!2, x!3)") (("2" (expand "member") (("2" (bddsimp 1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (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)) nil)) nil) ("2" (case "in_deg(v!1, G!1) = 0 AND out_deg(v!1, G!1) = 1") (("1" (flatten) (("1" (lemma "out_deg_1_sing") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "out_deg") (("1" (lemma "card_one[edgetype[T]]") (("1" (inst?) (("1" (flatten) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (case "outgoing_edges(v!1, G!1) = incident_edges(v!1, G!1)") (("1" (case-replace "incident_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)") (("1" (assert) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.101 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
