(old_mengernil 3507100603"" (skosimp*)"" (expand "sep_num" )"" (lemma "injection_and_cardinal[Path_from(G!1,s!1,t!1),T]" )"" (inst?)"" (assert )"" (hide 2)"" case "FORALL (p: (ips!1)): ") "1" (expand "intersection" )"1" (expand "member" )"1" "(LAMBDA (p: (ips!1)): choose({x: T | min_sep_set[T](G!1, s!1, t!1)(x) AND internal_verts(p)(x)}))" )"1" (expand "injective?" )"1" (skosimp*)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" expand "path_from?" )"1" "1" expand "ind_path_set?" )"1" "x1!1" "x2!1" )"1" assert )"1" expand "independent?" )"1" "1" "choose({x: T | AND internal_verts(x1!1)(x)})") "1" expand "internal_verts" )"1" "1" "1" replace -3 * rl)"1" "1" "choose({x: T | AND internal_verts(x2!1)(x)})") "1" "1" expand "internal_verts" )"1" "1" replace "1" "1" expand "finseq_appl" )"1" "i!1" "i!2" )"1" assert )nil )))))))))))))))"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x2!1" )"2" "2" "2" assert )"2" expand "internal_verts" )"2" expand "finseq_appl" )"2" "i!2" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" "x1!1" )nil )))))))))))))))))))))))))"2" (skosimp*) (("2" (assert ) nil )))))))))"2" (skosimp*)"2" (expand "nonempty?" )"2" (lemma "min_sep_set_seps" )"2" (inst?)"2" (assert )"2" (hide -4 1)"2" (expand "separates" )"2" "2" "p!1" )"2" "2" "p!1" )"2" expand "path_from?" )"2" "2" expand "walk_from?" )"2" expand "from?" )"2" "2" assert )"2" "walk?_del_verts_not" )"2" "2" expand "path?" )"2" "2" assert )"2" "2" "2" "MSS" "min_sep_set(G!1, s!1, t!1)" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" expand "verts_of" )"2" expand "internal_verts" )"2" expand "finseq_appl" )"2" "2" "x!1" )"2" assert )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )"nat" sep_sets nil )"bool" finite_sets nil )nil ind_paths nil )"finite_set[T]" sep_sets nil )nil sep_sets nil )"bool" sep_sets nil )"bool" walks nil )"finite_set[T]" walks nil )nil naturalnumbers nil )"bool" reals nil ) (path? const-decl "bool" paths nil )nil sep_sets nil )"bool" walks nil )"graph[T]" old_menger nil )"T" old_menger nil )"T" old_menger nil )"set_of_paths[T](G!1, s!1, t!1)" nil )"(p)" sets nil )"bool" ind_paths nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" ind_paths nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"bool" sets nil )"finite_set[T]" ind_paths nil )"set" sets nil )"bool" sets nil )"finite_set" nil )"(total_order?[real])" nil )nil finite_sets_card_eq"finite_sets/" )nil naturalnumbers nil )nil nat_types nil )nil old_menger 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" paths nil )nil paths nil ))nil ))nil 3507100603"" (skosimp*)"" (lemma "h_menger" )"" (inst?)"" (assert )"" (skosimp*)"" "add(p1!1,singleton[Path_from(G!1,s!1,t!1)](p2!1))" )"1" (rewrite "card_add[Path_from(G!1, s!1, t!1)]" )"1" rewrite "card_singleton[Path_from(G!1, s!1, t!1)]" )"1" (assert )"1" (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 )))))))))))))))))))))))))))))"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 )))))))))"2" assert )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" nil )))))))))))))))))))))))"2" (hide 2)"2" rewrite "finite_singleton[Path_from(G!1, s!1, t!1)]" )nil )))))"2" (rewrite "finite_add[Path_from(G!1, s!1, t!1)]" )"2" rewrite "finite_singleton[Path_from(G!1, s!1, t!1)]" )nil ))))))))))))))nil )nil old_menger nil )nil h_menger nil )"non_empty_finite_set" nil )"non_empty_finite_set" finite_sets nil )"T" old_menger nil )"T" old_menger nil )"prewalk[T]" old_menger nil )"graph[T]" old_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]" old_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 ))nil 3507100603"" (skosimp*)"" (expand "sep_num" )"" (lemma "injection_and_cardinal[Path_from(G!1,s!1,t!1),T]" )"" (inst?)"" (assert )"" (hide 2)"" case "FORALL (p: (ips!1)): ") "1" (expand "intersection" )"1" (expand "member" )"1" "(LAMBDA (p: (ips!1)): choose({x: T | min_sep_set[T](G!1, s!1, t!1)(x) AND internal_verts(p)(x)}))" )"1" (expand "injective?" )"1" (skosimp*)"1" (typepred "x1!1" )"1" (typepred "x2!1" )"1" expand "path_from?" )"1" "1" expand "ind_path_set?" )"1" "x1!1" "x2!1" )"1" assert )"1" expand "independent?" )"1" "1" "choose({x: T | AND internal_verts(x1!1)(x)})") "1" expand "internal_verts" )"1" "1" "1" replace -3 * rl)"1" "1" "choose({x: T | AND internal_verts(x2!1)(x)})") "1" "1" expand "internal_verts" )"1" "1" replace "1" "1" expand "finseq_appl" )"1" "i!1" "i!2" )"1" assert )nil )))))))))))))))"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x2!1" )"2" "2" "2" assert )"2" expand "internal_verts" )"2" expand "finseq_appl" )"2" "i!2" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" "x1!1" )nil )))))))))))))))))))))))))"2" (skosimp*) (("2" (assert ) nil )))))))))"2" (skosimp*)"2" (expand "nonempty?" )"2" (lemma "min_sep_set_seps" )"2" (inst?)"2" (assert )"2" (hide -4 1)"2" (expand "separates" )"2" "2" "p!1" )"2" "2" "p!1" )"2" expand "path_from?" )"2" "2" expand "walk_from?" )"2" expand "from?" )"2" "2" assert )"2" "walk?_del_verts_not" )"2" "2" expand "path?" )"2" "2" assert )"2" "2" "2" "MSS" "min_sep_set(G!1, s!1, t!1)" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" expand "verts_of" )"2" expand "internal_verts" )"2" expand "finseq_appl" )"2" "2" "x!1" )"2" assert )"2" "2" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )"nat" sep_sets nil )"bool" finite_sets nil )nil ind_paths nil )"finite_set[T]" sep_sets nil )nil sep_sets nil )"bool" sep_sets nil )"bool" walks nil )"finite_set[T]" walks nil )nil naturalnumbers nil )"bool" reals nil ) (path? const-decl "bool" paths nil )nil sep_sets nil )"bool" walks nil )"graph[T]" old_menger nil )"T" old_menger nil )"T" old_menger nil )"set_of_paths[T](G!1, s!1, t!1)" nil )"(p)" sets nil )"bool" ind_paths nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" ind_paths nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"bool" sets nil )"finite_set[T]" ind_paths nil )"set" sets nil )"bool" sets nil )"finite_set" nil )"(total_order?[real])" nil )nil finite_sets_card_eq"finite_sets/" )nil naturalnumbers nil )nil nat_types nil )nil old_menger 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" paths nil )nil paths nil ))nil )))quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
