Impressum graph_piece_path.prf

(graph_piece_path
 (union_edge_disj_TCC1 0
  (union_edge_disj_TCC1-1 nil 3251113235 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil graph_piece_path nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (graph type-eq-decl nil graphs nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (union_edge_disj 0
  (union_edge_disj-1 nil 3251113235
   ("" (skosimp*)
    (("" (apply-extensionality 2 :hide? t)
      (("1" (apply-extensionality 1 :hide? t)
        (("1" (iff 1)
          (("1" (prop)
            (("1" (replace -2)
              (("1" (hide -2)
                (("1" (replace -2)
                  (("1" (hide -2)
                    (("1" (expand "union")
                      (("1" (expand "union")
                        (("1" (expand "member")
                          (("1" (expand "subgraph")
                            (("1" (assert)
                              (("1"
                                (expand "difference")
                                (("1"
                                  (expand "member")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (typepred "G!1")
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst-cp -1 "x!2")
                                            (("1"
                                              (inst -1 "x!3")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (case-replace
                                                   "x!2 = x!3")
                                                  (("1"
                                                    (lemma
                                                     "edge_has_2_verts")
                                                    (("1"
                                                      (inst
                                                       -1
                                                       "x!1"
                                                       "x!2"
                                                       "x!3")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (inst
                                                           3
                                                           "x!3"
                                                           "x!2")
                                                          (("1"
                                                            (ground)
                                                            (("1"
                                                              (expand
                                                               "edg")
                                                              (("1"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "union")
              (("2" (expand "union")
                (("2" (expand "member")
                  (("2" (prop)
                    (("1" (replace -2)
                      (("1" (expand "subgraph")
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (replace -3)
                      (("2" (expand "subgraph")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (replace -1)
          (("2" (hide -1)
            (("2" (replace -1)
              (("2" (hide -1)
                (("2" (apply-extensionality 1 :hide? t)
                  (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil graph_piece_path 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)
    (union const-decl "graph[T]" graph_ops nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_difference application-judgement "finite_set" finite_sets
     nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (edg const-decl "doubleton[T]" graphs nil)
    (nil application-judgement "finite_set[T]" graph_piece_path nil)
    (edge_has_2_verts formula-decl nil graphs nil)
    (difference const-decl "set" sets nil)
    (subgraph const-decl "Subgraph(G)" subgraphs nil)
    (union const-decl "set" sets nil)
    (Subgraph type-eq-decl nil subgraphs nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (finite_union application-judgement "finite_set" finite_sets nil))
   nil))
 (piece_implies_path 0
  (piece_implies_path-1 nil 3251113235
   ("" (skosimp*)
    (("" (case "empty?(G!1)")
      (("1" (expand "piece_connected?") (("1" (flatten) nil nil)) nil)
       ("2" (expand "empty?")
        (("2" (expand "empty?")
          (("2" (expand "member")
            (("2" (skosimp*)
              (("2"
                (name "V"
                      "{u: T | (EXISTS (w: Walk(G!1)): w(0) = u AND w(length(w)-1) = x!1) OR u = x!1}")
                (("2" (ground)
                  (("2" (expand "finseq_appl")
                    (("2" (name "H" "subgraph(G!1,V)")
                      (("2" (name "W" "difference(vert(G!1),V)")
                        (("2" (name "K" "subgraph(G!1,W)")
                          (("2"
                            (case "(EXISTS (u,w:T): vert(H)(u) AND vert(K)(w) AND u /= w AND edges(G!1)(edg[T](u,w)))")
                            (("1" (skosimp*)
                              (("1"
                                (hide 1)
                                (("1"
                                  (expand "piece_connected?")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (inst -9 "K" "H")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (split -9)
                                          (("1"
                                            (expand "intersection")
                                            (("1"
                                              (expand "empty?")
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (expand "member")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (hide
                                                       -3
                                                       -4
                                                       -5
                                                       -9
                                                       -10
                                                       1)
                                                      (("1"
                                                        (replace
                                                         -3
                                                         *
                                                         rl)
                                                        (("1"
                                                          (hide -3)
                                                          (("1"
                                                            (replace
                                                             -3
                                                             *
                                                             rl)
                                                            (("1"
                                                              (hide -3)
                                                              (("1"
                                                                (replace
                                                                 -3
                                                                 *
                                                                 rl)
                                                                (("1"
                                                                  (hide
                                                                   -3)
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide -8 1 2)
                                            (("2"
                                              (case "V(u!1)")
                                              (("1"
                                                (case "V(w!1)")
                                                (("1"
                                                  (hide -5 -8 -9)
                                                  (("1"
                                                    (expand
                                                     "difference")
                                                    (("1"
                                                      (replace -6 * rl)
                                                      (("1"
                                                        (expand
                                                         "subgraph")
                                                        (("1"
                                                          (replace
                                                           -5
                                                           *
                                                           rl)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (hide
                                                               -5
                                                               -6)
                                                              (("1"
                                                                (expand
                                                                 "member")
                                                                (("1"
                                                                  (propax)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide -2 -6 -7)
                                                  (("2"
                                                    (replace -4 * rl)
                                                    (("2"
                                                      (hide -4)
                                                      (("2"
                                                        (expand
                                                         "subgraph")
                                                        (("2"
                                                          (flatten)
                                                          (("2"
                                                            (replace
                                                             -5
                                                             *
                                                             rl)
                                                            (("2"
                                                              (hide -5)
                                                              (("2"
                                                                (beta)
                                                                (("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (split
                                                                     -1)
                                                                    (("1"
                                                                      (skosimp*)
                                                                      (("1"
                                                                        (case-replace
                                                                         "u!1 = w!1")
                                                                        (("1"
                                                                          (inst
                                                                           1
                                                                           "w!2")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (inst
                                                                           +
                                                                           "gen_seq1(G!1,w!1) o w!2")
                                                                          (("1"
                                                                            (expand
                                                                             "o ")
                                                                            (("1"
                                                                              (expand
                                                                               "gen_seq1")
                                                                              (("1"
                                                                                (propax)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (lemma
                                                                             "walk_concat_edge")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "G!1"
                                                                               "w!1"
                                                                               "u!1"
                                                                               "w!1"
                                                                               "x!1"
                                                                               "gen_seq1[T](G!1, w!1)"
                                                                               "w!2")
                                                                              (("2"
                                                                                (expand
                                                                                 "walk_from?")
                                                                                (("2"
                                                                                  (assert)
                                                                                  (("2"
                                                                                    (split
                                                                                     +)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      (("1"
                                                                                        (hide
                                                                                         -1)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "o ")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "gen_seq1")
                                                                                            (("1"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (hide
                                                                                         1)
                                                                                        (("2"
                                                                                          (expand
                                                                                           "edg")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "edge?")
                                                                                            (("2"
                                                                                              (rewrite
                                                                                               "dbl_comm")
                                                                                              (("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (rewrite
                                                                                                   "gen_seq1_is_walk")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "gen_seq1")
                                                                                                    (("2"
                                                                                                      (propax)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (replace
                                                                       -1)
                                                                      (("2"
                                                                        (hide
                                                                         -1)
                                                                        (("2"
                                                                          (inst
                                                                           +
                                                                           "gen_seq2(G!1,w!1,x!1)")
                                                                          (("1"
                                                                            (expand
                                                                             "gen_seq2")
                                                                            (("1"
                                                                              (propax)
                                                                              nil
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (lemma
                                                                             "edge_to_walk")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (assert)
                                                                                (("2"
                                                                                  (expand
                                                                                   "edg")
                                                                                  (("2"
                                                                                    (rewrite
                                                                                     "dbl_comm")
                                                                                    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 -5 -7)
                                                (("2"
                                                  (expand "subgraph")
                                                  (("2"
                                                    (replace -2 * rl)
                                                    (("2"
                                                      (hide -2)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (expand "empty?")
                                            (("3"
                                              (expand "empty?")
                                              (("3"
                                                (inst -1 "w!1")
                                                (("3"
                                                  (expand "member")
                                                  (("3"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("4"
                                            (expand "empty?")
                                            (("4"
                                              (expand "empty?")
                                              (("4"
                                                (inst -1 "u!1")
                                                (("4"
                                                  (expand "member")
                                                  (("4"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide 2)
                              (("2"
                                (lemma "union_edge_disj")
                                (("2"
                                  (inst
                                   -1
                                   "G!1"
                                   "subgraph(G!1, V)"
                                   "subgraph(G!1, W)"
                                   "V")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (replace -2)
                                      (("2"
                                        (replace -4)
                                        (("2"
                                          (split -1)
                                          (("1"
                                            (hide 1)
                                            (("1"
                                              (expand
                                               "piece_connected?")
                                              (("1"
                                                (prop)
                                                (("1"
                                                  (inst -7 "H" "K")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (split -7)
                                                      (("1"
                                                        (hide -1 -6 2)
                                                        (("1"
                                                          (replace
                                                           -1
                                                           *
                                                           rl)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (replace
                                                               -1
                                                               *
                                                               rl)
                                                              (("1"
                                                                (hide
                                                                 -1)
                                                                (("1"
                                                                  (replace
                                                                   -1
                                                                   *
                                                                   rl)
                                                                  (("1"
                                                                    (hide
                                                                     -1)
                                                                    (("1"
                                                                      (replace
                                                                       -1
                                                                       *
                                                                       rl)
                                                                      (("1"
                                                                        (hide
                                                                         -1)
                                                                        (("1"
                                                                          (grind)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (replace
                                                         -5
                                                         *
                                                         rl)
                                                        (("2"
                                                          (expand
                                                           "empty?")
                                                          (("2"
                                                            (hide
                                                             -2
                                                             -3
                                                             -4
                                                             -5)
                                                            (("2"
                                                              (replace
                                                               -2
                                                               *
                                                               rl)
                                                              (("2"
                                                                (hide
                                                                 -2)
                                                                (("2"
                                                                  (expand
                                                                   "subgraph")
                                                                  (("2"
                                                                    (expand
                                                                     "empty?")
                                                                    (("2"
                                                                      (inst
                                                                       -1
                                                                       "x!1")
                                                                      (("2"
                                                                        (expand
                                                                         "member")
                                                                        (("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (hide -7)
                                                        (("3"
                                                          (reveal 2)
                                                          (("3"
                                                            (expand
                                                             "path_connected?")
                                                            (("3"
                                                              (skosimp*)
                                                              (("3"
                                                                (case
                                                                 "vert(K)(x!2) OR vert(K)(y!1)")
                                                                (("1"
                                                                  (hide
                                                                   -3
                                                                   -4
                                                                   -5
                                                                   -6
                                                                   -7
                                                                   1
                                                                   2
                                                                   3)
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (case
                                                                   "vert(H)(x!2) AND vert(H)(y!1)")
                                                                  (("1"
                                                                    (flatten)
                                                                    (("1"
                                                                      (hide
                                                                       -3
                                                                       -4
                                                                       -5
                                                                       -6
                                                                       1
                                                                       2)
                                                                      (("1"
                                                                        (replace
                                                                         -4
                                                                         *
                                                                         rl)
                                                                        (("1"
                                                                          (hide
                                                                           -4)
                                                                          (("1"
                                                                            (replace
                                                                             -3
                                                                             *
                                                                             rl)
                                                                            (("1"
                                                                              (hide
                                                                               -3)
                                                                              (("1"
                                                                                (expand
                                                                                 "subgraph")
                                                                                (("1"
                                                                                  (case-replace
                                                                                   "x!2 = x!1")
                                                                                  (("1"
                                                                                    (case-replace
                                                                                     "y!1 = x!1")
                                                                                    (("1"
                                                                                      (inst
                                                                                       1
                                                                                       "gen_seq1(G!1,x!1)")
                                                                                      (("1"
                                                                                        (expand
                                                                                         "gen_seq1")
                                                                                        (("1"
                                                                                          (propax)
                                                                                          nil
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (lemma
                                                                                         "gen_seq1_is_walk")
                                                                                        (("2"
                                                                                          (inst?)
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (assert)
                                                                                      (("2"
                                                                                        (skosimp*)
                                                                                        (("2"
                                                                                          (assert)
                                                                                          (("2"
                                                                                            (inst
                                                                                             +
                                                                                             "rev(w!1)")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "rev")
                                                                                              (("1"
                                                                                                (propax)
                                                                                                nil
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (rewrite
                                                                                               "walk?_rev")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "rev")
                                                                                                (("2"
                                                                                                  (ground)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (ground)
                                                                                    (("1"
                                                                                      (skosimp*)
                                                                                      (("1"
                                                                                        (case
                                                                                         "y!1 = x!2")
                                                                                        (("1"
                                                                                          (replace
                                                                                           -1)
                                                                                          (("1"
                                                                                            (hide
                                                                                             -1)
                                                                                            (("1"
                                                                                              (inst
                                                                                               +
                                                                                               "gen_seq1(G!1,x!2)")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "gen_seq1")
                                                                                                (("1"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (rewrite
                                                                                                 "gen_seq1_is_walk")
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (lemma
                                                                                           "walk_merge")
                                                                                          (("2"
                                                                                            (inst
                                                                                             -1
                                                                                             "G!1"
                                                                                             "w!1"
                                                                                             "w!2"
                                                                                             "x!2"
                                                                                             "y!1"
                                                                                             "x!1")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "walk_from?")
                                                                                              (("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (skosimp*)
                                                                                                  (("2"
                                                                                                    (inst
                                                                                                     +
                                                                                                     "p!1")
                                                                                                    (("2"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (replace
                                                                                       -1)
                                                                                      (("2"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("2"
                                                                    (hide
                                                                     3
                                                                     4)
                                                                    (("2"
                                                                      (case
                                                                       "disjoint?(vert(H),vert(K))")
                                                                      (("1"
                                                                        (hide
                                                                         -2
                                                                         -3
                                                                         -4
                                                                         -5
                                                                         -6)
                                                                        (("1"
                                                                          (expand
                                                                           "disjoint?")
                                                                          (("1"
                                                                            (expand
                                                                             "intersection")
                                                                            (("1"
                                                                              (expand
                                                                               "empty?")
                                                                              (("1"
                                                                                (expand
                                                                                 "member")
                                                                                (("1"
                                                                                  (inst-cp
                                                                                   -1
                                                                                   "x!2")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -1
                                                                                     "y!1")
                                                                                    (("1"
                                                                                      (case
                                                                                       "vert(G!1) = union(vert(H),vert(K))")
                                                                                      (("1"
                                                                                        (typepred
                                                                                         "y!1")
                                                                                        (("1"
                                                                                          (typepred
                                                                                           "x!2")
                                                                                          (("1"
                                                                                            (expand
                                                                                             "union")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "member")
                                                                                              (("1"
                                                                                                (replace
                                                                                                 -3)
                                                                                                (("1"
                                                                                                  (hide
                                                                                                   -3)
                                                                                                  (("1"
                                                                                                    (beta)
                                                                                                    (("1"
                                                                                                      (flatten)
                                                                                                      (("1"
                                                                                                        (ground)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (hide
                                                                                         -1
                                                                                         2
                                                                                         3
                                                                                         4
                                                                                         5
                                                                                         6)
                                                                                        (("2"
                                                                                          (reveal
                                                                                           -4)
                                                                                          (("2"
                                                                                            (replace
                                                                                             -1)
                                                                                            (("2"
                                                                                              (hide
                                                                                               -1)
                                                                                              (("2"
                                                                                                (grind)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide
                                                                         -1
                                                                         -2
                                                                         -6
                                                                         2
                                                                         3
                                                                         4)
                                                                        (("2"
                                                                          (replace
                                                                           -1
                                                                           *
                                                                           rl)
                                                                          (("2"
                                                                            (hide
                                                                             -1)
                                                                            (("2"
                                                                              (replace
                                                                               -1
                                                                               *
                                                                               rl)
                                                                              (("2"
                                                                                (hide
                                                                                 -1)
                                                                                (("2"
                                                                                  (replace
                                                                                   -1
                                                                                   *
                                                                                   rl)
                                                                                  (("2"
                                                                                    (hide
                                                                                     -1)
                                                                                    (("2"
                                                                                      (grind)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (skosimp*) (("3" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil graph_piece_path nil)
    (piece_connected? const-decl "bool" graph_conn_defs nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (Subgraph type-eq-decl nil subgraphs nil)
    (subgraph const-decl "Subgraph(G)" subgraphs nil)
    (walk?_rev formula-decl nil walks nil)
    (w!1 skolem-const-decl "Walk[T](G!1)" graph_piece_path nil)
    (rev const-decl "finseq[T]" doubletons nil)
    (walk_merge formula-decl nil walks nil)
    (p!1 skolem-const-decl "prewalk[T]" graph_piece_path nil)
    (x!2 skolem-const-decl "(vert(G!1))" graph_piece_path nil)
    (disjoint? const-decl "bool" sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (union const-decl "set" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (union const-decl "graph[T]" graph_ops nil)
    (union_edge_disj formula-decl nil graph_piece_path nil)
    (path_connected? const-decl "bool" graph_conn_defs nil)
    (intersection const-decl "set" sets nil)
    (gen_seq2 const-decl "Seq(G)" walks nil)
    (x!1 skolem-const-decl "T" graph_piece_path nil)
    (edge_to_walk formula-decl nil walks nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (G!1 skolem-const-decl "graph[T]" graph_piece_path nil)
    (w!1 skolem-const-decl "T" graph_piece_path nil)
    (O const-decl "finseq" finite_sequences nil)
    (verts_in? const-decl "bool" walks nil)
    (Seq type-eq-decl nil walks nil)
    (gen_seq1 const-decl "Seq(G)" walks nil)
    (w!2 skolem-const-decl "Walk[T](G!1)" graph_piece_path nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (dbl_comm formula-decl nil doubletons nil)
    (gen_seq1_is_walk formula-decl nil walks nil)
    (edge? const-decl "bool" graphs nil)
    (nil application-judgement "finite_set[T]" graph_piece_path nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (walk_from? const-decl "bool" walks nil)
    (walk_concat_edge formula-decl nil walks nil)
    (edg const-decl "doubleton[T]" graphs nil)
    (is_finite const-decl "bool" finite_sets nil)
    (difference const-decl "set" sets nil)
    (finite_difference application-judgement "finite_set" finite_sets
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (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)
    (prewalk type-eq-decl nil walks nil)
    (walk? const-decl "bool" walks nil)
    (Walk type-eq-decl nil walks nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (member const-decl "bool" sets nil))
   nil)))