|
(trees
(tree?_TCC1 0
(tree?_TCC1-1 nil 3262616780
("" (skosimp*)
(("" (expand "size")
(("" (expand "del_vert")
(("" (rewrite "card_remove") (("" (assert) nil))))))))
nil)
((size const-decl "nat" graphs nil)
(card_remove formula-decl nil finite_sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_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)
(pregraph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(graph type-eq-decl nil graphs nil)
(T formal-type-decl nil trees 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)
(del_vert const-decl "graph[T]" graph_ops nil))
nil))
(tree_nonempty 0
(tree_nonempty-1 nil 3262616780
("" (skosimp*)
(("" (expand "empty?")
(("" (use "card_empty?[T]")
(("" (assert)
(("" (iff)
(("" (assert)
(("" (expand "tree?")
(("" (skosimp*)
(("" (use "deg_to_card")
(("" (assert)
(("" (expand "size")
(("" (assert) nil))))))))))))))))))))))
nil)
((empty? const-decl "bool" graphs 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)
(size const-decl "nat" graphs nil)
(deg_to_card formula-decl nil graph_deg nil)
(tree? def-decl "bool" trees nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_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)
(pregraph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(graph type-eq-decl nil graphs nil)
(T formal-type-decl nil trees nil)
(card_empty? formula-decl nil finite_sets nil))
nil))
(tree_edge_card 0
(tree_edge_card-1 nil 3262616780
("" (induct "G" 1 "graph_induction_vert")
(("" (skosimp*)
(("" (expand "tree?" -2)
(("" (bddsimp)
(("1" (lemma "singleton_edges")
(("1" (inst -1 "G!1")
(("1" (expand "singleton?" -1)
(("1" (expand "size" -1)
(("1" (assert)
(("1"
(lemma "finite_sets[doubleton[T]].empty_card")
(("1" (inst -1 "edges(G!1)")
(("1" (bddsimp)
(("1" (assert)
(("1" (expand "size" 1)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "size_del_vert")
(("2" (inst -1 "G!1" "v!1")
(("2" (inst -2 "del_vert(G!1,v!1)")
(("2" (assert)
(("2" (replace -1 -2)
(("2" (expand "deg" -3)
(("2" (expand "incident_edges" -3)
(("2"
(lemma
"finite_sets[doubleton[T]].card_one")
(("2"
(inst -1
"{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}")
(("1"
(flatten)
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(expand "del_vert" -4)
(("1"
(lemma
"finite_sets[doubleton[T]].card_disj_union")
(("1"
(inst
-1
"{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}"
"{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}")
(("1"
(prop)
(("1"
(lemma
"finite_sets[doubleton[T]].card_singleton")
(("1"
(inst -1 "x!1")
(("1"
(replace -4 -1 rl)
(("1"
(replace -1 -2)
(("1"
(assert -6)
(("1"
(replace
-6
-2
rl)
(("1"
(expand
"union"
-2)
(("1"
(expand
"member"
-2)
(("1"
(assert
-2)
(("1"
(hide-all-but
-2
-)
(("1"
(case
"{x: doubleton[T] |
edges(G!1)(x) AND x(v!1) OR edges(G!1)(x) AND NOT x(v!1)}=edges(G!1)")
(("1"
(replace
-1
-2)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide
-1
2)
(("2"
(grind)
(("2"
(apply-extensionality
1)
(("2"
(hide
2)
(("2"
(iff
1)
(("2"
(prop)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 -3 -4 -5 2)
(("2"
(expand "disjoint?")
(("2"
(install-rewrites
"finite_sets[doubleton[T]]")
(("2"
(hide -1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"finite_subset[doubleton[T]]")
(("2"
(inst
-
"edges(G!1)"
"{e: doubleton[T] | edges(G!1)(e) AND NOT e(v!1)}")
(("2"
(assert)
(("2"
(hide 2)
(("2"
(expand "subset?")
(("2"
(skosimp*)
(("2"
(expand
"member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3"
(lemma
"finite_subset[doubleton[T]]")
(("3"
(inst
-
"edges(G!1)"
"{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}")
(("3"
(assert)
(("3"
(hide 2)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma "finite_subset[doubleton[T]]")
(("2"
(inst
-
"edges(G!1)"
"{e: doubleton[T] | edges(G!1)(e) AND e(v!1)}")
(("2"
(assert)
(("2"
(hide 2)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty_card formula-decl nil finite_sets nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(singleton? const-decl "bool" graphs nil)
(singleton_edges formula-decl nil graphs nil)
(size_del_vert formula-decl nil graph_ops nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
nil)
(G!1 skolem-const-decl "graph[T]" trees nil)
(v!1 skolem-const-decl "(vert(G!1))" trees nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(card_singleton formula-decl nil finite_sets nil)
(union const-decl "set" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(finite_subset formula-decl nil finite_sets nil)
(card_disj_union formula-decl nil finite_sets nil)
(card_one formula-decl nil finite_sets nil)
(deg const-decl "nat" graph_deg 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)
(graph_induction_vert formula-decl nil graph_inductions nil)
(T formal-type-decl nil trees nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(size const-decl "nat" graphs 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)
(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)
(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))
(tree_edge_k 0
(tree_edge_k-1 nil 3262616780
("" (skosimp*)
(("" (inst? -1)
(("" (inst -1 "size(G!1)-2")
(("1" (lemma "tree_nonempty")
(("1" (inst? -1)
(("1" (bddsimp) (("1" (assert 2) nil nil)) nil)) nil))
nil)
("2" (expand "size" 1)
(("2" (assert 1)
(("2" (case "card[T](vert(G!1)) > 0")
(("1" (hide -2 -3 2) (("1" (grind) nil nil)) nil)
("2" (lemma "tree_nonempty")
(("2" (inst? -1)
(("2" (bddsimp)
(("2" (expand "empty?" 1)
(("2" (lemma "finite_sets[T].empty_card")
(("2" (inst -1 "vert(G!1)")
(("2" (bddsimp)
(("2" (hide -1 -2 1 4 5 6)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil trees 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) (> const-decl "bool" reals nil)
(is_finite const-decl "bool" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" graphs nil)
(empty_card formula-decl nil finite_sets nil)
(tree_nonempty formula-decl nil trees nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(size const-decl "nat" graphs nil)
(G!1 skolem-const-decl "graph[T]" trees 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))
(tree_edge 0
(tree_edge-1 nil 3262616780
("" (induct "k" 1 "nat_induction")
(("1" (skosimp*)
(("1" (copy -2)
(("1" (expand "size" -1)
(("1" (expand "tree?" -2)
(("1" (case "card[T](vert(G!1)) = 1")
(("1" (propax) nil nil)
("2" (split)
(("1" (propax) nil nil)
("2" (hide -3 1 3)
(("2" (skosimp*)
(("2" (case "v!2=v!1")
(("1" (replace -1 -2) (("1" (assert) nil nil))
nil)
("2" (lemma "size_del_vert")
(("2" (inst -1 "G!1" "v!2")
(("2" (reveal -2)
(("2" (replace -1 -2)
(("2"
(assert -2)
(("2"
(expand "size" -2)
(("2"
(lemma "finite_sets[T].card_one")
(("2"
(inst
-1
"vert(del_vert(G!1, v!2))")
(("2"
(bddsimp)
(("2"
(hide -1 -3 -5)
(("2"
(skosimp*)
(("2"
(name
"HH"
"del_vert(G!1, v!2)")
(("2"
(replace -1 -2)
(("2"
(typepred "HH")
(("2"
(expand
"del_vert"
-2)
(("2"
(case
"vert(HH)= remove[T](v!2, vert(G!1))")
(("1"
(hide -3)
(("1"
(expand
"deg"
-4)
(("1"
(lemma
"finite_sets[doubleton[T]].card_one")
(("1"
(inst
-1
"incident_edges(v!2, G!1)")
(("1"
(bddsimp)
(("1"
(hide
-1)
(("1"
(skosimp*)
(("1"
(expand
"incident_edges"
-1)
(("1"
(replace
-2
-4)
(("1"
(hide
-2
-3
-5)
(("1"
(case
" ({e: doubleton[T] | edges(G!1)(e) AND e(v!2)})(x!2) = singleton(x!2)(x!2)")
(("1"
(hide
-2)
(("1"
(beta
-1)
(("1"
(case
"singleton(x!2)(x!2)")
(("1"
(iff
-2)
(("1"
(bddsimp)
(("1"
(lemma
"other_vert")
(("1"
(inst
-1
"G!1"
"x!2"
"v!2")
(("1"
(bddsimp)
(("1"
(skosimp*)
(("1"
(hide
-2
-5)
(("1"
(case
" ({y: T | v!2 /= y AND member(y, vert(G!1))})(x!1) = singleton(x!1)(x!1)")
(("1"
(case
" ({y: T | v!2 /= y AND member(y, vert(G!1))})(u!1) = singleton(x!1)(u!1)")
(("1"
(case
" ({y: T | v!2 /= y AND member(y, vert(G!1))})(v!1) = singleton(x!1)(v!1)")
(("1"
(case
" ({y: T | v!2 /= y AND member(y, vert(G!1))})(v!2) = singleton(x!1)(v!2)")
(("1"
(beta
-1
-2
-3
-4)
(("1"
(beta
-2)
(("1"
(beta
-3)
(("1"
(beta
-4)
(("1"
(hide
-8)
(("1"
(expand
"member"
-)
(("1"
(expand
"singleton"
*)
(("1"
(iff
*)
(("1"
(bddsimp)
(("1"
(assert)
(("1"
(replace
-3
(-6
-7
-8
1)
rl)
(("1"
(hide
-3)
(("1"
(replace
-5
-9)
(("1"
(reveal
-3)
(("1"
(hide
-2
-3
-4
-5
-6
-7
2
3)
(("1"
(expand
"deg"
2)
(("1"
(lemma
"finite_sets[doubleton[T]].nonempty_card")
(("1"
(inst
-1
"incident_edges(v!1, G!1)")
(("1"
(bddsimp)
(("1"
(expand
"nonempty?"
1)
(("1"
(expand
"empty?"
-1)
(("1"
(inst
-1
"x!2")
(("1"
(hide
2)
(("1"
(expand
"member"
1)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(grind)
nil
nil)
("3"
(grind)
nil
nil)
("4"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"singleton")
(("2"
(expand
"remove")
(("2"
(expand
"member")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"member")
(("2"
(expand
"singleton")
(("2"
(expand
"remove")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(ground)
(("2"
(decompose-equality
-6)
(("2"
(inst
-
"v!1")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
-5
-)
(("2"
(name
"hh"
"({y: T | v!2 /= y AND member(y, vert(G!1))})")
(("2"
(replace
-1
1)
(("2"
(grind)
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(expand
"singleton")
(("1"
(ground)
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(assert)
(("1"
(decompose-equality
-2)
(("1"
(inst
-
"u!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"remove")
(("2"
(expand
"member")
(("2"
(expand
"singleton")
(("2"
(ground)
(("2"
(replace
-1
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.256 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
