Quelle  graph_path_conn.prf

(graph_path_conn
 (isolated_not_path 0
  (isolated_not_path-1 nil 3263033576
   ("" (skosimp*)
    (("" (expand "path_connected?")
      (("" (flatten)
        (("" (expand "isolated?")
          (("" (expand "empty?" -1)
            (("" (expand "member")
              (("" (lemma "not_singleton_2_vert")
                (("" (inst?)
                  (("" (assert)
                    (("" (skosimp*)
                      (("" (inst -4 "x!1" "y!1")
                        (("" (assert)
                          (("" (skosimp*)
                            (("" (typepred "w!1")
                              ((""
                                (expand "walk?")
                                ((""
                                  (flatten)
                                  ((""
                                    (inst - "0")
                                    ((""
                                      (assert)
                                      ((""
                                        (expand "finseq_appl")
                                        ((""
                                          (assert)
                                          ((""
                                            (expand "edge?")
                                            ((""
                                              (flatten)
                                              ((""
                                                (inst
                                                 -6
                                                 "dbl[T](seq(w!1)(0), seq(w!1)(1))")
                                                ((""
                                                  (inst?)
                                                  ((""
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((path_connected? const-decl "bool" graph_conn_defs nil)
    (isolated? const-decl "bool" graphs nil)
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (prewalk type-eq-decl nil walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (edge? const-decl "bool" graphs nil)
    (nil application-judgement "finite_set[T]" graph_path_conn nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     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)
    (y!1 skolem-const-decl "T" graph_path_conn nil)
    (x!1 skolem-const-decl "T" graph_path_conn nil)
    (G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
    (T formal-type-decl nil graph_path_conn nil)
    (not_singleton_2_vert formula-decl nil graphs nil)
    (empty? const-decl "bool" sets nil))
   nil))
 (pic_A 0
  (pic_A-1 nil 3263033576
   ("" (skosimp*)
    (("" (case "NOT singleton?(G!1)")
      (("1" (expand "singleton?")
        (("1" (expand "size")
          (("1" (case "NOT empty?(G!1)")
            (("1" (expand "empty?")
              (("1" (lemma "card_empty?[T]")
                (("1" (inst?)
                  (("1" (iff)
                    (("1" (assert)
                      (("1" (hide 2)
                        (("1"
                          (case "(EXISTS (y: T): vert(G!1)(y) AND y /= v!1)")
                          (("1" (skosimp*)
                            (("1" (hide 2 3 4)
                              (("1"
                                (expand "path_connected?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (inst -4 "v!1" "y!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (typepred "w!1")
                                          (("1"
                                            (expand "walk?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (hide -1)
                                                (("1"
                                                  (inst - "0")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (expand
                                                       "finseq_appl")
                                                      (("1"
                                                        (replace -6)
                                                        (("1"
                                                          (expand
                                                           "deg")
                                                          (("1"
                                                            (expand
                                                             "edge?")
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (lemma
                                                                 "card_empty?[Dbl]")
                                                                (("1"
                                                                  (inst?)
                                                                  (("1"
                                                                    (assert)
                                                                    (("1"
                                                                      (iff)
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (expand
                                                                           "empty?")
                                                                          (("1"
                                                                            (expand
                                                                             "member")
                                                                            (("1"
                                                                              (inst?)
                                                                              (("1"
                                                                                (expand
                                                                                 "incident_edges")
                                                                                (("1"
                                                                                  (expand
                                                                                   "dbl"
                                                                                   1)
                                                                                  (("1"
                                                                                    (propax)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (inst?)
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -2 -3 4)
                            (("2" (lemma "card_2_has_2[T]")
                              (("2"
                                (inst?)
                                (("2"
                                  (assert)
                                  (("2"
                                    (skosimp*)
                                    (("2"
                                      (case-replace "x!1=v!1")
                                      (("1"
                                        (inst 2 "y!1")
                                        (("1" (assert) nil nil))
                                        nil)
                                       ("2"
                                        (inst 3 "x!1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide -3 -4 1 2)
              (("2" (expand "empty?")
                (("2" (expand "empty?")
                  (("2" (inst?)
                    (("2" (expand "member") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "connected?") (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((singleton? const-decl "bool" graphs nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil graph_path_conn nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (size const-decl "nat" graphs nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (prewalk type-eq-decl nil walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (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)
    (>= 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)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (deg const-decl "nat" graph_deg nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (Dbl type-eq-decl nil doubletons nil)
    (edge? const-decl "bool" graphs nil)
    (nil application-judgement "finite_set[T]" graph_path_conn nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (y!1 skolem-const-decl "T" graph_path_conn nil)
    (G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
    (path_connected? const-decl "bool" graph_conn_defs nil)
    (card_2_has_2 formula-decl nil finite_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (card_empty? formula-decl nil finite_sets nil)
    (empty? const-decl "bool" graphs nil)
    (connected? def-decl "bool" graph_conn_defs nil))
   nil))
 (thw_A 0
  (thw_A-1 nil 3263033576
   ("" (skosimp*)
    (("" (hide -1)
      (("" (lemma "deg_1_sing")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (hide -1)
                (("" (lemma "other_vert")
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert)
                        (("" (skosimp*)
                          (("" (case-replace "u!1 = y1!1")
                            (("1"
                              (case "walk?[T](G!1, gen_seq2[T](G!1, v!1, y1!1))")
                              (("1"
                                (inst 3 "gen_seq2(G!1,v!1,y1!1)")
                                (("1"
                                  (expand "walk_from?")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (expand "gen_seq2")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (expand "walk?")
                                (("2"
                                  (expand "finseq_appl")
                                  (("2"
                                    (ground)
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (expand "gen_seq2")
                                        (("2"
                                          (lift-if)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (rewrite "dbl_comm")
                                              (("2"
                                                (expand "edge?")
                                                (("2"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2"
                              (case "vert(del_vert(G!1,v!1))(u!1) AND vert(del_vert(G!1,v!1))(y1!1)")
                              (("1"
                                (flatten)
                                (("1"
                                  (reveal -5)
                                  (("1"
                                    (inst -1 "del_vert(G!1,v!1)")
                                    (("1"
                                      (split -1)
                                      (("1"
                                        (inst -1 "u!1" "y1!1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (skosimp*)
                                            (("1"
                                              (inst
                                               4
                                               "gen_seq1(G!1,v!1) o w!1")
                                              (("1"
                                                (expand "gen_seq1")
                                                (("1"
                                                  (expand "o ")
                                                  (("1"
                                                    (expand
                                                     "walk_from?")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (expand
                                                           "walk?")
                                                          (("1"
                                                            (expand
                                                             "finseq_appl")
                                                            (("1"
                                                              (expand
                                                               "verts_in?")
                                                              (("1"
                                                                (split)
                                                                (("1"
                                                                  (skosimp*)
                                                                  (("1"
                                                                    (ground)
                                                                    (("1"
                                                                      (lemma
                                                                       "vert_seq_lem")
                                                                      (("1"
                                                                        (expand
                                                                         "finseq_appl")
                                                                        (("1"
                                                                          (inst?)
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (typepred
                                                                               "w!1")
                                                                              (("2"
                                                                                (expand
                                                                                 "walk?")
                                                                                (("2"
                                                                                  (expand
                                                                                   "finseq_appl")
                                                                                  (("2"
                                                                                    (flatten)
                                                                                    (("2"
                                                                                      (hide
                                                                                       -3)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "verts_in?")
                                                                                        (("2"
                                                                                          (hide
                                                                                           -11)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "del_vert")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "remove")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "member")
                                                                                                (("2"
                                                                                                  (skosimp*)
                                                                                                  (("2"
                                                                                                    (inst?)
                                                                                                    (("2"
                                                                                                      (flatten)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (typepred
                                                                   "w!1")
                                                                  (("2"
                                                                    (expand
                                                                     "walk?")
                                                                    (("2"
                                                                      (expand
                                                                       "finseq_appl")
                                                                      (("2"
                                                                        (expand
                                                                         "verts_in?")
                                                                        (("2"
                                                                          (flatten)
                                                                          (("2"
                                                                            (skosimp*)
                                                                            (("2"
                                                                              (case-replace
                                                                               "n!1 = 0")
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (expand
                                                                                   "edge?")
                                                                                  (("1"
                                                                                    (replace
                                                                                     -6)
                                                                                    (("1"
                                                                                      (rewrite
                                                                                       "dbl_comm")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (lift-if)
                                                                                (("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (inst
                                                                                     -3
                                                                                     "n!1-1")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "edge?")
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "del_vert"
                                                                                               -3)
                                                                                              (("2"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (prop)
                                                (("1"
                                                  (expand "o ")
                                                  (("1"
                                                    (expand "gen_seq1")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide -8 -9)
                                                  (("2"
                                                    (expand "gen_seq1")
                                                    (("2"
                                                      (expand*
                                                       "walk?"
                                                       "finseq_appl")
                                                      (("2"
                                                        (expand
                                                         "verts_in?")
                                                        (("2"
                                                          (prop)
                                                          (("1"
                                                            (skosimp*)
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (expand
                                                                 "o ")
                                                                (("1"
                                                                  (ground)
                                                                  (("1"
                                                                    (typepred
                                                                     "w!1")
                                                                    (("1"
                                                                      (expand*
                                                                       "walk?"
                                                                       "finseq_appl")
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (hide
                                                                           -3
                                                                           -4
                                                                           -5
                                                                           -6)
                                                                          (("1"
                                                                            (expand
                                                                             "verts_in?")
                                                                            (("1"
                                                                              (inst?)
                                                                              (("1"
                                                                                (expand
                                                                                 "del_vert")
                                                                                (("1"
                                                                                  (expand
                                                                                   "remove")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("1"
                                                                                      (propax)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (assert)
                                                            (("2"
                                                              (expand
                                                               "o ")
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (skosimp*)
                                                                  (("2"
                                                                    (case-replace
                                                                     "n!1 = 0")
                                                                    (("1"
                                                                      (expand
                                                                       "walk_from?")
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (lift-if)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (replace
                                                                               -3)
                                                                              (("1"
                                                                                (expand
                                                                                 "edge?")
                                                                                (("1"
                                                                                  (rewrite
                                                                                   "dbl_comm")
                                                                                  (("1"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (typepred
                                                                       "w!1")
                                                                      (("2"
                                                                        (expand*
                                                                         "walk?"
                                                                         "finseq_appl")
                                                                        (("2"
                                                                          (expand
                                                                           "verts_in?")
                                                                          (("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (inst
                                                                               -3
                                                                               "n!1-1")
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (expand
                                                                                   "edge?")
                                                                                  (("1"
                                                                                    (flatten)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "edges_del_vert")
                                                                                        (("1"
                                                                                          (inst?)
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (inst?)
                                                                                (("1"
                                                                                  (assert)
                                                                                  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"
                                        (rewrite "size_del_vert")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide -6 -7 5)
                                (("2"
                                  (expand "del_vert")
                                  (("2"
                                    (expand "remove")
                                    (("2"
                                      (expand "member")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (other_vert formula-decl nil graphs nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (w!1 skolem-const-decl "Walk[T](del_vert(G!1, v!1))"
     graph_path_conn nil)
    (gen_seq1 const-decl "Seq(G)" walks nil)
    (O const-decl "finseq" finite_sequences nil)
    (vert_seq_lem formula-decl nil walks nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (n!1 skolem-const-decl "nat" graph_path_conn nil)
    (edges_del_vert formula-decl nil graph_ops nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (size_del_vert formula-decl nil graph_ops nil)
    (gen_seq2 const-decl "Seq(G)" walks nil)
    (Seq type-eq-decl nil walks nil)
    (verts_in? const-decl "bool" walks nil)
    (walk? const-decl "bool" walks nil)
    (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)
    (walk_from? const-decl "bool" walks nil)
    (nil application-judgement "finite_set[T]" graph_path_conn nil)
    (Walk type-eq-decl nil walks nil)
    (G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
    (v!1 skolem-const-decl "T" graph_path_conn nil)
    (y1!1 skolem-const-decl "T" graph_path_conn nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (dbl_comm formula-decl nil doubletons nil)
    (edge? const-decl "bool" graphs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (deg_1_sing formula-decl nil graph_deg nil)
    (T formal-type-decl nil graph_path_conn nil))
   nil))
 (tree_has_walk 0
  (tree_has_walk-1 nil 3263033576
   ("" (induct "TR" 1 "graph_induction_vert")
    (("" (skosimp*)
      (("" (hide -1)
        (("" (expand "tree?")
          (("" (split)
            (("1" (rewrite "card_one[T]")
              (("1" (skosimp*)
                (("1" (replace -1)
                  (("1" (hide -1)
                    (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (case-replace "x!1 =v!1")
                (("1" (reveal -1)
                  (("1" (lemma "thw_A")
                    (("1" (inst -1 "G!1" "v!1" "y!1")
                      (("1" (replace -2)
                        (("1" (hide -2) (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (case-replace "y!1 = v!1")
                  (("1" (lemma "thw_A")
                    (("1" (inst -1 "G!1" "v!1" "x!1")
                      (("1" (reveal -2)
                        (("1" (replace -1)
                          (("1" (hide -1)
                            (("1" (assert)
                              (("1"
                                (skosimp*)
                                (("1"
                                  (lemma "walk?_reverse")
                                  (("1"
                                    (inst?)
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (reveal -1)
                    (("2" (inst?)
                      (("2" (split -1)
                        (("1" (inst -1 "x!1" "y!1")
                          (("1" (assert)
                            (("1" (split -1)
                              (("1"
                                (skosimp*)
                                (("1"
                                  (inst 4 "w!1")
                                  (("1"
                                    (expand "walk_from?")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (typepred "w!1")
                                          (("1"
                                            (lemma "walk?_del_vert")
                                            (("1"
                                              (inst?)
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (lemma "walk?_del_vert")
                                    (("2"
                                      (inst?)
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide -1 -2 5)
                                (("2"
                                  (expand "del_vert")
                                  (("2"
                                    (expand "remove")
                                    (("2"
                                      (expand "member")
                                      (("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3"
                                (hide -1 -2 5)
                                (("3"
                                  (expand "del_vert")
                                  (("3"
                                    (expand "remove")
                                    (("3"
                                      (expand "member")
                                      (("3" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "size_del_vert")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((walk?_reverse formula-decl nil walks nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (size_del_vert formula-decl nil graph_ops nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
    (v!1 skolem-const-decl "(vert(G!1))" graph_path_conn nil)
    (w!1 skolem-const-decl "Walk[T](del_vert[T](G!1, v!1))"
     graph_path_conn nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (walk?_del_vert formula-decl nil path_ops nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (nil application-judgement "finite_set[T]" graph_path_conn nil)
    (thw_A formula-decl nil graph_path_conn nil)
    (is_finite const-decl "bool" finite_sets nil)
    (card_one formula-decl nil finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (graph_induction_vert formula-decl nil graph_inductions nil)
    (T formal-type-decl nil graph_path_conn nil)
    (walk_from? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (prewalk type-eq-decl nil walks nil)
    (> const-decl "bool" reals nil)
    (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)
    (tree? def-decl "bool" trees nil)
    (pred type-eq-decl nil defined_types nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (path_implies_conn 0
  (path_implies_conn-2 nil 3507897810
   ("" (induct "G" 1 "graph_induction_vert")
    (("" (skosimp*)
      (("" (case "(FORALL v: vert(G!1)(v) IMPLIES deg(v,G!1) > 0)")
        (("1" (hide -2)
          (("1" (expand "connected?")
            (("1" (flatten)
              (("1" (case "nonempty?(vert(G!1))")
                (("1" (name "MTR" "max_subtree(G!1)")
                  (("1" (lemma "max_tree_all_verts")
                    (("1" (assert)
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (case "tree?(MTR)")
                            (("1" (expand "tree?" -1)
                              (("1"
                                (split)
                                (("1"
                                  (expand "singleton?")
                                  (("1"
                                    (expand "size")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (name "TCd" "del_vert(MTR,v!1)")
                                    (("2"
                                      (replace -1)
                                      (("2"
                                        (inst 2 "v!1")
                                        (("2"
                                          (split 2)
                                          (("1"
                                            (hide -4 -7 -8 -9 2)
                                            (("1"
                                              (hide -4)
                                              (("1"
                                                (expand "deg")
                                                (("1"
                                                  (case
                                                   "subset?(incident_edges(v!1, MTR),incident_edges(v!1, G!1))")
                                                  (("1"
                                                    (lemma
                                                     "card_subset[Dbl]")
                                                    (("1"
                                                      (inst?)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide -2 2)
                                                    (("2"
                                                      (expand
                                                       "subset?")
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (expand
                                                             "incident_edges")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (reveal
                                                                 -2)
                                                                (("2"
                                                                  (lemma
                                                                   "max_subtree_subgraph")
                                                                  (("2"
                                                                    (inst?)
                                                                    (("2"
                                                                      (replace
                                                                       -2)
                                                                      (("2"
                                                                        (hide
                                                                         -2)
                                                                        (("2"
                                                                          (expand
                                                                           "subgraph?")
                                                                          (("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (hide
                                                                               -1)
                                                                              (("2"
                                                                                (expand
                                                                                 "subset?")
                                                                                (("2"
                                                                                  (inst?)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("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"
                                            (reveal -2)
                                            (("2"
                                              (inst
                                               -1
                                               "del_vert(G!1, v!1)")
                                              (("2"
                                                (split -1)
                                                (("1" (propax) nil nil)
                                                 ("2"
                                                  (lemma
                                                   "max_tree_all_verts")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (hide -8)
                                                        (("2"
                                                          (expand
                                                           "path_connected?")
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (hide 1)
                                                              (("1"
                                                                (hide
                                                                 -2
                                                                 -3
                                                                 -4
                                                                 -5
                                                                 -6
                                                                 -7
                                                                 -9)
                                                                (("1"
                                                                  (expand
                                                                   "empty?")
                                                                  (("1"
                                                                    (lemma
                                                                     "card_empty?[T]")
                                                                    (("1"
                                                                      (inst?)
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (iff)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (hide
                                                                               -2)
                                                                              (("1"
                                                                                (expand
                                                                                 "del_vert")
                                                                                (("1"
                                                                                  (rewrite
                                                                                   "card_remove")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "singleton?")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "size")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (skosimp*)
                                                              (("2"
                                                                (lemma
                                                                 "tree_has_walk")
                                                                (("2"
                                                                  (inst
                                                                   -1
                                                                   "TCd"
                                                                   "x!1"
                                                                   "y!1")
                                                                  (("2"
                                                                    (expand
                                                                     "walk_from?")
                                                                    (("2"
                                                                      (split
                                                                       -1)
                                                                      (("1"
                                                                        (skosimp*)
                                                                        (("1"
                                                                          (lemma
                                                                           "tree_has_walk")
                                                                          (("1"
                                                                            (inst
                                                                             -1
                                                                             "TCd"
                                                                             "x!1"
                                                                             "y!1")
                                                                            (("1"
                                                                              (expand
                                                                               "walk_from?")
                                                                              (("1"
                                                                                (split
                                                                                 -1)
                                                                                (("1"
                                                                                  (skosimp*)
                                                                                  (("1"
                                                                                    (inst
                                                                                     1
                                                                                     "w!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (hide
                                                                                       -1
                                                                                       -2)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -5
                                                                                         -9
                                                                                         2
                                                                                         3)
                                                                                        (("2"
                                                                                          (typepred
                                                                                           "w!1")
                                                                                          (("2"
                                                                                            (replace
                                                                                             -5
                                                                                             *
                                                                                             rl)
                                                                                            (("2"
                                                                                              (hide
                                                                                               -5)
                                                                                              (("2"
                                                                                                (replace
                                                                                                 -7
                                                                                                 *
                                                                                                 rl)
                                                                                                (("2"
                                                                                                  (hide
                                                                                                   -7)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "walk?")
                                                                                                    (("2"
                                                                                                      (flatten)
                                                                                                      (("2"
                                                                                                        (split
                                                                                                         1)
                                                                                                        (("1"
                                                                                                          (hide
                                                                                                           -3)
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "verts_in?")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "del_vert")
                                                                                                              (("1"
                                                                                                                (skosimp*)
                                                                                                                (("1"
                                                                                                                  (inst?)
                                                                                                                  (("1"
                                                                                                                    (expand
                                                                                                                     "remove")
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "member")
                                                                                                                      (("1"
                                                                                                                        (flatten)
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (skosimp*)
                                                                                                          (("2"
                                                                                                            (inst?)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "edge?")
                                                                                                                (("2"
                                                                                                                  (flatten)
                                                                                                                  (("2"
                                                                                                                    (typepred
                                                                                                                     "max_subtree(G!1)")
                                                                                                                    (("2"
                                                                                                                      (hide
                                                                                                                       -1
                                                                                                                       -2)
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "subgraph?")
                                                                                                                        (("2"
                                                                                                                          (flatten)
                                                                                                                          (("2"
                                                                                                                            (hide
                                                                                                                             -1)
                                                                                                                            (("2"
                                                                                                                              (expand
                                                                                                                               "subset?")
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "member")
                                                                                                                                (("2"
                                                                                                                                  (inst?)
                                                                                                                                  (("2"
                                                                                                                                    (hide
                                                                                                                                     -3)
                                                                                                                                    (("2"
                                                                                                                                      (expand
                                                                                                                                       "del_vert")
                                                                                                                                      (("2"
                                                                                                                                        (flatten)
                                                                                                                                        (("2"
                                                                                                                                          (assert)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (typepred
                                                                                   "x!1")
                                                                                  (("2"
                                                                                    (hide
                                                                                     -3)
                                                                                    (("2"
                                                                                      (hide
                                                                                       2
                                                                                       3
                                                                                       4)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -2
                                                                                         -4)
                                                                                        (("2"
                                                                                          (replace
                                                                                           -2
                                                                                           *
                                                                                           rl)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "del_vert"
                                                                                             1)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "remove")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "member")
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "del_vert"
                                                                                                     -1)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "remove")
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "member")
                                                                                                        (("2"
                                                                                                          (flatten)
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("3"
                                                                                  (typepred
                                                                                   "y!1")
                                                                                  (("3"
                                                                                    (hide
                                                                                     -2
                                                                                     -3
                                                                                     -6
                                                                                     -9
                                                                                     -10
                                                                                     2
                                                                                     3
                                                                                     4)
                                                                                    (("3"
                                                                                      (replace
                                                                                       -2
                                                                                       *
                                                                                       rl)
                                                                                      (("3"
                                                                                        (hide
                                                                                         -2)
                                                                                        (("3"
                                                                                          (expand
                                                                                           "del_vert")
                                                                                          (("3"
                                                                                            (expand
                                                                                             "remove")
                                                                                            (("3"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("3"
                                                                                                (flatten)
                                                                                                (("3"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("4"
                                                                                  (assert)
                                                                                  (("4"
                                                                                    (inst
                                                                                     2
                                                                                     "gen_seq1(del_vert(G!1,v!1),y!1)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "gen_seq1")
                                                                                      (("1"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "gen_seq1_is_walk")
                                                                                      (("2"
                                                                                        (inst?)
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (typepred
                                                                         "x!1")
                                                                        (("2"
                                                                          (hide
                                                                           -3)
                                                                          (("2"
                                                                            (hide
                                                                             2
                                                                             3
                                                                             4)
                                                                            (("2"
                                                                              (replace
                                                                               -2
                                                                               *
                                                                               rl)
                                                                              (("2"
                                                                                (expand
                                                                                 "del_vert"
                                                                                 1)
                                                                                (("2"
                                                                                  (expand
                                                                                   "remove")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "del_vert"
                                                                                         -1)
                                                                                        (("2"
                                                                                          (expand
                                                                                           "remove")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("2"
                                                                                              (flatten)
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("3"
                                                                        (typepred
                                                                         "y!1")
                                                                        (("3"
                                                                          (hide
                                                                           -4
                                                                           -7
                                                                           -8
                                                                           2
                                                                           3
                                                                           4)
                                                                          (("3"
                                                                            (replace
                                                                             -2
                                                                             *
                                                                             rl)
                                                                            (("3"
                                                                              (hide
                                                                               -2)
                                                                              (("3"
                                                                                (expand
                                                                                 "del_vert")
                                                                                (("3"
                                                                                  (expand
                                                                                   "remove")
                                                                                  (("3"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("3"
                                                                                      (flatten)
                                                                                      (("3"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("4"
                                                                        (assert)
                                                                        (("4"
                                                                          (inst
                                                                           2
                                                                           "gen_seq1(del_vert(G!1,v!1),y!1)")
                                                                          (("1"
                                                                            (expand
                                                                             "gen_seq1")
                                                                            (("1"
                                                                              (propax)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (lemma
                                                                             "gen_seq1_is_walk")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (rewrite
                                                   "size_del_vert")
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (propax) nil nil))
                  nil)
                 ("2" (expand "nonempty?")
                  (("2" (expand "path_connected?" -3)
                    (("2" (flatten)
                      (("2" (expand "empty?" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "pic_A")
            (("2" (inst?)
              (("2" (assert)
                (("2" (inst 1 "v!1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pic_A formula-decl nil graph_path_conn nil)
    (Graph type-eq-decl nil graphs nil)
    (tree? def-decl "bool" trees nil) (Tree type-eq-decl nil trees nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (Subtree type-eq-decl nil max_subtrees nil)
    (max_subtree const-decl "Subtree(G)" max_subtrees nil)
    (subset? const-decl "bool" sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Dbl type-eq-decl nil doubletons nil)
    (card_subset formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil)
    (max_subtree_subgraph formula-decl nil max_subtrees nil)
    (size_del_vert formula-decl nil graph_ops nil)
    (gen_seq1_is_walk formula-decl nil walks nil)
    (y!1 skolem-const-decl "(vert(del_vert(G!1, v!1)))" graph_path_conn
     nil)
    (gen_seq1 const-decl "Seq(G)" walks nil)
    (Seq type-eq-decl nil walks nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (edge? const-decl "bool" graphs nil)
    (nil application-judgement "finite_set[T]" graph_path_conn nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (remove const-decl "set" sets nil)
    (verts_in? const-decl "bool" walks nil)
    (w!1 skolem-const-decl "Walk[T](TCd)" graph_path_conn nil)
    (Walk type-eq-decl nil walks nil)
    (TCd skolem-const-decl "graph[T]" graph_path_conn nil)
    (v!1 skolem-const-decl "(vert(MTR))" graph_path_conn nil)
    (MTR skolem-const-decl "Subtree[T](G!1)" graph_path_conn nil)
    (G!1 skolem-const-decl "graph[T]" graph_path_conn nil)
    (walk? const-decl "bool" walks nil)
    (prewalk type-eq-decl nil walks nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (walk_from? const-decl "bool" walks nil)
    (tree_has_walk formula-decl nil graph_path_conn nil)
    (empty? const-decl "bool" graphs nil)
    (card_remove formula-decl nil finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_empty? formula-decl nil finite_sets nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (singleton? const-decl "bool" graphs nil)
    (size const-decl "nat" graphs nil)
    (max_tree_all_verts formula-decl nil subtrees nil)
    (nonempty? const-decl "bool" sets 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)
    (deg const-decl "nat" graph_deg nil)
    (graph_induction_vert formula-decl nil graph_inductions nil)
    (T formal-type-decl nil graph_path_conn nil)
    (connected? def-decl "bool" graph_conn_defs nil)
    (path_connected? const-decl "bool" graph_conn_defs nil)
    (pred type-eq-decl nil defined_types nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (path_implies_conn-1 nil 3263033576
   ("" (induct "G" 1 "graph_induction_vert")
    (("" (skosimp*)
      (("" (case "(FORALL v: vert(G!1)(v) IMPLIES deg(v,G!1) > 0)")
        (("1" (hide -2)
          (("1" (expand "connected?")
            (("1" (flatten)
              (("1" (case "nonempty?(vert(G!1))")
                (("1" (name "MTR" "max_subtree(G!1)")
                  (("1" (lemma "max_tree_all_verts")
                    (("1" (assert)
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (case "tree?(MTR)")
                            (("1" (expand "tree?" -1)
                              (("1"
                                (split)
                                (("1"
                                  (expand "singleton?")
                                  (("1"
                                    (expand "size")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skosimp*)
                                  (("2"
                                    (name "TC" "del_vert(MTR,v!1)")
                                    (("2"
                                      (replace -1)
                                      (("2"
                                        (inst 2 "v!1")
                                        (("2"
                                          (split 2)
                                          (("1"
                                            (hide -4 -7 -8 -9 2)
                                            (("1"
                                              (hide -4)
                                              (("1"
                                                (expand "deg")
                                                (("1"
                                                  (case
                                                   "subset?(incident_edges(v!1, MTR),incident_edges(v!1, G!1))")
                                                  (("1"
                                                    (lemma
                                                     "card_subset[Dbl]")
                                                    (("1"
                                                      (inst?)
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide -2 2)
                                                    (("2"
                                                      (expand
                                                       "subset?")
                                                      (("2"
                                                        (skosimp*)
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (expand
                                                             "incident_edges")
                                                            (("2"
                                                              (assert)
                                                              (("2"
                                                                (reveal
                                                                 -2)
                                                                (("2"
                                                                  (lemma
                                                                   "max_subtree_subgraph")
                                                                  (("2"
                                                                    (inst?)
                                                                    (("2"
                                                                      (replace
                                                                       -2)
                                                                      (("2"
                                                                        (hide
                                                                         -2)
                                                                        (("2"
                                                                          (expand
                                                                           "subgraph?")
                                                                          (("2"
                                                                            (flatten)
                                                                            (("2"
                                                                              (hide
                                                                               -1)
                                                                              (("2"
                                                                                (expand
                                                                                 "subset?")
                                                                                (("2"
                                                                                  (inst?)
                                                                                  (("2"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("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"
                                            (reveal -2)
                                            (("2"
                                              (inst
                                               -1
                                               "del_vert(G!1, v!1)")
                                              (("2"
                                                (split -1)
                                                (("1" (propax) nil nil)
                                                 ("2"
                                                  (lemma
                                                   "max_tree_all_verts")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (hide -8)
                                                        (("2"
                                                          (expand
                                                           "path_connected?")
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (hide 1)
                                                              (("1"
                                                                (hide
                                                                 -2
                                                                 -3
                                                                 -4
                                                                 -5
                                                                 -6
                                                                 -7
                                                                 -9)
                                                                (("1"
                                                                  (expand
                                                                   "empty?")
                                                                  (("1"
                                                                    (lemma
                                                                     "card_empty?[T]")
                                                                    (("1"
                                                                      (inst?)
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (iff)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (hide
                                                                               -2)
                                                                              (("1"
                                                                                (expand
                                                                                 "del_vert")
                                                                                (("1"
                                                                                  (rewrite
                                                                                   "card_remove")
                                                                                  (("1"
                                                                                    (expand
                                                                                     "singleton?")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "size")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (skosimp*)
                                                              (("2"
                                                                (lemma
                                                                 "tree_has_walk")
                                                                (("2"
                                                                  (inst
                                                                   -1
                                                                   "TC"
                                                                   "x!1"
                                                                   "y!1")
                                                                  (("2"
                                                                    (expand
                                                                     "walk_from?")
                                                                    (("2"
                                                                      (split
                                                                       -1)
                                                                      (("1"
                                                                        (skosimp*)
                                                                        (("1"
                                                                          (lemma
                                                                           "tree_has_walk")
                                                                          (("1"
                                                                            (inst
                                                                             -1
                                                                             "TC"
                                                                             "x!1"
                                                                             "y!1")
                                                                            (("1"
                                                                              (expand
                                                                               "walk_from?")
                                                                              (("1"
                                                                                (split
                                                                                 -1)
                                                                                (("1"
                                                                                  (skosimp*)
                                                                                  (("1"
                                                                                    (inst
                                                                                     1
                                                                                     "w!1")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil)
                                                                                     ("2"
                                                                                      (hide
                                                                                       -1
                                                                                       -2)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -5
                                                                                         -9
                                                                                         2
                                                                                         3)
                                                                                        (("2"
                                                                                          (typepred
                                                                                           "w!1")
                                                                                          (("2"
                                                                                            (replace
                                                                                             -5
                                                                                             *
                                                                                             rl)
                                                                                            (("2"
                                                                                              (hide
                                                                                               -5)
                                                                                              (("2"
                                                                                                (replace
                                                                                                 -7
                                                                                                 *
                                                                                                 rl)
                                                                                                (("2"
                                                                                                  (hide
                                                                                                   -7)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "walk?")
                                                                                                    (("2"
                                                                                                      (flatten)
                                                                                                      (("2"
                                                                                                        (split
                                                                                                         1)
                                                                                                        (("1"
                                                                                                          (hide
                                                                                                           -3)
                                                                                                          (("1"
                                                                                                            (expand
                                                                                                             "verts_in?")
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "del_vert")
                                                                                                              (("1"
                                                                                                                (skosimp*)
                                                                                                                (("1"
                                                                                                                  (inst?)
                                                                                                                  (("1"
                                                                                                                    (expand
                                                                                                                     "remove")
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "member")
                                                                                                                      (("1"
                                                                                                                        (flatten)
                                                                                                                        (("1"
                                                                                                                          (assert)
                                                                                                                          nil
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (skosimp*)
                                                                                                          (("2"
                                                                                                            (inst?)
                                                                                                            (("2"
                                                                                                              (assert)
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "edge?")
                                                                                                                (("2"
                                                                                                                  (flatten)
                                                                                                                  (("2"
                                                                                                                    (typepred
                                                                                                                     "max_subtree(G!1)")
                                                                                                                    (("2"
                                                                                                                      (hide
                                                                                                                       -1
                                                                                                                       -2)
                                                                                                                      (("2"
                                                                                                                        (expand
                                                                                                                         "subgraph?")
                                                                                                                        (("2"
                                                                                                                          (flatten)
                                                                                                                          (("2"
                                                                                                                            (hide
                                                                                                                             -1)
                                                                                                                            (("2"
                                                                                                                              (expand
                                                                                                                               "subset?")
                                                                                                                              (("2"
                                                                                                                                (expand
                                                                                                                                 "member")
                                                                                                                                (("2"
                                                                                                                                  (inst?)
                                                                                                                                  (("1"
                                                                                                                                    (hide
                                                                                                                                     -3)
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "del_vert")
                                                                                                                                      (("1"
                                                                                                                                        (flatten)
                                                                                                                                        (("1"
                                                                                                                                          (assert)
                                                                                                                                          nil
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil)
                                                                                                                                   ("2"
                                                                                                                                    (inst?)
                                                                                                                                    (("2"
                                                                                                                                      (assert)
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (typepred
                                                                                   "x!1")
                                                                                  (("2"
                                                                                    (hide
                                                                                     -3)
                                                                                    (("2"
                                                                                      (hide
                                                                                       2
                                                                                       3
                                                                                       4)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -2
                                                                                         -4)
                                                                                        (("2"
                                                                                          (replace
                                                                                           -2
                                                                                           *
                                                                                           rl)
                                                                                          (("2"
                                                                                            (expand
                                                                                             "del_vert"
                                                                                             1)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "remove")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "member")
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "del_vert"
                                                                                                     -1)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "remove")
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "member")
                                                                                                        (("2"
                                                                                                          (flatten)
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("3"
                                                                                  (typepred
                                                                                   "y!1")
                                                                                  (("3"
                                                                                    (hide
                                                                                     -2
                                                                                     -3
                                                                                     -6
                                                                                     -9
                                                                                     -10
                                                                                     2
                                                                                     3
                                                                                     4)
                                                                                    (("3"
                                                                                      (replace
                                                                                       -2
                                                                                       *
                                                                                       rl)
                                                                                      (("3"
                                                                                        (hide
                                                                                         -2)
                                                                                        (("3"
                                                                                          (expand
                                                                                           "del_vert")
                                                                                          (("3"
                                                                                            (expand
                                                                                             "remove")
                                                                                            (("3"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("3"
                                                                                                (flatten)
                                                                                                (("3"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("4"
                                                                                  (assert)
                                                                                  (("4"
                                                                                    (inst
                                                                                     2
                                                                                     "gen_seq1(del_vert(G!1,v!1),y!1)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "gen_seq1")
                                                                                      (("1"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "gen_seq1_is_walk")
                                                                                      (("2"
                                                                                        (inst?)
                                                                                        (("2"
                                                                                          (flatten)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (typepred
                                                                         "x!1")
                                                                        (("2"
                                                                          (hide
                                                                           -3)
                                                                          (("2"
                                                                            (hide
                                                                             2
                                                                             3
                                                                             4)
                                                                            (("2"
                                                                              (replace
                                                                               -2
                                                                               *
                                                                               rl)
                                                                              (("2"
                                                                                (expand
                                                                                 "del_vert"
                                                                                 1)
                                                                                (("2"
                                                                                  (expand
                                                                                   "remove")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (expand
                                                                                         "del_vert"
                                                                                         -1)
                                                                                        (("2"
                                                                                          (expand
                                                                                           "remove")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("2"
                                                                                              (flatten)
                                                                                              (("2"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("3"
                                                                        (typepred
                                                                         "y!1")
                                                                        (("3"
                                                                          (hide
                                                                           -4
                                                                           -7
                                                                           -8
                                                                           2
                                                                           3
                                                                           4)
                                                                          (("3"
                                                                            (replace
                                                                             -2
                                                                             *
                                                                             rl)
                                                                            (("3"
                                                                              (hide
                                                                               -2)
                                                                              (("3"
                                                                                (expand
                                                                                 "del_vert")
                                                                                (("3"
                                                                                  (expand
                                                                                   "remove")
                                                                                  (("3"
                                                                                    (expand
                                                                                     "member")
                                                                                    (("3"
                                                                                      (flatten)
                                                                                      (("3"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("4"
                                                                        (assert)
                                                                        (("4"
                                                                          (inst
                                                                           2
                                                                           "gen_seq1(del_vert(G!1,v!1),y!1)")
                                                                          (("1"
                                                                            (expand
                                                                             "gen_seq1")
                                                                            (("1"
                                                                              (propax)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (lemma
                                                                             "gen_seq1_is_walk")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (rewrite
                                                   "size_del_vert")
                                                  (("3"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (propax) nil nil))
                  nil)
                 ("2" (expand "nonempty?")
                  (("2" (expand "path_connected?" -3)
                    (("2" (flatten)
                      (("2" (expand "empty?" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skosimp*)
          (("2" (lemma "pic_A")
            (("2" (inst?)
              (("2" (assert)
                (("2" (inst 1 "v!1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Graph type-eq-decl nil graphs nil)
    (tree? def-decl "bool" trees nil) (Tree type-eq-decl nil trees nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (Subtree type-eq-decl nil max_subtrees nil)
    (max_subtree const-decl "Subtree(G)" max_subtrees nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (Dbl type-eq-decl nil doubletons nil)
    (max_subtree_subgraph formula-decl nil max_subtrees nil)
    (size_del_vert formula-decl nil graph_ops nil)
    (gen_seq1_is_walk formula-decl nil walks nil)
    (gen_seq1 const-decl "Seq(G)" walks nil)
    (Seq type-eq-decl nil walks nil)
    (edge? const-decl "bool" graphs nil)
    (verts_in? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (prewalk type-eq-decl nil walks nil)
    (walk_from? const-decl "bool" walks nil)
    (empty? const-decl "bool" graphs nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (singleton? const-decl "bool" graphs nil)
    (size const-decl "nat" graphs nil)
    (max_tree_all_verts formula-decl nil subtrees nil)
    (deg const-decl "nat" graph_deg nil)
    (graph_induction_vert formula-decl nil graph_inductions nil)
    (connected? def-decl "bool" graph_conn_defs nil)
    (path_connected? const-decl "bool" graph_conn_defs nil)
    (graph type-eq-decl nil graphs nil)
    (pregraph type-eq-decl nil graphs nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil))
   nil)))