|
(h_menger
(path_not_thru 0
(path_not_thru-1 nil 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"
(case-replace
"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"
(apply-extensionality :hide? t)
(("1"
(apply-extensionality :hide? t)
(("1"
(iff 1)
(("1"
(expand "del_verts")
(("1"
(expand "del_vert")
(("1"
(ground)
(("1" (inst - "z!1") nil nil)
("2"
(skosimp*)
(("2" (assert) 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)
("2"
(apply-extensionality :hide? t)
(("1"
(expand "del_verts")
(("1"
(expand "del_vert")
(("1"
(expand "difference")
(("1"
(expand "remove")
(("1"
(expand "member")
(("1"
(iff)
(("1" (ground) 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)
("3"
(lemma "finite_singleton[T]")
(("3"
(inst?)
(("3"
(expand "singleton")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (lemma "finite_singleton[T]")
(("3"
(inst?)
(("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 const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(separates const-decl "bool" sep_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil h_menger nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(walk_to_path_from formula-decl nil path_ops nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(finite_singleton judgement-tcc nil finite_sets nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(del_verts const-decl "graph[T]" sep_sets nil)
(z!1 skolem-const-decl "T" h_menger nil)
(min_sep_set_card formula-decl nil sep_sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_singleton formula-decl nil finite_sets nil)
(t!1 skolem-const-decl "T" h_menger nil)
(s!1 skolem-const-decl "T" h_menger nil)
(G!1 skolem-const-decl "graph[T]" h_menger nil)
(sep_num const-decl "nat" sep_sets nil))
nil))
(adjacent_fact 0
(adjacent_fact-2 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*)
((""
(name "path2"
"add1(gen_seq2(G!1,s!1,w1!1),t!1)")
(("" (case "independent?(pn!1,path2)")
(("1"
(lemma "path_from_l")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "path_from?")
(("1"
(flatten)
(("1"
(lemma "path?_del_vert")
(("1"
(inst?)
(("1"
(assert)
(("1"
(case
"path?[T](G!1, path2) AND from?[T](path2, s!1, t!1)")
(("1"
(flatten)
(("1"
(inst
+
"pn!1"
"path2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
-1
-2
-3
-5
-6
-7
-8
-9
8)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(split +)
(("1"
(expand
"path?")
(("1"
(split +)
(("1"
(lemma
"walk?_add1")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"gen_seq2")
(("1"
(hide
2)
(("1"
(expand
"walk?")
(("1"
(expand
"verts_in?")
(("1"
(skosimp*)
(("1"
(expand
"edge?")
(("1"
(assert)
(("1"
(rewrite
"dbl_comm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"add1")
(("2"
(expand
"gen_seq2")
(("2"
(typepred
"i!1")
(("2"
(typepred
"j!1")
(("2"
(expand
"add1")
(("2"
(expand
"gen_seq2")
(("2"
(ground)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil)
("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil)
("3"
(lift-if)
(("3"
(ground)
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"
(propax)
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"
(skosimp*)
(("2"
(replace -6 * rl)
(("2"
(hide -6)
(("2"
(expand "add1")
(("2"
(expand "gen_seq2")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(expand "path_from?")
(("2"
(expand "path?")
(("2"
(expand "walk?")
(("2"
(flatten)
(("2"
(hide -8 -9)
(("2"
(expand
"verts_in?")
(("2"
(inst?)
(("2"
(expand
"del_vert")
(("2"
(expand
"remove")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil h_menger nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dbl const-decl "set[T]" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(graph type-eq-decl nil graphs nil)
(independent? const-decl "bool" ind_paths nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(path_from? const-decl "bool" paths nil)
(path?_del_vert formula-decl nil path_ops nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(walk?_add1 formula-decl nil walks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(edge? const-decl "bool" graphs nil)
(dbl_comm formula-decl nil doubletons nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(walk? const-decl "bool" walks nil)
(from? const-decl "bool" walks nil)
(path? const-decl "bool" paths nil)
(path_from_l formula-decl nil paths nil)
(remove const-decl "set" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(prewalk type-eq-decl nil walks nil)
(add1 const-decl "prewalk" walks nil)
(verts_in? const-decl "bool" walks nil)
(Seq type-eq-decl nil walks nil)
(gen_seq2 const-decl "Seq(G)" walks nil)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(nil application-judgement "finite_set[T]" h_menger nil)
(path_not_thru formula-decl nil h_menger nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil)
(adjacent_fact-1 nil 3251049132
("" (skosimp*)
(("" (expand "in?")
(("" (flatten)
(("" (lemma "path_not_thru")
(("" (inst?)
(("" (assert)
(("" (inst -1 "w1!1")
(("" (expand "disjoint?")
(("" (flatten)
(("" (assert)
(("" (skosimp*)
((""
(name "path2"
"add1(gen_seq2(G!1,s!1,w1!1),t!1)")
(("" (case "independent?(pn!1,path2)")
(("1" (lemma "path_from_l")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "path_from?")
(("1"
(flatten)
(("1"
(lemma "path?_del_vert")
(("1"
(inst?)
(("1"
(assert)
(("1"
(case
"path?[T](G!1, path2) AND from?[T](path2, s!1, t!1)")
(("1"
(flatten)
(("1"
(inst
+
"pn!1"
"path2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
-1
-2
-3
-5
-6
-7
-8
-9
8)
(("2"
(replace -1 * rl)
(("2"
(hide -1)
(("2"
(split +)
(("1"
(expand
"path?")
(("1"
(split +)
(("1"
(lemma
"walk?_add1")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"gen_seq2")
(("1"
(hide
2)
(("1"
(expand
"walk?")
(("1"
(expand
"verts_in?")
(("1"
(skosimp*)
(("1"
(expand
"edge?")
(("1"
(assert)
(("1"
(rewrite
"dbl_comm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"add1")
(("2"
(expand
"gen_seq2")
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(typepred
"i!1")
(("2"
(typepred
"j!1")
(("2"
(expand
"add1")
(("2"
(expand
"gen_seq2")
(("2"
(ground)
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil)
("2"
(lift-if)
(("2"
(ground)
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"
(propax)
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"
(skosimp*)
(("2"
(replace -6 * rl)
(("2"
(hide -6)
(("2"
(expand "add1")
(("2"
(expand "gen_seq2")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(expand "path_from?")
(("2"
(expand "path?")
(("2"
(expand "walk?")
(("2"
(flatten)
(("2"
(hide -8 -9)
(("2"
(expand
"verts_in?")
(("2"
(inst?)
(("2"
(expand
"del_vert")
(("2"
(expand
"remove")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((in? const-decl "bool" meng_scaff_defs nil)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(gen_seq2 const-decl "Seq(G)" walks nil)
(Seq type-eq-decl nil walks nil)
(verts_in? const-decl "bool" walks nil)
(add1 const-decl "prewalk" walks nil)
(prewalk type-eq-decl nil walks nil)
(path_from_l formula-decl nil paths nil)
(path? const-decl "bool" paths nil)
(from? const-decl "bool" walks nil)
(walk? const-decl "bool" walks nil)
(dbl_comm formula-decl nil doubletons nil)
(edge? const-decl "bool" graphs nil)
(walk?_add1 formula-decl nil walks nil)
(path?_del_vert formula-decl nil path_ops nil)
(path_from? const-decl "bool" paths nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(independent? const-decl "bool" ind_paths nil)
(graph type-eq-decl nil graphs nil)
(pregraph type-eq-decl nil graphs nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil))
nil))
(sep_num_del 0
(sep_num_del-1 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"
(flatten)
(("3"
(assert)
(("3"
(expand "walk?")
(("3"
(split +)
(("1"
(flatten)
(("1"
(expand "verts_in?")
(("1"
(skosimp*)
(("1"
(hide -4)
(("1"
(inst?)
(("1"
(ground)
(("1"
(expand
"del_verts")
(("1"
(expand
"difference")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(expand
"del_vert")
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand "finseq_appl")
(("2"
(expand "edge?")
(("2"
(inst?)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(hide -4)
(("2"
(expand
"del_verts")
(("2"
(flatten)
(("2"
(split +)
(("1"
(lemma
"edges_del_vert")
(("1"
(inst?)
(("1"
(assert)
nil
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("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)
("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)
((T formal-type-decl nil h_menger nil)
(min_sep_set_seps formula-decl nil sep_sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(min_sep_set_card formula-decl nil sep_sets nil)
(separates const-decl "bool" sep_sets nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(walk? const-decl "bool" walks nil)
(nil application-judgement "finite_set[T]" h_menger nil)
(edge? const-decl "bool" graphs nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(edges_del_vert formula-decl nil graph_ops nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(del_verts const-decl "graph[T]" sep_sets nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(verts_in? const-decl "bool" walks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(walk_from? const-decl "bool" walks nil)
(is_finite const-decl "bool" finite_sets nil)
(min_sep_set const-decl "finite_set[T]" sep_sets nil)
(t!1 skolem-const-decl "T" h_menger nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(G!1 skolem-const-decl "graph[T]" h_menger nil)
(v!1 skolem-const-decl "T" h_menger nil)
(s!1 skolem-const-decl "T" h_menger nil)
(sep_num const-decl "nat" sep_sets nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(separates_del 0
(separates_del-1 nil 3251049132
("" (skosimp*)
(("" (expand "del_vert")
(("" (expand "separates")
(("" (expand "singleton")
(("" (expand "dbl")
(("" (flatten)
(("" (assert)
(("" (skosimp*)
(("" (inst?)
(("" (expand "walk_from?")
(("" (flatten)
(("" (assert)
(("" (expand "walk?")
(("" (flatten)
((""
(split +)
(("1"
(expand "verts_in?")
(("1"
(hide -7)
(("1"
(skosimp*)
(("1"
(expand "del_verts")
(("1"
(expand "difference")
(("1"
(expand "remove")
(("1"
(expand "member")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand "edge?")
(("2"
(inst?)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand "del_verts")
(("2"
(hide -7)
(("2"
(flatten)
(("2"
(assert)
(("2"
(split +)
(("1"
(expand "dbl")
(("1"
(inst-cp
-
"ajm!1")
nil
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
(("2"
(inst
-
"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)
((del_vert const-decl "graph[T]" graph_ops nil)
(singleton const-decl "(singleton?)" sets nil)
(walk_from? const-decl "bool" walks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" h_menger nil)
(verts_in? const-decl "bool" walks nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(remove const-decl "set" sets nil)
(del_verts const-decl "graph[T]" sep_sets nil)
(walk? const-decl "bool" walks nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil h_menger nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(dbl const-decl "set[T]" doubletons nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.57Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
