| products/sources/formale sprachen/PVS/digraphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: weighted_digraphs.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(weighted_digraphs
(wgt_aux_TCC1 0 (wgt_aux_TCC1-1 nil 3560186128 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (wgt_aux_TCC2 0 (wgt_aux_TCC2-1 nil 3560186128 ("" (subtype-tcc) nil nil) nil nil)) (wgt_aux_TCC3 0 (wgt_aux_TCC3-1 nil 3560186128 ("" (termination-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) (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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil weighted_digraphs nil) (edge? const-decl "bool" digraphs nil)) nil)) (wgt_walk_TCC1 0 (wgt_walk_TCC1-1 nil 3560090441 ("" (subtype-tcc) nil nil) nil nil)) (wgt_aux_shift_walk 0 (wgt_aux_shift_walk-1 nil 3560346969 ("" (skosimp) (("" (auto-rewrite "finseq_appl") (("" (case "j1!1 <= i1!1 OR j2!1 <= i2!1") (("1" (split) (("1" (expand "wgt_aux") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (hide 2) (("1" (expand "^" -2 1) (("1" (lift-if) (("1" (prop) (("1" (expand* "^" "min" "empty_seq") nil nil) ("2" (expand* "^" "min" "empty_seq") nil nil) ("3" (expand* "^" "min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "wgt_aux") (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (hide 2) (("2" (expand "^" -2 2) (("2" (lift-if) (("2" (prop) (("1" (expand* "^" "min" "empty_seq") nil nil) ("2" (expand* "^" "min" "empty_seq") nil nil) ("3" (expand* "^" "min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "^" -1) (("2" (assert) (("2" (expand "min") (("2" (flatten) (("2" (case "FORALL (k:nat): i1!1 + k <= j1!1 IMPLIES wgt_aux(G!1, w1!1)(i1!1, i1!1 + k) = wgt_aux(G!1, w2!1)(i2!1, i2!1 + k)") (("1" (inst -1 "j1!1 - i1!1") (("1" (assert) nil nil)) nil) ("2" (hide 4) (("2" (induct "k") (("1" (assert) (("1" (expand "wgt_aux") (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "wgt_aux" 1) (("2" (assert) (("2" (replaces -1) (("2" (case "wgt(G!1)(w1!1`seq(i1!1 + j), w1!1`seq(1 + i1!1 + j)) = wgt(G!1)(w2!1`seq(i2!1 + j), w2!1`seq(1 + i2!1 + j))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (decompose-equality -3) (("1" (inst-cp -1 "j") (("1" (inst -1 "j + 1") (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil) ("2" (expand "min") (("2" (assert) nil nil)) nil)) nil) ("2" (expand "min") (("2" (assert) nil nil)) nil) ("3" (expand "min") (("3" (assert) nil nil)) nil) ("4" (expand "min") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil) ("4" (skeep) (("4" (assert) nil nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil) ("4" (skeep) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (j skolem-const-decl "nat" weighted_digraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (w2!1 skolem-const-decl "Walk[T](dg(G!1))" weighted_digraphs nil) (i2!1 skolem-const-decl "nat" weighted_digraphs nil) (j1!1 skolem-const-decl "below(length(w1!1))" weighted_digraphs nil) (w1!1 skolem-const-decl "Walk[T](dg(G!1))" weighted_digraphs nil) (G!1 skolem-const-decl "wdg" weighted_digraphs nil) (i1!1 skolem-const-decl "nat" weighted_digraphs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (wgt_aux def-decl "Weight" weighted_digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil weighted_digraphs nil) (finseq type-eq-decl nil finite_sequences 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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil)) shostak)) (wgt_aux_first_TCC1 0 (wgt_aux_first_TCC1-1 nil 3560676770 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" digraphs nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (wgt_aux_first_TCC2 0 (wgt_aux_first_TCC2-1 nil 3579285665 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" digraphs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (wgt_aux_first_TCC3 0 (wgt_aux_first_TCC3-1 nil 3579285665 ("" (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) (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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil weighted_digraphs nil) (edge? const-decl "bool" digraphs nil)) nil)) (wgt_aux_first 0 (wgt_aux_first-1 nil 3560677429 ("" (auto-rewrite "finseq_appl") (("" (induct "j") (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = j!1") (("1" (hide -2) (("1" (expand "wgt_aux") (("1" (assert) (("1" (expand "wgt_aux") (("1" (replaces -1) (("1" (hide -) (("1" (typepred "0") (("1" (expand "identity?") (("1" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "G!1" "w!1" "i!1") (("2" (assert) (("2" (expand "wgt_aux" 2) (("2" (assert) (("2" (typepred "+") (("2" (expand "associative?") (("2" (inst-cp -1 "wgt(G!1)(w!1`seq(i!1), w!1`seq(1 + i!1))" "wgt_aux(G!1, w!1)(1 + i!1, j!1)" "wgt(G!1)(w!1`seq(j!1), w!1`seq(1 + j!1))") (("2" (replace -2 2 rl) (("2" (replace -3 2 rl) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (typepred "w") (("3" (expand* "walk?") (("3" (flatten) (("3" (inst -3 "i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (assert) nil nil)) nil)) nil) ("5" (hide 2) (("5" (skeep) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (T formal-type-decl nil weighted_digraphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (edge? const-decl "bool" digraphs nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (wgt_aux def-decl "Weight" weighted_digraphs nil) (associative? const-decl "bool" operator_defs nil) (+ formal-const-decl "{f: [[Weight, Weight] -> Weight] | associative?(f)}" weighted_digraphs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nat_induction formula-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}" weighted_digraphs nil) (identity? const-decl "bool" operator_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (wgt_aux_split_TCC1 0 (wgt_aux_split_TCC1-1 nil 3560644096 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" digraphs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (wgt_aux_split 0 (wgt_aux_split-1 nil 3560644097 ("" (auto-rewrite "finseq_appl") (("" (induct "n") (("1" (skeep) (("1" (case "i = 0") (("1" (replace -1) (("1" (expand "wgt_aux" 1 2) (("1" (typepred "0") (("1" (hide -2) (("1" (expand "identity?") (("1" (inst?) (("1" (flatten) (("1" (hide -1) (("1" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst -1 "G!1" "w!1" "i!1" "j!2") (("2" (assert) (("2" (case "i!1 = 1 + j!1") (("1" (hide -2) (("1" (replaces -1) (("1" (expand "wgt_aux" 1 2) (("1" (typepred "0") (("1" (hide -2) (("1" (expand "identity?") (("1" (inst?) (("1" (flatten) (("1" (hide -1) (("1" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "wgt_aux" 2 2) (("2" (lemma "wgt_aux_first") (("2" (inst -1 "G!1" "w!1" "j!1" "j!2") (("2" (assert) (("2" (replace -1 -2) (("2" (hide -1) (("2" (typepred "+") (("2" (expand "associative?") (("2" (inst -1 "wgt_aux(G!1, w!1)(i!1, j!1)" "wgt(G!1)(w!1`seq(j!1), w!1`seq(1 + j!1))" "wgt_aux(G!1, w!1)(1 + j!1, j!2)") (("2" (replace -1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (T formal-type-decl nil weighted_digraphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (wgt_aux def-decl "Weight" weighted_digraphs nil) (associative? const-decl "bool" operator_defs nil) (+ formal-const-decl "{f: [[Weight, Weight] -> Weight] | associative?(f)}" weighted_digraphs nil) (nat_induction formula-decl nil naturalnumbers nil) (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}" weighted_digraphs nil) (identity? const-decl "bool" operator_defs nil) (NOT const-decl "[bool -> bool]" booleans 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (wgt_aux_first formula-decl nil weighted_digraphs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (wgt_aux_sub_walk_TCC1 0 (wgt_aux_sub_walk_TCC1-1 nil 3560186371 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks 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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (edge? const-decl "bool" digraphs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (wgt_aux_sub_walk_TCC2 0 (wgt_aux_sub_walk_TCC2-1 nil 3560186371 ("" (skeep) (("" (expand "^" 1 1) (("" (assert) (("" (expand "min") (("" (rewrite "walk?_caret") nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (T formal-type-decl nil weighted_digraphs 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) (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) (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) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (walk?_caret formula-decl nil walks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (wgt_aux_sub_walk 0 (wgt_aux_sub_walk-1 nil 3560186373 ("" (auto-rewrite "finseq_appl") (("" (induct "j") (("1" (skeep) (("1" (expand "wgt_aux") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (case "i!1 = j!1") (("1" (hide -2) (("1" (replaces -1) (("1" (expand* "wgt_aux" "wgt_aux") (("1" (assert) (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "G!1" "w!1" "i!1") (("2" (assert) (("2" (expand "wgt_aux" 2) (("2" (assert) (("2" (expand "^" 2 (2 3)) (("2" (replace -1 2) (("2" (hide -1) (("2" (case "wgt_aux(G!1, w!1 ^ (i!1, j!1))(0, j!1 - i!1) = wgt_aux(G!1, w!1 ^ (i!1, 1 + j!1))(0, j!1 - i!1)") (("1" (assert) nil nil) ("2" (hide 3) (("2" (lemma "wgt_aux_shift_walk") (("2" (inst -1 "G!1" "0" "0" "w!1 ^ (i!1, j!1)" "w!1 ^ (i!1, 1 + j!1)" "j!1 - i!1" "j!1 - i!1") (("2" (assert) (("2" (hide 2) (("2" (decompose-equality) (("1" (expand* "^" "min") nil nil) ("2" (decompose-equality) (("2" (expand* "^" "min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (rewrite "walk?_caret") (("3" (expand* "^" "min") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp) (("4" (expand* "^" "min") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (T formal-type-decl nil weighted_digraphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (wgt_aux def-decl "Weight" weighted_digraphs nil) (nat_induction formula-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (int_plus_int_is_int application-judgement "int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (wgt_aux_shift_walk formula-decl nil weighted_digraphs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (walk?_caret formula-decl nil walks nil)) shostak)) (wgt_walk_to_aux 0 (wgt_walk_to_aux-1 nil 3560642270 ("" (skeep) (("" (expand "wgt_walk") (("" (case "j = i") (("1" (expand "^" 1 2) (("1" (assert) (("1" (expand "min") (("1" (expand "wgt_aux") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "j < i") (("1" (expand "^" 2 2) (("1" (expand "min") (("1" (assert) (("1" (expand "empty_seq") (("1" (expand "wgt_aux") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 3 2) (("2" (assert) (("2" (expand "min") (("2" (lemma "wgt_aux_sub_walk") (("2" (inst -1 "G" "w" "i" "j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((wgt_walk const-decl "Weight" weighted_digraphs nil) (< const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (wgt_aux_sub_walk formula-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (T formal-type-decl nil weighted_digraphs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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)) shostak)) (wgt_walk_decomposed_TCC1 0 (wgt_walk_decomposed_TCC1-1 nil 3560642802 ("" (skeep) (("" (expand "^" 1 1) (("" (expand "min") (("" (assert) (("" (rewrite "walk?_caret") nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (T formal-type-decl nil weighted_digraphs nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals 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) (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) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (walk?_caret formula-decl nil walks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)) nil)) (wgt_walk_decomposed_TCC2 0 (wgt_walk_decomposed_TCC2-1 nil 3560642802 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil weighted_digraphs 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) (walk? const-decl "bool" walks nil)) nil)) (wgt_walk_decomposed_TCC3 0 (wgt_walk_decomposed_TCC3-1 nil 3560642802 ("" (skeep) (("" (expand "^" 1 1) (("" (assert) (("" (expand "min") (("" (rewrite "walk?_caret") nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (T formal-type-decl nil weighted_digraphs nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (wdg type-eq-decl nil weighted_digraphs nil) (Weight formal-type-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil 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) (walk?_caret formula-decl nil walks nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs 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)) (wgt_walk_decomposed 0 (wgt_walk_decomposed-1 nil 3560642810 ("" (skeep) (("" (case-replace "length(w) = 1") (("1" (case-replace "j = 0") (("1" (assert) (("1" (expand "wgt_walk") (("1" (expand "^" 1 (2 4)) (("1" (expand "min") (("1" (replace -2) (("1" (assert) (("1" (expand "wgt_aux") (("1" (typepred "0") (("1" (hide -2) (("1" (expand "identity?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (rewrite "wgt_walk_to_aux") (("1" (rewrite "wgt_walk_to_aux") (("1" (expand "wgt_walk") (("1" (rewrite "wgt_aux_split") nil nil)) nil) ("2" (case-replace "j = length(w) - 1") (("1" (hide - 1 2) (("1" (expand "wgt_walk") (("1" (expand "^" 1 2) (("1" (expand "min") (("1" (expand "wgt_aux" 1 3) (("1" (typepred "0") (("1" (hide -2) (("1" (expand "identity?") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case-replace "j = 0") (("1" (hide - 1 2) (("1" (expand "wgt_walk" 1 2) (("1" (expand "^" 1 2) (("1" (expand "min") (("1" (expand "wgt_aux") (("1" (typepred "0") (("1" (hide -2) (("1" (expand "identity?") (("1" (inst?) (("1" (flatten) (("1" (replaces -2) (("1" (hide -1) (("1" (expand "wgt_walk") (("1" (rewrite "wgt_aux_sub_walk") (("1" (expand "^" 1 3) (("1" (expand "min") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil weighted_digraphs nil) (finseq type-eq-decl nil finite_sequences 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) (odd_minus_odd_is_even application-judgement "even_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) (^ const-decl "finseq" finite_sequences nil) (wgt_aux def-decl "Weight" weighted_digraphs nil) (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}" weighted_digraphs nil) (+ formal-const-decl "{f: [[Weight, Weight] -> Weight] | associative?(f)}" weighted_digraphs nil) (associative? const-decl "bool" operator_defs nil) (identity? const-decl "bool" operator_defs nil) (Weight formal-type-decl nil weighted_digraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (wgt_walk const-decl "Weight" weighted_digraphs 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) (wgt_aux_sub_walk formula-decl nil weighted_digraphs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (wgt_aux_split formula-decl nil weighted_digraphs nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (Walk type-eq-decl nil walks nil) (walk? const-decl "bool" walks 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) (wdg type-eq-decl nil weighted_digraphs nil) (edge type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil) (wgt_walk_to_aux formula-decl nil weighted_digraphs nil)) shostak)) (wgt_walk_edge_TCC1 0 (wgt_walk_edge_TCC1-1 nil 3582035697 ("" (subtype-tcc) nil nil) nil nil)) (wgt_walk_edge_TCC2 0 (wgt_walk_edge_TCC2-1 nil 3582035697 ("" (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) (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) (T formal-type-decl nil weighted_digraphs 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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (edge? const-decl "bool" digraphs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_in? const-decl "bool" walks nil)) nil)) (wgt_walk_edge_TCC3 0 (wgt_walk_edge_TCC3-1 nil 3582035697 ("" (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) (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) (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 weighted_digraphs nil) (wdg type-eq-decl nil weighted_digraphs nil) (Walk type-eq-decl nil walks nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (verts_in? const-decl "bool" walks nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil weighted_digraphs nil) (edge? const-decl "bool" digraphs nil)) nil)) (wgt_walk_edge 0 (wgt_walk_edge-1 nil 3582035801 ("" (skosimp) (("" (expand "finseq_appl") (("" (expand "wgt_walk") (("" (replace -1) (("" (assert) (("" (expand "wgt_aux") (("" (expand "finseq_appl") (("" (expand "wgt_aux") (("" (typepred "0") (("" (expand "identity?") (("" (inst -1 "wgt(G!1)(w!1`seq(0), w!1`seq(1))") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.45 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.Bot Zugriff |
