|
(subtrees
(walk_acr_TCC1 0
(walk_acr_TCC1-1 nil 3251113233 ("" (subtype-tcc) nil nil) nil nil))
(walk_acr_TCC2 0
(walk_acr_TCC2-1 nil 3251113233 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subtrees 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(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)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks 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)
(nil application-judgement "finite_set[T]" subtrees nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(verts_in? const-decl "bool" walks nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(walk_acr_TCC3 0
(walk_acr_TCC3-1 nil 3251113233 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subtrees 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(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)
(> const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks 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)
(nil application-judgement "finite_set[T]" subtrees 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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(edge? const-decl "bool" graphs nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(verts_in? const-decl "bool" walks nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil))
nil))
(walk_acr 0
(walk_acr-1 nil 3251113233
("" (induct "n" 1 "NAT_induction")
(("1" (skosimp*)
(("1" (inst -1 "j!1-1")
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst 3 "j!2") (("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2" (inst 2 "j!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j!1 skolem-const-decl "nat" subtrees nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NAT_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil subtrees 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)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(prewalk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks nil) (< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(walk_acr2 0
(walk_acr2-1 nil 3251113233
("" (induct "n" 1 "NAT_induction")
(("1" (skosimp*)
(("1" (inst -1 "j!1-1")
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst 3 "j!2") (("1" (assert) nil nil)) nil))
nil)
("2" (inst 2 "j!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(j!1 skolem-const-decl "nat" subtrees nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NAT_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil subtrees 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)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(prewalk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(Walk type-eq-decl nil walks nil) (< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(add_dbl_TCC1 0
(add_dbl_TCC1-1 nil 3251113233 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subtrees nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dbl const-decl "set[T]" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nil application-judgement "finite_set[T]" subtrees nil)
(G!1 skolem-const-decl "Graph[T]" subtrees nil)
(/= const-decl "boolean" notequal nil))
nil))
(add_dbl 0
(add_dbl-1 nil 3251113233
("" (skosimp*)
(("" (expand "add")
(("" (expand "member")
(("" (split)
(("1" (replace -1 * rl)
(("1" (hide -1)
(("1" (expand "dbl")
(("1" (flatten) (("1" (ground) nil nil)) nil)) nil))
nil))
nil)
("2" (typepred "G!1")
(("2" (inst?)
(("2" (assert)
(("2" (inst - "x!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((add const-decl "(nonempty?)" sets nil)
(dbl const-decl "set[T]" doubletons nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil subtrees 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)
(doubleton type-eq-decl nil doubletons nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(pregraph type-eq-decl nil graphs nil)
(graph type-eq-decl nil graphs nil)
(nonempty? const-decl "bool" sets nil)
(Graph type-eq-decl nil graphs nil)
(member const-decl "bool" sets nil))
nil))
(max_tree_all_verts 0
(max_tree_all_verts-1 nil 3251113233
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (iff 1)
(("" (prop)
(("1" (hide -2)
(("1" (lemma "max_subtree_subgraph")
(("1" (inst?)
(("1" (expand "subgraph?")
(("1" (flatten)
(("1" (hide -2)
(("1" (expand "subset?")
(("1" (inst?)
(("1" (expand "member")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "max_subtree_tree")
(("2" (inst?)
(("2" (name "TR" "max_subtree(G!1)")
(("2" (case "(EXISTS (v: T): vert(TR)(v))")
(("1" (skosimp*)
(("1" (expand "path_connected?")
(("1" (flatten)
(("1" (inst -5 "v!1" "x!1")
(("1" (assert)
(("1" (skosimp*)
(("1"
(case
"(EXISTS (j: posnat): j < length(w!1) AND vert(TR)(w!1(j-1)) AND
NOT vert(TR)(w!1(j)))")
(("1"
(skosimp*)
(("1"
(typepred "w!1")
(("1"
(expand "walk?")
(("1"
(expand "verts_in?")
(("1"
(expand "finseq_appl")
(("1"
(flatten)
(("1"
(inst - "j!1-1")
(("1"
(assert)
(("1"
(expand "edge?")
(("1"
(name
"ss"
"seq(w!1)(j!1 - 1)")
(("1"
(name
"tt"
"seq(w!1)(j!1)")
(("1"
(name
"TP"
"(# vert := add(tt,vert(TR)),
edges := add(dbl[T](ss,tt),edges(TR)) #)")
(("1"
(case
"tree?(TP)")
(("1"
(lemma
"max_subtree_max")
(("1"
(inst
-1
"G!1"
"TP")
(("1"
(replace
-4)
(("1"
(hide
-2
--4
-5
-6
-7
-8
-9
-10
-11
-13
-14
-15
-16
1
3
4)
(("1"
(replace
-2
*
rl)
(("1"
(hide
-2)
(("1"
(expand
"size")
(("1"
(rewrite
"card_add[T]")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(replace
-4)
(("2"
(inst
-
"j!1")
(("2"
(replace
-3)
(("2"
(hide
-1
-12
3
4)
(("2"
(replace
-1
*
rl)
(("2"
(hide
-1)
(("2"
(expand
"subgraph?")
(("2"
(lemma
"max_subtree_subgraph")
(("2"
(inst?)
(("2"
(replace
-10)
(("2"
(hide
-10)
(("2"
(expand
"subgraph?")
(("2"
(flatten)
(("2"
(split
1)
(("1"
(expand
"subset?")
(("1"
(skosimp*)
(("1"
(expand
"member")
(("1"
(expand
"add")
(("1"
(expand
"member")
(("1"
(split
-1)
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(reveal
-10)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(skosimp*)
(("2"
(expand
"add")
(("2"
(expand
"member")
(("2"
(split
-1)
(("1"
(reveal
-6)
(("1"
(inst
-
"j!1-1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
-2)
(("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)
("2"
(replace
-2)
(("2"
(replace
-3)
(("2"
(expand
"tree?")
(("2"
(flatten)
(("2"
(hide
1)
(("2"
(inst
1
"tt")
(("1"
(split
1)
(("1"
(hide
-11)
(("1"
(expand
"deg")
(("1"
(case-replace
"incident_edges(tt, TP) = singleton[Dbl](dbl[T](ss,tt))")
(("1"
(rewrite
"card_singleton[doubletons[T].doubleton]")
nil
nil)
("2"
(hide
2)
(("2"
(expand
"incident_edges")
(("2"
(expand
"singleton")
(("2"
(replace
-1
*
rl)
(("2"
(hide
-1)
(("2"
(apply-extensionality
:hide?
t)
(("1"
(expand
"add")
(("1"
(expand
"member")
(("1"
(iff)
(("1"
(ground)
(("1"
(typepred
"TR")
(("1"
(hide
-2
-3)
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst
-1
"tt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(expand
"dbl")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(case-replace
"del_vert[T]((# vert := add(tt, vert(TR)),
edges :=
add(dbl[T](ss, tt),
edges(TR))
#),
tt) = TR")
(("1"
(assert)
nil
nil)
("2"
(hide
-11
-12
-13
-14
2
5
6)
(("2"
(apply-extensionality
1
:hide?
t)
(("1"
(expand
"del_vert")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(expand
"add")
(("1"
(expand
"member")
(("1"
(iff
1)
(("1"
(ground)
(("1"
(replace
-1
*
rl)
(("1"
(expand
"dbl")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(typepred
"TR")
(("2"
(inst
-
"x!2")
(("2"
(assert)
(("2"
(inst
-
"tt")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"del_vert")
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(expand
"remove")
(("2"
(expand
"add")
(("2"
(expand
"member")
(("2"
(iff)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(assert)
(("2"
(expand
"add")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(assert)
(("3"
(skosimp*)
(("3"
(replace
-3
*
rl)
(("3"
(hide
-3)
(("3"
(assert)
(("3"
(expand
"add")
(("3"
(expand
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.91 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
