|
(meng_scaff_prelude
(line20_TCC1 0
(line20_TCC1-1 nil 3308649220
("" (skosimp*) (("" (expand "in?") (("" (flatten) nil nil)) nil))
nil)
((in? const-decl "bool" meng_scaff_defs nil)) nil))
(line20_TCC2 0
(line20_TCC2-1 nil 3308649220
("" (skosimp*) (("" (expand "in?") (("" (flatten) nil nil)) nil))
nil)
((in? const-decl "bool" meng_scaff_defs nil)) nil))
(line20_TCC3 0
(line20_TCC3-1 nil 3308649220
("" (skosimp*)
(("" (expand "separable?")
(("" (expand "in?")
(("" (flatten)
(("" (expand "disjoint?") (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((separable? const-decl "bool" sep_sets nil)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil))
(line20_TCC4 0
(line20_TCC4-1 nil 3308649220
("" (skosimp*)
(("" (expand "in?")
(("" (expand "disjoint?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((in? const-decl "bool" meng_scaff_defs nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(disjoint? const-decl "bool" meng_scaff_defs nil))
nil))
(line20_TCC5 0
(line20_TCC5-1 nil 3308649220
("" (skosimp*)
(("" (expand "in?")
(("" (expand "disjoint?")
(("" (flatten) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((in? const-decl "bool" meng_scaff_defs nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(disjoint? const-decl "bool" meng_scaff_defs nil))
nil))
(line20_TCC6 0
(line20_TCC6-1 nil 3308649220
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil))
nil))
(line20 0
(line20-1 nil 3308649220
("" (skosimp*)
((""
(case "EXISTS (yt: T): vert(path_comp(del_vert(
del_vert(G!1,w1!1),w2!1),t!1))(yt) AND yt /= t!1")
(("1" (hide 1)
(("1" (skosimp*)
(("1" (case "size(MM!1) < size(G!1)")
(("1" (expand "induction_step")
(("1" (inst - "MM!1")
(("1" (assert)
(("1" (inst - "s!1" "t!1")
(("1" (assert)
(("1"
(case "separable?(MM!1, s!1, t!1)
AND sep_num(MM!1, s!1, t!1) = 2
AND vert(MM!1)(s!1) AND vert(MM!1)(t!1)")
(("1" (flatten)
(("1" (assert)
(("1" (skosimp*)
(("1"
(hide -1 -2 -3 -4 -5 -9 -10)
(("1"
(lemma "line19")
(("1"
(inst?)
(("1"
(inst-cp -1 "p1!1")
(("1"
(inst -1 "p2!1")
(("1"
(assert)
(("1"
(flatten)
(("1"
(split -2)
(("1"
(assert)
(("1"
(case
"seq(p1!1)(length(p1!1) - 2) = w2!1")
(("1"
(assert)
(("1"
(hide -5 1)
(("1"
(inst
1
"p2!1"
"p1!1")
(("1"
(assert)
(("1"
(lemma
"independent?_comm")
(("1"
(inst
-
"p1!1"
"p2!1")
(("1"
(assert)
(("1"
(hide
-1
-4
-5
-6
-7)
(("1"
(expand
"independent?")
(("1"
(expand
"verts_of")
(("1"
(split
1)
(("1"
(skosimp*)
(("1"
(expand
"finseq_appl")
(("1"
(inst
-
"length(p1!1)-2"
"i!1")
(("1"
(assert)
(("1"
(typepred
"i!1")
(("1"
(expand
"path_from?")
(("1"
(flatten)
(("1"
(expand
"disjoint?")
(("1"
(flatten)
(("1"
(expand
"from?")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"finseq_appl")
(("2"
(inst
-
"i!1"
"length(p2!1)-2")
(("2"
(assert)
(("2"
(expand
"path_from?")
(("2"
(expand
"disjoint?")
(("2"
(flatten)
(("2"
(expand
"from?")
(("2"
(flatten)
(("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"
(hide -5 -6 2 3)
(("2"
(expand
"independent?")
(("2"
(inst
-
"length(p1!1)-2"
"length(p2!1)-2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide -5 -6 1)
(("2"
(inst
1
"p1!1"
"p2!1")
(("2"
(assert)
(("2"
(split -4)
(("1"
(assert)
(("1"
(expand
"verts_of")
(("1"
(split 1)
(("1"
(skosimp*)
(("1"
(expand
"finseq_appl")
(("1"
(expand
"independent?")
(("1"
(inst
-
"i!1"
"length(p2!1)-2")
(("1"
(expand
"disjoint?")
(("1"
(expand
"path_from?")
(("1"
(flatten)
(("1"
(expand
"from?")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"finseq_appl")
(("2"
(expand
"independent?")
(("2"
(inst
-
"length(p1!1)-2"
"i!1")
(("2"
(assert)
(("2"
(expand
"disjoint?")
(("2"
(expand
"path_from?")
(("2"
(expand
"from?")
(("2"
(flatten)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"independent?")
(("2"
(inst
-
"length(p1!1)-2"
"length(p2!1)-2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "pre20")
(("2" (inst?)
(("2" (assert)
(("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (hide -2 -4 -8)
(("2" (lemma "line17")
(("2" (inst?)
(("2" (expand "H")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "line15ab")
(("2" (inst -1 "G!1" "t!1" "s!1" "w1!1" "w2!1")
(("2" (rewrite "separable?_comm")
(("2" (rewrite "dbl_comm")
(("2" (rewrite "sep_num_comm")
(("1" (assert)
(("1" (split -1)
(("1" (flatten)
(("1" (skosimp*)
(("1" (case-replace "edge?(G!1)(w1!1, t!1)")
(("1" (assert)
(("1"
(lemma "line16")
(("1"
(assert)
(("1"
(inst
-
"G!1"
"s!1"
"t!1"
"w2!1"
"w1!1")
(("1"
(assert)
(("1"
(expand "disjoint?")
(("1"
(flatten)
(("1"
(expand "in?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst 2 "yt!1")
(("1"
(expand "H")
(("1"
(rewrite
"del_vert_comm")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(lemma "line16")
(("2"
(inst
-
"G!1"
"s!1"
"t!1"
"w1!1"
"w2!1")
(("2"
(assert)
(("2"
(rewrite "dbl_comm")
(("2"
(assert)
(("2"
(expand "in?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst 3 "yt!1")
(("2"
(expand "H")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "in?")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil)
("3" (assert)
(("3" (rewrite "dbl_comm")
(("3" (hide 2 3)
(("3" (lemma "separates_comm")
(("3"
(inst?)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "in?") (("2" (propax) nil nil)) nil)
("3" (expand "in?") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((del_vert const-decl "graph[T]" graph_ops nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(Subgraph type-eq-decl nil subgraphs nil)
(subgraph? const-decl "bool" subgraphs 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)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil meng_scaff_prelude nil)
(line17 formula-decl nil meng_scaff nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(induction_step const-decl "bool" meng_scaff_prelude nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pre20 formula-decl nil meng_scaff nil)
(line19 formula-decl nil meng_scaff nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(verts_of const-decl "finite_set[T]" walks nil)
(below type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(from? const-decl "bool" walks nil)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(path_from? const-decl "bool" paths nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(independent? const-decl "bool" ind_paths nil)
(independent?_comm formula-decl nil ind_paths nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sep_num const-decl "nat" sep_sets nil)
(separable? const-decl "bool" sep_sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(size const-decl "nat" graphs nil)
(line15ab formula-decl nil meng_scaff nil)
(separable?_comm formula-decl nil sep_set_lems nil)
(sep_num_comm formula-decl nil sep_set_lems nil)
(del_vert_comm formula-decl nil graph_ops nil)
(in? const-decl "bool" meng_scaff_defs nil)
(line16 formula-decl nil meng_scaff nil)
(edge? const-decl "bool" graphs nil)
(separates_comm formula-decl nil sep_set_lems nil)
(is_finite const-decl "bool" finite_sets nil)
(dbl_comm formula-decl nil doubletons nil))
nil))
(join2_TCC1 0
(join2_TCC1-1 nil 3308649220 ("" (subtype-tcc) nil nil) nil nil))
(join2_TCC2 0
(join2_TCC2-1 nil 3308649220
("" (skosimp*)
(("" (expand* "^" min empty_seq)
(("" (expand "o ")
(("" (expand "rev")
(("" (typepred "p2!1")
(("" (typepred "p1!1")
(("" (lemma "walk_concat")
(("" (inst?)
(("" (inst -1 "t!1" "p2!1")
(("" (assert)
(("" (hide -3 -5)
(("" (expand "o ")
(("" (expand "rev")
(("" (expand* "^" min empty_seq)
((""
(expand "walk_from?")
((""
(flatten)
((""
(assert)
((""
(expand "walk?")
((""
(expand "finseq_appl")
((""
(flatten)
((""
(split +)
(("1"
(hide -4)
(("1"
(expand "verts_in?")
(("1"
(propax)
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)
((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(^ const-decl "finseq" finite_sequences nil)
(rev const-decl "finseq[T]" doubletons nil)
(Long_walk_from type-eq-decl nil meng_scaff_prelude nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(walk? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(walk_concat formula-decl nil walks nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil meng_scaff_prelude nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks 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)
(walk_from? const-decl "bool" walks nil)
(Walk_from type-eq-decl nil walks nil)
(O const-decl "finseq" finite_sequences nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil))
nil))
(path_meng_t 0
(path_meng_t-1 nil 3308649220
("" (skosimp*)
(("" (expand "path_from?")
(("" (flatten)
(("" (expand "from?")
(("" (flatten)
(("" (expand "path?")
(("" (flatten)
(("" (expand "finseq_appl")
(("" (inst - "i!1" "length(p!1) - 1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((path_from? const-decl "bool" paths nil)
(from? const-decl "bool" walks nil)
(path? const-decl "bool" paths 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)
(real_gt_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)
(below type-eq-decl nil naturalnumbers nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil meng_scaff_prelude nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(path_H_def_TCC1 0
(path_H_def_TCC1-1 nil 3308649220
("" (skosimp*)
(("" (assert)
(("" (expand* "^" min empty_seq)
(("" (typepred "j!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ const-decl "finseq" finite_sequences nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
nil))
(path_H_def 0
(path_H_def-1 nil 3308649220
("" (skosimp*)
(("" (lemma "path_H_W")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (expand "path?")
(("" (flatten)
(("" (hide -2)
(("" (expand "H")
(("" (expand "walk?")
(("" (flatten)
(("" (split +)
(("1" (hide -2)
(("1" (expand "verts_in?")
(("1"
(skosimp*)
(("1"
(expand "del_verts")
(("1"
(expand "difference")
(("1"
(expand "member")
(("1"
(expand "dbl")
(("1"
(expand* "^" min empty_seq)
(("1"
(inst?)
(("1"
(expand "path_comp")
(("1"
(expand "subgraph")
(("1"
(flatten)
(("1"
(hide -2)
(("1"
(expand
"del_vert")
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(assert)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "i!1")
(("2"
(expand*
"^"
min
empty_seq)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (hide -2)
(("2"
(expand "finseq_appl")
(("2"
(expand* "^" min empty_seq)
(("2"
(expand "edge?")
(("2"
(inst?)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand "del_verts")
(("2"
(split 1)
(("1"
(expand "path_comp")
(("1"
(expand "subgraph")
(("1"
(flatten)
(("1"
(expand
"del_vert")
(("1"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand "dbl")
(("2"
(split -1)
(("1"
(expand
"verts_of")
(("1"
(expand
"finseq_appl")
(("1"
(replace
-1)
(("1"
(hide -1)
(("1"
(split
-1)
(("1"
(hide
-3)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand
"verts_of")
(("2"
(expand
"finseq_appl")
(("2"
(hide
1)
(("2"
(split
-1)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil)
("2"
(inst?)
(("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)
((T formal-type-decl nil meng_scaff_prelude nil)
(path_H_W formula-decl nil meng_scaff_defs nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(path? const-decl "bool" paths nil)
(walk? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks nil)
(del_verts const-decl "graph[T]" sep_sets nil)
(member const-decl "bool" sets nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(^ const-decl "finseq" finite_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(remove const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(i!1 skolem-const-decl "below(length(p!1 ^ (0, j!1)))"
meng_scaff_prelude nil)
(below type-eq-decl nil naturalnumbers nil)
(j!1 skolem-const-decl "nat" meng_scaff_prelude nil)
(p!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude 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)
(difference const-decl "set" sets nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(verts_of const-decl "finite_set[T]" walks nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pregraph type-eq-decl nil graphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(path_H_ind_TCC1 0
(path_H_ind_TCC1-1 nil 3308649220 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil meng_scaff_prelude nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(path_H_ind_TCC2 0
(path_H_ind_TCC2-1 nil 3308649220 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(doubleton type-eq-decl nil doubletons nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals 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)
(prewalk type-eq-decl nil walks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(T formal-type-decl nil meng_scaff_prelude nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(/= const-decl "boolean" notequal nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(dbl const-decl "set[T]" doubletons nil)
(edge? const-decl "bool" graphs nil)
(walk? const-decl "bool" walks nil)
(walk_from? const-decl "bool" walks nil)
(path_verts const-decl "set[T]" paths nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(trunc1 const-decl "prewalk" walks nil)
(path? const-decl "bool" paths nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(path_H_ind_TCC3 0
(path_H_ind_TCC3-1 nil 3308649220
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "finite_set[T]" meng_scaff_prelude nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(path_H_ind_TCC4 0
(path_H_ind_TCC4-1 nil 3308649220 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil meng_scaff_prelude nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(/= const-decl "boolean" notequal nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(dbl const-decl "set[T]" doubletons nil)
(edge? const-decl "bool" graphs nil)
(walk? const-decl "bool" walks nil)
(walk_from? const-decl "bool" walks nil)
(path_verts const-decl "set[T]" paths nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.181 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
