Quelle meng_scaff.prf
Sprache: Lisp
(meng_scaffnil 3251049125"" (skosimp*)"" (typepred "ps!1" )"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil meng_scaff nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil walks nil )nil finite_sequences nil )nil meng_scaff nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "first" )"" (lemma "min_lem" )"" (inst?)"1" (expand "minimum?" ) (("1" (flatten) nil nil )) nil )"2" (hide 2)"2" (expand "nonempty?" )"2" (typepred "ps!1" )"2" (skosimp*)"2" (expand "empty?" )"2" (expand "member" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"below(length(ps))" meng_scaff nil )"ps_ptype(P!1)" meng_scaff nil )nil meng_scaff nil )"pred[T]" meng_scaff nil )nil defined_types nil )nil naturalnumbers nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil meng_scaff nil )nil nat_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" min_nat nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil min_lem nil ))nil ))nil 3251049125"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "first" )"" (lemma "min_lem" )"" (inst?)"1" (expand "minimum?" )"1" (flatten)"1" (assert )"1" (inst -3 "i!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (typepred "ps!1" )"2" (skosimp*)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"below(length(ps))" meng_scaff nil )"ps_ptype(P!1)" meng_scaff nil )nil meng_scaff nil )"pred[T]" meng_scaff nil )nil defined_types nil )nil naturalnumbers nil )nil walks nil )"bool" reals nil )nil finite_sequences nil )nil meng_scaff nil )nil nat_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"bool" min_nat nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )nil min_lem nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil meng_scaff nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil meng_scaff nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"posint" nil )nil meng_scaff nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )"posint" nil )nil meng_scaff nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "separates" )"" (flatten)"" (expand "dbl" )"" (expand "singleton" )"" (flatten)"" (assert )"" (expand "in?" )"" (expand "disjoint?" )"" (flatten)"" (expand "verts_of" )"" (expand "finseq_appl" )"" case "(EXISTS (i: below(length(p!1))): seq(p!1)(i) = w1!1 OR seq(p!1)(i) = w2!1)" )"1" (skosimp*)"1" "ipf" "first((LAMBDA (x:T): x = w1!1 OR x = w2!1),p!1)" )"1" "first_lem" )"1" "1" "first_not" )"1" "1" replace -3)"1" "1" expand "walk_from?" )"1" "1" case "walk?(G!1,p!1^(0,ipf))" )"1" case "NOT verts_of(p!1^(0,ipf))(t!1)" )"1" "1" case "walk?(H(G!1,s!1,w1!1,w2!1),trunc1(p!1^(0,ipf)))" )"1" case "walk?(meng(G!1,s!1,t!1,w1!1,w2!1),p!1^(0,ipf))" )"1" "Ms" "meng(G!1, s!1, t!1, w1!1, w2!1)" )"1" "1" case "walk?(Ms,add1(p!1^(0,ipf),t!1))" )"1" "del_verts(Ms, {y: T | y = z!1}) = del_vert(Ms,z!1)" )"1" "add1(p!1^(0,ipf),t!1)" )"1" rewrite "walk?_del_vert_not" )"1" "1" expand "add1" )"1" expand *"^" "min" "empty_seq" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "verts_of" )"2" expand "finseq_appl" )"2" expand "add1" )"2" "2" expand *"^" "min" )"2" assert )"2" "2" "2" "2" expand *"^" "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" expand "del_verts" )"1" expand "del_vert" )"1" "1" nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_singleton[T]" )"2" "2" expand "singleton" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "del_vert" )"2" expand "del_verts" )"2" "2" "2" expand "difference" )"2" expand "member" )"2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "finite_singleton[T]" )"3" expand "singleton" )"3" nil nil ))nil ))nil ))nil ))nil )"3" "finite_singleton[T]" )"3" expand "singleton" )"3" nil nil ))nil ))nil ))nil )"2" "2" "walk?_add1" )"2" "2" assert )"2" "2" "2" replace "2" "2" "1" expand "meng" )"1" expand "add" )"1" nil nil ))nil ))nil )"2" expand "edge?" )"2" expand *"^" "min" )"2" expand "verts_of" )"2" expand "finseq_appl" )"2" "2" assert )"2" "2" expand "meng" )"2" expand "union" )"2" expand "add" )"2" expand "member" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "walk?" )"2" expand "finseq_appl" )"2" "2" "1" expand "verts_in?" )"1" "1" "i!2" )"1" expand "^" "1" expand "min" "1" expand "empty_seq" "1" assert )"1" case "i!2 = ipf" )"1" "1" replace "1" "1" expand "meng" )"1" expand "^" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" expand "add" )"1" expand "member" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "meng" )"1" expand "trunc1" )"1" expand *"^" "min" "empty_seq" )"1" expand "add" )"1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "trunc1" "2" expand "^" "2" expand "min" "2" expand "empty_seq" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" "2" expand "min" "2" expand "empty_seq" "2" assert )"2" case "n!1 = ipf - 1" )"1" "1" "1" expand "verts_in?" )"1" "1" expand "edge?" )"1" expand *"^" "min" "empty_seq" )"1" "1" "1" assert )"1" expand "meng" )"1" expand "union" )"1" expand "add" )"1" expand "member" )"1" "1" replace "1" "1" assert )"1" expand "incident" )"1" "seq(p!1)(ipf-1)" )"1" "seq(p!1)(ipf-1)" )"1" "1" "1" expand "verts_in?" )"1" "ipf-1" )"1" expand "trunc1" "1" expand "^" "1" expand "min" "1" rewrite "dbl_comm" "1" "1" replace "1" nil nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "trunc1" "2" expand "^" "2" expand "min" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" "2" expand "min" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" "n!1" )"2" "2" expand "trunc1" )"2" expand *"^" "min" "empty_seq" )"2" assert )"2" "2" assert )"2" expand "meng" )"2" expand "union" )"2" expand "add" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil )"4" nil nil )"5" nil nil )"6" nil nil ))nil )"2" "walk?_H" )"2" "2" assert )"2" "2" case "walk?(G!1, trunc1(p!1 ^ (0, ipf)))" )"1" assert )"1" "1" expand "trunc1" )"1" expand *"^" "min" "empty_seq" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" "1" assert )"1" "1" assert )"1" nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" "3" "i!2" )"3" assert )nil nil ))nil ))nil ))nil )"4" "4" nil nil ))nil )"5" "5" "5" "i!2" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "trunc1" )"2" rewrite "walk?_caret" )"1" expand "^" "1" expand "min" "1" assert )nil nil ))nil ))nil )"2" expand "^" "2" expand "min" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "^" "3" expand "min" "3" expand "empty_seq" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "verts_of" )"2" "2" expand "finseq_appl" )"2" expand "^" "2" "p!1^(0,i!2)" )"1" expand "^" "1" expand "min" "1" assert )"1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "1" expand "verts_in?" )"1" "i!2" )"1" expand "^" "1" expand "min" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "verts_in?" )"2" "2" expand "del_verts" )"2" expand "difference" )"2" expand "member" )"2" "i!3" )"2" "i!2" )"2" expand "^" "2" expand "min" "2" assert )"2" "i!3" )"2" assert )"2" case "i!3 = ipf" )"1" assert )nil nil )"2" "i!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "edge?" )"3" "n!1" )"3" "3" expand *"^" "min" )"3" case "n!1 = ipf" )"1" replace "1" "1" "1" "ipf" )"1" "i!2" )"1" expand *"^" "min" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "i!2" )"2" expand "^" "2" expand "min" "2" assert )"2" "2" assert )"2" expand "del_verts" )"2" "2" "2" "n!1" )"2" "n!1+1" )"2" assert )"2" case "n!1 = ipf -1" )"1" assert )nil nil )"2" assert )"2" expand "dbl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "i!2" )"2" expand "^" "2" expand "min" "2" assert )"2" expand "^" "2" expand "min" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "walk?_caret" )nil nil )"3" expand "^" 1)"3" expand "min" 1)"3" expand "empty_seq" "3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst?) nil nil ))nil ))nil )"2" (inst 11 "p!1" )"2" "2" expand "walk_from?" )"2" "2" assert )"2" expand "walk?" )"2" expand "finseq_appl" )"2" "1" "1" expand "verts_in?" )"1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" "1" "1" assert )"1" "1" assert )"1" expand "del_verts" )"1" "1" expand "dbl" )"1" "1" "1" "n!1+1" )"1" assert )nil nil ))nil ))nil )"2" "2" "n!1+1" )"2" assert )nil nil ))nil ))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 ))nil ))nil ))nil ))nil )"bool" sep_sets nil )"set[T]" doubletons nil )"bool" meng_scaff_defs nil )"[below[length(fs)] -> T]" finite_sequencesnil )"nat" meng_scaff nil )nil meng_scaff nil )nil meng_scaff nil )"bool" walks nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" walks nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"below(length(p!1 ^ (0, ipf)))" meng_scaffnil )"posint" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil meng_scaff_defs nil )nil walks nil )"graph[T]" meng_scaff_defs nil )"(nonempty?)" sets nil )"{k: nat | k <= i AND k <= j}" nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" graphs nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil walks nil )"graph[T]" graph_ops nil )"graph[T]" sep_sets nil )nil path_ops nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"prewalk[T]" meng_scaff nil )"below(length(p!1))" meng_scaff nil )"T" meng_scaff nil )nil finite_sets nil )"bool" sets nil )"finite_set" finite_sets nil )"finite_set" finite_setsnil )"set" sets nil )"set" sets nil )"prewalk" walks nil )"nat" meng_scaff nil )"int" integers nil )nil doubletons nil )"finite_set[doubleton[T]]" meng_scaff_defsnil )"bool" walks nil )"below(length(p!1 ^ (0, ipf)))" meng_scaffnil )"(total_order?[real])" nil )"prewalk" walks nil )nil walks nil )"Subgraph(G)" meng_scaff_defs nil )nil subgraphs nil )"bool" subgraphs nil )"bool" finite_sets nil )NOT const-decl "[bool -> bool]" booleans nil )"below(length(ps))" meng_scaff nil )nil meng_scaff nil )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil nat_types nil )nil meng_scaff nil )nil finite_sequences nil )"bool" reals nil )nil walks nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"finite_set[T]" walks nil )"bool" meng_scaff_defs nil )"(total_order?[real])" nil )"(singleton?)" sets nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"boolean" notequal nil )nil meng_scaff nil )"bool" meng_scaff_defs nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"boolean" notequal nil )nil meng_scaff nil )"bool" meng_scaff_defs nil ))nil ))nil 3251049125"" (skosimp*)"" (lemma "sep_num_le1" )"" "meng(G!1, s!1, t!1, w1!1, w2!1)" "w1!1" "s!1" "t!1" )"1" (assert )"1" (split -1)"1" (skosimp*)"1" (hide 1 2)"1" (hide -7 -8)"1" (lemma "sep_num_is_1" )"1" (inst?)"1" (inst -1 "z!1" )"1" (assert )"1" (split 1)"1" (expand "separates" )"1" "1" expand "singleton" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (expand "separates" )"2" "2" assert )"2" expand "singleton" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" "meng_to_G_sep" )"3" "3" "3" assert )"3" expand "in?" )"3" expand "verts_of" )"3" "3" expand "finseq_appl" )"3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -6 -7 -8 -9 -10)"2" (expand "meng" )"2" (expand "add" )"2" (expand "member" )"2" (expand "disjoint?" )"2" (flatten)"2" (lemma "vert_H_s" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -6 -7 -8 -9 -10)"3" (expand "meng" )"3" (expand "add" ) (("3" (propax) nil nil )) nil ))nil ))nil )"4" (hide -6 -7 -8 -9 -10)"4" (expand "meng" )"4" (expand "add" )"4" (flatten)"4" (expand "member" ) (("4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "disjoint?" ) (("5" (flatten) nil nil )) nil )"6" (expand "disjoint?" ) (("6" (flatten) nil nil )) nil )"7" (assert )"7" (hide -6 -7 -10 2)"7" (expand "separable?" )"7" (flatten)"7" (assert )"7" (expand "meng" )"7" (expand "edge?" )"7" (expand "add" )"7" (expand "union" )"7" expand "member" )"7" expand "disjoint?" )"7" "7" "1" "dbl_eq" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "dbl_eq" )"2" "2" (assert ) nil nil ))nil ))nil )"3" expand "H" )"3" expand "path_comp" )"3" expand "subgraph" )"3" "3" "t!1" )"3" expand "dbl" )"3" "3" expand "del_vert" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "incident" )"4" (skosimp*) nil nil ))nil )"5" expand "incident" )"5" (skosimp*) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "disjoint?" ) (("2" (propax) nil nil )) nil ))nil )"3" (expand "disjoint?" )"3" (flatten) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil meng_scaff nil )nil sep_set_lems nil )nil application-judgement "finite_set[T]" meng_scaff nil )"(total_order?[real])" nil )"bool" sep_sets nil )"bool" graphs nil )"set" sets nil )nil doubletons nil )"Subgraph(G)" meng_scaff_defs nil )"graph[T]" graph_ops nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"finite_set[doubleton[T]]" meng_scaff_defsnil )"(nonempty?)" sets nil )"bool" meng_scaff_defs nil )nil meng_scaff_defs nil )"bool" sets nil )"non_empty_finite_set" finite_sets nil )"finite_set[T]" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" meng_scaff_defs nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )nil meng_scaff nil )"bool" sep_sets nil )"(singleton?)" sets nil )nil sep_set_lems nil )"graph[T]" meng_scaff_defs nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3251049125"" (skosimp*) (("" (expand "in?" ) (("" (flatten) nil nil )) nil ))nil )"bool" meng_scaff_defs nil )) nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )"boolean" notequal nil )nil meng_scaff nil )"bool" meng_scaff_defs nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"finite_set[T]" sep_sets nil )"nat" sep_sets nil )"bool" meng_scaff_defs nil )"bool" sep_sets nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )"boolean" notequal nil )nil meng_scaff nil )"bool" meng_scaff_defs nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"finite_set[T]" sep_sets nil )"nat" sep_sets nil )"bool" meng_scaff_defs nil )"bool" sep_sets nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )"boolean" notequal nil )nil meng_scaff nil )"bool" meng_scaff_defs nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"finite_set[T]" sep_sets nil )"nat" sep_sets nil )"bool" meng_scaff_defs nil )"bool" sep_sets nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "sep_num" )"" (expand "in?" )"" (expand "disjoint?" )"" (flatten)"" case "separates(meng(G!1, s!1, t!1, w1!1, w2!1), dbl(w1!1, w2!1), s!1, t!1)" )"1" (assert )"1" (lemma "min_sep_set_card" )"1" (inst?)"1" (assert )"1" (rewrite "card_dbl" )"1" (lemma "prep_14" )"1" (inst?)"1" (assert )"1" expand "sep_num" )"1" expand "disjoint?" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 8)"2" (expand "meng" )"2" (expand "add" ) (("2" (propax) nil nil ))nil ))nil ))nil )"3" (hide -1 8)"3" (expand "meng" )"3" (expand "add" )"3" (expand "member" )"3" (lemma "vert_H_s" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 8)"2" (expand "separates" )"2" (flatten)"2" (expand "dbl" 1 (1 2))"2" (assert )"2" (skosimp*)"2" (inst + "w!1" )"2" (expand "walk_from?" )"2" "2" assert )"2" expand "walk?" )"2" "1" "1" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" expand "meng" )"1" "1" "1" expand "add" )"1" expand "member" )"1" "1" expand "H" )"1" expand "path_comp" )"1" expand "subgraph" )"1" "1" expand "del_vert" )"1" expand "remove" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "finseq_appl" )"2" expand "edge?" )"2" "2" assert )"2" "2" assert )"2" expand "del_verts" )"2" "2" expand "meng" )"2" expand "union" )"2" expand "add" )"2" expand "member" )"2" "1" expand "verts_in?" )"1" expand "difference" )"1" expand "member" )"1" "1" "dbl_eq" )"1" "1" assert )"1" "1" "1" "1" "n!1" )"1" assert )"1" "1" expand "dbl" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1+1" )"2" assert )"2" "2" expand "dbl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "dbl_eq" )"2" "2" assert )"2" "1" "1" "n!1" )"1" assert )"1" "1" expand "dbl" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1+1" )"2" assert )"2" "2" expand "dbl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "H" )"3" expand "path_comp" )"3" expand "subgraph" )"3" "3" expand "del_vert" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" expand "incident" )"4" nil nil ))nil )"5" expand "incident" )"5" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ) ("4" (assert ) nil nil )"5" (propax) nil nil ) ("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" sep_sets nil )"bool" meng_scaff_defs nil )"graph[T]" meng_scaff_defs nil )"bool" sep_sets nil )"bool" finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil meng_scaff nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil sep_sets nil )nil meng_scaff_defs nil )"bool" sets nil )"(nonempty?)" sets nil )nil meng_scaff nil )"(total_order?[real])" nil )nil doubletons nil )"T" meng_scaff nil )"T" meng_scaff nil )"T" meng_scaff nil )"T" meng_scaff nil )"graph[T]" meng_scaff nil )"bool" walks nil )"int" integers nil )"set" sets nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" subgraphs nil )"graph[T]" graph_ops nil )"set" sets nil )"Subgraph(G)" meng_scaff_defs nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"graph[T]" sep_sets nil )"bool" walks nil )"bool" graphs nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"set" sets nil )"finite_set[doubleton[T]]" meng_scaff_defsnil )nil doubletons nil )"posint" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" meng_scaff_defs nil ))nil ))nil 3251049125"" (skosimp*)"" (lemma "sep_num_gt_0" )"" (inst -1 "G!1" "s!1" "t!1" )"" (expand "in?" )"" (flatten)"" (assert )"" (skosimp*)"" (lemma "walk_to_path_from" )"" (inst?)"" (assert )"" (skosimp*)"" (hide -2)"" case "(EXISTS (i: below(length(p!1))): seq(p!1)(i) = w1!1 OR ") "1" (skosimp*)"1" case "seq(p!1)(i!1) = w1!1" )"1" "1" "one_to_each" )"1" "G!1" "s!1" "t!1" "w1!1" "w2!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" assert )"2" "one_to_each" )"2" "G!1" "s!1" "t!1" "w2!1" "w1!1" )"2" assert )"2" "1" "1" "1" "1" (inst?) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil )"2" "2" rewrite "dbl_comm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "separates" )"2" "2" "p!1" )"2" "2" expand "walk_from?" )"2" expand "path_from?" )"2" "2" expand "from?" )"2" "2" assert )"2" expand "path?" )"2" "2" "2" expand "walk?" )"2" "1" "1" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" expand "dbl" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" expand "edge?" )"2" "2" assert )"2" expand "del_verts" )"2" "2" expand "dbl" )"2" "n!1" )"2" "n!1+1" )"2" expand "finseq_appl" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil meng_scaff nil )nil sep_set_lems nil )"bool" meng_scaff_defs nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil path_ops nil )"bool" sep_sets nil )"bool" walks nil )"bool" paths nil )"set" sets nil )"bool" sets nil )"graph[T]" sep_sets nil )"bool" walks nil )"bool" graphs nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"bool" walks nil )"int" integers nil )"bool" walks nil )"bool" paths nil )nil doubletons nil )nil sep_set_lems nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3251049125"" (skosimp*)"" (case "separates(G!1, singleton(w2!1), s!1, t!1)" )"1" (hide -2 -3 -4)"1" (expand "sep_num" )"1" (lemma "min_sep_set_card" )"1" (inst?)"1" (assert )"1" (hide -2)"1" (rewrite "card_singleton" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "separates" )"2" (flatten)"2" (split +)"1" (expand "singleton" )"1" (expand "dbl" ) (("1" (assert ) nil nil )) nil )) nil )"2" (expand "singleton" )"2" (expand "dbl" ) (("2" (assert ) nil nil )) nil )) nil )"3" (skosimp*)"3" (lemma "walk_to_path_from" )"3" (inst?)"3" (assert )"3" (skosimp*)"3" (hide -2)"3" (inst + "p!1" )"3" (expand "path_from?" )"3" (flatten)"3" "path?_del_verts" )"3" "3" assert )"3" "path?_rev" )"3" "3" assert )"3" expand "path?" -3)"3" expand "finseq_appl" )"3" "3" expand "walk_from?" )"3" assert )"3" expand "from?" )"3" "3" assert )"3" expand "walk?" )"3" expand "finseq_appl" )"3" "3" "1" expand "verts_in?" )"1" "1" expand "del_verts" )"1" expand "difference" )"1" expand "member" )"1" "1" assert )"1" "1" assert )"1" expand "dbl" )"1" expand "singleton" )"1" assert )"1" "rev(p!1)^(0,(length(p!1) - i!1 - 1))" )"1" rewrite "path?_caret" )"1" expand *"^" "min" )"1" expand "rev" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" "1" "1" "length(p!1) - 1 - i!2" )"1" "1" expand "singleton" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "rev" )"2" assert )nil nil ))nil ))nil )"2" expand *"^" "min" )"2" assert )"2" expand "rev" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" "2" assert )"2" "2" assert )"2" expand "del_verts" )"2" assert )"2" "2" assert )"2" expand "verts_in?" )"2" expand "difference" )"2" expand "member" )"2" expand "singleton" )"2" "2" "v!1" )"2" expand "dbl" )"2" "1" replace "1" "1" "rev(p!1)^(0,length(p!1) - n!1 - 1)" )"1" rewrite "path?_caret" )"1" expand *"^" "min" )"1" expand "rev" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" "1" "length(p!1) - 1 - i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "rev" )"2" assert )nil nil ))nil ))nil )"2" expand "rev" )"2" assert )"2" expand *"^" "min" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "rev(p!1)^(0,length(p!1) - n!1 - 2)" )"1" rewrite "path?_caret" )"1" expand *"^" "min" "empty_seq" )"1" expand "rev" )"1" expand "verts_of" )"1" expand "finseq_appl" )"1" "1" "length(p!1) - 1 - i!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "rev" )"2" assert )nil nil ))nil ))nil )"2" expand *"^" "min" "empty_seq" )"2" assert )"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 ))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 )"(singleton?)" sets nil )"bool" sets nil )"bool" sep_sets nil )"bool" finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil meng_scaff nil )"non_empty_finite_set" finite_sets nil )"nat" sep_sets nil )"graph[T]" meng_scaff nil )"T" meng_scaff nil )"T" meng_scaff nil )nil finite_sets nil )"(total_order?[real])" nil )nil sep_sets nil )"graph[T]" sep_sets nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )nil paths nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" walks nil )"bool" walks nil )"int" integers nil )"set" sets nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil paths nil )"(strict_total_order?[real])" real_props nil )"finite_set[T]" walks nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"below(length(p!1))" meng_scaff nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"prewalk[T]" meng_scaff nil )"finseq[T]" doubletons nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )"bool" walks nil )"bool" graphs nil )"finite_set" finite_setsnil )"nat" meng_scaff nil )"finseq" finite_sequences nil )"bool" walks nil )"bool" paths nil )nil path_ops nil )"bool" paths nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil path_ops nil ))nil ))nil 3251049125"" (skosimp*)"" (lemma "prep_16" )"" (inst?)"" (assert )"" (skosimp*)"" (hide -3 -4 -5 -6)"" (lemma "path_from_l" )"" (inst?)"" (assert )"" (expand "disjoint?" )"" (flatten)"" (assert )"" (case "length(p!1) = 2" )"1" (expand "path_from?" )"1" "1" expand "from?" )"1" "1" replace -1)"1" "1" assert )"1" expand "path?" )"1" "1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" "0" )"1" assert )"1" expand "edge?" )"1" rewrite "dbl_comm" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "path_from?" )"2" "2" expand "from?" )"2" "2" "seq(p!1)(1)" )"2" expand "path?" )"2" "2" expand "finseq_appl" )"2" "0" "1" )"2" assert )"2" expand "H" )"2" expand "path_comp" )"2" expand "subgraph" )"2" case "vert(del_vert(del_vert(G!1, w1!1), w2!1))(seq(p!1)(1))" )"1" assert )"1" expand "path_verts" )"1" "1" "p!1^(0,1)" )"1" expand "walk_from?" )"1" expand *"^" "min" )"1" expand "walk?" )"1" expand "finseq_appl" )"1" "1" expand "verts_in?" )"1" "1" "1" expand "del_vert" )"1" expand "remove" )"1" expand "member" )"1" "1" expand "verts_of" )"1" "1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "length(p!1)-1" "i!1" )"2" assert )nil nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" "2" assert )"2" expand "del_vert" )"2" "1" "1" expand "dbl" )"1" expand "remove" )"1" expand "member" )"1" "1" "1+n!1" "length(p!1)-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "dbl" )"2" expand "verts_of" )"2" expand "finseq_appl" )"2" "1+n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand *"^" "min" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "del_vert" )"2" expand "remove" )"2" expand "member" )"2" "1" expand "verts_of" )"1" "1" expand "finseq_appl" )"1" assert )nil nil ))nil ))nil ))nil )"2" "length(p!1)-1" "1" )"2" assert )nil nil ))nil )"3" expand "walk?" )"3" expand "finseq_appl" )"3" "3" "3" expand "verts_in?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil meng_scaff nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" meng_scaff_defs nil )nil naturalnumbers nil )"bool" reals nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" subgraphs nil )"bool" walks nil )"bool" sets nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"finite_set[T]" walks nil )"set" sets nil )"bool" walks nil )"[numfield, numfield -> numfield]" number_fields nil )"finite_set" finite_sets nil )"{k: nat | k <= i AND k <= j}" nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"prewalk[T]" meng_scaff nil )"finseq" finite_sequences nil )"(strict_total_order?[real])" real_props nil )"set[T]" paths nil )"graph[T]" graph_ops nil )"Subgraph(G)" meng_scaff_defs nil )"bool" paths nil )"bool" walks nil )"odd_int" integersnil )"(total_order?[real])" nil )"[below[length(fs)] -> T]" finite_sequencesnil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" graphs nil )nil doubletons nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" walks nil )"bool" paths nil )nil paths nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil meng_scaff nil ))nil ))nil 3251049125"" (skosimp*) (("" (expand "in?" ) (("" (flatten) nil nil )) nil ))nil )"bool" meng_scaff_defs nil )) nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"boolean" notequal nil )nil meng_scaff nil )"bool" graphs nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"boolean" notequal nil )nil meng_scaff nil )"bool" graphs nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"boolean" notequal nil )nil meng_scaff nil )"bool" graphs nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125"" (skosimp*)"" (lemma "path_from_l" )"" (inst?)"" (expand "disjoint?" )"" (flatten)"" (assert )"" (expand "path_from?" )"" (flatten)"" (expand "from?" )"" (flatten)"" (hide -3)"" (expand "path?" )"" (flatten)"" (hide -6)"" expand "walk?" )"" expand "finseq_appl" )"" "" "" "length(p!1) -2" )"" assert )"" expand "edge?" )"" replace -7)"" "" "length(p!1) = 2" )"1" assert )"1" replace -4)"1" "1" expand "meng" )"1" expand "union" )"1" expand "incident" )"1" expand "add" )"1" expand "member" )"1" replace "1" "1" case "dbl[T](w1!1, t!1)(s!1) = dbl[T](s!1, t!1)(s!1)" )"1" "1" expand "dbl" )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" case "dbl[T](w2!1, t!1)(s!1) = dbl[T](s!1, t!1)(s!1)" )"1" "1" expand "dbl" )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil )"3" "H(G!1, s!1, w1!1, w2!1)" )"3" "3" expand "subgraph?" )"3" "3" "3" expand "subset?" )"3" expand "member" )"3" "3" assert )"3" "3" expand "separable?" )"3" expand "edge?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "separable?" )"4" expand "edge?" )"4" nil nil ))nil ))nil ))nil )"5" "5" expand "separable?" )"5" expand "edge?" )"5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -3)"2" "2" "2" expand "separates" )"2" "2" expand "meng" )"2" expand "union" )"2" expand "add" )"2" expand "member" )"2" expand "incident" )"2" "1" case "dbl[T](w1!1, t!1)(w1!1) = dbl[T](seq(p!1)(length(p!1) - 2), t!1)(w1!1)" )"1" "1" expand "dbl" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" case "dbl[T](w2!1, t!1)(w2!1) = dbl[T](seq(p!1)(length(p!1) - 2), t!1)(w2!1)" )"1" "1" expand "dbl" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"3" expand "H" )"3" expand "path_comp" )"3" expand "subgraph" )"3" "3" expand "del_vert" )"3" "3" "seq(p!1)(length(p!1) - 2)" )"3" expand "dbl" )"3" expand "path_verts" )"3" "3" expand "walk_from?" )"3" "3" "add1(w!1,t!1)" )"3" expand "add1" )"3" assert )"3" expand "del_verts" )"3" expand "walk?" )"3" expand "finseq_appl" )"3" "1" expand "verts_in?" )"1" "1" expand "difference" )"1" expand "member" )"1" expand "remove" )"1" expand "member" )"1" "1" "1" "1" "1" assert )nil nil ))nil )"2" "2" "2" expand "in?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "in?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "edge?" )"2" assert )"2" "2" "1" "1" "1" assert )"1" "1" assert )"1" "1" expand "dbl" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1 = length(w!1) - 1" )"1" "1" assert )"1" replace "1" replace "1" expand "dbl" )"1" assert )"1" "1" 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 ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" replace "4" case "dbl[T](seq(p!1)(length(p!1) - 2), t!1)(z!1) = dbl[T](w1!1, z!1)(z!1) AND dbl[T](seq(p!1)(length(p!1) - 2), t!1)(w1!1) = dbl[T](w1!1, z!1)(w1!1)" )"1" "1" "1" expand "dbl" )"1" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"5" "5" "5" case "dbl[T](seq(p!1)(length(p!1) - 2), t!1)(w2!1) = dbl[T](w2!1, z!1)(w2!1) AND dbl[T](seq(p!1)(length(p!1) - 2), t!1)(z!1) = dbl[T](w2!1, z!1)(z!1)" )"1" "1" "1" expand "dbl" )"1" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil meng_scaff nil )nil paths nil )"bool" meng_scaff_defs nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" meng_scaff nil )"bool" paths nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )"graph[T]" meng_scaff_defs nil )"finite_set[doubleton[T]]" meng_scaff_defsnil )"bool" sets nil )"bool" sets nil )"bool" sep_sets nil )"Subgraph(G)" meng_scaff_defs nil )nil subgraphs nil )"bool" subgraphs nil )NOT const-decl "[bool -> bool]" booleans nil )"(nonempty?)" sets nil )"set" sets nil )"even_int" integersnil )"odd_int" integersnil )"Subgraph(G)" meng_scaff_defs nil )"graph[T]" sep_sets nil )"posint" nil )"int" integers nil )"bool" walks nil )"set" sets nil )"set" sets nil ) (< const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"prewalk[T]" meng_scaff nil )nil naturalnumbers nil )"below(1 + length(w!1))" meng_scaff nil )"bool" meng_scaff_defs nil )"finite_set" finite_sets nil )"prewalk" walks nil )"bool" walks nil )"set[T]" paths nil )"graph[T]" graph_ops nil )"Subgraph(G)" subgraphs nil )"bool" sep_sets nil )"bool" graphs nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"bool" walks nil )"bool" walks nil )"bool" paths nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "disjoint?" )"" (flatten)"" (expand "H" )"" (expand "path_comp" )"" (expand "subgraph" )"" (flatten)"" (expand "path_verts" )"" (skosimp*)"" (expand "separates" )"" (flatten)"" (lemma "walk_merge" )"" (inst?)"" (inst -1 "w!2" "s!1" )"" assert )"" "" "p!1" )"" assert )"" rewrite "del_verts_eq" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" meng_scaff_defs nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" subgraphs nil )"set[T]" paths nil )"bool" sep_sets nil )nil walks nil )nil meng_scaff nil )nil sep_set_lems nil )nil application-judgement "finite_set[T]" meng_scaff nil )nil walks nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_sequences nil )nil nat_types nil )nil naturalnumbers nil )"graph[T]" graph_ops nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )"Subgraph(G)" meng_scaff_defs nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )nil meng_scaff nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )"graph[T]" graph_ops nil )"set" sets nil )"set[T]" paths nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )nil meng_scaff nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )"graph[T]" graph_ops nil )"set" sets nil )"set[T]" paths nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil meng_scaff nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )"graph[T]" graph_ops nil )"set" sets nil )"set[T]" paths nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125 ("" (subtype-tcc) nil nil )nil graphs nil )nil graphs nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )nil doubletons nil )"[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 )nil booleans nil )nil booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil walks nil )nil meng_scaff nil )"set[T]" doubletons nil )"graph[T]" sep_sets nil )"bool" sets nil )"set" sets nil )"bool" walks nil )"[below[length(fs)] -> T]" finite_sequencesnil )"boolean" notequal nil )"bool" graphs nil )"bool" walks nil )"bool" walks nil )"bool" sep_sets nil )"bool" meng_scaff_defs nil )"bool" meng_scaff_defs nil )"graph[T]" graph_ops nil )"set" sets nil )"set[T]" paths nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" meng_scaff_defs nil )nil application-judgement "finite_set[T]" meng_scaff nil ))nil ))nil 3251049125"" (skosimp*)"" (expand "in?" )"" (expand "disjoint?" )"" (flatten)"" case "subset?(vert(meng(G!1, s!1, t!1, w1!1, w2!1)),vert(G!1))" )"1" (lemma "card_subset[T]" )"1" (inst?)"1" (assert )"1" (expand "size" )"1" (hide -2)"1" (lemma "line17_prep" )"1" (inst?)"1" (assert )"1" (inst?)"1" expand "disjoint?" )"1" case "NOT vert(meng(G!1, s!1, t!1, w1!1, w2!1))(yt!1)" )"1" "Mt" "vert(meng(G!1, s!1, t!1, w1!1, w2!1))" )"1" case "vert(G!1)(yt!1)" )"1" "1" "same_card_subset[T]" )"1" "Mt" "vert(G!1)" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "H" )"2" expand "path_comp" )"2" expand "subgraph" )"2" "2" expand "del_vert" )"2" "2" expand "remove" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "separates_comm" )"2" "2" assert )"2" "2" expand "meng" )"2" expand "add" )"2" expand "member" )"2" "2" expand "H" )"2" expand "path_comp" )"2" expand "subgraph" )"2" "2" "2" expand "del_vert" )"2" expand "remove" )"2" expand "member" )"2" "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 )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil )"2" (lemma "vert_meng_sub" )"2" (inst?)"2" (expand "in?" )"2" (expand "disjoint?" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ) ("4" (assert ) nil nil )"5" (propax) nil nil ) ("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" meng_scaff_defs nil )nil meng_scaff_defs nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "finite_set[T]" meng_scaff nil )"(partial_order?[set[T]])" nil )NOT const-decl "[bool -> bool]" booleans nil )nil finite_sets nil )"Subgraph(G)" meng_scaff_defs nil )"Subgraph(G)" subgraphs nil )"graph[T]" graph_ops nil )"set" sets nil )"bool" sets nil )"Subgraph(G)" meng_scaff_defs nil )"(nonempty?)" sets nil )nil sep_set_lems nil )"(total_order?[real])" nil )nil meng_scaff nil )"nat" graphs nil )"bool" finite_sets nil )nil meng_scaff nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"graph[T]" meng_scaff_defs nil )"bool" meng_scaff_defs nil ))nil ))nil 3251049125"" (skosimp*)"" (split +)"1" (expand "separable?" )"1" (flatten)"1" (assert )"1" (expand "meng" )"1" (expand "edge?" )"1" (expand "add" )"1" (expand "member" )"1" (expand "union" )"1" (expand "member" )"1" (split -1)"1" (lemma "dbl_eq" )"1" (inst?)"1" assert )"1" expand "disjoint?" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "dbl_eq" )"2" (inst?)"2" assert )"2" expand "disjoint?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"3" (expand "disjoint?" )"3" (flatten)"3" expand "H" )"3" expand "path_comp" )"3" expand "subgraph" )"3" expand "del_vert" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "incident" )"4" (skosimp*) nil nil )) nil )"5" (expand "incident" )"5" (skosimp*) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "line14" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil )"3" (expand "meng" )"3" (expand "add" )"3" (expand "member" )"3" (assert )"3" (expand "in?" )"3" (expand "disjoint?" )"3" (flatten)"3" (assert )"3" (expand "H" )"3" (expand "path_comp" )"3" (expand "subgraph" )"3" (expand "del_vert" )"3" expand "remove" )"3" expand "member" )"3" expand "path_verts" )"3" "gen_seq1(G!1,s!1)" )"3" expand "walk_from?" )"3" expand "gen_seq1" )"3" expand "walk?" )"3" expand "verts_in?" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "meng" )"4" (expand "add" ) (("4" (propax) nil nil )) nil )) nil ))nil ))nil )"graph[T]" meng_scaff_defs nil )"(nonempty?)" sets nil )"set" sets nil )"bool" meng_scaff_defs nil )nil meng_scaff nil )nil doubletons nil )"Subgraph(G)" meng_scaff_defs nil )"graph[T]" graph_ops nil )"Subgraph(G)" subgraphs nil )"Subgraph(G)" meng_scaff_defs nil )"finite_set[doubleton[T]]" meng_scaff_defsnil )"bool" sets nil )"bool" graphs nil )nil application-judgement "finite_set[T]" meng_scaff nil )"bool" sep_sets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil meng_scaff nil )nil naturalnumbers nil )nil nat_types nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil walks nil )"bool" walks nil )nil walks nil )"Seq(G)" walks nil )"bool" walks nil )"bool" walks nil )"set[T]" paths nil )"set" sets nil )"bool" meng_scaff_defs nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.447Bemerkung:
(vorverarbeitet am 2026-04-25)
¤ *Bot Zugriff
2026-05-26
