Quelle h_menger.prf
Sprache: Lisp
(h_mengernil 3251049132"" (skosimp*)"" case "(FORALL (zz: T): NOT separates(G!1,singleton(zz),s!1,t!1))" )"1" (inst -1 "z!1" )"1" (expand "separates" 1)"1" (expand "singleton" )"1" (assert )"1" (skosimp*)"1" (lemma "walk_to_path_from" )"1" (inst?)"1" (assert )"1" (hide -2)"1" (skosimp*)"1" "del_verts(G!1, {y: T | y = z!1}) = del_vert(G!1, z!1)" )"1" (hide -1)"1" (inst + "p!1" ) nil nil )) nil )"2" (hide -1 -2 -3 4)"2" "1" "1" "1" expand "del_verts" )"1" expand "del_vert" )"1" "1" (inst - "z!1" ) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[T]" )"2" "2" expand "singleton" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "1" expand "del_verts" )"1" expand "del_vert" )"1" expand "difference" )"1" expand "remove" )"1" expand "member" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[T]" )"2" "2" expand "singleton" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" "finite_singleton[T]" )"3" "3" expand "singleton" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "finite_singleton[T]" )"3" "3" expand "singleton" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "finite_singleton[T]" )"2" (inst?)"2" (expand "singleton" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (hide -2)"2" (expand "sep_num" )"2" (lemma "min_sep_set_card" )"2" (inst?)"2" (assert )"2" (rewrite "card_singleton" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(singleton?)" sets nil )"bool" sets nil )"bool" sep_sets nil )"bool" finite_sets 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil h_menger nil )"non_empty_finite_set" finite_sets nil )nil path_ops nil )"set" sets nil )"bool" sets nil )"set" sets nil )nil finite_sets nil )"graph[T]" graph_ops 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 )"T" h_menger nil )nil sep_sets nil )"(total_order?[real])" nil )nil finite_sets nil )"T" h_menger nil )"T" h_menger nil )"graph[T]" h_menger nil )"nat" sep_sets nil ))nil ))nil 3559572389"" (skosimp*)"" (auto-rewrite finseq_appl)"" (expand "in?" )"" (flatten)"" (lemma "path_not_thru" )"" (inst?)"" (assert )"" (inst -1 "w1!1" )"" (expand "disjoint?" )"" (flatten)"" (assert )"" (skosimp*)"" "path2" "add1(gen_seq2(G!1,s!1,w1!1),t!1)" )"" (case "independent?(pn!1,path2)" )"1" "path_from_l" )"1" "1" assert )"1" expand "path_from?" )"1" "1" "path?_del_vert" )"1" "1" assert )"1" case "path?[T](G!1, path2) AND from?[T](path2, s!1, t!1)" )"1" "1" "pn!1" "path2" )"1" assert )nil nil ))nil ))nil )"2" "2" replace -1 * rl)"2" "2" "1" expand "path?" )"1" "1" "walk?_add1" )"1" "1" assert )"1" expand "gen_seq2" )"1" "1" expand "walk?" )"1" expand "verts_in?" )"1" "1" expand "edge?" )"1" assert )"1" rewrite "dbl_comm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "i!1" )"2" "j!1" )"2" expand "add1" )"2" expand "gen_seq2" )"2" "2" "2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "add1" )"2" expand "from?" )"2" expand "gen_seq2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "independent?" )"2" "2" replace -6 * rl)"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "2" "2" expand "path_from?" )"2" expand "path?" )"2" expand "walk?" )"2" "2" "2" expand "verts_in?" )"2" "2" expand "del_vert" )"2" expand "remove" )"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 h_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" ind_paths nil )"graph[T]" graph_ops nil )"bool" paths nil )nil path_ops nil )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil walks nil )"int" integers nil )"bool" graphs nil )nil doubletons nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"posint" nil )"bool" walks nil )"bool" walks nil )"bool" paths nil )nil paths nil )"set" sets nil )"(strict_total_order?[real])" real_props 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 )"prewalk" walks nil )"bool" walks nil )nil walks nil )"Seq(G)" walks nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" h_menger nil )nil h_menger nil )"bool" meng_scaff_defs nil ))nil )nil 3251049132"" (skosimp*)"" (expand "in?" )"" (flatten)"" (lemma "path_not_thru" )"" (inst?)"" (assert )"" (inst -1 "w1!1" )"" (expand "disjoint?" )"" (flatten)"" (assert )"" (skosimp*)"" "path2" "add1(gen_seq2(G!1,s!1,w1!1),t!1)" )"" (case "independent?(pn!1,path2)" )"1" (lemma "path_from_l" )"1" "1" assert )"1" expand "path_from?" )"1" "1" "path?_del_vert" )"1" "1" assert )"1" case "path?[T](G!1, path2) AND from?[T](path2, s!1, t!1)" )"1" "1" "pn!1" "path2" )"1" assert )nil nil ))nil ))nil )"2" "2" replace -1 * rl)"2" "2" "1" expand "path?" )"1" "1" "walk?_add1" )"1" "1" assert )"1" expand "gen_seq2" )"1" "1" expand "walk?" )"1" expand "verts_in?" )"1" "1" expand "edge?" )"1" assert )"1" rewrite "dbl_comm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "2" "2" "i!1" )"2" "j!1" )"2" expand "add1" )"2" expand "gen_seq2" )"2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "add1" )"2" expand "from?" )"2" expand "gen_seq2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 -4 -5 8)"2" expand "independent?" )"2" "2" replace -6 * rl)"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "2" "2" expand "path_from?" )"2" expand "path?" )"2" expand "walk?" )"2" "2" "2" expand "verts_in?" )"2" "2" expand "del_vert" )"2" expand "remove" )"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 )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )"Seq(G)" walks nil )nil walks nil )"bool" walks nil )"prewalk" walks nil )nil walks nil )nil paths nil )"bool" paths nil )"bool" walks nil )"bool" walks nil )nil doubletons nil )"bool" graphs nil )nil walks nil )nil path_ops nil )"bool" paths nil )"graph[T]" graph_ops nil )"bool" ind_paths nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil ))nil ))nil 3251049132"" (skosimp*)"" (lemma "min_sep_set_seps" )"" (inst?)"" (assert )"" (expand "sep_num" )"" (lemma "min_sep_set_card" )"" (inst?)"1" (assert )"1" (hide -2 2)"1" (expand "separates" )"1" (skosimp*)"1" (split 1)"1" (propax) nil nil )"2" (propax) nil nil )"3" (skosimp*)"3" (inst?)"3" expand "walk_from?" )"3" "3" assert )"3" expand "walk?" )"3" "1" "1" expand "verts_in?" )"1" "1" "1" "1" "1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" expand "del_vert" )"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" expand "finseq_appl" )"2" expand "edge?" )"2" "2" assert )"2" "2" assert )"2" "2" expand "del_verts" )"2" "2" "1" "edges_del_vert" )"1" "1" assert )nil nil )"2" "2" assert )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 )"2" (hide -1 2)"2" (expand "del_vert" )"2" (expand "remove" )"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" (hide -1 4)"3" (expand "del_vert" )"3" (expand "remove" )"3" (expand "member" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil h_menger nil )nil sep_sets nil )"(total_order?[real])" nil )nil sep_sets nil )"bool" sep_sets 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 )"bool" walks nil )nil application-judgement "finite_set[T]" h_menger nil )"bool" graphs nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil graph_ops nil )"[below[length(fs)] -> T]" finite_sequencesnil )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 )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"set" sets nil )"bool" walks nil )"int" integers nil )"bool" walks nil )"bool" finite_sets nil )"finite_set[T]" sep_sets nil )"T" h_menger nil )"graph[T]" graph_ops nil )"graph[T]" h_menger nil )"T" h_menger nil )"T" h_menger nil )"nat" sep_sets 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 ))nil ))nil 3251049132"" (skosimp*)"" (expand "del_vert" )"" (expand "separates" )"" (expand "singleton" )"" (expand "dbl" )"" (flatten)"" (assert )"" (skosimp*)"" (inst?)"" (expand "walk_from?" )"" (flatten)"" (assert )"" (expand "walk?" )"" (flatten)"" "1" expand "verts_in?" )"1" "1" "1" expand "del_verts" )"1" expand "difference" )"1" expand "remove" )"1" expand "member" )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" "2" assert )"2" "2" assert )"2" expand "del_verts" )"2" "2" "2" assert )"2" "1" expand "dbl" )"1" "ajm!1" )nil nil ))nil )"2" "2" assert )"2" "z!1" )"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 )"graph[T]" graph_ops nil )"(singleton?)" sets nil )"bool" walks nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"bool" graphs nil )nil application-judgement "finite_set[T]" h_menger nil )"bool" walks nil )"set" sets nil )"bool" sets 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 )"set" sets nil )"graph[T]" sep_sets nil )"bool" walks nil )nil walks nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil finite_sequences nil )nil h_menger nil )nil nat_types nil )nil naturalnumbers nil )"set[T]" doubletons nil )"bool" sep_sets nil ))nil ))nil 3251049132"" (skosimp*)"" (expand "induction_step" ) (("" (propax) nil nil )) nil )) nil )"bool" meng_scaff_prelude nil )) nil ))nil 3251049132"" (skosimp*)"" (expand "separable?" )"" (flatten)"" (assert )"" (expand "edge?" )"" (expand "del_vert" )"" (assert )"" (expand "remove" )"" (expand "member" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sep_sets nil )"graph[T]" graph_ops nil )"set" sets nil )"bool" sets nil )"finite_set" finite_sets nil )"bool" graphs nil )nil application-judgement "finite_set[T]" h_menger nil ))nil ))nil 3251049132 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil h_menger nil )nil finite_sequences nil )nil walks nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3251049132 ("" (subtype-tcc) nil nil )"boolean" notequal nil )nil h_menger nil )"bool" graphs nil )nil application-judgement "finite_set[T]" h_menger nil ))nil ))nil 3251049132 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"boolean" notequal nil )nil h_menger nil )"bool" graphs nil )nil application-judgement "finite_set[T]" h_menger nil ))nil ))nil 3251049132"" (induct "p" 1 "graph_induction_walk" )"1" (skosimp*)"1" (inst -1 "trunc1(w!1)" )"1" (rewrite "l_trunc1" )"1" (assert )"1" case "NOT edge?(G!1)(seq(w!1)(length(w!1) - 3), t!1) AND edge?(G!1)(seq(w!1)(length(w!1)-2), t!1)") "1" (inst + "length(w!1)-2" )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (inst -1 "G!1" "t!1" )"2" (case "length(w!1) = 4" )"1" (hide -2)"1" (replace -1)"1" (hide -1)"1" (assert )"1" (inst + "1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "trunc1" )"2" (expand * "^" min empty_seq)"2" (skosimp*)"2" (inst + "j!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )nil walks nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"even_int" integersnil )"finseq" finite_sequences nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil walks nil )"prewalk" walks nil )"prewalk[T]" h_menger nil )"(total_order?[real])" nil )nil walk_inductions nil )nil h_menger nil )nil defined_types nil )"bool" graphs nil )NOT const-decl "[bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil walks 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" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3251049132"" (skosimp*)"" (lemma "path_not_thru" )"" (inst?)"" (assert )"" (inst?)"" (expand "edge?" )"" (flatten)"" (assert )"" (skosimp*)"" "path2" "add1(gen_seq2(G!1,s!1,x!1),t!1)" )"" (inst + "path2" "pn!1" )"" (expand "path_from?" )"" (flatten)"" (expand "from?" )"" "" assert )"" "path?_del_vert" )"" "" assert )"" replace -2 * rl)"" "" "1" rewrite "path?_add1" )"1" "1" rewrite "path?_gen_seq2" )nil nil ))nil )"2" expand "gen_seq2" )"2" expand "edge?" )"2" nil nil ))nil ))nil )"3" expand "verts_of" "3" expand "finseq_appl" )"3" expand "gen_seq2" "3" "3" "3" "3" expand "separable?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "add1" )"2" expand "gen_seq2" )"2" nil nil ))nil ))nil )"3" expand "add1" )"3" nil nil ))nil )"4" expand "independent?" )"4" "4" expand "add1" )"4" expand "gen_seq2" )"4" "4" expand "path?" )"4" expand "walk?" )"4" "4" "4" expand "verts_in?" )"4" expand "finseq_appl" )"4" "i!1" "j!1" )"1" "1" expand "del_vert" )"1" expand "remove" )"1" expand "member" )"1" "1" "j!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "j!1" )"2" expand "del_vert" )"2" expand "remove" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "i!1" )"3" 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 h_menger nil )nil application-judgement "finite_set[T]" h_menger nil )"bool" graphs nil )"Seq(G)" walks nil )nil walks nil )"bool" walks nil )"prewalk" 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 )"bool" paths nil )"bool" walks nil )"int" integers nil )"finite_set[T]" walks nil )"bool" sep_sets nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil paths nil )nil paths nil )"bool" paths nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"nat" h_menger nil )"prewalk[T]" h_menger nil )"nat" h_menger nil )nil naturalnumbers nil )"graph[T]" graph_ops nil )"bool" sets nil )"set" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" walks nil )"bool" ind_paths nil )nil path_ops 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 )nil h_menger nil ))nil ))nil 3559573458"" (skosimp*)"" (auto-rewrite finseq_appl)"" (lemma "sep_num_gt_0" )"" (inst?)"" (assert )"" (skosimp*)"" (lemma "walk_to_path_from" )"" (inst?)"" (assert )"" (skosimp*)"" (hide -2)"" (case "length(p!1) <= 3" )"1" (lemma "path_from_l" )"1" (inst?)"1" assert )"1" expand "separable?" )"1" "1" assert )"1" expand "path_from?" -)"1" expand "path?" )"1" expand "walk?" )"1" expand "verts_in?" )"1" "1" "1" )"1" "0" )"1" "1" )"1" assert )"1" expand "from?" )"1" "1" "length(p!1) = 3" )"1" assert )"1" "short_path_case" )"1" "1" "1" assert )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" case " (EXISTS (j: nat): j > 1 AND j < length(p!1)-1 AND NOT edge?(G!1)(seq(p!1)(j - 1), t!1)AND edge?(G!1)(seq(p!1)(j), t!1))") "1" (skosimp*)"1" case "vert(G!1)(seq(p!1)(j!1 - 1)) AND vert(G!1)(seq(p!1)(j!1)) AND ") "1" "1" case "separates(G!1,dbl(seq(p!1)(j!1-1),seq(p!1)(j!1)),s!1,t!1)" )"1" "prelude" )"1" "G!1" "s!1" "t!1" "_" "_" )"1" "1" assert )"1" expand "in?" )"1" "1" (propax) nil nil )"2" "2" "adjacent_fact" )"2" "G!1" "s!1" "t!1" "seq(p!1)(j!1)" "seq(p!1)(j!1-1)" )"2" assert )"2" expand "in?" )"2" expand "disjoint?" )"2" "2" assert )"2" rewrite "dbl_comm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" expand "separates" )"2" expand "disjoint?" )"2" "2" expand "dbl" 1 (1 2))"2" assert )"2" "2" "walk_to_path_from" )"2" "2" assert )"2" "2" "2" case "edge?(G!1)(s!1,seq(p!1)(j!1-1))" )"1" "Pscat" "add1(add1(gen_seq2(G!1,s!1,seq(p!1)(j!1-1)),seq(p!1)(j!1)),t!1)" )"1" case "independent?(p!2,Pscat)" )"1" "p!2" "Pscat" )"1" assert )"1" expand "path_from?" )"1" "1" assert )"1" "path?_del_verts" )"1" "1" assert )"1" "1" replace "1" "1" "1" expand "path?" "1" "1" expand "walk?" )"1" "1" "j!1-1" )"1" assert )"1" rewrite "path?_add1" )"1" "1" rewrite "path?_add1" )"1" "1" rewrite "path?_gen_seq2" )nil nil ))nil )"2" expand "gen_seq2" )"2" nil nil ))nil )"3" expand "verts_of" "3" expand "gen_seq2" "3" "3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "add1" )"2" nil nil ))nil )"3" "3" expand "verts_of" "3" expand "add1" "3" expand "gen_seq2" "3" "3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "from?" )"2" expand "add1" )"2" expand "gen_seq2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" expand "path_from?" )"2" expand "path?" )"2" expand "walk?" )"2" "2" "2" expand "independent?" )"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "2" expand "verts_in?" )"2" expand "del_verts" )"2" expand "difference" )"2" expand "member" )"2" "1" "1" expand "dbl" )"1" 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 )"2" case "(FORALL (v:T): vert(G!1)(v) AND v /= s!1 AND v /= t!1 ") "1" "seq(p!1)(j!1-1)" )"1" assert )"1" "sep_num_le1" )"1" "del_vert(G!1, seq(p!1)(j!1 - 1))" "seq(p!1)(j!1)" "s!1" "t!1" )"1" expand "separable?" )"1" assert )"1" "separable?_del" )"1" "G!1" "s!1" "t!1" "seq(p!1)(j!1 - 1)" )"1" assert )"1" "1" assert )"1" "1" "1" expand "del_vert" "1" expand "remove" )"1" "1" expand "member" )"1" "separates_del" )"1" "1" assert )"1" "prelude" )"1" "1" assert )"1" expand "in?" )"1" expand "disjoint?" )"1" expand "edge?" )"1" rewrite "dbl_comm" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "del_vert" "2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil )"3" expand "edge?" )"3" expand "del_vert" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "induction_step" )"2" "del_vert(G!1,v!1)" )"2" rewrite "size_del_vert" )"2" assert )"2" "s!1" "t!1" )"2" "sep_num_del" )"2" "2" assert )"2" "separable?_del" )"2" "2" assert )"2" "2" assert )"2" "2" "p1!1" "p2!1" )"2" assert )"2" expand "path_from?" )"2" "2" assert )"2" "path?_del_vert" )"2" "2" assert )"2" "path?_del_vert" )"2" "G!1" "v!1" "p2!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "path_from?" )"2" "2" expand "from?" )"2" "2" expand "path?" )"2" expand "walk?" )"2" expand "verts_in?" )"2" "2" "j!1" )"2" "j!1-1" )"1" "j!1-1" )"1" "j!1" )"1" assert )"1" expand "disjoint?" )"1" "j!1-1" "j!1" )"1" "j!1-1" "0" )"1" "j!1-1" "length(p!1)-1" )"1" "j!1" "0" )"1" "j!1" "length(p!1)-1" )"1" assert )"1" expand "separable?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (assert ) nil nil ))nil ))nil )"2" (lemma "seq_j" )"2" "2" "2" assert )"2" expand "path_from?" )"2" expand "from?" )"2" "2" assert )"2" "p!1" "t!1" )"2" assert )"2" expand "separable?" )"2" "2" assert )"2" "1" "1" "j!1" )"1" assert )"1" case "j!1 = 1" )"1" replace "1" "1" assert )"1" "short_path_case" )"1" "G!1" "s!1" "t!1" "seq(p!1)(1)" )"1" assert )"1" expand "path?" "1" "1" expand "walk?" )"1" "1" expand "verts_in?" )"1" "1" )"1" assert )"1" "0" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "j!1 = length(p!1) - 1" )"1" replace "1" "1" assert )"1" expand "path?" "1" "1" expand "walk?" )"1" "1" "length(p!1)-2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "path?" "2" "2" expand "walk?" )"2" "2" "length(p!1)-2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 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" reals nil )"bool" sep_sets nil )"bool" paths nil )"bool" walks 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 )"bool" walks nil )nil h_menger nil )"even_int" integersnil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )"int" integers nil )"bool" walks nil )"bool" paths nil )"(total_order?[real])" nil )nil paths nil )nil h_menger nil )"prewalk[T]" h_menger nil )"posint" nil )"nat" sep_sets nil )"graph[T]" graph_ops nil )nil h_menger nil )"non_empty_finite_set" finite_sets nil )"set" sets nil )nil h_menger nil )nil sep_set_lems nil )nil h_menger nil )nil path_ops nil )nil graph_ops nil )"bool" meng_scaff_prelude nil )"prewalk" walks nil )nil walks nil )"Seq(G)" walks nil )"bool" sets nil )"prewalk[T]" h_menger nil )"nat" h_menger nil )"set" sets nil )nil paths nil )nil paths nil )"finite_set[T]" walks nil )nil path_ops nil )"bool" ind_paths nil )"graph[T]" sep_sets nil )nil meng_scaff_prelude nil )"nat" h_menger nil )"bool" meng_scaff_defs nil )nil doubletons nil )nil h_menger nil )"bool" sep_sets nil )"bool" finite_sets nil )nil application-judgement "finite_set[T]" h_menger nil )"bool" meng_scaff_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" graphs nil )nil path_ops nil )"(strict_total_order?[real])" real_props nil )nil sep_set_lems nil )nil h_menger nil ))nil )nil 3251049132"" (skosimp*)"" (lemma "sep_num_gt_0" )"" (inst?)"" (assert )"" (skosimp*)"" (lemma "walk_to_path_from" )"" (inst?)"" (assert )"" (skosimp*)"" (hide -2)"" (case "length(p!1) <= 3" )"1" (lemma "path_from_l" )"1" (inst?)"1" (assert )"1" expand "separable?" )"1" "1" assert )"1" expand "path_from?" -)"1" expand "path?" )"1" expand "walk?" )"1" expand "verts_in?" )"1" "1" "1" )"1" "0" )"1" "1" )"1" assert )"1" expand "from?" )"1" "1" "length(p!1) = 3" )"1" assert )"1" "short_path_case" )"1" "1" "1" assert )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" case " (EXISTS (j: nat): j > 1 AND j < length(p!1)-1 AND NOT edge?(G!1)(seq(p!1)(j - 1), t!1)AND edge?(G!1)(seq(p!1)(j), t!1))") "1" (skosimp*)"1" case "vert(G!1)(seq(p!1)(j!1 - 1)) AND vert(G!1)(seq(p!1)(j!1)) AND ") "1" "1" case "separates(G!1,dbl(seq(p!1)(j!1-1),seq(p!1)(j!1)),s!1,t!1)" )"1" "prelude" )"1" "G!1" "s!1" "t!1" "_" "_" )"1" "1" assert )"1" expand "in?" )"1" "1" (propax) nil nil )"2" "2" "adjacent_fact" )"2" "G!1" "s!1" "t!1" "seq(p!1)(j!1)" "seq(p!1)(j!1-1)" )"2" assert )"2" expand "in?" )"2" expand "disjoint?" )"2" "2" assert )"2" rewrite "dbl_comm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" expand "separates" )"2" expand "disjoint?" )"2" "2" expand "dbl" 1 (1 2))"2" assert )"2" "2" "walk_to_path_from" )"2" "2" assert )"2" "2" "2" case "edge?(G!1)(s!1,seq(p!1)(j!1-1))" )"1" "Pscat" "add1(add1(gen_seq2(G!1,s!1,seq(p!1)(j!1-1)),seq(p!1)(j!1)),t!1)" )"1" case "independent?(p!2,Pscat)" )"1" "p!2" "Pscat" )"1" assert )"1" expand "path_from?" )"1" "1" assert )"1" "path?_del_verts" )"1" "1" assert )"1" "1" replace "1" "1" "1" expand "path?" "1" "1" expand "walk?" )"1" "1" "j!1-1" )"1" assert )"1" rewrite "path?_add1" )"1" "1" rewrite "path?_add1" )"1" "1" rewrite "path?_gen_seq2" )nil nil ))nil )"2" expand "gen_seq2" )"2" nil nil ))nil )"3" expand "verts_of" "3" expand "gen_seq2" "3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "add1" )"2" nil nil ))nil )"3" "3" expand "verts_of" "3" expand "add1" "3" expand "gen_seq2" "3" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "from?" )"2" expand "add1" )"2" expand "gen_seq2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "2" expand "path_from?" )"2" expand "path?" )"2" expand "walk?" )"2" "2" "2" expand "independent?" )"2" "2" expand "add1" )"2" expand "gen_seq2" )"2" "2" expand "verts_in?" )"2" expand "del_verts" )"2" expand "difference" )"2" expand "member" )"2" "1" "1" expand "dbl" )"1" 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 )"2" case "(FORALL (v:T): vert(G!1)(v) AND v /= s!1 AND v /= t!1 ") "1" "seq(p!1)(j!1-1)" )"1" assert )"1" "sep_num_le1" )"1" "del_vert(G!1, seq(p!1)(j!1 - 1))" "seq(p!1)(j!1)" "s!1" "t!1" )"1" expand "separable?" )"1" assert )"1" "separable?_del" )"1" "G!1" "s!1" "t!1" "seq(p!1)(j!1 - 1)" )"1" assert )"1" "1" assert )"1" "1" "1" expand "del_vert" "1" expand "remove" )"1" "1" expand "member" )"1" "separates_del" )"1" "1" assert )"1" "prelude" )"1" "1" assert )"1" expand "in?" )"1" expand "disjoint?" )"1" expand "edge?" )"1" rewrite "dbl_comm" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "del_vert" "2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil )"3" expand "edge?" )"3" expand "del_vert" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "induction_step" )"2" "del_vert(G!1,v!1)" )"2" rewrite "size_del_vert" )"2" assert )"2" "s!1" "t!1" )"2" "sep_num_del" )"2" "2" assert )"2" "separable?_del" )"2" "2" assert )"2" "2" assert )"2" "2" "p1!1" "p2!1" )"2" assert )"2" expand "path_from?" )"2" "2" assert )"2" "path?_del_vert" )"2" "2" assert )"2" "path?_del_vert" )"2" "G!1" "v!1" "p2!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "j!1" )"3" (assert ) nil nil ))nil ))nil ))nil )"2" "2" expand "path_from?" )"2" "2" expand "from?" )"2" "2" expand "path?" )"2" expand "walk?" )"2" expand "verts_in?" )"2" "2" "j!1" )"1" "j!1-1" )"1" "j!1-1" )"1" "j!1" )"1" assert )"1" expand "disjoint?" )"1" "j!1-1" "j!1" )"1" "j!1-1" "0" )"1" "j!1-1" "length(p!1)-1" )"1" "j!1" "0" )"1" "j!1" "length(p!1)-1" )"1" assert )"1" expand "separable?" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil )"4" (assert ) nil nil )"5" (assert ) nil nil )"6" (assert ) nil nil ))nil ))nil )"2" (lemma "seq_j" )"2" (ground)"2" "2" assert )"2" expand "path_from?" )"2" expand "from?" )"2" "2" assert )"2" "p!1" "t!1" )"2" assert )"2" expand "separable?" )"2" "2" assert )"2" "1" "1" "j!1" )"1" assert )"1" case "j!1 = 1" )"1" replace "1" "1" assert )"1" "short_path_case" )"1" "G!1" "s!1" "t!1" "seq(p!1)(1)" )"1" assert )"1" expand "path?" "1" "1" expand "walk?" )"1" "1" expand "verts_in?" )"1" "1" )"1" assert )"1" "0" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "j!1 = length(p!1) - 1" )"1" replace "1" "1" assert )"1" expand "path?" "1" "1" expand "walk?" )"1" "1" "length(p!1)-2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "path?" "2" "2" expand "walk?" )"2" "2" "length(p!1)-2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sep_set_lems nil )nil path_ops nil )"bool" graphs nil )"bool" meng_scaff_defs nil )"bool" sep_sets nil )nil doubletons nil )"bool" meng_scaff_defs nil )nil meng_scaff_prelude nil )"graph[T]" sep_sets nil )"bool" ind_paths nil )nil path_ops nil )"finite_set[T]" walks nil )nil paths nil )nil paths nil )"Seq(G)" walks nil )nil walks nil )"prewalk" walks nil )"bool" meng_scaff_prelude nil )nil graph_ops nil )nil path_ops nil )nil sep_set_lems nil )"graph[T]" graph_ops nil )"nat" sep_sets nil )nil paths nil )"bool" paths nil )"bool" walks nil )"bool" walks nil )"bool" walks nil )"bool" paths nil )"bool" sep_sets nil )nil walks nil )nil graphs nil )nil graphs nil )nil doubletons nil )"set[T]" doubletons nil ))nil ))nil 3251049132"" (induct "G" 1 "graph_induction_vert" )"" (skosimp*)"" (lemma "finale" )"" (inst?)"" (assert )"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (expand "induction_step" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" meng_scaff_prelude nil )nil h_menger nil )nil graph_inductions nil )nil h_menger nil )"bool" ind_paths nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil nat_types nil )"nat" sep_sets nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" sep_sets nil )nil defined_types 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 ))nil ))nil 3251049132"" (skosimp*)"" (lemma "h_menger" )"" (inst?)"" (assert )"" (skosimp*)"" "add(p1!1,singleton[Path_from(G!1,s!1,t!1)](p2!1))" )"" (rewrite "card_add[Path_from(G!1, s!1, t!1)]" )"" rewrite "card_singleton[Path_from(G!1, s!1, t!1)]" )"" (assert )"" (split +)"1" (lift-if)"1" (ground)"1" (expand "singleton" )"1" (replace -1)"1" "1" case "length(p2!1) = 2" )"1" expand "path_from?" )"1" "1" "1" expand "path?" )"1" expand "walk?" )"1" "1" "1" "0" )"1" assert )"1" expand "finseq_appl" )"1" expand "separable?" )"1" "1" expand "from?" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "independent?" )"2" expand "path_from?" )"2" "2" "1" "1" )"2" assert )"2" case "length(p2!1) = 1" )"1" expand "from?" )"1" "1" assert )"1" expand "separable?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "ind_path_set?" )"2" (skosimp*)"2" (expand "add" )"2" (expand "member" )"2" expand "singleton" )"2" "independent?_comm" )"2" "p1!1" "p2!1" )"2" assert )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil h_menger nil )"non_empty_finite_set" nil )"non_empty_finite_set" finite_sets nil )"T" h_menger nil )"T" h_menger nil )"prewalk[T]" h_menger nil )"graph[T]" h_menger 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 )"prewalk[T]" h_menger nil )nil paths nil )"bool" finite_sets nil )nil ind_paths nil )"bool" sets nil )"(nonempty?)" sets nil )"bool" sets nil )"(singleton?)" sets nil )nil finite_sets nil )"even_int" integersnil )"odd_int" integers nil )"bool" paths nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )"bool" sep_sets nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" walks nil )"(strict_total_order?[real])" real_props nil )"bool" ind_paths nil )"bool" sets nil )nil ind_paths nil )"bool" ind_paths nil )"posint" nil )"nonneg_int" nil )nil finite_sets 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 )nil h_menger nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.270 Sekunden
(vorverarbeitet am 2026-05-06)
¤ *© Formatika GbR, Deutschland
2026-05-26
