|
(wgt_digraphs_props
(min_wgt_TCC1 0
(min_wgt_TCC1-1 nil 3588008037 ("" (subtype-tcc) nil nil) nil nil))
(walk_member_set_min 0
(walk_member_set_min-1 nil 3588007494
("" (skosimp)
(("" (typepred "w!1" "e!1")
(("" (expand* "member" "nonempty?")
(("" (expand "set_min" 2)
(("" (name-replace "e1" "e!1`1" :hide? nil)
(("" (name-replace "e2" "e!1`2" :hide? nil)
(("" (prop)
(("" (expand "min_wgt")
(("" (lemma "choose_member[Walk(dg(G!1))]")
(("" (inst -1 "set_min(G!1)(e!1)")
(("" (assert)
(("" (expand "member")
((""
(name-replace "ww"
"choose(set_min(G!1)(e!1))")
(("" (expand "set_min" -1)
((""
(flatten)
((""
(replace -3)
((""
(replace -4)
((""
(expand "min_walk?")
((""
(skosimp)
((""
(inst -2 "w1!1")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (Walk type-eq-decl nil walks nil)
(wdg type-eq-decl nil weighted_digraphs nil)
(0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
wgt_digraphs_props nil)
(identity? const-decl "bool" operator_defs nil)
(+ formal-const-decl
"{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
wgt_digraphs_props nil)
(associative? const-decl "bool" operator_defs nil)
(commutative? const-decl "bool" operator_defs nil)
(Weight formal-type-decl nil wgt_digraphs_props nil)
(edge type-eq-decl nil digraphs nil)
(walk? const-decl "bool" walks nil)
(digraph type-eq-decl nil digraphs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs nil)
(prewalk type-eq-decl nil walks nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil wgt_digraphs_props 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(min_wgt const-decl "Weight" wgt_digraphs_props nil)
(min_walk? const-decl "bool" wgt_digraphs_props nil)
(from? const-decl "bool" walks nil)
(choose const-decl "(p)" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(choose_member formula-decl nil sets_lemmas nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member const-decl "bool" sets nil))
nil))
(wgt_min_walk_choose_TCC1 0
(wgt_min_walk_choose_TCC1-1 nil 3588007607 ("" (subtype-tcc) nil nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(prewalk type-eq-decl nil walks nil)
(edgetype type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs nil)
(walk? const-decl "bool" walks nil)
(edge type-eq-decl nil digraphs nil)
(wdg type-eq-decl nil weighted_digraphs nil)
(Walk type-eq-decl nil walks 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)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(edge? const-decl "bool" digraphs nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
wgt_digraphs_props nil)
(identity? const-decl "bool" operator_defs nil)
(+ formal-const-decl
"{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
wgt_digraphs_props nil)
(associative? const-decl "bool" operator_defs nil)
(commutative? const-decl "bool" operator_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Weight formal-type-decl nil wgt_digraphs_props nil)
(wgt_walk const-decl "Weight" weighted_digraphs nil)
(min_walk? const-decl "bool" wgt_digraphs_props nil)
(set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(from? const-decl "bool" walks nil)
(T formal-type-decl nil wgt_digraphs_props nil))
nil))
(wgt_min_walk_choose 0
(wgt_min_walk_choose-1 nil 3588007614
("" (skeep)
(("" (expand "member")
((""
(case "FORALL (w1, w2: Walk(dg(G))):
set_min(G)(u, v)(w1) AND set_min(G)(u, v)(w2)
IMPLIES wgt_walk(G, w1) = wgt_walk(G, w2)")
(("1" (inst -1 "w" "choose(set_min(G)(u, v))")
(("1" (assert) nil nil)) nil)
("2" (hide -1 2)
(("2" (skeep)
(("2" (expand "set_min")
(("2" (flatten)
(("2" (expand "min_walk?")
(("2" (inst -2 "w2")
(("2" (inst -4 "w1")
(("2" (hide -1 -3)
(("2" (typepred "<=")
(("2" (expand "partial_order?")
(("2" (flatten)
(("2"
(hide -1)
(("2"
(expand "antisymmetric?")
(("2"
(inst
-1
"wgt_walk(G, w1)"
"wgt_walk(G, w2)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(min_walk? const-decl "bool" wgt_digraphs_props nil)
(w1 skolem-const-decl "Walk[T](dg(G))" wgt_digraphs_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(partial_order? const-decl "bool" orders nil)
(<= formal-const-decl "{<=: (partial_order?[Weight]) |
FORALL (a, b, c: Weight): a + b <= a + c => b <= c}"
wgt_digraphs_props nil)
(antisymmetric? const-decl "bool" relations nil)
(v skolem-const-decl "T" wgt_digraphs_props nil)
(u skolem-const-decl "T" wgt_digraphs_props nil)
(w2 skolem-const-decl "Walk[T](dg(G))" wgt_digraphs_props nil)
(G skolem-const-decl "wdg[T, Weight, +, 0]" wgt_digraphs_props nil)
(from? const-decl "bool" walks nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil wgt_digraphs_props nil)
(finseq type-eq-decl nil finite_sequences nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(prewalk type-eq-decl nil walks nil)
(edgetype type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(predigraph type-eq-decl nil digraphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(digraph type-eq-decl nil digraphs nil)
(walk? const-decl "bool" walks nil)
(edge type-eq-decl nil digraphs nil)
(Weight formal-type-decl nil wgt_digraphs_props nil)
(commutative? const-decl "bool" operator_defs nil)
(associative? const-decl "bool" operator_defs nil)
(+ formal-const-decl
"{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
wgt_digraphs_props nil)
(identity? const-decl "bool" operator_defs nil)
(0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
wgt_digraphs_props nil)
(wdg type-eq-decl nil weighted_digraphs nil)
(Walk type-eq-decl nil walks nil) (set type-eq-decl nil sets nil)
(set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(wgt_walk const-decl "Weight" weighted_digraphs nil))
nil))
(min_walk_min_wgt 0
(min_walk_min_wgt-1 nil 3588007762
("" (skosimp)
(("" (expand "min_wgt")
(("" (rewrite "wgt_min_walk_choose") nil nil)) nil))
nil)
((min_wgt const-decl "Weight" wgt_digraphs_props nil)
(Walk type-eq-decl nil walks nil)
(walk? const-decl "bool" walks nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(predigraph type-eq-decl nil digraphs nil)
(finite_set type-eq-decl nil finite_sets nil)
(edgetype type-eq-decl nil digraphs 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)
(wdg type-eq-decl nil weighted_digraphs nil)
(0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
wgt_digraphs_props nil)
(identity? const-decl "bool" operator_defs nil)
(+ formal-const-decl
"{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
wgt_digraphs_props nil)
(associative? const-decl "bool" operator_defs nil)
(commutative? const-decl "bool" operator_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Weight formal-type-decl nil wgt_digraphs_props nil)
(edge type-eq-decl nil digraphs nil)
(digraph type-eq-decl nil digraphs nil)
(T formal-type-decl nil wgt_digraphs_props nil)
(wgt_min_walk_choose formula-decl nil wgt_digraphs_props nil))
nil))
(sub_min_walk_nonempty 0
(sub_min_walk_nonempty-1 nil 3562952713
("" (auto-rewrite "finseq_appl")
(("" (skeep)
(("" (case "0 < i AND j < length(w) - 1")
(("1" (flatten)
(("1" (assert)
(("1" (typepred "e")
(("1" (lemma "walk_member_set_min")
(("1" (inst -1 "G" "w" "e")
(("1" (expand "walk_from?")
(("1" (assert)
(("1" (hide -2)
(("1" (expand* "nonempty?" "empty?" "member")
(("1" (name "ww" "w^(i,j)")
(("1" (name-replace "e1" "e`1" :hide? nil)
(("1"
(name-replace "e2" "e`2" :hide? nil)
(("1"
(name-replace
"wi"
"w`seq(i)"
:hide?
nil)
(("1"
(name-replace
"wj"
"w`seq(j)"
:hide?
nil)
(("1"
(inst -12 "ww")
(("1"
(expand "set_min")
(("1"
(split)
(("1"
(hide-all-but (-1 -2 -5 1))
(("1"
(replace -1 1 rl)
(("1"
(replace -2 1 rl)
(("1"
(replace -3 1 rl)
(("1"
(hide -)
(("1"
(expand "from?")
(("1"
(expand*
"^"
"min")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "min_walk?")
(("2"
(skeep)
(("2"
(typepred "w1")
(("2"
(name
"woi"
"w ^ (0, i)")
(("2"
(name
"wjl"
"w ^ (j + 1, length(w) - 1)")
(("2"
(name
"w1t"
"w1 ^ (1, length(w1) - 1)")
(("2"
(name
"w1w"
"woi o w1t o wjl")
(("2"
(inst
-13
"w1w")
(("1"
(lemma
"wgt_walk_decomposed")
(("1"
(inst-cp
-1
"G"
"i"
"w")
(("1"
(assert)
(("1"
(replace
-2
-15)
(("1"
(hide
-2)
(("1"
(inst
-1
"G"
"j - i"
"w ^ (i, length(w) - 1)")
(("1"
(expand
"^"
-1
1)
(("1"
(expand
"min")
(("1"
(rewrite
"walk?_caret")
(("1"
(case
"w ^ (i, length(w) - 1) ^ (0, j - i) = ww")
(("1"
(replace
-1
-2)
(("1"
(expand
"^"
-2
4)
(("1"
(expand
"min")
(("1"
(case
"w ^ (i, length(w) - 1) ^ (j - i, w`length - 1 - i) = w^(j, length(w) - 1)")
(("1"
(replace
-1
-3)
(("1"
(hide
-1
-2)
(("1"
(replace
-1
-14)
(("1"
(hide
-1)
(("1"
(lemma
"wgt_walk_decomposed")
(("1"
(inst-cp
-1
"G"
"i"
"w1w")
(("1"
(split
-2)
(("1"
(case
"w1w ^ (0, i) = w^(0, i)")
(("1"
(replaces
-1)
(("1"
(replace
-1
-15)
(("1"
(hide
-1)
(("1"
(inst
-1
"G"
"length(w1) - 1"
"w1w ^ (i, length(w1w) - 1)")
(("1"
(split
-1)
(("1"
(case
"w1w ^ (i, length(w1w) - 1) ^ (0, length(w1) - 1) = w1")
(("1"
(replaces
-1)
(("1"
(case
"w1w ^ (i, length(w1w) - 1) ^
(length(w1) - 1, length(w1w ^ (i, length(w1w) - 1)) - 1)
= w ^ (j, length(w) - 1)")
(("1"
(replaces
-1)
(("1"
(replaces
-1)
(("1"
(hide
-1)
(("1"
(hide-all-but
(-12
1))
(("1"
(name-replace
"aa"
"wgt_walk(G, w ^ (0, i))")
(("1"
(name-replace
"bb"
"wgt_walk(G, w ^ (j, length(w) - 1))")
(("1"
(name-replace
"cc"
"wgt_walk(G, ww)")
(("1"
(name-replace
"dd"
"wgt_walk(G, w1)")
(("1"
(typepred
"+"
"<=")
(("1"
(copy
-1)
(("1"
(expand
"commutative?")
(("1"
(inst
-1
"cc"
"bb")
(("1"
(inst
-2
"dd"
"bb")
(("1"
(replaces
-1)
(("1"
(replaces
-1)
(("1"
(copy
-1)
(("1"
(expand
"associative?")
(("1"
(inst
-1
"aa"
"bb"
"cc")
(("1"
(inst
-2
"aa"
"bb"
"dd")
(("1"
(replace
-1
-5
rl)
(("1"
(replace
-2
-5
rl)
(("1"
(hide
-1
-2
-3)
(("1"
(inst
-1
"aa + bb"
"cc"
"dd")
(("1"
(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)
("2"
(hide
-1
-7
-13
-14
-17
-18
2)
(("2"
(case
"length(w1w) = length(w1) + length(w) + i - j - 1")
(("1"
(replace
-1
1)
(("1"
(expand
"^"
1
3)
(("1"
(expand
"min")
(("1"
(assert)
(("1"
(decompose-equality
1)
(("1"
(expand
"^"
1)
(("1"
(expand
"min")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(decompose-equality
1)
(("2"
(expand
"^"
1)
(("2"
(expand
"min")
(("2"
(typepred
"x!1")
(("2"
(expand
"^"
-1)
(("2"
(expand*
"min"
"empty_seq")
(("2"
(replace
-3
1
rl)
(("2"
(replace
-4
1
rl)
(("2"
(replace
-5
1
rl)
(("2"
(expand
"o"
1)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(replace
-8
-2
rl)
(("1"
(expand
"^"
-2)
(("1"
(expand*
"min"
"empty_seq")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(case-replace
"length(w1) = 1")
(("1"
(assert)
(("1"
(case-replace
"x!1 = 0")
(("1"
(assert)
(("1"
(replace
-11
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 1.11 Sekunden
(vorverarbeitet)
]
|
