| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 466 kB |
|
Impressum meng_scaff_prelude.prfSprache: Lisp |
|||||||||||||||
|
(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) (trunc1 const-decl "prewalk" walks nil) (path? const-decl "bool" paths nil) (del_verts const-decl "graph[T]" sep_sets nil) (difference const-decl "set" sets nil) (separates const-decl "bool" sep_sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (path_H_ind 0 (path_H_ind-3 nil 3559575114 ("" (skosimp*) (("" (auto-rewrite finseq_appl) (("" (expand "independent?") (("" (skosimp*) (("" (expand "separates") (("" (flatten) (("" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p1!1^(0,i!1), s!1, seq(p1!1)(i!1))") (("1" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p2!1^(0,j!1), t!1, seq(p2!1)(j!1))") (("1" (name-replace "DV" "del_verts(G!1, dbl(w1!1, w2!1))") (("1" (inst + "join2(DV,s!1,t!1,seq(p2!1)(j!1),p1!1^(0,i!1),p2!1^(0,j!1))") (("1" (assert) nil nil) ("2" (assert) (("2" (expand* "^" min empty_seq) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "walk_from?") (("2" (split 1) (("1" (expand* "^" min empty_seq) nil nil) ("2" (expand* "^" min empty_seq) (("2" (assert) nil nil)) nil) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "j!1" "trunc1(p2!1)" "t!1" "w1!1" "w2!1") (("3" (assert) (("3" (expand "trunc1" -1) (("3" (expand* "^" min empty_seq) (("3" (assert) (("3" (hide-all-but (-1 1)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "^" 1) (("3" (expand min 1) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "walk_from?") (("2" (split 1) (("1" (expand "^" 1) (("1" (propax) nil nil)) nil) ("2" (expand* "^" min empty_seq) (("2" (assert) nil nil)) nil) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "i!1" "trunc1(p1!1)" "s!1" "w1!1" "w2!1") (("3" (assert) (("3" (expand "trunc1") (("3" (expand* "^" min empty_seq) (("3" (hide-all-but (-1 1)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand* "^" min empty_seq) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((DV skolem-const-decl "graph[T]" meng_scaff_prelude nil) (p2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (j!1 skolem-const-decl "nat" meng_scaff_prelude nil) (t!1 skolem-const-decl "T" meng_scaff_prelude nil) (s!1 skolem-const-decl "T" meng_scaff_prelude nil) (i!1 skolem-const-decl "nat" meng_scaff_prelude nil) (p1!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (join2 const-decl "Walk_from(G, s, t)" meng_scaff_prelude nil) (Long_walk_from type-eq-decl nil meng_scaff_prelude nil) (Walk_from type-eq-decl nil walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (int_minus_int_is_int application-judgement "int" integers nil) (path_H_def formula-decl nil meng_scaff_prelude nil) (finite_difference application-judgement "finite_set" finite_sets nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (Longprewalk type-eq-decl nil walks nil) (trunc1 const-decl "prewalk" walks nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (T formal-type-decl nil meng_scaff_prelude 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) (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) (walk_from? const-decl "bool" walks nil) (is_finite const-decl "bool" finite_sets nil) (del_verts const-decl "graph[T]" sep_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 "finseq" finite_sequences nil) (separates const-decl "bool" sep_sets nil) (independent? const-decl "bool" ind_paths nil)) nil) (path_H_ind-2 nil 3559575027 ("" (skosimp*) (("" (auto-rewrite finseq_appl) (("" (expand "independent?") (("" (skosimp*) (("" (expand "separates") (("" (flatten) (("" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p1!1^(0,i!1), s!1, seq(p1!1)(i!1))") (("1" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p2!1^(0,j!1), t!1, seq(p2!1)(j!1))") (("1" (name-replace "DV" "del_verts(G!1, dbl(w1!1, w2!1))") (("1" (inst + "join2(DV,s!1,t!1,seq(p2!1)(j!1),p1!1^(0,i!1),p2!1^(0,j!1))") (("1" (assert) nil) ("2" (assert) (("2" (expand* "^" min empty_seq) (("2" (assert) nil))))) ("3" (assert) (("3" (expand "^" 1) (("3" (propax) nil))))) ("4" (assert) nil) ("5" (assert) nil))))) ("2" (hide -1 4) (("2" (expand "walk_from?") (("2" (split 1) (("1" (expand* "^" min empty_seq) (("1" (propax) nil))) ("2" (expand* "^" min empty_seq) (("2" (propax) nil))) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "j!1" "trunc1(p2!1)" "t!1" "w1!1" "w2!1") (("1" (assert) (("1" (expand "trunc1" -1) (("1" (expand* "^" min empty_seq) (("1" (propax) nil))))))) ("2" (assert) nil))))))))))) ("3" (expand "^" 1) (("3" (assert) nil))) ("4" (assert) nil))) ("2" (expand "walk_from?") (("2" (split 1) (("1" (expand "^" 1) (("1" (propax) nil))) ("2" (expand* "^" min empty_seq) (("2" (propax) nil))) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "i!1" "trunc1(p1!1)" "s!1" "w1!1" "w2!1") (("1" (assert) (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (propax) nil))))))) ("2" (assert) nil))))))))) ("3" (expand* "^" min empty_seq) (("3" (assert) nil))) ("4" (assert) nil)))))))))))))) nil) nil nil) (path_H_ind-1 nil 3308649220 ("" (skosimp*) (("" (expand "independent?") (("" (skosimp*) (("" (expand "separates") (("" (flatten) (("" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p1!1^(0,i!1), s!1, seq(p1!1)(i!1))") (("1" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p2!1^(0,j!1), t!1, seq(p2!1)(j!1))") (("1" (name-replace "DV" "del_verts(G!1, dbl(w1!1, w2!1))") (("1" (inst + "join2(DV,s!1,t!1,seq(p2!1)(j!1),p1!1^(0,i!1),p2!1^(0,j!1))") (("1" (assert) nil nil) ("2" (assert) (("2" (expand* "^" min empty_seq) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (expand "^" 1) (("3" (propax) nil nil)) nil)) nil) ("4" (assert) nil nil) ("5" (assert) nil nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "walk_from?") (("2" (split 1) (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil nil)) nil) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "j!1" "trunc1(p2!1)" "t!1" "w1!1" "w2!1") (("1" (assert) (("1" (expand "trunc1" -1) (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "^" 1) (("3" (assert) nil nil)) nil) ("4" (assert) nil nil)) nil) ("2" (expand "walk_from?") (("2" (split 1) (("1" (expand "^" 1) (("1" (propax) nil nil)) nil) ("2" (expand* "^" min empty_seq) (("2" (propax) nil nil)) nil) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "i!1" "trunc1(p1!1)" "s!1" "w1!1" "w2!1") (("1" (assert) (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand* "^" min empty_seq) (("3" (assert) nil nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((independent? const-decl "bool" ind_paths nil) (separates const-decl "bool" sep_sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (walk_from? const-decl "bool" walks nil) (prewalk type-eq-decl nil walks 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) (trunc1 const-decl "prewalk" walks nil) (Longprewalk type-eq-decl nil walks nil) (Walk_from type-eq-decl nil walks nil)) nil)) (path_comps_ind3_TCC1 0 (path_comps_ind3_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_comps_ind3_TCC2 0 (path_comps_ind3_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) (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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers 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) (trunc1 const-decl "prewalk" walks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (path_comps_ind3_TCC3 0 (path_comps_ind3_TCC3-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_comps_ind3_TCC4 0 (path_comps_ind3_TCC4-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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers 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_comps_ind3_TCC5 0 (path_comps_ind3_TCC5-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_comps_ind3_TCC6 0 (path_comps_ind3_TCC6-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_comps_ind3 0 (path_comps_ind3-1 nil 3308649220 ("" (skosimp*) (("" (lemma "path_H_ind") (("" (inst?) (("1" (inst -1 "trunc1(p2!1)" "t!1") (("1" (assert) (("1" (hide -3 -4 -5 2) (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((path_H_ind formula-decl nil meng_scaff_prelude nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (trunc1 const-decl "prewalk" walks nil) (Longprewalk type-eq-decl nil walks nil) (>= const-decl "bool" reals 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) (T formal-type-decl nil meng_scaff_prelude nil)) nil)) (path_H_trunc_TCC1 0 (path_H_trunc_TCC1-1 nil 3560107624 ("" (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) (int_minus_int_is_int application-judgement "int" integers 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) (from? const-decl "bool" walks nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (path_H_trunc_TCC2 0 (path_H_trunc_TCC2-1 nil 3560107624 ("" (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) (trunc1 const-decl "prewalk" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (path_H_trunc 0 (path_H_trunc-1 nil 3560107625 ("" (skosimp*) (("" (lemma "path_comp_in") (("" (inst?) (("" (assert) (("" (lemma "path_H_W") (("" (inst?) (("" (assert) (("" (flatten) (("" (expand "path_from?") (("" (hide -3) (("" (expand "path?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (expand "walk?") (("1" (expand "finseq_appl") (("1" (split +) (("1" (flatten) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (hide -2 -3) (("1" (inst?) (("1" (expand "trunc1") (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "trunc1") (("2" (expand* "^" "min" "empty_seq") (("2" (typepred "i!1") (("2" (case-replace "i!1 = length(p!1) - 1") (("1" (hide -1 -2 -3 1) (("1" (typepred "G!1") (("1" (expand "edge?") (("1" (flatten) (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (hide -4) (("2" (inst -3 "n!1") (("2" (assert) (("2" (expand "trunc1") (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "i!1" "j!1") (("1" (assert) (("1" (hide -2) (("1" (expand "trunc1") (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "trunc1") (("2" (expand* "^" "min") (("2" (assert) (("2" (hide -2) (("2" (typepred "j!1") (("2" (case-replace "j!1 = length(p!1) - 1") (("1" (expand "from?") (("1" (flatten) (("1" (replace -6) (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "from?") (("2" (flatten) (("2" (hide 4) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "trunc1") (("3" (expand* "^" "min") (("3" (assert) (("3" (case "i!1 = length(p!1) - 1") (("1" (replace -1) (("1" (expand "from?") (("1" (flatten) (("1" (replace -6) (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (inst 3 "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil meng_scaff_prelude nil) (path_comp_in formula-decl nil meng_scaff_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (p!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(p!1))" meng_scaff_prelude nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (NOT const-decl "[bool -> bool]" booleans nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (i!1 skolem-const-decl "below(length(p!1))" meng_scaff_prelude nil) (j!1 skolem-const-decl "below(length(p!1))" meng_scaff_prelude nil) (verts_of const-decl "finite_set[T]" walks nil) (from? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (path_from? const-decl "bool" paths nil) (path_H_W formula-decl nil meng_scaff_defs nil) (trunc1 const-decl "prewalk" walks nil) (Longprewalk type-eq-decl nil walks nil) (>= const-decl "bool" reals 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)) shostak)) (meng_last_TCC1 0 (meng_last_TCC1-1 nil 3308649220 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (meng_last_TCC2 0 (meng_last_TCC2-1 nil 3308649220 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (meng_last_TCC3 0 (meng_last_TCC3-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) (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) (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) (meng const-decl "graph[T]" meng_scaff_defs nil) (add const-decl "(nonempty?)" sets nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (union const-decl "set" sets nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (meng_last_TCC4 0 (meng_last_TCC4-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) (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) (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) (meng const-decl "graph[T]" meng_scaff_defs nil) (add const-decl "(nonempty?)" sets nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (union const-decl "set" sets nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (meng_last 0 (meng_last-1 nil 3308649220 ("" (skosimp*) (("" (lemma "path_meng_t") (("" (inst?) (("1" (assert) (("1" (assert) (("1" (hide -1) (("1" (expand "path_from?") (("1" (flatten) (("1" (hide -7 -8) (("1" (expand "path?") (("1" (flatten) (("1" (hide -7) (("1" (expand "walk?") (("1" (flatten) (("1" (expand "finseq_appl") (("1" (inst?) (("1" (assert) (("1" (hide -6) (("1" (expand "edge?") (("1" (flatten) (("1" (assert) (("1" (expand "meng") (("1" (expand "union") (("1" (expand "add") (("1" (expand "member") (("1" (split -) (("1" (assert) (("1" (lemma "dbl_eq") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (reveal -7) (("1" (split -) (("1" (flatten) (("1" (hide -1) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "dbl_eq") (("2" (inst?) (("2" (assert) (("2" (hide -2) (("2" (reveal -7) (("2" (split -) (("1" (flatten) (("1" (hide -1) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "H") (("3" (expand "path_comp") (("3" (expand "subgraph") (("3" (flatten) (("3" (hide -2) (("3" (expand "del_vert") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "incident") (("4" (assert) (("4" (skosimp*) nil nil)) nil)) nil) ("5" (assert) (("5" (expand "incident") (("5" (skosimp*) 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" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil) ((path_meng_t formula-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) (path_from? const-decl "bool" paths nil) (walk? const-decl "bool" walks 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) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (edge? const-decl "bool" graphs nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (H const-decl "Subgraph(G)" meng_scaff_defs nil) (subgraph const-decl "Subgraph(G)" subgraphs nil) (del_vert const-decl "graph[T]" graph_ops nil) (path_comp const-decl "Subgraph(G)" meng_scaff_defs nil) (dbl_eq formula-decl nil doubletons nil) (add const-decl "(nonempty?)" 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) (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) (path? const-decl "bool" paths 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) (meng const-decl "graph[T]" meng_scaff_defs 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) (T formal-type-decl nil meng_scaff_prelude nil)) nil)) (ind_verts_W_TCC1 0 (ind_verts_W_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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons 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) (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) (T formal-type-decl nil meng_scaff_prelude nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (ind_verts_W_TCC2 0 (ind_verts_W_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) (dbl const-decl "set[T]" doubletons 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) (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) (T formal-type-decl nil meng_scaff_prelude nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (ind_verts_W 0 (ind_verts_W-1 nil 3308649220 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "from?") (("" (flatten) (("" (expand "independent?") (("" (split +) (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (skosimp*) (("1" (inst - "i!1" "length(p2!1) - 2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "verts_of") (("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (inst - "length(p1!1) - 2" "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (independent? const-decl "bool" ind_paths nil) (p1!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (verts_of const-decl "finite_set[T]" walks 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) (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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (p2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (ind_verts_w_TCC1 0 (ind_verts_w_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) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons 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) (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) (T formal-type-decl nil meng_scaff_prelude nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (ind_verts_w_TCC2 0 (ind_verts_w_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) (dbl const-decl "set[T]" doubletons 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) (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) (T formal-type-decl nil meng_scaff_prelude nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (/= const-decl "boolean" notequal nil) (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil)) nil)) (ind_verts_w 0 (ind_verts_w-1 nil 3308649220 ("" (skosimp*) (("" (expand "path_from?") (("" (flatten) (("" (expand "from?") (("" (flatten) (("" (expand "independent?") (("" (split +) (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (skosimp*) (("1" (inst - "i!1" "length(p2!1) - 2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "verts_of") (("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (inst - "length(p1!1) - 2" "i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (independent? const-decl "bool" ind_paths nil) (p1!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (verts_of const-decl "finite_set[T]" walks 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) (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) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (p2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (path_meng_in_TCC1 0 (path_meng_in_TCC1-1 nil 3308649220 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers 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_meng_in_TCC2 0 (path_meng_in_TCC2-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)) nil)) (path_meng_in_TCC3 0 (path_meng_in_TCC3-1 nil 3308649220 ("" (subtype-tcc) nil nil) ((prewalk type-eq-decl nil walks 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) (> 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) (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (doubleton type-eq-decl nil doubletons nil) (= const-decl "[T, T -> boolean]" equalities 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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil meng_scaff_prelude nil) (verts_of const-decl "finite_set[T]" walks nil) (from? const-decl "bool" walks 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) (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) (meng const-decl "graph[T]" meng_scaff_defs nil) (add const-decl "(nonempty?)" sets nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (union const-decl "set" sets nil) (path? const-decl "bool" paths nil) (trunc1 const-decl "prewalk" walks nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (path_meng_in 0 (path_meng_in-1 nil 3308649220 ("" (skosimp*) (("" (expand "path?") (("" (flatten) (("" (split +) (("1" (expand "walk?") (("1" (flatten) (("1" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (assert) (("1" (hide -8) (("1" (expand "finseq_appl") (("1" (inst?) (("1" (expand "meng") (("1" (expand "add") (("1" (expand "member") (("1" (split -7) (("1" (expand "from?") (("1" (flatten) (("1" (inst - "i!1" "length(p!1) - 1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (split -10) (("1" (flatten) (("1" (inst - "i!1" "length(p!1) - 2") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "verts_of") (("2" (expand "finseq_appl") (("2" (inst + "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (split -10) (("1" (flatten) (("1" (expand "verts_of") (("1" (inst + "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst - "i!1" "length(p!1) - 2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "finseq_appl") (("2" (expand "trunc1") (("2" (skosimp*) (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide -7) (("2" (expand "meng") (("2" (expand "edge?") (("2" (flatten) (("2" (assert) (("2" (expand "union") (("2" (expand "add") (("2" (expand "member") (("2" (split -7) (("1" (lemma "dbl_eq") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (split -1) (("1" (flatten) (("1" (expand "from?") (("1" (flatten) (("1" (inst - "1 + n!1" "length(p!1) - 1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst - "n!1" "length(p!1) - 1") (("2" (assert) (("2" (expand "from?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "from?") (("2" (flatten) (("2" (lemma "dbl_eq") (("2" (inst?) (("2" (assert) (("2" (hide -2) (("2" (split -1) (("1" (flatten) (("1" (inst - "1 + n!1" "length(p!1) - 1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst - "n!1" "length(p!1) - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "incident") (("3" (skosimp*) (("3" (hide -1) (("3" (lemma "dbl_eq") (("3" (inst?) (("3" (assert) (("3" (hide -2) (("3" (split -1) (("1" (flatten) (("1" (split -12) (("1" (flatten) (("1" (inst - "n!1" "length(p!1) - 2") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "verts_of") (("2" (inst + "n!1") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -12) (("1" (flatten) (("1" (inst - "1 + n!1" "length(p!1) - 2") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "verts_of") (("2" (inst + "1 + n!1") (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "incident") (("4" (skosimp*) (("4" (hide -1) (("4" (lemma "dbl_eq") (("4" (inst?) (("4" (assert) (("4" (hide -2) (("4" (expand "from?") (("4" (flatten) (("4" (ground) (("1" (expand "verts_of") (("1" (expand "finseq_appl") (("1" (inst + "n!1") nil nil)) nil)) nil) ("2" (inst - "n!1" "length(p!1) - 2") (("2" (assert) nil nil)) nil) ("3" (expand "verts_of") (("3" (expand "finseq_appl") (("3" (inst + "1 + n!1") nil nil)) nil)) nil) ("4" (inst - "1 + n!1" "length(p!1) - 2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (typepred "i!1") (("2" (typepred "j!1") (("2" (hide -9 -11 -12) (("2" (expand "trunc1") (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (inst - "i!1" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path? const-decl "bool" paths nil) (union const-decl "set" sets nil) (incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs nil) (dbl_eq formula-decl nil doubletons nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonempty_add_finite application-judgement "non_empty_finite_set" finite_sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (verts_in? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (trunc1 const-decl "prewalk" walks nil) (Longprewalk type-eq-decl nil walks 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) (nat nonempty-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) (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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (add const-decl "(nonempty?)" sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (from? const-decl "bool" walks nil) (verts_of const-decl "finite_set[T]" walks nil) (member const-decl "bool" sets nil) (meng const-decl "graph[T]" meng_scaff_defs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (walk? const-decl "bool" walks nil)) nil)) (join2_lem_TCC1 0 (join2_lem_TCC1-1 nil 3308649220 ("" (skosimp*) (("" (lemma "path_from_l") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((T formal-type-decl nil meng_scaff_prelude nil) (path_from_l formula-decl nil paths nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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)) (join2_lem_TCC2 0 (join2_lem_TCC2-1 nil 3308649220 ("" (assert) (("" (skosimp*) (("" (assert) (("" (lemma "path_from_l") (("" (hide -2) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil meng_scaff_prelude nil) (path_from_l formula-decl nil paths 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) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (join2_lem_TCC3 0 (join2_lem_TCC3-1 nil 3308649220 ("" (skosimp*) (("" (lemma "path_from_l") (("" (inst?) (("" (assert) (("" (expand "path_from?") (("" (expand "walk_from?") (("" (expand "from?") (("" (expand "path?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil meng_scaff_prelude nil) (path_from_l formula-decl nil paths nil) (walk_from? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths 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)) (join2_lem_TCC4 0 (join2_lem_TCC4-1 nil 3308649220 ("" (skosimp*) (("" (hide -1 -3) (("" (expand "path_from?") (("" (expand "path?") (("" (expand "from?") (("" (expand "walk_from?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path? const-decl "bool" paths nil) (walk_from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil)) nil)) (join2_lem 0 (join2_lem-3 nil 3559576863 ("" (skosimp*) (("" (auto-rewrite finseq_appl) (("" (lemma "path_from_l") (("" (inst?) (("" (assert) (("" (lemma "path_from_l") (("" (inst -1 "G!1" "p2!1" "t!1" "v!1") (("" (assert) (("" (expand "path_from?") (("" (flatten) (("" (split +) (("1" (expand "join2") (("1" (expand "path?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "walk?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (ground) (("1" (inst?) nil nil) ("2" (inst? -6) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -4 -7 -10) (("2" (expand "from?") (("2" (flatten) (("2" (expand "o ") (("2" (expand "rev") (("2" (expand* "^" min empty_seq) (("2" (expand "edge?") (("2" (case "n!1 < length(p1!1) - 1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (lift-if) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -7 "length(p1!1) + length(p2!1) - 3 - n!1") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (rewrite "dbl_comm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -4 -7) (("2" (expand "o ") (("2" (expand* "^" min empty_seq) (("2" (assert) (("2" (expand "rev") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (inst -6 "i!1" "j!1") (("1" (assert) nil nil)) nil) ("2" (typepred "j!1") (("2" (expand* "^" min empty_seq) (("2" (expand "o ") (("2" (expand "rev") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "trunc1") (("2" (expand* "^" min empty_seq) (("2" (case "j!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -11) (("1" (replace -8 * rl) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -6 -8) (("2" (inst -8 "i!1" "length(p1!1) + length(p2!1) - 2 - j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (prop) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (hide -6 -8) (("1" (expand "disjoint?") (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (case "i!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -9) (("1" (replace -7 * rl) (("1" (reveal -2) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -8 "j!1" "length(p1!1) + length(p2!1) - 2 - i!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -6 "length(p1!1) + length(p2!1) - 2 - i!1" "length(p1!1) + length(p2!1) - 2 - j!1") (("1" (assert) nil nil) ("2" (typepred j!1) (("2" (expand* o ^ min empty_seq rev) (("2" (assert) nil nil)) nil)) nil) ("3" (typepred i!1) (("3" (expand* o ^ min empty_seq rev) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "from?") (("2" (expand "join2") (("2" (expand "o ") (("2" (flatten) (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (join2 const-decl "Walk_from(G, s, t)" meng_scaff_prelude nil) (disjoint? const-decl "bool" meng_scaff_prelude nil) (trunc1 const-decl "prewalk" walks nil) (p1!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (p2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (i!1 skolem-const-decl "below(length(p1!1 ^ (0, length(p1!1) - 2) o rev(p2!1)))" meng_scaff_prelude nil) (j!1 skolem-const-decl "below(length(p1!1 ^ (0, length(p1!1) - 2) o rev(p2!1)))" meng_scaff_prelude nil) (from? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (dbl_comm formula-decl nil doubletons nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" meng_scaff_prelude nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (below type-eq-decl nil naturalnumbers nil) (rev const-decl "finseq[T]" doubletons nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "finseq" finite_sequences nil) (O const-decl "finseq" finite_sequences 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) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (path? const-decl "bool" paths nil) (path_from? const-decl "bool" paths nil) (path_from_l formula-decl nil paths nil) (T formal-type-decl nil meng_scaff_prelude nil)) nil) (join2_lem-2 nil 3559576115 ("" (skosimp*) (("" (lemma "path_from_l") (("" (inst?) (("" (assert) (("" (lemma "path_from_l") (("" (inst -1 "G!1" "p2!1" "t!1" "v!1") (("" (assert) (("" (expand "path_from?") (("" (flatten) (("" (split +) (("1" (expand "join2") (("1" (expand "path?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "walk?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (ground) (("1" (inst?) nil) ("2" (inst? -6) nil))))))))))))))))) ("2" (skosimp*) (("2" (hide -4 -7 -10) (("2" (expand "from?") (("2" (flatten) (("2" (expand "o ") (("2" (expand "rev") (("2" (expand* "^" min empty_seq) (("2" (expand "edge?") (("2" (case "n!1 < length(p1!1) - 1") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case-replace "n!1 = length(p1!1) - 1") (("1" (assert) nil) ("2" (lift-if) (("2" (assert) nil))))))))))))) ("2" (assert) (("2" (inst -7 "length(p1!1) + length(p2!1) - 3 - n!1") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (rewrite "dbl_comm") nil))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (hide -4 -7) (("2" (expand "o ") (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (inst -6 "i!1" "j!1") (("1" (assert) nil))) ("2" (typepred "j!1") (("2" (expand* "^" min empty_seq) (("2" (expand "o ") (("2" (expand "rev") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "trunc1") (("2" (expand* "^" min empty_seq) (("2" (case "j!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -11) (("1" (replace -8 * rl) (("1" (inst?) (("1" (inst -6 "length(p1!1) -1") (("1" (assert) nil))))))))))))))))))) ("2" (assert) (("2" (inst?) (("2" (hide -6 -8) (("2" (inst?) (("2" (assert) nil))))))))))))))))))))))))))) ("3" (case "j!1 < length(p1!1) - 1") (("1" (assert) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (hide -6 -8) (("1" (expand "disjoint?") (("1" (expand "trunc1") (("1" (expand* "^" min empty_seq) (("1" (case "i!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -9) (("1" (replace -7 * rl) (("1" (reveal -2) (("1" (inst?) (("1" (inst -1 "j!1") (("1" (assert) nil))))))))))))))))))))) ("2" (inst?) (("2" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))))))))))))))))))))) ("2" (assert) (("2" (expand "disjoint?") (("2" (hide -4 -8) (("2" (inst?) (("1" (inst -5 "length(p1!1) + length(p2!1) - 2 - j!1") (("1" (assert) nil) ("2" (assert) (("2" (typepred "j!1") (("2" (expand* "^" min empty_seq) (("2" (expand "o ") (("2" (expand "rev") (("2" (assert) nil))))))))))))) ("2" (assert) (("2" (typepred "i!1") (("2" (expand "o ") (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (expand "from?") (("2" (expand "join2") (("2" (expand "o ") (("2" (flatten) (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (assert) nil)))))))))))))))))))))))))))))))) nil) nil nil) (join2_lem-1 nil 3308649220 ("" (skosimp*) (("" (lemma "path_from_l") (("" (inst?) (("" (assert) (("" (lemma "path_from_l") (("" (inst -1 "G!1" "p2!1" "t!1" "v!1") (("" (assert) (("" (expand "path_from?") (("" (flatten) (("" (split +) (("1" (expand "join2") (("1" (expand "path?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "walk?") (("1" (flatten) (("1" (split +) (("1" (hide -4 -7) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (ground) (("1" (inst?) nil nil) ("2" (inst? -6) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -4 -7 -10) (("2" (expand "from?") (("2" (flatten) (("2" (expand "o ") (("2" (expand "rev") (("2" (expand* "^" min empty_seq) (("2" (expand "edge?") (("2" (case "n!1 < length(p1!1) - 1") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case-replace "n!1 = length(p1!1) - 1") (("1" (assert) nil nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -7 "length(p1!1) + length(p2!1) - 3 - n!1") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (rewrite "dbl_comm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -4 -7) (("2" (expand "o ") (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (inst -6 "i!1" "j!1") (("1" (assert) nil nil)) nil) ("2" (typepred "j!1") (("2" (expand* "^" min empty_seq) (("2" (expand "o ") (("2" (expand "rev") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "trunc1") (("2" (expand "^") (("2" (case "j!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -11) (("1" (replace -8 * rl) (("1" (inst?) (("1" (inst -6 "length(p1!1) -1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst?) (("2" (hide -6 -8) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "j!1 < length(p1!1) - 1") (("1" (assert) (("1" (typepred "i!1") (("1" (expand "o ") (("1" (expand "rev") (("1" (expand* "^" min empty_seq) (("1" (hide -6 -8) (("1" (expand "disjoint?") (("1" (expand "trunc1") (("1" (expand "^") (("1" (case "i!1 = length(p1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "from?") (("1" (flatten) (("1" (replace -9) (("1" (replace -7 * rl) (("1" (reveal -2) (("1" (inst?) (("1" (inst -1 "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "disjoint?") (("2" (hide -4 -8) (("2" (inst?) (("1" (inst -5 "length(p1!1) + length(p2!1) - 2 - j!1") (("1" (assert) nil nil) ("2" (assert) (("2" (typepred "j!1") (("2" (expand "^") (("2" (expand "o ") (("2" (expand "rev") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "i!1") (("2" (expand "o ") (("2" (expand "^") (("2" (expand "rev") (("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) ("2" (expand "from?") (("2" (expand "join2") (("2" (expand "o ") (("2" (flatten) (("2" (expand* "^" min empty_seq) (("2" (expand "rev") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_from_l formula-decl nil paths nil) (path_from? const-decl "bool" paths nil) (path? const-decl "bool" paths nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil) (dbl_comm formula-decl nil doubletons nil) (from? const-decl "bool" walks nil) (trunc1 const-decl "prewalk" walks nil) (prewalk type-eq-decl nil walks 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)) (path_from_to_walk_from 0 (path_from_to_walk_from-1 nil 3308649220 ("" (skosimp*) (("" (expand "path_from?") (("" (expand "walk_from?") (("" (expand "from?") (("" (expand "path?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((path_from? const-decl "bool" paths nil) (from? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (path? const-decl "bool" paths nil) (walk_from? const-decl "bool" walks nil)) nil)) (paths_H_disj_TCC1 0 (paths_H_disj_TCC1-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)) nil)) (paths_H_disj_TCC2 0 (paths_H_disj_TCC2-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)) nil)) (paths_H_disj 0 (paths_H_disj-1 nil 3308649220 ("" (skosimp*) (("" (expand "disjoint?") (("" (skosimp*) (("" (expand "separates") (("" (flatten) (("" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p1!1^(0,i!1), s!1, seq(p1!1)(i!1))") (("1" (case "walk_from?[T](del_verts[T](G!1, dbl[T](w1!1, w2!1)), p2!1^(0,j!1), t!1, seq(p2!1)(j!1))") (("1" (hide -3 -4) (("1" (name-replace "DV" "del_verts(G!1, dbl(w1!1, w2!1))") (("1" (case-replace "i!1 = 0") (("1" (replace -4) (("1" (replace -8 * rl) (("1" (inst + "rev(p2!1 ^ (0, j!1))") (("1" (hide -3) (("1" (expand "walk_from?") (("1" (flatten) (("1" (lemma "walk?_rev") (("1" (inst -1 "DV" "p2!1 ^ (0, j!1)") (("1" (assert) (("1" (expand "^" +) (("1" (expand "min" +) (("1" (expand "rev") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 1) (("2" (expand "min" 1) (("2" (expand "rev") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "join2(DV,s!1,t!1,seq(p2!1)(j!1),p1!1^(0,i!1),p2!1^(0,j!1))") (("1" (typepred "join2(DV, s!1, t!1, seq(p2!1)(j!1), p1!1 ^ (0, i!1), p2!1 ^ (0, j!1))") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (expand "^" 1) (("2" (expand "min" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "walk_from?") (("2" (split 1) (("1" (expand* "^" min empty_seq) nil nil) ("2" (expand* "^" min empty_seq) (("2" (assert) nil nil)) nil) ("3" (lemma "path_H_def") (("3" (inst -1 "G!1" "j!1" "p2!1" "t!1" "w1!1" "w2!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "^" 1) (("3" (expand "min" 1) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (lemma "path_H_def") (("2" (inst -1 "G!1" "i!1" "p1!1" "s!1" "w1!1" "w2!1") (("2" (assert) (("2" (expand "walk_from?") (("2" (expand "^" 1) (("2" (expand "min" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "^" 1) (("3" (expand "min" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" meng_scaff_prelude nil) (separates const-decl "bool" sep_sets nil) (^ const-decl "finseq" finite_sequences 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) (is_finite const-decl "bool" finite_sets nil) (walk_from? const-decl "bool" walks 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) (T formal-type-decl nil meng_scaff_prelude 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) (path_H_def formula-decl nil meng_scaff_prelude nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (walk?_rev formula-decl nil walks nil) (j!1 skolem-const-decl "nat" meng_scaff_prelude nil) (p2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (rev const-decl "finseq[T]" doubletons nil) (NOT const-decl "[bool -> bool]" booleans nil) (Walk_from type-eq-decl nil walks nil) (Long_walk_from type-eq-decl nil meng_scaff_prelude nil) (join2 const-decl "Walk_from(G, s, t)" meng_scaff_prelude nil) (p1!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (i!1 skolem-const-decl "nat" meng_scaff_prelude nil) (s!1 skolem-const-decl "T" meng_scaff_prelude nil) (t!1 skolem-const-decl "T" meng_scaff_prelude nil) (DV skolem-const-decl "graph[T]" meng_scaff_prelude nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil)) nil)) (prelude 0 (prelude-1 nil 3308649220 ("" (skosimp*) (("" (expand "in?") (("" (expand "disjoint?") (("" (flatten) (("" (lemma "line20") (("" (inst -1 "G!1" "meng(G!1, s!1, t!1, w1!1, w2!1)" "s!1" "t!1" "w1!1" "w2!1") (("1" (assert) (("1" (expand "in?") (("1" (expand "disjoint?") (("1" (split -1) (("1" (skosimp*) (("1" (hide 1 2) (("1" (lemma "line20") (("1" (inst -1 "G!1" "meng(G!1, t!1, s!1, w1!1, w2!1)" "t!1" "s!1" "w1!1" "w2!1") (("1" (assert) (("1" (rewrite "separable?_comm") (("1" (expand "in?") (("1" (expand "disjoint?") (("1" (rewrite "sep_num_comm") (("1" (assert) (("1" (rewrite "separates_comm") (("1" (split -1) (("1" (skosimp*) (("1" (hide 1 2) (("1" (hide -15 -16 -17 -18 7 8) (("1" (name "HS" "H(G!1, s!1, w1!1, w2!1)") (("1" (name "HT" "H(G!1, t!1, w1!1, w2!1)") (("1" (case "path?(HS,trunc1(trunc1(P1!1))) AND from?(trunc1(P1!1),s!1,w1!1)") (("1" (case "path?(HS,trunc1(trunc1(P2!1))) AND from?(trunc1(P2!1),s!1,w2!1)") (("1" (case "path?(HT,trunc1(trunc1(P1!2))) AND from?(trunc1(P1!2),t!1,w1!1)") (("1" (case "path?(HT,trunc1(trunc1(P2!2))) AND from?(trunc1(P2!2),t!1,w2!1)") (("1" (flatten) (("1" (case "path_from?[T](G!1, trunc1(P1!1), s!1, w1!1) AND path_from?[T](G!1, trunc1(P1!2), t!1, w1!1)") (("1" (flatten) (("1" (name "Rw1" "join2(G!1,s!1,t!1,w1!1,trunc1(P1!1),trunc1(P1!2))") (("1" (case "disjoint?(trunc1(trunc1(P1!1)),trunc1(trunc1(P1!2)))") (("1" (lemma "join2_lem") (("1" (inst?) (("1" (assert) (("1" (replace -3) (("1" (case "path_from?[T](G!1, trunc1(P2!1), s!1, w2!1) AND path_from?[T](G!1, trunc1(P2!2), t!1, w2!1)") (("1" (flatten) (("1" (case "disjoint?(trunc1(trunc1(P2!1)),trunc1(trunc1(P2!2)))") (("1" (lemma "join2_lem") (("1" (inst -1 "G!1" "trunc1(P2!1)" "trunc1(P2!2)" "s!1" "t!1" "w2!1") (("1" (assert) (("1" (name "Rw2" "join2(G!1,s!1,t!1,w2!1,trunc1(P2!1),trunc1(P2!2))") (("1" (replace -1) (("1" (hide -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -28 -30) (("1" (case "independent?(Rw1,Rw2)") (("1" (case "Rw1 /= Rw2") (("1" (assert) (("1" (flatten) (("1" (expand "path_from?") (("1" (flatten) (("1" (assert) (("1" (hide -2 -3 -4 -5 -6 -7 -8 -9 -10) (("1" (hide -2 -3 -4 -5 -8 -9 -10) (("1" (lemma "independent?_comm") (("1" (inst -1 "Rw1" "Rw2") (("1" (assert) (("1" (reveal -10 -11 -15 -16) (("1" (inst 8 "Rw1" "Rw2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "independent_ne") (("2" (inst?) (("2" (case "independent?(Rw1, Rw2)") (("1" (assert) (("1" (replace -10 * rl) (("1" (expand "join2" 1) (("1" (expand "o ") (("1" (expand "trunc1" 1) (("1" (expand* "^" "min") (("1" (expand "rev") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -4 -5 -9 -10 8) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (replace -5 * rl) (("2" (hide -5) (("2" (hide -1 -2 -3 -4) (("2" (reveal -11 -12 -13 -14 -15 -16 -17 -18) (("2" (lemma "path_comps_ind3") (("2" (inst -1 "G!1" "P1!1" "P2!2" "s!1" "t!1" "w1!1" "w2!1") (("2" (assert) (("2" (split -1) (("1" (lemma "path_comps_ind3") (("1" (inst -1 "G!1" "P2!1" "P1!2" "s!1" "t!1" "w1!1" "w2!1") (("1" (assert) (("1" (split -1) (("1" (hide -3 -4 -5 -6 -7 -8 -9 -10) (("1" (expand "independent?" 1) (("1" (skosimp*) (("1" (expand "join2") (("1" (rewrite "l_trunc1") (("1" (rewrite "l_trunc1") (("1" (expand* "^" "min") (("1" (assert) (("1" (expand "o ") (("1" (expand "rev") (("1" (rewrite "l_trunc1") (("1" (rewrite "l_trunc1") (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (expand "independent?" -14) (("1" (inst - "i!1" "j!1") (("1" (assert) (("1" (hide -4 -5) (("1" (expand "trunc1") (("1" (expand* "^" "min") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "j!1 < length(P2!1) - 2") (("1" (assert) (("1" (expand "independent?" -5) (("1" (inst - "j!1" "length(P1!1) + length(P1!2) - 4 - i!1") (("1" (rewrite "l_trunc1") (("1" (rewrite "l_trunc1") (("1" (assert) (("1" (case "i!1 = length(P1!1) - 2") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (hide -3) (("1" (expand "trunc1") (("1" (expand* "^" "min") (("1" (reveal -29 7) (("1" (replace -1) (("1" (hide -1) (("1" (expand "verts_of") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (prop) (("1" (grind) nil nil) ("2" (assert) (("2" (hide -4 -5 -13) (("2" (expand "independent?") (("2" (expand "trunc1") (("2" (expand* "^" "min") (("2" (inst - "length(P1!1) + length(P1!2) - 4 - i!1" "length(P2!1) + length(P2!2) - 4 - j!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "from?" -7) (("2" (flatten) (("2" (expand "trunc1" -7) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "from?" -5) (("3" (flatten) (("3" (expand "trunc1" -5) (("3" (assert) (("3" (expand "^") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "from?" -8) (("2" (flatten) (("2" (expand "trunc1" -8) (("2" (expand "^") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "from?" -2) (("3" (flatten) (("3" (expand "trunc1" -2) (("3" (assert) (("3" (expand "^") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "paths_H_disj") (("2" (inst?) (("2" (inst?) (("2" (inst -1 "s!1") (("2" (assert) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 2 9) (("2" (hide -2 -3 -4 -6 -7 -8 -9 -10 -12 -17 -19 -23) (("2" (expand "from?") (("2" (expand "trunc1") (("2" (expand* "^" "min" "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -16 -18 -23 -25) (("2" (hide -3 -4 -7 -8) (("2" (replace -5 * rl) (("2" (hide -5) (("2" (replace -5 * rl) (("2" (hide -5) (("2" (lemma "path_comp_in") (("2" (expand "path_from?") (("2" (inst?) (("2" (assert) (("2" (lemma "path_H_trunc") (("2" (expand "finseq_appl") (("2" (split +) (("1" (inst -1 "G!1" "trunc1(P2!1)" "s!1" "t!1" "w2!1" "w1!1") (("1" (rewrite "H_comm" -1) (("1" (assert) (("1" (expand "path_from?") (("1" (hide 1) (("1" (reveal -16 -28) (("1" (expand "trunc1" 1) (("1" (expand* "^" "min" "empty_seq") (("1" (lemma "meng_last") (("1" (hide -2) (("1" (reveal -17) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "G!1" "trunc1(P2!2)" "t!1" "s!1" "w2!1" "w1!1") (("2" (assert) (("2" (rewrite "H_comm") (("2" (assert) (("2" (expand "path_from?") (("2" (hide 1) (("2" (expand "trunc1" 1) (("2" (expand* "^" "min" "empty_seq") (("2" (lemma "meng_last") (("2" (reveal -15) (("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) ("2" (lemma "paths_H_disj") (("2" (inst?) (("2" (inst?) (("2" (inst -1 "s!1") (("2" (assert) (("2" (hide -1 -2 -3 -4 -5 -6 -8 -9 -10 -12 -13 2 9) (("2" (hide -3 -5 -7 -8 -9 -10 -12 -14 -15 -16) (("2" (expand "from?") (("2" (expand "trunc1") (("2" (flatten) (("2" (expand* "^" "min" "empty_seq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "path_from_to_walk_from") nil nil) ("3" (rewrite "path_from_to_walk_from") (("3" (assert) (("3" (expand "trunc1" 1) (("3" (expand* "^" "min" "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -24 -23 -21 -20 -17 -16) (("2" (hide -14 -13 -1 -2 -5 -6 8) (("2" (replace -5 * rl) (("2" (hide -5) (("2" (replace -5 * rl) (("2" (hide -5) (("2" (expand "path_from?") (("2" (flatten) (("2" (lemma "path_comp_in") (("2" (split 1) (("1" (hide -2 -3) (("1" (inst?) (("1" (assert) (("1" (lemma "path_H_trunc") (("1" (expand "finseq_appl") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "path_from?") (("1" (expand "trunc1" 1) (("1" (expand* "^" "min" "empty_seq") (("1" (lemma "meng_last") (("1" (hide -2 -3 -4 -5 -6) (("1" (inst?) (("1" (inst?) (("1" (expand "path_from?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (inst?) (("3" (assert) (("3" (lemma "path_H_trunc") (("3" (expand "finseq_appl") (("3" (inst?) (("3" (inst?) (("3" (expand "path_from?") (("3" (expand "trunc1" 1) (("3" (expand* "^" "min" "empty_seq") (("3" (lemma "meng_last") (("3" (hide -2 -3 -4 -5 -6) (("3" (inst?) (("3" (inst?) (("3" (expand "path_from?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -7 * rl) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -13 -14 -15 -16 -17 -18) (("2" (reveal -9 -11 -12 -13) (("2" (lemma "ind_verts_w") (("2" (inst -1 "meng(G!1, t!1, s!1, w1!1, w2!1)" "P1!2" "P2!2" "t!1" "s!1" "w1!1" "w2!1") (("2" (assert) (("2" (flatten) (("2" (hide -1 -4) (("2" (lemma "path_meng_in") (("2" (expand "path_from?") (("2" (inst?) (("2" (flatten) (("2" (assert) (("2" (expand "from?") (("2" (flatten) (("2" (expand "trunc1" +) (("2" (expand* "^" "min" "empty_seq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (expand "trunc1" 1) (("4" (expand* "^" "min" "empty_seq") (("4" (assert) nil nil)) nil)) nil) ("5" (assert) nil nil)) nil) ("2" (replace -3 * rl) (("2" (hide -1 -2 -3 -4 -7 -12 -14 8) (("2" (reveal -5) (("2" (lemma "ind_verts_w") (("2" (inst -1 "meng(G!1, t!1, s!1, w1!1, w2!1)" "P1!2" "P2!2" "t!1" "s!1" "w1!1" "w2!1") (("2" (assert) (("2" (flatten) (("2" (hide -1) (("2" (lemma "path_meng_in") (("2" (expand "path_from?") (("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (hide -1 -2) (("2" (expand "from?") (("2" (expand "trunc1") (("2" (expand* "^" "min" "empty_seq") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (expand "trunc1" 1) (("4" (expand* "^" "min" "empty_seq") (("4" (assert) nil nil)) nil)) nil) ("5" (assert) nil nil)) nil) ("2" (replace -3 * rl) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 8) (("2" (reveal -11) (("2" (lemma "ind_verts_w") (("2" (inst -1 "meng(G!1, s!1, t!1, w1!1, w2!1)" "P1!1" "P2!1" "s!1" "t!1" "w1!1" "w2!1") (("2" (assert) (("2" (flatten) (("2" (hide -1) (("2" (lemma "path_meng_in") (("2" (expand "path_from?") (("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (expand "from?") (("2" (expand "trunc1" +) (("2" (expand* "^" "min" "empty_seq") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "trunc1" 1) (("3" (expand* "^" "min" "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -2 * rl) (("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 -13 8) (("2" (lemma "ind_verts_w") (("2" (inst -1 "meng(G!1, s!1, t!1, w1!1, w2!1)" "P1!1" "P2!1" "s!1" "t!1" "w1!1" "w2!1") (("2" (assert) (("2" (flatten) (("2" (lemma "path_meng_in") (("2" (expand "path_from?") (("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (expand "from?") (("2" (expand "trunc1" +) (("2" (expand* "^" "min" "empty_seq") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "trunc1" 1) (("3" (expand* "^" "min" "empty_seq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "induction_step") (("2" (propax) nil nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((in? const-decl "bool" meng_scaff_defs nil) (s!1 skolem-const-decl "T" meng_scaff_prelude nil) (G!1 skolem-const-decl "graph[T]" meng_scaff_prelude 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) (T formal-type-decl nil meng_scaff_prelude nil) (t!1 skolem-const-decl "T" meng_scaff_prelude nil) (w1!1 skolem-const-decl "T" meng_scaff_prelude nil) (w2!1 skolem-const-decl "T" meng_scaff_prelude nil) (meng const-decl "graph[T]" meng_scaff_defs nil) (separable?_comm formula-decl nil sep_set_lems nil) (subgraph? const-decl "bool" subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (H const-decl "Subgraph(G)" meng_scaff_defs 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) (path? const-decl "bool" paths nil) (>= const-decl "bool" reals nil) (Longprewalk type-eq-decl nil walks nil) (trunc1 const-decl "prewalk" walks nil) (from? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty_seq const-decl "finseq" finite_sequences nil) (path_meng_in formula-decl nil meng_scaff_prelude nil) (ind_verts_w formula-decl nil meng_scaff_prelude nil) (path_from_to_walk_from formula-decl nil meng_scaff_prelude nil) (disjoint? const-decl "bool" meng_scaff_prelude nil) (path_comp_in formula-decl nil meng_scaff_defs nil) (path_H_trunc formula-decl nil meng_scaff_prelude nil) (H_comm formula-decl nil meng_scaff_defs nil) (meng_last formula-decl nil meng_scaff_prelude nil) (paths_H_disj formula-decl nil meng_scaff_prelude nil) (independent? const-decl "bool" ind_paths nil) (independent_ne formula-decl nil ind_paths nil) (O const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rev const-decl "finseq[T]" doubletons nil) (independent?_comm formula-decl nil ind_paths nil) (path_comps_ind3 formula-decl nil meng_scaff_prelude nil) (l_trunc1 formula-decl nil walks nil) (int_plus_int_is_int application-judgement "int" integers 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) (j!1 skolem-const-decl "nat" meng_scaff_prelude nil) (P2!2 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (P2!1 skolem-const-decl "prewalk[T]" meng_scaff_prelude nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (verts_of const-decl "finite_set[T]" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (join2_lem formula-decl nil meng_scaff_prelude nil) (join2 const-decl "Walk_from(G, s, t)" meng_scaff_prelude nil) (Long_walk_from type-eq-decl nil meng_scaff_prelude nil) (Walk_from type-eq-decl nil walks nil) (walk_from? const-decl "bool" walks nil) (path_from? const-decl "bool" paths nil) (induction_step const-decl "bool" meng_scaff_prelude nil) (separates_comm formula-decl nil sep_set_lems nil) (is_finite const-decl "bool" finite_sets nil) (sep_num_comm formula-decl nil sep_set_lems 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) (line20 formula-decl nil meng_scaff_prelude nil) (disjoint? const-decl "bool" meng_scaff_defs nil)) nil)))
¤ Dauer der Verarbeitung: 0.578 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26