Quellcode-Bibliothek wgt_digraphs_props.prf

(wgt_digraphs_props
 (min_wgt_TCC1 0
  (min_wgt_TCC1-1 nil 3588008037 ("" (subtype-tcc) nil nil) nil nil))
 (walk_member_set_min 0
  (walk_member_set_min-1 nil 3588007494
   ("" (skosimp)
    (("" (typepred "w!1" "e!1")
      (("" (expand* "member" "nonempty?")
        (("" (expand "set_min" 2)
          (("" (name-replace "e1" "e!1`1" :hide? nil)
            (("" (name-replace "e2" "e!1`2" :hide? nil)
              (("" (prop)
                (("" (expand "min_wgt")
                  (("" (lemma "choose_member[Walk(dg(G!1))]")
                    (("" (inst -1 "set_min(G!1)(e!1)")
                      (("" (assert)
                        (("" (expand "member")
                          ((""
                            (name-replace "ww"
                             "choose(set_min(G!1)(e!1))")
                            (("" (expand "set_min" -1)
                              ((""
                                (flatten)
                                ((""
                                  (replace -3)
                                  ((""
                                    (replace -4)
                                    ((""
                                      (expand "min_walk?")
                                      ((""
                                        (skosimp)
                                        ((""
                                          (inst -2 "w1!1")
                                          (("" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil) (Walk type-eq-decl nil walks nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (associative? const-decl "bool" operator_defs nil)
    (commutative? const-decl "bool" operator_defs nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (edge type-eq-decl nil digraphs nil)
    (walk? const-decl "bool" walks nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (prewalk type-eq-decl nil walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-type-decl nil wgt_digraphs_props nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (min_wgt const-decl "Weight" wgt_digraphs_props nil)
    (min_walk? const-decl "bool" wgt_digraphs_props nil)
    (from? const-decl "bool" walks nil)
    (choose const-decl "(p)" sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (member const-decl "bool" sets nil))
   nil))
 (wgt_min_walk_choose_TCC1 0
  (wgt_min_walk_choose_TCC1-1 nil 3588007607 ("" (subtype-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (walk? const-decl "bool" walks nil)
    (edge type-eq-decl nil digraphs nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (Walk type-eq-decl nil walks nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (verts_in? const-decl "bool" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (edge? const-decl "bool" digraphs nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (associative? const-decl "bool" operator_defs nil)
    (commutative? const-decl "bool" operator_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (wgt_walk const-decl "Weight" weighted_digraphs nil)
    (min_walk? const-decl "bool" wgt_digraphs_props nil)
    (set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (from? const-decl "bool" walks nil)
    (T formal-type-decl nil wgt_digraphs_props nil))
   nil))
 (wgt_min_walk_choose 0
  (wgt_min_walk_choose-1 nil 3588007614
   ("" (skeep)
    (("" (expand "member")
      ((""
        (case "FORALL (w1, w2: Walk(dg(G))):
                                           set_min(G)(u, v)(w1) AND set_min(G)(u, v)(w2)
                                          IMPLIES wgt_walk(G, w1) = wgt_walk(G, w2)")
        (("1" (inst -1 "w" "choose(set_min(G)(u, v))")
          (("1" (assert) nil nil)) nil)
         ("2" (hide -1 2)
          (("2" (skeep)
            (("2" (expand "set_min")
              (("2" (flatten)
                (("2" (expand "min_walk?")
                  (("2" (inst -2 "w2")
                    (("2" (inst -4 "w1")
                      (("2" (hide -1 -3)
                        (("2" (typepred "<=")
                          (("2" (expand "partial_order?")
                            (("2" (flatten)
                              (("2"
                                (hide -1)
                                (("2"
                                  (expand "antisymmetric?")
                                  (("2"
                                    (inst
                                     -1
                                     "wgt_walk(G, w1)"
                                     "wgt_walk(G, w2)")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (min_walk? const-decl "bool" wgt_digraphs_props nil)
    (w1 skolem-const-decl "Walk[T](dg(G))" wgt_digraphs_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (partial_order? const-decl "bool" orders nil)
    (<= formal-const-decl "{<=: (partial_order?[Weight]) |
         FORALL (a, b, c: Weight): a + b <= a + c => b <= c}"
        wgt_digraphs_props nil)
    (antisymmetric? const-decl "bool" relations nil)
    (v skolem-const-decl "T" wgt_digraphs_props nil)
    (u skolem-const-decl "T" wgt_digraphs_props nil)
    (w2 skolem-const-decl "Walk[T](dg(G))" wgt_digraphs_props nil)
    (G skolem-const-decl "wdg[T, Weight, +, 0]" wgt_digraphs_props nil)
    (from? const-decl "bool" walks nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil wgt_digraphs_props nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (edgetype type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (walk? const-decl "bool" walks nil)
    (edge type-eq-decl nil digraphs nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (commutative? const-decl "bool" operator_defs nil)
    (associative? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (Walk type-eq-decl nil walks nil) (set type-eq-decl nil sets nil)
    (set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (wgt_walk const-decl "Weight" weighted_digraphs nil))
   nil))
 (min_walk_min_wgt 0
  (min_walk_min_wgt-1 nil 3588007762
   ("" (skosimp)
    (("" (expand "min_wgt")
      (("" (rewrite "wgt_min_walk_choose") nil nil)) nil))
    nil)
   ((min_wgt const-decl "Weight" wgt_digraphs_props nil)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (associative? const-decl "bool" operator_defs nil)
    (commutative? const-decl "bool" operator_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (edge type-eq-decl nil digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (T formal-type-decl nil wgt_digraphs_props nil)
    (wgt_min_walk_choose formula-decl nil wgt_digraphs_props nil))
   nil))
 (sub_min_walk_nonempty 0
  (sub_min_walk_nonempty-1 nil 3562952713
   ("" (auto-rewrite "finseq_appl")
    (("" (skeep)
      (("" (case "0 < i AND j < length(w) - 1")
        (("1" (flatten)
          (("1" (assert)
            (("1" (typepred "e")
              (("1" (lemma "walk_member_set_min")
                (("1" (inst -1 "G" "w" "e")
                  (("1" (expand "walk_from?")
                    (("1" (assert)
                      (("1" (hide -2)
                        (("1" (expand* "nonempty?" "empty?" "member")
                          (("1" (name "ww" "w^(i,j)")
                            (("1" (name-replace "e1" "e`1" :hide? nil)
                              (("1"
                                (name-replace "e2" "e`2" :hide? nil)
                                (("1"
                                  (name-replace
                                   "wi"
                                   "w`seq(i)"
                                   :hide?
                                   nil)
                                  (("1"
                                    (name-replace
                                     "wj"
                                     "w`seq(j)"
                                     :hide?
                                     nil)
                                    (("1"
                                      (inst -12 "ww")
                                      (("1"
                                        (expand "set_min")
                                        (("1"
                                          (split)
                                          (("1"
                                            (hide-all-but (-1 -2 -5 1))
                                            (("1"
                                              (replace -1 1 rl)
                                              (("1"
                                                (replace -2 1 rl)
                                                (("1"
                                                  (replace -3 1 rl)
                                                  (("1"
                                                    (hide -)
                                                    (("1"
                                                      (expand "from?")
                                                      (("1"
                                                        (expand*
                                                         "^"
                                                         "min")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "min_walk?")
                                            (("2"
                                              (skeep)
                                              (("2"
                                                (typepred "w1")
                                                (("2"
                                                  (name
                                                   "woi"
                                                   "w ^ (0, i)")
                                                  (("2"
                                                    (name
                                                     "wjl"
                                                     "w ^ (j + 1, length(w) - 1)")
                                                    (("2"
                                                      (name
                                                       "w1t"
                                                       "w1 ^ (1, length(w1) - 1)")
                                                      (("2"
                                                        (name
                                                         "w1w"
                                                         "woi o w1t o wjl")
                                                        (("2"
                                                          (inst
                                                           -13
                                                           "w1w")
                                                          (("1"
                                                            (lemma
                                                             "wgt_walk_decomposed")
                                                            (("1"
                                                              (inst-cp
                                                               -1
                                                               "G"
                                                               "i"
                                                               "w")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (replace
                                                                   -2
                                                                   -15)
                                                                  (("1"
                                                                    (hide
                                                                     -2)
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "G"
                                                                       "j - i"
                                                                       "w ^ (i, length(w) - 1)")
                                                                      (("1"
                                                                        (expand
                                                                         "^"
                                                                         -1
                                                                         1)
                                                                        (("1"
                                                                          (expand
                                                                           "min")
                                                                          (("1"
                                                                            (rewrite
                                                                             "walk?_caret")
                                                                            (("1"
                                                                              (case
                                                                               "w ^ (i, length(w) - 1) ^ (0, j - i) = ww")
                                                                              (("1"
                                                                                (replace
                                                                                 -1
                                                                                 -2)
                                                                                (("1"
                                                                                  (expand
                                                                                   "^"
                                                                                   -2
                                                                                   4)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "min")
                                                                                    (("1"
                                                                                      (case
                                                                                       "w ^ (i, length(w) - 1) ^ (j - i, w`length - 1 - i) = w^(j, length(w) - 1)")
                                                                                      (("1"
                                                                                        (replace
                                                                                         -1
                                                                                         -3)
                                                                                        (("1"
                                                                                          (hide
                                                                                           -1
                                                                                           -2)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -1
                                                                                             -14)
                                                                                            (("1"
                                                                                              (hide
                                                                                               -1)
                                                                                              (("1"
                                                                                                (lemma
                                                                                                 "wgt_walk_decomposed")
                                                                                                (("1"
                                                                                                  (inst-cp
                                                                                                   -1
                                                                                                   "G"
                                                                                                   "i"
                                                                                                   "w1w")
                                                                                                  (("1"
                                                                                                    (split
                                                                                                     -2)
                                                                                                    (("1"
                                                                                                      (case
                                                                                                       "w1w ^ (0, i) = w^(0, i)")
                                                                                                      (("1"
                                                                                                        (replaces
                                                                                                         -1)
                                                                                                        (("1"
                                                                                                          (replace
                                                                                                           -1
                                                                                                           -15)
                                                                                                          (("1"
                                                                                                            (hide
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -1
                                                                                                               "G"
                                                                                                               "length(w1) - 1"
                                                                                                               "w1w ^ (i, length(w1w) - 1)")
                                                                                                              (("1"
                                                                                                                (split
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (case
                                                                                                                   "w1w ^ (i, length(w1w) - 1) ^ (0, length(w1) - 1) = w1")
                                                                                                                  (("1"
                                                                                                                    (replaces
                                                                                                                     -1)
                                                                                                                    (("1"
                                                                                                                      (case
                                                                                                                       "w1w ^ (i, length(w1w) - 1) ^
                                                                                                                                                                                                                                                         (length(w1) - 1, length(w1w ^ (i, length(w1w) - 1)) - 1)
                                                                                                                                                                                                                                               = w ^ (j, length(w) - 1)")
                                                                                                                      (("1"
                                                                                                                        (replaces
                                                                                                                         -1)
                                                                                                                        (("1"
                                                                                                                          (replaces
                                                                                                                           -1)
                                                                                                                          (("1"
                                                                                                                            (hide
                                                                                                                             -1)
                                                                                                                            (("1"
                                                                                                                              (hide-all-but
                                                                                                                               (-12
                                                                                                                                1))
                                                                                                                              (("1"
                                                                                                                                (name-replace
                                                                                                                                 "aa"
                                                                                                                                 "wgt_walk(G, w ^ (0, i))")
                                                                                                                                (("1"
                                                                                                                                  (name-replace
                                                                                                                                   "bb"
                                                                                                                                   "wgt_walk(G, w ^ (j, length(w) - 1))")
                                                                                                                                  (("1"
                                                                                                                                    (name-replace
                                                                                                                                     "cc"
                                                                                                                                     "wgt_walk(G, ww)")
                                                                                                                                    (("1"
                                                                                                                                      (name-replace
                                                                                                                                       "dd"
                                                                                                                                       "wgt_walk(G, w1)")
                                                                                                                                      (("1"
                                                                                                                                        (typepred
                                                                                                                                         "+"
                                                                                                                                         "<=")
                                                                                                                                        (("1"
                                                                                                                                          (copy
                                                                                                                                           -1)
                                                                                                                                          (("1"
                                                                                                                                            (expand
                                                                                                                                             "commutative?")
                                                                                                                                            (("1"
                                                                                                                                              (inst
                                                                                                                                               -1
                                                                                                                                               "cc"
                                                                                                                                               "bb")
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -2
                                                                                                                                                 "dd"
                                                                                                                                                 "bb")
                                                                                                                                                (("1"
                                                                                                                                                  (replaces
                                                                                                                                                   -1)
                                                                                                                                                  (("1"
                                                                                                                                                    (replaces
                                                                                                                                                     -1)
                                                                                                                                                    (("1"
                                                                                                                                                      (copy
                                                                                                                                                       -1)
                                                                                                                                                      (("1"
                                                                                                                                                        (expand
                                                                                                                                                         "associative?")
                                                                                                                                                        (("1"
                                                                                                                                                          (inst
                                                                                                                                                           -1
                                                                                                                                                           "aa"
                                                                                                                                                           "bb"
                                                                                                                                                           "cc")
                                                                                                                                                          (("1"
                                                                                                                                                            (inst
                                                                                                                                                             -2
                                                                                                                                                             "aa"
                                                                                                                                                             "bb"
                                                                                                                                                             "dd")
                                                                                                                                                            (("1"
                                                                                                                                                              (replace
                                                                                                                                                               -1
                                                                                                                                                               -5
                                                                                                                                                               rl)
                                                                                                                                                              (("1"
                                                                                                                                                                (replace
                                                                                                                                                                 -2
                                                                                                                                                                 -5
                                                                                                                                                                 rl)
                                                                                                                                                                (("1"
                                                                                                                                                                  (hide
                                                                                                                                                                   -1
                                                                                                                                                                   -2
                                                                                                                                                                   -3)
                                                                                                                                                                  (("1"
                                                                                                                                                                    (inst
                                                                                                                                                                     -1
                                                                                                                                                                     "aa + bb"
                                                                                                                                                                     "cc"
                                                                                                                                                                     "dd")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (hide
                                                                                                                         -1
                                                                                                                         -7
                                                                                                                         -13
                                                                                                                         -14
                                                                                                                         -17
                                                                                                                         -18
                                                                                                                         2)
                                                                                                                        (("2"
                                                                                                                          (case
                                                                                                                           "length(w1w) = length(w1) + length(w) + i - j - 1")
                                                                                                                          (("1"
                                                                                                                            (replace
                                                                                                                             -1
                                                                                                                             1)
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "^"
                                                                                                                               1
                                                                                                                               3)
                                                                                                                              (("1"
                                                                                                                                (expand
                                                                                                                                 "min")
                                                                                                                                (("1"
                                                                                                                                  (assert)
                                                                                                                                  (("1"
                                                                                                                                    (decompose-equality
                                                                                                                                     1)
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "^"
                                                                                                                                       1)
                                                                                                                                      (("1"
                                                                                                                                        (expand
                                                                                                                                         "min")
                                                                                                                                        (("1"
                                                                                                                                          (propax)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil)
                                                                                                                                     ("2"
                                                                                                                                      (decompose-equality
                                                                                                                                       1)
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "^"
                                                                                                                                         1)
                                                                                                                                        (("2"
                                                                                                                                          (expand
                                                                                                                                           "min")
                                                                                                                                          (("2"
                                                                                                                                            (typepred
                                                                                                                                             "x!1")
                                                                                                                                            (("2"
                                                                                                                                              (expand
                                                                                                                                               "^"
                                                                                                                                               -1)
                                                                                                                                              (("2"
                                                                                                                                                (expand*
                                                                                                                                                 "min"
                                                                                                                                                 "empty_seq")
                                                                                                                                                (("2"
                                                                                                                                                  (replace
                                                                                                                                                   -3
                                                                                                                                                   1
                                                                                                                                                   rl)
                                                                                                                                                  (("2"
                                                                                                                                                    (replace
                                                                                                                                                     -4
                                                                                                                                                     1
                                                                                                                                                     rl)
                                                                                                                                                    (("2"
                                                                                                                                                      (replace
                                                                                                                                                       -5
                                                                                                                                                       1
                                                                                                                                                       rl)
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "o"
                                                                                                                                                         1)
                                                                                                                                                        (("2"
                                                                                                                                                          (lift-if)
                                                                                                                                                          (("2"
                                                                                                                                                            (ground)
                                                                                                                                                            (("1"
                                                                                                                                                              (replace
                                                                                                                                                               -8
                                                                                                                                                               -2
                                                                                                                                                               rl)
                                                                                                                                                              (("1"
                                                                                                                                                                (expand
                                                                                                                                                                 "^"
                                                                                                                                                                 -2)
                                                                                                                                                                (("1"
                                                                                                                                                                  (expand*
                                                                                                                                                                   "min"
                                                                                                                                                                   "empty_seq")
                                                                                                                                                                  (("1"
                                                                                                                                                                    (lift-if)
                                                                                                                                                                    (("1"
                                                                                                                                                                      (ground)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (case-replace
                                                                                                                                                                         "length(w1) = 1")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (assert)
                                                                                                                                                                          (("1"
                                                                                                                                                                            (case-replace
                                                                                                                                                                             "x!1 = 0")
                                                                                                                                                                            (("1"
                                                                                                                                                                              (assert)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (replace
                                                                                                                                                                                 -11
                                                                                                                                                                                 1
                                                                                                                                                                                 rl)
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (expand
                                                                                                                                                                                   "^"
                                                                                                                                                                                   1)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (expand
                                                                                                                                                                                     "from?")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (flatten)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (replace
                                                                                                                                                                                         -2)
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (assert)
                                                                                                                                                                                          nil
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil)
                                                                                                                                                                             ("2"
                                                                                                                                                                              (assert)
                                                                                                                                                                              nil
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil)
                                                                                                                                                                         ("2"
                                                                                                                                                                          (assert)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil)
                                                                                                                                                                       ("2"
                                                                                                                                                                        (case-replace
                                                                                                                                                                         "length(w1) = 1")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (assert)
                                                                                                                                                                          (("1"
                                                                                                                                                                            (case-replace
                                                                                                                                                                             "x!1 = 0")
                                                                                                                                                                            (("1"
                                                                                                                                                                              (assert)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (replace
                                                                                                                                                                                 -11
                                                                                                                                                                                 1
                                                                                                                                                                                 rl)
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (expand
                                                                                                                                                                                   "^"
                                                                                                                                                                                   1)
                                                                                                                                                                                  (("1"
                                                                                                                                                                                    (expand
                                                                                                                                                                                     "from?")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (flatten)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (replace
                                                                                                                                                                                         -2)
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (assert)
                                                                                                                                                                                          nil
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil)
                                                                                                                                                                             ("2"
                                                                                                                                                                              (assert)
                                                                                                                                                                              nil
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil)
                                                                                                                                                                         ("2"
                                                                                                                                                                          (assert)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil)
                                                                                                                                                                       ("3"
                                                                                                                                                                        (case-replace
                                                                                                                                                                         "x!1 = 0")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (assert)
                                                                                                                                                                          (("1"
                                                                                                                                                                            (replace
                                                                                                                                                                             -9
                                                                                                                                                                             -3
                                                                                                                                                                             rl)
                                                                                                                                                                            (("1"
                                                                                                                                                                              (expand
                                                                                                                                                                               "^"
                                                                                                                                                                               -3)
                                                                                                                                                                              (("1"
                                                                                                                                                                                (expand
                                                                                                                                                                                 "min")
                                                                                                                                                                                (("1"
                                                                                                                                                                                  (assert)
                                                                                                                                                                                  nil
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil)
                                                                                                                                                                         ("2"
                                                                                                                                                                          (assert)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil)
                                                                                                                                                             ("2"
                                                                                                                                                              (replace
                                                                                                                                                               -7
                                                                                                                                                               -1
                                                                                                                                                               rl)
                                                                                                                                                              (("2"
                                                                                                                                                                (expand
                                                                                                                                                                 "^"
                                                                                                                                                                 -1)
                                                                                                                                                                (("2"
                                                                                                                                                                  (expand*
                                                                                                                                                                   "min"
                                                                                                                                                                   "empty_seq")
                                                                                                                                                                  (("2"
                                                                                                                                                                    (replace
                                                                                                                                                                     -7
                                                                                                                                                                     1
                                                                                                                                                                     rl)
                                                                                                                                                                    (("2"
                                                                                                                                                                      (expand
                                                                                                                                                                       "^"
                                                                                                                                                                       1)
                                                                                                                                                                      (("2"
                                                                                                                                                                        (expand
                                                                                                                                                                         "min")
                                                                                                                                                                        (("2"
                                                                                                                                                                          (lift-if)
                                                                                                                                                                          (("2"
                                                                                                                                                                            (ground)
                                                                                                                                                                            (("2"
                                                                                                                                                                              (replace
                                                                                                                                                                               -7
                                                                                                                                                                               4
                                                                                                                                                                               rl)
                                                                                                                                                                              (("2"
                                                                                                                                                                                (expand
                                                                                                                                                                                 "^"
                                                                                                                                                                                 4)
                                                                                                                                                                                (("2"
                                                                                                                                                                                  (expand
                                                                                                                                                                                   "min")
                                                                                                                                                                                  (("2"
                                                                                                                                                                                    (case-replace
                                                                                                                                                                                     "x!1 = 0")
                                                                                                                                                                                    (("1"
                                                                                                                                                                                      (assert)
                                                                                                                                                                                      (("1"
                                                                                                                                                                                        (expand
                                                                                                                                                                                         "from?")
                                                                                                                                                                                        (("1"
                                                                                                                                                                                          (propax)
                                                                                                                                                                                          nil
                                                                                                                                                                                          nil))
                                                                                                                                                                                        nil))
                                                                                                                                                                                      nil)
                                                                                                                                                                                     ("2"
                                                                                                                                                                                      (assert)
                                                                                                                                                                                      nil
                                                                                                                                                                                      nil))
                                                                                                                                                                                    nil))
                                                                                                                                                                                  nil))
                                                                                                                                                                                nil))
                                                                                                                                                                              nil))
                                                                                                                                                                            nil))
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil)
                                                                                                                                                             ("3"
                                                                                                                                                              (replace
                                                                                                                                                               -6
                                                                                                                                                               (1
                                                                                                                                                                2)
                                                                                                                                                               rl)
                                                                                                                                                              (("3"
                                                                                                                                                                (expand
                                                                                                                                                                 "^"
                                                                                                                                                                 (1
                                                                                                                                                                  2))
                                                                                                                                                                (("3"
                                                                                                                                                                  (expand*
                                                                                                                                                                   "min"
                                                                                                                                                                   "empty_seq")
                                                                                                                                                                  (("3"
                                                                                                                                                                    (lift-if)
                                                                                                                                                                    (("3"
                                                                                                                                                                      (ground)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil)
                                                                                                                           ("2"
                                                                                                                            (hide
                                                                                                                             2)
                                                                                                                            (("2"
                                                                                                                              (replace
                                                                                                                               -1
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (replace
                                                                                                                                   -2
                                                                                                                                   1
                                                                                                                                   rl)
                                                                                                                                  (("2"
                                                                                                                                    (replace
                                                                                                                                     -3
                                                                                                                                     1
                                                                                                                                     rl)
                                                                                                                                    (("2"
                                                                                                                                      (replace
                                                                                                                                       -4
                                                                                                                                       1
                                                                                                                                       rl)
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "^"
                                                                                                                                         1)
                                                                                                                                        (("2"
                                                                                                                                          (expand*
                                                                                                                                           "min"
                                                                                                                                           "empty_seq")
                                                                                                                                          (("2"
                                                                                                                                            (lift-if)
                                                                                                                                            (("2"
                                                                                                                                              (ground)
                                                                                                                                              nil
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("3"
                                                                                                                        (hide
                                                                                                                         -1
                                                                                                                         -7
                                                                                                                         -8
                                                                                                                         -13
                                                                                                                         -14
                                                                                                                         -17
                                                                                                                         -18
                                                                                                                         2)
                                                                                                                        (("3"
                                                                                                                          (replace
                                                                                                                           -1
                                                                                                                           1
                                                                                                                           rl)
                                                                                                                          (("3"
                                                                                                                            (replace
                                                                                                                             -2
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("3"
                                                                                                                              (replace
                                                                                                                               -3
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("3"
                                                                                                                                (replace
                                                                                                                                 -4
                                                                                                                                 1
                                                                                                                                 rl)
                                                                                                                                (("3"
                                                                                                                                  (hide
                                                                                                                                   -1
                                                                                                                                   -2
                                                                                                                                   -3
                                                                                                                                   -4)
                                                                                                                                  (("3"
                                                                                                                                    (expand*
                                                                                                                                     "o"
                                                                                                                                     "^"
                                                                                                                                     "min"
                                                                                                                                     "empty_seq")
                                                                                                                                    (("3"
                                                                                                                                      (assert)
                                                                                                                                      (("3"
                                                                                                                                        (lift-if)
                                                                                                                                        (("3"
                                                                                                                                          (lift-if)
                                                                                                                                          (("3"
                                                                                                                                            (lift-if)
                                                                                                                                            (("3"
                                                                                                                                              (ground)
                                                                                                                                              nil
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (hide
                                                                                                                     -1
                                                                                                                     -7
                                                                                                                     -13
                                                                                                                     -14
                                                                                                                     -17
                                                                                                                     -18
                                                                                                                     2)
                                                                                                                    (("2"
                                                                                                                      (decompose-equality
                                                                                                                       1)
                                                                                                                      (("1"
                                                                                                                        (replace
                                                                                                                         -1
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "o"
                                                                                                                           1
                                                                                                                           (3
                                                                                                                            4))
                                                                                                                          (("1"
                                                                                                                            (replace
                                                                                                                             -2
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("1"
                                                                                                                              (replace
                                                                                                                               -3
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("1"
                                                                                                                                (replace
                                                                                                                                 -4
                                                                                                                                 1
                                                                                                                                 rl)
                                                                                                                                (("1"
                                                                                                                                  (hide
                                                                                                                                   -1
                                                                                                                                   -2
                                                                                                                                   -3
                                                                                                                                   -4)
                                                                                                                                  (("1"
                                                                                                                                    (grind)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (decompose-equality)
                                                                                                                        (("1"
                                                                                                                          (case
                                                                                                                           "length(w1w) =  length(w1) + length(w) + i - j - 1")
                                                                                                                          (("1"
                                                                                                                            (typepred
                                                                                                                             "x!1")
                                                                                                                            (("1"
                                                                                                                              (replace
                                                                                                                               -2)
                                                                                                                              (("1"
                                                                                                                                (expand
                                                                                                                                 "^"
                                                                                                                                 -1)
                                                                                                                                (("1"
                                                                                                                                  (expand*
                                                                                                                                   "min"
                                                                                                                                   "empty_seq")
                                                                                                                                  (("1"
                                                                                                                                    (replace
                                                                                                                                     -2)
                                                                                                                                    (("1"
                                                                                                                                      (assert)
                                                                                                                                      (("1"
                                                                                                                                        (expand
                                                                                                                                         "^"
                                                                                                                                         1)
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "min")
                                                                                                                                          (("1"
                                                                                                                                            (replace
                                                                                                                                             -3
                                                                                                                                             1
                                                                                                                                             rl)
                                                                                                                                            (("1"
                                                                                                                                              (replace
                                                                                                                                               -4
                                                                                                                                               1
                                                                                                                                               rl)
                                                                                                                                              (("1"
                                                                                                                                                (replace
                                                                                                                                                 -5
                                                                                                                                                 1
                                                                                                                                                 rl)
                                                                                                                                                (("1"
                                                                                                                                                  (replace
                                                                                                                                                   -6
                                                                                                                                                   1
                                                                                                                                                   rl)
                                                                                                                                                  (("1"
                                                                                                                                                    (expand
                                                                                                                                                     "o"
                                                                                                                                                     1)
                                                                                                                                                    (("1"
                                                                                                                                                      (expand
                                                                                                                                                       "^"
                                                                                                                                                       1)
                                                                                                                                                      (("1"
                                                                                                                                                        (expand*
                                                                                                                                                         "min"
                                                                                                                                                         "empty_seq")
                                                                                                                                                        (("1"
                                                                                                                                                          (lift-if)
                                                                                                                                                          (("1"
                                                                                                                                                            (lift-if)
                                                                                                                                                            (("1"
                                                                                                                                                              (lift-if)
                                                                                                                                                              (("1"
                                                                                                                                                                (assert)
                                                                                                                                                                (("1"
                                                                                                                                                                  (ground)
                                                                                                                                                                  (("1"
                                                                                                                                                                    (case-replace
                                                                                                                                                                     "x!1 = 0")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (expand
                                                                                                                                                                         "from?")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (propax)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil)
                                                                                                                                                                     ("2"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil)
                                                                                                                                                                   ("2"
                                                                                                                                                                    (case-replace
                                                                                                                                                                     "x!1 = 0")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (expand
                                                                                                                                                                         "from?")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (propax)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil)
                                                                                                                                                                     ("2"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil)
                                                                                                                                                                   ("3"
                                                                                                                                                                    (case-replace
                                                                                                                                                                     "x!1 = 0")
                                                                                                                                                                    (("1"
                                                                                                                                                                      (assert)
                                                                                                                                                                      (("1"
                                                                                                                                                                        (expand
                                                                                                                                                                         "from?")
                                                                                                                                                                        (("1"
                                                                                                                                                                          (propax)
                                                                                                                                                                          nil
                                                                                                                                                                          nil))
                                                                                                                                                                        nil))
                                                                                                                                                                      nil)
                                                                                                                                                                     ("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)
                                                                                                                           ("2"
                                                                                                                            (hide
                                                                                                                             2)
                                                                                                                            (("2"
                                                                                                                              (replace
                                                                                                                               -1
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (replace
                                                                                                                                   -3
                                                                                                                                   1
                                                                                                                                   rl)
                                                                                                                                  (("2"
                                                                                                                                    (replace
                                                                                                                                     -2
                                                                                                                                     1
                                                                                                                                     rl)
                                                                                                                                    (("2"
                                                                                                                                      (replace
                                                                                                                                       -4
                                                                                                                                       1
                                                                                                                                       rl)
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "^"
                                                                                                                                         1)
                                                                                                                                        (("2"
                                                                                                                                          (expand*
                                                                                                                                           "min"
                                                                                                                                           "empty_seq")
                                                                                                                                          (("2"
                                                                                                                                            (lift-if)
                                                                                                                                            (("2"
                                                                                                                                              (ground)
                                                                                                                                              nil
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (replace
                                                                                                                           -1
                                                                                                                           1
                                                                                                                           rl)
                                                                                                                          (("2"
                                                                                                                            (expand
                                                                                                                             "o"
                                                                                                                             1)
                                                                                                                            (("2"
                                                                                                                              (replace
                                                                                                                               -4
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "^"
                                                                                                                                 1)
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "min")
                                                                                                                                  (("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("3"
                                                                                                                        (replace
                                                                                                                         -1
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("3"
                                                                                                                          (expand
                                                                                                                           "o"
                                                                                                                           1)
                                                                                                                          (("3"
                                                                                                                            (replace
                                                                                                                             -4
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("3"
                                                                                                                              (expand
                                                                                                                               "^"
                                                                                                                               1)
                                                                                                                              (("3"
                                                                                                                                (expand
                                                                                                                                 "min")
                                                                                                                                (("3"
                                                                                                                                  (assert)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("3"
                                                                                                                    (replace
                                                                                                                     -2
                                                                                                                     1
                                                                                                                     rl)
                                                                                                                    (("3"
                                                                                                                      (expand
                                                                                                                       "o"
                                                                                                                       1)
                                                                                                                      (("3"
                                                                                                                        (replace
                                                                                                                         -5
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("3"
                                                                                                                          (expand
                                                                                                                           "^"
                                                                                                                           1)
                                                                                                                          (("3"
                                                                                                                            (expand
                                                                                                                             "min")
                                                                                                                            (("3"
                                                                                                                              (assert)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (hide-all-but
                                                                                                                   (-1
                                                                                                                    -2
                                                                                                                    -3
                                                                                                                    -4
                                                                                                                    -5
                                                                                                                    -16
                                                                                                                    -17
                                                                                                                    -18
                                                                                                                    1))
                                                                                                                  (("2"
                                                                                                                    (replace
                                                                                                                     -1
                                                                                                                     1
                                                                                                                     rl)
                                                                                                                    (("2"
                                                                                                                      (replace
                                                                                                                       -2
                                                                                                                       1
                                                                                                                       rl)
                                                                                                                      (("2"
                                                                                                                        (replace
                                                                                                                         -3
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (replace
                                                                                                                           -4
                                                                                                                           1
                                                                                                                           rl)
                                                                                                                          (("2"
                                                                                                                            (hide
                                                                                                                             -1
                                                                                                                             -2
                                                                                                                             -3
                                                                                                                             -4)
                                                                                                                            (("2"
                                                                                                                              (grind)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("3"
                                                                                                                  (hide
                                                                                                                   -13
                                                                                                                   -17
                                                                                                                   2)
                                                                                                                  (("3"
                                                                                                                    (case-replace
                                                                                                                     "w1w ^ (i, length(w1w) - 1) = w1 o wjl")
                                                                                                                    (("1"
                                                                                                                      (lemma
                                                                                                                       "walk_o")
                                                                                                                      (("1"
                                                                                                                        (inst
                                                                                                                         -1
                                                                                                                         "dg(G)"
                                                                                                                         "w1"
                                                                                                                         "w ^ (j, length(w) - 1)")
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          (("1"
                                                                                                                            (rewrite
                                                                                                                             "walk?_caret")
                                                                                                                            (("1"
                                                                                                                              (case
                                                                                                                               " w ^ (j, length(w) - 1) ^ (1, length(w ^ (j, length(w) - 1)) - 1) = wjl")
                                                                                                                              (("1"
                                                                                                                                (replaces
                                                                                                                                 -1)
                                                                                                                                (("1"
                                                                                                                                  (assert)
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "^"
                                                                                                                                     1)
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "from?")
                                                                                                                                      (("1"
                                                                                                                                        (flatten)
                                                                                                                                        (("1"
                                                                                                                                          (assert)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("2"
                                                                                                                                (hide-all-but
                                                                                                                                 (-5
                                                                                                                                  -15
                                                                                                                                  -16
                                                                                                                                  -18
                                                                                                                                  1))
                                                                                                                                (("2"
                                                                                                                                  (replace
                                                                                                                                   -1
                                                                                                                                   1
                                                                                                                                   rl)
                                                                                                                                  (("2"
                                                                                                                                    (hide
                                                                                                                                     -1)
                                                                                                                                    (("2"
                                                                                                                                      (grind)
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil)
                                                                                                                               ("3"
                                                                                                                                (hide-all-but
                                                                                                                                 1)
                                                                                                                                (("3"
                                                                                                                                  (grind)
                                                                                                                                  nil
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (hide-all-but
                                                                                                                           1)
                                                                                                                          (("2"
                                                                                                                            (grind)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil)
                                                                                                                     ("2"
                                                                                                                      (hide
                                                                                                                       -6
                                                                                                                       -12
                                                                                                                       -15
                                                                                                                       2)
                                                                                                                      (("2"
                                                                                                                        (case
                                                                                                                         "length(w1w) =  length(w1) + length(w) + i - j - 1")
                                                                                                                        (("1"
                                                                                                                          (replace
                                                                                                                           -1)
                                                                                                                          (("1"
                                                                                                                            (decompose-equality
                                                                                                                             1)
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "o"
                                                                                                                               1)
                                                                                                                              (("1"
                                                                                                                                (replace
                                                                                                                                 -4
                                                                                                                                 1
                                                                                                                                 rl)
                                                                                                                                (("1"
                                                                                                                                  (expand
                                                                                                                                   "^"
                                                                                                                                   1)
                                                                                                                                  (("1"
                                                                                                                                    (expand*
                                                                                                                                     "min"
                                                                                                                                     "empty_seq")
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil)
                                                                                                                             ("2"
                                                                                                                              (decompose-equality
                                                                                                                               1)
                                                                                                                              (("2"
                                                                                                                                (typepred
                                                                                                                                 "x!1")
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "^"
                                                                                                                                   -1)
                                                                                                                                  (("2"
                                                                                                                                    (expand
                                                                                                                                     "min")
                                                                                                                                    (("2"
                                                                                                                                      (expand
                                                                                                                                       "^"
                                                                                                                                       1)
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "o"
                                                                                                                                         1)
                                                                                                                                        (("2"
                                                                                                                                          (lift-if)
                                                                                                                                          (("2"
                                                                                                                                            (ground)
                                                                                                                                            (("1"
                                                                                                                                              (replace
                                                                                                                                               -4
                                                                                                                                               1
                                                                                                                                               rl)
                                                                                                                                              (("1"
                                                                                                                                                (expand
                                                                                                                                                 "o"
                                                                                                                                                 1)
                                                                                                                                                (("1"
                                                                                                                                                  (lift-if)
                                                                                                                                                  (("1"
                                                                                                                                                    (ground)
                                                                                                                                                    (("1"
                                                                                                                                                      (replace
                                                                                                                                                       -9
                                                                                                                                                       *
                                                                                                                                                       rl)
                                                                                                                                                      (("1"
                                                                                                                                                        (expand
                                                                                                                                                         "^"
                                                                                                                                                         (-1
                                                                                                                                                          -2
                                                                                                                                                          1))
                                                                                                                                                        (("1"
                                                                                                                                                          (expand
                                                                                                                                                           "min")
                                                                                                                                                          (("1"
                                                                                                                                                            (case-replace
                                                                                                                                                             "x!1 = 0")
                                                                                                                                                            (("1"
                                                                                                                                                              (assert)
                                                                                                                                                              (("1"
                                                                                                                                                                (expand
                                                                                                                                                                 "from?")
                                                                                                                                                                (("1"
                                                                                                                                                                  (propax)
                                                                                                                                                                  nil
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil)
                                                                                                                                                             ("2"
                                                                                                                                                              (assert)
                                                                                                                                                              nil
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil)
                                                                                                                                                     ("2"
                                                                                                                                                      (replace
                                                                                                                                                       -6
                                                                                                                                                       2
                                                                                                                                                       rl)
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "^"
                                                                                                                                                         2)
                                                                                                                                                        (("2"
                                                                                                                                                          (case-replace
                                                                                                                                                           "length(w1) = 1")
                                                                                                                                                          (("1"
                                                                                                                                                            (hide
                                                                                                                                                             2)
                                                                                                                                                            (("1"
                                                                                                                                                              (expand
                                                                                                                                                               "^"
                                                                                                                                                               -7)
                                                                                                                                                              (("1"
                                                                                                                                                                (replace
                                                                                                                                                                 -7
                                                                                                                                                                 -2
                                                                                                                                                                 rl)
                                                                                                                                                                (("1"
                                                                                                                                                                  (expand
                                                                                                                                                                   "empty_seq"
                                                                                                                                                                   -2)
                                                                                                                                                                  (("1"
                                                                                                                                                                    (propax)
                                                                                                                                                                    nil
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil)
                                                                                                                                                           ("2"
                                                                                                                                                            (assert)
                                                                                                                                                            (("2"
                                                                                                                                                              (replace
                                                                                                                                                               -8
                                                                                                                                                               3
                                                                                                                                                               rl)
                                                                                                                                                              (("2"
                                                                                                                                                                (expand
                                                                                                                                                                 "^"
                                                                                                                                                                 3)
                                                                                                                                                                (("2"
                                                                                                                                                                  (expand
                                                                                                                                                                   "min")
                                                                                                                                                                  (("2"
                                                                                                                                                                    (propax)
                                                                                                                                                                    nil
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil)
                                                                                                                                                     ("3"
                                                                                                                                                      (replace
                                                                                                                                                       -5
                                                                                                                                                       1
                                                                                                                                                       rl)
                                                                                                                                                      (("3"
                                                                                                                                                        (replace
                                                                                                                                                         -7
                                                                                                                                                         1
                                                                                                                                                         rl)
                                                                                                                                                        (("3"
                                                                                                                                                          (expand
                                                                                                                                                           "^"
                                                                                                                                                           1)
                                                                                                                                                          (("3"
                                                                                                                                                            (expand*
                                                                                                                                                             "min"
                                                                                                                                                             "empty_seq")
                                                                                                                                                            (("3"
                                                                                                                                                              (lift-if)
                                                                                                                                                              (("3"
                                                                                                                                                                (case
                                                                                                                                                                 "length(w1) = 1")
                                                                                                                                                                (("1"
                                                                                                                                                                  (assert)
                                                                                                                                                                  nil
                                                                                                                                                                  nil)
                                                                                                                                                                 ("2"
                                                                                                                                                                  (assert)
                                                                                                                                                                  nil
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil)
                                                                                                                                             ("2"
                                                                                                                                              (replace
                                                                                                                                               -3
                                                                                                                                               2
                                                                                                                                               rl)
                                                                                                                                              (("2"
                                                                                                                                                (expand
                                                                                                                                                 "o"
                                                                                                                                                 2)
                                                                                                                                                (("2"
                                                                                                                                                  (lift-if)
                                                                                                                                                  (("2"
                                                                                                                                                    (ground)
                                                                                                                                                    (("1"
                                                                                                                                                      (replace
                                                                                                                                                       -8
                                                                                                                                                       -1
                                                                                                                                                       rl)
                                                                                                                                                      (("1"
                                                                                                                                                        (expand
                                                                                                                                                         "^"
                                                                                                                                                         -1)
                                                                                                                                                        (("1"
                                                                                                                                                          (expand
                                                                                                                                                           "min")
                                                                                                                                                          (("1"
                                                                                                                                                            (case-replace
                                                                                                                                                             "x!1 = 0")
                                                                                                                                                            (("1"
                                                                                                                                                              (assert)
                                                                                                                                                              nil
                                                                                                                                                              nil)
                                                                                                                                                             ("2"
                                                                                                                                                              (assert)
                                                                                                                                                              nil
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil)
                                                                                                                                                     ("2"
                                                                                                                                                      (replace
                                                                                                                                                       -5
                                                                                                                                                       -1
                                                                                                                                                       rl)
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "^"
                                                                                                                                                         -1)
                                                                                                                                                        (("2"
                                                                                                                                                          (expand*
                                                                                                                                                           "min"
                                                                                                                                                           "empty_seq")
                                                                                                                                                          (("2"
                                                                                                                                                            (lift-if)
                                                                                                                                                            (("2"
                                                                                                                                                              (ground)
                                                                                                                                                              (("2"
                                                                                                                                                                (replace
                                                                                                                                                                 -7
                                                                                                                                                                 -1
                                                                                                                                                                 rl)
                                                                                                                                                                (("2"
                                                                                                                                                                  (expand
                                                                                                                                                                   "^"
                                                                                                                                                                   -1)
                                                                                                                                                                  (("2"
                                                                                                                                                                    (expand
                                                                                                                                                                     "min")
                                                                                                                                                                    (("2"
                                                                                                                                                                      (assert)
                                                                                                                                                                      nil
                                                                                                                                                                      nil))
                                                                                                                                                                    nil))
                                                                                                                                                                  nil))
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil)
                                                                                                                                                     ("3"
                                                                                                                                                      (replace
                                                                                                                                                       -4
                                                                                                                                                       2
                                                                                                                                                       rl)
                                                                                                                                                      (("3"
                                                                                                                                                        (replace
                                                                                                                                                         -6
                                                                                                                                                         2
                                                                                                                                                         rl)
                                                                                                                                                        (("3"
                                                                                                                                                          (expand
                                                                                                                                                           "^"
                                                                                                                                                           2)
                                                                                                                                                          (("3"
                                                                                                                                                            (expand*
                                                                                                                                                             "min"
                                                                                                                                                             "empty_seq")
                                                                                                                                                            (("3"
                                                                                                                                                              (lift-if)
                                                                                                                                                              (("3"
                                                                                                                                                                (ground)
                                                                                                                                                                nil
                                                                                                                                                                nil))
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (hide-all-but
                                                                                                                           (-1
                                                                                                                            -2
                                                                                                                            -3
                                                                                                                            -4
                                                                                                                            1))
                                                                                                                          (("2"
                                                                                                                            (replace
                                                                                                                             -1
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("2"
                                                                                                                              (replace
                                                                                                                               -2
                                                                                                                               1
                                                                                                                               rl)
                                                                                                                              (("2"
                                                                                                                                (replace
                                                                                                                                 -3
                                                                                                                                 1
                                                                                                                                 rl)
                                                                                                                                (("2"
                                                                                                                                  (replace
                                                                                                                                   -4
                                                                                                                                   1
                                                                                                                                   rl)
                                                                                                                                  (("2"
                                                                                                                                    (hide
                                                                                                                                     -)
                                                                                                                                    (("2"
                                                                                                                                      (grind)
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil)
                                                                                                                     ("3"
                                                                                                                      (replace
                                                                                                                       -1
                                                                                                                       1
                                                                                                                       rl)
                                                                                                                      (("3"
                                                                                                                        (expand
                                                                                                                         "o"
                                                                                                                         1)
                                                                                                                        (("3"
                                                                                                                          (replace
                                                                                                                           -4
                                                                                                                           1
                                                                                                                           rl)
                                                                                                                          (("3"
                                                                                                                            (expand
                                                                                                                             "^"
                                                                                                                             1)
                                                                                                                            (("3"
                                                                                                                              (expand
                                                                                                                               "min")
                                                                                                                              (("3"
                                                                                                                                (assert)
                                                                                                                                nil
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil)
                                                                                                               ("2"
                                                                                                                (replace
                                                                                                                 -1
                                                                                                                 1
                                                                                                                 rl)
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "o"
                                                                                                                   1)
                                                                                                                  (("2"
                                                                                                                    (replace
                                                                                                                     -4
                                                                                                                     1
                                                                                                                     rl)
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "^"
                                                                                                                       1)
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "min")
                                                                                                                        (("2"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil)
                                                                                                       ("2"
                                                                                                        (hide-all-but
                                                                                                         (-3
                                                                                                          -4
                                                                                                          -5
                                                                                                          -6
                                                                                                          1))
                                                                                                        (("2"
                                                                                                          (decompose-equality
                                                                                                           1)
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "^"
                                                                                                             1)
                                                                                                            (("1"
                                                                                                              (expand*
                                                                                                               "min"
                                                                                                               "empty_seq")
                                                                                                              (("1"
                                                                                                                (lift-if)
                                                                                                                (("1"
                                                                                                                  (ground)
                                                                                                                  (("1"
                                                                                                                    (replace
                                                                                                                     -2
                                                                                                                     -1
                                                                                                                     rl)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "o"
                                                                                                                       -1)
                                                                                                                      (("1"
                                                                                                                        (replace
                                                                                                                         -5
                                                                                                                         -1
                                                                                                                         rl)
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "^"
                                                                                                                           -1)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "min")
                                                                                                                            (("1"
                                                                                                                              (assert)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (replace
                                                                                                                     -2
                                                                                                                     -1
                                                                                                                     rl)
                                                                                                                    (("2"
                                                                                                                      (expand
                                                                                                                       "o"
                                                                                                                       -1)
                                                                                                                      (("2"
                                                                                                                        (replace
                                                                                                                         -5
                                                                                                                         -1
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (replace
                                                                                                                           -3
                                                                                                                           -1
                                                                                                                           rl)
                                                                                                                          (("2"
                                                                                                                            (replace
                                                                                                                             -4
                                                                                                                             -1
                                                                                                                             rl)
                                                                                                                            (("2"
                                                                                                                              (expand
                                                                                                                               "^"
                                                                                                                               -1)
                                                                                                                              (("2"
                                                                                                                                (expand*
                                                                                                                                 "min"
                                                                                                                                 "empty_seq")
                                                                                                                                (("2"
                                                                                                                                  (lift-if)
                                                                                                                                  (("2"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil)
                                                                                                           ("2"
                                                                                                            (decompose-equality
                                                                                                             1)
                                                                                                            (("2"
                                                                                                              (replace
                                                                                                               -1
                                                                                                               1
                                                                                                               rl)
                                                                                                              (("2"
                                                                                                                (typepred
                                                                                                                 "x!1")
                                                                                                                (("2"
                                                                                                                  (replace
                                                                                                                   -2
                                                                                                                   -1
                                                                                                                   rl)
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "^"
                                                                                                                     -1)
                                                                                                                    (("2"
                                                                                                                      (expand*
                                                                                                                       "min"
                                                                                                                       "empty_seq")
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "o"
                                                                                                                         -1)
                                                                                                                        (("2"
                                                                                                                          (lift-if)
                                                                                                                          (("2"
                                                                                                                            (ground)
                                                                                                                            (("1"
                                                                                                                              (replace
                                                                                                                               -4
                                                                                                                               -1
                                                                                                                               rl)
                                                                                                                              (("1"
                                                                                                                                (replace
                                                                                                                                 -5
                                                                                                                                 -1
                                                                                                                                 rl)
                                                                                                                                (("1"
                                                                                                                                  (replace
                                                                                                                                   -6
                                                                                                                                   -1
                                                                                                                                   rl)
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "^"
                                                                                                                                     -1)
                                                                                                                                    (("1"
                                                                                                                                      (expand*
                                                                                                                                       "min"
                                                                                                                                       "empty_seq")
                                                                                                                                      (("1"
                                                                                                                                        (lift-if)
                                                                                                                                        (("1"
                                                                                                                                          (ground)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil)
                                                                                                                             ("2"
                                                                                                                              (expand
                                                                                                                               "^"
                                                                                                                               3)
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "o"
                                                                                                                                 3
                                                                                                                                 (1
                                                                                                                                  2))
                                                                                                                                (("2"
                                                                                                                                  (expand
                                                                                                                                   "o"
                                                                                                                                   3)
                                                                                                                                  (("2"
                                                                                                                                    (lift-if)
                                                                                                                                    (("2"
                                                                                                                                      (ground)
                                                                                                                                      (("1"
                                                                                                                                        (replace
                                                                                                                                         -7
                                                                                                                                         1
                                                                                                                                         rl)
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "^"
                                                                                                                                           1)
                                                                                                                                          (("1"
                                                                                                                                            (propax)
                                                                                                                                            nil
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil)
                                                                                                                                       ("2"
                                                                                                                                        (grind)
                                                                                                                                        nil
                                                                                                                                        nil)
                                                                                                                                       ("3"
                                                                                                                                        (grind)
                                                                                                                                        nil
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide-all-but
                                                                                                       (-2
                                                                                                        -3
                                                                                                        -4
                                                                                                        -5
                                                                                                        -6
                                                                                                        -15
                                                                                                        -16
                                                                                                        -19
                                                                                                        1))
                                                                                                      (("2"
                                                                                                        (replace
                                                                                                         -1
                                                                                                         1
                                                                                                         rl)
                                                                                                        (("2"
                                                                                                          (replace
                                                                                                           -2
                                                                                                           1
                                                                                                           rl)
                                                                                                          (("2"
                                                                                                            (replace
                                                                                                             -3
                                                                                                             1
                                                                                                             rl)
                                                                                                            (("2"
                                                                                                              (replace
                                                                                                               -4
                                                                                                               1
                                                                                                               rl)
                                                                                                              (("2"
                                                                                                                (hide
                                                                                                                 -1
                                                                                                                 -2
                                                                                                                 -3
                                                                                                                 -4)
                                                                                                                (("2"
                                                                                                                  (grind)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("3"
                                                                                                      (hide
                                                                                                       -1
                                                                                                       -13
                                                                                                       -14
                                                                                                       -18
                                                                                                       2)
                                                                                                      (("3"
                                                                                                        (replace
                                                                                                         -1
                                                                                                         1
                                                                                                         rl)
                                                                                                        (("3"
                                                                                                          (lemma
                                                                                                           "walk_o")
                                                                                                          (("3"
                                                                                                            (inst
                                                                                                             -1
                                                                                                             "dg(G)"
                                                                                                             "woi o w1t"
                                                                                                             "w ^ (j, length(w) - 1)")
                                                                                                            (("1"
                                                                                                              (rewrite
                                                                                                               "walk?_caret")
                                                                                                              (("1"
                                                                                                                (split)
                                                                                                                (("1"
                                                                                                                  (case-replace
                                                                                                                   "w ^ (j, length(w) - 1) ^ (1, length(w ^ (j, length(w) - 1)) - 1) = wjl")
                                                                                                                  (("1"
                                                                                                                    (replace
                                                                                                                     -4
                                                                                                                     1
                                                                                                                     rl)
                                                                                                                    (("1"
                                                                                                                      (hide-all-but
                                                                                                                       1)
                                                                                                                      (("1"
                                                                                                                        (grind)
                                                                                                                        nil
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (hide-all-but
                                                                                                                     1)
                                                                                                                    (("2"
                                                                                                                      (grind)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (hide
                                                                                                                   2)
                                                                                                                  (("2"
                                                                                                                    (lemma
                                                                                                                     "walk_o")
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       -1
                                                                                                                       "dg(G)"
                                                                                                                       "woi"
                                                                                                                       "w1")
                                                                                                                      (("1"
                                                                                                                        (assert)
                                                                                                                        (("1"
                                                                                                                          (hide
                                                                                                                           2)
                                                                                                                          (("1"
                                                                                                                            (replace
                                                                                                                             -4
                                                                                                                             1
                                                                                                                             rl)
                                                                                                                            (("1"
                                                                                                                              (rewrite
                                                                                                                               "walk?_caret")
                                                                                                                              (("1"
                                                                                                                                (expand
                                                                                                                                 "^"
                                                                                                                                 1)
                                                                                                                                (("1"
                                                                                                                                  (expand
                                                                                                                                   "min")
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "from?")
                                                                                                                                    (("1"
                                                                                                                                      (assert)
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil)
                                                                                                                       ("2"
                                                                                                                        (replace
                                                                                                                         -4
                                                                                                                         1
                                                                                                                         rl)
                                                                                                                        (("2"
                                                                                                                          (expand
                                                                                                                           "^"
                                                                                                                           1)
                                                                                                                          (("2"
                                                                                                                            (expand
                                                                                                                             "min")
                                                                                                                            (("2"
                                                                                                                              (assert)
                                                                                                                              nil
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("3"
                                                                                                                  (hide
                                                                                                                   2)
                                                                                                                  (("3"
                                                                                                                    (expand
                                                                                                                     "o"
                                                                                                                     1)
                                                                                                                    (("3"
                                                                                                                      (expand
                                                                                                                       "^"
                                                                                                                       1)
                                                                                                                      (("3"
                                                                                                                        (lift-if)
                                                                                                                        (("3"
                                                                                                                          (replace
                                                                                                                           -2
                                                                                                                           1
                                                                                                                           rl)
                                                                                                                          (("3"
                                                                                                                            (expand
                                                                                                                             "^"
                                                                                                                             1
                                                                                                                             1)
                                                                                                                            (("3"
                                                                                                                              (expand*
                                                                                                                               "min"
                                                                                                                               "empty_seq")
                                                                                                                              (("3"
                                                                                                                                (case
                                                                                                                                 " length(w1) = 1")
                                                                                                                                (("1"
                                                                                                                                  (assert)
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "^"
                                                                                                                                     1)
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "empty_seq")
                                                                                                                                      (("1"
                                                                                                                                        (replace
                                                                                                                                         -5
                                                                                                                                         1
                                                                                                                                         rl)
                                                                                                                                        (("1"
                                                                                                                                          (expand
                                                                                                                                           "^"
                                                                                                                                           1)
                                                                                                                                          (("1"
                                                                                                                                            (expand
                                                                                                                                             "min")
                                                                                                                                            (("1"
                                                                                                                                              (expand
                                                                                                                                               "from?")
                                                                                                                                              (("1"
                                                                                                                                                (flatten)
                                                                                                                                                (("1"
                                                                                                                                                  (assert)
                                                                                                                                                  nil
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil)
                                                                                                                                 ("2"
                                                                                                                                  (assert)
                                                                                                                                  (("2"
                                                                                                                                    (expand
                                                                                                                                     "^"
                                                                                                                                     2)
                                                                                                                                    (("2"
                                                                                                                                      (expand
                                                                                                                                       "min")
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "from?")
                                                                                                                                        (("2"
                                                                                                                                          (flatten)
                                                                                                                                          (("2"
                                                                                                                                            (assert)
                                                                                                                                            nil
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (expand
                                                                                                               "^"
                                                                                                               1)
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "min")
                                                                                                                (("2"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("3"
                                                                                                              (expand
                                                                                                               "o"
                                                                                                               1)
                                                                                                              (("3"
                                                                                                                (replace
                                                                                                                 -4
                                                                                                                 1
                                                                                                                 rl)
                                                                                                                (("3"
                                                                                                                  (expand
                                                                                                                   "^"
                                                                                                                   1)
                                                                                                                  (("3"
                                                                                                                    (expand
                                                                                                                     "min")
                                                                                                                    (("3"
                                                                                                                      (assert)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide-all-but
                                                                                         1)
                                                                                        (("2"
                                                                                          (grind)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (replace
                                                                                 -13
                                                                                 1
                                                                                 rl)
                                                                                (("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (split)
                                                            (("1"
                                                              (replace
                                                               -1
                                                               1
                                                               rl)
                                                              (("1"
                                                                (expand
                                                                 "o"
                                                                 1)
                                                                (("1"
                                                                  (replace
                                                                   -4
                                                                   1
                                                                   rl)
                                                                  (("1"
                                                                    (expand
                                                                     "^"
                                                                     1)
                                                                    (("1"
                                                                      (expand
                                                                       "min")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide
                                                               -14
                                                               2)
                                                              (("2"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("2"
                                                                  (lemma
                                                                   "walk_o")
                                                                  (("2"
                                                                    (inst
                                                                     -1
                                                                     "dg(G)"
                                                                     "woi o w1t"
                                                                     " w ^ (j, length(w) - 1)")
                                                                    (("1"
                                                                      (rewrite
                                                                       "walk?_caret")
                                                                      (("1"
                                                                        (split)
                                                                        (("1"
                                                                          (case
                                                                           "w ^ (j, length(w) - 1) ^
                                                                                                                                                                                    (1, length(w ^ (j, length(w) - 1)) - 1) = wjl")
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (replace
                                                                             -4
                                                                             1
                                                                             rl)
                                                                            (("2"
                                                                              (hide-all-but
                                                                               1)
                                                                              (("2"
                                                                                (grind)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("3"
                                                                            (hide-all-but
                                                                             1)
                                                                            (("3"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide
                                                                           2)
                                                                          (("2"
                                                                            (lemma
                                                                             "walk_o")
                                                                            (("2"
                                                                              (inst
                                                                               -1
                                                                               "dg(G)"
                                                                               "woi"
                                                                               "w1")
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (replace
                                                                                   -4
                                                                                   1
                                                                                   rl)
                                                                                  (("1"
                                                                                    (rewrite
                                                                                     "walk?_caret")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "^"
                                                                                       1)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "min")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "from?")
                                                                                          (("1"
                                                                                            (flatten)
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (replace
                                                                                 -4
                                                                                 1
                                                                                 rl)
                                                                                (("2"
                                                                                  (expand
                                                                                   "^"
                                                                                   1)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "min")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("3"
                                                                          (hide
                                                                           2)
                                                                          (("3"
                                                                            (expand
                                                                             "^"
                                                                             1)
                                                                            (("3"
                                                                              (expand
                                                                               "o"
                                                                               1)
                                                                              (("3"
                                                                                (lift-if)
                                                                                (("3"
                                                                                  (case
                                                                                   "w1`length = 1")
                                                                                  (("1"
                                                                                    (replace
                                                                                     -3
                                                                                     1
                                                                                     rl)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "^"
                                                                                       1)
                                                                                      (("1"
                                                                                        (expand*
                                                                                         "min"
                                                                                         "empty_seq")
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -5
                                                                                             1
                                                                                             rl)
                                                                                            (("1"
                                                                                              (expand
                                                                                               "^"
                                                                                               1)
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "min")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "from?")
                                                                                                  (("1"
                                                                                                    (replace
                                                                                                     -1)
                                                                                                    (("1"
                                                                                                      (flatten)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (replace
                                                                                     -2
                                                                                     2
                                                                                     rl)
                                                                                    (("2"
                                                                                      (expand
                                                                                       "^"
                                                                                       2)
                                                                                      (("2"
                                                                                        (expand*
                                                                                         "min"
                                                                                         "empty_seq")
                                                                                        (("2"
                                                                                          (assert)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "from?")
                                                                                            (("2"
                                                                                              (propax)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       1)
                                                                      (("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (expand
                                                                       "o"
                                                                       1)
                                                                      (("3"
                                                                        (replace
                                                                         -4
                                                                         1
                                                                         rl)
                                                                        (("3"
                                                                          (expand
                                                                           "^"
                                                                           1)
                                                                          (("3"
                                                                            (expand
                                                                             "min")
                                                                            (("3"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("3"
                                                              (hide
                                                               -2
                                                               -5
                                                               -6
                                                               -7
                                                               -8
                                                               -9
                                                               -12
                                                               -16
                                                               2)
                                                              (("3"
                                                                (expand
                                                                 "from?")
                                                                (("3"
                                                                  (flatten)
                                                                  (("3"
                                                                    (split)
                                                                    (("1"
                                                                      (replace
                                                                       -1
                                                                       1
                                                                       rl)
                                                                      (("1"
                                                                        (replace
                                                                         -2
                                                                         1
                                                                         rl)
                                                                        (("1"
                                                                          (replace
                                                                           -3
                                                                           1
                                                                           rl)
                                                                          (("1"
                                                                            (hide
                                                                             -1
                                                                             -2
                                                                             -3)
                                                                            (("1"
                                                                              (expand*
                                                                               "o"
                                                                               "^"
                                                                               "min"
                                                                               "empty_seq")
                                                                              (("1"
                                                                                (lift-if)
                                                                                (("1"
                                                                                  (ground)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (replace
                                                                       -1
                                                                       1
                                                                       rl)
                                                                      (("2"
                                                                        (replace
                                                                         -2
                                                                         1
                                                                         rl)
                                                                        (("2"
                                                                          (replace
                                                                           -3
                                                                           1
                                                                           rl)
                                                                          (("2"
                                                                            (hide
                                                                             -1
                                                                             -2
                                                                             -3)
                                                                            (("2"
                                                                              (expand*
                                                                               "o"
                                                                               "^"
                                                                               "min"
                                                                               "empty_seq")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (replace -5 1 rl)
                                        (("2"
                                          (rewrite "walk?_caret")
                                          (("2"
                                            (expand "^" 1)
                                            (("2"
                                              (expand "min")
                                              (("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (split)
          (("1" (case-replace "i = 0")
            (("1" (hide 1)
              (("1" (case-replace "j = length(w) - 1")
                (("1" (assert)
                  (("1" (hide -1 -2 -5)
                    (("1" (typepred "e")
                      (("1" (lemma "walk_member_set_min")
                        (("1" (inst -1 "G" "w" "e")
                          (("1" (expand "walk_from?")
                            (("1" (assert)
                              (("1"
                                (expand "from?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (replace -3)
                                    (("1"
                                      (replace -4)
                                      (("1"
                                        (case "e = (e`1, e`2)")
                                        (("1"
                                          (replace -1 1 rl)
                                          (("1" (propax) nil nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (typepred "e")
                    (("2" (lemma "walk_member_set_min")
                      (("2" (inst -1 "G" "w" "e")
                        (("2" (expand "walk_from?")
                          (("2" (assert)
                            (("2" (hide -2)
                              (("2"
                                (expand* "nonempty?" "empty?" "member")
                                (("2"
                                  (name "ww" "w^(0,j)")
                                  (("2"
                                    (name-replace
                                     "w0"
                                     "w`seq(0)"
                                     :hide?
                                     nil)
                                    (("2"
                                      (name-replace
                                       "wj"
                                       "w`seq(j)"
                                       :hide?
                                       nil)
                                      (("2"
                                        (inst -9 "ww")
                                        (("1"
                                          (expand "set_min")
                                          (("1"
                                            (split)
                                            (("1"
                                              (hide-all-but
                                               (-1 -2 -3 1))
                                              (("1"
                                                (replace -1 1 rl)
                                                (("1"
                                                  (replace -2 1 rl)
                                                  (("1"
                                                    (replace -3 1 rl)
                                                    (("1"
                                                      (hide -)
                                                      (("1"
                                                        (expand
                                                         "from?")
                                                        (("1"
                                                          (expand*
                                                           "^"
                                                           "min")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "min_walk?")
                                              (("2"
                                                (skeep)
                                                (("2"
                                                  (typepred "w1")
                                                  (("2"
                                                    (name
                                                     "woj"
                                                     "w ^ (0, j)")
                                                    (("2"
                                                      (name
                                                       "wjl"
                                                       "w ^ (j + 1, length(w) - 1)")
                                                      (("2"
                                                        (name
                                                         "w1w"
                                                         "w1 o wjl")
                                                        (("2"
                                                          (inst
                                                           -10
                                                           "w1w")
                                                          (("1"
                                                            (lemma
                                                             "wgt_walk_decomposed")
                                                            (("1"
                                                              (inst-cp
                                                               -1
                                                               "G"
                                                               "j"
                                                               "w")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (replace
                                                                   -2
                                                                   -12)
                                                                  (("1"
                                                                    (hide
                                                                     -2)
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "G"
                                                                       "length(w1) - 1"
                                                                       "w1w")
                                                                      (("1"
                                                                        (split
                                                                         -1)
                                                                        (("1"
                                                                          (case
                                                                           "w1w ^ (0, length(w1) - 1) = w1")
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            (("1"
                                                                              (replaces
                                                                               -1)
                                                                              (("1"
                                                                                (case
                                                                                 "w1w ^ (length(w1) - 1, length(w1w) - 1) = w ^ (j, length(w) - 1)")
                                                                                (("1"
                                                                                  (replaces
                                                                                   -1)
                                                                                  (("1"
                                                                                    (replace
                                                                                     -9)
                                                                                    (("1"
                                                                                      (hide
                                                                                       -1)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (hide-all-but
                                                                                           (-9
                                                                                            1))
                                                                                          (("1"
                                                                                            (name-replace
                                                                                             "aa"
                                                                                             "wgt_walk(G, w ^ (j, length(w) - 1))")
                                                                                            (("1"
                                                                                              (name-replace
                                                                                               "cc"
                                                                                               "wgt_walk(G, ww)")
                                                                                              (("1"
                                                                                                (name-replace
                                                                                                 "dd"
                                                                                                 "wgt_walk(G, w1)")
                                                                                                (("1"
                                                                                                  (typepred
                                                                                                   "+"
                                                                                                   "<=")
                                                                                                  (("1"
                                                                                                    (copy
                                                                                                     -1)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "commutative?")
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         -1
                                                                                                         "cc"
                                                                                                         "aa")
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           -2
                                                                                                           "dd"
                                                                                                           "aa")
                                                                                                          (("1"
                                                                                                            (replaces
                                                                                                             -1)
                                                                                                            (("1"
                                                                                                              (replaces
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (hide
                                                                                                                 -1
                                                                                                                 -2)
                                                                                                                (("1"
                                                                                                                  (inst
                                                                                                                   -1
                                                                                                                   "aa"
                                                                                                                   "cc"
                                                                                                                   "dd")
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    nil
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide
                                                                                   -5
                                                                                   -10
                                                                                   -13
                                                                                   2)
                                                                                  (("2"
                                                                                    (replace
                                                                                     -1
                                                                                     1
                                                                                     rl)
                                                                                    (("2"
                                                                                      (replace
                                                                                       -2
                                                                                       1
                                                                                       rl)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1
                                                                                         -2
                                                                                         -3
                                                                                         -8
                                                                                         -9)
                                                                                        (("2"
                                                                                          (decompose-equality
                                                                                           1)
                                                                                          (("1"
                                                                                            (expand*
                                                                                             "o"
                                                                                             "^"
                                                                                             "min"
                                                                                             "empty_seq")
                                                                                            nil
                                                                                            nil)
                                                                                           ("2"
                                                                                            (decompose-equality)
                                                                                            (("1"
                                                                                              (expand*
                                                                                               "o"
                                                                                               "^"
                                                                                               "min"
                                                                                               "empty_seq")
                                                                                              (("1"
                                                                                                (lift-if)
                                                                                                (("1"
                                                                                                  (ground)
                                                                                                  (("1"
                                                                                                    (case-replace
                                                                                                     "x!1 = 0")
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "from?")
                                                                                                      (("1"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (expand*
                                                                                               "o"
                                                                                               "^"
                                                                                               "min"
                                                                                               "empty_seq")
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("3"
                                                                                            (expand*
                                                                                             "o"
                                                                                             "^"
                                                                                             "min"
                                                                                             "empty_seq")
                                                                                            (("3"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("3"
                                                                                  (replace
                                                                                   -1
                                                                                   1
                                                                                   rl)
                                                                                  (("3"
                                                                                    (expand
                                                                                     "o"
                                                                                     1)
                                                                                    (("3"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide
                                                                             -1
                                                                             -6
                                                                             -11
                                                                             -14
                                                                             2)
                                                                            (("2"
                                                                              (replace
                                                                               -1
                                                                               1
                                                                               rl)
                                                                              (("2"
                                                                                (replace
                                                                                 -2
                                                                                 1
                                                                                 rl)
                                                                                (("2"
                                                                                  (hide
                                                                                   -1
                                                                                   -2
                                                                                   -3
                                                                                   -8)
                                                                                  (("2"
                                                                                    (decompose-equality)
                                                                                    (("1"
                                                                                      (expand*
                                                                                       "o"
                                                                                       "^"
                                                                                       "min"
                                                                                       "empty_seq")
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (decompose-equality)
                                                                                      (("2"
                                                                                        (expand*
                                                                                         "o"
                                                                                         "^"
                                                                                         "min"
                                                                                         "empty_seq")
                                                                                        (("2"
                                                                                          (lift-if)
                                                                                          (("2"
                                                                                            (ground)
                                                                                            (("2"
                                                                                              (typepred
                                                                                               "x!1")
                                                                                              (("2"
                                                                                                (expand*
                                                                                                 "o"
                                                                                                 "^"
                                                                                                 "min"
                                                                                                 "empty_seq")
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           (-1
                                                                            -2
                                                                            -14
                                                                            1
                                                                            3))
                                                                          (("2"
                                                                            (replace
                                                                             -1
                                                                             1
                                                                             rl)
                                                                            (("2"
                                                                              (expand
                                                                               "o"
                                                                               1)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("3"
                                                                          (hide
                                                                           -3
                                                                           -9
                                                                           -10
                                                                           -11
                                                                           -13
                                                                           2)
                                                                          (("3"
                                                                            (replace
                                                                             -1
                                                                             1
                                                                             rl)
                                                                            (("3"
                                                                              (replace
                                                                               -2
                                                                               1
                                                                               rl)
                                                                              (("3"
                                                                                (hide
                                                                                 -1
                                                                                 -2)
                                                                                (("3"
                                                                                  (lemma
                                                                                   "walk_o")
                                                                                  (("3"
                                                                                    (inst
                                                                                     -1
                                                                                     "dg(G)"
                                                                                     "w1"
                                                                                     "w ^ (j, length(w) - 1)")
                                                                                    (("1"
                                                                                      (rewrite
                                                                                       "walk?_caret")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (split)
                                                                                          (("1"
                                                                                            (case
                                                                                             "w ^ (j, length(w) - 1) ^
                                                                                                                                                     (1, length(w ^ (j, length(w) - 1)) - 1) = w ^ (1 + j, length(w) - 1)")
                                                                                            (("1"
                                                                                              (replaces
                                                                                               -1)
                                                                                              nil
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide-all-but
                                                                                               1)
                                                                                              (("2"
                                                                                                (grind)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("3"
                                                                                              (hide-all-but
                                                                                               1)
                                                                                              (("3"
                                                                                                (grind)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide
                                                                                             -2
                                                                                             2)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "^")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "from?")
                                                                                                (("2"
                                                                                                  (flatten)
                                                                                                  (("2"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (hide-all-but
                                                                                       1)
                                                                                      (("2"
                                                                                        (grind)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide
                                                             -12
                                                             2)
                                                            (("2"
                                                              (split)
                                                              (("1"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("1"
                                                                  (expand
                                                                   "o"
                                                                   1)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("2"
                                                                  (replace
                                                                   -2
                                                                   1
                                                                   rl)
                                                                  (("2"
                                                                    (hide
                                                                     -1
                                                                     -2
                                                                     -3
                                                                     -9
                                                                     -10)
                                                                    (("2"
                                                                      (lemma
                                                                       "walk_o")
                                                                      (("2"
                                                                        (inst
                                                                         -1
                                                                         "dg(G)"
                                                                         "w1"
                                                                         "w ^ (j, length(w) - 1)")
                                                                        (("1"
                                                                          (rewrite
                                                                           "walk?_caret")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (split)
                                                                              (("1"
                                                                                (case
                                                                                 "w ^ (j, length(w) - 1) ^
                                                                                                                                                     (1, length(w ^ (j, length(w) - 1)) - 1) = w ^ (1 + j, length(w) - 1)")
                                                                                (("1"
                                                                                  (replaces
                                                                                   -1)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("2"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil)
                                                                                 ("3"
                                                                                  (hide-all-but
                                                                                   1)
                                                                                  (("3"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (hide
                                                                                 -2
                                                                                 2)
                                                                                (("2"
                                                                                  (expand
                                                                                   "^")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "from?")
                                                                                    (("2"
                                                                                      (flatten)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           1)
                                                                          (("2"
                                                                            (grind)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("3"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("3"
                                                                  (replace
                                                                   -2
                                                                   1
                                                                   rl)
                                                                  (("3"
                                                                    (hide
                                                                     -1
                                                                     -2
                                                                     -3
                                                                     -5
                                                                     -9)
                                                                    (("3"
                                                                      (expand
                                                                       "from?")
                                                                      (("3"
                                                                        (flatten)
                                                                        (("3"
                                                                          (split)
                                                                          (("1"
                                                                            (expand*
                                                                             "o"
                                                                             "^")
                                                                            (("1"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (expand*
                                                                             "o"
                                                                             "^"
                                                                             "min"
                                                                             "empty_seq")
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (replace -3 1 rl)
                                          (("2"
                                            (rewrite "walk?_caret")
                                            (("2"
                                              (expand "^" 1)
                                              (("2"
                                                (expand "min")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil)
           ("2" (case-replace "j = length(w) - 1")
            (("1" (hide 1)
              (("1" (case-replace "i = 0")
                (("1" (assert)
                  (("1" (hide -1 -2 -5)
                    (("1" (typepred "e")
                      (("1" (lemma "walk_member_set_min")
                        (("1" (inst -1 "G" "w" "e")
                          (("1" (expand "walk_from?")
                            (("1" (assert)
                              (("1"
                                (expand "from?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (replace -3)
                                    (("1"
                                      (replace -4)
                                      (("1"
                                        (case "e = (e`1, e`2)")
                                        (("1"
                                          (replace -1 1 rl)
                                          (("1" (propax) nil nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (typepred "e")
                    (("2" (lemma "walk_member_set_min")
                      (("2" (inst -1 "G" "w" "e")
                        (("2" (expand "walk_from?")
                          (("2" (assert)
                            (("2" (hide -2)
                              (("2"
                                (expand* "nonempty?" "empty?" "member")
                                (("2"
                                  (name-replace
                                   "wi"
                                   "w`seq(i)"
                                   :hide?
                                   nil)
                                  (("2"
                                    (name-replace
                                     "wj"
                                     "w`seq(length(w) - 1)"
                                     :hide?
                                     nil)
                                    (("2"
                                      (name "ww" "w^(i,length(w) - 1)")
                                      (("2"
                                        (inst -9 "ww")
                                        (("1"
                                          (expand "set_min")
                                          (("1"
                                            (split)
                                            (("1"
                                              (hide-all-but
                                               (-1 -2 -3 1))
                                              (("1"
                                                (replace -1 1 rl)
                                                (("1"
                                                  (replace -2 1 rl)
                                                  (("1"
                                                    (replace -3 1 rl)
                                                    (("1"
                                                      (hide -)
                                                      (("1"
                                                        (expand
                                                         "from?")
                                                        (("1"
                                                          (expand*
                                                           "^"
                                                           "min")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "min_walk?")
                                              (("2"
                                                (skeep)
                                                (("2"
                                                  (typepred "w1")
                                                  (("2"
                                                    (name
                                                     "woi"
                                                     "w ^ (0, i)")
                                                    (("2"
                                                      (name
                                                       "w1t"
                                                       "w1 ^ (1, length(w1) - 1)")
                                                      (("2"
                                                        (name
                                                         "ww1"
                                                         "woi o w1t")
                                                        (("2"
                                                          (inst
                                                           -10
                                                           "ww1")
                                                          (("1"
                                                            (lemma
                                                             "wgt_walk_decomposed")
                                                            (("1"
                                                              (inst-cp
                                                               -1
                                                               "G"
                                                               "i"
                                                               "w")
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (replace
                                                                   -2
                                                                   -12)
                                                                  (("1"
                                                                    (hide
                                                                     -2)
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "G"
                                                                       "i"
                                                                       "ww1")
                                                                      (("1"
                                                                        (split
                                                                         -1)
                                                                        (("1"
                                                                          (case
                                                                           "ww1 ^ (0, i) = woi")
                                                                          (("1"
                                                                            (replaces
                                                                             -1)
                                                                            (("1"
                                                                              (replaces
                                                                               -1)
                                                                              (("1"
                                                                                (replace
                                                                                 -3)
                                                                                (("1"
                                                                                  (case
                                                                                   "ww1 ^ (i, length(ww1) - 1) = w1")
                                                                                  (("1"
                                                                                    (replaces
                                                                                     -1)
                                                                                    (("1"
                                                                                      (replace
                                                                                       -7)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (hide-all-but
                                                                                           (-10
                                                                                            1))
                                                                                          (("1"
                                                                                            (name-replace
                                                                                             "aa"
                                                                                             "wgt_walk(G, woi)")
                                                                                            (("1"
                                                                                              (name-replace
                                                                                               "bb"
                                                                                               "wgt_walk(G, w1)")
                                                                                              (("1"
                                                                                                (name-replace
                                                                                                 "cc"
                                                                                                 "wgt_walk(G, ww)")
                                                                                                (("1"
                                                                                                  (typepred
                                                                                                   "<=")
                                                                                                  (("1"
                                                                                                    (hide
                                                                                                     -1)
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       -1
                                                                                                       "aa"
                                                                                                       "cc"
                                                                                                       "bb")
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (hide
                                                                                     -5
                                                                                     -10
                                                                                     -13
                                                                                     2)
                                                                                    (("2"
                                                                                      (replace
                                                                                       -1
                                                                                       1
                                                                                       rl)
                                                                                      (("2"
                                                                                        (replace
                                                                                         -2
                                                                                         1
                                                                                         rl)
                                                                                        (("2"
                                                                                          (replace
                                                                                           -3
                                                                                           1
                                                                                           rl)
                                                                                          (("2"
                                                                                            (hide
                                                                                             -1
                                                                                             -2
                                                                                             -3
                                                                                             -6)
                                                                                            (("2"
                                                                                              (decompose-equality)
                                                                                              (("1"
                                                                                                (expand*
                                                                                                 "o"
                                                                                                 "^"
                                                                                                 "min"
                                                                                                 "empty_seq")
                                                                                                (("1"
                                                                                                  (lift-if)
                                                                                                  (("1"
                                                                                                    (lift-if)
                                                                                                    (("1"
                                                                                                      (lift-if)
                                                                                                      (("1"
                                                                                                        (ground)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (decompose-equality)
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "x!1 = 0")
                                                                                                  (("1"
                                                                                                    (case-replace
                                                                                                     "length(w1) = 1")
                                                                                                    (("1"
                                                                                                      (expand*
                                                                                                       "o"
                                                                                                       "^"
                                                                                                       "min"
                                                                                                       "empty_seq")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "from?")
                                                                                                        (("1"
                                                                                                          (flatten)
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (expand*
                                                                                                       "o"
                                                                                                       "^"
                                                                                                       "min"
                                                                                                       "empty_seq")
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "from?")
                                                                                                          (("2"
                                                                                                            (propax)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (case-replace
                                                                                                     "length(w1) = 1")
                                                                                                    (("1"
                                                                                                      (typepred
                                                                                                       "x!1")
                                                                                                      (("1"
                                                                                                        (hide
                                                                                                         2)
                                                                                                        (("1"
                                                                                                          (expand*
                                                                                                           "o"
                                                                                                           "^"
                                                                                                           "min"
                                                                                                           "empty_seq")
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (expand*
                                                                                                       "o"
                                                                                                       "^"
                                                                                                       "min"
                                                                                                       "empty_seq")
                                                                                                      (("2"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (expand*
                                                                                                   "o"
                                                                                                   "^"
                                                                                                   "min"
                                                                                                   "empty_seq")
                                                                                                  (("2"
                                                                                                    (lift-if)
                                                                                                    (("2"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("3"
                                                                                                (expand*
                                                                                                 "o"
                                                                                                 "^"
                                                                                                 "min"
                                                                                                 "empty_seq")
                                                                                                (("3"
                                                                                                  (lift-if)
                                                                                                  (("3"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("3"
                                                                                    (replace
                                                                                     -1
                                                                                     1
                                                                                     rl)
                                                                                    (("3"
                                                                                      (expand
                                                                                       "o"
                                                                                       1)
                                                                                      (("3"
                                                                                        (replace
                                                                                         -3
                                                                                         1
                                                                                         rl)
                                                                                        (("3"
                                                                                          (expand
                                                                                           "^"
                                                                                           1)
                                                                                          (("3"
                                                                                            (expand
                                                                                             "min")
                                                                                            (("3"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide-all-but
                                                                             (-2
                                                                              -3
                                                                              -4
                                                                              -5
                                                                              -7
                                                                              -9
                                                                              -10
                                                                              -13
                                                                              -15
                                                                              1
                                                                              3))
                                                                            (("2"
                                                                              (replace
                                                                               -1
                                                                               1
                                                                               rl)
                                                                              (("2"
                                                                                (replace
                                                                                 -2
                                                                                 1
                                                                                 rl)
                                                                                (("2"
                                                                                  (replace
                                                                                   -3
                                                                                   1
                                                                                   rl)
                                                                                  (("2"
                                                                                    (hide
                                                                                     -1
                                                                                     -2
                                                                                     -3)
                                                                                    (("2"
                                                                                      (decompose-equality)
                                                                                      (("1"
                                                                                        (grind)
                                                                                        nil
                                                                                        nil)
                                                                                       ("2"
                                                                                        (decompose-equality)
                                                                                        (("2"
                                                                                          (typepred
                                                                                           "x!1")
                                                                                          (("2"
                                                                                            (case-replace
                                                                                             "length(w1) = 1")
                                                                                            (("1"
                                                                                              (expand*
                                                                                               "o"
                                                                                               "^"
                                                                                               "min"
                                                                                               "empty_seq")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (expand*
                                                                                               "o"
                                                                                               "^"
                                                                                               "min"
                                                                                               "empty_seq")
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           (-1
                                                                            -3
                                                                            -14
                                                                            1
                                                                            3))
                                                                          (("2"
                                                                            (replace
                                                                             -1
                                                                             1
                                                                             rl)
                                                                            (("2"
                                                                              (replace
                                                                               -2
                                                                               1
                                                                               rl)
                                                                              (("2"
                                                                                (hide
                                                                                 -1
                                                                                 -2)
                                                                                (("2"
                                                                                  (expand*
                                                                                   "o"
                                                                                   "^"
                                                                                   "min"
                                                                                   "empty_seq")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("3"
                                                                          (hide
                                                                           -7
                                                                           -10
                                                                           -13
                                                                           2)
                                                                          (("3"
                                                                            (replace
                                                                             -1
                                                                             1
                                                                             rl)
                                                                            (("3"
                                                                              (hide
                                                                               -1)
                                                                              (("3"
                                                                                (replace
                                                                                 -1
                                                                                 1
                                                                                 rl)
                                                                                (("3"
                                                                                  (hide
                                                                                   -1)
                                                                                  (("3"
                                                                                    (lemma
                                                                                     "walk_o")
                                                                                    (("3"
                                                                                      (inst
                                                                                       -1
                                                                                       "dg(G)"
                                                                                       "woi"
                                                                                       "w1")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (hide
                                                                                           2)
                                                                                          (("1"
                                                                                            (replace
                                                                                             -1
                                                                                             1
                                                                                             rl)
                                                                                            (("1"
                                                                                              (rewrite
                                                                                               "walk?_caret")
                                                                                              (("1"
                                                                                                (hide
                                                                                                 -1)
                                                                                                (("1"
                                                                                                  (expand*
                                                                                                   "^"
                                                                                                   "min")
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "from?")
                                                                                                    (("1"
                                                                                                      (flatten)
                                                                                                      (("1"
                                                                                                        (assert)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (replace
                                                                                         -1
                                                                                         1
                                                                                         rl)
                                                                                        (("2"
                                                                                          (hide-all-but
                                                                                           (-9
                                                                                            1
                                                                                            3))
                                                                                          (("2"
                                                                                            (expand*
                                                                                             "^"
                                                                                             "min")
                                                                                            (("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (split)
                                                            (("1"
                                                              (hide-all-but
                                                               (-1
                                                                -3
                                                                -13
                                                                1
                                                                3))
                                                              (("1"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("1"
                                                                  (replace
                                                                   -2
                                                                   1
                                                                   rl)
                                                                  (("1"
                                                                    (hide
                                                                     -1
                                                                     -2)
                                                                    (("1"
                                                                      (expand*
                                                                       "o"
                                                                       "^"
                                                                       "min")
                                                                      (("1"
                                                                        (assert)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (hide
                                                               -7
                                                               -12
                                                               2)
                                                              (("2"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("2"
                                                                  (replace
                                                                   -2
                                                                   1
                                                                   rl)
                                                                  (("2"
                                                                    (hide
                                                                     -1
                                                                     -2)
                                                                    (("2"
                                                                      (lemma
                                                                       "walk_o")
                                                                      (("2"
                                                                        (inst
                                                                         -1
                                                                         "dg(G)"
                                                                         "woi"
                                                                         "w1")
                                                                        (("1"
                                                                          (assert)
                                                                          (("1"
                                                                            (hide
                                                                             2)
                                                                            (("1"
                                                                              (replace
                                                                               -1
                                                                               1
                                                                               rl)
                                                                              (("1"
                                                                                (rewrite
                                                                                 "walk?_caret")
                                                                                (("1"
                                                                                  (hide
                                                                                   -1)
                                                                                  (("1"
                                                                                    (expand*
                                                                                     "^"
                                                                                     "min")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "from?")
                                                                                      (("1"
                                                                                        (flatten)
                                                                                        (("1"
                                                                                          (assert)
                                                                                          nil
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (replace
                                                                           -1
                                                                           1
                                                                           rl)
                                                                          (("2"
                                                                            (hide-all-but
                                                                             (1
                                                                              3))
                                                                            (("2"
                                                                              (expand*
                                                                               "^"
                                                                               "min")
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("3"
                                                              (hide
                                                               -4
                                                               -7
                                                               -10
                                                               -12
                                                               2)
                                                              (("3"
                                                                (replace
                                                                 -1
                                                                 1
                                                                 rl)
                                                                (("3"
                                                                  (replace
                                                                   -2
                                                                   1
                                                                   rl)
                                                                  (("3"
                                                                    (replace
                                                                     -3
                                                                     1
                                                                     rl)
                                                                    (("3"
                                                                      (hide
                                                                       -1
                                                                       -2
                                                                       -3)
                                                                      (("3"
                                                                        (expand
                                                                         "from?")
                                                                        (("3"
                                                                          (flatten)
                                                                          (("3"
                                                                            (split)
                                                                            (("1"
                                                                              (expand*
                                                                               "o"
                                                                               "^"
                                                                               "min")
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (case-replace
                                                                               "length(w1) = 1")
                                                                              (("1"
                                                                                (expand*
                                                                                 "o"
                                                                                 "^"
                                                                                 "min"
                                                                                 "empty_seq")
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (expand*
                                                                                 "o"
                                                                                 "^"
                                                                                 "min"
                                                                                 "empty_seq")
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (replace -1 1 rl)
                                          (("2"
                                            (rewrite "walk?_caret")
                                            (("2"
                                              (hide -)
                                              (("2"
                                                (expand* "^" "min")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                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))
    nil)
   ((w1w skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (w0 skolem-const-decl "T" wgt_digraphs_props nil)
    (wj skolem-const-decl "T" wgt_digraphs_props nil)
    (w1 skolem-const-decl "{w1: Walk(dg(G)) | from?(w1, w0, wj)}"
     wgt_digraphs_props nil)
    (ww skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (ww1 skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (woi skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (i skolem-const-decl "below(length(w))" wgt_digraphs_props nil)
    (wi skolem-const-decl "T" wgt_digraphs_props nil)
    (wj skolem-const-decl "T" wgt_digraphs_props nil)
    (w1 skolem-const-decl "{w1: Walk(dg(G)) | from?(w1, wi, wj)}"
     wgt_digraphs_props nil)
    (ww skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (ww skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (G skolem-const-decl "wdg[T, Weight, +, 0]" wgt_digraphs_props nil)
    (from? const-decl "bool" walks nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (w1w skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (e skolem-const-decl "{e: edgetype | nonempty?(set_min(G)(e))}"
     wgt_digraphs_props nil)
    (w1t skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (woi skolem-const-decl "finseq[T]" wgt_digraphs_props nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (walk_o formula-decl nil walks nil)
    (j skolem-const-decl "below(length(w))" wgt_digraphs_props nil)
    (w skolem-const-decl "Walk[T](dg(G))" wgt_digraphs_props nil)
    (wgt_aux def-decl "Weight" weighted_digraphs nil)
    (min_wgt const-decl "Weight" wgt_digraphs_props nil)
    (<= formal-const-decl "{<=: (partial_order?[Weight]) |
         FORALL (a, b, c: Weight): a + b <= a + c => b <= c}"
        wgt_digraphs_props nil)
    (partial_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (wgt_walk const-decl "Weight" weighted_digraphs nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nat_min application-judgement "{k: nat | k <= i AND k <= j}"
     real_defs nil)
    (empty_seq const-decl "finseq" finite_sequences nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (walk?_caret formula-decl nil walks nil)
    (wgt_walk_decomposed formula-decl nil weighted_digraphs nil)
    (O const-decl "finseq" finite_sequences nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (min_walk? const-decl "bool" wgt_digraphs_props nil)
    (^ const-decl "finseq" finite_sequences nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (walk_from? const-decl "bool" walks nil)
    (walk_member_set_min formula-decl nil wgt_digraphs_props nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND 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)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil wgt_digraphs_props nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (> 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)
    (digraph type-eq-decl nil digraphs nil)
    (walk? const-decl "bool" walks nil)
    (edge type-eq-decl nil digraphs nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (commutative? const-decl "bool" operator_defs nil)
    (associative? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (Walk type-eq-decl nil walks nil)
    (below type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil))
 (sub_min_walk_is_min_TCC1 0
  (sub_min_walk_is_min_TCC1-1 nil 3562952609
   ("" (skeep)
    (("" (rewrite "walk?_caret")
      (("" (expand* "^" "min") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((walk?_caret formula-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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (edge type-eq-decl nil digraphs nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (commutative? const-decl "bool" operator_defs nil)
    (associative? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (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)
    (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)
    (finseq type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (below type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil wgt_digraphs_props 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)
    (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)
    (^ 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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (sub_min_walk_is_min_TCC2 0
  (sub_min_walk_is_min_TCC2-1 nil 3562952609
   ("" (skeep)
    (("" (lemma "sub_min_walk_nonempty")
      (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((sub_min_walk_nonempty formula-decl nil wgt_digraphs_props nil)
    (set_min const-decl "set[Walk(dg(G))]" wgt_digraphs_props nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (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)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (wdg type-eq-decl nil weighted_digraphs nil)
    (0 formal-const-decl "{zero: Weight | identity?(+)(zero)}"
     wgt_digraphs_props nil)
    (identity? const-decl "bool" operator_defs nil)
    (+ formal-const-decl
       "{f: [[Weight, Weight] -> Weight] | commutative?(f) AND associative?(f)}"
       wgt_digraphs_props nil)
    (associative? const-decl "bool" operator_defs nil)
    (commutative? const-decl "bool" operator_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Weight formal-type-decl nil wgt_digraphs_props nil)
    (edge type-eq-decl nil digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (T formal-type-decl nil wgt_digraphs_props nil))
   nil))
 (sub_min_walk_is_min 0
  (sub_min_walk_is_min-2 nil 3567171943
   ("" (auto-rewrite "finseq_appl")
    (("" (skeep)
      (("" (case "0 < i AND j < length(w) - 1")
        (("1" (flatten)
          (("1" (assert)
            (("1" (typepred "e")
              (("1" (lemma "walk_member_set_min")
                (("1" (inst -1 "G" "w" "e")
                  (("1" (expand "walk_from?")
                    (("1" (assert)
                      (("1" (hide -2)
                        (("1" (rewrite "min_walk_min_wgt")
                          (("1" (hide 2)
                            (("1" (expand "member")
                              (("1"
                                (name-replace
                                 "ww"
                                 "w^(i,j)"
                                 :hide?
                                 nil)
                                (("1"
                                  (name-replace "e1" "e`1" :hide? nil)
                                  (("1"
                                    (name-replace
                                     "e2"
                                     "e`2"
                                     :hide?
                                     nil)
                                    (("1"
                                      (name-replace
                                       "wi"
                                       "w`seq(i)"
                                       :hide?
                                       nil)
                                      (("1"
                                        (name-replace
                                         "wj"
                                         "w`seq(j)"
                                         :hide?
                                         nil)
                                        (("1"
                                          (expand "set_min")
                                          (("1"
                                            (split)
                                            (("1"
                                              (replace -5 1 rl)
                                              (("1"
                                                (replace -1 1 rl)
                                                (("1"
                                                  (replace -2 1 rl)
                                                  (("1"
                                                    (hide-all-but 1)
                                                    (("1"
                                                      (expand "from?")
                                                      (("1"
                                                        (expand*
                                                         "^"
                                                         "min")
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "min_walk?")
                                              (("2"
                                                (skeep)
                                                (("2"
                                                  (typepred "w1")
                                                  (("2"
                                                    (name
                                                     "woi"
                                                     "w ^ (0, i)")
                                                    (("2"
                                                      (name
                                                       "wjl"
                                                       "w ^ (j + 1, length(w) - 1)")
                                                      (("2"
                                                        (name
                                                         "w1t"
                                                         "w1 ^ (1, length(w1) - 1)")
                                                        (("2"
                                                          (name
                                                           "w1w"
                                                           "woi o w1t o wjl")
                                                          (("2"
                                                            (inst
                                                             -13
                                                             "w1w")
                                                            (("1"
                                                              (lemma
                                                               "wgt_walk_decomposed")
                                                              (("1"
                                                                (inst-cp
                                                                 -1
                                                                 "G"
                                                                 "i"
                                                                 "w")
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (replace
                                                                     -2
                                                                     -15)
                                                                    (("1"
                                                                      (hide
                                                                       -2)
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         "G"
                                                                         "j - i"
                                                                         "w ^ (i, length(w) - 1)")
                                                                        (("1"
                                                                          (expand
                                                                           "^"
                                                                           -1
                                                                           1)
                                                                          (("1"
                                                                            (expand
                                                                             "min")
                                                                            (("1"
                                                                              (rewrite
                                                                               "walk?_caret")
                                                                              (("1"
                                                                                (case
                                                                                 "w ^ (i, length(w) - 1) ^ (0, j - i) = ww")
                                                                                (("1"
                                                                                  (replace
                                                                                   -1
                                                                                   -2)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "^"
                                                                                     -2
                                                                                     4)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "min")
                                                                                      (("1"
                                                                                        (case
                                                                                         "w ^ (i, length(w) - 1) ^ (j - i, w`length - 1 - i) = w^(j, length(w) - 1)")
                                                                                        (("1"
                                                                                          (replace
                                                                                           -1
                                                                                           -3)
                                                                                          (("1"
                                                                                            (hide
                                                                                             -1
                                                                                             -2)
                                                                                            (("1"
                                                                                              (replace
                                                                                               -1
                                                                                               -14)
                                                                                              (("1"
                                                                                                (hide
                                                                                                 -1)
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "wgt_walk_decomposed")
                                                                                                  (("1"
                                                                                                    (inst-cp
                                                                                                     -1
                                                                                                     "G"
                                                                                                     "i"
                                                                                                     "w1w")
                                                                                                    (("1"
                                                                                                      (split
                                                                                                       -2)
                                                                                                      (("1"
                                                                                                        (case
                                                                                                         "w1w ^ (0, i) = w^(0, i)")
                                                                                                        (("1"
                                                                                                          (replaces
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (replace
                                                                                                             -1
                                                                                                             -15)
                                                                                                            (("1"
                                                                                                              (hide
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (inst
                                                                                                                 -1
                                                                                                                 "G"
                                                                                                                 "length(w1) - 1"
                                                                                                                 "w1w ^ (i, length(w1w) - 1)")
                                                                                                                (("1"
                                                                                                                  (split
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (case
                                                                                                                     "w1w ^ (i, length(w1w) - 1) ^ (0, length(w1) - 1) = w1")
                                                                                                                    (("1"
                                                                                                                      (replaces
                                                                                                                       -1)
                                                                                                                      (("1"
                                                                                                                        (case
--> --------------------

--> maximum size reached

--> --------------------