| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 7 MB |
|
Impressum k_menger.prf Sprache: Lisp |
|||||||||||||||
|
(k_menger (sep_num_B 0 (sep_num_B-1 nil 3375303932 ("" (skosimp*) (("" (expand "B") (("" (prop) (("" (copy -1) (("" (inst -3 "min_sep_set(G!1,s!1,t!1)") (("" (expand "sep_num") (("" (lemma "min_sep_set_card") (("" (inst?) (("1" (bddsimp) (("1" (lemma "min_sep_set_seps") (("1" (inst?) (("1" (prop) (("1" (expand "good?") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "good?") (("2" (bddsimp) nil nil)) nil) ("3" (expand "good?") (("3" (bddsimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((B const-decl "bool" k_menger nil) (sep_num const-decl "nat" sep_sets nil) (G!1 skolem-const-decl "graph[T]" k_menger nil) (s!1 skolem-const-decl "T" k_menger nil) (t!1 skolem-const-decl "T" k_menger nil) (min_sep_set_seps formula-decl nil sep_sets nil) (good? const-decl "bool" k_menger nil) (min_sep_set_card formula-decl nil sep_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) (T formal-type-decl nil k_menger nil)) shostak)) (sep_num_implies 0 (sep_num_implies-1 nil 3379680344 ("" (skosimp*) (("" (expand "B") (("" (prop) (("" (skosimp*) (("" (lemma "min_sep_set_card") (("" (inst?) (("1" (expand "sep_num") (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "good?") (("2" (prop) nil nil)) nil) ("3" (expand "good?") (("3" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((B const-decl "bool" k_menger nil) (s!1 skolem-const-decl "T" k_menger nil) (G!1 skolem-const-decl "graph[T]" k_menger 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!1 skolem-const-decl "T" k_menger nil) (is_finite const-decl "bool" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sep_num const-decl "nat" sep_sets nil) (good? const-decl "bool" k_menger nil) (min_sep_set_card formula-decl nil sep_sets nil) (T formal-type-decl nil k_menger nil)) shostak)) (card_extension_W 0 (card_extension_W-1 nil 3389097760 ("" (skosimp*) (("" (lemma "card_extension[T,(W!1)]") (("" (inst -1 "V!1") (("" (expand "restrict") (("" (expand "extend") (("" (case "(LAMBDA (t: T): IF (W!1)(t) THEN V!1(t) ELSE FALSE ENDIF)=V!1") (("1" (replace -1 1 lr) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (iff) (("2" (prop) (("2" (expand "subset?") (("2" (inst? -3) (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (T formal-type-decl nil k_menger nil) (card_extension formula-decl nil finite_sets_card_from nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (FALSE const-decl "bool" booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (restrict const-decl "R" restrict nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil)) shostak)) (card_extension_same 0 (card_extension_same-1 nil 3389098779 ("" (skosimp*) (("" (lemma "card_extension_W") (("" (inst -1 "W!1" "W!1") (("" (prop) (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((card_extension_W formula-decl nil k_menger nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets 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) (T formal-type-decl nil k_menger nil)) shostak)) (easy_menger_B 0 (easy_menger_B-2 "sec" 3379689668 ("" (skosimp*) (("" (lemma "easy_menger[T]") (("" (expand "many_ind") (("" (skosimp*) (("" (inst -1 "G!1" "s!1" "t!1" "ips!1") (("" (expand "B") (("" (prop) (("1" (expand "st_path_set?") (("1" (lemma "finite_sets_card_eq[prewalk,Path_from[T](G!1, s!1, t!1)].card_eq_bij") (("1" (expand "restrict") (("1" (inst -1 "ips!1" "LAMBDA (s: Path_from[T](G!1, s!1, t!1)): ips!1(s)") (("1" (prop) (("1" (replace -1 -3 rl) (("1" (replace -7 -3 lr) (("1" (lemma "min_sep_set_card") (("1" (skosimp*) (("1" (inst?) (("1" (expand "sep_num") (("1" (prop) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "good?") (("2" (prop) nil nil)) nil) ("3" (expand "good?") (("3" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 -5 2 3) (("2" (inst 1 "LAMBDA (p1:(ips!1)) :p1") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -3 -5 2) (("2" (typepred "ips!1") (("2" (lemma "restrict_set_props[prewalk,Path_from[T](G!1, s!1, t!1)].restrict_finite") (("2" (inst -1 "ips!1") (("2" (prop) (("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "good?") (("2" (prop) nil nil)) nil) ("3" (hide -4 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil k_menger nil) (easy_menger formula-decl nil easy_menger nil) (B const-decl "bool" k_menger nil) (ind_prewalk_set? const-decl "bool" k_menger nil) (ind_path_set? const-decl "bool" ind_paths nil) (independent? const-decl "bool" ind_paths nil) (st_path_set? const-decl "bool" k_menger nil) (restrict_finite formula-decl nil restrict_set_props nil) (good? const-decl "bool" k_menger nil) (sep_num const-decl "nat" sep_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_sep_set_card formula-decl nil sep_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (from? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil) (separable? const-decl "bool" sep_sets nil) (edge? const-decl "bool" graphs nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (nil application-judgement "finite_set[T]" k_menger nil) (nil application-judgement "finite_set[T]" graphs nil) (ips!1 skolem-const-decl "set_of_prewalks" k_menger nil) (t!1 skolem-const-decl "T" k_menger nil) (s!1 skolem-const-decl "T" k_menger nil) (G!1 skolem-const-decl "graph[T]" k_menger nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (set_of_prewalks type-eq-decl nil k_menger nil) (restrict const-decl "R" restrict nil) (set_of_paths type-eq-decl nil ind_paths nil) (is_finite const-decl "bool" finite_sets nil) (Path_from type-eq-decl nil paths nil) (path_from? const-decl "bool" paths 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) (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) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (many_ind const-decl "bool" k_menger nil)) shostak) (easy_menger_B-1 nil 3379687287 ("" (skosimp*) (("" (lemma "easy_menger") (("" (expand "many_ind") (("" (skosimp*) (("" (inst -1 "G!1" "s!1" "t!1" "ips!1") (("" (prop) (("1" (expand "B") (("1" (prop) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sep_set_small 0 (sep_set_small-1 nil 3379682439 ("" (skosimp*) (("" (expand "B") (("" (prop) (("" (inst?) (("" (prop) (("1" (assert) nil nil) ("2" (expand "separates") (("2" (expand "green?") (("2" (prop) (("2" (skosimp*) (("2" (lemma "walk_to_path") (("2" (inst -1 "del_verts(G!1,V!1)" "s!1" "t!1") (("2" (prop) (("1" (skosimp*) (("1" (hide -3 -4 -5) (("1" (expand "walk_from?") (("1" (prop) (("1" (inst 3 "p!1") (("1" (expand "path_from?") (("1" (prop) (("1" (expand "from?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -3 4) (("2" (inst 1 "w!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((B const-decl "bool" k_menger nil) (T formal-type-decl nil k_menger 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) (separates const-decl "bool" sep_sets nil) (walk_to_path formula-decl nil path_ops nil) (path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers 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) (walk_from? const-decl "bool" walks nil) (del_verts const-decl "graph[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) (green? const-decl "bool" k_menger nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (B_many_1 0 (B_many_1-1 nil 3379681920 ("" (skosimp*) (("" (expand "B_many") (("" (prop) (("" (expand "many_ind") (("" (lemma "sep_set_small") (("" (expand "B") (("" (prop) (("" (inst -1 "G!1" "_" "1" "s!1" "t!1") (("" (inst -1 "emptyset[T]") (("" (prop) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (assert) (("1" (expand "emptyset") (("1" (skosimp*) (("1" (inst 1 "singleton[prewalk](p!1)") (("1" (hide -2 -3) (("1" (lemma "card_singleton[prewalk]") (("1" (inst -1 "p!1") (("1" (prop) (("1" (expand "ind_prewalk_set?") (("1" (skosimp*) (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "st_path_set?") (("2" (hide -1) (("2" (skosimp*) (("2" (expand "singleton") (("2" (replace -1 * lr) (("2" (install-rewrites "paths") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (lemma "card_emptyset[T]") (("2" (assert) (("2" (expand "green?") (("2" (prop) (("1" (assert) (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "card_emptyset[T]") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((B_many const-decl "bool" k_menger nil) (many_ind const-decl "bool" k_menger nil) (B const-decl "bool" k_menger nil) (T formal-type-decl nil k_menger 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) (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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (difference const-decl "set" sets nil) (st_path_set? const-decl "bool" k_menger nil) (path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" k_menger nil) (ind_prewalk_set? const-decl "bool" k_menger nil) (card_singleton formula-decl nil finite_sets 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) (set_of_prewalks type-eq-decl nil k_menger nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (member const-decl "bool" sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (card_emptyset formula-decl nil finite_sets nil) (green? const-decl "bool" k_menger nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (is_finite const-decl "bool" finite_sets nil) (emptyset const-decl "set" sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" k_menger nil) (sep_set_small formula-decl nil k_menger nil)) shostak)) (sub_tight 0 (sub_tight-1 nil 3379015166 ("" (skosimp*) (("" (expand "tight?") (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (inst -1 "x!1") (("" (inst -2 "x!1") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tight? const-decl "bool" k_menger nil) (T formal-type-decl nil k_menger nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) shostak)) (smaller_tight 0 (smaller_tight-3 "good" 3378204176 ("" (skosimp*) (("" (expand "tight?") (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "intersection") (("" (expand "member") (("" (inst 2 "remove(x!1,W!1)") (("" (prop) (("1" (skosimp*) (("1" (expand "remove") (("1" (prop) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (hide -2 1) (("2" (grind) (("2" (decompose-equality -1) (("2" (inst -1 "x!1") (("2" (iff) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "separates") (("3" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "walk_from?") (("3" (prop) (("3" (inst 4 "w!1") (("3" (prop) (("3" (case "verts_of(w!1)(x!1)") (("1" (hide -4) (("1" (hide 1) (("1" (expand "path_verts") (("1" (expand "verts_of") (("1" (skosimp*) (("1" (expand "finseq_appl") (("1" (inst 1 "w!1^(0,i!1)") (("1" (expand "walk_from?") (("1" (prop) (("1" (expand* "^" min empty_seq) nil nil) ("2" (expand* "^" min empty_seq) nil nil) ("3" (reveal -1) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "i!1" "w!1") (("3" (typepred "i!1") (("3" (assert) (("3" (lemma "walk?_subgraph") (("3" (inst -1 "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1") (("3" (prop) (("3" (hide -2 2 3) (("3" (assert) (("3" (install-rewrites "finite_sets[T]") (("3" (assert) (("3" (prop) (("1" (skosimp*) nil nil) ("2" (skosimp*) 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) ("2" (hide 3) (("2" (install-rewrites "walks") (("2" (expand "walk?") (("2" (expand "finseq_appl") (("2" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (typepred "i!1") (("1" (hide -5) (("1" (inst -4 "i!1") (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (expand "difference") (("1" (expand "member") (("1" (prop) (("1" (inst 1 "i!1") (("1" (expand "remove") (("1" (expand "member") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -5 "n!1") (("2" (prop) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (prop) (("2" (hide -5) (("2" (expand "del_verts") (("2" (prop) (("2" (skosimp*) (("2" (copy -4) (("2" (inst -1 "seq(w!1)(n!1)") (("2" (inst -5 "seq(w!1)(n!1 + 1)") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (inst 3 "1+n!1") (("4" (assert) nil nil)) nil)) nil) ("5" (inst 3 "n!1") (("5" (assert) nil nil)) nil) ("6" (inst 3 "n!1") (("6" (assert) nil nil)) nil) ("7" (replace -1 -2 lr) (("7" (propax) nil nil)) nil) ("8" (replace -1 -2 lr) (("8" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) 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)) nil) ("4" (skosimp*) (("4" (hide -2 2) (("4" (expand "remove") (("4" (expand "member") (("4" (prop) nil nil)) nil)) nil)) nil)) nil) ("5" (hide -2 1) (("5" (expand "remove") (("5" (decompose-equality -1) (("5" (inst?) (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "separates") (("6" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "walk_from?") (("3" (prop) (("3" (inst 4 "w!1") (("3" (prop) (("3" (case "verts_of(w!1)(x!1)") (("1" (hide -4) (("1" (hide 1) (("1" (expand "path_verts") (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (skosimp*) (("1" (inst 1 "rev(w!1)^(0,length(w!1)-1-i!1)") (("1" (expand "walk_from?") (("1" (prop) (("1" (expand "rev") (("1" (expand* "^" min empty_seq) nil nil)) nil) ("2" (expand "rev") (("2" (expand* "^" min empty_seq) nil nil)) nil) ("3" (reveal -1) (("3" (lemma "walk?_caret") (("3" (lemma "walk?_rev") (("3" (inst -1 "G!1" "w!1") (("3" (inst -2 "G!1" "0" "length(w!1)-1-i!1" "rev(w!1)") (("1" (typepred "i!1") (("1" (assert) (("1" (lemma "walk?_subgraph") (("1" (inst -1 "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1") (("1" (prop) (("1" (lemma "walk?_caret") (("1" (inst -1 "G!1" "0" "length(w!1)-1-i!1" "rev(w!1)") (("1" (assert) (("1" (expand "rev") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "rev") (("2" (assert) nil nil)) nil) ("3" (expand "rev") (("3" (assert) nil nil)) nil) ("4" (hide -2 1 2 4) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rev") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rev") (("2" (expand* "^" min empty_seq) (("2" (typepred "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (install-rewrites "walks") (("2" (expand "walk?") (("2" (expand "finseq_appl") (("2" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (typepred "i!1") (("1" (hide -5) (("1" (inst -4 "i!1") (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (expand "difference") (("1" (expand "member") (("1" (prop) (("1" (inst 1 "i!1") (("1" (expand "remove") (("1" (expand "member") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -5 "n!1") (("2" (prop) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (prop) (("2" (hide -5) (("2" (expand "del_verts") (("2" (prop) (("2" (skosimp*) (("2" (copy -4) (("2" (inst -1 "seq(w!1)(n!1)") (("2" (inst -5 "seq(w!1)(n!1 + 1)") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (inst 3 "1+n!1") (("4" (assert) nil nil)) nil)) nil) ("5" (inst 3 "n!1") (("5" (assert) nil nil)) nil) ("6" (inst 3 "n!1") (("6" (assert) nil nil)) nil) ("7" (replace -1 -2 lr) (("7" (propax) nil nil)) nil) ("8" (replace -1 -2 lr) (("8" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tight? const-decl "bool" k_menger nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (finite_remove application-judgement "finite_set[T]" k_menger nil) (T formal-type-decl nil k_menger 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) (remove const-decl "set" sets nil) (n!1 skolem-const-decl "nat" k_menger nil) (rev const-decl "finseq[T]" doubletons nil) (w!1 skolem-const-decl "prewalk[T]" k_menger nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "below(length(w!1))" k_menger nil) (walk?_rev formula-decl nil walks nil) (separates const-decl "bool" sep_sets nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" k_menger nil) (edge? const-decl "bool" graphs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (n!1 skolem-const-decl "nat" k_menger nil) (path_verts const-decl "set[T]" paths nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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 "finseq" finite_sequences nil) (w!1 skolem-const-decl "prewalk[T]" k_menger nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(w!1))" k_menger nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (walk?_caret formula-decl nil walks nil) (walk?_subgraph formula-decl nil subgraph_paths nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_difference application-judgement "finite_set[T]" k_menger nil) (difference const-decl "set" sets nil) (subgraph? const-decl "bool" subgraphs nil) (del_verts const-decl "graph[T]" sep_sets 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_of const-decl "finite_set[T]" 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) (walk_from? const-decl "bool" walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (subset? const-decl "bool" sets nil)) shostak) (smaller_tight-2 "sec" 3378155661 ("" (skosimp*) (("" (expand "tight?") (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "intersection") (("" (expand "member") (("" (inst 2 "remove(x!1,W!1)") (("" (prop) (("1" (skosimp*) (("1" (expand "remove") (("1" (prop) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (hide -2 1) (("2" (grind) (("2" (decompose-equality -1) (("2" (inst -1 "x!1") (("2" (iff) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "separates") (("3" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "walk_from?") (("3" (prop) (("3" (inst 4 "w!1") (("3" (prop) (("3" (case "verts_of(w!1)(x!1)") (("1" (hide -4) (("1" (hide 1) (("1" (expand "path_verts") (("1" (expand "verts_of") (("1" (skosimp*) (("1" (inst 1 "w!1^(0,i!1)") (("1" (expand "walk_from?") (("1" (prop) (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil nil)) nil) ("3" (reveal -1) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "i!1" "w!1") (("3" (typepred "i!1") (("3" (assert) (("3" (lemma "walk?_subgraph") (("3" (inst -1 "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1") (("3" (prop) (("3" (hide -2 2 3) (("3" (assert) (("3" (install-rewrites "finite_sets[T]") (("3" (assert) (("3" (prop) (("1" (skosimp*) nil nil) ("2" (skosimp*) 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) ("2" (hide 3) (("2" (install-rewrites "walks") (("2" (expand "walk?") (("2" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (typepred "i!1") (("1" (hide -5) (("1" (inst -4 "i!1") (("1" (expand "verts_of") (("1" (expand "difference") (("1" (expand "member") (("1" (prop) (("1" (inst 1 "i!1") (("1" (expand "remove") (("1" (expand "member") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -5 "n!1") (("2" (prop) (("2" (expand "verts_of") (("2" (expand "edge?") (("2" (prop) (("2" (hide -5) (("2" (expand "del_verts") (("2" (prop) (("2" (skosimp*) (("2" (copy -4) (("2" (inst -1 "seq(w!1)(n!1)") (("2" (inst -5 "seq(w!1)(n!1 + 1)") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (inst 3 "1+n!1") (("4" (assert) nil nil)) nil)) nil) ("5" (inst 3 "n!1") (("5" (assert) nil nil)) nil) ("6" (inst 3 "n!1") (("6" (assert) nil nil)) nil) ("7" (replace -1 -2 lr) (("7" (propax) nil nil)) nil) ("8" (replace -1 -2 lr) (("8" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) 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) ("4" (skosimp*) (("4" (hide -2 2) (("4" (expand "remove") (("4" (expand "member") (("4" (prop) nil nil)) nil)) nil)) nil)) nil) ("5" (hide -2 1) (("5" (expand "remove") (("5" (decompose-equality -1) (("5" (inst?) (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "separates") (("6" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "walk_from?") (("3" (prop) (("3" (inst 4 "w!1") (("3" (prop) (("3" (case "verts_of(w!1)(x!1)") (("1" (hide -4) (("1" (hide 1) (("1" (expand "path_verts") (("1" (expand "verts_of") (("1" (skosimp*) (("1" (inst 1 "rev(w!1)^(0,length(w!1)-1-i!1)") (("1" (expand "walk_from?") (("1" (prop) (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "rev") (("2" (expand* "^" min empty_seq) (("2" (propax) nil nil)) nil)) nil) ("3" (reveal -1) (("3" (lemma "walk?_caret") (("3" (lemma "walk?_rev") (("3" (inst -1 "G!1" "w!1") (("3" (inst -2 "G!1" "0" "length(w!1)-1-i!1" "rev(w!1)") (("1" (typepred "i!1") (("1" (assert) (("1" (typepred "w!1") (("1" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk?_rev formula-decl nil walks nil) (separates const-decl "bool" sep_sets nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (verts_in? const-decl "bool" walks nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (del_verts const-decl "graph[T]" sep_sets nil) (subgraph? const-decl "bool" subgraphs nil) (walk?_caret formula-decl nil walks nil) (verts_of const-decl "finite_set[T]" walks nil) (prewalk type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil)) shostak) (smaller_tight-1 nil 3378121587 ("" (skosimp*) (("" (expand "tight?") (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "intersection") (("" (expand "member") (("" (inst 2 "remove(x!1,W!1)") (("" (prop) (("1" (skosimp*) (("1" (expand "remove") (("1" (prop) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (hide -2 1) (("2" (grind) (("2" (decompose-equality -1) (("2" (inst -1 "x!1") (("2" (iff) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "separates") (("3" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "walk_from?") (("3" (prop) (("3" (inst 4 "w!1") (("3" (prop) (("3" (case "verts_of(w!1)(x!1)") (("1" (hide -4) (("1" (hide 1) (("1" (expand "path_verts") (("1" (expand "verts_of") (("1" (skosimp*) (("1" (inst 1 "w!1^(0,i!1)") (("1" (expand "walk_from?") (("1" (prop) (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil nil)) nil) ("3" (reveal -1) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "0" "i!1" "w!1") (("3" (typepred "i!1") (("3" (assert) (("3" (lemma "walk?_subgraph") (("3" (inst -1 "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1") (("3" (prop) (("3" (hide -2 2 3) (("3" (assert) (("3" (install-rewrites "finite_sets[T]") (("3" (assert) (("3" (prop) (("1" (skosimp*) nil nil) ("2" (skosimp*) 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) ("2" (hide 3) (("2" (install-rewrites "walks") (("2" (expand "walk?") (("2" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (typepred "i!1") (("1" (hide -5) (("1" (inst -4 "i!1") (("1" (expand "verts_of") (("1" (expand "difference") (("1" (expand "member") (("1" (prop) (("1" (inst 1 "i!1") (("1" (expand "remove") (("1" (expand "member") (("1" (prop) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -5 "n!1") (("2" (prop) (("2" (expand "verts_of") (("2" (expand "edge?") (("2" (prop) (("2" (hide -5) (("2" (expand "del_verts") (("2" (prop) (("2" (skosimp*) (("2" (copy -4) (("2" (inst -1 "seq(w!1)(n!1)") (("2" (inst -5 "seq(w!1)(n!1 + 1)") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (assert) (("4" (inst 3 "1+n!1") (("4" (assert) nil nil)) nil)) nil) ("5" (inst 3 "n!1") (("5" (assert) nil nil)) nil) ("6" (inst 3 "n!1") (("6" (assert) nil nil)) nil) ("7" (replace -1 -2 lr) (("7" (propax) nil nil)) nil) ("8" (replace -1 -2 lr) (("8" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (grind) 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) ("4" (skosimp*) (("4" (hide -2 2) (("4" (expand "remove") (("4" (expand "member") (("4" (prop) nil nil)) nil)) nil)) nil)) nil) ("5" (hide -2 1) (("5" (expand "remove") (("5" (decompose-equality -1) (("5" (inst?) (("5" (expand "member") (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (small_tight 0 (small_tight-1 nil 3378206435 ("" (lemma "finite_set_induction_gen") (("" (skosimp*) (("" (inst -1 "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1 (("" (prop) (("1" (inst -1 "W!1") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "smaller_tight") (("2" (inst -1 "G!1" "S!1" "s!1" "t!1") (("2" (hide -4 2) (("2" (prop) (("1" (inst 1 "S!1") (("1" (hide -2) (("1" (prop) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "card(V!1)<card(S!1)") (("1" (inst -4 "V!1") (("1" (prop) (("1" (skosimp*) (("1" (inst 2 "V1!1") (("1" (prop) (("1" (hide-all-but (-1 -5 1)) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1 2)) (("2" (lemma "same_card_subset") (("2" (inst -1 "V!1" "S!1") (("2" (prop) (("2" (lemma "card_subset") (("2" (inst -1 "V!1" "S!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((smaller_tight formula-decl nil k_menger nil) (card_subset formula-decl nil finite_sets nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (same_card_subset formula-decl nil finite_sets 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (nil application-judgement "finite_set[T]" graphs nil) (nil application-judgement "finite_set[T]" k_menger nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (path_verts const-decl "set[T]" paths nil) (intersection const-decl "set" sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (difference const-decl "set" sets nil) (tight? const-decl "bool" k_menger nil) (subset? const-decl "bool" sets nil) (separates const-decl "bool" sep_sets nil) (graph type-eq-decl nil graphs 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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) (finite_set_induction_gen formula-decl nil finite_sets_inductions "finite_sets/") (T formal-type-decl nil k_menger nil)) shostak)) (exists_tight 0 (exists_tight-2 nil 3378222865 ("" (skosimp*) (("" (expand "good?") (("" (expand "separable?") (("" (prop) (("" (lemma "small_tight") (("" (inst?) (("" (inst -1 "{t: T | vert(G!1)(t) AND t /= s!1 AND t /= t!1}" "s!1" "t!1") (("1" (prop) (("1" (skosimp*) (("1" (inst 3 "V!1") (("1" (prop) nil nil)) nil)) nil) ("2" (hide 4) (("2" (expand "separates") (("2" (skosimp*) (("2" (expand "walk_from?") (("2" (flatten) (("2" (case "length(w!1) = 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case-replace "length(w!1) = 2") (("1" (assert) (("1" (expand "walk?") (("1" (expand "finseq_appl") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (hide -4) (("1" (replace -2 * lr) (("1" (replace -3 * lr) (("1" (hide 1) (("1" (expand "edge?") (("1" (expand "del_verts") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (i: below(length(w!1))): seq(w!1)(i) = s!1 OR seq(w!1)(i) = t!1") (("1" (expand "walk?") (("1" (expand "finseq_appl") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (expand "edge?") (("1" (expand "del_verts") (("1" (flatten) (("1" (inst -1 "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walk_verts_in") (("2" (inst?) (("1" (split -1) (("1" (hide -4) (("1" (expand "verts_in?") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (skosimp*) (("1" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide -1 -2 -3 2 3 4 5 6) (("2" (lemma "finite_subset[T]") (("2" (inst?) (("2" (inst -1 "vert(G!1)") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3 4) (("2" (lemma "finite_subset[T]") (("2" (inst?) (("2" (inst -1 "vert(G!1)") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((good? const-decl "bool" k_menger nil) (T formal-type-decl nil k_menger 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) (separates const-decl "bool" sep_sets nil) (walk_from? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers 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_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) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (finite_difference application-judgement "finite_set[T]" k_menger nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil) (verts_in? const-decl "bool" walks nil) (finite_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (walk_verts_in formula-decl nil walks nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (nil application-judgement "finite_set[T]" k_menger nil) (edge? const-decl "bool" graphs nil) (del_verts const-decl "graph[T]" sep_sets 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) (walk? const-decl "bool" walks nil) (is_finite const-decl "bool" finite_sets nil) (G!1 skolem-const-decl "graph[T]" k_menger nil) (s!1 skolem-const-decl "T" k_menger nil) (t!1 skolem-const-decl "T" k_menger nil) (small_tight formula-decl nil k_menger nil) (separable? const-decl "bool" sep_sets nil)) nil) (exists_tight-1 nil 3378222242 ("" (skosimp*) (("" (lemma "sep_set_exists") (("" (inst?) (("" (inst?) (("" (inst?) (("" (skosimp*) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (close_tight 0 (close_tight-1 nil 3378932482 ("" (skosimp*) (("" (install-rewrites "k_menger") (("" (expand "tight?") (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (expand "intersection") (("" (expand "member") (("" (prop) (("1" (expand "close?") (("1" (inst -1 "x!1") (("1" (prop) (("1" (skosimp*) (("1" (expand "intersection") (("1" (expand "member") (("1" (decompose-equality -2) (("1" (inst -1 "x!1") (("1" (iff) (("1" (expand "singleton") (("1" (prop) (("1" (expand "internal_verts") (("1" (expand "finseq_appl") (("1" (skosimp*) (("1" (expand "path_verts") (("1" (inst 1 "p!1^(0,i!1)") (("1" (expand* "^" min empty_seq) (("1" (expand "walk_from?") (("1" (prop) (("1" (install-rewrites "paths") (("1" (assert) nil nil)) nil) ("2" (expand "path_from?") (("2" (prop) (("2" (expand "path?") (("2" (expand "finseq_appl") (("2" (prop) (("2" (lemma "walk?_caret") (("2" (inst -1 "G!1" "0" "i!1" "p!1") (("2" (prop) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (assert) (("3" (prop) (("1" (skosimp) (("1" (inst?) nil nil)) nil) ("2" (skosimp) (("2" (inst -7 "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (install-rewrites "walks") (("2" (assert) (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "close?") (("2" (inst -1 "x!1") (("2" (prop) (("2" (skosimp*) (("2" (expand "intersection") (("2" (expand "member") (("2" (decompose-equality -2) (("2" (inst -1 "x!1") (("2" (iff) (("2" (expand "singleton") (("2" (prop) (("2" (expand "internal_verts") (("2" (expand "finseq_appl") (("2" (skosimp*) (("2" (expand "path_verts") (("2" (inst 1 "rev(p!1^(i!1,length(p!1)-1))") (("1" (expand* "^" min empty_seq) (("1" (expand "rev") (("1" (expand "walk_from?") (("1" (prop) (("1" (install-rewrites "walks") (("1" (assert) (("1" (prop) nil nil)) nil)) nil) ("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil) ("3" (install-rewrites "paths") (("3" (expand "path_from?") (("3" (prop) (("3" (expand "path?") (("3" (expand "finseq_appl") (("3" (prop) (("3" (lemma "walk?_caret") (("3" (inst -1 "G!1" "i!1" "length(p!1)-1" "p!1") (("3" (prop) (("1" (lemma "walk?_rev") (("1" (inst -1 "G!1" " p!1 ^ (i!1, length(p!1) - 1)") (("1" (hide -7 -8 -9) (("1" (prop) (("1" (hide -2) (("1" (expand "^") (("1" (expand "rev") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (install-rewrites "walks") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (empty_seq const-decl "finseq" finite_sequences nil) (walk?_rev formula-decl nil walks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" k_menger nil) (p!1 skolem-const-decl "prewalk[T]" k_menger nil) (rev const-decl "finseq[T]" doubletons nil) (close? const-decl "bool" k_menger nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" 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) (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) (internal_verts const-decl "finite_set[T]" ind_paths nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (walk_from? const-decl "bool" walks nil) (path_verts const-decl "set[T]" paths nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (nil application-judgement "finite_set[T]" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" k_menger 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) (walk?_caret formula-decl nil walks nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (i!1 skolem-const-decl "nat" k_menger nil) (p!1 skolem-const-decl "prewalk[T]" k_menger nil) (^ const-decl "finseq" finite_sequences 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil k_menger nil) (intersection const-decl "set" sets nil) (tight? const-decl "bool" k_menger nil)) shostak)) (smaller_close 0 (smaller_close-1 nil 3379013579 ("" (skosimp*) (("" (expand "close?") (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "intersection") (("" (expand "member") (("" (inst 2 "remove(w!1,W!1)") (("" (prop) (("1" (skosimp*) (("1" (expand "remove") (("1" (prop) (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (hide -2 1) (("2" (decompose-equality -1) (("2" (inst -1 "w!1") (("2" (iff) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "separates") (("3" (prop) (("1" (expand "remove") (("1" (expand "member") (("1" (prop) nil nil)) nil)) nil) ("2" (expand "remove") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide -2 3) (("3" (lemma "walk_to_path_from") (("3" (inst -1 "del_verts(G!1, remove(w!1, W!1))" "s!1" "t!1" "w!2") (("3" (prop) (("3" (skosimp*) (("3" (hide -2) (("3" (inst 3 "p!1") (("3" (lemma "path?_subgraph") (("3" (inst -1 "G!1" "del_verts(G!1, remove(w!1, W!1))" "p!1") (("3" (prop) (("1" (expand "path_from?") (("1" (prop) nil nil)) nil) ("2" (expand "path_from?") (("2" (prop) (("2" (hide -1 -3) (("2" (expand "path?") (("2" (expand "finseq_appl") (("2" (prop) (("2" (expand "internal_verts") (("2" (install-rewrites "walks") (("2" (expand "finseq_appl") (("2" (apply-extensionality 1 :hide? t) (("1" (iff) (("1" (prop) (("1" (skosimp*) (("1" (inst -5 "i!1") (("1" (rop work forjava.lang.StringIndexOutOfBoundsException: Index 57 out of bounds for len (inst -7 "i!1") (("1" (assert) nil nil) >.toolsaccessor/java.lang.StringIndexOutOfBoundsException: Range [59, 58) out of (inst -6 "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (reveal 2) (("3" (inst 1 "p!1") (("3" (expand "walk_from?") (("3" (prop) (("1" (reveal -3) (("1" (expand "from?") (("1" (prop) nil nil)) nil)) nil) ("2" (reveal -3) (("2" (expand "from?") (("2" (prop) nil nil)) nil)) nil) ("3" (expand "walk?") (("3" (expand "finseq_appl") (("3" (prop) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst -2 "i!1") (("1" (inst -3 "i!1") (("1" (prop) (("1" (typepred "i!1") (("1" (inst -3 "x!1") (("1" (assert) (("1" (prop) (("1" (reveal -6) (("1" (expand "from?") (("1" (prop) (("1" (inst 3 "i!1") (("1" (replace -6 * rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (reveal -5) (("2" (expand "from?") (("2" (prop) (("2" (case "i!1=length(p!1)-1") (("1" (replace -1 * lr) (("1" (replace -3 * lr) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 -5 1 4) (("3" (grind) nil nil)) nil) ("4" (hide -3 4) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -4 "n!1") (("2" (prop) (("2" (expand "edge?") (("2" (prop) (("2" (expand "del_verts") (("2" (prop) (("2" (skosimp*) (("2" (inst -4 "v!1") (("2" (prop) (("1" (hide -3 -6 -7 4) (("1" (assert) nil nil)) nil) ("2" (copy 2) (("2" (inst 1 "n!1") (("2" (inst 3 "n!1+1") (("2" (assert) (("2" (replace -1 * rl) (("2" (replace -6 * lr) (("2" (hide -4 -7 -8) (("2" (grind) (("1" (case "n!1+1=length(p!1)-1") (("1" (reveal -8) (("1" (expand "from?") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (reveal -8) (("2" (expand "from?") (("2" (propax) nil nil)) nil)) nil) ("3" (reveal -8) (("3" (expand "from?") (("3" (propax) nil nil)) nil)) nil) ("4" (reveal -8) (("4" (expand "from?") (("4" (propax) 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)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "path_from?") (("3" (lemma "path?_subgraph") (("3" (inst -1 "G!1" "del_verts(G!1, remove(w!1, W!1))" "p!1") (("3" (prop) (("3" (hide 3) (("3" (hide -1 -2 1) (("3" (install-rewrites "graphs") (("3" (assert) (("3" (prop) (("1" (skosimp*) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -1 1) (("4" (install-rewrites "graphs") (("4" (assert) (("4" (prop) (("1" (skosimp*) nil nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("5" (expand "path_from?") (("5" (prop) nil nil)) nil) ("6" (expand "path_from?") (("6" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "sub_tight") (("4" (inst -1 "G!1" "remove(w!1,W!1)" "W!1" "s!1" "t!1") (("4" (prop) (("4" (hide -1 -2 2) (("4" (install-rewrites "finite_sets") (("4" (assert) (("4" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((close? const-decl "bool" k_menger nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (finite_remove application-judgement "finite_set[T]" k_menger nil) (T formal-type-decl nil k_menger 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) (remove const-decl "set" sets nil) (sub_tight formula-decl nil k_menger nil) (separates const-decl "bool" sep_sets nil) (walk_to_path_from formula-decl nil path_ops nil) (path?_subgraph formula-decl nil subgraph_paths nil) (path_from? const-decl "bool" paths nil) (path? const-decl "bool" paths nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (p!1 skolem-const-decl "prewalk[T]" k_menger nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals 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) (W!1 skolem-const-decl "finite_set[T]" k_menger nil) (int_minus_int_is_int application-judgement "int" integers nil) (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (verts_in? const-decl "bool" walks nil) (difference const-decl "set" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (finite_difference application-judgement "finite_set[T]" k_menger nil) (nil application-judgement "finite_set[T]" k_menger nil) (below type-eq-decl nil naturalnumbers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (from? const-decl "bool" walks nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (walk_from? const-decl "bool" walks nil) (internal_verts const-decl "finite_set[T]" ind_paths nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (subgraph? const-decl "bool" subgraphs nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (subset? const-decl "bool" sets nil)) nil)) (small_close 0 (small_close-3 "variabl" 3379069981 ("" (lemma "finite_set_induction_gen") (("" (skosimp*) (("" (inst -1 "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1 (("" (prop) (("1" (inst -1 "W!1") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (hide -3 2) (("2" (lemma "smaller_close") (("2" (lemma "small_tight") (("2" (inst -1 "G!1" "S!1" "s!1" "t!1") (("2" (prop) (("2" (skosimp*) (("2" (inst -4 "G!1" "V!1" "s!1" "t!1") (("2" (prop) (("1" (inst 1 "V!1") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (inst -7 "V!2") (("2" (prop) (("1" (skosimp*) (("1" (inst 2 "V1!1") (("1" (prop) (("1" (hide-all-but (-1 -4 -7 1 2)) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -3 -5 -6 -7 3)) (("2" (lemma "same_card_subset") (("2" (lemma "card_subset") (("2" (copy -1) (("2" (copy -3) (("2" (inst -1 "V!2" "V!1") (("2" (inst -4 "V!1" "S!1") (("2" (inst -2 "V!2" "V!1") (("2" (inst -3 "V!1" "S!1") (("2" (prop) (("1" (replace -1 * lr) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((small_tight formula-decl nil k_menger nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (same_card_subset formula-decl nil finite_sets nil) (real_lt_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_subset formula-decl nil finite_sets nil) (smaller_close formula-decl nil k_menger nil) (close? const-decl "bool" k_menger nil) (subset? const-decl "bool" sets nil) (separates const-decl "bool" sep_sets nil) (graph type-eq-decl nil graphs 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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) (finite_set_induction_gen formula-decl nil finite_sets_inductions "finite_sets/") (T formal-type-decl nil k_menger nil)) shostak) (small_close-2 "put_in_tight" 3379067892 ("" (lemma "finite_set_induction_gen") (("" (skosimp*) (("" (inst -1 "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1 (("" (prop) (("1" (inst -1 "W!1") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "smaller_close") (("2" (lemma "small_tight") (("2" (inst -1 "G!1" "S!1" "s!1" "t!1") (("2" (prop) (("2" (skosimp*) (("2" (inst -4 "G!1" "V!1" "s!1" "t!1") (("2" (prop) (("1" (inst 1 "V!1") (("1" (prop) nil nil)) nil) ("2" (skosimp*) (("2" (case "card(V!1)<card(S!1)") (("1" (inst -8 "V!1") (("1" (prop) (("1" (skosimp*) (("1" (inst 2 "V1!1") (("1" (prop) (("1" (hide-all-but (-1 -8 1)) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (inst?) (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (small_close-1 nil 3379064658 ("" (lemma "finite_set_induction_gen") (("" (skosimp*) (("" (inst -1 "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1 (("" (prop) (("1" (inst -1 "W!1") (("1" (prop) nil))) ("2" (skosimp*) (("2" (lemma "smaller_tight") (("2" (inst -1 "G!1" "S!1" "s!1" "t!1") (("2" (hide -4 2) (("2" (prop) (("1" (inst 1 "S!1") (("1" (hide -2) (("1" (prop) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (hide-all-but 1) (("1" (grind) nil))))))))))))) ("2" (skosimp*) (("2" (case "card(V!1)<card(S!1)") (("1" (inst -4 "V!1") (("1" (prop) (("1" (skosimp*) (("1" (inst 2 "V1!1") (("1" (prop) (("1" (hide-all-but (-1 -5 1)) (("1" (install-rewrites "finite_sets[T]") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (inst?) (("1" (prop) nil))))))))))))))))))))))) ("2" (hide-all-but (-1 1 2)) (("2" (lemma "same_card_subset") (("2" (inst -1 "V!1" "S!1") (("2" (prop) (("2" (lemma "card_subset") (("2" (inst -1 "V!1" "S!1") (("2" (assert) nil)))))))))))))))))))))))))))))))))) nil) nil nil)) (exists_close 0 (exists_close-3 "copied from exists tight" 3379073276 ("" (skosimp*) (("" (expand "good?") (("" (expand "separable?") (("" (prop) (("" (lemma "small_close") (("" (inst?) (("" (inst -1 "{t: T | vert(G!1)(t) AND t /= s!1 AND t /= t!1}" "s!1" "t!1") (("1" (prop) (("1" (skosimp*) (("1" (inst 3 "V!1") (("1" (prop) nil nil)) nil)) nil) ("2" (hide 4) (("2" (expand "separates") (("2" (skosimp*) (("2" (expand "walk_from?") (("2" (flatten) (("2" (case "length(w!1) = 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case-replace "length(w!1) = 2") (("1" (assert) (("1" (expand "walk?") (("1" (expand "finseq_appl") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (hide -4) (("1" (replace -2 * lr) (("1" (replace -3 * lr) (("1" (hide 1) (("1" (expand "edge?") (("1" (expand "del_verts") (("1" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (i: below(length(w!1))): seq(w!1)(i) = s!1 OR seq(w!1)(i) = t!1") (("1" (expand "walk?") (("1" (expand "finseq_appl") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (expand "edge?") (("1" (expand "del_verts") (("1" (flatten) (("1" (inst -1 "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walk_verts_in") (("2" (inst?) (("1" (split -1) (("1" (hide -4) (("1" (expand "verts_in?") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (skosimp*) (("1 instjava.lang.StringIndexOutOfBoundsException: Index 61 out of bounds for length AcquireSampleRowsFuncBlockNumberrelpages (flatten) (("1" nil nil)) nil) ) nil)) nil)) nil)) nil)) nil)) nil) ("2*probablynot to .(We dont ; nil ( (- -2-32 34 ) (("2" (lemmafinite_subset[T" (("" (inst?) (("2" java.lang.StringIndexOutOfBoundsException: Range [19, 18) out of bounds for ( 1"G!1)) ( (assert) (("2" (hide 2) (2java.lang.StringIndexOutOfBoundsException: Index 55 out of bounds for length 5 rows /* ALLOCSET_DEFAULT_SIZES); nil)) nil)) nil)) nil)) nil)) nil)) nil)) )java.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for length 39 nil)) (i =1i =attr_cnt i+) nil)) nil)) nil) nil)) nil)) nil) ("java.lang.StringIndexOutOfBoundsException: Range [11, 10) out of bounds for le (("2"( finite_subset[T]) (("2" (instjava.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for l (("2" (java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for lengt (""(ssert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil) nil)) nil)) nil)) nil nil)) nil)) nil)) nil)) nil)) nil) ((good? const-decl "bool" k_menger nil) (T if (n_dist =00) ( -decl java.lang.StringIndexOutOfBoundsException: Range [45, 44) out of bounds fo --q-declnil ) (set type-eq-decl nil sets nil) (AND constjava.lang.StringIndexOutOfBoundsException: Index 69 out of bounds for l (/= const-decl "boolean" notequal nil) (= const-decl "[T, T (bl constdecl setT" doubletons ) (doubleton type-eq-decl nil doubletons nil) (finite_set type-eq-decl InvalidTransactionId, (pregraph type-eq-decl nilIrel[] IMPLIES -decl "bool bool -> bool]" booleans nil) (graph type-eq- *theirentries except java.lang.StringIndexOutOfBoundsException: Rang (separates const-decl "bool" sep_sets nil) (walk_from? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers 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_field_pred )) java.lang.StringIndexOutOfBoundsException: Index 9 out of bounds for length 9 (number_field nonempty-type-from/* Log the action if appropriate */ (eal_pred const-decl "[number_field ->boolean]" reals nil) (real nonempty-type- total_blks_dirtied = buff.+ (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (application-"ven_int"integers nil) (< const-decl "bool" reals nil) eq- nil naturalnumbersnil) (OR const-decl "[bool, bool -> bool]" booleans nil) (java.lang.StringIndexOutOfBoundsException: Range [3, 2) out of bounds for lengt nil) constb nil (difference const-decl "set" sets nil) (verts_in? const-decl "bool" walks nil) (finite_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set pfree(.; sets_lemmas nil) (walk_verts_in formula-decl * int java.lang.StringIndexOutOfBoundsException: Range [ (even_minus_odd_is_odd java.lang.StringIndexOutOfBoundsException: Range [25, 24) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) >-java.lang.StringIndexOutOfBoundsException: Range [20, 18) out of bounds for len (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers java.lang.StringIndexOutOfBou (rational nonempty-type-from-decl nil rationals nil) r java.lang.StringIndexOutOfBoundsException: Range [25, 24) out of bounds for len (nil application-judgement "finite_set[T]" k_menger nil) e? onst- "bool graphs niljava.lang.StringIndexOutOfBoundsException: Index 40 out of (del_verts tcnt] false; (real_lt_is_strict_total_order name-judgement "( thisdata-tupleFract=(double) numindexrows / (double) numrows; (int_minus_int_is_int application-judgement "int" integers nil) "ool"walksnil) (is_finite const-decl "bool" finite_sets nil) (G MemoryContextDelete(); (!1 -onst-""k_menger java.lang.StringIndexOutOfBoundsException: Index 44 out of bo (t!1 skolem-const-decl "T" k_menger nil) (small_close formula-decl nil k_menger nil) (separable? const-decl "bool ok; shostak)) (closed_minimal 0 (closed_minimal-1 nil 3379073798 java.lang.StringIndexOutOfBoundsException: Index 24 out of bounds for length 24 (("" (expand "close?") (("" (expand "separates") (("" (prop) (("" (expand "subset?") (("" (expand "member") (("" (apply-extensionality 7 :hide? t) (("" (inst -2 "x!1") (("" (iff) (("" (prop) (("1" (hide -1) (("1" (inst -2 "x!1") ((" >java.lang.StringIndexOutOfBoundsException: Range [19, 18) out of bounds for l (("1" (skosimp*) (hide/ (("1" java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2 java.lang.StringIndexOutOfBoundsException: Range [46, 45) out of bounds for leng (expand "path_from?") (("1" "") (("1" (prop) " (expand "from?") (("1" (prop) nil nil)) java.lang.StringIndexOutOfBoundsException: Range [12, 11) out of bounds for leng ("2" (expand "from?") (("2" (prop) nil nil)) nil) ("3" (hide -2) ( (expand "walk?") (("3" (expand "finseq_appl") (("3" (prop) (("1" (expand "verts_in?") (("1" (expand d) ("" (expand ) (1java.lang.StringIndexOutOfBoundsException: Index 59 out of bounds for length 5 (expand "member") (("1t scanned is (skosimp*) "" (expand ""s":scanned d % pages," " (expand cHeapTuple )java.lang.StringIndexOutOfBoundsException: Index 39 out of bounds for (("1" (expand "finseq_appl") (("1" (prop) (("1" (expand "walk?") i; " (expand (("1 *java.lang.StringIndexOutOfBoundsException: Range [19, 18) out of bounds fo (expand "verts_in?") (prop) (("1" "i!1") nil nil)) nil)) nil)) nil)) supports . (" * (hide (("2" decompose-equality (("2" -1) 2" (inst -1 get_namespace_name(RelationGetNamespace(onerel)), -2 "seq(p!1)(i!1)") (("2" (expand "singleton") (("2" [ java.lang.StringIndexOutOfBoundsException: Index 34 out of bounds for length 34 (("2" (expand "intersection") " (expand *; (prop) 1 (replace -6 lr) (("1" , nil nil)) nil) ("2" (skosimp*) (("2" (reveal -6) (("2" ( -* java.lang.StringIndexOutOfBoundsException: Range [7, 6) out of bounds for leng "seq(p1(i!1" ( java.lang.StringIndexOutOfBoundsException: Index 2 out of bounds for length 2 (prop) nil nil)) il)) nil) [+]=Int16GetDatum(stats-stakind[k]); /* stakindN */ (inst?) ( } (typepred "i!1") (("3" (reveal java.lang.StringIndexOutOfBoundsException: Range [35, 34) out of bounds for leng (("3" (expand "from stats>[k], (("3" (case (replace * ) ( (prop) (("1" (replace -2 lr) (("1" (propax) nil nil)) nil) ("2" (case "length(p!1)=1") (("1" -1 * ) (("1" (assert) nil)) nil) ("2" (assert) nil nil)) double totalrows); nil) ("2" (case "i!1=length(p!1)-1") (("1" (replace -1 * java.lang.StringIndexOutOfBoundsException: Index 63 out of bounds for length 63 (("1" (prop) (("1" (assert) nil nil) ("2" (("2" (hide -4) (("2" (replace -3 -6 weak;even n=1012,a*ksample gives =0.66 (("2" (propax) nil nil)) nil)) nil)) nil)) ) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil){ nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (prop) (("1" (expand "path?") (("1" (expand "finseq_appl") " (prop) (("1" (inst java.lang.StringIndexOutOfBoundsException: Index 23 out of bounds for length 23 "n!1+1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "path?") (("2" (expand "finseq_appl") (("2" (prop) (("2" (expand "walk?") (("2" (expand "finseq_appl") (. -]; (("2" j. j-]; -3 } (("2" / >java.lang.StringIndexOutOfBoundsException: Range [19, 18) out of bounds for leng "edge?") (("2" (prop) (("2" (expand "del_verts") (("2" (prop) (("2" (reveal -5) (("2" (skosimp*) (("2" (inst "v!1") (("2" -values. (("2" (expand "internal_verts") (("2" (expand "finseq_appl") (("2" (expand stadistinct=( )/( )+f1*n /N; "dbl") " (prop) (("1" (java.lang.StringIndexOutOfBoundsException: Index 99 out of bounds for length 71 = (tats->stadistinct/totalrows)java.lang.StringIndexOutOfBoundsException: Index 58 (("1" (inst -1 1) (("1" (expand "java.lang.StringIndexOutOfBoundsException: Index 116 out of bounds for length 1 (("1" (expand "member") (("1" (expand -stadistinct >0 &java.lang.StringIndexOutOfBoundsException: Index 28 out of bo (("1" (iff) (("1" (prop) (("1" (replace (i=0;;i<num_mcv;i+ -6 lr) (propax) nil nil)) nil) ("2" "n!1") (("2" (assert) (("2" (typepred "n!1") (("2" (case "n!1=0") (("1" (replace -1 * lr) (("1" (hide -2 -6 -7 2 3) (("1" (reveal -6) (("1" "from?") (("1" (propax) nil java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0 nil)) )) nil)) nil) ("2" (assert) nil)) nil)) nil)) nil)) value = fetchfunc(stats, i, &isnull); nil)) (snulljava.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for leng java.lang.StringIndexOutOfBoundsException: Index 3 out of bounds for length 3 nil)) nil)) nil)) nil) ("2" (decompose-equality -8) (("2" (inst -1 "v!1") (("2" (expand "singleton") (("2" (expand "java.lang.StringIndexOutOfBoundsException: Index 111 out of bounds for length 0 (("2" (expand "member") (("2" (("2" (prop) (("1" (replace -3 -6 lr) (("1" (propax) nil nil)) nil) ("2" (inst 2 ScalarItem has been found the end ofthe ,a ScalarItem's will point toitself if only it (prop) (("1" (assert) nil nil) ("2" (case "n!1+1=length(p!1)-" (("1" (replace -1 -2 lr) (("1" (reveal -3) (("1" "from?") (("1" (("1" (replace -2 -4 lr) (("1" (replace -4 -6 in the sample java.lang.StringIndexOutOfBoundsException: Range [41, 40) out of boun (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) how many are storing as commonvalues. 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)) =analyze_mcv_list(mcv_counts, num_mcv, nil)) nil)) ("2" (hide 1) (("2 (("2" (prop) (("2" (skosimp*) (("2" (hide 4) (("2" (inst 6 "p!1") (("2" (expand "path_from?") (("2" (expand"alk_from?) (("2" (prop) (("1" (expand "from?") (("1" (prop) nil nil)) nil) ("2" from") (("2" (prop) nil nil)) l) ("3" (hide -2) (("3" (expand "walk?") (("3" (expand java.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for len (("3" (prop) (("1" (expand "verts_in?") (("1" /* "del_verts") (("1" (expand "java.lang.StringIndexOutOfBoundsException: Index 58 out of bounds for length 4 (("1" (expand "member") (("1" continue; (expand "internal_verts") (("1" (expand "path?") (("1" (expand "finseq_appl") (("1" (prop) (("1" (expand "walk?") (("1" (expand "verts_in?") (("1" (expand "finseq_appl") (("1" (("1" (inst -1 "i!1") nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (decompose-equality -3) (("2" (copy -1) (("2" (inst -1 "x!1") (("2" (inst -2 "seq(p!1)(i!1)") (("2" (expand "singleton") (("2" (iff) (("2" (expand "intersection") (("2" (expand "member") (("2" (prop) (("1" (replace -3 -6 lr) (("1" ndistinct_table = stadistinct; nil nil)) nil) ("2" (skosimp*) (("2" (reveal -5) (("2" (inst */ -1 "seq(p!1)(i!1)") (("2" (prop) nil nil)) nil)) nil)) nil) ("3" (inst?) (("3" (typepred "i!1") (("3" (reveal -3) (("3" (expand "from?") (("3" (case "i!1=0") 0java.lang.StringIndexOutOfBoundsException: Index 20 out of bounds for length 20 (replace -1 * lr) (("1" (prop) (("1" (replace -2 -7 lr) (("1" (propax) nil nil)) nil) ("2" (case "length(p!1)=1") (("1" (replace -1 * lr) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "i!1=length(p!1)-1") (("1" (replace -1 * lr) (("1" (prop) (("1" (assert) nil nil) ("2" (hide 1) (("2" (hide -4) (("2" (replace -3 -6 lr) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (prop) (("1" (expand "path?") (("1" (expand "finseq_appl") (("1" (prop) (("1" (inst -4 "n!1" "n!1+1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "path?") (("2" (prop) (("2" (expand "walk?") (("2" (expand "finseq_appl") (("2" (prop) (("2" (inst -3 "n!1") (("2" (assert) (("2" (expand "edge?") (("2" (prop) (("2" (expand "del_verts") (("2" (prop) (("2" (reveal -4) (("2" (skosimp*) (("2" (inst -1 "v!1") (("2" (prop) (("2" (expand "internal_verts") (("2" (expand "dbl") (("2" (prop) (("1" (decompose-equality -8) (("1" (inst -1 "v!1") (("1" (expand "intersection") (("1" (expand "member") (("1" (expand "singleton") (("1" (iff) (("1" (prop) (("1" (replace -3 -6 lr) (("1" (propax) nil nil)) nil) ("2" (inst 2 "n!1") (("2" (assert) (("2" (typepred "n!1") (("2" (case "n!1=0") (("1" (replace -1 * lr) (("1" (hide -2 -6 -7 2 3) (("1" (reveal -6) (("1" (expand "from?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality -8) (("2" (inst -1 "v!1") (("2" (expand "singleton") (("2" (expand "intersection") (("2" (expand "member") (("2" (iff) (("2" (prop) (("1" (replace -3 -6 lr) (("1" (propax) nil nil)) nil) ("2" (inst 2 "n!1+1") (("2" (prop) (("1" (assert) nil nil) ("2" (case "n!1+1=length(p!1)-1") (("1" (replace -1 -2 lr) (("1" (reveal -3) (("1" (expand "from?") (("1" (prop) (("1" (replace -2 -4 lr) (("1" (replace -4 -6 lr) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (expand "finseq_appl") (("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)) 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) ((close? const-decl "bool" k_menger nil) (member const-decl "bool" sets 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) (walk_from? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (n!1 skolem-const-decl "nat" k_menger nil) (p!1 skolem-const-decl "prewalk[T]" k_menger nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (dbl const-decl "set[T]" doubletons nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" k_menger nil) (verts_in? const-decl "bool" walks nil) (difference const-decl "set" sets nil) (path? const-decl "bool" paths 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (intersection const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (int_minus_int_is_int application-judgement "int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_intersection2 application-judgement "finite_set[T]" k_menger nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (nil application-judgement "finite_set[T]" graphs nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (internal_verts const-decl "finite_set[T]" ind_paths nil) (del_verts const-decl "graph[T]" sep_sets nil) (walk? const-decl "bool" walks nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (n!1 skolem-const-decl "nat" k_menger nil) (p!1 skolem-const-decl "prewalk[T]" k_menger 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) (T formal-type-decl nil k_menger nil) (subset? const-decl "bool" sets nil) (separates const-decl "bool" sep_sets nil)) shostak)) (closed_verts 0 (closed_verts-1 nil 3392627299 ("" (skosimp*) (("" (expand "subset?") (("" (expand "member") (("" (expand "close?") (("" (skosimp*) (("" (inst -1 "x!1") (("" (prop) (("" (skosimp*) (("" (expand "intersection") (("" (expand "path_from?") (("" (prop) (("" (expand "path?") (("" (prop) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (prop) (("" (hide -2 -3) (("" (expand "member") (("" (decompose-equality -3) (("" (inst -1 "x!1") (("" (expand "singleton") (("" (prop) (("" (expand "internal_verts") (("" (expand "finseq_appl") (("" (skosimp*) (("" (expand "verts_in?") (("" (inst -5 "i!1") (("" (replace -4 -5 lr) (("" (propax) 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)) nil)) nil) ((subset? const-decl "bool" sets nil) (close? const-decl "bool" k_menger nil) (T formal-type-decl nil k_menger nil) (path_from? const-decl "bool" paths nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks 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) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (internal_verts const-decl "finite_set[T]" ind_paths 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil)) shostak)) (attach_edges_TCC1 0 (attach_edges_TCC1-1 nil 3377812958 ("" (skosimp*) (("" (typepred "W!1") (("" (lemma "finite_add[T]") (("" (inst -1 "W!1" "x!1") (("" (lemma "all_edges_finite[T]") (("" (inst -1 "add(x!1,W!1)") (("" (lemma "finite_subset[doubleton[T]]") (("" (inst -1 "all_edges(add(x!1,W!1))" "{e: doubleton[T] | EXISTS w: W!1(w) AND e = dbl[T](w, x!1)}") (("" (prop) (("" (hide 2) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "all_edges") (("" (typepred "x!2") (("" (skosimp*) (("" (inst 2 "w!1" "x!1") (("" (hide -4 -5) (("" (prop) (("1" (replace -2 -4 lr) (("1" (lemma "dbl_eq") (("1" (inst -1 "w!1" "x!3" "y!1" "x!1") (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "add") (("2" (expand "member") (("2" (prop) nil nil)) nil)) nil) ("3" (expand "add") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (T formal-type-decl nil k_menger nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nonempty_add_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" k_menger nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (x!1 skolem-const-decl "T" k_menger nil) (W!1 skolem-const-decl "finite_set[T]" k_menger nil) (member const-decl "bool" sets nil) (dbl_eq formula-decl nil doubletons nil) (subset? const-decl "bool" sets nil) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (finite_subset formula-decl nil finite_sets nil) (all_edges_finite formula-decl nil complem nil) (finite_add formula-decl nil finite_sets nil)) nil)) (Hverts_TCC1 0 (Hverts_TCC1-2 "try" 3392467780 ("" (skosimp*) (("" (typepred "G!1") (("" (typepred "W!1") (("" (typepred "vert(G!1)") (("" (case "subset?(path_verts[T](del_verts[T](G!1, W!1), x!1),vert(G!1))") (("1" (lemma "finite_subset") (("1" (inst -1 "vert(G!1)" "path_verts[T](del_verts[T](G!1, W!1), x!1)") (("1" (prop) nil nil)) nil)) nil) ("2" (hide -3 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "path_verts") (("2" (skosimp*) (("2" (expand "walk_from?") (("2" (prop) (("2" (expand "walk?") (("2" (prop) (("2" (expand "verts_in?") (("2" (inst -3 "length(w!1)-1") (("2" (expand "del_verts") (("2" (expand "difference") (("2" (expand "member") (("2" (prop) (("2" (replace -2 -3 lr) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (T formal-type-decl nil k_menger nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (difference const-decl "set" sets 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (path_verts const-decl "set[T]" paths nil) (del_verts const-decl "graph[T]" sep_sets nil) (is_finite const-decl "bool" finite_sets nil)) shostak) (Hverts_TCC1-1 nil 3377812958 ("" (subtype-tcc) nil nil) nil nil)) (Mgraph_TCC1 0 (Mgraph_TCC1-2 "none" 3392652497 ("" (skosimp*) (("" (expand "add") (("" (expand "member") (("" (prop) (("" (expand "union") (("" (expand "member") (("" (prop) (("1" (typepred "Kgraph(G!1,W!1,x!1)") (("1" (inst -1 "e!1") (("1" (prop) (("1" (inst -1 "x!2") (("1" (prop) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "attach_edges") (("2" (skosimp*) (("2" (expand "intersection") (("2" (expand "member") (("2" (replace -2 -3 lr) (("2" (expand "dbl") (("2" (prop) (("1" (expand "Kgraph") (("1" (expand "subgraph") (("1" (expand "difference") (("1" (expand "member") (("1" (prop) (("1" (replace -1 -2 rl) (("1" (propax) nil nil)) nil) ("2" (replace -1 -2 rl) (("2" (propax) nil nil)) nil) ("3" (expand "Hverts") (("3" (expand "path_verts") (("3" (skosimp*) (("3" (expand "del_verts") (("3" (expand "walk_from?") (("3" (prop) (("3" (expand "walk?") (("3" (prop) (("3" (hide -4) (("3" (expand "verts_in?") (("3" (expand "difference") (("3" (expand "member") (("3" (inst -3 "length(w!2)-1") (("3" (prop) (("3" (replace -2 -4 rl) (("3" (replace -4 -6 rl) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((add const-decl "(nonempty?)" sets nil) (attach_edges const-decl "finite_set[doubleton[T]]" k_menger nil) (intersection const-decl "set" sets nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (Hverts const-decl "finite_set[T]" k_menger nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (verts_in? const-decl "bool" walks nil) (del_verts const-decl "graph[T]" sep_sets nil) (path_verts const-decl "set[T]" paths nil) (difference const-decl "set" sets nil) (Kgraph const-decl "graph" k_menger nil) (is_finite const-decl "bool" finite_sets nil) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (T formal-type-decl nil k_menger nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil)) shostak) (Mgraph_TCC1-1 nil 3377812958 ("" (subtype-tcc) nil nil) nil nil)) (Hst_intersect 0 (Hst_intersect-1 nil 3378035424 ("" (skosimp*) (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (expand "intersection") (("" (expand "member") (("" (prop) (("" (expand "Hverts") (("" (expand "path_verts") (("" (skosimp*) (("" (expand "separates") (("" (prop) (("" (lemma "walk_merge") (("" (inst -1 "del_verts(G!1,W!1)" "w!2" "w!1" "s!1" "t!1" "x!1") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (Hverts const-decl "finite_set[T]" k_menger 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) (del_verts const-decl "graph[T]" sep_sets 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) (T formal-type-decl nil k_menger nil) (walk_merge formula-decl nil walks nil) (separates const-decl "bool" sep_sets nil) (path_verts const-decl "set[T]" paths nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil)) shostak)) (subset_Ws 0 (subset_Ws-1 nil 3378036419 ("" (skosimp*) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "Mgraph") (("" (expand "add") (("" (expand "member") (("" (prop) (("1" (expand "good?") (("1" (prop) (("1" (replace -1 -3 lr) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "Kgraph") (("2" (expand "subgraph") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (good? const-decl "bool" k_menger nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (Kgraph const-decl "graph" k_menger nil) (Mgraph const-decl "graph" k_menger nil) (member const-decl "bool" sets nil)) shostak)) (subset_Wt 0 (subset_Wt-1 nil 3378036813 ("" (skosimp*) (("" (expand "subset?") (("" (expand "member") (("" (skosimp*) (("" (expand "Mgraph") (("" (expand "add") (("" (expand "member") (("" (prop) (("1" (expand "good?") (("1" (prop) (("1" (replace -1 -4 lr) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "Kgraph") (("2" (expand "subgraph") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (good? const-decl "bool" k_menger nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (Kgraph const-decl "graph" k_menger nil) (Mgraph const-decl "graph" k_menger nil) (member const-decl "bool" sets nil)) nil)) (size_Ws 0 (size_Ws-3 "redo defns" 3378322265 ("" (skosimp*) (("" (lemma "finite_sets[T].card_subset") (("" (lemma "finite_sets[T].same_card_subset") (("" (inst -1 "vert(Mgraph(G!1,W!1,s!1))" "vert(G!1)") (("" (inst -2 "vert(Mgraph(G!1,W!1,s!1))" "vert(G!1)") (("" (expand "size") (("" (hide -1) (("" (prop) (("1" (case "vert(Mgraph(G!1, W!1, s!1)) = vert(G!1)") (("1" (expand "close?") (("1" (expand "attached?") (("1" (prop) (("1" (skosimp*) (("1" (inst -5 "w!1") (("1" (prop) (("1" (expand "intersection") (("1" (expand "member") (("1" (skosimp*) (("1" (hide -4 3) (("1" (expand "Mgraph") (("1" (expand "Kgraph") (("1" (expand "add") (("1" (expand "member") (("1" (expand "difference") (("1" (expand "member") (("1" (expand "Hverts") (("1" (expand "path_verts") (("1" (expand "subgraph") (("1" (decompose-equality -3) (("1" (inst -1 "p!1(1)") (("1" (iff) (("1" (expand "finseq_appl") (("1" (prop) (("1" (hide -4 -5 -6) (("1" (install-rewrites "paths") (("1" (assert) (("1" (prop) (("1" (inst -7 "0" "1") (("1" (assert) nil nil)) nil) ("2" (inst -5 "0") (("2" (assert) (("2" (case "length(p!1)=1") (("1" (replace -1 * lr) (("1" (assert) (("1" (reveal -3) (("1" (expand "good?") (("1" (expand "separable?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst -5 "0") (("3" (assert) (("3" (case "length(p!1)=1") (("1" (replace -1 * lr) (("1" (assert) (("1" (reveal -3) (("1" (expand "good?") (("1" (expand "separable?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("4" (inst -4 "0") (("4" (assert) (("4" (case "length(p!1)=1") (("1" (replace -1 * lr) (("1" (assert) (("1" (reveal -3) (("1" (expand "good?") (("1" (expand "separable?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) * nil) nil)) nil) ) ("" (nst ) "ath_from?) " ***b-*a-*bc-1*^,(^1*^1d^2)2, (xpand (("1" (prop) (("1" - -9) ("1" (expand*bb-*d*-1**)2d***^1a, ?") "" expand "finseq_appl") [ ^,c2,a, b^**bc,(*)2 *a-2*d*,a^1**^1^, d*-1b)^,a^1b-*^1c***ab^1***^1 a-**)4java.lang.StringIndexOutOfBoundsException: In a-*b^1(*^2**^)^*^1***b^1*a*)2ab-*java.lang.StringIndexOutOfBoundsException: Inde (hide -5) "^") expand "walk?") (1java.lang.StringIndexOutOfBoundsException: Index 97 out of bounds for length 9 (prop) *a)********^*c**c^1a*d***bd , -5 "0") (("1" "p!1") "" (assert) ^c(-*^*a-*^*ba-2, (1>) (("1" # 688128.10 (("" *b**^2*-*^1*^3a-*, "walk_from) *^a^1*^*^2*a-1c^1]java.lang.StringIndexOutOfBoundsException: Index 50 out of bou (expand "finseq_appl") (( -1*a^*d*a^1*b*^-*b^1*^1d^1*a-1*b*ajava.lang.StringIndexOutOfBoundsException: I -a2**^*^2**^1*^1*a^1d-**b-, "del_verts") "walk?") 2**^**c)2 (expand " (("1" (expand ^*^-) **b-*^1^2,^(^1^)] (("1" (prop) ("" (expand -^1(^)2a-\ (("1" ^**b)*^a-**)*b-*^*^a-***^1*-\ (expand "member") ** ^1-*****ca^1* a^-2bc^1^, (skosimp*) 2*^**^**^2a^1b^1**^-1*^1*-*a-*^1a-)java.lang.StringIndexOutOfBoundsException: In *^*^1*-*^2 -*^1(^1a^1^*a-*^2a*a*b*b-*b)*^1**a*b\ 0) (("1" -1 * )****a-^*-*^1 *a*^a*-,b^12b*a^1c^1 b^)(-1*-) *b*c*^1*,(*^)3,a*^3*a*^*java.lang.StringIndexOutOfBoundsException: Index 60 out -8 "0") (java.lang.StringIndexOutOfBoundsException: Index 141 out of bounds for length 1 (reveal b)java.lang.StringIndexOutOfBoundsException: Index 9 out of bounds for length 9 (expand "separates")2b^a^)*cb-)3java.lang.StringIndexOutOfBoundsException: Index 34 out (("1" (assert) nil)^-*b*a^1-**a^2*b^-1*^2*-*^1*b^-***a*^1a^2*^1( nil)) nil)) )*-*^2b-***a-)*^1(-*)2a-*-java.lang.StringIndexOutOfBoundsException: Index 78 ou ^1^-a*^1b-*^, b^--1^ ]] nil) ^*c "i!1=1") (("1" -1 -2*-, (("1" (prop) (("1" (replace -11 -10 lr) (("22^1a*-a^2*^-1(^1b-)^*a^1b2*(a*^1^3, (equality -12) *2c^*2*b-*-*^**bc ^c^*^***b*-3*a**a*cb-*ab^3c*java.lang.StringIndexOutOfBoundsException: Index 77 "seq(p!1)(1)") (("1" (iff) d^1b^1d*d*a^-1*b**b-, -*b-***^**)2 (("1" (hide 2) bd2(*-*^,b-*^1*a**java.lang.StringIndexOutOfBoundsException: Range [67, 66) out " (expand (("1" (inst 1 "1") (("1" (assert) (("1" "length(p!1)=2") -b-*^*b-*a-*^*b*, (replace ^^1(^*^-1*b-c*a\ * (("1" -,(-)^-*1b-)^a^1) -5 -*a^**c-*,c^2d^*^2(^1d3, 1) ^*^*^1*^1(^*-)^***b^**^*2java.lang.StringIndexOutOfBoundsException: Index 57 out (expand "good?") (("1" 3*^1c^-1*(*)2c1b2a^1*a*b^1c-*b-1\ (expand "separable?") (("1" (prop) (("1" (reveal *-1ab^-**-a-** (reveal -5) *-**b**)2*^*^2*b\ (expand "finseq_appl") ("1 *^1aa*^2a^2b***b*c*a^-*, (("1" -3 -2 lr) (("1" (assert) nil)) nil)) nil)) nil)) a^b^-2^1*^-c*^1ab^2**^1c-***^java.lang.StringIndexOutOfBoundsException: Index 78 nil)) nil)) nil)) nil)) java.lang.StringIndexOutOfBoundsException: Range [39, 38) out of bounds for leng *d^2a-**a-*)2a-*^1a*^2a^-1*b-1a^b- nil) ("2" (assert) (("2" (expand (("2" (propax) nil nil)) nil)) nil)) ) nil)) nil)) nil)) ^*2*-***a^*)2*b-***b^- nil)) nil)) ) nil)) nil)) nil) (assert) java.lang.StringIndexOutOfBoundsException: Index 136 out of bounds for length 63 nil)) nil)) nil)) ,^2^a-1 ^a^1, ^b-) (-) ^1**^2,c^ nil)) nil)) nil) ("2" (skosimp*) *^***c-*1c*a-**^1java.lang.StringIndexOutOfBoundsException: Index 51 out of boun (case 0) (("1" -1 * java.lang.StringIndexOutOfBoundsException: Index 127 out of bounds for length 78 (("1" (expandb^-1*d*^1bc*b-***a-*^2ac1bdc(^1c-)2b*b^1* "edge?" 1) (("1" (prop) (("1" (expand "edge? ^1a**-*d*-)2*^1c*^1* (("1" ) c-**c*-1**^1*a^*d***-**ad**^ ] nil) 56,28 ], a2d*^2 ^1d2a^1d-, "dge?) (("2" (assert) nil nil) (skosimp*) (("3" "dbl") (split -2) (hide * -7 -8) (("1" (reveal ) (("1" (expand (("1" (prop) (("1" (replace -1 -2 (("1" (replace -9 c1java.lang.StringIndexOutOfBoundsException: Range [43, 42) out of bounds for le (("1" (propax) nil nil)) nil)) nil)) nil)) *-b^*1^1c12- nil)) nil) ("2" (hide -4 -7 -8) (("2" (expand "good?") (2java.lang.StringIndexOutOfBoundsException: Index 145 out of bounds for length (expand "separable?") (("2" (prop) (decompose-equality -10) (inst -1 "v!1") (("2" 1*bdc^-1*-**d-*^1c*-2***^-1*^1c***^java.lang.StringIndexOutOfBoundsException: In (prop) (("1" (expand "singleton") ( -12 * lr) (("1" (replace -4 -11 rlc ((1cjava.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length (replace -3 * lr) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) --*b2c**^, "singleton") ^*^-***d*b^1*2c^1*^1d*^1, "internal_verts") (("2" (inst 2 (("2" (prop) ( nil nil) ("2" (case "length(p!1)=2") (("1" (replace -1 * lr) (("1" (hide -5 -6 1) ("1 (reveal -8) (("1" (replace -2 * lr) (("1" (assert) java.lang.StringIndexOutOfBoundsException: Index 78 out of bounds for length 78 bjava.lang.StringIndexOutOfBoundsException: Range [41, 40) out of bounds for len nil)) nil) ("2" (assert) nil nil)) ("3" 4,d*^1*d*, a^*c^1*^2c,(^-*d)^2 "finseq_appl") (("3" bcb-*a^-**b-*^1 nil 1c*^1*-1b^**b^1*-*^1b nil)) nil) nil)) nil)) nil)) nil)) ^a22*-1d\ nil)) nil)) nil)) *cb-****b-*^2 nil)) nil)) nil)) nil)) c1*^11*^1ab**b^**^-1c**-* nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) java.lang.StringIndexOutOfBoundsException: Range [0, 117) out of bounds for leng nil)) nil))a^-1eac-1a-1bdc, nil)) nil)) nil) ("2" (expand **^1**a^2d-*d*^1d**^1, da^1*b*^1a^1*^1-**^1d-1*^1*^1**d, "length(p!1)=1") (("1" (replace -1 * lr) (("1" (assert) e^2c*^1c*ae*^2*-****^1*a-**c-*\ (("1" ^1***,1**c* a-*^1*^java.lang.StringIndexOutOfBoundsException: Index 67 out of bou -3) (("1" (hide -5 *aa^1*b^-1*^-1(**^1a^*b*^2**b^1ajava.lang.StringIndexOutOfBoundsException: Index -10 1 2) (("1" (replace -3 * lr) (("1" (assert) (("1" (expand "good?") (("1" (expand "separable?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal -3) (("2" (replace -2 * lr) (("2" (("2" (expand "good?") (("2" (expand d-*; (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) ) nil)) nil) ("2" (assert nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" "^" "min") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil) ("3" (hide -2 -3 -4 4 5) (("3" (install-rewrites "paths") (("3" (assert) (("3" (prop) (("3" (inst -1 "1") nil nil)) nil)) nil) ("4" (hide-all--but (-1 1)) (install-rewrites "paths") (("4" (assert) (("4" (prop) (("4" (inst -1 *java.lang.StringIndexOutOfBoundsException: Range [14, 13) out of bounds for len nil nil)) nil)) nil) nil)) nil) ("5" (hide-all-but (-2 1)) 688128.5 (installrewrites "paths") (("5" (assert) (("5" (prop) (inst -1 "1") nil ***^**(*^1^**ba*-)2*d*a*d*b^-1*a*****^1ca* nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "good?") (("2" (expand "separable?") (("2" (prop) (("2" (hide -2 -5 3 4 5) (("2" (install-rewrites "paths") (("2" (assert) (("2" (prop) (("2" (typepred *^*dab^-(a^d-*bd), (("2" (case "length(p!1)=1") (("1" (replace -[ 2java.lang.StringIndexOutOfBoundsException: Range [17, 16) out of bounds for l * (("1" (assert) nil nil)) nil) " (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)) nil)) nil) ("2" (reveal -3) (("2" (inst -1 "vert(Mgraph(G!1, W!1, s!1))" "vert(G!1)") (("2" (prop) (("1" (hide -1 -4 3 4) (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) nil)) nil) ("2" (hide -2 -3 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil k_menger nil) (card_subset formula-decl nil finite_sets 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) [[c ,^a^1) c(^1, ^1)] ]]; ((abcde) (/= const-decl " b*d^2cb^1d**, a*b*c*b-*c**d-2,ce-*b^1d-2c**e^-, (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (Mgraph const-decl "graph" k_menger nil) (size const-decl "nat" graphs nil) (finite_intersection2 application-judgement "finite_set[T]" k_menger nil) (finite_union application-judgement " d*c*a*d*b^-1*a^-1*(b^-1*a)^2*b^-1*d*a^-1*b^-1 (nonempty_add_finite application-judgement (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas) (subset? const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (close? const-decl "bool" k_menger nil) (intersection const-decl "set" sets nil) (add const-decl "(nonempty?)" sets nil) (difference const-decl "set" sets nil) (Hverts const-decl "finite_set[T]" k_menger nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (p!1 skolem-const-decl "prewalk[T]" k_menger nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (>= const-decl "bool" reals nil) (nt nonempty-type-declnil integers) (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_gt_is_strict_total_order-judgement "(strict_total_order?[real])" real_props nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (separates const-decl "bool" a^-1*d*a*b^-1*a^-1*d*a*b, c^-1*b^-1*c^*^bjava.lang.Stri (even_minus_odd_is_odd application-judgement "odd_int" integers ( -decl "finite_set[T] ind_paths niljava.lang.StringIndexOutOfBoundsException: Index (singleton? const-decl "bool" sets nil) s const- "singleton?"setsjava.lang.StringIndexOutOfBoundsException: Index 50 out o (odd_plus_even_is_odd application-judgement "odd_int" integers nil) ( application-udgement "finite_set[]"k_menger nil) (min const(*d^**d*b^*ba**b^***c-*^1*da, pjava.lang.StringIndexOutOfBoundsException: Range [28, 27) out of bounds for len real_defs nil) (nat_min application-judgement "{k: nat | k <(d*a^-1)^2*b^-1*c^-1*b^-1, real_defs nil) (nil application-judgement "finite_set[T]" graphs nil) (int_minus_int_is_int application-judgement "int" integers nil) (nil application-judgement "finite_set[T]" k_menger nil) (verts_in? const--*^*-***^**^1*b-*-*b1-*-*-*-java.lang.StringIndexOutOfBoundsExce (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (good? const-decl "bool" k_menger nil) (separable? const-decl "bool" sep_sets nil) (below type-eq-decl nil naturalnumbers nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" k_menger nil) (del_verts const-decl "graph[T]" sep_sets nil) (^ ^*)*^*^1b^)22java.lang.StringIndexOutOfBoundsException: Index 53 out of bounds (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) ---nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field_pred const nil) number--decl 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) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (path_verts const-decl "set[T]" paths nil) (Kgraph const-decl "graph" k_menger nil) (member const-decl "bool" sets nil) (attached? const-decl "bool" k_menger nil) (same_card_subset formula-decl nil finite_sets nil)) shostak) (size_Ws-2 "try2" 3378120234 ("" (skosimp*) (("" (lemma "finite_sets[T].card_subset") [].same_card_subset") (("" (inst -1 "vert(Mgraph(G!1,W!1,s!1))" "vert(G!1)") (("" (inst -2 "vert(Mgraph(G!1,W!1,s!1))" "vert(G!1)") (("" (expand "size") (("" (hide -1) (( (("1" ( "vert(Mgraph(G!1, W!1, s!1)) = vert(G!1)") (("1" (hide -2 2) (("1" (decompose-equality -1) (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (size_Ws-1 nil*^1*1b*^1b-1a*ab-)2a-*^1a(*-*^1a-)2ba\ ("" (skosimp*) (("" (lemma "finite_sets[T].card_subset") (" lemma "finite_sets.same_card_subset) (("" (inst -1 "vert(Mgraph(G!1,W!1,s!1))" "vert(G!1)") ( , , ^b^1 ^,a(-*^1,(-*^1b-)(^-, ((""a^*b-**b^,(^2a^2*b)(^1,(^*^b^, (("1" (expand "attached?") (("1" (skosimp*) (("1" (expand "Mgraph") (("1" (expand "add") (("1" (expand "member") (("1" (hide -1 3) (("1" (expand "Kgraph") (("1" (expand "subgraph") (("1" *^**-*-^-1*(b*a*b^-1*a)^2*d^-1*b*a, (("1" (expand "member") (("1" (expand "Hverts") (expand "del_verts") (("1" (expand "path_verts") (("1" (decompose-equality^1*^*(a^1)^, (("1" (inst -1 "w!1") (("1" (iff -1) (("1" (prop) (("1" (expand "separates") (("1" (prop) (("1" (replace -1 1 lr) (("1" (propax) nil nil)) nil) nil)) nil) ("2" (postpone) nil nil) (postpone) nil nil) ("4" (postpone) nil nil) ("5" --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.954Angebot ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-10-11