| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/digraphs/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 159 kB |
|
Quelle walks.prfSprache: Lisp |
|||||||||||||||
|
(walks (walk?_TCC1 0 (walk?_TCC1-1 nil 3253634007 ("" (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 walks nil) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (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) (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) (>= 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)) nil)) (walk?_TCC2 0 (walk?_TCC2-1 nil 3253634007 ("" (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 walks nil) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (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) (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) (posint_plus_nnint_is_posint application-judgement "posint" integers 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)) nil)) (from?_TCC1 0 (from?_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (from?_TCC2 0 (from?_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (verts_of_TCC1 0 (verts_of_TCC1-1 nil 3253634007 ("" (skosimp*) (("" (lemma "is_finite_surj[T]") (("" (inst - "{t: T | EXISTS (i: below(length(ww!1))): finseq_appl[T](ww!1)(i) = t}") (("" (assert) (("" (hide 2) (("" (inst 1 "length(ww!1)" "(LAMBDA (i: below(length(ww!1))): seq(ww!1)(i))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst?) (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil walks nil) (is_finite_surj formula-decl nil finite_sets nil) (ww!1 skolem-const-decl "prewalk" walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers 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 "bool" reals 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (edges_of_TCC1 0 (edges_of_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (edges_of_TCC2 0 (edges_of_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (edges_of_TCC3 0 (edges_of_TCC3-1 nil 3253634007 ("" (skosimp*) (("" (lemma "is_finite_surj[edgetype[T]]") (("" (inst?) (("" (assert) (("" (hide 2) (("" (inst + "length(ww!1)-1" "(LAMBDA (i: below[length(ww!1)-1]): (ww!1(i),ww!1(i+1)))") (("1" (expand "finseq_appl") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (skosimp*) (("1" (inst + "i!1") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil walks nil) (is_finite_surj formula-decl nil finite_sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (ww!1 skolem-const-decl "prewalk" walks nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals 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) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (walk_from_l 0 (walk_from_l-2 nil 3560851290 ("" (skosimp*) (("" (expand* "walk_from?" "from?") (("" (flatten) (("" (expand "walk?") (("" (flatten) (("" (inst - "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (walk_from_l-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "walk?") (("" (flatten) (("" (inst - "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (verts_in?_concat_TCC1 0 (verts_in?_concat_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((O const-decl "finseq" finite_sequences nil)) nil)) (verts_in?_concat 0 (verts_in?_concat-1 nil 3253634007 ("" (skosimp*) (("" (expand "verts_in?") (("" (skosimp*) (("" (typepred "i!1") (("" (expand "o ") (("" (ground) (("1" (typepred "s1!1") (("1" (expand "verts_in?") (("1" (inst?) nil nil)) nil)) nil) ("2" (typepred "s2!1") (("2" (expand "verts_in?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (Seq type-eq-decl nil 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) (> const-decl "bool" reals nil) (O const-decl "finseq" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks 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) (< 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) (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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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)) nil)) (verts_in?_caret_TCC1 0 (verts_in?_caret_TCC1-1 nil 3253634007 ("" (skosimp*) (("" (expand "verts_in?") (("" (expand "^") (("" (expand min) (("" (expand "empty_seq") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (verts_in?_caret 0 (verts_in?_caret-1 nil 3253634007 ("" (skosimp*) (("" (expand "verts_in?") (("" (skosimp*) (("" (inst?) (("1" (typepred "i!2") (("1" (expand "^") (("1" (expand "empty_seq") (("1" (lift-if) (("1" (ground) (("1" (typepred "i!2") (("1" (expand "^") (("1" (typepred "j!1") (("1" (reveal -1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "i!1") (("2" (typepred "i!2") (("2" (expand "^") (("2" (lift-if) (("2" (expand "empty_seq") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ps!1 skolem-const-decl "prewalk" walks nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (i!1 skolem-const-decl "nat" walks 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) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (below type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (vert_seq_lem 0 (vert_seq_lem-1 nil 3253634007 ("" (skosimp*) (("" (expand "finseq_appl") (("" (typepred "w!1") (("" (expand "verts_in?") (("" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences 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) (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 walks 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) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil)) nil)) (verts_of_subset 0 (verts_of_subset-1 nil 3253634007 ("" (skosimp*) (("" (typepred "w!1") (("" (expand "subset?") (("" (skosimp*) (("" (expand "verts_in?") (("" (expand "member") (("" (expand "verts_of") (("" (skosimp*) (("" (expand "finseq_appl") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Seq type-eq-decl nil walks nil) (verts_in? 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 walks 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) (member const-decl "bool" sets 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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers 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) (verts_of const-decl "finite_set[T]" walks nil) (subset? const-decl "bool" sets nil)) nil)) (edges_of_subset 0 (edges_of_subset-1 nil 3253634007 ("" (skosimp*) (("" (expand "subset?") (("" (skosimp*) (("" (expand "member") (("" (expand "edges_of") (("" (expand "finseq_appl") (("" (skosimp*) (("" (replace -2) (("" (hide -2) (("" (expand "walk?") (("" (flatten) (("" (inst - "i!1") (("" (assert) (("" (expand "edge?") (("" (expand "finseq_appl") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (walk? const-decl "bool" walks 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) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers 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) (int_minus_int_is_int application-judgement "int" integers nil) (edges_of const-decl "finite_set[edgetype[T]]" walks nil)) nil)) (walk_verts_in 0 (walk_verts_in-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) nil nil)) nil)) nil) ((walk? const-decl "bool" walks nil)) nil)) (walk_from_vert 0 (walk_from_vert-2 nil 3560851336 ("" (skosimp*) (("" (expand* "walk_from?" "from?") (("" (flatten) (("" (expand "walk?") (("" (flatten) (("" (expand "verts_in?") (("" (inst-cp -3 "0") (("" (inst -3 "length(w!1)-1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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)) nil) (walk_from_vert-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "walk?") (("" (flatten) (("" (expand "verts_in?") (("" (inst-cp -3 "0") (("" (inst -3 "length(w!1)-1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (walk_edge_in 0 (walk_edge_in-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split 1) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (expand "verts_of") (("1" (hide -2) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst?) (("1" (split -2) (("1" (propax) nil nil) ("2" (inst?) (("2" (expand "finseq_appl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -5) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst?) (("2" (assert) (("2" (expand "edge?") (("2" (inst?) (("2" (expand "edges_of") (("2" (assert) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks 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) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (subset? const-decl "bool" sets nil) (verts_of const-decl "finite_set[T]" walks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (edgetype type-eq-decl nil digraphs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (edges_of const-decl "finite_set[edgetype[T]]" walks nil) (edge? const-decl "bool" digraphs nil)) nil)) (prewalk_across_TCC1 0 (prewalk_across_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (prewalk_across_TCC2 0 (prewalk_across_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (prewalk_across_TCC3 0 (prewalk_across_TCC3-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (prewalk_across_TCC4 0 (prewalk_across_TCC4-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil)) (prewalk_across 0 (prewalk_across-1 nil 3253634007 ("" (skosimp*) (("" (case "(FORALL (i: below(length(ww!1))): seq(ww!1)(i) = seq(ww!1)(0))") (("1" (inst -1 "length(ww!1)-1") (("1" (assert) (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (induct "i") (("2" (skosimp*) (("2" (reveal 1) (("2" (inst + "jb!1") (("2" (expand "finseq_appl") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (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) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (below_induction formula-decl nil bounded_nat_inductions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (jb!1 skolem-const-decl "below(length(ww!1))" walks nil) (ww!1 skolem-const-decl "prewalk" walks nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (gen_seq1_TCC1 0 (gen_seq1_TCC1-1 nil 3253634007 ("" (skosimp*) (("" (expand "verts_in?") (("" (propax) nil nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil)) nil)) (gen_seq2_TCC1 0 (gen_seq2_TCC1-1 nil 3253634007 ("" (skosimp*) (("" (expand "verts_in?") (("" (propax) nil nil)) nil)) nil) ((verts_in? const-decl "bool" walks nil)) nil)) (trunc1_TCC1 0 (trunc1_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (trunc1_TCC2 0 (trunc1_TCC2-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (add1_TCC1 0 (add1_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) nil nil)) (gen_seq1_is_walk 0 (gen_seq1_is_walk-1 nil 3253634007 ("" (skosimp*) (("" (expand "gen_seq1") (("" (expand "walk?") (("" (expand "verts_in?") (("" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ((gen_seq1 const-decl "Seq(G)" walks nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil)) nil)) (edge_to_walk_TCC1 0 (edge_to_walk_TCC1-1 nil 3253634007 ("" (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 walks nil) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (/= const-decl "boolean" notequal nil)) nil)) (edge_to_walk_TCC2 0 (edge_to_walk_TCC2-1 nil 3253634007 ("" (skosimp*) (("" (typepred "G!1") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((digraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (edge_to_walk 0 (edge_to_walk-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk?") (("" (expand "gen_seq2") (("" (split 2) (("1" (expand "verts_in?") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (assert) (("2" (expand "edge?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks 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) (gen_seq2 const-decl "Seq(G)" walks nil)) nil)) (walk?_caret_TCC1 0 (walk?_caret_TCC1-1 nil 3253634007 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences 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) (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_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) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk?_caret 0 (walk?_caret-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split +) (("1" (rewrite "verts_in?_caret") nil nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (expand "^") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (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) (T formal-type-decl nil walks nil) (verts_in?_caret formula-decl nil walks 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) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs 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) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (edge? const-decl "bool" digraphs nil)) nil)) (l_trunc1_TCC1 0 (l_trunc1_TCC1-1 nil 3253634007 ("" (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 walks nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks 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)) (l_trunc1 0 (l_trunc1-1 nil 3253634007 ("" (skosimp*) (("" (expand "trunc1") (("" (expand "^") (("" (expand min) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((trunc1 const-decl "prewalk" walks 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) (int_minus_int_is_int application-judgement "int" integers nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk?_add1 0 (walk?_add1-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk?") (("" (flatten) (("" (split 1) (("1" (expand "verts_in?") (("1" (expand "add1") (("1" (skosimp*) (("1" (hide -2) (("1" (inst?) (("1" (ground) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "add1") (("2" (lift-if) (("2" (split 1) (("1" (flatten) (("1" (inst?) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((walk? const-decl "bool" walks nil) (add1 const-decl "prewalk" walks nil) (int_minus_int_is_int application-judgement "int" integers 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) (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) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (ww!1 skolem-const-decl "prewalk" walks nil) (x!1 skolem-const-decl "T" walks nil) (below type-eq-decl nil naturalnumbers nil) (i!1 skolem-const-decl "below(length(add1(ww!1, x!1)))" walks nil) (real_lt_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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk_concat_edge_TCC1 0 (walk_concat_edge_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (from? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (O const-decl "finseq" finite_sequences nil)) nil)) (walk_concat_edge 0 (walk_concat_edge-2 nil 3560851383 ("" (skosimp*) (("" (expand* "walk_from?" "from?") (("" (flatten) (("" (expand "o ") (("" (assert) (("" (auto-rewrite "finseq_appl") (("" (expand "walk?") (("" (assert) (("" (flatten) (("" (assert) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (hide -4) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -3) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "n!1 < length(w1!1)") (("1" (assert) (("1" (lift-if) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -5) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (O const-decl "finseq" finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (verts_in? const-decl "bool" walks nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (walk? const-decl "bool" walks nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil) (walk_concat_edge-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "o ") (("" (assert) (("" (auto-rewrite "finseq_appl") (("" (expand "walk?") (("" (assert) (("" (flatten) (("" (assert) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (hide -4) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -3) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "n!1 < length(w1!1)") (("1" (assert) (("1" (lift-if) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -5) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (walk_concat_TCC1 0 (walk_concat_TCC1-1 nil 3253634007 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (from? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil)) nil)) (walk_concat_TCC2 0 (walk_concat_TCC2-1 nil 3253634007 ("" (skosimp*) (("" (expand "o ") (("" (expand "^") (("" (expand min) (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((O const-decl "finseq" finite_sequences 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk_concat 0 (walk_concat-2 nil 3560851417 ("" (skosimp*) (("" (expand* "walk_from?" "from?") (("" (flatten) (("" (assert) (("" (expand "o ") (("" (expand "^") (("" (expand min) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -2 -3 -4 -5 -6 -7 -9) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (case "n!1 < length(w1!1) - 1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (case "n!1 = length(w1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -6) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((from? const-decl "bool" walks nil) (walk_from? const-decl "bool" 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (walk? const-decl "bool" walks nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (edge? const-decl "bool" digraphs nil) (verts_in? const-decl "bool" walks 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) (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) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (T formal-type-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (O const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil) (walk_concat-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (assert) (("" (expand "o ") (("" (expand "^") (("" (expand min) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (flatten) (("" (split +) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (ground) (("1" (inst?) nil nil) ("2" (hide -2 -3 -4 -5 -6 -7 -9) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (case "n!1 < length(w1!1) - 1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (case "n!1 = length(w1!1) - 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -6) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edge? const-decl "bool" digraphs nil)) nil)) (walk?_cut_TCC1 0 (walk?_cut_TCC1-1 nil 3253634007 ("" (subtype-tcc) nil nil) ((from? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil)) nil)) (walk?_cut_TCC2 0 (walk?_cut_TCC2-1 nil 3582042098 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (< 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (from? const-decl "bool" walks nil) (verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk?_cut 0 (walk?_cut-2 nil 3560851456 ("" (skosimp*) (("" (expand* "walk_from?" "from?") (("" (flatten) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (expand "o ") (("" (expand "^") (("" (expand "min") (("" (expand "empty_seq") (("" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (lift-if) (("2" (split 1) (("1" (flatten) (("1" (expand "verts_in?") (("1" (hide -7) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "verts_in?") (("3" (skosimp*) (("3" (hide -6) (("3" (split 1) (("1" (flatten) (("1" (inst?) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "i!2") (("2" (lift-if) (("2" (ground) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lift-if) (("4" (split 1) (("1" (flatten) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil) ("3" (lift-if) (("3" (split 3) (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (case "n!1 = i!1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -4) (("1" (reveal -2) (("1" (inst -1 "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (O const-decl "finseq" finite_sequences 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (verts_in? const-decl "bool" walks nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil)) nil) (walk?_cut-1 nil 3253634007 ("" (skosimp*) (("" (expand "walk_from?") (("" (flatten) (("" (expand "walk?") (("" (expand "finseq_appl") (("" (expand "o ") (("" (expand "^") (("" (expand "min") (("" (expand "empty_seq") (("" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (lift-if) (("2" (split 1) (("1" (flatten) (("1" (expand "verts_in?") (("1" (hide -7) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (expand "verts_in?") (("3" (skosimp*) (("3" (hide -6) (("3" (split 1) (("1" (flatten) (("1" (inst?) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "i!2") (("2" (lift-if) (("2" (ground) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lift-if) (("4" (split 1) (("1" (flatten) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil) ("3" (lift-if) (("3" (split 3) (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (case "n!1 = i!1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (replace -4) (("1" (reveal -2) (("1" (inst -1 "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (walk_merge 0 (walk_merge-2 nil 3560851513 ("" (skosimp*) (("" (case-replace "u!1 = v!1") (("1" (hide -3) (("1" (expand* "walk_from?" "from?") (("1" (flatten) (("1" (lemma "walk_verts_in") (("1" (inst?) (("1" (assert) (("1" (hide -2 -4 -5) (("1" (inst + "gen_seq1(G!1,v!1)") (("1" (expand "gen_seq1") (("1" (expand "walk?") (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "verts_in?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "u!1 = yt!1") (("1" (inst + "p2!1") nil nil) ("2" (lemma "walk_from_l") (("2" (inst?) (("2" (assert) (("2" (lemma "walk_concat") (("2" (inst?) (("2" (inst -1 "v!1" "p2!1") (("2" (assert) (("2" (inst + "p1!1 ^ (0, length(p1!1) - 2) o p2!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil walks nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk_verts_in formula-decl nil walks nil) (int_minus_int_is_int application-judgement "int" integers nil) (G!1 skolem-const-decl "digraph[T]" walks nil) (v!1 skolem-const-decl "T" walks nil) (gen_seq1 const-decl "Seq(G)" walks nil) (Seq type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (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) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers 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) (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) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (edgetype type-eq-decl nil digraphs nil) (walk_from_l formula-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) (O const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (walk_concat formula-decl nil walks nil)) nil) (walk_merge-1 nil 3253634007 ("" (skosimp*) (("" (case-replace "u!1 = v!1") (("1" (hide -3) (("1" (expand "walk_from?") (("1" (flatten) (("1" (lemma "walk_verts_in") (("1" (inst?) (("1" (assert) (("1" (hide -2 -4 -5) (("1" (inst + "gen_seq1(G!1,v!1)") (("1" (expand "gen_seq1") (("1" (expand "walk?") (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "verts_in?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "u!1 = yt!1") (("1" (inst + "p2!1") nil nil) ("2" (lemma "walk_from_l") (("2" (inst?) (("2" (assert) (("2" (lemma "walk_concat") (("2" (inst?) (("2" (inst -1 "v!1" "p2!1") (("2" (assert) (("2" (inst + "p1!1 ^ (0, length(p1!1) - 2) o p2!1") (("2" (hide -1 -3 -4) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((digraph type-eq-decl nil digraphs nil) (predigraph type-eq-decl nil digraphs nil) (edgetype type-eq-decl nil digraphs nil)) nil)) (reord_prewalk_TCC1 0 (reord_prewalk_TCC1-1 nil 3562934566 ("" (subtype-tcc) nil nil) nil nil)) (reord_prewalk_TCC2 0 (reord_prewalk_TCC2-1 nil 3562934566 ("" (skeep) (("" (expand* "o" "^" "min" "empty_seq") (("" (lift-if) (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) 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)) (reord_prewalk_TCC3 0 (reord_prewalk_TCC3-1 nil 3563136007 ("" (grind) 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 walks nil) (finseq type-eq-decl nil finite_sequences nil) (prewalk type-eq-decl nil walks 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (empty_seq const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (^ const-decl "finseq" finite_sequences nil) (O const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (eq_relation_eq_prewalk 0 (eq_relation_eq_prewalk-1 nil 3563236147 ("" (expand "equivalence?") (("" (split) (("1" (expand "reflexive?") (("1" (skeep) (("1" (expand "eq_prewalk?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "symmetric?") (("2" (skeep) (("2" (expand "eq_prewalk?") (("2" (split) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (skeep -1) (("2" (expand "reord_prewalk") (("2" (case "i > length(x) - 1") (("1" (expand "^" -2) (("1" (assert) (("1" (expand "empty_seq") (("1" (expand "o" -2) (("1" (expand "min") (("1" (decompose-equality -2) (("1" (decompose-equality -2) (("1" (lift-if) (("1" (ground) (("1" (decompose-equality 1) (("1" (decompose-equality 1) nil nil)) nil) ("2" (decompose-equality 2) (("2" (decompose-equality 1) nil nil)) nil)) nil)) nil) ("2" (expand "min") (("2" (propax) nil nil)) nil) ("3" (expand "min") (("3" (propax) nil nil)) nil)) nil) ("2" (expand "min") (("2" (propax) nil nil)) nil) ("3" (expand "min") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 3 "length(x) - i") (("1" (decompose-equality 3) (("1" (expand "o") (("1" (decompose-equality -1) (("1" (hide -2) (("1" (expand* "^" "min" "empty_seq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "o" -2) (("2" (decompose-equality -2) (("2" (expand "^" -1) (("2" (expand "min") (("2" (decompose-equality -2) (("1" (expand "o" 1) (("1" (expand "^" 1) (("1" (assert) (("1" (expand "min") (("1" (lift-if) (("1" (ground) (("1" (inst -2 "length(x) - i + x!1") (("1" (expand "^") (("1" (expand "min") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst -1 "length(x) - y`length - i + x!1") (("2" (expand* "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3 2) (("2" (expand* "^" "min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "transitive?") (("3" (skeep) (("3" (expand "eq_prewalk?") (("3" (flatten) (("3" (ground) (("3" (skosimp*) (("3" (expand "reord_prewalk") (("3" (case "i!1 > length(y) - 1 OR i!2 > length(x) - 1") (("1" (split) (("1" (expand "^" -2 1) (("1" (assert) (("1" (case "z = y") (("1" (inst 2 "i!2") (("1" (assert) nil nil)) nil) ("2" (hide -3 2 3) (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (decompose-equality) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "y = x") (("1" (inst 2 "i!1") (("1" (assert) nil nil)) nil) ("2" (hide -2 2 3) (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (decompose-equality) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "o" (-1 -2)) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (decompose-equality) (("2" (expand "^" (-2 -4)) (("2" (expand "min") (("2" (assert) (("2" (expand "^" -1 (1 4)) (("2" (expand "min") (("2" (expand "^" -3 (1 4)) (("2" (expand "min") (("2" (case "i!1 + i!2 = length(x)") (("1" (hide 4) (("1" (decompose-equality 3) (("1" (decompose-equality 1) (("1" (inst -4 "x!1") (("1" (lift-if) (("1" (prop) (("1" (expand "^" -2) (("1" (inst -4 "i!1 + x!1") (("1" (assert) (("1" (expand "^" -4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "^" -1) (("2" (inst -3 "i!1 - y`length + x!1") (("1" (assert) (("1" (expand "^" -3) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "i!1 + i!2 > length(x) - 1") (("1" (inst 5 "i!1 + i!2 - length(x)") (("1" (decompose-equality 5) (("1" (hide -2 -4) (("1" (expand* "o" "^" "min" "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "o" 1) (("2" (expand "^" 1 (1 4)) (("2" (expand "min") (("2" (lift-if) (("2" (ground) (("1" (expand "^" 1) (("1" (inst -6 "x!1") (("1" (lift-if) (("1" (ground) (("1" (expand "^" -2) (("1" (inst -6 "i!1 + x!1") (("1" (assert) (("1" (expand "^" -6) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "^" -1) (("2" (inst -5 "i!1 - y`length + x!1") (("2" (assert) (("2" (expand "^" -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 2) (("2" (inst -5 "x!1") (("2" (assert) (("2" (expand "^" -5) (("2" (inst -3 "i!1 - y`length + x!1") (("2" (assert) (("2" (expand "^" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst 6 "i!1 + i!2") (("2" (decompose-equality 6) (("1" (hide -1 -3) (("1" (expand* "o" "^" "min" "empty_seq") (("1" (assert) nil nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (typepred "x!1") (("2" (expand "o" 1) (("2" (expand "^" 1 (1 4)) (("2" (expand "min") (("2" (lift-if) (("2" (ground) (("1" (expand "^" 1) (("1" (inst -5 "x!1") (("1" (lift-if) (("1" (ground) (("1" (expand "^" -2) (("1" (inst -5 "i!1 + x!1") (("1" (assert) (("1" (expand "^" -5) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 2) (("2" (inst -4 "x!1") (("2" (lift-if) (("2" (ground) (("1" (expand "^" -2) (("1" (inst -4 "i!1 + x!1") (("1" (assert) (("1" (expand "^" -4) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "^" -1) (("2" (inst -3 "i!1 - y`length + x!1") (("2" (assert) (("2" (expand "^" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_prewalk? const-decl "bool" walks nil) (reflexive? const-decl "bool" relations nil) (prewalk type-eq-decl nil walks nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil walks nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (int_minus_int_is_int application-judgement "int" integers nil) (nat_min application-judgement "{k: nat | 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) (O const-decl "finseq" finite_sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (i skolem-const-decl "posnat" walks nil) (x skolem-const-decl "prewalk" walks nil) (reord_prewalk const-decl "prewalk" walks nil) (symmetric? const-decl "bool" relations nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (i!1 skolem-const-decl "posnat" walks nil) (y skolem-const-decl "prewalk" walks nil) (x skolem-const-decl "prewalk" walks nil) (x!1 skolem-const-decl "below[x`length]" walks nil) (i!2 skolem-const-decl "posnat" walks nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) shostak)) (eq_prewalk_length 0 (eq_prewalk_length-1 nil 3579517557 ("" (skeep) (("" (expand "eq_prewalk?") (("" (split) (("1" (assert) nil nil) ("2" (skeep) (("2" (expand "reord_prewalk") (("2" (replaces -1) (("2" (expand* "^" "min" "o") (("2" (assert) (("2" (lift-if) (("2" (expand "empty_seq") (("2" (lift-if) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((eq_prewalk? const-decl "bool" walks 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_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (O const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (reord_prewalk const-decl "prewalk" walks nil)) shostak)) (subwalk_is_walk 0 (subwalk_is_walk-1 nil 3560698081 ("" (skeep) (("" (expand "sub_walk?") (("" (skeep -1) (("" (lemma "walk?_caret") (("" (inst -1 "G" "i" "j" "w") (("" (assert) (("" (expand "^") (("" (typepred "ww") (("" (expand "empty_seq") (("" (decompose-equality -2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sub_walk? const-decl "bool" walks nil) (walk?_caret formula-decl nil walks 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) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (TRUE const-decl "bool" booleans nil) (epsilon const-decl "T" epsilons nil) (pred type-eq-decl nil defined_types nil) (FALSE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (below type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals 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) (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) (T formal-type-decl nil walks nil)) shostak)) (walk_o_TCC1 0 (walk_o_TCC1-1 nil 3561205902 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil)) nil)) (walk_o_TCC2 0 (walk_o_TCC2-1 nil 3561205902 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil)) nil)) (walk_o_TCC3 0 (walk_o_TCC3-1 nil 3561205902 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (O const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (walk_o 0 (walk_o-1 nil 3561206166 ("" (skeep) (("" (case-replace "length(w2) = 1") (("1" (assert) (("1" (expand "^") (("1" (case-replace "w1 o empty_seq = w1") (("1" (hide 2) (("1" (expand "o") (("1" (decompose-equality) (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil) ("2" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (typepred "x!1") (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil) ("3" (skeep) (("3" (expand "empty_seq") (("3" (propax) nil nil)) nil)) nil) ("4" (skeep) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walk_concat_edge") (("2" (inst -1 "G" "seq(w1)(0)" "seq(w2)(1)" "seq(w1)(length(w1) - 1)" "seq(w2)(length(w2) - 1)" "w1" "w2^(1, length(w2) - 1)") (("1" (split) (("1" (expand "walk_from?") (("1" (flatten) nil nil)) nil) ("2" (hide 3) (("2" (expand "walk_from?") (("2" (assert) (("2" (expand "from?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "walk_from?") (("3" (rewrite "walk?_caret") (("3" (expand "from?") (("3" (grind) nil nil)) nil)) nil)) nil) ("4" (replace -3 1) (("4" (hide-all-but (-2 1 2)) (("4" (expand "walk?") (("4" (flatten) (("4" (inst -2 "0") (("4" (assert) (("4" (expand "finseq_appl") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (expand "^") (("2" (assert) (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (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 walks 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "finseq" finite_sequences nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (w1 skolem-const-decl "prewalk" walks nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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_ge_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) (O const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (w2 skolem-const-decl "prewalk" 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (min const-decl "{p: real | p <= m AND p <= n}" real_defs 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (walk?_caret formula-decl nil walks nil) (from? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (walk_concat_edge formula-decl nil walks nil)) shostak)) (edges_o_walk_TCC1 0 (edges_o_walk_TCC1-1 nil 3582042098 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil)) nil)) (edges_o_walk_TCC2 0 (edges_o_walk_TCC2-1 nil 3582042098 ("" (subtype-tcc) nil nil) ((verts_in? const-decl "bool" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil)) nil)) (edges_o_walk_TCC3 0 (edges_o_walk_TCC3-1 nil 3582042098 ("" (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) (edgetype type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (T formal-type-decl nil walks nil) (last const-decl "T" seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (verts_in? const-decl "bool" walks nil) (edge? const-decl "bool" digraphs nil) (walk? const-decl "bool" walks nil) (rest const-decl "finseq" seq_extras "structures/") (O const-decl "finseq" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (edges_o_walk 0 (edges_o_walk-1 nil 3582042116 ("" (auto-rewrite "finseq_appl") (("" (skeep) (("" (case "length(w2) = 1") (("1" (lemma "length_rest_0") (("1" (inst -1 "w2") (("1" (assert) (("1" (rewrite "empty_0") (("1" (replaces -1) (("1" (rewrite "seq_o_empty") (("1" (case-replace "edges_of(w2) = emptyset") (("1" (rewrite "union_empty") nil nil) ("2" (hide-all-but (-1 1)) (("2" (decompose-equality) (("2" (expand "emptyset") (("2" (expand "edges_of") (("2" (skeep) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 2) (("2" (iff) (("2" (expand* "union" "member" "edges_of") (("2" (prop) (("1" (skeep) (("1" (assert) (("1" (typepred "i") (("1" (expand* "o" "rest" "^" "min") (("1" (case "1 + i < w1`length") (("1" (assert) (("1" (hide 2) (("1" (inst 1 "i") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "i < w1`length") (("1" (assert) (("1" (hide 2) (("1" (inst 2 "i - length(w1) + 1") (("1" (expand* "last" "first") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (inst 3 "i - length(w1) + 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (typepred "i") (("2" (inst 1 "i") (("1" (assert) (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "o") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (typepred "i") (("3" (case "i = 0") (("1" (inst 1 "i + length(w1) - 1") (("1" (assert) (("1" (expand "o") (("1" (replaces -1) (("1" (expand* "last" "first") (("1" (assert) (("1" (expand "rest") (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o") (("2" (assert) (("2" (expand "rest") (("2" (expand "^") (("2" (expand "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "i + length(w1) - 1") (("1" (assert) (("1" (expand* "o" "rest" "^" "min") nil nil)) nil) ("2" (expand* "o" "rest" "^" "min") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((O const-decl "finseq" finite_sequences nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (i skolem-const-decl "below(length(w2) - 1)" walks nil) (w1 skolem-const-decl "prewalk" walks nil) (i skolem-const-decl "below(length(w1) - 1)" walks nil) (w2 skolem-const-decl "prewalk" walks nil) (NOT const-decl "[bool -> bool]" booleans 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (last const-decl "T" seq_extras "structures/") (first const-decl "T" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length_rest_0 formula-decl nil seq_extras "structures/") (finite_union application-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (edgetype type-eq-decl nil digraphs 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) (edges_of const-decl "finite_set[edgetype[T]]" walks nil) (emptyset const-decl "set" sets nil) (union_empty formula-decl nil sets_lemmas nil) (seq_o_empty formula-decl nil seq_extras "structures/") (empty_0 formula-decl nil seq_extras "structures/") (rest const-decl "finseq" seq_extras "structures/") (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 walks 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)) shostak)))
¤ Dauer der Verarbeitung: 0.145 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26