Impressum k_menger.prf
Sprache: Lisp
(k_mengernil 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 )"bool" k_menger nil )"nat" sep_sets nil )"graph[T]" k_menger nil )"T" k_menger nil )"T" k_menger nil )nil sep_sets nil )"bool" k_menger nil )nil sep_sets nil )"finite_set[T]" sep_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil k_menger nil ))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 )"bool" k_menger nil )"T" k_menger nil )"graph[T]" k_menger nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )"T" k_menger nil )"bool" finite_sets nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"nat" sep_sets nil )"bool" k_menger nil )nil sep_sets nil )nil k_menger nil ))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 )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil k_menger nil )nil finite_sets_card_from nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"R" extend nil )"R" restrict nil )"finite_set[S]" nil ))nil 3389098779"" (skosimp*)"" (lemma "card_extension_W" )"" (inst -1 "W!1" "W!1" )"" (prop) (("" (hide 2) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )nil k_menger nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil k_menger nil ))"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" "finite_sets_card_eq[prewalk,Path_from[T](G!1, s!1, t!1)].card_eq_bij" )"1" (expand "restrict" )"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" "min_sep_set_card" )"1" "1" "1" expand "sep_num" )"1" "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" "restrict_set_props[prewalk,Path_from[T](G!1, s!1, t!1)].restrict_finite" )"2" "ips!1" )"2" "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 )nil k_menger nil )nil easy_menger nil )"bool" k_menger nil )"bool" k_menger nil )"bool" ind_paths nil )"bool" ind_paths nil )"bool" k_menger nil )nil restrict_set_props nil )"bool" k_menger nil )"nat" sep_sets nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sep_sets nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )"bool" sep_sets nil )"bool" graphs nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )nil application-judgement "finite_set[T]" k_menger nil )nil application-judgement "finite_set[T]" graphs nil )"set_of_prewalks" k_menger nil )"T" k_menger nil )"T" k_menger nil )"graph[T]" k_menger nil )nil finite_sets_card_eq "finite_sets/" )nil k_menger nil )"R" restrict nil )nil ind_paths nil )"bool" finite_sets nil )nil paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )"finite_set[S]" nil )"bool" k_menger nil ))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))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" "1" "p!1" )"1" expand "path_from?" )"1" "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 )"bool" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sep_sets nil )nil path_ops nil )"bool" paths nil )"bool" walks nil )"int" integers nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )"graph[T]" sep_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" k_menger nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))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" "1" "singleton[prewalk](p!1)" )"1" "1" "card_singleton[prewalk]" )"1" "p!1" )"1" "1" expand "ind_prewalk_set?" )"1" "1" expand "singleton" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "st_path_set?" )"2" "2" "2" expand "singleton" )"2" replace -1 * lr)"2" "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" "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 )"bool" k_menger nil )"bool" k_menger nil )"bool" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"set" sets nil )"bool" k_menger nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil application-judgement "finite_set[T]" graphs nil )"int" integers nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" k_menger nil )nil finite_sets nil )nil nat_types nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )nil k_menger nil )"bool" sets nil )"(singleton?)" sets nil )"non_empty_finite_set" finite_sets nil )"bool" sets nil )"graph[T]" sep_sets nil )nil finite_sets nil )"bool" k_menger nil )"(strict_total_order?[real])" real_props nil )"bool" finite_sets nil )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" k_menger nil )nil k_menger nil ))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 )"bool" k_menger nil )nil k_menger nil )"bool" sets nil )"bool" sets nil ))"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" "x!1" )"2" "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" "w!1" )"3" "3" case "verts_of(w!1)(x!1)" )"1" "1" "1" expand "path_verts" )"1" expand "verts_of" )"1" "1" expand "finseq_appl" )"1" "w!1^(0,i!1)" )"1" expand "walk_from?" )"1" "1" expand *"^" min nil nil )"2" expand *"^" min nil nil )"3" "3" "walk?_caret" )"3" "G!1" "0" "i!1" "w!1" )"3" "i!1" )"3" assert )"3" "walk?_subgraph" )"3" "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1" )"3" "3" "3" assert )"3" "finite_sets[T]" )"3" assert )"3" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "walks" )"2" expand "walk?" )"2" expand "finseq_appl" )"2" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" "i!1" )"1" "1" "i!1" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1" )"1" expand "remove" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" expand "verts_of" )"2" expand "finseq_appl" )"2" expand "edge?" )"2" "2" "2" expand "del_verts" )"2" "2" "2" "2" "seq(w!1)(n!1)" )"2" "seq(w!1)(n!1 + 1)" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1+n!1" )"4" assert )nil nil ))nil ))nil )"5" "n!1" )"5" assert )nil nil ))nil )"6" "n!1" )"6" assert )nil nil ))nil )"7" replace "7" nil nil ))nil )"8" replace "8" nil nil ))nil ))nil ))nil ))nil )"2" 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" "w!1" )"3" "3" case "verts_of(w!1)(x!1)" )"1" "1" "1" expand "path_verts" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" "1" "rev(w!1)^(0,length(w!1)-1-i!1)" )"1" expand "walk_from?" )"1" "1" expand "rev" )"1" expand *"^" min nil nil ))nil )"2" expand "rev" )"2" expand *"^" min nil nil ))nil )"3" "3" "walk?_caret" )"3" "walk?_rev" )"3" "G!1" "w!1" )"3" "G!1" "0" "length(w!1)-1-i!1" "rev(w!1)" )"1" "i!1" )"1" assert )"1" "walk?_subgraph" )"1" "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1" )"1" "1" "walk?_caret" )"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" "4" 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 "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "walks" )"2" expand "walk?" )"2" expand "finseq_appl" )"2" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" "i!1" )"1" "1" "i!1" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1" )"1" expand "remove" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" expand "verts_of" )"2" expand "finseq_appl" )"2" expand "edge?" )"2" "2" "2" expand "del_verts" )"2" "2" "2" "2" "seq(w!1)(n!1)" )"2" "seq(w!1)(n!1 + 1)" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1+n!1" )"4" assert )nil nil ))nil ))nil )"5" "n!1" )"5" assert )nil nil ))nil )"6" "n!1" )"6" assert )nil nil ))nil )"7" replace "7" nil nil ))nil )"8" replace "8" nil nil ))nil ))nil ))nil ))nil )"2" 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 )"bool" k_menger nil )"bool" sets nil )"set" sets nil )"finite_set[T]" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )"nat" k_menger nil )"finseq[T]" doubletons nil )"prewalk[T]" k_menger nil )"[numfield, numfield -> numfield]" number_fields nil )"below(length(w!1))" k_menger nil )nil walks nil )"bool" sep_sets nil )"bool" walks nil )"bool" walks nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" graphs nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" k_menger nil )"set[T]" paths nil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"finseq" finite_sequences nil )"prewalk[T]" k_menger nil )"bool" reals nil )nil naturalnumbers nil )"below(length(w!1))" k_menger nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil walks nil )nil subgraph_paths nil )"(partial_order?[set[T]])" nil )"finite_set[T]" k_mengernil )"set" sets nil )"bool" subgraphs nil )"graph[T]" sep_sets nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"finite_set[T]" walks nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" sets nil ))"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" "x!1" )"2" "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" "w!1" )"3" "3" case "verts_of(w!1)(x!1)" )"1" "1" "1" expand "path_verts" )"1" expand "verts_of" )"1" "1" "w!1^(0,i!1)" )"1" expand "walk_from?" )"1" "1" expand *"^" min "1" nil nil ))nil )"2" expand *"^" min "2" nil nil ))nil )"3" "3" "walk?_caret" )"3" "G!1" "0" "i!1" "w!1" )"3" "i!1" )"3" assert )"3" "walk?_subgraph" )"3" "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1" )"3" "3" "3" assert )"3" "finite_sets[T]" )"3" assert )"3" "1" nil nil )"2" 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" "2" "walks" )"2" expand "walk?" )"2" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" "i!1" )"1" "1" "i!1" )"1" expand "verts_of" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1" )"1" expand "remove" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" expand "verts_of" )"2" expand "edge?" )"2" "2" "2" expand "del_verts" )"2" "2" "2" "2" "seq(w!1)(n!1)" )"2" "seq(w!1)(n!1 + 1)" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1+n!1" )"4" assert )nil nil ))nil ))nil )"5" "n!1" )"5" assert )nil nil ))nil )"6" "n!1" )"6" assert )nil nil ))nil )"7" replace "7" nil nil ))nil )"8" replace "8" nil nil ))nil ))nil ))nil ))nil )"2" 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" "w!1" )"3" "3" case "verts_of(w!1)(x!1)" )"1" "1" "1" expand "path_verts" )"1" expand "verts_of" )"1" "1" "rev(w!1)^(0,length(w!1)-1-i!1)" )"1" expand "walk_from?" )"1" "1" expand "rev" )"1" expand *"^" min "1" nil nil ))nil ))nil )"2" expand "rev" )"2" expand *"^" min "2" nil nil ))nil ))nil )"3" "3" "walk?_caret" )"3" "walk?_rev" )"3" "G!1" "w!1" )"3" "G!1" "0" "length(w!1)-1-i!1" "rev(w!1)" )"1" "i!1" )"1" assert )"1" "w!1" )"1" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" 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 )nil walks nil )"bool" sep_sets nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" subgraphs nil )nil walks nil )"finite_set[T]" walks nil )nil walks nil )"bool" walks nil ))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" "x!1" )"2" "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" "w!1" )"3" "3" case "verts_of(w!1)(x!1)" )"1" "1" "1" expand "path_verts" )"1" expand "verts_of" )"1" "1" "w!1^(0,i!1)" )"1" expand "walk_from?" )"1" "1" expand *"^" min "1" nil nil ))nil )"2" expand *"^" min "2" nil nil ))nil )"3" "3" "walk?_caret" )"3" "G!1" "0" "i!1" "w!1" )"3" "i!1" )"3" assert )"3" "walk?_subgraph" )"3" "G!1" "del_verts(G!1, remove(x!1, W!1))" "w!1" )"3" "3" "3" assert )"3" "finite_sets[T]" )"3" assert )"3" "1" nil nil )"2" 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" "2" "walks" )"2" expand "walk?" )"2" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" "i!1" )"1" "1" "i!1" )"1" expand "verts_of" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1" )"1" expand "remove" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" expand "verts_of" )"2" expand "edge?" )"2" "2" "2" expand "del_verts" )"2" "2" "2" "2" "seq(w!1)(n!1)" )"2" "seq(w!1)(n!1 + 1)" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil )"4" assert )"4" "1+n!1" )"4" assert )nil nil ))nil ))nil )"5" "n!1" )"5" assert )nil nil ))nil )"6" "n!1" )"6" assert )nil nil ))nil )"7" replace "7" nil nil ))nil )"8" replace "8" nil nil ))nil ))nil ))nil ))nil )"2" 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))nil 3378206435"" (lemma "finite_set_induction_gen" )"" (skosimp*)"" "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1,V1,s!1,t!1) and tight?(G!1,s!1,t!1,V1)))" )"" (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" "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" "V1!1" )"1" "1" "1" "finite_sets[T]" )"1" assert )"1" "1" "1" "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" "2" "card_subset" )"2" "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 )nil k_menger nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil finite_sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" finite_sets nil )"{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 )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"set[T]" paths nil )"set" sets nil )"graph[T]" sep_sets nil )"set" sets nil )"bool" k_menger nil )"bool" sets nil )"bool" sep_sets nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_sets_inductions"finite_sets/" )nil k_menger nil ))nil 3378222865"" (skosimp*)"" (expand "good?" )"" (expand "separable?" )"" (prop)"" (lemma "small_tight" )"" (inst?)"" "{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" "1" (assert ) nil nil ))nil ))nil )"2" "length(w!1) = 2" )"1" assert )"1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "0" )"1" assert )"1" "1" replace -2 * lr)"1" replace -3 * lr)"1" "1" expand "edge?" )"1" expand "del_verts" )"1" 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" "1" "0" )"1" assert )"1" expand "edge?" )"1" expand "del_verts" )"1" "1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walk_verts_in" )"2" "1" "1" "1" expand "verts_in?" )"1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" "2" "finite_subset[T]" )"2" "2" "vert(G!1)" )"2" assert )"2" "2" 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 )"bool" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sep_sets nil )"bool" walks nil )nil numbers nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"even_int" integersnil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"finite_set[T]" k_mengernil )"bool" sets nil )"set" sets nil )"bool" walks nil )nil finite_sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil walks nil )"odd_int" integersnil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" graphs nil )"graph[T]" sep_sets nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" walks nil )"bool" finite_sets nil )"graph[T]" k_menger nil )"T" k_menger nil )"T" k_menger nil )nil k_menger nil )"bool" sep_sets nil ))nil )nil 3378222242"" (skosimp*)"" (lemma "sep_set_exists" )"" (inst?)"" (inst?)"" (inst?) (("" (skosimp*) (("" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil shostak))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" "1" "x!1" )"1" "1" expand "singleton" )"1" "1" expand "internal_verts" )"1" expand "finseq_appl" )"1" "1" expand "path_verts" )"1" "p!1^(0,i!1)" )"1" expand *"^" min "1" expand "walk_from?" )"1" "1" "paths" )"1" assert )nil nil ))nil )"2" expand "path_from?" )"2" "2" expand "path?" )"2" expand "finseq_appl" )"2" "2" "walk?_caret" )"2" "G!1" "0" "i!1" "p!1" )"2" "1" "walks" )"1" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )"3" "1" "1" nil nil ))nil )"2" "2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "2" "x!1" )"2" "2" expand "singleton" )"2" "2" expand "internal_verts" )"2" expand "finseq_appl" )"2" "2" expand "path_verts" )"2" "rev(p!1^(i!1,length(p!1)-1))" )"1" expand *"^" min "1" expand "rev" )"1" expand "walk_from?" )"1" "1" "walks" )"1" assert )"1" nil nil ))nil ))nil )"2" "walks" )"2" assert )nil nil ))nil )"3" "paths" )"3" expand "path_from?" )"3" "3" expand "path?" )"3" expand "finseq_appl" )"3" "3" "walk?_caret" )"3" "G!1" "i!1" "length(p!1)-1" "p!1" )"3" "1" "walk?_rev" )"1" "G!1" " p!1 ^ (i!1, length(p!1) - 1)" )"1" "1" "1" "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" "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 )"bool" sets nil )"bool" sets nil )"finseq" finite_sequences nil )nil walks nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" k_menger nil )"prewalk[T]" k_menger nil )"finseq[T]" doubletons nil )"bool" k_menger nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"finite_set[T]" ind_paths nil )"bool" sets nil )"(singleton?)" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"set[T]" paths nil )"non_empty_finite_set[T]" k_menger nil )nil application-judgement "finite_set[T]" graphs nil )"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" nil )"(strict_total_order?[real])" real_props nil )nil walks nil )"{k: nat | k <= i AND k <= j}" nil )"int" integers nil )"{k: int | k <= i AND k <= j}" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )"nat" k_menger nil )"prewalk[T]" k_menger nil )"finseq" finite_sequences nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(strict_total_order?[real])" real_props nil )nil k_menger nil )"set" sets nil )"bool" k_menger nil ))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" "del_verts(G!1, remove(w!1, W!1))" "s!1" "t!1" "w!2" )"3" "3" "3" "3" "p!1" )"3" "path?_subgraph" )"3" "G!1" "del_verts(G!1, remove(w!1, W!1))" "p!1" )"3" "1" expand "path_from?" )"1" (prop) nil nil ))nil )"2" expand "path_from?" )"2" "2" "2" expand "path?" )"2" expand "finseq_appl" )"2" "2" expand "internal_verts" )"2" "walks" )"2" expand "finseq_appl" )"2" "1" "1" "1" "1" "i!1" )"1" "1" "i!1" )"1" assert )nil nil ))nil )"2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "p!1" )"3" expand "walk_from?" )"3" "1" "1" expand "from?" )"1" nil nil ))nil ))nil )"2" "2" expand "from?" )"2" nil nil ))nil ))nil )"3" expand "walk?" )"3" expand "finseq_appl" )"3" "1" expand "verts_in?" )"1" "1" "i!1" )"1" "i!1" )"1" "1" "i!1" )"1" "x!1" )"1" assert )"1" "1" "1" expand "from?" )"1" "1" "i!1" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!1" )"2" "2" expand "from?" )"2" "2" case "i!1=length(p!1)-1" )"1" replace "1" replace "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" nil nil ))nil )"4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" "2" expand "edge?" )"2" "2" expand "del_verts" )"2" "2" "2" "v!1" )"2" "1" "1" assert )nil nil ))nil )"2" "2" "n!1" )"2" "n!1+1" )"2" assert )"2" replace "2" replace "2" "2" "1" case "n!1+1=length(p!1)-1" )"1" "1" expand "from?" )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "from?" )"2" nil nil ))nil ))nil )"3" "3" expand "from?" )"3" nil nil ))nil ))nil )"4" "4" expand "from?" )"4" 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" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" expand "path_from?" )"3" "path?_subgraph" )"3" "G!1" "del_verts(G!1, remove(w!1, W!1))" "p!1" )"3" "3" "3" "3" "graphs" )"3" assert )"3" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "graphs" )"4" assert )"4" "1" nil nil )"2" 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" "G!1" "remove(w!1,W!1)" "W!1" "s!1" "t!1" )"4" (prop)"4" (hide -1 -2 2)"4" "finite_sets" )"4" assert )"4" (skosimp*) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" k_menger nil )"bool" sets nil )"set" sets nil )"finite_set[T]" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"set" sets nil )nil k_menger nil )"bool" sep_sets nil )nil path_ops nil )nil subgraph_paths nil )"bool" paths nil )"bool" paths nil )"bool" sets nil )"(singleton?)" sets nil )"prewalk[T]" k_menger nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"finite_set[T]" k_menger nil )"int" integers nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"set" sets nil )"non_empty_finite_set[T]" k_menger nil )"finite_set[T]" k_mengernil )nil application-judgement "finite_set[T]" k_menger nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" walks nil )"finite_set[T]" ind_paths nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" subgraphs nil )"(partial_order?[set[T]])" nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"graph[T]" sep_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" sets nil ))nil ))"variabl" 3379069981"" (lemma "finite_set_induction_gen" )"" (skosimp*)"" "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1,V1,s!1,t!1) and close?(G!1,s!1,t!1,V1)))" )"" (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" "V!2" )"2" "1" "1" "V1!1" )"1" "1" "1" "finite_sets[T]" )"1" assert )"1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "same_card_subset" )"2" "card_subset" )"2" "2" "2" "V!2" "V!1" )"2" "V!1" "S!1" )"2" "V!2" "V!1" )"2" "V!1" "S!1" )"2" "1" replace "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 )nil k_menger nil )"(partial_order?[set[T]])" nil )"bool" sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil finite_sets nil )nil k_menger nil )"bool" k_menger nil )"bool" sets nil )"bool" sep_sets nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_sets_inductions"finite_sets/" )nil k_menger nil ))"put_in_tight" 3379067892"" (lemma "finite_set_induction_gen" )"" (skosimp*)"" "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1,V1,s!1,t!1) and close?(G!1,s!1,t!1,V1)))" )"" (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" "V!1" )"1" "1" "1" "V1!1" )"1" "1" "1" "finite_sets[T]" )"1" assert )"1" "1" "1" "1" 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)nil 3379064658"" (lemma "finite_set_induction_gen" )"" (skosimp*)"" "lambda W: (separates(G!1,W,s!1,t!1) implies (exists V1 : subset?(V1,W) and separates(G!1,V1,s!1,t!1) and tight?(G!1,s!1,t!1,V1)))" )"" (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" "1" (grind) nil )))))))))))))"2" (skosimp*)"2" (case "card(V!1)<card(S!1)" )"1" (inst -4 "V!1" )"1" (prop)"1" (skosimp*)"1" "V1!1" )"1" "1" "1" "finite_sets[T]" )"1" assert )"1" "1" "1" "1" nil )))))))))))))))))))))))"2" (hide-all-but (-1 1 2))"2" (lemma "same_card_subset" )"2" (inst -1 "V!1" "S!1" )"2" "2" "card_subset" )"2" "V!1" "S!1" )"2" assert )nil ))))))))))))))))))))))))))))))))))nil )nil nil ))"copied from exists tight" 3379073276"" (skosimp*)"" (expand "good?" )"" (expand "separable?" )"" (prop)"" (lemma "small_close" )"" (inst?)"" "{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" "1" (assert ) nil nil ))nil ))nil )"2" "length(w!1) = 2" )"1" assert )"1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "0" )"1" assert )"1" "1" replace -2 * lr)"1" replace -3 * lr)"1" "1" expand "edge?" )"1" expand "del_verts" )"1" 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" "1" "0" )"1" assert )"1" expand "edge?" )"1" expand "del_verts" )"1" "1" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "walk_verts_in" )"2" "1" "1" "1" expand "verts_in?" )"1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" "2" "finite_subset[T]" )"2" "2" "vert(G!1)" )"2" assert )"2" "2" 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 )"bool" k_menger nil )nil k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" sep_sets nil )"bool" walks nil )nil numbers nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"even_int" integersnil )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"finite_set[T]" k_mengernil )"bool" sets nil )"set" sets nil )"bool" walks nil )nil finite_sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil walks nil )"odd_int" integersnil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" graphs nil )"graph[T]" sep_sets nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" walks nil )"bool" finite_sets nil )"graph[T]" k_menger nil )"T" k_menger nil )"T" k_menger nil )nil k_menger nil )"bool" sep_sets nil ))nil 3379073798"" (skosimp*)"" (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" )"1" (prop)"1" (skosimp*)"1" "1" "p!1" )"1" expand "path_from?" )"1" expand "walk_from?" )"1" "1" expand "from?" )"1" (prop) nil nil ))nil )"2" expand "from?" )"2" (prop) nil nil ))nil )"3" "3" expand "walk?" )"3" expand "finseq_appl" )"3" "1" expand "verts_in?" )"1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" expand "internal_verts" )"1" expand "path?" )"1" expand "finseq_appl" )"1" "1" expand "walk?" )"1" expand "finseq_appl" )"1" expand "verts_in?" )"1" "1" "i!1" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!1" )"2" "seq(p!1)(i!1)" )"2" expand "singleton" )"2" "2" expand "intersection" )"2" expand "member" )"2" "1" replace "1" nil nil ))nil )"2" "2" "2" "seq(p!1)(i!1)" )"2" nil nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" "3" expand "from?" )"3" case "i!1=0" )"1" replace "1" "1" replace "1" nil nil ))nil )"2" case "length(p!1)=1" )"1" replace "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" case "i!1=length(p!1)-1" )"1" replace "1" "1" assert )nil nil )"2" "2" "2" replace "2" 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" "2" expand "edge?" )"2" "1" expand "path?" )"1" expand "finseq_appl" )"1" "1" "n!1" "n!1+1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "path?" )"2" expand "finseq_appl" )"2" "2" expand "walk?" )"2" expand "finseq_appl" )"2" "2" "n!1" )"2" assert )"2" expand "edge?" )"2" "2" expand "del_verts" )"2" "2" "2" "2" "v!1" )"2" "2" expand "internal_verts" )"2" expand "finseq_appl" )"2" expand "dbl" )"2" "1" "1" "v!1" )"1" expand "intersection" )"1" expand "member" )"1" expand "singleton" )"1" "1" "1" replace "1" nil nil ))nil )"2" "n!1" )"2" assert )"2" "n!1" )"2" case "n!1=0" )"1" replace "1" "1" "1" expand "from?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "v!1" )"2" expand "singleton" )"2" expand "intersection" )"2" expand "member" )"2" "2" "1" replace "1" nil nil ))nil )"2" "n!1+1" )"2" "1" assert )nil nil )"2" case "n!1+1=length(p!1)-1" )"1" replace "1" "1" expand "from?" )"1" "1" replace "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 1)"2" (inst -2 "x!1" )"2" (prop)"2" (skosimp*)"2" "2" "p!1" )"2" expand "path_from?" )"2" expand "walk_from?" )"2" "1" expand "from?" )"1" (prop) nil nil ))nil )"2" expand "from?" )"2" (prop) nil nil ))nil )"3" "3" expand "walk?" )"3" expand "finseq_appl" )"3" "1" expand "verts_in?" )"1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" expand "internal_verts" )"1" expand "path?" )"1" expand "finseq_appl" )"1" "1" expand "walk?" )"1" expand "verts_in?" )"1" expand "finseq_appl" )"1" "1" "i!1" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!1" )"2" "seq(p!1)(i!1)" )"2" expand "singleton" )"2" "2" expand "intersection" )"2" expand "member" )"2" "1" replace "1" nil nil ))nil )"2" "2" "2" "seq(p!1)(i!1)" )"2" nil nil ))nil ))nil ))nil )"3" "3" "i!1" )"3" "3" expand "from?" )"3" case "i!1=0" )"1" replace "1" "1" replace "1" nil nil ))nil )"2" case "length(p!1)=1" )"1" replace "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" case "i!1=length(p!1)-1" )"1" replace "1" "1" assert )nil nil )"2" "2" "2" replace "2" 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" "2" expand "edge?" )"2" "1" expand "path?" )"1" expand "finseq_appl" )"1" "1" "n!1" "n!1+1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "path?" )"2" "2" expand "walk?" )"2" expand "finseq_appl" )"2" "2" "n!1" )"2" assert )"2" expand "edge?" )"2" "2" expand "del_verts" )"2" "2" "2" "2" "v!1" )"2" "2" expand "internal_verts" )"2" expand "dbl" )"2" "1" "1" "v!1" )"1" expand "intersection" )"1" expand "member" )"1" expand "singleton" )"1" "1" "1" replace "1" nil nil ))nil )"2" "n!1" )"2" assert )"2" "n!1" )"2" case "n!1=0" )"1" replace "1" "1" "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" "2" "v!1" )"2" expand "singleton" )"2" expand "intersection" )"2" expand "member" )"2" "2" "1" replace "1" nil nil ))nil )"2" "n!1+1" )"2" "1" assert )nil nil )"2" case "n!1+1=length(p!1)-1" )"1" replace "1" "1" expand "from?" )"1" "1" replace "1" replace "1" 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 )"bool" k_menger nil )"bool" sets nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" k_menger nil )"prewalk[T]" k_menger nil )"posint" nil )"set[T]" doubletons nil )"bool" graphs nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" walks nil )"set" sets nil )"bool" paths nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"(singleton?)" sets nil )"bool" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"[T, T -> boolean]" equalities nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"finite_set[T]" nil )"non_empty_finite_set[T]" k_menger nil )nil application-judgement "finite_set[T]" graphs nil )"even_int" integersnil )"finite_set[T]" ind_paths nil )"graph[T]" sep_sets nil )"bool" walks nil )"bool" walks nil )"bool" paths nil )"nat" k_menger nil )"prewalk[T]" k_menger nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil k_menger nil )"bool" sets nil )"bool" sep_sets nil ))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" )"" "" "" expand "member" )"" "" "x!1" )"" expand "singleton" )"" "" expand "internal_verts" )"" expand "finseq_appl" )"" "" expand "verts_in?" )"" "i!1" )"" replace "" 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 )"bool" sets nil )"bool" k_menger nil )nil k_menger nil )"bool" paths nil )"bool" paths nil )"bool" walks nil )"bool" walks nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"non_empty_finite_set[T]" k_menger nil )"(singleton?)" sets nil )"bool" sets nil )"finite_set[T]" ind_paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )"[below[length(fs)] -> T]" finite_sequencesnil )"set" sets nil )"bool" sets nil ))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]]" )"" "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" )"" "x!2" )"" "" "w!1" "x!1" )"" "" "1" replace -2 -4 lr)"1" "dbl_eq" )"1" "w!1" "x!3" "y!1" "x!1" )"1" "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 )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil k_menger nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"non_empty_finite_set[T]" k_menger nil )"(nonempty?)" sets nil )"bool" sets nil )nil application-judgement "finite_set[T]" k_menger nil )"set[doubleton[T]]" complem nil )"T" k_menger nil )"finite_set[T]" k_menger nil )"bool" sets nil )nil doubletons nil )"bool" sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil complem nil )nil finite_sets nil ))nil ))"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" "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" "2" expand "verts_in?" )"2" "length(w!1)-1" )"2" expand "del_verts" )"2" expand "difference" )"2" expand "member" )"2" "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 )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil k_menger nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" walks nil )"bool" walks nil )"bool" walks nil )"set" sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )nil finite_sets nil )"bool" sets nil )"set[T]" paths nil )"graph[T]" sep_sets nil )"bool" finite_sets nil ))nil 3377812958 ("" (subtype-tcc) nil nil ) nil nil ))"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" "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" "3" expand "del_verts" )"3" expand "walk_from?" )"3" "3" expand "walk?" )"3" "3" "3" expand "verts_in?" )"3" expand "difference" )"3" expand "member" )"3" "length(w!2)-1" )"3" "3" replace "3" replace "3" 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 )"(nonempty?)" sets nil )"finite_set[doubleton[T]]" k_menger nil )"set" sets nil )"Subgraph(G)" subgraphs nil )"finite_set[T]" k_menger nil )"bool" walks nil )"bool" walks nil )"(total_order?[real])" nil )"int" integers nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" walks nil )"graph[T]" sep_sets nil )"set[T]" paths nil )"set" sets nil )"graph" k_menger nil )"bool" finite_sets nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil k_menger nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"bool" sets nil ))nil 3377812958 ("" (subtype-tcc) nil nil ) nil nil ))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" )"" "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 )"bool" sets nil )"finite_set[T]" k_menger nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" finite_sets nil )"graph[T]" sep_sets nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )nil k_menger nil )nil walks nil )"bool" sep_sets nil )"set[T]" paths nil )"set" sets nil )"bool" sets nil ))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 )"bool" sets nil )"(nonempty?)" sets nil )"bool" k_menger nil )"Subgraph(G)" subgraphs nil )"graph" k_menger nil )"graph" k_menger nil )"bool" sets nil ))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 )"bool" sets nil )"(nonempty?)" sets nil )"bool" k_menger nil )"Subgraph(G)" subgraphs nil )"graph" k_menger nil )"graph" k_menger nil )"bool" sets nil ))nil ))"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" "1" expand "intersection" )"1" expand "member" )"1" "1" "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" "1" "p!1(1)" )"1" "1" expand "finseq_appl" )"1" "1" "1" "paths" )"1" assert )"1" "1" "0" "1" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )"2" case "length(p!1)=1" )"1" replace "1" assert )"1" "1" expand "good?" )"1" expand "separable?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"3" "0" )"3" assert )"3" case "length(p!1)=1" )"1" replace "1" assert )"1" "1" expand "good?" )"1" expand "separable?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"4" "0" )"4" assert )"4" case "length(p!1)=1" )"1" replace "1" assert )"1" "1" expand "good?" )"1" expand "separable?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "p!1^(0,1)" )"1" expand "path_from?" )"1" "1" expand "from?" )"1" "1" "1" expand "path?" )"1" expand "finseq_appl" )"1" "1" "1" expand "^" )"1" expand "walk?" )"1" "1" "0" )"1" "p!1" )"1" assert )"1" case "length(p!1)>1" )"1" assert )"1" expand "walk_from?" )"1" expand "finseq_appl" )"1" expand "del_verts" )"1" expand "walk?" )"1" expand "finseq_appl" )"1" expand "min" )"1" "1" expand "verts_in?" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1" )"1" case "i!1=0" )"1" replace "1" "0" )"1" "1" "1" expand "separates" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!1=1" )"1" replace "1" "1" replace "1" "1" "seq(p!1)(1)" )"1" "1" expand "singleton" )"1" "1" assert )"1" expand "internal_verts" )"1" "1" )"1" assert )"1" case "length(p!1)=2" )"1" replace "1" "1" expand "good?" )"1" "1" expand "separable?" )"1" "1" "1" "1" expand "finseq_appl" )"1" "0" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "finseq_appl" )"2" 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 )"2" "2" case "n!1=0" )"1" replace "1" assert )"1" expand "edge?" "1" "1" expand "edge?" "1" assert )nil nil ))nil )"2" expand "edge?" )"2" assert )nil nil ))nil )"3" "3" expand "dbl" )"3" "1" "1" "1" expand "separates" )"1" "1" replace "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "good?" )"2" expand "separable?" )"2" "2" "2" "v!1" )"2" "2" "1" expand "singleton" )"1" replace "1" replace "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" expand "singleton" )"2" expand "internal_verts" )"2" "1" )"2" "1" assert )nil nil )"2" case "length(p!1)=2" )"1" replace "1" "1" "1" replace "1" assert )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 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "finseq_appl" )"2" case "length(p!1)=1" )"1" replace "1" assert )"1" "1" "1" "1" replace "1" assert )"1" expand "good?" )"1" expand "separable?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" assert )"2" expand "good?" )"2" expand "separable?" )"2" 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 ))nil ))nil ))nil ))nil )"2" expand *"^" "min" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "paths" )"3" assert )"3" "3" "1" )nil nil ))nil ))nil ))nil ))nil )"4" "4" "paths" )"4" assert )"4" "4" "1" )nil nil ))nil ))nil ))nil ))nil )"5" "5" "paths" )"5" assert )"5" "5" "1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "good?" )"2" expand "separable?" )"2" "2" "2" "paths" )"2" assert )"2" "2" "p!1" )"2" case "length(p!1)=1" )"1" replace "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 ))nil ))nil ))nil ))nil )"2" (reveal -3)"2" "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 )nil k_menger nil )nil finite_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"graph" k_menger nil )"nat" graphs nil )"finite_set[T]" nil )"finite_set" finite_sets nil )"non_empty_finite_set[T]" k_menger nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"(total_order?[real])" nil )"bool" k_menger nil )"set" sets nil )"(nonempty?)" sets nil )"set" sets nil )"finite_set[T]" k_menger nil )"Subgraph(G)" subgraphs nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"prewalk[T]" k_menger nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(strict_total_order?[real])" real_props nil )"finseq" finite_sequences nil )"posint" nil )"bool" sep_sets nil )"odd_int" integersnil )"finite_set[T]" ind_paths nil )"bool" sets nil )"(singleton?)" sets nil )"odd_int" integers nil )"finite_set[T]" k_mengernil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{k: posint | k <= i AND k <= j}" nil )"{k: nat | k <= i AND k <= j}" nil )nil application-judgement "finite_set[T]" graphs nil )"int" integers nil )nil application-judgement "finite_set[T]" k_menger nil )"bool" walks nil )"bool" graphs nil )"bool" walks nil )"bool" paths nil )"bool" walks nil )"bool" paths nil )"even_int" integersnil )"bool" k_menger nil )"bool" sep_sets nil )nil naturalnumbers nil )"non_empty_finite_set[T]" k_menger nil )"graph[T]" sep_sets nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"set[T]" paths nil )"graph" k_menger nil )"bool" sets nil )"bool" k_menger nil )nil finite_sets nil ))"try2" 3378120234"" (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" (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)nil 3378041558"" (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)" )"" (prop)"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" expand "difference" )"1" expand "member" )"1" expand "Hverts" )"1" expand "del_verts" )"1" expand "path_verts" )"1" "1" "w!1" )"1" "1" "1" expand "separates" )"1" "1" replace -1 1 lr)"1" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil )"5"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.794Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
