|
(graph_path_conn
(isolated_not_path 0
(isolated_not_path-1 nil 3263033576
("" (skosimp*)
(("" (expand "path_connected?")
(("" (flatten)
(("" (expand "isolated?")
(("" (expand "empty?" -1)
(("" (expand "member")
(("" (lemma "not_singleton_2_vert")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (inst -4 "x!1" "y!1")
(("" (assert)
(("" (skosimp*)
(("" (typepred "w!1")
((""
(expand "walk?")
((""
(flatten)
((""
(inst - "0")
((""
(assert)
((""
(expand "finseq_appl")
((""
(assert)
((""
(expand "edge?")
((""
(flatten)
((""
(inst
-6
"dbl[T](seq(w!1)(0), seq(w!1)(1))")
((""
(inst?)
((""
(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)
((path_connected? const-decl "bool" graph_conn_defs nil)
(isolated? const-decl "bool" graphs nil)
(member const-decl "bool" sets 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)
(Walk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks 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)
(NOT const-decl "[bool -> bool]" booleans 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" graph_path_conn nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(y!1 skolem-const-decl "T" graph_path_conn nil)
(x!1 skolem-const-decl "T" graph_path_conn nil)
(G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
(T formal-type-decl nil graph_path_conn nil)
(not_singleton_2_vert formula-decl nil graphs nil)
(empty? const-decl "bool" sets nil))
nil))
(pic_A 0
(pic_A-1 nil 3263033576
("" (skosimp*)
(("" (case "NOT singleton?(G!1)")
(("1" (expand "singleton?")
(("1" (expand "size")
(("1" (case "NOT empty?(G!1)")
(("1" (expand "empty?")
(("1" (lemma "card_empty?[T]")
(("1" (inst?)
(("1" (iff)
(("1" (assert)
(("1" (hide 2)
(("1"
(case "(EXISTS (y: T): vert(G!1)(y) AND y /= v!1)")
(("1" (skosimp*)
(("1" (hide 2 3 4)
(("1"
(expand "path_connected?")
(("1"
(flatten)
(("1"
(inst -4 "v!1" "y!1")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(typepred "w!1")
(("1"
(expand "walk?")
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(inst - "0")
(("1"
(assert)
(("1"
(expand
"finseq_appl")
(("1"
(replace -6)
(("1"
(expand
"deg")
(("1"
(expand
"edge?")
(("1"
(flatten)
(("1"
(lemma
"card_empty?[Dbl]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(iff)
(("1"
(assert)
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(inst?)
(("1"
(expand
"incident_edges")
(("1"
(expand
"dbl"
1)
(("1"
(propax)
nil
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)
("2" (hide -2 -3 4)
(("2" (lemma "card_2_has_2[T]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(case-replace "x!1=v!1")
(("1"
(inst 2 "y!1")
(("1" (assert) nil nil))
nil)
("2"
(inst 3 "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -3 -4 1 2)
(("2" (expand "empty?")
(("2" (expand "empty?")
(("2" (inst?)
(("2" (expand "member") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "connected?") (("2" (assert) nil nil)) nil))
nil))
nil)
((singleton? const-decl "bool" graphs 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)
(T formal-type-decl nil graph_path_conn nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(size const-decl "nat" graphs nil)
(is_finite const-decl "bool" finite_sets nil)
(Walk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks 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)
(>= 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)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(deg const-decl "nat" graph_deg nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Dbl type-eq-decl nil doubletons nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" graph_path_conn 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)
(y!1 skolem-const-decl "T" graph_path_conn nil)
(G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
(path_connected? const-decl "bool" graph_conn_defs nil)
(card_2_has_2 formula-decl nil finite_sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_empty? formula-decl nil finite_sets nil)
(empty? const-decl "bool" graphs nil)
(connected? def-decl "bool" graph_conn_defs nil))
nil))
(thw_A 0
(thw_A-1 nil 3263033576
("" (skosimp*)
(("" (hide -1)
(("" (lemma "deg_1_sing")
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (hide -1)
(("" (lemma "other_vert")
(("" (inst?)
(("" (inst?)
(("" (assert)
(("" (skosimp*)
(("" (case-replace "u!1 = y1!1")
(("1"
(case "walk?[T](G!1, gen_seq2[T](G!1, v!1, y1!1))")
(("1"
(inst 3 "gen_seq2(G!1,v!1,y1!1)")
(("1"
(expand "walk_from?")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(expand "gen_seq2")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "walk?")
(("2"
(expand "finseq_appl")
(("2"
(ground)
(("2"
(skosimp*)
(("2"
(expand "gen_seq2")
(("2"
(lift-if)
(("2"
(assert)
(("2"
(rewrite "dbl_comm")
(("2"
(expand "edge?")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "vert(del_vert(G!1,v!1))(u!1) AND vert(del_vert(G!1,v!1))(y1!1)")
(("1"
(flatten)
(("1"
(reveal -5)
(("1"
(inst -1 "del_vert(G!1,v!1)")
(("1"
(split -1)
(("1"
(inst -1 "u!1" "y1!1")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst
4
"gen_seq1(G!1,v!1) o w!1")
(("1"
(expand "gen_seq1")
(("1"
(expand "o ")
(("1"
(expand
"walk_from?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand
"walk?")
(("1"
(expand
"finseq_appl")
(("1"
(expand
"verts_in?")
(("1"
(split)
(("1"
(skosimp*)
(("1"
(ground)
(("1"
(lemma
"vert_seq_lem")
(("1"
(expand
"finseq_appl")
(("1"
(inst?)
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(typepred
"w!1")
(("2"
(expand
"walk?")
(("2"
(expand
"finseq_appl")
(("2"
(flatten)
(("2"
(hide
-3)
(("2"
(expand
"verts_in?")
(("2"
(hide
-11)
(("2"
(expand
"del_vert")
(("2"
(expand
"remove")
(("2"
(expand
"member")
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"w!1")
(("2"
(expand
"walk?")
(("2"
(expand
"finseq_appl")
(("2"
(expand
"verts_in?")
(("2"
(flatten)
(("2"
(skosimp*)
(("2"
(case-replace
"n!1 = 0")
(("1"
(assert)
(("1"
(expand
"edge?")
(("1"
(replace
-6)
(("1"
(rewrite
"dbl_comm")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
(("2"
(inst
-3
"n!1-1")
(("2"
(assert)
(("2"
(expand
"edge?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand
"del_vert"
-3)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(expand "o ")
(("1"
(expand "gen_seq1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide -8 -9)
(("2"
(expand "gen_seq1")
(("2"
(expand*
"walk?"
"finseq_appl")
(("2"
(expand
"verts_in?")
(("2"
(prop)
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(expand
"o ")
(("1"
(ground)
(("1"
(typepred
"w!1")
(("1"
(expand*
"walk?"
"finseq_appl")
(("1"
(flatten)
(("1"
(hide
-3
-4
-5
-6)
(("1"
(expand
"verts_in?")
(("1"
(inst?)
(("1"
(expand
"del_vert")
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"o ")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(case-replace
"n!1 = 0")
(("1"
(expand
"walk_from?")
(("1"
(flatten)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(replace
-3)
(("1"
(expand
"edge?")
(("1"
(rewrite
"dbl_comm")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"w!1")
(("2"
(expand*
"walk?"
"finseq_appl")
(("2"
(expand
"verts_in?")
(("2"
(flatten)
(("2"
(inst
-3
"n!1-1")
(("1"
(assert)
(("1"
(expand
"edge?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(lemma
"edges_del_vert")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("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)
("2"
(rewrite "size_del_vert")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -6 -7 5)
(("2"
(expand "del_vert")
(("2"
(expand "remove")
(("2"
(expand "member")
(("2" (assert) nil 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)
(other_vert formula-decl nil graphs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(w!1 skolem-const-decl "Walk[T](del_vert(G!1, v!1))"
graph_path_conn nil)
(gen_seq1 const-decl "Seq(G)" walks nil)
(O const-decl "finseq" finite_sequences nil)
(vert_seq_lem formula-decl nil walks nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(n!1 skolem-const-decl "nat" graph_path_conn nil)
(edges_del_vert formula-decl nil graph_ops nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(size_del_vert formula-decl nil graph_ops nil)
(gen_seq2 const-decl "Seq(G)" walks nil)
(Seq type-eq-decl nil walks nil)
(verts_in? const-decl "bool" walks nil)
(walk? 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)
(walk_from? const-decl "bool" walks nil)
(nil application-judgement "finite_set[T]" graph_path_conn nil)
(Walk type-eq-decl nil walks nil)
(G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
(v!1 skolem-const-decl "T" graph_path_conn nil)
(y1!1 skolem-const-decl "T" graph_path_conn 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(deg_1_sing formula-decl nil graph_deg nil)
(T formal-type-decl nil graph_path_conn nil))
nil))
(tree_has_walk 0
(tree_has_walk-1 nil 3263033576
("" (induct "TR" 1 "graph_induction_vert")
(("" (skosimp*)
(("" (hide -1)
(("" (expand "tree?")
(("" (split)
(("1" (rewrite "card_one[T]")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (hide 2) (("1" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (case-replace "x!1 =v!1")
(("1" (reveal -1)
(("1" (lemma "thw_A")
(("1" (inst -1 "G!1" "v!1" "y!1")
(("1" (replace -2)
(("1" (hide -2) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (case-replace "y!1 = v!1")
(("1" (lemma "thw_A")
(("1" (inst -1 "G!1" "v!1" "x!1")
(("1" (reveal -2)
(("1" (replace -1)
(("1" (hide -1)
(("1" (assert)
(("1"
(skosimp*)
(("1"
(lemma "walk?_reverse")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (reveal -1)
(("2" (inst?)
(("2" (split -1)
(("1" (inst -1 "x!1" "y!1")
(("1" (assert)
(("1" (split -1)
(("1"
(skosimp*)
(("1"
(inst 4 "w!1")
(("1"
(expand "walk_from?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(typepred "w!1")
(("1"
(lemma "walk?_del_vert")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "walk?_del_vert")
(("2"
(inst?)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 5)
(("2"
(expand "del_vert")
(("2"
(expand "remove")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("3"
(hide -1 -2 5)
(("3"
(expand "del_vert")
(("3"
(expand "remove")
(("3"
(expand "member")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "size_del_vert")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((walk?_reverse formula-decl nil walks nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(size_del_vert formula-decl nil graph_ops nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
(v!1 skolem-const-decl "(vert(G!1))" graph_path_conn nil)
(w!1 skolem-const-decl "Walk[T](del_vert[T](G!1, v!1))"
graph_path_conn nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(walk?_del_vert formula-decl nil path_ops nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(nil application-judgement "finite_set[T]" graph_path_conn nil)
(thw_A formula-decl nil graph_path_conn nil)
(is_finite const-decl "bool" finite_sets nil)
(card_one formula-decl nil finite_sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(singleton const-decl "(singleton?)" sets nil)
(graph_induction_vert formula-decl nil graph_inductions nil)
(T formal-type-decl nil graph_path_conn nil)
(walk_from? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks nil)
(walk? 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)
(tree? def-decl "bool" trees nil)
(pred type-eq-decl nil defined_types 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_implies_conn 0
(path_implies_conn-2 nil 3507897810
("" (induct "G" 1 "graph_induction_vert")
(("" (skosimp*)
(("" (case "(FORALL v: vert(G!1)(v) IMPLIES deg(v,G!1) > 0)")
(("1" (hide -2)
(("1" (expand "connected?")
(("1" (flatten)
(("1" (case "nonempty?(vert(G!1))")
(("1" (name "MTR" "max_subtree(G!1)")
(("1" (lemma "max_tree_all_verts")
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1" (case "tree?(MTR)")
(("1" (expand "tree?" -1)
(("1"
(split)
(("1"
(expand "singleton?")
(("1"
(expand "size")
(("1" (assert) nil nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(name "TCd" "del_vert(MTR,v!1)")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.78 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
