| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 53 kB |
|
Quelle sep_set_lems.prf Sprache: Lisp |
|||||||||
|
(sep_set_lems
(sep_num_0 0 (sep_num_0-1 nil 3251049123 ("" (skosimp*) (("" (expand "sep_num") (("" (lemma "min_sep_set_seps") (("" (lemma "card_is_0[T]") (("" (inst?) (("" (iff -1) (("" (assert) (("" (inst?) (("" (assert) nil)))))))))))))))) nil) ((sep_num const-decl "nat" sep_sets nil) (card_is_0 formula-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (min_sep_set const-decl "finite_set[T]" sep_sets 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) (min_sep_set_seps formula-decl nil sep_sets nil) (T formal-type-decl nil sep_set_lems nil)) nil)) (sep_num_gt_0 0 (sep_num_gt_0-1 nil 3251049123 ("" (skosimp*) (("" (expand "sep_num") (("" (case "separates(G!1,emptyset[T],s!1,t!1)") (("1" (lemma "min_sep_set_card") (("1" (inst?) (("1" (assert) (("1" (rewrite "card_emptyset[T]") (("1" (assert) nil))))))))) ("2" (hide -1 -2) (("2" (expand "separates") (("2" (prop) (("1" (expand "emptyset") (("1" (propax) nil))) ("2" (expand "emptyset") (("2" (propax) nil))) ("3" (skosimp*) (("3" (typepred "w!1") (("3" (case-replace "del_verts(G!1, emptyset[T]) = G!1") (("1" (hide -1) (("1" (inst 1 "w!1") nil))) ("2" (hide -1 -2 -3 2) (("2" (apply-extensionality :hide? t) (("1" (apply-extensionality :hide? t) (("1" (expand "emptyset") (("1" (expand "del_verts") (("1" (propax) nil))))))) ("2" (apply-extensionality :hide? t) (("2" (expand "del_verts") (("2" (grind) nil)))))))))))))))))))))))))) nil) ((sep_num const-decl "nat" sep_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks nil) (finite_difference application-judgement "finite_set" finite_sets nil) (difference const-decl "set" sets nil) (member const-decl "bool" sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (min_sep_set_card formula-decl nil sep_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (card_emptyset formula-decl nil finite_sets nil) (t!1 skolem-const-decl "T" sep_set_lems nil) (s!1 skolem-const-decl "T" sep_set_lems nil) (G!1 skolem-const-decl "graph[T]" sep_set_lems nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (T formal-type-decl nil sep_set_lems 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) (separates const-decl "bool" sep_sets nil) (emptyset const-decl "set" sets nil)) nil)) (sep_num_is_1 0 (sep_num_is_1-1 nil 3251049123 ("" (skosimp*) (("" (case "separates(G!1, singleton[T](v!1), s!1, t!1)") (("1" (hide -2) (("1" (expand "sep_num") (("1" (lemma "min_sep_set_card") (("1" (inst?) (("1" (assert) (("1" (rewrite "card_singleton[T]") nil))) ("2" (reveal -2) (("2" (propax) nil))))))))))) ("2" (hide 2) (("2" (expand "separates") (("2" (split 1) (("1" (expand "singleton") (("1" (reveal 1) (("1" (assert) nil))))) ("2" (expand "singleton") (("2" (assert) nil))) ("3" (skosimp*) (("3" (inst -4 "w!1") (("3" (expand "walk_from?") (("3" (flatten) (("3" (assert) (("3" (split -6) (("1" (skosimp*) (("1" (expand "walk?") (("1" (flatten) (("1" (hide -5) (("1" (expand "verts_in?") (("1" (inst - "i!1") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (flatten) (("1" (expand "singleton") (("1" (propax) nil))))))))))))))))))))))) ("2" (hide -1 -2 3) (("2" (expand "walk?") (("2" (flatten) (("2" (split 1) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (expand "singleton") (("1" (flatten) (("1" (propax) nil))))))))))))))))))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) (("2" (expand "edge?") (("2" (flatten) (("2" (expand "del_verts") (("2" (flatten) (("2" (hide -4) (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))) ("3" (rewrite "finite_singleton") nil)))) nil) ((singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (separates const-decl "bool" sep_sets 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 sep_set_lems nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (sep_num const-decl "nat" sep_sets nil) (G!1 skolem-const-decl "graph[T]" sep_set_lems nil) (t!1 skolem-const-decl "T" sep_set_lems nil) (s!1 skolem-const-decl "T" sep_set_lems nil) (card_singleton formula-decl nil finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_sep_set_card formula-decl nil sep_sets nil) (walk_from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" sep_set_lems nil) (edge? const-decl "bool" graphs nil) (finite_difference application-judgement "finite_set" finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil) (del_verts const-decl "graph[T]" sep_sets nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (walk? const-decl "bool" walks nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil)) nil)) (sep_num_le1 0 (sep_num_le1-1 nil 3251049123 ("" (skosimp*) (("" (expand "sep_num") (("" (lemma "min_sep_set_seps") (("" (inst?) (("" (assert) (("" (case "card(min_sep_set(G!1, s!1, t!1)) = 1") (("1" (lemma "card_one[T]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (lemma "min_sep_set_vert") (("1" (inst?) (("1" (inst - "x!1") (("1" (assert) (("1" (replace -2) (("1" (expand "singleton" -1) (("1" (expand "separable?") (("1" (flatten) (("1" (assert) (("1" (expand "separates") (("1" (flatten) (("1" (expand "singleton") (("1" (assert) nil))))))))))))))))))))))))))))))))))) ("2" (case "card(min_sep_set(G!1, s!1, t!1)) = 0") (("1" (hide -6 1) (("1" (lemma "sep_num_0") (("1" (inst -1 "G!1" "s!1" "t!1") (("1" (assert) (("1" (expand "sep_num") (("1" (inst + "av!1") (("1" (assert) (("1" (hide -2 -3 -7) (("1" (expand "separates") (("1" (flatten) (("1" (assert) (("1" (expand "singleton") (("1" (skosimp*) (("1" (inst?) (("1" (expand "walk_from?") (("1" (flatten) (("1" (assert) (("1" (expand "walk?") (("1" (flatten) (("1" (split +) (("1" (expand "verts_in?") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "emptyset") (("1" (propax) nil))))))))))))))))))))) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "del_verts") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (expand "emptyset") (("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil)))))))))))))) nil) ((sep_num const-decl "nat" sep_sets 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) (min_sep_set const-decl "finite_set[T]" sep_sets 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) (min_sep_set_vert formula-decl nil sep_sets nil) (separable? const-decl "bool" sep_sets nil) (separates const-decl "bool" sep_sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (card_one formula-decl nil finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (walk_from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finite_difference application-judgement "finite_set" finite_sets nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" sep_set_lems nil) (verts_in? const-decl "bool" walks nil) (difference const-decl "set" sets nil) (emptyset const-decl "set" sets nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (member const-decl "bool" sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (walk? const-decl "bool" walks nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (sep_num_0 formula-decl nil sep_set_lems nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_sep_set_seps formula-decl nil sep_sets nil) (T formal-type-decl nil sep_set_lems nil)) nil)) (separable?_comm 0 (separable?_comm-1 nil 3251049123 ("" (skosimp*) (("" (expand "separable?") (("" (flatten) (("" (assert) (("" (expand "edge?") (("" (rewrite "dbl_comm") nil)))))))))) nil) ((separable? const-decl "bool" sep_sets nil) (T formal-type-decl nil sep_set_lems nil) (dbl_comm formula-decl nil doubletons nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" sep_set_lems nil)) nil)) (separates_comm 0 (separates_comm-1 nil 3251049123 ("" (skosimp*) (("" (expand "separates") (("" (iff 1) (("" (ground) (("1" (skosimp*) (("1" (lemma "walk?_reverse") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst 3 "w!2") nil))))) ("2" (expand "walk_from?") (("2" (flatten) (("2" (propax) nil))))))))))) ("2" (skosimp*) (("2" (lemma "walk?_reverse") (("2" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst 3 "w!2") nil))))) ("2" (expand "walk_from?") (("2" (flatten) (("2" (propax) nil)))))))))))))))))) nil) ((separates const-decl "bool" sep_sets nil) (T formal-type-decl nil sep_set_lems nil) (walk?_reverse formula-decl nil walks nil) (walk? const-decl "bool" walks nil) (Walk type-eq-decl nil walks nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (del_verts const-decl "graph[T]" sep_sets 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)) nil)) (sep_num_comm 0 (sep_num_comm-1 nil 3251049123 ("" (skosimp*) (("" (case "separable?(G!1,s!1,t!1)") (("1" (lemma "min_sep_set_seps") (("1" (inst?) (("1" (lemma "min_sep_set_seps") (("1" (inst -1 "G!1" "t!1" "s!1") (("1" (lemma "separable?_comm") (("1" (inst?) (("1" (assert) (("1" (expand "sep_num") (("1" (lemma "min_sep_set_card") (("1" (inst -1 "G!1" "min_sep_set(G!1, t!1, s!1)" "s!1" "t!1") (("1" (lemma "min_sep_set_card") (("1" (inst -1 "G!1" "min_sep_set(G!1, s!1, t!1)" "t!1" "s!1") (("1" (split -1) (("1" (split -2) (("1" (assert) nil) ("2" (rewrite "separates_comm") nil))) ("2" (rewrite "separates_comm") nil))))))))))))))))))))))))))) ("2" (expand "sep_num") (("2" (lemma "min_sep_set_edge") (("2" (copy -1) (("2" (inst?) (("2" (inst -2 "G!1" "t!1" "s!1") (("2" (lemma "separable?_comm") (("2" (inst?) (("2" (assert) nil)))))))))))))))))) nil) ((separable? const-decl "bool" sep_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 sep_set_lems nil) (sep_num const-decl "nat" sep_sets nil) (min_sep_set const-decl "finite_set[T]" sep_sets nil) (is_finite const-decl "bool" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (separates_comm formula-decl nil sep_set_lems nil) (min_sep_set_card formula-decl nil sep_sets nil) (separable?_comm formula-decl nil sep_set_lems nil) (min_sep_set_seps formula-decl nil sep_sets nil) (min_sep_set_edge formula-decl nil sep_sets nil)) nil)) (v_not_in 0 (v_not_in-1 nil 3251049123 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (assert) (("" (hide -1 -2) (("" (expand "walk?") (("" (flatten) (("" (split 2) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "remove") (("1" (expand "member") (("1" (inst?) (("1" (flatten) (("1" (assert) (("1" (expand "verts_of") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (assert) nil))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (hide -2) (("2" (expand "del_verts") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (expand "dbl") (("2" (expand "remove") (("2" (expand "member") (("2" (inst -5 "v!2") (("2" (assert) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (split -3) (("1" (inst?) (("1" (assert) nil))) ("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) nil) ((walk_from? const-decl "bool" walks nil) (finite_remove application-judgement "finite_set" finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (del_verts const-decl "graph[T]" sep_sets nil) (remove const-decl "set" sets nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil sep_set_lems nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_of const-decl "finite_set[T]" walks nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (dbl const-decl "set[T]" doubletons nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" sep_set_lems nil)) nil)) (path_thru_each 0 (path_thru_each-1 nil 3251049123 ("" (skosimp*) (("" (case "separates(G!1, remove(v!1,W!1) , s!1, t!1)") (("1" (hide 1) (("1" (lemma "min_sep_set_card") (("1" (inst?) (("1" (assert) (("1" (expand "sep_num") (("1" (replace -3) (("1" (hide -3) (("1" (hide -2 -3 -5 -6 -7) (("1" (rewrite "card_remove") (("1" (assert) nil))))))))))))))))))) ("2" (expand "separates") (("2" (flatten) (("2" (split 1) (("1" (expand "remove") (("1" (expand "member") (("1" (flatten) (("1" (propax) nil))))))) ("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (propax) nil))))))) ("3" (skosimp*) (("3" (case "verts_of(w!1)(v!1)") (("1" (hide 3) (("1" (lemma "walk_to_path_from") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst 3 "p!1") (("1" (lemma "path?_del_verts") (("1" (inst?) (("1" (inst?) (("1" (expand "path_from?") (("1" (flatten) (("1" (assert) (("1" (reveal 2) (("1" (inst 1 "p!1") (("1" (hide -1 -6 -7 -8 -10 2 3) (("1" (expand "path?") (("1" (flatten) (("1" (hide -2) (("1" (lemma "v_not_in") (("1" (hide -5) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (hide 2 3) (("1" (expand "walk_from?") (("1" (expand "from?") (("1" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (hide 5) (("2" (inst + "w!1") (("2" (hide -2 -3 -5 -6 2 3) (("2" (lemma "v_not_in") (("2" (inst?) (("2" (assert) nil)))))))))))))))))))))))) nil) ((remove const-decl "set" sets nil) (separates const-decl "bool" sep_sets 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 sep_set_lems nil) (finite_remove application-judgement "finite_set" finite_sets nil) (min_sep_set_card formula-decl nil sep_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (card_remove formula-decl nil finite_sets nil) (sep_num const-decl "nat" sep_sets nil) (t!1 skolem-const-decl "T" sep_set_lems nil) (s!1 skolem-const-decl "T" sep_set_lems nil) (G!1 skolem-const-decl "graph[T]" sep_set_lems nil) (del_verts const-decl "graph[T]" sep_sets nil) (path?_del_verts formula-decl nil path_ops nil) (v_not_in formula-decl nil sep_set_lems nil) (walk_from? const-decl "bool" walks nil) (from? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (path_from? const-decl "bool" paths nil) (walk_to_path_from formula-decl nil path_ops nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (verts_of const-decl "finite_set[T]" walks nil) (member const-decl "bool" sets nil)) nil)) (one_to_each 0 (one_to_each-1 nil 3251049123 ("" (skosimp*) (("" (lemma "path_thru_each") (("" (inst?) (("" (case "w1!1 = w2!1") (("1" (hide -2 1) (("1" (expand "sep_num") (("1" (lemma "min_sep_set_card") (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (hide -3) (("1" (case-replace "dbl(w1!1, w2!1) = singleton(w1!1)") (("1" (rewrite "card_singleton") (("1" (assert) nil))) ("2" (apply-extensionality 1 :hide? t) (("2" (hide -1 -3 -4 -5) (("2" (expand "dbl") (("2" (expand "singleton") (("2" (iff 1) (("2" (ground) nil))))))))))))))))))))))))))) ("2" (case "card(dbl(w1!1,w2!1)) = 2") (("1" (split 2) (("1" (inst - "dbl(w1!1, w2!1)" "w1!1") (("1" (assert) (("1" (expand "dbl" -2) (("1" (skosimp*) (("1" (expand "verts_of") (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (inst + "pv!1^(0,i!1)") (("1" (expand "path_from?") (("1" (expand "from?") (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (rewrite "path?_caret") nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil))) ("3" (expand* "^" min empty_seq) (("3" (propax) nil))))))))))))) ("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))))))))))))) ("2" (rewrite "finite_dbl") nil))) ("2" (inst - "dbl(w1!1, w2!1)" "w2!1") (("1" (assert) (("1" (expand "dbl" -2) (("1" (skosimp*) (("1" (expand "verts_of") (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (inst + "pv!1^(0,i!1)") (("1" (expand "path_from?") (("1" (expand "from?") (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (rewrite "path?_caret") nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil))) ("3" (expand* "^" min empty_seq) (("3" (propax) nil))))))))))))) ("2" (expand* "^" min empty_seq) (("2" (assert) nil))))))))))))))))) ("2" (rewrite "finite_dbl") nil))))) ("2" (hide -1 -2 -3 -4 -5 3) (("2" (rewrite "card_dbl") nil))) ("3" (rewrite "finite_dbl") nil)))))))))) nil) ((path_thru_each formula-decl nil sep_set_lems nil) (sep_num const-decl "nat" sep_sets nil) (nil application-judgement "finite_set[T]" sep_set_lems nil) (G!1 skolem-const-decl "graph[T]" sep_set_lems nil) (s!1 skolem-const-decl "T" sep_set_lems nil) (t!1 skolem-const-decl "T" sep_set_lems nil) (is_finite const-decl "bool" finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (card_singleton formula-decl nil finite_sets nil) (min_sep_set_card formula-decl nil sep_sets nil) (card_dbl formula-decl nil doubletons nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (prewalk type-eq-decl nil walks nil) (pv!1 skolem-const-decl "prewalk[T]" sep_set_lems nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(pv!1))" sep_set_lems nil) (from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (path?_caret formula-decl nil paths nil) (path_from? const-decl "bool" paths nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_of const-decl "finite_set[T]" walks nil) (pv!1 skolem-const-decl "prewalk[T]" sep_set_lems nil) (i!1 skolem-const-decl "below(length(pv!1))" sep_set_lems 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) (number nonempty-type-decl nil numbers 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 sep_set_lems nil)) nil)) (walk?_del_verts 0 (walk?_del_verts-1 nil 3251049123 ("" (skosimp*) (("" (expand "walk?") (("" (split +) (("1" (flatten) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (assert) nil))))))))))))))))) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (assert) (("2" (hide -2) (("2" (expand "edge?") (("2" (flatten) (("2" (assert) (("2" (expand "del_verts") (("2" (propax) nil)))))))))))))))))))))))) nil) ((walk? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" sep_set_lems nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (verts_in? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil sep_set_lems nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (difference const-decl "set" sets nil) (member const-decl "bool" sets nil) (del_verts const-decl "graph[T]" sep_sets nil)) nil)) (del_verts_eq 0 (del_verts_eq-1 nil 3251049123 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (apply-extensionality 1 :hide? t) (("1" (iff 1) (("1" (expand "del_vert") (("1" (expand "del_verts") (("1" (ground) (("1" (skosimp*) (("1" (expand "dbl") (("1" (ground) nil))))) ("2" (inst?) (("2" (expand "dbl") (("2" (propax) nil))))) ("3" (inst?) (("3" (expand "dbl") (("3" (propax) nil))))))))))))))) ("2" (apply-extensionality 1 :hide? t) (("2" (expand "del_vert") (("2" (expand "remove") (("2" (expand "member") (("2" (iff 1) (("2" (expand "del_verts") (("2" (expand "difference") (("2" (expand "member") (("2" (expand "dbl") (("2" (ground) nil)))))))))))))))))))))) nil) ((T formal-type-decl nil sep_set_lems nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (del_verts const-decl "graph[T]" sep_sets nil) (is_finite const-decl "bool" finite_sets nil) (del_vert const-decl "graph[T]" graph_ops nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" sep_set_lems nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil) (remove const-decl "set" sets nil)) nil))) ¤ Dauer der Verarbeitung: 0.33 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28