| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispUntersuchung PVS© |
|
|
(mantel
(one_to_some 0 (one_to_some-1 nil 3599344018 ("" (skolem!) (("" (flatten) (("" (expand "tri?") (("" (expand "tri?") (("" (inst 1 "z!1") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mantel nil) (tri? const-decl "bool" mantel nil) (tri? const-decl "bool" mantel nil)) shostak)) (some_to_lots 0 (some_to_lots-1 nil 3599345379 ("" (ground) (("" (skolem!) (("" (flatten) (("" (expand "tri?") (("" (expand "tri?") (("" (skolem!) (("" (assert) (("" (inst 1 "x!1" "y!1" "z!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tri? const-decl "bool" mantel nil) (tri? const-decl "bool" mantel nil) (T formal-type-decl nil mantel nil) (tri? const-decl "bool" mantel nil)) shostak)) (one_to_lots 0 (one_to_lots-1 nil 3599345415 ("" (skolem!) (("" (flatten) (("" (expand "tri?") (("" (expand "tri?") (("" (inst 1 "x!1" "y!1" "z!1") nil nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mantel nil) (tri? const-decl "bool" mantel nil) (tri? const-decl "bool" mantel nil)) shostak)) (exst_tri 0 (exst_tri-1 nil 3599405533 ("" (skosimp*) (("" (expand "tri?") (("" (expand "edge?") (("" (expand "common_neighbor?") (("" (skolem!) (("" (expand "tri?") (("" (lemma "edges_vert_in") (("" (copy -1) (("" (inst -2 "G!1" "dbl[T](x!1,y!1)" "x!1" "y!1") (("" (expand "edge?") (("" (inst -1 "G!1" "dbl[T](x!1, z!1)" "x!1" "z!1") (("" (inst 1 "z!1") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tri? const-decl "bool" mantel nil) (common_neighbor? const-decl "bool" mantel nil) (tri? const-decl "bool" mantel 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 mantel nil) (edges_vert_in formula-decl nil graphs nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" mantel nil)) shostak)) (one_vert_edges 0 (one_vert_edges-1 nil 3599485848 ("" (skosimp*) (("" (lemma "singleton_edges") (("" (inst?) (("" (prop) (("" (lemma "emptyset_is_empty?") (("" (inst -1 "edges(G!1)") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mantel nil) (singleton_edges formula-decl nil graphs nil) (emptyset_is_empty? formula-decl nil 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) (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)) shostak)) (edge_adjacent 0 (edge_adjacent-1 nil 3599430155 ("" (skosimp*) (("" (expand "adjacent") (("" (lemma "vert_in") (("" (inst -1 "G!1" "x!1" "y!1") (("" (prop) (("" (assert) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjacent const-decl "finite_set[T]" graph_ops 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) (nil application-judgement "finite_set[T]" mantel nil) (edge? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (vert_in formula-decl nil graphs nil) (T formal-type-decl nil mantel nil)) shostak)) (disj_neighbor_sets 0 (disj_neighbor_sets-1 nil 3599429113 ("" (skolem!) (("" (flatten) (("" (rewrite "disjoint?") (("" (rewrite "common_neighbor?") (("" (skolem!) (("" (expand "empty?") (("" (inst -1 "z!1") (("" (expand "edge?") (("" (lemma "edge_adjacent") (("" (inst -1 "G!1" "x!1" "z!1") (("" (lemma "edge_adjacent") (("" (inst -1 "G!1" "y!1" "z!1") (("" (expand "edge?") (("" (prop) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((common_neighbor? const-decl "bool" mantel nil) (empty? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" mantel nil) (edge? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (edge_adjacent formula-decl nil mantel nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (T formal-type-decl nil mantel nil) (adjacent const-decl "finite_set[T]" graph_ops 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) (disjoint? const-decl "bool" sets nil)) shostak)) (adj_is_subset 0 (adj_is_subset-1 nil 3599516023 ("" (skosimp*) (("" (expand "subset?") (("" (expand "adjacent") (("" (assert) (("" (expand "union") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" mantel nil) (member const-decl "bool" sets nil) (edge? const-decl "bool" graphs nil) (T formal-type-decl nil mantel nil) (/= const-decl "boolean" notequal nil) (union const-decl "set" sets nil) (adjacent const-decl "finite_set[T]" graph_ops nil)) shostak)) (adj_is_subset2 0 (adj_is_subset2-1 nil 3599580805 ("" (skosimp*) (("" (expand "subset?") (("" (expand "adjacent") (("" (assert) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (T formal-type-decl nil mantel nil) (edge? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" mantel nil) (adjacent const-decl "finite_set[T]" graph_ops nil)) shostak)) (no_cn 0 (no_cn-1 nil 3599516518 ("" (skosimp*) (("" (expand "common_neighbor?") (("" (expand "adjacent") (("" (lemma "vert_in") (("" (inst?) (("" (expand "disjoint?") (("" (expand "intersection") (("" (expand "empty?") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((common_neighbor? const-decl "bool" mantel nil) (T formal-type-decl nil mantel nil) (vert_in formula-decl nil graphs nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" mantel nil) (intersection const-decl "set" 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) (adjacent const-decl "finite_set[T]" graph_ops nil)) shostak)) (disj_adj_card 0 (disj_adj_card-1 nil 3599662456 ("" (skosimp*) (("" (lemma "card_disj_union[T]") (("" (inst?) (("" (prop) (("" (lemma "adj_is_subset") (("" (inst?) (("" (lemma "card_subset[T]") (("" (inst?) (("" (prop) (("" (expand "size") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mantel nil) (card_disj_union formula-decl nil finite_sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (union const-decl "set" sets nil) (size const-decl "nat" graphs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (nil application-judgement "finite_set[T]" mantel nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (edge? const-decl "bool" graphs nil) (card_subset formula-decl nil finite_sets nil) (adj_is_subset formula-decl nil mantel nil) (adjacent const-decl "finite_set[T]" graph_ops nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (pre_edges_del21 0 (pre_edges_del21-1 nil 3599666465 ("" (skosimp) (("" (expand "del2_vert") (("" (expand "del_vert") (("" (expand "incident_edges") (("" (expand "union") (("" (apply-extensionality) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((del2_vert const-decl "graph[T]" mantel nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (T formal-type-decl nil mantel 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) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (OR const-decl "[bool, 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) (union const-decl "set" sets nil) (del_vert const-decl "graph[T]" graph_ops nil)) shostak)) (pre_edges_del22 0 (pre_edges_del22-1 nil 3599666650 ("" (skosimp*) (("" (expand "disjoint?") (("" (lemma "emptyset_is_empty?") (("" (inst?) (("" (prop) (("" (hide 2 3) (("" (expand "incident_edges") (("" (expand "del2_vert") (("" (expand "del_vert") (("" (expand "intersection") (("" (apply-extensionality) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_intersection1 application-judgement "finite_set" mantel nil) (disjoint? const-decl "bool" sets nil) (intersection const-decl "set" 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) (del2_vert const-decl "graph[T]" mantel nil) (union const-decl "set" sets nil) (is_finite const-decl "bool" finite_sets nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (finite_emptyset name-judgement "finite_set" mantel nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (emptyset const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (del_vert const-decl "graph[T]" graph_ops nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (T formal-type-decl nil mantel 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)) shostak)) (edges_del2 0 (edges_del2-1 nil 3599521819 ("" (skosimp*) (("" (lemma "pre_edges_del21") (("" (inst?) (("" (lemma "pre_edges_del22") (("" (inst?) (("" (lemma "card_disj_union") (("" (inst -1 "edges(del2_vert(G!1, x!1, y!1))" "union(incident_edges(x!1, G!1), incident_edges(y!1, G!1))") (("" (prop) (("" (replace -3 -1 rl) (("" (expand "num_edges") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pre_edges_del21 formula-decl nil mantel nil) (pre_edges_del22 formula-decl nil mantel nil) (card_disj_union formula-decl nil finite_sets nil) (num_edges const-decl "nat" graph_ops nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (union const-decl "set" sets nil) (del2_vert const-decl "graph[T]" mantel nil) (is_finite const-decl "bool" finite_sets nil) (finite_union application-judgement "finite_set" mantel 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 mantel nil)) shostak)) (verts_del2 0 (verts_del2-1 nil 3599522689 ("" (skosimp*) (("" (expand "del2_vert") (("" (lemma "size_del_vert") (("" (inst -1 "G!1" "x!1") (("" (lemma "del_vert_still_in") (("" (inst -1 "G!1" "x!1" "y!1") (("" (prop) (("1" (lemma "size_del_vert") (("1" (inst -1 "del_vert(G!1,x!1)" "y!1") (("1" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((del2_vert const-decl "graph[T]" mantel nil) (x!1 skolem-const-decl "T" mantel nil) (G!1 skolem-const-decl "graph[T]" mantel 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) (y!1 skolem-const-decl "T" mantel nil) (size const-decl "nat" graphs nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_remove application-judgement "finite_set" finite_sets nil) (del_vert const-decl "graph[T]" graph_ops nil) (del_vert_still_in formula-decl nil graph_ops nil) (size_del_vert formula-decl nil graph_ops nil) (T formal-type-decl nil mantel nil)) shostak)) (tri_del2 0 (tri_del2-1 nil 3599586908 ("" (skosimp*) (("" (expand "del2_vert") (("" (expand "tri?" -1) (("" (expand "tri?" -1) (("" (expand "edge?") (("" (skolem!) (("" (expand "del_vert") (("" (expand "tri?") (("" (expand "tri?") (("" (inst 1 "x!2" "y!2" "z!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((del2_vert const-decl "graph[T]" mantel nil) (tri? const-decl "bool" mantel nil) (T formal-type-decl nil mantel nil) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (dbl const-decl "set[T]" doubletons nil) (finite_remove application-judgement "finite_set" finite_sets nil) (del_vert const-decl "graph[T]" graph_ops nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" mantel nil) (tri? const-decl "bool" mantel nil)) shostak)) (int_lem 0 (int_lem-1 nil 3599526905 ("" (skosimp*) (("" (expand "edge?") (("" (grind) (("" (lemma "dbl_comm") (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((nil application-judgement "finite_set[T]" mantel nil) (edge? const-decl "bool" graphs nil) (dbl_comm formula-decl nil doubletons nil) (NOT const-decl "[bool -> bool]" booleans 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 "[T, T -> boolean]" equalities 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) (singleton? const-decl "bool" sets nil) (/= const-decl "boolean" notequal nil) (dbl const-decl "set[T]" doubletons nil) (T formal-type-decl nil mantel nil)) shostak)) (card_union 0 (card_union-1 nil 3599525549 ("" (skosimp*) (("" (lemma "card_union") (("" (inst?) (("" (expand "incident_edges") (("" (lemma "edge_has_2_verts") (("" (grind) (("" (expand "intersection") (("" (grind) (("" (lemma "int_lem") (("" (inst?) (("" (expand "edge?") (("" (lemma "singleton_singleton") (("" (inst?) (("" (prop) (("" (skolem!) (("" (lemma "card_singleton") (("" (inst?) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 mantel nil) (card_union formula-decl nil finite_sets nil) (edge? const-decl "bool" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" mantel nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (member const-decl "bool" sets nil) (singleton_singleton formula-decl nil sets nil) (card_singleton formula-decl nil finite_sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" mantel nil) (int_lem formula-decl nil mantel nil) (intersection const-decl "set" sets nil) (edge_has_2_verts formula-decl nil graphs 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (adj_helper 0 (adj_helper-1 nil 3599611275 ("" (skosimp*) (("" (expand "empty?") (("" (lemma "adj_is_subset2") (("" (inst?) (("" (lemma "card_emptyset[T]") (("" (lemma "emptyset_min[T]") (("" (inst -1 "adjacent(G!1,x!1)") (("" (prop) (("1" (replace -1 -2 rl) (("1" (propax) nil nil)) nil) ("2" (expand "empty?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" graphs nil) (T formal-type-decl nil mantel 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) (emptyset_min formula-decl nil sets_lemmas nil) (nil application-judgement "finite_set[T]" mantel nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (edge? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (emptyset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (is_finite const-decl "bool" finite_sets nil) (adjacent const-decl "finite_set[T]" graph_ops nil) (card_emptyset formula-decl nil finite_sets nil) (adj_is_subset2 formula-decl nil mantel nil)) shostak)) (adj_helper2 0 (adj_helper2-1 nil 3599615305 ("" (skosimp*) (("" (expand "adjacent") (("" (expand "edge?") (("" (grind) (("" (lemma "card_emptyset[T]") (("" (grind) (("" (replace -1 1 rl) (("" (grind) (("" (lemma "emptyset[T]") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((adjacent const-decl "finite_set[T]" graph_ops nil) (/= const-decl "boolean" notequal nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set" mantel nil) (emptyset const-decl "set" sets nil) (T formal-type-decl nil mantel nil) (card_emptyset formula-decl nil finite_sets nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" mantel nil)) shostak)) (inc_ind1 0 (inc_ind1-1 nil 3599619746 ("" (skosimp*) (("" (expand "incident_edges") (("" (expand "del_edge") (("" (apply-extensionality) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (T formal-type-decl nil mantel 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) (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) (remove const-decl "set" sets nil) (finite_remove application-judgement "finite_set" mantel nil) (member const-decl "bool" sets nil) (del_edge const-decl "graph[T]" graph_ops nil)) shostak)) (adj_ind1 0 (adj_ind1-1 nil 3599620302 ("" (skosimp*) (("" (expand "adjacent") (("" (expand "del_edge") (("" (expand "edge?") (("" (apply-extensionality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((adjacent const-decl "finite_set[T]" graph_ops nil) (nil application-judgement "finite_set[T]" mantel nil) (edge? const-decl "bool" graphs nil) (member const-decl "bool" sets nil) (finite_remove application-judgement "finite_set" mantel nil) (G!1 skolem-const-decl "graph[T]" mantel nil) (graph type-eq-decl nil graphs 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) (set type-eq-decl nil sets nil) (x!1 skolem-const-decl "T" mantel nil) (/= const-decl "boolean" notequal 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) (remove const-decl "set" sets nil) (T formal-type-decl nil mantel nil) (boolean nonempty-type-decl nil booleans nil) (del_edge const-decl "graph[T]" graph_ops nil)) shostak)) (inc_ind2 0 (inc_ind2-1 nil 3599620901 ("" (skosimp*) (("" (expand "incident_edges") (("" (expand "del_edge") (("" (lemma "card_remove") (("" (case "{e: doubleton[T] | remove(e!1, edges(G!1))(e) AND e(x!1)} = remove(e!1,{e: doubleton[T] | edges(G!1)(e) AND e(x!1)})") (("1" (inst -2 "{e: doubleton[T] | edges(G!1)(e) AND e(x!1)}" "e!1") (("1" (grind) nil nil) ("2" (typepred "incident_edges(x!1,G!1)") (("2" (expand "incident_edges") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((incident_edges const-decl "finite_set[doubleton[T]]" graph_deg 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 mantel nil) (card_remove formula-decl nil finite_sets nil) (finite_remove application-judgement "finite_set" mantel nil) (is_finite const-decl "bool" finite_sets nil) (G!1 skolem-const-decl "graph[T]" mantel nil) (x!1 skolem-const-decl "T" mantel nil) (int_minus_int_is_int application-judgement "int" integers nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (remove const-decl "set" 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) (del_edge const-decl "graph[T]" graph_ops nil)) shostak)) (adj_ind2 0 (adj_ind2-1 nil 3599622537 ("" (skosimp*) (("" (lemma "other_vert") (("" (inst?) (("" (inst -1 "G!1") (("" (prop) (("" (skolem!) (("" (flatten) (("" (expand "adjacent") (("" (expand "del_edge") (("" (lemma "card_remove[T]") (("" (case "{y: T | G!1`vert(y) AND edge?(G!1 WITH [edges := remove(e!1, edges(G!1))])(x!1, y)} = remove(u!1,{y: T | vert(G!1)(y) AND edge?(G!1)(x!1, y)})") (("1" (inst -2 "{y: T | vert(G!1)(y) AND edge?(G!1)(x!1, y)}" "u!1") (("1" (expand "edge?") (("1" (grind) (("1" (lemma "dbl_comm") (("1" (inst -1 "x!1" "u!1") (("1" (replace -1 -6 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "adjacent(G!1,x!1)") (("2" (expand "adjacent") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (apply-extensionality) (("1" (replace -3 1) (("1" (expand "edge?") (("1" (hide -1 2 4) (("1" (grind) (("1" (lemma "dbl_comm") (("1" (inst?) nil nil)) nil) ("2" (lemma "dbl_comm") (("2" (inst -1 "x!1" "u!1") (("2" (replace -1 -2 rl) (("2" (lemma "dbl_eq") (("2" (inst -1 "x!1" "x!1" "u!1" "x!2") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 3 4) (("2" (grind) (("1" (lemma "edges_vert_in") (("1" (inst -1 "G!1" "e!2" "x!2" "y!2") (("1" (prop) (("1" (replace -1 -3 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "edges_vert_in") (("2" (inst -1 "G!1" "e!2" "x!2" "y!2") (("2" (prop) (("2" (replace -1 -3 rl) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1) (("3" (grind) (("1" (lemma "edges_vert_in") (("1" (inst -1 "G!1" "e!2" "x!2" "y!2") (("1" (replace -2 -4 rl) (("1" (prop) nil nil)) nil)) nil)) nil) ("2" (lemma "edges_vert_in") (("2" (inst -1 "G!1" "e!2" "x!2" "y!2") (("2" (replace -2 -4 rl) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil mantel nil) (other_vert formula-decl nil graphs 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) (adjacent const-decl "finite_set[T]" graph_ops nil) (card_remove formula-decl nil finite_sets nil) (e!1 skolem-const-decl "doubleton[T]" mantel nil) (dbl_eq formula-decl nil doubletons nil) (edges_vert_in formula-decl nil graphs nil) (is_finite const-decl "bool" finite_sets nil) (G!1 skolem-const-decl "graph[T]" mantel nil) (x!1 skolem-const-decl "T" mantel nil) (member const-decl "bool" sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (dbl_comm formula-decl nil doubletons nil) (nil application-judgement "finite_set[T]" mantel nil) (NOT const-decl "[bool -> bool]" booleans nil) (remove const-decl "set" sets nil) (edge? const-decl "bool" graphs nil) (finite_remove application-judgement "finite_set" mantel nil) (del_edge const-decl "graph[T]" graph_ops 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)) shostak)) (inc_equals_adj 0 (inc_equals_adj-1 nil 3599575984 ("" (induct "G" 1 "graph_induction_edge") (("" (skosimp*) (("" (case "num_edges(G!1)>=1") (("1" (expand "num_edges") (("1" (case "card(edges(G!1))>0") (("1" (hide -2) (("1" (lemma "nonempty_card") (("1" (inst -1 "edges(G!1)") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (prop) (("1" (skolem!) (("1" (hide -2) (("1" (case "x!2(x!1)") (("1" (lemma "inc_ind2") (("1" (inst -1 "G!1" "x!2" "x!1") (("1" (prop) (("1" (lemma "adj_ind2") (("1" (inst -1 "G!1" "x!2" "x!1") (("1" (prop) (("1" (lemma "del_edge_num") (("1" (inst -1 "G!1" "x!2") (("1" (lift-if) (("1" (prop) (("1" (inst -8 "del_edge(G!1, x!2)") (("1" (expand "num_edges") (("1" (case "card(edges(del_edge(G!1, x!2))) < card(edges(G!1))") (("1" (prop) (("1" (inst -1 "x!1") (("1" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "inc_ind1") (("2" (inst -1 "G!1" "x!2" "x!1") (("2" (prop) (("1" (lemma "adj_ind1") (("1" (inst?) (("1" (inst -1 "x!1") (("1" (prop) (("1" (lemma "del_edge_num") (("1" (inst?) (("1" (lift-if) (("1" (prop) (("1" (inst -7 "del_edge(G!1,x!2)") (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil) ("2" (expand "num_edges") (("2" (lemma "card_emptyset[doubleton[T]]") (("2" (case "edges(G!1) = emptyset[doubleton[T]]") (("1" (lemma "adj_helper2") (("1" (inst?) (("1" (prop) (("1" (lemma "incident_edges_subset") (("1" (inst?) (("1" (replace -3 -1) (("1" (lemma "emptyset_min[doubleton[T]]") (("1" (inst -1 "incident_edges(x!1, G!1)") (("1" (prop) (("1" (replace -1 -5 rl) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "card(edges(G!1))=0") (("1" (lemma "card_is_0") (("1" (inst -1 "edges(G!1)") (("1" (grind) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set" mantel nil) (emptyset const-decl "set" sets nil) (incident_edges_subset formula-decl nil graph_deg nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" mantel nil) (subset? const-decl "bool" sets nil) (emptyset_min formula-decl nil sets_lemmas nil) (adj_helper2 formula-decl nil mantel nil) (card_is_0 formula-decl nil finite_sets nil) (card_emptyset formula-decl nil finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (adj_ind2 formula-decl nil mantel nil) (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_remove application-judgement "finite_set" mantel nil) (< const-decl "bool" reals nil) (del_edge const-decl "graph[T]" graph_ops nil) (del_edge_num formula-decl nil graph_ops nil) (inc_ind2 formula-decl nil mantel nil) (adj_ind1 formula-decl nil mantel nil) (inc_ind1 formula-decl nil mantel nil) (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (> const-decl "bool" reals nil) (num_edges const-decl "nat" graph_ops nil) (graph_induction_edge formula-decl nil graph_inductions nil) (T formal-type-decl nil mantel nil) (adjacent const-decl "finite_set[T]" graph_ops nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (is_finite const-decl "bool" finite_sets nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (Mantel 0 (Mantel-1 nil 3599409890 ("" (induct "G" 1 "graph_induction_vert") (("" (skosimp*) (("" (case "NOT num_edges(G!1)>0") (("1" (expand "num_edges" 1) (("1" (lemma "nonempty_card") (("1" (inst -1 "edges(G!1)") (("1" (expand "num_edges" 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (copy -1) (("2" (expand "num_edges" -2) (("2" (lemma "nonempty_card") (("2" (inst -1 "edges(G!1)") (("2" (case "card(edges(G!1))>0 IMPLIES nonempty?(edges(G!1))") (("1" (prop) (("1" (hide -1 -2) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (skolem!) (("1" (typepred "x!1") (("1" (skolem! -1) (("1" (lemma "edges_vert_in") (("1" (flatten -2) (("1" (inst -1 "G!1" "x!1" "x!2" "y!1") (("1" (prop) (("1" (case "common_neighbor?(G!1)(x!2,y!1)") (("1" (lemma "exst_tri") (("1" (inst -1 "G!1" "x!2" "y!1") (("1" (expand "edge?") (("1" (lemma "some_to_lots") (("1" (inst -1 "G!1" "x!2" "y!1") (("1" (replace -6 -7) (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "edges_del2") (("2" (inst -1 "G!1" "x!2" "y!1") (("2" (lemma "verts_del2") (("2" (inst -1 "G!1" "x!2" "y!1") (("2" (prop) (("2" (inst -9 "del2_vert(G!1, x!2, y!1)") (("2" (replace -1 -9) (("2" (case "size(G!1)-2 (("1" (prop) (("1" (lemma "card_union") (("1" (inst -1 "G!1" "x!2" "y!1") (("1" (expand "edge?") (("1" (prop) (("1" (replace -1 -5) (("1" (hide -10 -11) (("1" (case "size(G!1)=size(del2_vert(G!1, x!2, y!1))+2") (("1" (replace -1 4) (("1" (lemma "inc_equals_adj") (("1" (copy -1) (("1" (inst -1 "G!1" "x!2") (("1" (inst -2 "G!1" "y!1") (("1" (replace -1 -8) (("1" (replace -2 -8) (("1" (hide -1 -2) (("1" (hide -2) (("1" (lemma "no_cn") (("1" (inst -1 "G!1" "x!2" "y!1") (("1" (prop) (("1" (lemma "disj_adj_card") (("1" (inst -1 "G!1" "x!2" "y!1") (("1" (prop) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.67Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchenEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
