$$$top.pvs
%-------------------------------------------------------------------------------
%
% Directed Graph Theory
%
%  Authors:
%
%      Jon Sjogren       AFOSR
%      Ricky W. Butler   NASA Langley
%
%  Version 2.0           Last modified 5/21/97
%                        UPDATED to PVS 2.2: 11/17/98
%
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        R.W.Butler@larc.nasa.gov
%
%  abstract_min          -- abstract definition of min
%  abstract_max          -- abstract definition of max
%  circuits              -- theory of circuits
%  pairs                 -- theory of pairs used for definition of edge
%  digraphs              -- fundamental definition of a digraph
%  digraph_conn_defs     -- defs of piece, path, and structural connectedness
%  digraph_deg           -- definition of degree
%  digraph_inductions    -- vertex and edge inductions for digraphs
%  digraph_ops           -- delete vertex and delete edge operations
%  dags,                 -- directed acyclic graphs
%  ind_paths             -- definition of independent paths
%  max_di_subgraphs       -- maximal di_subgraphs with specified property
%  max_subtrees          -- maximal subtrees with specified property
%  min_walk_reduced      -- theorem that minimum walk is reduced
%  min_walks             -- minimum walk satisfying a property
%  path_lems             -- some useful lemmas about paths
%  path_ops              -- deleting vertex and edge operations
%  paths                 -- fundamental definition and properties about paths
%  reduce_walks          -- operation to reduce a walk
%  sep_sets              -- definition of separating sets
%  di_subgraphs           -- generation of di_subgraphs from vertex sets
%  di_subgraphs_from_walk -- generation of di_subgraphs from walks
%  subtrees              -- subtrees of a digraph
%  trees                 -- fundamental definition of trees
%  walk_inductions       -- induction on length of a walk
%  walks                 -- fundamental definition and properties of walks
%
%-------------------------------------------------------------------------------
top: THEORY
BEGIN
   IMPORTING digraphs,
             digraph_deg,
             walks,
             paths,
             path_ops,
             dags,
             path_lems,
             circuits,
             di_subgraphs,
             di_subgraphs_from_walk,
             digraph_ops,
             max_di_subgraphs,
             max_subtrees,
             trees,
             subtrees,
             walk_inductions,
             min_walk_reduced,
             reduce_walks,
	     abstract_min      ,
	     abstract_max     ,
	     pairs        ,
	     digraph_conn_defs   ,
	     digraph_inductions  ,
	     ind_paths         ,
	     min_walks,
	     sep_sets
%  digraph_deg_sum       -- theorem relating vertex degree and number of edges
%  tree_circ             -- theorem that tree has no circuits
%  digraph_connected     -- all connected defs are equivalent
%  ramsey_new            -- Ramsey's theorem
%  menger                -- menger's theorem
%  tree_paths            -- theorem that tree has only one path between vertices
%  circuit_deg           -- degree of circuits
%  cycle_deg             -- theorem about degree and existence of cycle
%  digraph_complected    -- unusual definition of connected digraph
%  digraph_conn_piece    -- structural connected ==> piece connected
%  digraph_path_conn     -- path connected ==> structural connected
%  digraph_piece_path    -- piece connected ==> path connected
%  h_menger              -- hard menger
%  meng_scaff            -- scaffolding for hard menger proof
%  meng_scaff_defs       -- scaffolding for hard menger proof
%  meng_scaff_prelude    -- scaffolding for hard menger proof
%  sep_set_lems          -- properties of separating sets
%            digraph_deg_sum,
%            tree_circ,
%            digraph_connected,
%            ramsey_new,
%            menger,
%            tree_paths,         % Proof incorrect
%            circuit_deg,
%	     cycle_deg,          % not attempted yet
%	     digraph_complected  ,
%	     digraph_conn_piece  ,
%	     digraph_connected   ,
%	     digraph_path_conn   ,
%	     digraph_piece_path  ,
%	     h_menger          ,
%	     meng_scaff        ,
%	     meng_scaff_defs   ,
%	     meng_scaff_prelude,
%	     menger            ,
%	     sep_set_lems      ,
END top
$$$ind_paths.pvs
ind_paths[T: TYPE]: THEORY
BEGIN
   IMPORTING paths[T]
   G: VAR digraph[T]
   u,v,s,t: VAR T
   e: VAR edgetype[T]
   V: VAR finite_set[T]
   n: VAR nat
   independent?(w1,w2: prewalk): bool =
                       (FORALL (i,j: nat): i > 0 AND i < l(w1) - 1 AND
                                           j > 0 AND j < l(w2) - 1 IMPLIES
                                    seq(w1)(i) /= seq(w2)(j))
   p1,p2: VAR prewalk
   independent?_comm: LEMMA independent?(p1,p2) IMPLIES
                                    independent?(p2,p1)
   independent_ne: LEMMA l(p1) > 2 AND independent?(p1,p2) IMPLIES p1 /= p2
   ps: VAR prewalk
   IMPORTING finite_sets
   set_of_paths(G,s,t): TYPE = finite_set[Path_from(G,s,t)]
   ind_path_set?(G,s,t,(pset: set_of_paths(G,s,t))): bool =
                   (FORALL (p1,p2: Path_from(G,s,t)):
                             pset(p1) AND pset(p2) AND  p1 /= p2
                                         IMPLIES independent?(p1,p2))
   ind_path_set_2: LEMMA FORALL (ips: set_of_paths(G,s,t)):
                                    card(ips) = 2 AND
                                    ind_path_set?(G, s, t, ips)
                              IMPLIES
                         (EXISTS (P_1,P_2: prewalk): path_from?(G, P_1, s, t) AND
                                                    path_from?(G, P_2, s, t) AND
                                                      independent?(P_1,P_2) )
   internal_verts(w: prewalk): finite_set[T] =
               {t: T | (EXISTS (i: nat): i > 0 AND i < l(w) - 1 AND w(i) = t)}
   indep?(w1,w2: prewalk): bool = empty?(intersection(internal_verts(w1),
                                                      internal_verts(w2)))
   w1,w2: VAR prewalk
   indep?_lem: LEMMA indep?(w1,w2) IFF independent?(w1,w2)
END ind_paths
$$$ind_paths.prf
(|ind_paths| (|independent?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|independent?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|independent?_comm| "" (SKOSIMP*)
  (("" (EXPAND "independent?")
    (("" (SKOSIMP*) (("" (INST -1 "j!1" "i!1") (("" (ASSERT) NIL)))))))))
 (|independent_ne| "" (SKOSIMP*)
  (("" (EXPAND "independent?")
    (("" (REPLACE -3)
      (("" (HIDE -3) (("" (INST - "1" "1") (("" (ASSERT) NIL)))))))))))
 (|ind_path_set_2| "" (SKOSIMP*)
  (("" (LEMMA "card_2_has_2[Path_from(G!1,s!1,t!1)]")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SKOSIMP*)
          (("" (INST 2 "x!1" "y!1")
            (("" (EXPAND "ind_path_set?")
              (("" (INST?)
                (("" (ASSERT)
                  (("" (EXPAND "path_from?")
                    (("" (PROPAX) NIL)))))))))))))))))))))
 (|internal_verts_TCC1| "" (SUBTYPE-TCC) NIL)
 (|internal_verts_TCC2| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[T]")
    (("" (INST?)
      (("1" (ASSERT)
        (("1" (INST - "verts_of(w!1)")
          (("1" (ASSERT) (("1" (HIDE 2) (("1" (GRIND) NIL)))))))))
       ("2" (HIDE 2) (("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))))))
 (|indep?_lem| "" (SKOSIMP*)
  (("" (EXPAND "indep?")
    (("" (EXPAND "independent?")
      (("" (PROP)
        (("1" (SKOSIMP*)
          (("1" (EXPAND "empty?")
            (("1" (EXPAND "member")
              (("1" (EXPAND "intersection")
                (("1" (EXPAND "internal_verts")
                  (("1" (EXPAND "member")
                    (("1" (EXPAND "fseq")
                      (("1" (INST - "seq(w1!1)(i!1)")
                        (("1" (PROP)
                          (("1" (INST?) (("1" (ASSERT) NIL)))
                           ("2" (INST + "j!1") (("2" (ASSERT) NIL)))))
                         ("2" (ASSERT) NIL)))))))))))))))))
         ("2" (EXPAND "empty?")
          (("2" (EXPAND "intersection")
            (("2" (EXPAND "internal_verts")
              (("2" (EXPAND "member")
                (("2" (EXPAND "fseq")
                  (("2" (SKOSIMP*)
                    (("2" (INST - "i!1" "i!2")
                      (("2" (ASSERT) NIL))))))))))))))))))))))))
$$$digraph_inductions.pvs
digraph_inductions[T: TYPE]: THEORY
BEGIN
  IMPORTING digraphs[T]
  G,GG,GGG: VAR digraph[T]
  P: VAR pred[digraph[T]]
  n: VAR nat
  size_prep              : LEMMA (FORALL G : P(G)) IFF
                                      (FORALL n, G : size(G) = n IMPLIES P(G))
  digraph_induction_vert    : THEOREM (FORALL G:
                                (FORALL GG: size(GG) < size(G) IMPLIES P(GG))
                                                IMPLIES P(G))
                                  IMPLIES (FORALL G: P(G))
  digraph_induction_vert_not: THEOREM (FORALL G: P(G)
                               IMPLIES
                             (EXISTS GG: size(GG) < size(G) AND
                                            P(GG)))
                           IMPLIES (FORALL G: NOT P(G))
  IMPORTING digraph_ops[T]
  num_edges_prep         : LEMMA (FORALL G : P(G)) IFF
                                   (FORALL n, G : num_edges(G) = n IMPLIES P(G))
  digraph_induction_edge   : THEOREM (FORALL G:
                          (FORALL GG: num_edges(GG) < num_edges(G) IMPLIES P(GG))
                                                IMPLIES P(G))
                                  IMPLIES (FORALL G: P(G))
END digraph_inductions
$$$digraph_inductions.prf
(|digraph_inductions| (|size_prep| "" (GRIND) NIL)
 (|digraph_induction_vert| "" (SKOSIMP)
  (("" (REWRITE "size_prep" +)
    (("" (INDUCT "n" 1 "NAT_induction")
      (("" (SKOSIMP*)
        (("" (INST -3 "G!1")
          (("" (SPLIT -3)
            (("1" (PROPAX) NIL)
             ("2" (SKOSIMP*)
              (("2" (INST -2 "size(GG!1)")
                (("2" (ASSERT)
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|digraph_induction_vert_not| "" (SKOSIMP*)
  (("" (LEMMA "digraph_induction_vert")
    (("" (INST -1 "(LAMBDA (GG: digraph[T]): NOT P!1(GG))")
      (("" (BETA)
        (("" (PROP)
          (("1" (INST?) NIL)
           ("2" (SKOSIMP*)
            (("2" (INST -3 "G!2")
              (("2" (ASSERT)
                (("2" (SKOSIMP*)
                  (("2" (INST -1 "GG!1")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|num_edges_prep| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (SKOSIMP*) (("1" (INST?) NIL)))
     ("2" (SKOSIMP*)
      (("2" (INST?)
        (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))
 (|digraph_induction_edge| "" (SKOSIMP)
  (("" (REWRITE "num_edges_prep" +)
    (("" (INDUCT "n" 1 "NAT_induction")
      (("" (SKOSIMP*)
        (("" (INST -3 "G!1")
          (("" (SPLIT -3)
            (("1" (PROPAX) NIL)
             ("2" (SKOSIMP*)
              (("2" (INST -2 "num_edges(GG!1)")
                (("2" (ASSERT)
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|digraph_induction_both| "" (SKOSIMP*)
  (("" (INST?)
    (("" (PROP)
      (("1" (LEMMA "digraph_induction_edge")
        (("1" (INST -1 "P!1")
          (("1" (SPLIT -1)
            (("1" (INST?) NIL) ("2" (SKOSIMP*) (("2" (POSTPONE) NIL)))))))))
       ("2" (POSTPONE) NIL))))))))
$$$abstract_max.pvs
abstract_max[T: TYPE, N: nat, size: [T -> upto[N]], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
%  The need for a function that returns the largest object that
%  satisfies a particular predicate arises in many contexts.  Thus it is
%  useful to develop an "abstract" max theory that can be instantiated in
%  multiple ways to provide different max functions.  Such a theory must
%  be parameterized by
%
%    -------------------------------------------------------------------------
%    | T: TYPE          | the base type over which max is defined            |
%    | size:[T -> nat]  | the size function by which objects are compared    |
%    | P: pred[T]       | the property that the max function must satisfy    |
%    -------------------------------------------------------------------------
%
%  Author:
%
%      Ricky W. Butler   NASA Langley
%
%  Version 2.0           Last modified 10/21/97
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        R.W.Butler@larc.nasa.gov
%
%------------------------------------------------------------------------------
BEGIN
   ASSUMING
   T_ne: ASSUMPTION EXISTS (t: T): P(t)
   ENDASSUMING
   IMPORTING max_upto
   TP: TYPE = {t: T | P(t)}
   n: VAR upto[N]
   S,SS: VAR T
   is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)
   prep0: LEMMA nonempty?({n: upto[N] | is_one(n)})
   max_f: upto[N] = max({n: upto[N] | is_one(n)})
   prep1: LEMMA nonempty?({S: T | size(S) = max_f AND P(S)})
   maximal?(S): bool = P(S) AND
                       (FORALL (SS: T): P(SS) IMPLIES size(S) >= size(SS))
   max: {S: T | maximal?(S)}
   max_def: LEMMA maximal?(max)
   max_in : LEMMA P(max)
   max_is_max: LEMMA P(SS) IMPLIES size(max) >= size(SS)
END abstract_max
$$$abstract_max.prf
(|abstract_max|
 (|prep0| "" (LEMMA "T_ne")
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (SKOSIMP*)
        (("" (EXPAND "member")
          (("" (EXPAND "is_one")
            (("" (INST -2 "size(t!1)") (("" (INST 1 "t!1") (("" (ASSERT) NIL)))))))))))))))))
 (|max_f_TCC1| "" (LEMMA "prep0") (("" (PROPAX) NIL)))
 (|prep1| "" (EXPAND "nonempty?")
  (("" (EXPAND "empty?")
    (("" (EXPAND "member")
      (("" (EXPAND "max_f")
        (("" (TYPEPRED "max({n: upto[N] | is_one(n)})")
          (("1" (EXPAND "is_one")
            (("1" (SKOSIMP*) (("1" (INST -5 "S!1") (("1" (ASSERT) NIL)))))))
           ("2" (REWRITE "prep0") NIL)))))))))))
 (|max_TCC1| "" (LEMMA "prep1")
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (SKOSIMP*)
        (("" (EXPAND "member")
          (("" (INST?)
            (("" (EXPAND "maximal?")
              (("" (FLATTEN)
                (("" (ASSERT)
                  (("" (SKOSIMP*)
                    (("" (EXPAND "max_f")
                      (("" (REPLACE -2)
                        (("" (HIDE -2)
                          (("" (TYPEPRED "max({n: upto[N] | is_one(n)})")
                            (("1" (INST -3 "size(SS!1)")
                              (("1" (ASSERT)
                                (("1" (EXPAND "is_one") (("1" (INST?) (("1" (ASSERT) NIL)))))))))
                             ("2" (LEMMA "prep0")
                              (("2" (PROPAX) NIL)))))))))))))))))))))))))))))))
 (|max_def| "" (TYPEPRED "max") (("" (PROPAX) NIL)))
 (|max_in| "" (TYPEPRED "max") (("" (EXPAND "maximal?") (("" (FLATTEN) (("" (PROPAX) NIL)))))))
 (|max_is_max| "" (SKOSIMP*)
  (("" (TYPEPRED "max")
    (("" (EXPAND "maximal?") (("" (FLATTEN) (("" (INST?) (("" (ASSERT) NIL))))))))))))
$$$reduce_walks.pvs
reduce_walks[T: TYPE]: THEORY
BEGIN
   IMPORTING paths[T]
   G: VAR digraph[T]
   Long_walk(G): TYPE = {w: Walk(G) | l(w) > 3}
   reduce(G: digraph[T], w: Long_walk(G),
          k: {n: nat | n > 0 AND n < l(w)-1}): Walk(G) =
                      IF w(k-1) = w(k+1) THEN
                          (# l := l(w) - 2,
                          seq := (LAMBDA (i: below(l(w)-2)):
                                     IF i < k THEN w(i)
                                     ELSE w(i+2)
                                     ENDIF) #)
                      ELSE
                          w
                      ENDIF
   reduce_lem: LEMMA FORALL (w: Walk(G),
                            k: {n: nat | n > 0 AND n < l(w)-1}):
       w(k-1) = w(k+1) AND l(w) > 3 IMPLIES
          reduce(G,w,k) = w^(0,k-1) o w^(k+2,l(w)-1)
END reduce_walks
$$$reduce_walks.prf
(|reduce_walks| (|reduce_TCC1| "" (SUBTYPE-TCC) NIL)
 (|reduce_TCC2| "" (SUBTYPE-TCC) NIL)
 (|reduce_TCC3| "" (SUBTYPE-TCC) NIL)
 (|reduce_TCC4| "" (SUBTYPE-TCC) NIL)
 (|reduce_TCC5| "" (SUBTYPE-TCC) NIL)
 (|reduce_TCC6| "" (SKOSIMP*)
  (("" (EXPAND "fseq") (("" (GRIND) NIL)))))
 (|reduce_TCC7| "" (SKOSIMP*)
  (("" (EXPAND "fseq")
    (("" (TYPEPRED "w!1")
      (("" (EXPAND "walk?")
        (("" (EXPAND "fseq")
          (("" (FLATTEN)
            (("" (SPLIT +)
              (("1" (HIDE -3)
                (("1" (EXPAND "verts_in?")
                  (("1" (SKOSIMP*)
                    (("1" (GROUND)
                      (("1" (INST?) NIL) ("2" (INST?) NIL)))))))))
               ("2" (SKOSIMP*)
                (("2" (LIFT-IF)
                  (("2" (TYPEPRED "k!1")
                    (("2" (LIFT-IF)
                      (("2" (GROUND)
                        (("1" (INST?) (("1" (ASSERT) NIL)))
                         ("2" (CASE-REPLACE "k!1=n!1+1")
                          (("1" (ASSERT)
                            (("1" (REPLACE -10)
                              (("1"
                                (HIDE -10)
                                (("1"
                                  (INST?)
                                  (("1" (ASSERT) NIL)))))))))
                           ("2" (ASSERT) NIL)))
                         ("3" (INST?)
                          (("3" (ASSERT) NIL)))))))))))))))))))))))))))
 (|reduce_lem_TCC1| "" (SUBTYPE-TCC) NIL)
 (|reduce_lem_TCC2| "" (SUBTYPE-TCC) NIL)
 (|reduce_lem_TCC3| "" (SUBTYPE-TCC) NIL)
 (|reduce_lem_TCC4| "" (SUBTYPE-TCC) NIL)
 (|reduce_lem| "" (SKOSIMP*)
  (("" (EXPAND "o ")
    (("" (EXPAND "^")
      (("" (AUTO-REWRITE "fseq")
        (("" (TYPEPRED "k!1")
          (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
            (("1" (EXPAND "reduce")
              (("1" (LIFT-IF) (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))
             ("2" (EXPAND "emptyseq")
              (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                (("1" (TYPEPRED "x!1")
                  (("1" (LIFT-IF) (("1" (GRIND) NIL)))))
                 ("2" (SKOSIMP*)
                  (("2" (EXPAND "^")
                    (("2" (EXPAND "emptyseq")
                      (("2" (EXPAND "reduce")
                        (("2" (LIFT-IF)
                          (("2" (EXPAND "fseq")
                            (("2" (GROUND) NIL)))))))))))))
                 ("3" (SKOSIMP*)
                  (("3" (TYPEPRED "n!1")
                    (("1" (EXPAND "^")
                      (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
                     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))
                 ("4" (SKOSIMP*)
                  (("4" (TYPEPRED "n!1")
                    (("1" (EXPAND "^")
                      (("1" (EXPAND "emptyseq")
                        (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))
                     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))
                 ("5" (SKOSIMP*)
                  (("5" (TYPEPRED "n!1")
                    (("1" (EXPAND "^")
                      (("1" (LIFT-IF) (("1" (GROUND) NIL)))))
                     ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))))))
                 ("6" (SKOSIMP*)
                  (("6" (TYPEPRED "n!1")
                    (("1" (EXPAND "reduce")
                      (("1" (EXPAND "fseq")
                        (("1" (EXPAND "^")
                          (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))))
                     ("2" (SKOSIMP*)
                      (("2" (ASSERT) (("2" (ASSERT) NIL)))))))))))))
             ("3" (SKOSIMP*) (("3" (EXPAND "^") (("3" (PROPAX) NIL)))))
             ("4" (SKOSIMP*)
              (("4" (TYPEPRED "n!1")
                (("4" (EXPAND "^")
                  (("4" (EXPAND "emptyseq")
                    (("4" (LIFT-IF) (("4" (GROUND) NIL)))))))))))
             ("5" (SKOSIMP*)
              (("5" (TYPEPRED "n!1")
                (("5" (EXPAND "^")
                  (("5" (EXPAND "emptyseq")
                    (("5" (LIFT-IF) (("5" (GROUND) NIL)))))))))))
             ("6" (SKOSIMP*)
              (("6" (TYPEPRED "n!1")
                (("6" (EXPAND "^")
                  (("6" (LIFT-IF)
                    (("6" (EXPAND "emptyseq")
                      (("6" (GROUND) NIL)))))))))))
             ("7" (SKOSIMP*)
              (("7" (TYPEPRED "n!1")
                (("7" (EXPAND "^") (("7" (PROPAX) NIL)))))))
             ("8" (LIFT-IF) (("8" (GROUND) NIL))))))))))))))))
$$$min_walks.pvs
min_walks[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T]
   IMPORTING walks[T], abstract_min
   v1,v2,x,y: VAR T
   G: VAR digraph[T]
   gr_walk(v1,v2): TYPE = {G: digraph[T] | vert(G)(v1) AND vert(G)(v2) AND
                                         (EXISTS (w: Seq(G)):
                                           walk_from?(G,w,v1,v2))}
   min_walk_from(x,y,(Gw:gr_walk(x,y))): Walk(Gw) =
                        min[Seq(Gw),(LAMBDA (w: Seq(Gw)): l(w)),
                                (LAMBDA (w: Seq(Gw)): walk_from?(Gw,w,x,y))]
   is_min(G,(w: Seq(G)),x,y): bool = walk?(G,w) AND
                       (FORALL (ww: Seq(G)): walk_from?(G,ww,x,y) IMPLIES
                                                        l(w) <= l(ww))
   min_walk_def: LEMMA FORALL (Gw: gr_walk(x,y)):
                          walk_from?(Gw,min_walk_from(x,y,Gw),x,y) AND
                          is_min(Gw, min_walk_from(x,y,Gw),x,y)
   min_walk_in : LEMMA FORALL (Gw: gr_walk(x,y)):
                          walk_from?(Gw,min_walk_from(x,y,Gw),x,y)
   min_walk_is_min: LEMMA FORALL (Gw: gr_walk(x,y), ww: Seq(Gw)):
                              walk_from?(Gw,ww,x,y) IMPLIES
                                        l(min_walk_from(x,y,Gw)) <= l(ww)
END min_walks
$$$min_walks.prf
(|min_walks|
 (|min_walk_from_TCC1| "" (SKOSIMP*)
  (("" (TYPEPRED "Gw!1") (("" (PROPAX) NIL)))))
 (|min_walk_from_TCC2| "" (SKOSIMP*)
  (("" (TYPEPRED "Gw!1")
    (("" (HIDE -1 -2 -3 -4)
      ((""
        (LEMMA "min_in[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): l(w)),
                   (LAMBDA (w: Seq(Gw!1)): walk_from?(Gw!1, w, x!1, y!1))]")
        (("1" (BETA)
          (("1" (EXPAND "walk_from?")
            (("1" (FLATTEN) (("1" (PROPAX) NIL)))))))
         ("2" (HIDE 2) (("2" (TYPEPRED "Gw!1") (("2" (PROPAX) NIL)))))))))))))
 (|min_walk_def_TCC1| "" (SUBTYPE-TCC) NIL)
 (|min_walk_def| "" (SKOSIMP*)
  (("" (TYPEPRED "min_walk_from(x!1, y!1,Gw!1)")
    (("" (PROP)
      (("1"
        (LEMMA "min_in[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): l(w)),
                (LAMBDA (w: Seq(Gw!1)):
                   walk_from?(Gw!1, w, x!1, y!1))]")
        (("1" (HIDE -2 -3 -4)
          (("1" (BETA)
            (("1" (EXPAND "min_walk_from") (("1" (PROPAX) NIL)))))))
         ("2" (HIDE -1 -2 -3 2)
          (("2" (TYPEPRED "Gw!1") (("2" (PROPAX) NIL)))))))
       ("2"
        (LEMMA "min_is_min[Seq(Gw!1), (LAMBDA (w: Seq(Gw!1)): l(w)),
                (LAMBDA (w: Seq(Gw!1)):
                   walk_from?(Gw!1, w, x!1, y!1))]")
        (("1" (HIDE -3 -4)
          (("1" (EXPAND "is_min")
            (("1" (ASSERT)
              (("1" (SKOSIMP*)
                (("1" (INST?)
                  (("1" (ASSERT)
                    (("1" (EXPAND "min_walk_from")
                      (("1" (PROPAX) NIL)))))))))))))))
         ("2" (HIDE -1 -2 -3 2)
          (("2" (TYPEPRED "Gw!1") (("2" (PROPAX) NIL)))))))))))))
 (|min_walk_in| "" (SKOSIMP*)
  (("" (LEMMA "min_walk_def")
    (("" (INST?) (("" (FLATTEN) (("" (PROPAX) NIL)))))))))
 (|min_walk_is_min| "" (SKOSIMP*)
  (("" (LEMMA "min_walk_def")
    (("" (INST?)
      (("" (FLATTEN)
        (("" (HIDE -1)
          (("" (EXPAND "is_min")
            (("" (FLATTEN) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))
$$$min_walk_reduced.pvs
min_walk_reduced[T: TYPE]: THEORY
BEGIN
   IMPORTING min_walks[T], path_ops[T]
   reduced?(G: digraph[T], w: Seq(G)): bool =
          (FORALL (k: nat): k > 0 AND k < l(w) - 1 IMPLIES w(k-1) /= w(k+1))
   x,y: VAR T
   i: VAR nat
   min_walk_vert: LEMMA FORALL (Gw: gr_walk(x,y)): i < l(min_walk_from(x,y,Gw))
                               IMPLIES vert(Gw)(min_walk_from(x,y,Gw)(i))
   min_walk_is_reduced: LEMMA FORALL (Gw: gr_walk(x,y)):
                                     reduced?(Gw,min_walk_from(x,y,Gw))
END min_walk_reduced
$$$min_walk_reduced.prf
(|min_walk_reduced| (|reduced?_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|reduced?_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|min_walk_vert| "" (SKOSIMP*)
  (("" (EXPAND "fseq")
    (("" (LEMMA "min_walk_in")
      (("" (INST?)
        (("" (EXPAND "walk_from?")
          (("" (FLATTEN)
            (("" (EXPAND "walk?")
              (("" (FLATTEN)
                (("" (HIDE -4)
                  (("" (EXPAND "verts_in?")
                    (("" (INST -3 "i!1") NIL)))))))))))))))))))))
 (|min_walk_is_reduced_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?")
    (("" (SKOSIMP*)
      (("" (LEMMA "min_walk_vert")
        (("" (INST?) (("" (INST?) (("" (EXPAND "fseq") (("" (PROPAX) NIL)))))))))))))))
 (|min_walk_is_reduced| "" (SKOSIMP*)
  (("" (EXPAND "reduced?")
    (("" (EXPAND "fseq")
      (("" (SKOSIMP*)
        (("" (NAME MIN_W "min_walk_from(x!1,y!1,Gw!1)")
          (("" (REPLACE -1)
            (("" (LEMMA "min_walk_is_min")
              (("" (INST?)
                (("" (LEMMA "min_walk_in")
                  (("" (INST?)
                    (("" (REPLACE -3)
                      (("" (EXPAND "walk_from?")
                        (("" (FLATTEN)
                          (("" (CASE "k!1 = l(MIN_W) - 2")
                            (("1" (REPLACE -1)
                              (("1" (HIDE -1)
                                (("1" (ASSERT)
                                  (("1" (NAME RED_W "MIN_W ^ (0, l(MIN_W) - 3)")
                                    (("1" (INST -5 "RED_W")
                                      (("1" (REPLACE -1 * RL)
                                        (("1" (HIDE -1)
                                          (("1" (EXPAND "^")
                                            (("1" (EXPAND "walk?")
                                              (("1" (FLATTEN)
                                                (("1"
                                                  (EXPAND "verts_in?")
                                                  (("1"
                                                    (SPLIT +)
                                                    (("1"
                                                      (SKOSIMP*)
                                                      (("1" (INST?) NIL)))
                                                     ("2"
                                                      (SKOSIMP*)
                                                      (("2"
                                                        (EXPAND "fseq")
                                                        (("2"
                                                          (HIDE -4)
                                                          (("2"
                                                            (INST -4 "n!1")
                                                            (("2"
                                                              (ASSERT)
                                                              NIL)))))))))))))))))))))))
                                       ("2" (PROP)
                                        (("1" (REPLACE -1 * RL)
                                          (("1" (HIDE -1)
                                            (("1" (EXPAND "^") (("1" (PROPAX) NIL)))))))
                                         ("2" (EXPAND "verts_in?")
                                          (("2" (SKOSIMP*)
                                            (("2" (REPLACE -1 * RL)
                                              (("2" (TYPEPRED "i!1")
                                                (("2"
                                                  (REPLACE -2 * RL)
                                                  (("2"
                                                    (HIDE -2)
                                                    (("2"
                                                      (EXPAND "^")
                                                      (("2"
                                                        (EXPAND "walk?")
                                                        (("2"
                                                          (FLATTEN)
                                                          (("2"
                                                            (HIDE -5)
                                                            (("2"
                                                              (EXPAND "verts_in?")
                                                              (("2"
                                                                (INST - "i!1")
                                                                (("2"
                                                                  (ASSERT)
                                                                  NIL)))))))))))))))))))))))))))))))))))))
                             ("2"
                              (INST -4
                               "MIN_W ^ (0, k!1 - 1) o MIN_W ^ (2 + k!1, l(MIN_W) - 1)")
                              (("1" (SPLIT -4)
                                (("1" (EXPAND "o ")
                                  (("1" (EXPAND "^")
                                    (("1" (EXPAND "emptyseq")
                                      (("1" (LIFT-IF)
                                        (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))))))
                                 ("2" (EXPAND "o ")
                                  (("2" (EXPAND "^")
                                    (("2" (LIFT-IF)
                                      (("2" (EXPAND "emptyseq")
                                        (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))
                                 ("3" (EXPAND "o ")
                                  (("3" (EXPAND "^")
                                    (("3" (EXPAND "emptyseq")
                                      (("3" (LIFT-IF)
                                        (("3" (LIFT-IF) (("3" (GROUND) NIL)))))))))))
                                 ("4" (LEMMA "walk?_cut")
                                  (("4" (INST?)
                                    (("1" (INST -1 "Gw!1" "x!1" "y!1")
                                      (("1" (ASSERT)
                                        (("1" (EXPAND "walk_from?")
                                          (("1" (PROPAX) NIL)))))))
                                     ("2" (ASSERT) NIL) ("3" (ASSERT) NIL)))))))
                               ("2" (SPLIT +)
                                (("1" (EXPAND "o ")
                                  (("1" (EXPAND "^")
                                    (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))
                                 ("2" (EXPAND "verts_in?")
                                  (("2" (SKOSIMP*)
                                    (("2" (TYPEPRED "i!1")
                                      (("1" (EXPAND "o ")
                                        (("1" (EXPAND "^")
                                          (("1" (LIFT-IF)
                                            (("1" (EXPAND "walk?")
                                              (("1" (FLATTEN)
                                                (("1"
                                                  (HIDE -5)
                                                  (("1"
                                                    (EXPAND "verts_in?")
                                                    (("1"
                                                      (GROUND)
                                                      (("1" (INST?) NIL)
                                                       ("2" (INST?) NIL)))))))))))))))))
                                       ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
                                       ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))))))
                               ("3" (ASSERT) NIL)
                               ("4" (ASSERT) NIL))))))))))))))))))))))))))))))))
$$$digraph_conn_defs.pvs
digraph_conn_defs[T: TYPE]: THEORY
BEGIN
   IMPORTING digraph_deg[T]
   G,G1,G2: VAR digraph[T]
   connected?(G): RECURSIVE bool = singleton?(G) OR
                                   (EXISTS (v: (vert(G))): deg(v,G) > 0
                                       AND connected?(del_vert(G,v)))
                  MEASURE size(G)
   IMPORTING walks[T]
   path_connected?(G): bool = NOT empty?(G) AND
                              (FORALL (x,y: (vert(G))): % x /= y IMPLIES
                                   (EXISTS (w: Walk(G)): seq(w)(0) = x AND
                                                         seq(w)(l(w)-1) = y))
   H1,H2: VAR digraph[T]
   piece_connected?(G): bool = NOT empty?(G) AND
                               (FORALL H1,H2: G = union(H1,H2) AND
                                         NOT empty?(H1) AND NOT empty?(H2)
                                  IMPLIES NOT empty?(intersection(vert(H1),
                                                                   vert(H2))))
   complected?(G): bool = IF isolated?(G) THEN singleton?(G)
                          ELSIF (EXISTS (v: (vert(G))): deg(v,G) = 1) THEN
                           (EXISTS (x: (vert(G))): deg(x,G) = 1 AND
                              connected?(del_vert(G,x)))
                          ELSE
                             (EXISTS (e: (edges(G))):
                              connected?(del_edge(G,e)))
                          ENDIF
END digraph_conn_defs
$$$digraph_conn_defs.prf
(|digraph_conn_defs|
 (|connected?_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "size_del_vert") (("" (ASSERT) NIL)))))
 (|path_connected?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path_connected?_TCC2| "" (SUBTYPE-TCC) NIL))
$$$subtrees.pvs
subtrees[T: TYPE]: THEORY
BEGIN
   IMPORTING max_subtrees[T], digraph_conn_defs[T]
   G: VAR Digraph[T]    % not empty?(G)
   S: VAR digraph[T]
   n: VAR nat
   walk_acr: LEMMA FORALL (w: Walk(G)): n < l(w) AND
                                vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
                               IMPLIES
                    (EXISTS (j: posnat): (j <= n
                        AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))
   walk_acr2: LEMMA FORALL (w: Walk(G)): n < l(w) AND
                                vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
                               IMPLIES
                    (EXISTS (j: posnat): (j <= n
                        AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))
    e: VAR edgetype[T]
    v,w: VAR T
    add_pair: LEMMA  vert(G)(v) AND v /= w AND
                 add((v, w), edges(G))(e)
              IMPLIES
                 LET (x,y) = e IN add(w, vert(G))(x) AND add(w, vert(G))(y)
    max_tree_all_verts: LEMMA path_connected?(G)   IMPLIES
                               vert(max_subtree(G)) = vert(G)
END subtrees
$$$subtrees.prf
(|subtrees| (|walk_acr_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk_acr_TCC2| "" (SUBTYPE-TCC) NIL)
 (|walk_acr_TCC3| "" (SUBTYPE-TCC) NIL)
 (|walk_acr| "" (INDUCT "n" 1 "NAT_induction")
  (("1" (SKOSIMP*)
    (("1" (INST -1 "j!1-1")
      (("1" (ASSERT)
        (("1" (INST?)
          (("1" (ASSERT)
            (("1" (SPLIT -1)
              (("1" (SKOSIMP*)
                (("1" (INST 3 "j!2") (("1" (ASSERT) NIL)))))
               ("2" (ASSERT)
                (("2" (INST 2 "j!1") (("2" (ASSERT) NIL)))))))))))))
       ("2" (ASSERT) NIL)))))
   ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
   ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
 (|walk_acr2| "" (INDUCT "n" 1 "NAT_induction")
  (("1" (SKOSIMP*)
    (("1" (INST -1 "j!1-1")
      (("1" (ASSERT)
        (("1" (INST?)
          (("1" (ASSERT)
            (("1" (SPLIT -1)
              (("1" (SKOSIMP*)
                (("1" (INST 3 "j!2") (("1" (ASSERT) NIL)))))
               ("2" (INST 2 "j!1") (("2" (ASSERT) NIL)))))))))))
       ("2" (ASSERT) NIL)))))
   ("2" (SKOSIMP*) (("2" (ASSERT) NIL)))
   ("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))
 (|add_pair| "" (SKOSIMP*)
  (("" (EXPAND "add")
    (("" (EXPAND "member")
      (("" (SPLIT -2)
        (("1" (REPLACE -1 * RL) (("1" (HIDE -1) (("1" (GROUND) NIL)))))
         ("2" (TYPEPRED "G!1")
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (FLATTEN) (("2" (ASSERT) NIL)))))))))))))))))
 (|max_tree_all_verts| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
    (("" (IFF 1)
      (("" (PROP)
        (("1" (HIDE -2)
          (("1" (LEMMA "max_subtree_di_subgraph")
            (("1" (INST?)
              (("1" (EXPAND "di_subgraph?")
                (("1" (FLATTEN)
                  (("1" (HIDE -2)
                    (("1" (EXPAND "subset?")
                      (("1" (INST?)
                        (("1" (EXPAND "member")
                          (("1" (ASSERT) NIL)))))))))))))))))))
         ("2" (LEMMA "max_subtree_tree")
          (("2" (INST?)
            (("2" (NAME "TR" "max_subtree(G!1)")
              (("2" (CASE "(EXISTS (v: T): vert(TR)(v))")
                (("1" (SKOSIMP*)
                  (("1" (EXPAND "path_connected?")
                    (("1" (FLATTEN)
                      (("1" (INST -5 "v!1" "x!1")
                        (("1" (ASSERT)
                          (("1" (SKOSIMP*)
                            (("1"
                              (CASE "(EXISTS (j: posnat): j < l(w!1) AND vert(TR)(w!1(j-1)) AND
	                               NOT vert(TR)(w!1(j)))")
                              (("1"
                                (EXPAND "fseq")
                                (("1"
                                  (SKOSIMP*)
                                  (("1"
                                    (TYPEPRED "w!1")
                                    (("1"
                                      (EXPAND "walk?")
                                      (("1"
                                        (EXPAND "verts_in?")
                                        (("1"
                                          (FLATTEN)
                                          (("1"
                                            (INST -1 "j!1-1")
                                            (("1"
                                              (ASSERT)
                                              (("1"
                                                (EXPAND "edge?")
                                                (("1"
                                                  (EXPAND "fseq")
                                                  (("1"
                                                    (NAME
                                                     "ss"
                                                     "seq(w!1)(j!1 - 1)")
                                                    (("1"
                                                      (NAME
                                                       "tt"
                                                       "seq(w!1)(j!1)")
                                                      (("1"
                                                        (NAME
                                                         "TP"
                                                         "(# vert := add(tt,vert(TR)),
                     edges := add((ss,tt),edges(TR)) #)")
                                                        (("1"
                                                          (CASE
                                                           "tree?(TP)")
                                                          (("1"
                                                            (LEMMA
                                                             "max_subtree_max")
                                                            (("1"
                                                              (INST
                                                               -1
                                                               "G!1"
                                                               "TP")
                                                              (("1"
                                                                (REPLACE
                                                                 -4)
                                                                (("1"
                                                                  (HIDE
                                                                   -2
                                                                   --4
                                                                   -5
                                                                   -6
                                                                   -7
                                                                   -8
                                                                   -9
                                                                   -10
                                                                   -11
                                                                   -13
                                                                   -14
                                                                   -15
                                                                   -16
                                                                   1
                                                                   3
                                                                   4)
                                                                  (("1"
                                                                    (REPLACE
                                                                     -2
                                                                     *
                                                                     RL)
                                                                    (("1"
                                                                      (HIDE
                                                                       -2)
                                                                      (("1"
                                                                        (EXPAND
                                                                         "size")
                                                                        (("1"
                                                                          (REWRITE
                                                                           "card_add[T]")
                                                                          (("1"
                                                                            (ASSERT)
                                                                            NIL)))))))))))))
                                                               ("2"
                                                                (PROP)
                                                                (("1"
                                                                  (SKOSIMP*)
                                                                  (("1"
                                                                    (LEMMA
                                                                     "add_pair")
                                                                    (("1"
                                                                      (INST?)
                                                                      (("1"
                                                                        (INST?)
                                                                        (("1"
                                                                          (ASSERT)
                                                                          (("1"
                                                                            (INST?)
                                                                            (("1"
                                                                              (REPLACE
                                                                               -4
                                                                               +
                                                                               RL)
                                                                              (("1"
                                                                                (ASSERT)
                                                                                NIL)))))))))
                                                                       ("2"
                                                                        (EXPAND
                                                                         "nonempty?")
                                                                        (("2"
                                                                          (EXPAND
                                                                           "empty?")
                                                                          (("2"
                                                                            (EXPAND
                                                                             "member")
                                                                            (("2"
                                                                              (INST
                                                                               -1
                                                                               "v!1")
                                                                              NIL)))))))))))))
                                                                 ("2"
                                                                  (REPLACE
                                                                   -4)
                                                                  (("2"
                                                                    (INST
                                                                     -6
                                                                     "j!1-1")
                                                                    (("2"
                                                                      (REPLACE
                                                                       -3)
                                                                      (("2"
                                                                        (HIDE
                                                                         -1
                                                                         -12
                                                                         3
                                                                         4)
                                                                        (("2"
                                                                          (REPLACE
                                                                           -1
                                                                           *
                                                                           RL)
                                                                          (("2"
                                                                            (HIDE
                                                                             -1)
                                                                            (("2"
                                                                              (EXPAND
                                                                               "di_subgraph?")
                                                                              (("2"
                                                                                (ASSERT)
                                                                                (("2"
                                                                                  (LEMMA
                                                                                   "max_subtree_di_subgraph")
                                                                                  (("2"
                                                                                    (INST?)
                                                                                    (("2"
                                                                                      (REPLACE
                                                                                       -10)
                                                                                      (("2"
                                                                                        (HIDE
                                                                                         -10)
                                                                                        (("2"
                                                                                          (EXPAND
                                                                                           "di_subgraph?")
                                                                                          (("2"
                                                                                            (FLATTEN)
                                                                                            (("2"
                                                                                              (SPLIT
                                                                                               1)
                                                                                              (("1"
                                                                                                (EXPAND
                                                                                                 "subset?")
                                                                                                (("1"
                                                                                                  (SKOSIMP*)
                                                                                                  (("1"
                                                                                                    (EXPAND
                                                                                                     "member")
                                                                                                    (("1"
                                                                                                      (EXPAND
                                                                                                       "add")
                                                                                                      (("1"
                                                                                                        (EXPAND
                                                                                                         "member")
                                                                                                        (("1"
                                                                                                          (SPLIT
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (INST?)
                                                                                                            (("1"
                                                                                                              (ASSERT)
                                                                                                              (("1"
                                                                                                                (REPLACE
                                                                                                                 -1)
                                                                                                                (("1"
                                                                                                                  (HIDE
                                                                                                                   -1)
                                                                                                                  (("1"
                                                                                                                    (REVEAL
                                                                                                                     -10)
                                                                                                                    (("1"
                                                                                                                      (INST?)
                                                                                                                      (("1"
                                                                                                                        (ASSERT)
                                                                                                                        NIL)))))))))))))
                                                                                                           ("2"
                                                                                                            (INST?)
                                                                                                            (("2"
                                                                                                              (ASSERT)
                                                                                                              NIL)))))))))))))))
                                                                                               ("2"
                                                                                                (EXPAND
                                                                                                 "subset?")
                                                                                                (("2"
                                                                                                  (EXPAND
                                                                                                   "member")
                                                                                                  (("2"
                                                                                                    (SKOSIMP*)
                                                                                                    (("2"
                                                                                                      (EXPAND
                                                                                                       "add")
                                                                                                      (("2"
                                                                                                        (EXPAND
                                                                                                         "member")
                                                                                                        (("2"
                                                                                                          (SPLIT
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (ASSERT)
                                                                                                            (("1"
                                                                                                              (HIDE
                                                                                                               -2)
                                                                                                              (("1"
                                                                                                                (INST?)
                                                                                                                (("1"
                                                                                                                  (REPLACE
                                                                                                                   -4)
                                                                                                                  (("1"
                                                                                                                    (ASSERT)
                                                                                                                    (("1"
                                                                                                                      (REPLACE
                                                                                                                       -1
                                                                                                                       +
                                                                                                                       RL)
                                                                                                                      (("1"
                                                                                                                        (PROPAX)
                                                                                                                        NIL)))))))))))))
                                                                                                           ("2"
                                                                                                            (INST
                                                                                                             -3
                                                                                                             "x!2")
                                                                                                            (("2"
                                                                                                              (ASSERT)
                                                                                                              NIL)))))))))))))))))))))))))))))))))))))))))))))))))))
                                                           ("2"
                                                            (REPLACE
                                                             -2)
                                                            (("2"
                                                              (REPLACE
                                                               -3)
                                                              (("2"
                                                                (EXPAND
                                                                 "tree?")
                                                                (("2"
                                                                  (FLATTEN)
                                                                  (("2"
                                                                    (HIDE
                                                                     1)
                                                                    (("2"
                                                                      (INST
                                                                       1
                                                                       "tt")
                                                                      (("1"
                                                                        (SPLIT
                                                                         1)
                                                                        (("1"
                                                                          (HIDE
                                                                           -11)
                                                                          (("1"
                                                                            (EXPAND
                                                                             "deg")
                                                                            (("1"
                                                                              (CASE-REPLACE
                                                                               "incident_edges(tt, TP) = singleton((ss,tt))")
                                                                              (("1"
                                                                                (REWRITE
                                                                                 "card_singleton")
                                                                                NIL)
                                                                               ("2"
                                                                                (HIDE
                                                                                 2)
                                                                                (("2"
                                                                                  (EXPAND
                                                                                   "incident_edges")
                                                                                  (("2"
                                                                                    (EXPAND
                                                                                     "singleton")
                                                                                    (("2"
                                                                                      (REPLACE
                                                                                       -1
                                                                                       *
                                                                                       RL)
                                                                                      (("2"
                                                                                        (HIDE
                                                                                         -1)
                                                                                        (("2"
                                                                                          (APPLY-EXTENSIONALITY
                                                                                           :HIDE?
                                                                                           T)
                                                                                          (("2"
                                                                                            (EXPAND
                                                                                             "add")
                                                                                            (("2"
                                                                                              (EXPAND
                                                                                               "member")
                                                                                              (("2"
                                                                                                (EXPAND
                                                                                                 "in?")
                                                                                                (("2"
                                                                                                  (IFF)
                                                                                                  (("2"
                                                                                                    (TYPEPRED
                                                                                                     "TR")
                                                                                                    (("2"
                                                                                                      (HIDE
                                                                                                       -1
                                                                                                       -2)
                                                                                                      (("2"
                                                                                                        (INST?)
                                                                                                        (("2"
                                                                                                          (GROUND)
                                                                                                          NIL)))))))))))))))))))))))))))))))))
                                                                         ("2"
                                                                          (REPLACE
                                                                           -1
                                                                           *
                                                                           RL)
                                                                          (("2"
                                                                            (CASE-REPLACE
                                                                             "del_vert[T]((# vert := add(tt, vert(TR)),
                           edges :=
                             add((ss, tt),
                                 edges(TR))
                           #),
                        tt) = TR")
                                                                            (("1"
                                                                              (ASSERT)
                                                                              NIL)
                                                                             ("2"
                                                                              (HIDE
                                                                               -11
                                                                               -12
                                                                               -13
                                                                               -14
                                                                               2
                                                                               5
                                                                               6)
                                                                              (("2"
                                                                                (APPLY-EXTENSIONALITY
                                                                                 1
                                                                                 :HIDE?
                                                                                 T)
                                                                                (("1"
                                                                                  (EXPAND
                                                                                   "del_vert")
                                                                                  (("1"
                                                                                    (APPLY-EXTENSIONALITY
                                                                                     1
                                                                                     :HIDE?
                                                                                     T)
                                                                                    (("1"
                                                                                      (EXPAND
                                                                                       "add")
                                                                                      (("1"
                                                                                        (EXPAND
                                                                                         "member")
                                                                                        (("1"
                                                                                          (IFF
                                                                                           1)
                                                                                          (("1"
                                                                                            (EXPAND
                                                                                             "in?")
                                                                                            (("1"
                                                                                              (TYPEPRED
                                                                                               "TR")
                                                                                              (("1"
                                                                                                (HIDE
                                                                                                 -1
                                                                                                 -2)
                                                                                                (("1"
                                                                                                  (INST?)
                                                                                                  (("1"
                                                                                                    (ASSERT)
                                                                                                    (("1"
                                                                                                      (GROUND)
                                                                                                      NIL)))))))))))))))))))))
                                                                                 ("2"
                                                                                  (EXPAND
                                                                                   "del_vert")
                                                                                  (("2"
                                                                                    (APPLY-EXTENSIONALITY
                                                                                     1
                                                                                     :HIDE?
                                                                                     T)
                                                                                    (("2"
                                                                                      (EXPAND
                                                                                       "remove")
                                                                                      (("2"
                                                                                        (EXPAND
                                                                                         "add")
                                                                                        (("2"
                                                                                          (EXPAND
                                                                                           "member")
                                                                                          (("2"
                                                                                            (IFF)
                                                                                            (("2"
                                                                                              (GROUND)
                                                                                              NIL)))))))))))))
                                                                                 ("3"
                                                                                  (SKOSIMP*)
                                                                                  (("3"
                                                                                    (LEMMA
                                                                                     "add_pair")
                                                                                    (("3"
                                                                                      (INST?)
                                                                                      (("1"
                                                                                        (ASSERT)
                                                                                        NIL)
                                                                                       ("2"
                                                                                        (EXPAND
                                                                                         "nonempty?")
                                                                                        (("2"
                                                                                          (EXPAND
                                                                                           "empty?")
                                                                                          (("2"
                                                                                            (EXPAND
                                                                                             "member")
                                                                                            (("2"
                                                                                              (INST
                                                                                               -1
                                                                                               "v!1")
                                                                                              NIL)))))))))))))))))
                                                                             ("3"
                                                                              (SKOSIMP*)
                                                                              (("3"
                                                                                (LEMMA
                                                                                 "add_pair")
                                                                                (("3"
                                                                                  (INST?)
                                                                                  (("1"
                                                                                    (ASSERT)
                                                                                    NIL)
                                                                                   ("2"
                                                                                    (EXPAND
                                                                                     "nonempty?")
                                                                                    (("2"
                                                                                      (EXPAND
                                                                                       "empty?")
                                                                                      (("2"
                                                                                        (EXPAND
                                                                                         "member")
                                                                                        (("2"
                                                                                          (INST
                                                                                           -1
                                                                                           "v!1")
                                                                                          NIL)))))))))))))))))))
                                                                       ("2"
                                                                        (REPLACE
                                                                         -1
                                                                         *
                                                                         RL)
                                                                        (("2"
                                                                          (ASSERT)
                                                                          (("2"
                                                                            (EXPAND
                                                                             "add")
                                                                            (("2"
                                                                              (PROPAX)
                                                                              NIL)))))))))))))))))))
                                                           ("3"
                                                            (SKOSIMP*)
                                                            (("3"
                                                              (REPLACE
                                                               -3
                                                               *
                                                               RL)
                                                              (("3"
                                                                (HIDE
                                                                 -3)
                                                                (("3"
                                                                  (ASSERT)
                                                                  (("3"
                                                                    (EXPAND
                                                                     "add")
                                                                    (("3"
                                                                      (EXPAND
                                                                       "member")
                                                                      (("3"
                                                                        (REPLACE
                                                                         -2
                                                                         *
                                                                         RL)
                                                                        (("3"
                                                                          (ASSERT)
                                                                          (("3"
                                                                            (TYPEPRED
                                                                             "TR")
                                                                            (("3"
                                                                              (HIDE
                                                                               -1
                                                                               -2)
                                                                              (("3"
                                                                                (INST?)
                                                                                (("3"
                                                                                  (GROUND)
                                                                                  (("1"
                                                                                    (REPLACE
                                                                                     -1
                                                                                     *
                                                                                     RL)
                                                                                    (("1"
                                                                                      (ASSERT)
                                                                                      NIL)))
                                                                                   ("2"
                                                                                    (REPLACE
                                                                                     -1
                                                                                     *
                                                                                     RL)
                                                                                    (("2"
                                                                                      (ASSERT)
                                                                                      NIL)))))))))))))))))))))))))))))))))))))))))
                                             ("2"
                                              (EXPAND "fseq")
                                              (("2"
                                                (LEMMA "walk_acr")
                                                (("2"
                                                  (INST
                                                   -1
                                                   "G!1"
                                                   "TR"
                                                   "l(w!1)-1"
                                                   "w!1")
                                                  (("2"
                                                    (ASSERT)
                                                    NIL)))))))))))))))))))))
                               ("2"
                                (EXPAND "fseq")
                                (("2"
                                  (LEMMA "walk_acr")
                                  (("2"
                                    (INST
                                     -1
                                     "G!1"
                                     "TR"
                                     "l(w!1)-1"
                                     "w!1")
                                    (("2"
                                      (ASSERT)
                                      (("2"
                                        (SKOSIMP*)
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (ASSERT)
                                            NIL)))))))))))))
                               ("3"
                                (SKOSIMP*)
                                (("3" (ASSERT) NIL)))))))))
                         ("2" (ASSERT)
                          (("2" (HIDE -4 2)
                            (("2" (REPLACE -2)
                              (("2"
                                (HIDE -2)
                                (("2"
                                  (TYPEPRED "TR")
                                  (("2"
                                    (HIDE -2 -3)
                                    (("2"
                                      (EXPAND "di_subgraph?")
                                      (("2"
                                        (FLATTEN)
                                        (("2"
                                          (HIDE -2)
                                          (("2"
                                            (EXPAND "subset?")
                                            (("2"
                                              (EXPAND "member")
                                              (("2"
                                                (INST?)
                                                (("2"
                                                  (ASSERT)
                                                  NIL)))))))))))))))))))))))))))))))))
                 ("2" (HIDE -4 2)
                  (("2" (REPLACE -1)
                    (("2" (HIDE -1)
                      (("2" (EXPAND "tree?")
                        (("2" (PROP)
                          (("1" (LEMMA "card_1_has_1[T]")
                            (("1" (INST?) (("1" (ASSERT) NIL)))))
                           ("2" (SKOSIMP*)
                            (("2" (HIDE -2 -3)
                              (("2"
                                (INST?)
                                (("2"
                                  (EXPAND "deg")
                                  (("2"
                                    (LEMMA "card_1_has_1[Dbl]")
                                    (("2"
                                      (ASSERT)
                                      NIL))))))))))))))))))))))))))))))))))))))
$$$doubletons.pvs
doubletons[T: TYPE]: THEORY
BEGIN
   x,y,z: VAR T
   dbl(x,y): set[T] = {t: T | t = x OR t = y}
   S: VAR set[T]
   doubleton?(S): bool = (EXISTS x,y: x /= y AND S = dbl(x,y))
   doubleton: TYPE = {S | EXISTS x,y: x /= y AND S = dbl(x,y)}
   Dbl: TYPE = doubleton
   dbl_comm: LEMMA dbl(x,y) = dbl(y,x)
   D: VAR doubleton
   doubleton_irreflexive  : LEMMA NOT doubleton?(dbl(x,x))
   doubleton_nonempty     : LEMMA nonempty?(D)
   doubleton_rest_nonempty: LEMMA nonempty?(rest(D))
   dbl_choose             : LEMMA choose(dbl(x,y)) = x or choose(dbl(x,y)) = y
   dbl_rest_choose        : LEMMA x /= y IMPLIES
                                  (choose(dbl(x,y)) /= choose(rest(dbl(x,y)))) AND
                                  (choose(rest(dbl(x,y))) = x
                                      OR choose(rest(dbl(x,y))) = y)
   dbl_to_pair(D) : {(x,y) | D = dbl(x,y)}
   dbl_def        : LEMMA dbl(PROJ_1(dbl_to_pair(D)), PROJ_2(dbl_to_pair(D))) = D
   dbl_in         : LEMMA D = dbl(x,y) IMPLIES D(x) AND D(y)
   dbl_not_in     : LEMMA D = dbl(x,y) AND z /= x AND z /= y IMPLIES NOT D(z)
   dbl_to_pair_lem        : LEMMA x /= y IMPLIES
                                   dbl_to_pair(dbl(x,y)) = (x,y) OR
                                   dbl_to_pair(dbl(x,y)) = (y,x)
   dbl_to_pair_inverse_l  : LEMMA dbl(dbl_to_pair(D)) = D
   dbl_proj               : LEMMA D(PROJ_1(dbl_to_pair(D))) AND
                                  D(PROJ_2(dbl_to_pair(D)))
   v: VAR T
   proj_dbl: LEMMA (PROJ_1(dbl_to_pair(D)) = v OR PROJ_2(dbl_to_pair(D)) = v)
                    IMPLIES D(v)
   dbl_eq: LEMMA dbl(x,y) = dbl(v,z) IMPLIES
                        (x = v AND y = z) OR (x = z AND y = v)
   IMPORTING finite_sets@finite_sets
   finite_dbl: LEMMA is_finite(dbl(x,y))
END doubletons
$$$doubletons.prf
(|doubletons|
 (|dbl_comm| "" (SKOSIMP*)
  (("" (EXPAND "dbl")
    (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
      (("" (IFF) (("" (GROUND) NIL)))))))))
 (|doubleton_irreflexive| "" (SKOSIMP*)
  (("" (EXPAND "doubleton?")
    (("" (SKOSIMP*)
      ((""
        (CASE "(FORALL (z:T): member(z,dbl(x!1, x!1)) = member(z,dbl(x!2, y!1)))")
        (("1" (INST-CP -1 "x!2")
          (("1" (INST -1 "y!1")
            (("1" (EXPAND "member")
              (("1" (EXPAND "dbl")
                (("1" (HIDE -3) (("1" (GROUND) NIL)))))))))))
         ("2" (SKOSIMP*)
          (("2" (EXPAND "member")
            (("2" (REPLACE -1) (("2" (PROPAX) NIL)))))))))))))))
 (|doubleton_nonempty| "" (GRIND) NIL)
 (|doubleton_rest_nonempty| "" (SKOLEM-TYPEPRED)
  (("" (SKOSIMP*)
    (("" (EXPAND "rest")
      (("" (REWRITE "doubleton_nonempty")
        (("" (EXPAND "nonempty?")
          (("" (ASSERT)
            (("" (PROP)
              (("" (EXPAND "empty?")
                (("" (EXPAND "remove")
                  (("" (EXPAND "member")
                    (("" (INST-CP - "x!1")
                      (("" (INST - "y!1")
                        (("" (REPLACE -1)
                          (("" (EXPAND "dbl")
                            (("" (ASSERT)
                              NIL)))))))))))))))))))))))))))))
 (|dbl_choose_TCC1| "" (SUBTYPE-TCC) NIL)
 (|dbl_choose| "" (SKOSIMP*)
  (("" (EXPAND "dbl")
    (("" (EXPAND "choose")
      (("" (ASSERT)
        (("" (LEMMA "epsilon_ax[T]")
          (("1" (INST?)
            (("1" (ASSERT)
              (("1" (INST + "x!1") (("1" (ASSERT) NIL)))))))
           ("2" (INST + "x!1") NIL)))))))))))
 (|dbl_rest_choose_TCC1| "" (SKOSIMP*)
  (("" (USE "doubleton_rest_nonempty")
    (("" (INST?) (("" (ASSERT) NIL)))))))
 (|dbl_rest_choose| "" (SKOSIMP*)
  (("" (EXPAND "rest")
    (("" (LEMMA "doubleton_nonempty")
      (("" (INST - "dbl(x!1, y!1)")
        (("1" (EXPAND "nonempty?")
          (("1" (ASSERT)
            (("1" (USE "dbl_choose")
              (("1" (GROUND)
                (("1" (REPLACE -2)
                  (("1" (EXPAND "remove")
                    (("1" (EXPAND "member") (("1" (ASSERT) NIL)))))))
                 ("2" (REPLACE -1)
                  (("2" (EXPAND "remove")
                    (("2" (EXPAND "member")
                      (("2" (ASSERT)
                        (("2" (EXPAND "dbl")
                          (("2" (HIDE -1 3)
                            (("2" (EXPAND "choose")
                              (("2"
                                (LEMMA "epsilon_ax[T]")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (INST + "y!1")
                                      (("1" (ASSERT) NIL)))))))
                                 ("2"
                                  (INST + "y!1")
                                  NIL)))))))))))))))))
                 ("3" (REPLACE -2)
                  (("3" (EXPAND "remove") (("3" (ASSERT) NIL)))))
                 ("4" (REPLACE -1)
                  (("4" (EXPAND "remove")
                    (("4" (EXPAND "member")
                      (("4" (EXPAND "dbl")
                        (("4" (ASSERT)
                          (("4" (HIDE -1)
                            (("4" (HIDE 3)
                              (("4"
                                (EXPAND "choose")
                                (("4"
                                  (LEMMA "epsilon_ax[T]")
                                  (("1"
                                    (INST?)
                                    (("1"
                                      (ASSERT)
                                      (("1"
                                        (INST + "x!1")
                                        (("1" (ASSERT) NIL)))))))
                                   ("2"
                                    (INST + "x!1")
                                    NIL)))))))))))))))))))))))))))
         ("2" (HIDE 3) (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))
 (|dbl_to_pair_TCC1| ""
  (INST 1 " (LAMBDA D: (choose(D),choose(rest(D))))")
  (("1" (SKOSIMP*)
    (("1" (TYPEPRED "D!1")
      (("1" (SKOSIMP*)
        (("1" (REPLACE -1)
          (("1" (LEMMA "dbl_choose")
            (("1" (INST?)
              (("1" (LEMMA "dbl_rest_choose")
                (("1" (INST?)
                  (("1" (ASSERT)
                    (("1" (FLATTEN)
                      (("1" (ASSERT)
                        (("1" (PROP)
                          (("1" (REPLACE*) NIL)
                           ("2" (REPLACE*)
                            (("2" (REWRITE "dbl_comm") NIL)))
                           ("3" (REPLACE*) NIL)
                           ("4" (REPLACE*) NIL)))))))))))))))))))))))))
   ("2" (LEMMA "doubleton_rest_nonempty") (("2" (PROPAX) NIL)))
   ("3" (LEMMA "doubleton_nonempty") (("3" (PROPAX) NIL)))))
 (|dbl_def| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|dbl_in| "" (SKOSIMP*)
  (("" (REPLACE -1) (("" (HIDE -1) (("" (GRIND) NIL)))))))
 (|dbl_not_in| "" (SKOSIMP*)
  (("" (REPLACE -1) (("" (HIDE -1) (("" (GRIND) NIL)))))))
 (|dbl_to_pair_lem_TCC1| "" (SUBTYPE-TCC) NIL)
 (|dbl_to_pair_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "dbl_to_pair(dbl(x!1, y!1))")
    (("1"
      (CASE "dbl(x!1, y!1)(x!1)
          =
        dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
            PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(x!1)")
      (("1"
        (CASE "dbl(x!1, y!1)(y!1)
          =
        dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
            PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(y!1)")
        (("1" (HIDE -3)
          (("1" (EXPAND "dbl")
            (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T)
              (("1" (APPLY-EXTENSIONALITY 3 :HIDE? T)
                (("1" (EXPAND "dbl")
                  (("1" (INST?) (("1" (ASSERT) NIL)))))))
               ("2" (APPLY-EXTENSIONALITY 3 :HIDE? T)
                (("2" (EXPAND "dbl")
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))
               ("3" (EXPAND "dbl")
                (("3" (INST?) (("3" (ASSERT) NIL)))))))))))
         ("2" (ASSERT) NIL)))
       ("2" (ASSERT) NIL)))
     ("2" (INST?) (("2" (ASSERT) NIL)))))))
 (|dbl_to_pair_inverse_l| "" (SKOLEM-TYPEPRED)
  (("" (SKOSIMP*)
    (("" (REPLACE -1)
      (("" (USE "dbl_to_pair_lem")
        (("" (ASSERT)
          (("" (GROUND)
            (("1" (REPLACE -1) (("1" (PROPAX) NIL)))
             ("2" (REPLACE -1)
              (("2" (REWRITE "dbl_comm") NIL)))))))))))))))
 (|dbl_proj| "" (SKOSIMP*)
  (("" (LEMMA "dbl_to_pair_inverse_l")
    (("" (INST?)
      (("" (EXPAND "dbl")
        (("" (REPLACE -1 + RL) (("" (ASSERT) NIL)))))))))))
 (|proj_dbl| "" (SKOSIMP*)
  (("" (TYPEPRED "D!1")
    (("" (SKOSIMP*)
      (("" (REPLACE -1)
        (("" (HIDE -1)
          (("" (LEMMA "dbl_to_pair_lem")
            (("" (INST?)
              (("" (ASSERT) (("" (GRIND) NIL)))))))))))))))))
 (|dbl_eq| "" (SKOSIMP*)
  (("" (CASE "dbl(x!1, y!1)(x!1) = dbl(v!1, z!1)(x!1)")
    (("1" (CASE "dbl(x!1, y!1)(y!1) = dbl(v!1, z!1)(y!1)")
      (("1" (CASE "dbl(x!1, y!1)(z!1) = dbl(v!1, z!1)(z!1)")
        (("1" (CASE "dbl(x!1, y!1)(v!1) = dbl(v!1, z!1)(v!1)")
          (("1" (EXPAND "dbl") (("1" (GROUND) NIL)))
           ("2" (ASSERT) NIL)))
         ("2" (ASSERT) NIL)))
       ("2" (ASSERT) NIL)))
     ("2" (ASSERT) NIL)))))
 (|finite_dbl| "" (SKOSIMP*)
  (("" (CASE-REPLACE "dbl(x!1, y!1) = add(x!1,singleton(y!1))")
    (("1" (REWRITE "finite_add")
      (("1" (REWRITE "finite_singleton") NIL)))
     ("2" (HIDE 2)
      (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
        (("2" (GRIND) NIL))))))))))
$$$trees.pvs
trees[T: TYPE]: THEORY
BEGIN
   IMPORTING digraph_deg[T], digraph_ops[T], di_subgraphs[T]
   G,GP,C,GG: VAR digraph[T]
   tree?(G): RECURSIVE bool = card[T](vert(G)) = 1 OR
                         (EXISTS (v: (vert(G))): deg(v,G) = 1 AND
                                  tree?(del_vert[T](G,v)))
             MEASURE size(G)
   tree_nonempty: LEMMA tree?(G) IMPLIES NOT empty?(G)
   Tree: TYPE = {G: digraph[T] | tree?(G)}
END trees
$$$trees.prf
(|trees|
 (|tree?_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "size")
    (("" (EXPAND "del_vert")
      (("" (REWRITE "card_remove") (("" (ASSERT) NIL)))))))))
 (|tree_nonempty| "" (SKOSIMP*)
  (("" (EXPAND "empty?")
    (("" (USE "card_empty?[T]")
      (("" (IFF)
        (("" (ASSERT)
          (("" (EXPAND "tree?")
            (("" (SKOSIMP*)
              (("" (LEMMA "deg_1_sing")
                (("" (INST?)
                  (("" (ASSERT)
                    (("" (SKOSIMP*)
                      (("" (EXPAND "in?")
                        (("" (EXPAND "empty?")
                          (("" (INST?)
                            (("" (EXPAND "member")
                              ((""
                                (PROPAX)
                                NIL))))))))))))))))))))))))))))))))
$$$max_subtrees.pvs
max_subtrees[T: TYPE]: THEORY
BEGIN
   IMPORTING trees[T]
   G: VAR Digraph[T]    % not empty?(G)
   IMPORTING  max_di_subgraphs[T], doubletons[T]
   v: VAR T
   sing_is_tree: LEMMA tree?[T](singleton_digraph(v))
   tree_in: LEMMA (EXISTS (Tr: Tree[T]): di_subgraph?(Tr,G) AND
                          nonempty?[T](vert(Tr)))
   Tr,S: VAR Tree[T]
   Subtree(G: digraph[T]): TYPE = {Tr: Tree | di_subgraph?(Tr,G)}
   max_subtree(G: Digraph[T]): Subtree(G) = max_di_subgraph(G,(LAMBDA G: tree?(G)))
   max_subtree_tree    : LEMMA tree?(max_subtree(G))
   max_subtree_di_subgraph: LEMMA di_subgraph?(max_subtree(G),G)
   max_subtree_max     : LEMMA FORALL (SS: Subtree(G)):
                                         size(SS) <= size(max_subtree(G))
END max_subtrees
$$$max_subtrees.prf
(|max_subtrees|
 (|sing_is_tree| "" (SKOSIMP*)
  (("" (EXPAND "tree?")
    (("" (PROP)
      (("" (HIDE 2)
        (("" (EXPAND "singleton_digraph")
          (("" (REWRITE "card_singleton") NIL)))))))))))
 (|tree_in| "" (SKOSIMP*)
  (("" (TYPEPRED "G!1")
    (("" (HIDE -2)
      (("" (EXPAND "nonempty?")
        (("" (EXPAND "empty?")
          (("" (SKOSIMP*)
            (("" (EXPAND "member")
              (("" (CASE "isolated?(G!1)")
                (("1" (INST 1 "singleton_digraph(x!1)")
                  (("1" (GRIND) NIL)
                   ("2" (REWRITE "sing_is_tree") NIL)))
                 ("2" (EXPAND "isolated?")
                  (("2" (EXPAND "empty?")
                    (("2" (SKOSIMP*)
                      (("2" (EXPAND "member")
                        (("2" (LEMMA "edges_to_pair")
                          (("2" (INST?)
                            (("2" (ASSERT)
                              (("2"
                                (SKOSIMP*)
                                (("2"
                                  (INST
                                   +
                                   "(# vert := dbl[T](x!3,y!1), edges := singleton[edgetype]((x!3,y!1)) #)")
                                  (("1"
                                    (EXPAND "dbl")
                                    (("1"
                                      (EXPAND "di_subgraph?")
                                      (("1"
                                        (PROP)
                                        (("1" (GRIND) NIL)
                                         ("2" (GRIND) NIL)
                                         ("3"
                                          (INST -1 "x!3")
                                          (("3" (ASSERT) NIL)))))))))
                                   ("2"
                                    (PROP)
                                    (("1"
                                      (SKOSIMP*)
                                      (("1"
                                        (EXPAND "singleton")
                                        (("1"
                                          (EXPAND "dbl")
                                          (("1"
                                            (LEMMA "proj_rew")
                                            (("1"
                                              (INST?)
                                              (("1"
                                                (ASSERT)
                                                NIL)))))))))))
                                     ("2"
                                      (EXPAND "tree?")
                                      (("2"
                                        (FLATTEN)
                                        (("2"
                                          (INST 2 "x!3")
                                          (("1"
                                            (PROP)
                                            (("1"
                                              (HIDE 2)
                                              (("1"
                                                (EXPAND "deg")
                                                (("1"
                                                  (EXPAND
                                                   "incident_edges")
                                                  (("1"
                                                    (CASE-REPLACE
                                                     "{e: edgetype[T] | (singleton[edgetype](x!3, y!1)(e) AND in?(x!3, e))} = singleton[edgetype](x!3, y!1)")
                                                    (("1"
                                                      (REWRITE
                                                       "card_singleton")
                                                      NIL)
                                                     ("2"
                                                      (HIDE 2)
                                                      (("2"
                                                        (APPLY-EXTENSIONALITY
                                                         1
                                                         :HIDE?
                                                         T)
                                                        (("2"
                                                          (GRIND)
                                                          NIL)))))))))))))
                                             ("2"
                                              (ASSERT)
                                              (("2"
                                                (CASE "x!3 = y!1")
                                                (("1"
                                                  (ASSERT)
                                                  (("1"
                                                    (CASE-REPLACE
                                                     "dbl[T](x!3, y!1) = singleton[T](y!1)")
                                                    (("1"
                                                      (REWRITE
                                                       "card_singleton[T]")
                                                      NIL)
                                                     ("2"
                                                      (HIDE 2 3)
                                                      (("2"
                                                        (APPLY-EXTENSIONALITY
                                                         1
                                                         :HIDE?
                                                         T)
                                                        (("2"
                                                          (GRIND)
                                                          NIL)))))))))
                                                 ("2"
                                                  (CASE-REPLACE
                                                   "del_vert[T]((# vert := dbl[T](x!3, y!1),
                              edges :=
                                singleton[edgetype]((x!3, y!1))
                              #),
                           x!3) = singleton_digraph(y!1)")
                                                  (("1"
                                                    (HIDE -1)
                                                    (("1"
                                                      (REWRITE
                                                       "sing_is_tree")
                                                      NIL)))
                                                   ("2"
                                                    (HIDE 3 4)
                                                    (("2"
                                                      (APPLY-EXTENSIONALITY
                                                       :HIDE?
                                                       T)
                                                      (("1"
                                                        (GRIND)
                                                        (("1"
                                                          (APPLY-EXTENSIONALITY
                                                           :HIDE?
                                                           T)
                                                          (("1"
                                                            (GRIND)
                                                            NIL)))))
                                                       ("2"
                                                        (EXPAND
                                                         "del_vert")
                                                        (("2"
                                                          (EXPAND
                                                           "remove")
                                                          (("2"
                                                            (EXPAND
                                                             "singleton_digraph")
                                                            (("2"
                                                              (EXPAND
                                                               "member")
                                                              (("2"
                                                                (EXPAND
                                                                 "singleton")
                                                                (("2"
                                                                  (EXPAND
                                                                   "dbl")
                                                                  (("2"
                                                                    (APPLY-EXTENSIONALITY
                                                                     1
                                                                     :HIDE?
                                                                     T)
                                                                    (("2"
                                                                      (IFF
                                                                       1)
                                                                      (("2"
                                                                        (GROUND)
                                                                        NIL)))))))))))))))))
                                                       ("3"
                                                        (SKOSIMP*)
                                                        (("3"
                                                          (EXPAND
                                                           "dbl")
                                                          (("3"
                                                            (EXPAND
                                                             "singleton")
                                                            (("3"
                                                              (ASSERT)
                                                              (("3"
                                                                (GROUND)
                                                                (("1"
                                                                  (REPLACE
                                                                   -1)
                                                                  (("1"
                                                                    (ASSERT)
                                                                    NIL)))
                                                                 ("2"
                                                                  (LEMMA
                                                                   "proj_rew")
                                                                  (("2"
                                                                    (INST?)
                                                                    (("2"
                                                                      (ASSERT)
                                                                      NIL)))))))))))))))
                                                       ("4"
                                                        (REWRITE
                                                         "finite_dbl")
                                                        NIL)))))
                                                   ("3"
                                                    (HIDE 3 4)
                                                    (("3"
                                                      (SKOSIMP*)
                                                      (("3"
                                                        (EXPAND
                                                         "singleton")
                                                        (("3"
                                                          (ASSERT)
                                                          (("3"
                                                            (EXPAND
                                                             "dbl")
                                                            (("3"
                                                              (REPLACE
                                                               -1)
                                                              (("3"
                                                                (ASSERT)
                                                                NIL)))))))))))))
                                                   ("4"
                                                    (HIDE 2 3)
                                                    (("4"
                                                      (REWRITE
                                                       "finite_dbl")
                                                      NIL)))))))))))
                                           ("2"
                                            (ASSERT)
                                            (("2"
                                              (EXPAND "dbl")
                                              (("2"
                                                (PROPAX)
                                                NIL)))))))))))))
                                   ("3" (REWRITE "finite_dbl") NIL)
                                   ("4"
                                    (REWRITE "finite_singleton")
                                    NIL)))))))))))))))))))))))))))))))))))
 (|max_subtree_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "tree_in")
    (("" (INST?)
      (("" (SKOSIMP*)
        (("" (INST?)
          (("" (PROP)
            (("" (EXPAND "extend") (("" (ASSERT) NIL)))))))))))))))
 (|max_subtree_TCC2| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (LEMMA "max_di_subgraph_in")
      (("1" (INST?)
        (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))
         ("2" (HIDE 2)
          (("2" (LEMMA "tree_in")
            (("2" (INST?)
              (("2" (SKOSIMP*)
                (("2" (INST?)
                  (("2" (ASSERT)
                    (("2" (EXPAND "extend")
                      (("2" (PROPAX) NIL)))))))))))))))))))
     ("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))
 (|max_subtree_tree| "" (SKOSIMP*)
  (("" (EXPAND "max_subtree")
    (("" (LEMMA "max_di_subgraph_in")
      (("" (INST?)
        (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))
         ("2" (HIDE 2)
          (("2" (LEMMA "tree_in")
            (("2" (INST?)
              (("2" (SKOSIMP*)
                (("2" (INST?)
                  (("2" (EXPAND "extend")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|max_subtree_di_subgraph| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|max_subtree_max| "" (SKOSIMP*)
  (("" (EXPAND "max_subtree")
    (("" (LEMMA "max_di_subgraph_is_max")
      (("" (INST?)
        (("1" (EXPAND "extend")
          (("1" (GROUND)
            (("1" (HIDE 2)
              (("1" (TYPEPRED "SS!1")
                (("1" (HIDE -1 -3)
                  (("1" (LEMMA "tree_nonempty")
                    (("1" (INST?)
                      (("1" (EXPAND "empty?")
                        (("1" (EXPAND "nonempty?")
                          (("1" (PROPAX) NIL)))))))))))))))))))
         ("2" (HIDE 2)
          (("2" (LEMMA "tree_in")
            (("2" (INST?)
              (("2" (SKOSIMP*)
                (("2" (INST?)
                  (("2" (ASSERT)
                    (("2" (EXPAND "extend")
                      (("2" (PROPAX) NIL))))))))))))))))))))))))
$$$min_lem.pvs
min_lem: THEORY
BEGIN
  IMPORTING min_nat
  S: VAR (nonempty?[nat])
  min_lem        : LEMMA minimum?(min(S), S)
END min_lem
$$$min_lem.prf
(|min_lem|
 (|min_lem| "" (SKOSIMP*)
  (("" (LEMMA "min_def") (("" (INST?) (("" (ASSERT) NIL))))))))
$$$max_upto.pvs
max_upto[N: nat]: THEORY
  EXPORTING ALL
BEGIN
  IMPORTING min_lem
  S: VAR (nonempty?[upto[N]])
  n,a,x: VAR upto[N]
  max(S): {a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}
  maximum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a >= x)
  max_def         : LEMMA max(S) = a IFF maximum?(a, S)
  max_lem         : LEMMA maximum?(max(S), S)
END max_upto
$$$max_upto.prf
(|max_upto|
 (|max_TCC1| "" (INST 1 "(LAMBDA S: N - min({y: upto[N] | S(N-y)}))")
  (("1" (SKOSIMP*)
    (("1" (LEMMA "min_lem")
      (("1" (EXPAND "extend")
        (("1" (INST?)
          (("1" (EXPAND "minimum?")
            (("1" (FLATTEN)
              (("1" (ASSERT)
                (("1" (GROUND)
                  (("1" (SKOSIMP*)
                    (("1" (INST -4 "N-x!1") (("1" (ASSERT) NIL)))))))))))))
           ("2" (HIDE 2)
            (("2" (EXPAND "nonempty?")
              (("2" (TYPEPRED "S!1")
                (("2" (EXPAND "nonempty?")
                  (("2" (EXPAND "empty?")
                    (("2" (SKOSIMP*)
                      (("2" (EXPAND "member")
                        (("2" (INST -2 "N-x!1")
                          (("2" (ASSERT) NIL)))))))))))))))))
           ("3" (HIDE 2) (("3" (SKOSIMP*) (("3" (ASSERT) NIL)))))))))))))
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "S!1")
      (("2" (EXPAND "nonempty?")
        (("2" (EXPAND "empty?")
          (("2" (SKOSIMP*)
            (("2" (EXPAND "member")
              (("2" (INST -2 "N-x!1")
                (("2" (EXPAND "extend") (("2" (PROPAX) NIL)))))))))))))))))))
 (|max_def| "" (SKOLEM-TYPEPRED)
  (("" (TYPEPRED "max(S!1)")
    (("" (PROP)
      (("1" (EXPAND "maximum?")
        (("1" (ASSERT) (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))))))
       ("2" (EXPAND "maximum?")
        (("2" (FLATTEN)
          (("2" (INST -5 "a!1")
            (("2" (ASSERT)
              (("2" (INST -2 "max(S!1)") (("2" (ASSERT) NIL)))))))))))))))))
 (|max_lem| "" (SKOSIMP*)
  (("" (EXPAND "maximum?")
    (("" (ASSERT)
      (("" (LEMMA "max_def")
        (("" (INST?) (("" (INST?) (("" (ASSERT) NIL))))))))))))))
$$$max_di_subgraphs.pvs
max_di_subgraphs[T: TYPE]: THEORY
BEGIN
   IMPORTING  di_subgraphs[T], max_upto
   G: VAR digraph[T]
   Gpred(G): TYPE = {P: pred[digraph[T]] | (EXISTS (S: digraph[T]):
                                             di_subgraph?(S,G) AND P(S))}
   n: VAR nat
   is_one_of_size(G: digraph[T], P: Gpred(G),n: nat): bool =
            (EXISTS (S: di_subgraph(G)): P(S) AND size(S) = n)
   prep0: LEMMA FORALL (G: digraph[T], P: Gpred(G)):
       nonempty?[upto[size(G)]]({n: upto[size(G)] | is_one_of_size(G,P,n)})
   max_size(G: digraph[T], P: Gpred(G)): upto[size(G)] =
             max({n: upto[size(G)] | is_one_of_size(G,P,n)})
   prep    : LEMMA FORALL (G: digraph[T], P: Gpred(G)):
                            nonempty?[di_subgraph(G)]({S: di_subgraph(G)
                                | size[T](S) = max_size(G,P) AND P(S)})
   maximal?(G: digraph[T], S: di_subgraph(G),P: Gpred(G)): bool = P(S) AND
                       (FORALL (SS: di_subgraph(G)): P(SS) IMPLIES
                                                        size(SS) <= size(S))
%  Existence TCC satisfied by
%    choose({S: di_subgraph(G) | size(S) = max_size AND P(S)})
   max_di_subgraph(G: digraph[T], P: Gpred(G)): {S: di_subgraph(G) | maximal?(G,S,P)}
   max_di_subgraph_def    : LEMMA FORALL (P: Gpred(G)):
                                     maximal?(G,max_di_subgraph(G,P),P)
   max_di_subgraph_in     : LEMMA FORALL (P: Gpred(G)): P(max_di_subgraph(G,P))
   max_di_subgraph_is_max : LEMMA FORALL (P: Gpred(G)):
                          (FORALL (SS: di_subgraph(G)): P(SS) IMPLIES
                                          size(SS) <= size(max_di_subgraph(G,P)))
END max_di_subgraphs
$$$max_di_subgraphs.prf
(|max_di_subgraphs|
 (|prep0| "" (SKOSIMP*)
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (TYPEPRED "P!1")
        (("" (SKOSIMP*)
          (("" (INST -3 "size(S!1)")
            (("1" (EXPAND "member")
              (("1" (EXPAND "is_one_of_size")
                (("1" (INST?) (("1" (ASSERT) NIL)))))))
             ("2" (REWRITE "di_subgraph_smaller") NIL)))))))))))))
 (|max_size_TCC1| "" (EXPAND "nonempty?")
  (("" (EXPAND "empty?")
    (("" (EXPAND "member")
      (("" (SKOSIMP*)
        (("" (LEMMA "prep0")
          (("" (INST?)
            (("" (INST?)
              (("" (EXPAND "nonempty?")
                (("" (EXPAND "empty?")
                  (("" (SKOSIMP*)
                    (("" (EXPAND "member")
                      (("" (INST?) NIL)))))))))))))))))))))))
 (|prep| "" (SKOSIMP*)
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (EXPAND "member")
        (("" (EXPAND "max_size")
          ((""
            (TYPEPRED
             "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})")
            (("1" (HIDE -1 -3)
              (("1" (EXPAND "is_one_of_size")
                (("1" (SKOSIMP*)
                  (("1" (INST -3 "S!1") (("1" (ASSERT) NIL)))))))))
             ("2" (REWRITE "prep0") NIL)))))))))))))
 (|max_di_subgraph_TCC1| ""
  (INST 1
   "(LAMBDA (G: digraph[T], P: Gpred(G)): choose({S: di_subgraph(G) | size(S) = max_size(G,P) AND P(S)}))")
  (("1" (SKOSIMP*)
    (("1" (EXPAND "maximal?")
      (("1" (PROP)
        (("1" (ASSERT) NIL)
         ("2" (SKOSIMP*)
          (("2" (TYPEPRED "max_size(G!1,P!1)")
            (("2" (HIDE -1)
              (("2" (EXPAND "max_size")
                (("2"
                  (TYPEPRED
                   "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})")
                  (("1" (HIDE -1 -2)
                    (("1" (INST -1 "size(SS!1)")
                      (("1" (ASSERT)
                        (("1" (HIDE -1 2)
                          (("1" (EXPAND "is_one_of_size")
                            (("1" (INST?) (("1" (ASSERT) NIL)))))))))
                       ("2" (HIDE -1 2)
                        (("2" (TYPEPRED "SS!1")
                          (("2" (HIDE -2 -2)
                            (("2" (REWRITE "di_subgraph_smaller")
                              NIL)))))))))))
                   ("2" (HIDE -1 2)
                    (("2" (LEMMA "prep")
                      (("2" (REWRITE "prep0") NIL)))))))))))))))))))))
   ("2" (ASSERT)
    (("2" (SKOSIMP*) (("2" (LEMMA "prep") (("2" (INST?) NIL)))))))))
 (|max_di_subgraph_def| "" (SKOSIMP*)
  (("" (TYPEPRED "max_di_subgraph(G!1, P!1)") (("" (PROPAX) NIL)))))
 (|max_di_subgraph_in| "" (SKOSIMP*)
  (("" (TYPEPRED "max_di_subgraph(G!1, P!1)")
    (("" (HIDE -2 -3)
      (("" (EXPAND "maximal?")
        (("" (FLATTEN) (("" (PROPAX) NIL)))))))))))
 (|max_di_subgraph_is_max| "" (SKOSIMP*)
  (("" (TYPEPRED "max_di_subgraph(G!1, P!1)")
    (("" (HIDE -2 -3)
      (("" (EXPAND "maximal?")
        (("" (FLATTEN)
          (("" (HIDE -1) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))
$$$di_subgraphs_from_walk.pvs
di_subgraphs_from_walk[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T], walks[T], di_subgraphs[T]
   G,GG: VAR digraph[T]
   t,t1,t2,v: VAR T
   i: VAR nat
   e: VAR edgetype[T]
   G_from(G, (w: Walk(G))): di_subgraph(G) = (# vert  := verts_of(w),
                                             edges := edges_of(w) #)
   G_from_vert     : LEMMA FORALL (w: Walk(G)): vert(G_from(G,w)) = verts_of(w)
   vert_G_from     : LEMMA FORALL (w: Walk(G), i: below(l(w))):
                                      vert(G_from(G, w))(w(i))
   edge?_G_from    : LEMMA FORALL (w: Walk(G), i: below(l(w)-1)):
                                      edge?(G_from(G, w))(w(i), w(i+1))
%%%%%%%%%%%%%%%%%%%%%%%%%% not true for directed graphs %%%%%%%%%%%%%%%%%%%%
%
%   edge?_G_from_rev: LEMMA FORALL (w: Walk(G), i: below(l(w)-1)):
%                                     edge?(G_from(G, w))(w(i+1), w(i))
   vert_G_from_not : LEMMA FORALL (w: Walk(G)):
                       subset?(vert(G_from(G, w)), vert(GG)) AND
                       NOT  verts_of(w)(v)
                     IMPLIES
                        subset?(vert(G_from(G, w)), remove[T](v, vert(GG)))
   IMPORTING digraph_ops[T]
   del_vert_di_subgraph: LEMMA FORALL (w: Walk(G), v: (vert(GG))):
                              di_subgraph?(G_from(G, w), GG) AND
                              NOT verts_of(w)(v) IMPLIES
                                    di_subgraph?(G_from(G, w), del_vert(GG, v))
END di_subgraphs_from_walk
$$$di_subgraphs_from_walk.prf
(|di_subgraphs_from_walk|
 (|G_from_TCC1| "" (SKOSIMP*)
  (("" (TYPEPRED "w!1")
    (("" (SPLIT +)
      (("1" (SKOSIMP*)
        (("1" (EXPAND "walk?")
          (("1" (FLATTEN)
            (("1" (EXPAND "verts_of")
              (("1" (EXPAND "verts_in?")
                (("1" (EXPAND "fseq")
                  (("1" (HIDE -4)
                    (("1" (EXPAND "edges_of")
                      (("1" (SKOSIMP*)
                        (("1" (REPLACE -1)
                          (("1" (HIDE -1)
                            (("1" (EXPAND "fseq")
                              (("1"
                                (SPLIT +)
                                (("1" (INST?) NIL)
                                 ("2"
                                  (INST?)
                                  NIL)))))))))))))))))))))))))))
       ("2" (EXPAND "di_subgraph?")
        (("2" (EXPAND "walk?")
          (("2" (FLATTEN)
            (("2" (EXPAND "subset?")
              (("2" (EXPAND "member")
                (("2" (EXPAND "verts_of")
                  (("2" (EXPAND "edges_of")
                    (("2" (EXPAND "fseq")
                      (("2" (SPLIT +)
                        (("1" (SKOSIMP*)
                          (("1" (EXPAND "verts_in?")
                            (("1" (INST?) (("1" (ASSERT) NIL)))))))
                         ("2" (SKOSIMP*)
                          (("2" (EXPAND "edge?")
                            (("2" (INST?)
                              (("2"
                                (ASSERT)
                                (("2"
                                  (REPLACE -1)
                                  (("2"
                                    (FLATTEN)
                                    (("2"
                                      (PROPAX)
                                      NIL)))))))))))))))))))))))))))))))))))))
 (|G_from_vert| "" (SKOSIMP*)
  (("" (EXPAND "G_from") (("" (PROPAX) NIL)))))
 (|vert_G_from| "" (SKOSIMP*)
  (("" (EXPAND "G_from")
    (("" (EXPAND "verts_of") (("" (INST?) NIL)))))))
 (|edge?_G_from_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|edge?_G_from_TCC2| "" (SUBTYPE-TCC) NIL)
 (|edge?_G_from_TCC3| "" (SUBTYPE-TCC) NIL)
 (|edge?_G_from| "" (SKOSIMP*)
  (("" (EXPAND "G_from")
    (("" (EXPAND "edge?")
      (("" (TYPEPRED "w!1")
        (("" (EXPAND "walk?")
          (("" (FLATTEN)
            (("" (INST?)
              (("" (ASSERT)
                (("" (EXPAND "edge?")
                  (("" (FLATTEN)
                    (("" (ASSERT)
                      (("" (EXPAND "edges_of")
                        (("" (INST + "i!1")
                          (("" (ASSERT) NIL)))))))))))))))))))))))))))
 (|edge?_G_from_rev| "" (SKOSIMP*)
  (("" (EXPAND "G_from")
    (("" (TYPEPRED "w!1")
      (("" (EXPAND "walk?")
        (("" (FLATTEN)
          (("" (EXPAND "edge?")
            (("" (INST -2 "i!1")
              (("" (ASSERT)
                (("" (FLATTEN)
                  (("" (REWRITE "pair_comm")
                    (("" (ASSERT)
                      (("" (EXPAND "edges_of")
                        (("" (INST?)
                          (("" (HIDE -1 -2 -3 1)
                            (("" (REWRITE "pair_comm")
                              NIL)))))))))))))))))))))))))))))
 (|vert_G_from_not| "" (SKOSIMP*)
  (("" (EXPAND "subset?")
    (("" (SKOSIMP*)
      (("" (REWRITE "G_from_vert")
        (("" (INST?)
          (("" (ASSERT)
            (("" (EXPAND "remove")
              (("" (EXPAND "member") (("" (ASSERT) NIL)))))))))))))))))
 (|del_vert_di_subgraph| "" (SKOSIMP*)
  (("" (EXPAND "di_subgraph?")
    (("" (PROP)
      (("1" (HIDE -2)
        (("1" (EXPAND "del_vert")
          (("1" (REWRITE "vert_G_from_not") NIL)))))
       ("2" (LEMMA "vert_G_from_not")
        (("2" (INST?)
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (EXPAND "subset?" +)
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "member")
                    (("2" (REWRITE "edge_in_del_vert")
                      (("1" (HIDE -1 -3 2 3)
                        (("1" (EXPAND "subset?")
                          (("1" (INST?)
                            (("1" (EXPAND "member")
                              (("1" (PROPAX) NIL)))))))))
                       ("2" (HIDE -4 -5 1)
                        (("2" (EXPAND "subset?")
                          (("2" (INST?)
                            (("2" (EXPAND "member")
                              (("2"
                                (NAME-REPLACE SG "G_from(G!1, w!1)")
                                (("2"
                                  (TYPEPRED "SG")
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (ASSERT)
                                      (("2"
                                        (EXPAND "remove")
                                        (("2"
                                          (EXPAND "in?")
                                          (("2"
                                            (FLATTEN)
                                            (("2"
                                              (GROUND)
                                              NIL))))))))))))))))))))))))))))))))))))))))))))))
$$$circuits.pvs
circuits[T: TYPE]: THEORY
BEGIN
   IMPORTING walks[T]
   G: VAR digraph[T]
   reducible?(G: digraph[T], w: Seq(G)): bool  =
          (EXISTS (k: posnat): k < l(w) - 1 AND w(k-1) = w(k+1))
   reduced?(G: digraph[T], w: Seq(G)): bool = NOT reducible?(G,w)
%
%   cyclically_reduced?(G: digraph[T], w: Long_walk(G)): bool =
%         reduced?(G,w) AND
%         (FORALL (j: below(l(w)-1)): reduced?(G,w^(j+1, l(w)-1) o w^(1,j)))
   cyclically_reduced?(G: digraph[T], w: Seq(G)): bool = l(w) > 2 AND
         reduced?(G,w) AND w(1) /= w(l(w)-2)
   circuit?(G:  digraph[T], w: Seq(G)): bool = walk?(G,w) AND
                                             cyclically_reduced?(G,w) AND
                                             pre_circuit?(G,w)
END circuits
$$$circuits.prf
(|circuits| (|reducible?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|reducible?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|cyclically_reduced?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|cyclically_reduced?_TCC2| "" (SUBTYPE-TCC) NIL))
$$$fslib.pvs
fslib : THEORY
BEGIN
     IMPORTING finite_sets@finite_sets,
               finite_sets@finite_sets_below,
               finite_sets@finite_sets_card_eq
END fslib
$$$seq_pidgeon.pvs
seq_pidgeon[T: TYPE, (IMPORTING fslib)
            S: finite_set[T]]: THEORY
BEGIN
   IMPORTING seq_def
   w: VAR finite_seq[(S)]
   seq_pigeon_lem: LEMMA
          (FORALL (i,j: below(l(w))): i /= j IMPLIES w(i) /= w(j)) IMPLIES
              l(w) <= card(S)
   seq_pigeon_hole: THEOREM l(w) > card(S) IMPLIES
                      (EXISTS (i,j: below(l(w))): i /= j AND w(i) = w(j))
END seq_pidgeon
$$$seq_pidgeon.prf
(|seq_pidgeon| (T_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))
 (T_1 "" (SKOSIMP*)
  (("" (EXPAND "T")
    (("" (EXPAND "fseq")
      (("" (CASE "{j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}(i!1)")
        (("1" (LEMMA "card_empty?[below(l(w!1))]")
          (("1" (INST -1 "{j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}")
            (("1"
              (CASE "card({j: below(l(w!1)) | (seq(w!1)(j) = seq(w!1)(i!1))}) = 0")
              (("1" (ASSERT)
                (("1" (HIDE -1 1)
                  (("1" (EXPAND "empty?")
                    (("1" (INST?)
                      (("1" (EXPAND "member") (("1" (PROPAX) NIL)))))))))))
               ("2" (HIDE -1 -2) (("2" (ASSERT) NIL)))
               ("3" (HIDE -1 -2 2) (("3" (REWRITE "finite_below") NIL)))))
             ("2" (REWRITE "finite_below") NIL)))))
         ("2" (HIDE 2) (("2" (GRIND) NIL)))))))))))
 (X_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))
 (Y_TCC1 "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))
 (W_TCC1 "" (SUBTYPE-TCC)) (|X_lem| "" (SKOSIMP*) (("" (POSTPONE) NIL)))
 (|XY_lem| "" (SKOSIMP*)
  (("" (CASE "fullset[below(l(w!1))] = union(X(w!1),Y(w!1))")
    (("1"
      (CASE-REPLACE
       "card(fullset[below(l(w!1))]) = card(union(X(w!1), Y(w!1)))")
      (("1" (HIDE -2)
        (("1" (REWRITE "card_union[below(l(w!1))]")
          (("1" (CASE-REPLACE "card(intersection(X(w!1), Y(w!1))) = 0")
            (("1" (HIDE -1)
              (("1" (REWRITE "card_below_fullset") (("1" (ASSERT) NIL)))))
             ("2" (HIDE -1 2)
              (("2"
                (CASE-REPLACE
                 "intersection(X(w!1), Y(w!1)) = emptyset[below(l(w!1))]")
                (("1" (HIDE -1)
                  (("1" (REWRITE "card_emptyset[below(l(w!1))]") NIL)))
                 ("2" (HIDE 2)
                  (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                    (("2" (GRIND) NIL)))))))))
             ("3" (REWRITE "finite_below") NIL)))))))
       ("2" (ASSERT) NIL) ("3" (REWRITE "finite_below") NIL)
       ("4" (REWRITE "finite_below") NIL)))
     ("2" (HIDE 2)
      (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL)))))))))
 (|Y_lem| "" (SKOSIMP*)
  (("" (LEMMA "X_lem")
    (("" (INST?)
      (("" (LEMMA "XY_lem") (("" (INST?) (("" (ASSERT) NIL)))))))))))
 (|CY_lem| "" (SKOSIMP*)
  (("" (LEMMA "card_empty?[below(l(w!1))]")
    (("" (INST?)
      (("" (ASSERT)
        (("" (EXPAND "empty?")
          (("" (SKOSIMP*)
            (("" (EXPAND "member")
              (("" (HIDE -2)
                (("" (EXPAND "Y")
                  (("" (CASE-REPLACE "card(T(w!1, x!1)) > 1")
                    (("1" (HIDE -2)
                      (("1"
                        (INST 1 "choose(T(w!1,x!1))"
                         "choose(remove(choose(T(w!1,x!1)),
                                                  T(w!1,x!1)))")
                        (("1" (POSTPONE) NIL) ("2" (POSTPONE) NIL)
                         ("3" (POSTPONE) NIL)))))
                     ("2" (HIDE 2)
                      (("2" (LEMMA "T_1")
                        (("2" (INST?)
                          (("2" (ASSERT) NIL)))))))))))))))))))))))))))
 (|seq_pigeon_lem| "" (SKOSIMP*)
  (("" (CASE "l(w!1) = card(fullset[below(l(w!1))])")
    (("1" (REPLACE -1)
      (("1" (HIDE -1)
        (("1" (LEMMA "injection_and_cardinal[below(l(w!1)),T]")
          (("1" (INST?)
            (("1" (ASSERT)
              (("1" (HIDE 2)
                (("1" (INST 1 "(LAMBDA (i: below(l(w!1))): w!1(i))")
                  (("1" (EXPAND "restrict")
                    (("1" (EXPAND "injective?")
                      (("1" (SKOSIMP*)
                        (("1" (INST?)
                          (("1" (INST -2 "x2!1") (("1" (ASSERT) NIL)))))))))))
                   ("2" (HIDE -1) (("2" (GRIND) NIL)))))))))
             ("2" (REWRITE "finite_below") NIL)))))))))
     ("2" (HIDE -1 2) (("2" (REWRITE "card_below_fullset") NIL)))
     ("3" (REWRITE "finite_below") NIL)))))
 (|seq_pigeon_hole| "" (SKOSIMP*)
  (("" (LEMMA "seq_pigeon_lem")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL)))))))))))))
 (|seq_pigeon_hole2| "" (SKOSIMP*)
  (("" (LEMMA "seq_pigeon_lem")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL))))))))))))))
$$$path_lems.pvs
path_lems[T: TYPE]: THEORY
BEGIN
   IMPORTING paths[T]
   G: VAR digraph[T]
   cycle?(G: digraph[T], (w: Seq(G))): bool = pre_circuit?(G,w) AND l(w) > 1 AND
                          w(1) /= w(l(w)-2) AND
                          (FORALL (i,j: below(l(w))):
                             w(i) = w(j) IMPLIES (i = j OR
                                          (endpoint?(i,w) AND endpoint?(j,w))))
   cycle_l_gt_3: LEMMA (FORALL (w: Seq(G)): cycle?(G,w) IMPLIES l(w) > 3)
   cycle_has_path: LEMMA FORALL (w: Seq(G)): cycle?(G,w) IMPLIES
                            (EXISTS (j: below(l(w))): path?(G,w^(0,j)))
%   fslib: LIBRARY = "../lib/fs/"
%
%   IMPORTING digraphs, fslib@finite_sets_card_eq, seq_pidgeon
   IMPORTING digraphs, finite_sets_card_eq, seq_pidgeon
   GF: VAR Digraph[T]
   Pigeon_hole: THEOREM FORALL (w: Walk(GF)): l(w) > card(vert(GF)) IMPLIES
                  (EXISTS (i,j: below(l(w))): i /= j AND w(i) = w(j))
END path_lems
$$$path_lems.prf
(|path_lems| (|cycle?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|cycle?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|cycle_l_gt_3| "" (SKOSIMP*)
  (("" (EXPAND "cycle?")
    (("" (FLATTEN)
      (("" (AUTO-REWRITE "fseq")
        (("" (EXPAND "pre_circuit?")
          (("" (FLATTEN) (("" (ASSERT) NIL)))))))))))))
 (|cycle_has_path_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "^") (("" (TYPEPRED "j!1") (("" (ASSERT) NIL)))))))
 (|cycle_has_path| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "fseq")
    (("" (LEMMA "cycle_l_gt_3")
      (("" (INST?)
        (("" (ASSERT)
          (("" (CASE "walk?(G!1, w!1)")
            (("1" (INST 1 "l(w!1)-2")
              (("1" (EXPAND "path?")
                (("1" (PROP)
                  (("1" (REWRITE "walk?_caret") NIL)
                   ("2" (SKOSIMP*)
                    (("2" (EXPAND "^")
                      (("2" (TYPEPRED "j!1")
                        (("1" (TYPEPRED "i!1")
                          (("1" (EXPAND "^")
                            (("1" (EXPAND "cycle?")
                              (("1"
                                (FLATTEN)
                                (("1"
                                  (INST -7 "i!1" "j!1")
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (FLATTEN)
                                      (("1"
                                        (EXPAND "endpoint?")
                                        (("1" (ASSERT) NIL)))))))
                                   ("2" (ASSERT) NIL)
                                   ("3" (ASSERT) NIL)))))))))
                           ("2" (SKOSIMP*) (("2" (GROUND) NIL)))))
                         ("2" (SKOSIMP*)
                          (("2" (GROUND) NIL)))))))))))))))
             ("2" (HIDE 2)
              (("2" (EXPAND "cycle?")
                (("2" (EXPAND "pre_circuit?")
                  (("2" (FLATTEN)
                    (("2" (PROPAX) NIL)))))))))))))))))))))
 (|Pigeon_hole| "" (SKOSIMP*)
  (("" (LEMMA "seq_pigeon_hole[T,(vert(GF!1))]")
    (("" (INST?)
      (("1" (ASSERT)
        (("1" (SKOSIMP*)
          (("1" (INST?)
            (("1" (INST 2 "j!1")
              (("1" (EXPAND "fseq") (("1" (ASSERT) NIL)))))))))))
       ("2" (SKOSIMP*)
        (("2" (HIDE 2)
          (("2" (TYPEPRED "x1!1")
            (("2" (TYPEPRED "w!1")
              (("2" (EXPAND "walk?")
                (("2" (FLATTEN)
                  (("2" (EXPAND "verts_in?")
                    (("2" (INST?) NIL))))))))))))))))))))))
$$$dags.pvs
dags[T: TYPE+]: THEORY
BEGIN
   IMPORTING paths[T]
   acyclic_digraph: TYPE = {G: digraph | (FORALL (w: Walk(G)): path?(G,w))}
   dag: TYPE = acyclic_digraph
   DG: VAR dag
   dag_no_self_loops: LEMMA FORALL (e: edgetype): edges(DG)(e) IMPLIES
                                  LET (x,y) = e IN x /= y
END dags
$$$dags.prf
(|dags|
 (|dag_no_self_loops| "" (SKOSIMP*)
  (("" (TYPEPRED "DG!1")
    (("" (INST? -2)
      (("" (ASSERT)
        (("" (FLATTEN)
          (("" (NAME-REPLACE "vv" "proj_1(e!1)")
            (("" (CASE "walk?[T](DG!1, gen_seq2[T](DG!1, vv, vv))")
              (("1" (INST - "gen_seq2(DG!1,vv,vv)")
                (("1" (EXPAND "path?")
                  (("1" (ASSERT)
                    (("1" (HIDE -1)
                      (("1" (EXPAND "fseq")
                        (("1" (EXPAND "gen_seq2")
                          (("1" (INST -1 "0" "1")
                            (("1" (ASSERT) NIL)
                             ("2" (EXPAND "gen_seq2")
                              (("2" (ASSERT) NIL)))))))))))))))))
               ("2" (HIDE -1)
                (("2" (EXPAND "walk?")
                  (("2" (PROP)
                    (("1" (EXPAND "verts_in?")
                      (("1" (SKOSIMP*) (("1" (GRIND) NIL)))))
                     ("2" (SKOSIMP*)
                      (("2" (EXPAND "fseq")
                        (("2" (EXPAND "gen_seq2")
                          (("2" (EXPAND "edge?")
                            (("2" (ASSERT) NIL)))))))))))))))
               ("3" (PROPAX) NIL))))))))))))))))
$$$walk_inductions.pvs
walk_inductions[T: TYPE]: THEORY
BEGIN
   IMPORTING walks[T]
   P: VAR pred[prewalk]
   n: VAR nat
   w,ww: VAR prewalk
   walk_prep              : LEMMA (FORALL w: P(w)) IFF
                                       (FORALL n, w : l(w) = n IMPLIES P(w))
   digraph_induction_walk    : THEOREM (FORALL w:
                                 (FORALL ww: l(ww) < l(w) IMPLIES P(ww))
                                                 IMPLIES P(w))
                                   IMPLIES (FORALL w: P(w))
END walk_inductions
$$$walk_inductions.prf
(|walk_inductions|
 (|walk_prep| "" (SKOSIMP*)
  (("" (SPLIT)
    (("1" (FLATTEN) (("1" (SKOSIMP*) (("1" (INST?) NIL)))))
     ("2" (FLATTEN) (("2" (SKOSIMP*) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))
 (|digraph_induction_walk| "" (SKOSIMP)
  (("" (REWRITE "walk_prep" +)
    (("" (INDUCT "n" 1 "NAT_induction")
      (("" (SKOSIMP*)
        (("" (INST -3 "w!1")
          (("" (SPLIT -3)
            (("1" (PROPAX) NIL)
             ("2" (SKOSIMP*)
              (("2" (INST -2 "l(ww!1)") (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|walk_to_path| "" (SKOLEM!)
  ((""
    (CASE "FORALL (w: prewalk): NOT walk_from?(G!1, w, s!1, t!1)
           OR (EXISTS (p: prewalk): path?(G!1, p) AND walk_from?(G!1, p, s!1, t!1))")
    (("1" (FLATTEN) (("1" (SKOSIMP*) (("1" (INST -1 "w!1") (("1" (ASSERT) NIL)))))))
     ("2" (HIDE 2)
      (("2" (INDUCT "w" 1 "digraph_induction_walk")
        (("2" (SKOSIMP*)
          (("2" (CASE "(EXISTS (i,j: below(l(w!1))): i /= j AND seq(w!1)(i) = seq(w!1)(j))")
            (("1" (SKOSIMP*)
              (("1" (CASE "i!1 < j!1")
                (("1" (INST -3 "w!1^(0,i!1) o w!1^(j!1-1,l(w!1)-1)")
                  (("1" (SPLIT -3)
                    (("1" (POSTPONE) NIL) ("2" (PROPAX) NIL)
                     ("3" (EXPAND "^")
                      (("3" (EXPAND "o ")
                        (("3" (ASSERT)
                          (("3" (TYPEPRED "j!1") (("3" (TYPEPRED "i!1") (("3" (POSTPONE) NIL)))))))))))))
                   ("2" (POSTPONE) NIL) ("3" (ASSERT) NIL)))
                 ("2" (POSTPONE) NIL)))))
             ("2" (INST 2 "w!1")
              (("2" (ASSERT)
                (("2" (EXPAND "path?")
                  (("2" (EXPAND "walk_from?")
                    (("2" (ASSERT)
                      (("2" (FLATTEN)
                        (("2" (ASSERT)
                          (("2" (SKOSIMP*)
                            (("2" (INST 1 "i!1" "j!1")
                              (("2" (ASSERT)
                                (("2" (EXPAND "fseq") (("2" (PROPAX) NIL))))))))))))))))))))))))))))))))))))
$$$abstract_min.pvs
abstract_min[T: TYPE, size: [T -> nat], P: pred[T]]: THEORY
%------------------------------------------------------------------------------
%
%  The need for a function that returns the smallest object that
%  satisfies a particular predicate arises in many contexts.  Thus it is
%  useful to develop an "abstract" min theory that can be instantiated in
%  multiple ways to provide different min functions.  Such a theory must
%  be parameterized by
%
%    -------------------------------------------------------------------------
%    | T: TYPE          | the base type over which min is defined            |
%    | size:[T -> nat]  | the size function by which objects are compared    |
%    | P: pred[T]       | the property that the min function must satisfy    |
%    -------------------------------------------------------------------------
%
%  Author:
%
%      Ricky W. Butler   NASA Langley
%
%  Version 2.0           Last modified 10/21/97
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        R.W.Butler@larc.nasa.gov
%
%------------------------------------------------------------------------------
BEGIN
   ASSUMING
   T_ne: ASSUMPTION EXISTS (t: T): P(t)
   ENDASSUMING
   IMPORTING min_nat
   n: VAR nat
   S,SS: VAR T
   is_one(n): bool = (EXISTS (S: T): P(S) AND size(S) = n)
   prep0: LEMMA nonempty?({n: nat | is_one(n)})
   min_f: nat = min({n: nat | is_one(n)})
   prep1: LEMMA nonempty?({S: T | size(S) = min_f AND P(S)})
   minimal?(S): bool = P(S) AND
                       (FORALL (SS: T): P(SS) IMPLIES size(S) <= size(SS))
   min: {S: T | minimal?(S)}
   min_def: LEMMA minimal?(min)
   min_in : LEMMA P(min)
   min_is_min: LEMMA P(SS) IMPLIES size(min) <= size(SS)
END abstract_min
$$$abstract_min.prf
(|abstract_min|
 (|prep0| "" (LEMMA "T_ne")
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (SKOSIMP*)
        (("" (EXPAND "member")
          (("" (EXPAND "is_one")
            (("" (INST -2 "size(t!1)")
              (("" (INST 1 "t!1") (("" (ASSERT) NIL)))))))))))))))))
 (|min_f_TCC1| "" (LEMMA "prep0") (("" (PROPAX) NIL)))
 (|prep1| "" (EXPAND "nonempty?")
  (("" (EXPAND "empty?")
    (("" (EXPAND "member")
      (("" (EXPAND "min_f")
        (("" (TYPEPRED "min({n: nat | is_one(n)})")
          (("1" (EXPAND "is_one")
            (("1" (SKOSIMP*) (("1" (INST -4 "S!1") (("1" (ASSERT) NIL)))))))
           ("2" (REWRITE "prep0") NIL)))))))))))
 (|min_TCC1| "" (LEMMA "prep1")
  (("" (EXPAND "nonempty?")
    (("" (EXPAND "empty?")
      (("" (SKOSIMP*)
        (("" (EXPAND "member")
          (("" (INST?)
            (("" (EXPAND "minimal?")
              (("" (ASSERT)
                (("" (EXPAND "min_f")
                  (("" (FLATTEN)
                    (("" (ASSERT)
                      (("" (SKOSIMP*)
                        (("" (TYPEPRED "min({n: nat | is_one(n)})")
                          (("1" (INST -2 "size(SS!1)")
                            (("1" (HIDE -1)
                              (("1" (ASSERT)
                                (("1" (EXPAND "is_one")
                                  (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
                           ("2" (LEMMA "prep0")
                            (("2" (PROPAX) NIL)))))))))))))))))))))))))))))
 (|min_def| "" (TYPEPRED "min") (("" (PROPAX) NIL)))
 (|min_in| "" (TYPEPRED "min")
  (("" (EXPAND "minimal?") (("" (FLATTEN) (("" (PROPAX) NIL)))))))
 (|min_is_min| "" (SKOSIMP*)
  (("" (TYPEPRED "min")
    (("" (EXPAND "minimal?")
      (("" (FLATTEN) (("" (INST?) (("" (ASSERT) NIL))))))))))))
$$$sep_sets.pvs
sep_sets[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T], walks[T]
   G: VAR digraph[T]
   v,s,t: VAR T
   e: VAR edgetype[T]
   V: VAR finite_set[T]
   del_verts(G,V): digraph[T] =
           (# vert := difference[T](vert(G),V),
              edges := {e | edges(G)(e) AND
                           (FORALL v: V(v) IMPLIES NOT in?(v,e))} #)
   separates(G,V,s,t): bool = NOT V(s) AND NOT V(t) AND
                   NOT (EXISTS (w: prewalk): walk_from?(del_verts(G,V),w,s,t))
   seps(G,s,t): TYPE = {V: finite_set[T] | IF s = t OR edge?(G)(s,t) THEN
                                              V = vert(G)
                                           ELSE separates(G,V,s,t)
                                           ENDIF}
   IMPORTING abstract_min
   sep_set_exists: LEMMA (EXISTS (t: seps(G, s, t)): TRUE)
   min_sep_set(G,s,t): finite_set[T] = min[seps(G,s,t),
                                  (LAMBDA (v: seps(G,s,t)): card(v)),
                                  (LAMBDA (v: seps(G,s,t)): true)]
   separable?(G,s,t): bool = (s /= t AND NOT edge?(G)(s,t))
   min_sep_set_edge: LEMMA NOT separable?(G,s,t) IMPLIES
                                  min_sep_set(G,s,t) = vert(G)
   min_sep_set_card: LEMMA FORALL (s,t: (vert(G))): separates(G,V,s,t)
                                  IMPLIES card(min_sep_set(G,s,t)) <= card(V)
   min_sep_set_seps: LEMMA separable?(G,s,t) IMPLIES
                               separates(G,min_sep_set(G,s,t),s,t)
   min_sep_set_vert: LEMMA separable?(G,s,t) AND min_sep_set(G,s,t)(v)
                                    IMPLIES vert(G)(v)
   ends_not_in_min_sep_set: LEMMA separable?(G,s,t)  AND min_sep_set(G, s, t)(v)
                                  IMPLIES v /= s AND v /= t
   w: VAR prewalk
   walk?_del_verts_not : LEMMA walk?(G, w) AND
                                  empty?(intersection(verts_of(w),V))
                                      IMPLIES walk?(del_verts(G, V), w)
   sep_num(G,s,t): nat = card(min_sep_set(G,s,t))
   IMPORTING digraph_deg[T], finite_sets@finite_sets_card_eq
   adj_verts(G,s): finite_set[T] = {v: T | (EXISTS (e: edgetype[T]):
                                         incident_edges[T](s, G)(e)
                                           AND in?(v,e) AND NOT v = s)}
%   adj_verts_lem: LEMMA card(adj_verts(G,s)) = deg(s,G)
%
%   sep_num_min: LEMMA FORALL (s,t: (vert(G))):
%                      separable?(G,s,t) IMPLIES
%                       sep_num(G,s,t) <= min(deg(s,G),deg(t,G))
END sep_sets
$$$sep_sets.prf
(|sep_sets|
 (|del_verts_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[edgetype]")
    (("" (INST?)
      (("" (INST -1 "edges(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|del_verts_TCC2| "" (SKOSIMP*)
  (("" (EXPAND "difference")
    (("" (EXPAND "member")
      (("" (TYPEPRED "G!1")
        (("" (INST?)
          (("" (ASSERT)
            (("" (EXPAND "in?")
              (("" (FLATTEN)
                (("" (GROUND)
                  (("1" (INST - "proj_1(e!1)") (("1" (ASSERT) NIL)))
                   ("2" (INST - "proj_2(e!1)")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|sep_set_exists| "" (SKOSIMP*)
  (("" (CASE "s!1 = t!1 OR edge?(G!1)(s!1,t!1)")
    (("1" (INST 1 "vert(G!1)") (("1" (GROUND) NIL)))
     ("2" (INST 2 "{t: T | vert(G!1)(t)  AND t /= s!1 AND t /= t!1}")
      (("2" (PROP)
        (("1" (LEMMA "finite_subset[T]")
          (("1" (INST?)
            (("1" (INST?)
              (("1" (ASSERT)
                (("1" (HIDE 2 3 4) (("1" (GRIND) NIL)))))))))))
         ("2" (HIDE 4 5)
          (("2" (EXPAND "separates")
            (("2" (SKOSIMP*)
              (("2" (EXPAND "walk_from?")
                (("2" (FLATTEN)
                  (("2" (CASE "l(w!1) = 1")
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1) (("1" (ASSERT) NIL)))))
                     ("2" (CASE-REPLACE "l(w!1) = 2")
                      (("1" (ASSERT)
                        (("1" (EXPAND "walk?")
                          (("1" (FLATTEN)
                            (("1" (INST -5 "0")
                              (("1"
                                (ASSERT)
                                (("1"
                                  (EXPAND "del_verts")
                                  (("1"
                                    (EXPAND "edge?")
                                    (("1"
                                      (EXPAND "fseq")
                                      (("1"
                                        (ASSERT)
                                        NIL)))))))))))))))))
                       ("2"
                        (CASE "FORALL (i: below(l(w!1))): seq(w!1)(i) = s!1 OR seq(w!1)(i) = t!1")
                        (("1" (EXPAND "walk?")
                          (("1" (FLATTEN)
                            (("1" (HIDE -5)
                              (("1"
                                (EXPAND "verts_in?")
                                (("1"
                                  (EXPAND "del_verts")
                                  (("1"
                                    (EXPAND "difference")
                                    (("1"
                                      (EXPAND "member")
                                      (("1"
                                        (LEMMA "prewalk_across")
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (EXPAND "fseq")
                                              (("1"
                                                (SKOSIMP*)
                                                (("1"
                                                  (INST -5 "i!1+1")
                                                  (("1"
                                                    (ASSERT)
                                                    (("1"
                                                      (FLATTEN)
                                                      (("1"
                                                        (ASSERT)
                                                        (("1"
                                                          (REPLACE -3)
                                                          (("1"
                                                            (REPLACE
                                                             -6)
                                                            (("1"
                                                              (EXPAND
                                                               "edge?")
                                                              (("1"
                                                                (REVEAL
                                                                 -3)
                                                                (("1"
                                                                  (INST
                                                                   -1
                                                                   "i!1")
                                                                  (("1"
                                                                    (ASSERT)
                                                                    (("1"
                                                                      (EXPAND
                                                                       "edge?")
                                                                      (("1"
                                                                        (EXPAND
                                                                         "del_verts")
                                                                        (("1"
                                                                          (EXPAND
                                                                           "fseq")
                                                                          (("1"
                                                                            (PROPAX)
                                                                            NIL)))))))))))))))))))))))))))))))))))))))))))))))))))
                         ("2" (LEMMA "walk_verts_in")
                          (("2" (INST?)
                            (("1" (SPLIT -1)
                              (("1"
                                (HIDE -4)
                                (("1"
                                  (EXPAND "verts_in?")
                                  (("1"
                                    (EXPAND "del_verts")
                                    (("1"
                                      (EXPAND "difference")
                                      (("1"
                                        (EXPAND "member")
                                        (("1"
                                          (SKOSIMP*)
                                          (("1"
                                            (INST?)
                                            (("1"
                                              (FLATTEN)
                                              (("1"
                                                (ASSERT)
                                                NIL)))))))))))))))))
                               ("2" (PROPAX) NIL)))
                             ("2" (HIDE -1 -2 -3 2 3 4 5 6)
                              (("2"
                                (LEMMA "finite_subset[T]")
                                (("2"
                                  (INST?)
                                  (("2"
                                    (INST -1 "vert(G!1)")
                                    (("2"
                                      (ASSERT)
                                      (("2"
                                        (HIDE 2)
                                        (("2"
                                          (GRIND)
                                          NIL)))))))))))))))))))))))))))))))))))))))))
 (|min_sep_set_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "sep_set_exists") (("" (INST?) NIL)))))
 (|min_sep_set_edge| "" (SKOSIMP*)
  (("" (EXPAND "separable?")
    (("" (EXPAND "min_sep_set")
      ((""
        (LEMMA "min_in[seps(G!1, s!1, t!1),
                (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
                (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
        (("1"
          (TYPEPRED
           "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
           (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
          (("1" (EXPAND "minimal?")
            (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL)))))))
           ("2" (LEMMA "sep_set_exists")
            (("2" (INST?)
              (("2" (ASSERT)
                (("2" (SKOSIMP*) (("2" (INST?) NIL)))))))))))
         ("2" (LEMMA "sep_set_exists") (("2" (INST?) NIL)))))))))))
 (|min_sep_set_card| "" (SKOSIMP*)
  (("" (EXPAND "min_sep_set")
    ((""
      (LEMMA "min_is_min[seps(G!1, s!1, t!1),
                (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
                (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
      (("1" (INST -1 "V!1")
        (("1" (BETA) (("1" (ASSERT) NIL)))
         ("2" (HIDE 2)
          (("2" (GROUND)
            (("1" (EXPAND "separates")
              (("1" (FLATTEN)
                (("1" (INST 4 "gen_seq1(G!1,s!1)")
                  (("1" (EXPAND "walk_from?")
                    (("1" (EXPAND "gen_seq1")
                      (("1" (EXPAND "walk?")
                        (("1" (EXPAND "verts_in?")
                          (("1" (SKOSIMP*)
                            (("1" (EXPAND "del_verts")
                              (("1"
                                (EXPAND "difference")
                                (("1"
                                  (EXPAND "member")
                                  (("1"
                                    (PROPAX)
                                    NIL)))))))))))))))))))))))
             ("2" (EXPAND "separates")
              (("2" (FLATTEN)
                (("2" (INST 4 "gen_seq2(G!1,s!1,t!1)")
                  (("2" (EXPAND "walk_from?")
                    (("2" (EXPAND "gen_seq2")
                      (("2" (EXPAND "del_verts")
                        (("2" (EXPAND "walk?")
                          (("2" (SPLIT 4)
                            (("1" (EXPAND "verts_in?")
                              (("1"
                                (SKOSIMP*)
                                (("1"
                                  (EXPAND "difference")
                                  (("1"
                                    (EXPAND "member")
                                    (("1" (GROUND) NIL)))))))))
                             ("2" (SKOSIMP*)
                              (("2"
                                (EXPAND "fseq")
                                (("2"
                                  (EXPAND "edge?")
                                  (("2"
                                    (ASSERT)
                                    (("2"
                                      (SKOSIMP*)
                                      (("2"
                                        (EXPAND "in?")
                                        (("2"
                                          (GROUND)
                                          NIL)))))))))))))))))))))))))))))))))))
       ("2" (LEMMA "sep_set_exists") (("2" (INST?) NIL)))))))))
 (|min_sep_set_seps| "" (SKOSIMP*)
  (("" (EXPAND "separable?")
    (("" (FLATTEN)
      ((""
        (LEMMA "min_in[seps(G!1, s!1, t!1),
                (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
                (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
        (("1"
          (TYPEPRED
           "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
           (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
          (("1" (ASSERT)
            (("1" (EXPAND "min_sep_set") (("1" (PROPAX) NIL)))))
           ("2" (SKOSIMP*) (("2" (INST?) NIL)))))
         ("2" (LEMMA "sep_set_exists") (("2" (INST?) NIL)))))))))))
 (|min_sep_set_vert| "" (SKOSIMP*)
  ((""
    (TYPEPRED
     "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)),
          (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]")
    (("1" (HIDE -2 -3 -4)
      (("1" (EXPAND "minimal?")
        (("1" (INST -1 "remove(v!1,(min_sep_set(G!1, s!1, t!1)))")
          (("1" (REWRITE "card_remove[T]")
            (("1" (ASSERT)
              (("1" (EXPAND "min_sep_set" -1) (("1" (ASSERT) NIL)))))))
           ("2" (SPLIT 1)
            (("1" (FLATTEN)
              (("1" (LEMMA "min_sep_set_edge")
                (("1" (INST?)
                  (("1" (SPLIT -1)
                    (("1" (REPLACE -1) (("1" (PROPAX) NIL)))
                     ("2" (HIDE -1)
                      (("2" (EXPAND "separable?")
                        (("2" (FLATTEN)
                          (("2" (ASSERT) NIL)))))))))))))))
             ("2" (FLATTEN)
              (("2" (GROUND)
                (("2" (LEMMA "min_sep_set_seps")
                  (("2" (INST?)
                    (("2" (ASSERT)
                      (("2" (EXPAND "separates")
                        (("2" (FLATTEN)
                          (("2" (EXPAND "remove")
                            (("2" (EXPAND "member")
                              (("2"
                                (ASSERT)
                                (("2"
                                  (SKOSIMP*)
                                  (("2"
                                    (INST 3 "w!1")
                                    (("2"
                                      (EXPAND "walk_from?")
                                      (("2"
                                        (FLATTEN)
                                        (("2"
                                          (EXPAND "walk?")
                                          (("2"
                                            (FLATTEN)
                                            (("2"
                                              (ASSERT)
                                              (("2"
                                                (SPLIT 3)
                                                (("1"
                                                  (HIDE -4)
                                                  (("1"
                                                    (EXPAND
                                                     "verts_in?")
                                                    (("1"
                                                      (SKOSIMP*)
                                                      (("1"
                                                        (EXPAND
                                                         "del_verts")
                                                        (("1"
                                                          (EXPAND
                                                           "difference")
                                                          (("1"
                                                            (EXPAND
                                                             "member")
                                                            (("1"
                                                              (INST
                                                               -3
                                                               "i!1")
                                                              (("1"
                                                                (FLATTEN)
                                                                (("1"
                                                                  (ASSERT)
                                                                  NIL)))))))))))))))))
                                                 ("2"
                                                  (HIDE -3)
                                                  (("2"
                                                    (SKOSIMP*)
                                                    (("2"
                                                      (INST?)
                                                      (("2"
                                                        (ASSERT)
                                                        (("2"
                                                          (EXPAND
                                                           "del_verts")
                                                          (("2"
                                                            (EXPAND
                                                             "edge?")
                                                            (("2"
                                                              (EXPAND
                                                               "fseq")
                                                              (("2"
                                                                (FLATTEN)
                                                                (("2"
                                                                  (ASSERT)
                                                                  (("2"
                                                                    (SKOSIMP*)
                                                                    (("2"
                                                                      (INST
                                                                       -7
                                                                       "v!2")
                                                                      (("2"
                                                                        (EXPAND
                                                                         "in?")
                                                                        (("2"
                                                                          (ASSERT)
                                                                          (("2"
                                                                            (SPLIT
                                                                             -7)
                                                                            (("1"
                                                                              (PROPAX)
                                                                              NIL)
                                                                             ("2"
                                                                              (CASE-REPLACE
                                                                               "v!1 = v!2")
                                                                              (("1"
                                                                                (HIDE
                                                                                 -1
                                                                                 -3
                                                                                 -5
                                                                                 -6
                                                                                 -7
                                                                                 -8
                                                                                 -9
                                                                                 1
                                                                                 2
                                                                                 3
                                                                                 4
                                                                                 5)
                                                                                (("1"
                                                                                  (REVEAL
                                                                                   -9)
                                                                                  (("1"
                                                                                    (EXPAND
                                                                                     "verts_in?")
                                                                                    (("1"
                                                                                      (EXPAND
                                                                                       "del_verts")
                                                                                      (("1"
                                                                                        (EXPAND
                                                                                         "difference")
                                                                                        (("1"
                                                                                          (EXPAND
                                                                                           "member")
                                                                                          (("1"
                                                                                            (SPLIT
                                                                                             -3)
                                                                                            (("1"
                                                                                              (INST?)
                                                                                              (("1"
                                                                                                (FLATTEN)
                                                                                                (("1"
                                                                                                  (ASSERT)
                                                                                                  NIL)))))
                                                                                             ("2"
                                                                                              (INST?)
                                                                                              (("2"
                                                                                                (FLATTEN)
                                                                                                (("2"
                                                                                                  (ASSERT)
                                                                                                  NIL)))))))))))))))))))
                                                                               ("2"
                                                                                (ASSERT)
                                                                                NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     ("2" (LEMMA "sep_set_exists")
      (("2" (INST?) (("2" (SKOSIMP*) (("2" (INST?) NIL)))))))
     ("3" (ASSERT)
      (("3" (LEMMA "sep_set_exists") (("3" (INST?) NIL)))))))))
 (|ends_not_in_min_sep_set| "" (SKOSIMP*)
  (("" (LEMMA "min_sep_set_seps")
    (("" (INST?)
      (("" (ASSERT)
        (("" (EXPAND "separates")
          (("" (FLATTEN) (("" (HIDE 3) (("" (GROUND) NIL)))))))))))))))
 (|walk?_del_verts_not| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (SPLIT +)
      (("1" (FLATTEN)
        (("1" (HIDE -2)
          (("1" (EXPAND "verts_in?")
            (("1" (SKOSIMP*)
              (("1" (EXPAND "del_verts")
                (("1" (EXPAND "intersection")
                  (("1" (EXPAND "empty?")
                    (("1" (EXPAND "difference")
                      (("1" (EXPAND "member")
                        (("1" (INST?)
                          (("1" (ASSERT)
                            (("1" (INST?)
                              (("1"
                                (ASSERT)
                                (("1"
                                  (EXPAND "verts_of")
                                  (("1"
                                    (INST?)
                                    (("1"
                                      (EXPAND "fseq")
                                      (("1"
                                        (PROPAX)
                                        NIL)))))))))))))))))))))))))))))))))
       ("2" (SKOSIMP*)
        (("2" (EXPAND "edge?")
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (ASSERT)
                (("2" (EXPAND "del_verts")
                  (("2" (EXPAND "empty?")
                    (("2" (EXPAND "intersection")
                      (("2" (EXPAND "member")
                        (("2" (SKOSIMP*)
                          (("2" (INST?)
                            (("2" (EXPAND "in?")
                              (("2"
                                (EXPAND "verts_of")
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (SPLIT -3)
                                    (("1" (INST?) (("1" (ASSERT) NIL)))
                                     ("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|adj_verts_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[T]")
    (("" (INST?)
      (("" (INST -1 "vert(G!1)")
        (("" (ASSERT)
          (("" (HIDE 2)
            (("" (TYPEPRED "G!1") (("" (GRIND) NIL))))))))))))))))
$$$di_subgraphs.pvs
di_subgraphs[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T]
   V: VAR set[T]
   G,G1,G2,SS: VAR digraph[T]
   i: VAR T
   e: VAR edgetype[T]
   di_subgraph?(G1,G2): bool = subset?(vert(G1),vert(G2)) AND
                            subset?(edges(G1),edges(G2))
   equal?(G1,G2): bool = di_subgraph?(G1,G2) AND di_subgraph?(G2,G1)
   di_subgraph(G): TYPE = {S: digraph[T] | di_subgraph?(S,G)}
   finite_vert_subset: LEMMA is_finite(LAMBDA (i:T): vert(G)(i) AND V(i))
%   di_subgraph(G, V): di_subgraph(G) =
%       (G WITH [vert :=  {i | vert(G)(i) AND V(i)},
%                edges := {e | edges(G)(e) AND
%                              (FORALL (x: T): in?(x,e) IMPLIES V(x))}])
   x,y: VAR T
   di_subgraph(G, V): di_subgraph(G) =
       (G WITH [vert :=  {i | vert(G)(i) AND V(i)},
                edges := {e | edges(G)(e) AND (Let (x,y) = e IN V(x) AND V(y))}])
   di_subgraph_vert_sub: LEMMA subset?(V,vert(G)) IMPLIES
                                        vert(di_subgraph(G,V)) = V
   di_subgraph_lem     : LEMMA di_subgraph?(di_subgraph(G,V),G)
   di_subgraph_smaller: LEMMA di_subgraph?(SS, G) IMPLIES
   	                     size(SS) <= size(G)
END di_subgraphs
$$$di_subgraphs.prf
(|di_subgraphs|
 (|finite_vert_subset| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[T]")
    (("" (INST?)
      (("" (INST -1 "vert(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|di_subgraph_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[edgetype[T]]")
    (("" (INST?)
      (("" (INST -1 "edges(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|di_subgraph_TCC2| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[T]")
    (("" (INST?)
      (("" (INST -1 "vert(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|di_subgraph_TCC3| "" (SKOSIMP*)
  (("" (PROP)
    (("1" (SKOSIMP*)
      (("1" (INST-CP -2 "y!1")
        (("1" (INST -2 "x!1")
          (("1" (EXPAND "in?")
            (("1" (ASSERT)
              (("1" (TYPEPRED "G!1")
                (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))
     ("2" (EXPAND "di_subgraph?")
      (("2" (PROP) (("1" (GRIND) NIL) ("2" (GRIND) NIL)))))))))
 (|di_subgraph_vert_sub| "" (SKOSIMP*)
  (("" (EXPAND "di_subgraph")
    (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
      (("" (EXPAND "subset?")
        (("" (INST?)
          (("" (EXPAND "member")
            (("" (IFF 1) (("" (GROUND) NIL)))))))))))))))
 (|di_subgraph_lem| "" (SKOSIMP*) (("" (ASSERT) NIL)))
 (|di_subgraph_smaller| "" (SKOSIMP*)
  (("" (EXPAND "size")
    (("" (EXPAND "di_subgraph?")
      (("" (REWRITE "card_subset[T]") NIL))))))))
$$$path_ops.pvs
path_ops[T: TYPE]: THEORY
BEGIN
   IMPORTING paths[T], di_subgraphs[T], sep_sets[T], digraph_ops[T]
   G: VAR digraph[T]
   v,s,t: VAR T
   e: VAR edgetype[T]
   W,V: VAR finite_set[T]
   w: VAR prewalk
   walk?_del_vert     : LEMMA walk?(del_vert(G, v), w) IMPLIES walk?[T](G, w)
   walk?_del_vert_not : LEMMA walk?(G, w) AND NOT verts_of(w)(v)
                                          IMPLIES walk?(del_vert(G, v), w)
   path?_del_vert     : LEMMA FORALL (w: prewalk): path?(del_vert(G, v), w)
                                                       IMPLIES path?[T](G, w)
   path?_del_verts    : LEMMA FORALL (w: prewalk): path?(del_verts(G, W), w)
                                                       IMPLIES path?[T](G, w)
   IMPORTING walk_inductions[T]
   walk_to_path      : LEMMA (EXISTS (w: prewalk): walk_from?(G,w,s,t)) IMPLIES
                                 (EXISTS (p: prewalk): path?(G,p) and
                                                   walk_from?(G,p,s,t))
   walk_to_path_from : LEMMA walk_from?(G,w,s,t) IMPLIES
                                 (EXISTS (p: prewalk): path_from?(G,p,s,t))
END path_ops
$$$path_ops.prf
(|path_ops|
 (|walk?_del_vert| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (FLATTEN)
      (("" (PROP)
        (("1" (HIDE -2)
          (("1" (EXPAND "verts_in?")
            (("1" (SKOSIMP*) (("1" (INST?) (("1" (GRIND) NIL)))))))))
         ("2" (HIDE -1)
          (("2" (SKOSIMP*)
            (("2" (INST?)
              (("2" (ASSERT)
                (("2" (LEMMA "edges_del_vert")
                  (("2" (EXPAND "edge?")
                    (("2" (INST?)
                      (("2" (ASSERT) NIL)))))))))))))))))))))))
 (|walk?_del_vert_not| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (FLATTEN)
      (("" (PROP)
        (("1" (HIDE -2)
          (("1" (EXPAND "verts_in?")
            (("1" (SKOSIMP*)
              (("1" (EXPAND "verts_of")
                (("1" (INST 2 "i!1")
                  (("1" (EXPAND "fseq")
                    (("1" (INST?)
                      (("1" (EXPAND "del_vert")
                        (("1" (EXPAND "remove")
                          (("1" (EXPAND "member")
                            (("1" (GROUND) NIL)))))))))))))))))))))
         ("2" (SKOSIMP*)
          (("2" (INST?)
            (("2" (HIDE -2)
              (("2" (EXPAND "del_vert")
                (("2" (EXPAND "edge?")
                  (("2" (ASSERT)
                    (("2" (ASSERT)
                      (("2" (EXPAND "verts_of")
                        (("2" (EXPAND "in?")
                          (("2" (EXPAND "fseq")
                            (("2" (SPLIT -2)
                              (("1" (INST?) (("1" (ASSERT) NIL)))
                               ("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|path?_del_vert| "" (SKOSIMP*)
  (("" (EXPAND "path?")
    (("" (FLATTEN)
      (("" (LEMMA "walk?_del_vert")
        (("" (INST?) (("" (ASSERT) NIL)))))))))))
 (|path?_del_verts| "" (SKOSIMP*)
  (("" (EXPAND "path?")
    (("" (FLATTEN)
      (("" (SPLIT +)
        (("1" (HIDE -2)
          (("1" (EXPAND "walk?")
            (("1" (FLATTEN)
              (("1" (SPLIT +)
                (("1" (HIDE -2)
                  (("1" (EXPAND "verts_in?")
                    (("1" (EXPAND "del_verts")
                      (("1" (EXPAND "difference")
                        (("1" (EXPAND "member")
                          (("1" (SKOSIMP*)
                            (("1" (INST?)
                              (("1" (ASSERT) NIL)))))))))))))))
                 ("2" (SKOSIMP*)
                  (("2" (EXPAND "fseq")
                    (("2" (INST?)
                      (("2" (ASSERT)
                        (("2" (EXPAND "edge?")
                          (("2" (ASSERT)
                            (("2" (EXPAND "del_verts")
                              (("2" (PROPAX) NIL)))))))))))))))))))))))
         ("2" (PROPAX) NIL)))))))))
 (|walk_to_path| "" (SKOLEM!)
  ((""
    (CASE "FORALL (w: prewalk): NOT walk_from?(G!1, w, s!1, t!1)
           OR (EXISTS (p: prewalk): path?(G!1, p) AND walk_from?(G!1, p, s!1, t!1))")
    (("1" (FLATTEN)
      (("1" (SKOSIMP*) (("1" (INST -1 "w!1") (("1" (ASSERT) NIL)))))))
     ("2" (HIDE 2)
      (("2" (INDUCT "w" 1 "digraph_induction_walk")
        (("2" (SKOSIMP*)
          (("2"
            (CASE "(EXISTS (i,j: below(l(w!1))): i /= j AND seq(w!1)(i) = seq(w!1)(j))")
            (("1" (SKOSIMP*)
              (("1" (CASE "i!1 < j!1")
                (("1" (INST -3 "w!1^(0,i!1) o w!1^(j!1+1,l(w!1)-1)")
                  (("1" (SPLIT -3)
                    (("1" (REWRITE "walk?_cut") NIL) ("2" (PROPAX) NIL)
                     ("3" (HIDE -2 -3 3)
                      (("3" (EXPAND "o ")
                        (("3" (EXPAND "^")
                          (("3" (EXPAND "emptyseq")
                            (("3" (LIFT-IF)
                              (("3" (GROUND) NIL)))))))))))))
                   ("2" (EXPAND "o ")
                    (("2" (EXPAND "^")
                      (("2" (LIFT-IF)
                        (("2" (EXPAND "emptyseq")
                          (("2" (PROPAX) NIL)))))))))))
                 ("2" (ASSERT)
                  (("2" (INST -2 "w!1^(0,j!1) o w!1^(i!1+1,l(w!1)-1)")
                    (("1" (ASSERT)
                      (("1" (SPLIT -2)
                        (("1" (HIDE 4)
                          (("1" (REWRITE "walk?_cut") NIL)))
                         ("2" (PROPAX) NIL)
                         ("3" (EXPAND "o ")
                          (("3" (EXPAND "^")
                            (("3" (LIFT-IF)
                              (("3"
                                (EXPAND "emptyseq")
                                (("3" (PROPAX) NIL)))))))))))))
                     ("2" (EXPAND "o ")
                      (("2" (EXPAND "^")
                        (("2" (EXPAND "emptyseq")
                          (("2" (LIFT-IF)
                            (("2" (GROUND) NIL)))))))))))))))))
             ("2" (HIDE -1)
              (("2" (INST 2 "w!1")
                (("2" (ASSERT)
                  (("2" (EXPAND "path?")
                    (("2" (EXPAND "walk_from?")
                      (("2" (FLATTEN)
                        (("2" (ASSERT)
                          (("2" (SKOSIMP*)
                            (("2" (EXPAND "fseq")
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|walk_to_path_from| "" (SKOSIMP*)
  (("" (LEMMA "walk_to_path")
    (("" (INST?)
      (("" (INST -1 "s!1" "t!1")
        (("" (SPLIT -1)
          (("1" (SKOSIMP*)
            (("1" (INST?)
              (("1" (EXPAND "path_from?")
                (("1" (ASSERT)
                  (("1" (EXPAND "walk_from?")
                    (("1" (FLATTEN)
                      (("1" (EXPAND "from?")
                        (("1" (ASSERT) NIL)))))))))))))))
           ("2" (INST?) NIL))))))))))))
$$$paths.pvs
paths[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T], walks[T], seq_def
   G: VAR digraph[T]
   x,y,s,t: VAR T
   i,j: VAR nat
   p,ps: VAR prewalk
   path?(G,ps): bool = walk?(G,ps) AND (FORALL (i,j: below(l(ps))):
                                          i /= j IMPLIES ps(i) /= ps(j))
   Path(G): TYPE = {p: prewalk | path?(G,p)}
   path_from?(G,ps,s,t): bool = path?(G,ps) AND from?(ps,s,t)
   Path_from(G,s,t): TYPE = {p: prewalk | path_from?(G,p,s,t)}
   endpoint?(i: nat, w: prewalk): bool = (i = 0) OR (i = l(w)-1)
   path?_verts     : LEMMA path?(G,ps) IMPLIES verts_in?(G,ps)
   path_from_l     : LEMMA path_from?(G,ps,s,t) AND s /= t IMPLIES l(ps) >= 2
   path_from_in    : LEMMA path_from?(G, ps, s, t) IMPLIES
                          vert(G)(s) AND vert(G)(t)
   path?_caret     : LEMMA i <= j AND j < l(ps) AND path?(G,ps)
                            IMPLIES path?(G,ps^(i,j))
   path_from?_caret: LEMMA  i <= j AND j < l(ps) AND path_from?(G, ps, s, t)
                         IMPLIES path_from?(G, ps^(i, j),seq(ps)(i),seq(ps)(j))
%%%%%%%%%%%%%%%%%%%% NOT TRUE fpr directed graphs %%%%%%%%%%%%%%%%%%%
%
%   path?_rev       : LEMMA path?(G,ps) IMPLIES path?(G,rev(ps))
   path?_gen_seq2  : LEMMA vert(G)(x) AND vert(G)(y) AND x /= y AND
                            edge?(G)(x,y) IMPLIES path?(G,gen_seq2(G,x,y))
   path?_add1      : LEMMA path?(G,p) AND vert(G)(x)
                            AND edge?(G)(seq(p)(l(p)-1),x)
                            AND NOT verts_of(p)(x)
                            IMPLIES path?(G,add1(p,x))
   path?_trunc1      : LEMMA path?(G,p) AND l(p) > 1 IMPLIES
                            path_from?(G,trunc1(p),seq(p)(0),seq(p)(l(p)-2))
END paths
$$$paths.prf
(|paths|
 (|path?_verts| "" (SKOSIMP*)
  (("" (EXPAND "path?")
    (("" (EXPAND "walk?") (("" (FLATTEN) (("" (PROPAX) NIL)))))))))
 (|path_from_l| "" (SKOSIMP*)
  (("" (EXPAND "path_from?")
    (("" (FLATTEN)
      (("" (EXPAND "path?")
        (("" (FLATTEN)
          (("" (EXPAND "from?")
            (("" (FLATTEN)
              (("" (EXPAND "fseq")
                (("" (INST -2 "0" "(l(ps!1)-1)")
                  (("" (SPLIT -2)
                    (("1" (ASSERT) NIL)
                     ("2" (ASSERT) NIL)))))))))))))))))))))
 (|path_from_in| "" (SKOSIMP*)
  (("" (EXPAND "path_from?")
    (("" (FLATTEN)
      (("" (EXPAND "path?")
        (("" (FLATTEN)
          (("" (HIDE -2)
            (("" (EXPAND "walk?")
              (("" (FLATTEN)
                (("" (HIDE -2)
                  (("" (EXPAND "from?")
                    (("" (EXPAND "verts_in?")
                      (("" (FLATTEN)
                        (("" (INST-CP -1 "0")
                          (("" (INST -1 "l(ps!1) - 1")
                            (("" (ASSERT)
                              NIL)))))))))))))))))))))))))))))
 (|path?_caret_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path?_caret_TCC2| "" (SUBTYPE-TCC) NIL)
 (|path?_caret| "" (SKOSIMP*)
  (("" (EXPAND "path?")
    (("" (EXPAND "fseq")
      (("" (FLATTEN)
        (("" (SPLIT 1)
          (("1" (EXPAND "walk?")
            (("1" (SPLIT 1)
              (("1" (FLATTEN)
                (("1" (HIDE -4 -5)
                  (("1" (EXPAND "verts_in?")
                    (("1" (SKOSIMP*)
                      (("1" (TYPEPRED "i!2")
                        (("1" (EXPAND "^")
                          (("1" (LIFT-IF)
                            (("1" (ASSERT) (("1" (INST?) NIL)))))))
                         ("2" (SKOSIMP*) NIL)))))))))))
               ("2" (SKOSIMP*)
                (("2" (HIDE -6)
                  (("2" (EXPAND "fseq")
                    (("2" (EXPAND "edge?")
                      (("2" (INST - "n!1+i!1")
                        (("2" (EXPAND "^")
                          (("2" (ASSERT) NIL)))))))))))))))))
           ("2" (SKOSIMP*)
            (("2" (EXPAND "^")
              (("2" (ASSERT)
                (("2" (INST - "i!1+i!2" "i!1+j!2")
                  (("1" (ASSERT) NIL)
                   ("2" (TYPEPRED "i!2")
                    (("2" (TYPEPRED "j!2")
                      (("2" (EXPAND "^") (("2" (ASSERT) NIL)))))))
                   ("3" (TYPEPRED "i!2")
                    (("3" (TYPEPRED "i!1")
                      (("3" (EXPAND "^")
                        (("3" (ASSERT) NIL)))))))))))))))))))))))))
 (|path_from?_caret_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path_from?_caret_TCC2| "" (SUBTYPE-TCC) NIL)
 (|path_from?_caret_TCC3| "" (SUBTYPE-TCC) NIL)
 (|path_from?_caret| "" (SKOSIMP*)
  (("" (EXPAND "path_from?")
    (("" (FLATTEN)
      (("" (REWRITE "path?_caret")
        (("" (EXPAND "from?")
          (("" (EXPAND "^") (("" (ASSERT) NIL)))))))))))))
 (|path?_gen_seq2_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path?_gen_seq2_TCC2| "" (SUBTYPE-TCC) NIL)
 (|path?_gen_seq2| "" (SKOSIMP*)
  (("" (EXPAND "gen_seq2")
    (("" (EXPAND "path?")
      (("" (EXPAND "fseq")
        (("" (SPLIT +)
          (("1" (EXPAND "walk?")
            (("1" (SPLIT +)
              (("1" (EXPAND "verts_in?") (("1" (PROPAX) NIL)))
               ("2" (SKOSIMP*)
                (("2" (EXPAND "fseq")
                  (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))
           ("2" (SKOSIMP*)
            (("2" (EXPAND "edge?")
              (("2" (LIFT-IF) (("2" (GROUND) NIL)))))))))))))))))
 (|path?_add1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path?_add1| "" (SKOSIMP*)
  (("" (EXPAND "path?")
    (("" (FLATTEN)
      (("" (SPLIT +)
        (("1" (REWRITE "walk?_add1") NIL)
         ("2" (SKOSIMP*)
          (("2" (EXPAND "fseq")
            (("2" (EXPAND "add1")
              (("2" (LIFT-IF)
                (("2" (LIFT-IF)
                  (("2" (EXPAND "verts_of")
                    (("2" (TYPEPRED "i!1")
                      (("2" (TYPEPRED "j!1")
                        (("2" (EXPAND "add1")
                          (("2" (GROUND)
                            (("1" (INST - "i!1" "j!1")
                              (("1" (ASSERT) NIL)))
                             ("2" (EXPAND "fseq")
                              (("2"
                                (INST + "j!1")
                                (("2" (ASSERT) NIL)))))
                             ("3" (INST + "i!1")
                              (("3"
                                (EXPAND "fseq")
                                (("3"
                                  (PROPAX)
                                  NIL)))))))))))))))))))))))))))))))))
 (|path?_trunc1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|path?_trunc1_TCC2| "" (SUBTYPE-TCC) NIL)
 (|path?_trunc1_TCC3| "" (SUBTYPE-TCC) NIL)
 (|path?_trunc1| "" (SKOSIMP*)
  (("" (EXPAND "path_from?")
    (("" (SPLIT 1)
      (("1" (EXPAND "trunc1")
        (("1" (LEMMA "path?_caret")
          (("1" (INST?) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
       ("2" (EXPAND "from?")
        (("2" (EXPAND "trunc1")
          (("2" (EXPAND "^") (("2" (ASSERT) NIL))))))))))))))
$$$finite_sets_more.pvs
finite_sets_more[T: TYPE]: THEORY
BEGIN
  IMPORTING finite_sets
  S: VAR set[T]
  is_finite_surj: LEMMA (EXISTS (N: posnat), (f: [below[N] -> (S)]):
                             surjective?(f)) IMPLIES is_finite(S)
END finite_sets_more
$$$finite_sets_more.prf
(|finite_sets_more|
 (|is_finite_surj| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N!1" "inverse(f!1)")
      (("1" (REWRITE "inj_inv") (("1" (INST 1 "0") NIL)))
       ("2" (INST + "0") NIL))))))))
$$$seq_def.pvs
seq_def[T: TYPE]: THEORY
BEGIN
  finite_seq: TYPE = [# l: nat, seq: [below[l] -> T] #]
  fs, fs1, fs2, fs3: VAR finite_seq
  m, n: VAR nat
  fin_seq(n): TYPE = {fs | l(fs) = n}
  fseq(fs): [below[l(fs)] -> T] = seq(fs)
  CONVERSION fseq
  o(fs1, fs2): finite_seq =
     LET l1 = l(fs1),
         lsum = l1 + l(fs2)
      IN (# l := lsum,
            seq := (LAMBDA (n:below[lsum]):
                      IF n < l1
                         THEN seq(fs1)(n)
                         ELSE seq(fs2)(n-l1)
                      ENDIF) #);
  emptyarr(x: below[0]): T
  emptyseq: fin_seq(0) = (# l := 0, seq := emptyarr #) ;
  p: VAR [nat, nat] ;
  ^(fs: finite_seq, (p: [nat, below(l(fs))])):
       fin_seq(IF proj_1(p) > proj_2(p) THEN 0
               ELSE proj_2(p)-proj_1(p)+1 ENDIF) =
    LET (m, n) = p
     IN IF m > n
        THEN emptyseq
        ELSE (# l := n-m+1,
                seq := (LAMBDA (x: below[n-m+1]): seq(fs)(x + m)) #)
        ENDIF ;
  rev(fs): finite_seq = (# l := l(fs),
                           seq := (LAMBDA (i: below(l(fs))): seq(fs)(l(fs)-1-i))
                         #)
%%  ^(fs: finite_seq, (p: [m: nat, {n: nat | n >= m AND n < l(fs)}])):
%%       fin_seq(proj_2(p)-proj_1(p)+1) =
%%    LET (m, n) = p IN
%%             (# l   := n-m+1,
%%                seq := (LAMBDA (x: below[n-m+1]): seq(fs)(x + m)) #) ;
%
%
%  ^^(fs, p): finite_seq =
%    LET (m, n) = p
%     IN IF m > n OR m >= l(fs)
%        THEN emptyseq
%        ELSE LET len = IF n < l(fs)  THEN n - m + 1
%                       ELSE l(fs) - m ENDIF
%              IN (# l := len,
%                    seq := (LAMBDA (x: below[len]): seq(fs)(x + m)) #)
%        ENDIF ;
%
%  i,j: VAR nat
%  extractors_eq: LEMMA j < l(fs) IMPLIES fs^(i,j) = fs^^(i,j)
END seq_def
$$$seq_def.prf
(|seq_def| (|oh_TCC1| "" (SUBTYPE-TCC) NIL) (|oh_TCC2| "" (SUBTYPE-TCC) NIL)
 (|emptyarr_TCC1| "" (INST 1 "(LAMBDA (x: below[0]): epsilon! (t:T): true)") (("" (SKOSIMP*) NIL)))
 (|emptyseq_TCC1| "" (PROPAX) NIL) (|caret_TCC1| "" (SUBTYPE-TCC) NIL) (|caret_TCC2| "" (SUBTYPE-TCC) NIL)
 (|caret_TCC3| "" (SUBTYPE-TCC) NIL) (|caret_TCC4| "" (SUBTYPE-TCC) NIL) (|caret_TCC5| "" (SUBTYPE-TCC) NIL)
 (|rev_TCC1| "" (SUBTYPE-TCC) NIL))
$$$walks.pvs
walks[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T], seq_def, finite_sets@finite_sets_eq,
             finite_sets_more
   G,GG: VAR digraph[T]
   n: VAR nat
   x,u,v,u1,u2,v1,v2,v3: VAR T
   e: VAR edgetype[T]
   i,j: VAR nat
   prewalk: TYPE = {w: finite_seq[T] | l(w) > 0}
   s,ps,ww: VAR prewalk
   verts_in?(G,s): bool = (FORALL (i: below(l(s))): vert(G)(seq(s)(i)))
   Seq(G): TYPE = {w: prewalk | verts_in?(G,w)}
   walk?(G,ps): bool = verts_in?(G,ps) AND
                             (FORALL n: n < l(ps) - 1 IMPLIES
                                         edge?(G)(ps(n),ps(n+1)))
   Walk(G): TYPE = {w: prewalk | walk?(G,w)}
   from?(ps,u,v): bool = seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v
   walk_from?(G,ps,u,v): bool =
	          seq(ps)(0) = u AND seq(ps)(l(ps) - 1) = v AND walk?(G,ps)
   Walk_from(G,u,v): TYPE = {w: prewalk | walk_from?(G,w,u,v)}
   walk_from_l     : LEMMA walk_from?(G,ps,u,v) AND u /= v IMPLIES l(ps) >= 2
   verts_of(ww: prewalk): finite_set[T] =
               {t: T | (EXISTS (i: below(l(ww))): ww(i) = t)}
   edges_of(ww): finite_set[edgetype[T]] = {e: edgetype[T] |
                           EXISTS (i: below(l(ww)-1)): e = (ww(i),ww(i+1))}
   pre_circuit?(G: digraph[T], w: prewalk): bool = walk?(G,w) AND
                                                 w(0) = w(l(w)-1)
%  ----------------------- Properties -----------------------
   verts_in?_concat: LEMMA FORALL (s1,s2: Seq(G)): verts_in?(G,s1 o s2)
   verts_in?_caret : LEMMA FORALL (j: below(l(ps))): i <= j IMPLIES
                                   verts_in?(G,ps) IMPLIES verts_in?(G,ps^(i,j))
   vert_seq_lem    : LEMMA FORALL (w: Seq(G)): n < l(w) IMPLIES vert(G)(w(n))
   verts_of_subset : LEMMA FORALL (w: Seq(G)):
                                   subset?(verts_of(w),vert(G))
   edges_of_subset : LEMMA walk?(G,ww) IMPLIES subset?(edges_of(ww),edges(G))
   walk_verts_in   : LEMMA walk?(G,ps) IMPLIES verts_in?(G,ps)
   walk_from_vert  : LEMMA FORALL (w: prewalk,v1,v2:T):
                             walk_from?(G,w,v1,v2) IMPLIES
                                vert(G)(v1) AND vert(G)(v2)
   walk_edge_in    : LEMMA walk?(G,ww) AND
                           subset?(edges_of(ww),edges(GG)) AND
                           subset?(verts_of(ww),vert(GG))
                         IMPLIES walk?(GG,ww)
   prewalk_across: LEMMA ww(0) /= ww(l(ww)-1) AND l(ww) > 1 IMPLIES
                        (EXISTS (i: below(l(ww)-1)): ww(i) = ww(0) AND
                                                  ww(i+1) /= ww(0))
%  ----------- operations and constructors for walks --------------------
   gen_seq1(G, (u: (vert(G)))): Seq(G) =
                        (# l := 1, seq := (LAMBDA (i: below(1)): u) #)
   gen_seq2(G, (u,v: (vert(G)))): Seq(G) =
                  (# l := 2,
                     seq := (LAMBDA (i: below(2)):
                                      IF i = 0 THEN u ELSE v ENDIF) #)
   Longprewalk: TYPE = {ps: prewalk | l(ps) >= 2}
   trunc1(p: Longprewalk ): prewalk = p^(0,l(p)-2)
   add1(ww,x): prewalk = (# l := l(ww) + 1,
                           seq := (LAMBDA (ii: below(l(ww) + 1)):
                                    IF ii < l(ww) THEN seq(ww)(ii) ELSE x ENDIF)
                         #)
   gen_seq1_is_walk: LEMMA vert(G)(x) IMPLIES walk?(G,gen_seq1(G,x))
   edge_to_walk    : LEMMA u /= v AND edges(G)((u, v)) IMPLIES
                             walk?(G,gen_seq2(G,u,v))
   w1,w2: VAR prewalk
%%%%%%%%%%%%%%%%%%%%% NOT THEOREMS for directed graphs %%%%%%%%%%%%%%
%
%   walk?_rev       : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps))
%
%
%
%   walk?_reverse   : LEMMA walk_from?(G,w1,v1,v2) IMPLIES
%                             (EXISTS (w: Walk(G)): walk_from?(G,w,v2,v1))
   walk?_caret     : LEMMA i <= j AND j < l(ps) AND walk?(G,ps)
                               IMPLIES walk?(G,ps^(i,j))
   l_trunc1        : LEMMA l(ww) > 1 IMPLIES l(trunc1(ww)) = l(ww)-1
   walk?_add1      : LEMMA walk?(G,ww) AND vert(G)(x)
                           AND edge?(G)(seq(ww)(l(ww)-1),x)
                           IMPLIES walk?(G,add1(ww,x))
   walk_concat_edge: LEMMA walk_from?(G, w1, u1, v1) AND
         		           walk_from?(G, w2, u2, v2) AND
                              edge?(G)(v1,u2)
         		        IMPLIES
         		            walk_from?(G, w1 o w2,u1,v2)
   walk_concat: LEMMA l(w1) > 1 AND
      		      walk_from?(G, w1, u1, v) AND
      		      walk_from?(G, w2, v, u2)
      		 IMPLIES
      		     walk_from?(G, w1 ^ (0, l(w1) - 2) o w2,u1,u2)
   walk?_cut  : LEMMA FORALL (i,j: below(l(ps))): i < j AND
                                  seq(ps)(i) = seq(ps)(j) AND
                                  walk_from?(G, ps, u, v)
                               IMPLIES
                                  walk_from?(G, ps^(0,i) o ps^(j+1,l(ps)-1),u,v)
   yt: VAR T
   p1,p2: VAR prewalk
   walk_merge: LEMMA walk_from?(G, p1, u, yt) AND
      	             walk_from?(G, p2, yt, v )
                           IMPLIES
      	                (EXISTS (p: prewalk): walk_from?(G, p, u, v))
END walks
$$$walks.prf
(|walks| (|walk?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|from?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|from?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|walk_from_l| "" (SKOSIMP*)
  (("" (EXPAND "walk_from?")
    (("" (FLATTEN)
      (("" (EXPAND "walk?")
        (("" (FLATTEN) (("" (INST - "0") (("" (ASSERT) NIL)))))))))))))
 (|verts_of_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "surjection_from_finite_set[below(l(ww!1)),T]")
    (("" (INST?)
      (("" (INST -1 "fullset[below(l(ww!1))]")
        (("1" (ASSERT)
          (("1" (HIDE 2)
            (("1" (INST 1 "(LAMBDA (i: below(l(ww!1))): seq(ww!1)(i))")
              (("1" (EXPAND "restrict")
                (("1" (EXPAND "surjective?")
                  (("1" (SKOSIMP*)
                    (("1" (TYPEPRED "y!1")
                      (("1" (SKOSIMP*)
                        (("1" (INST?)
                          (("1" (ASSERT)
                            (("1" (EXPAND "fseq")
                              (("1" (PROPAX) NIL)))))
                           ("2" (EXPAND "fullset")
                            (("2" (PROPAX) NIL)))))))))))))))
               ("2" (SKOSIMP*)
                (("2" (INST?)
                  (("2" (EXPAND "fseq") (("2" (PROPAX) NIL)))))))
               ("3" (SKOSIMP*)
                (("3" (EXPAND "fullset") (("3" (PROPAX) NIL)))))))))))
         ("2" (HIDE 2)
          (("2" (EXPAND "is_finite")
            (("2"
              (INST 1 "l(ww!1)" "(LAMBDA (ii: below(l(ww!1))): ii)")
              (("1" (EXPAND "injective?")
                (("1" (EXPAND "restrict") (("1" (SKOSIMP*) NIL)))))
               ("2" (SKOSIMP*)
                (("2" (EXPAND "fullset")
                  (("2" (PROPAX) NIL)))))))))))))))))))
 (|edges_of_TCC1| "" (SUBTYPE-TCC) NIL)
 (|edges_of_TCC2| "" (SUBTYPE-TCC) NIL)
 (|edges_of_TCC3| "" (SUBTYPE-TCC) NIL)
 (|edges_of_TCC4| "" (SKOSIMP*)
  (("" (CASE "l(ww!1) = 1")
    (("1"
      (CASE-REPLACE "{e: edgetype[T] |
                               EXISTS (i: below(l(ww!1) - 1)):
                                 e
                                     = (fseq[T](ww!1)(i),
                                        fseq[T](ww!1)(i + 1))} = emptyset[edgetype]")
      (("1" (REWRITE "finite_emptyset") NIL)
       ("2" (HIDE 2)
        (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
          (("2" (EXPAND "emptyset") (("2" (SKOSIMP*) NIL)))))))))
     ("2" (LEMMA "is_finite_surj[edgetype]")
      (("2" (INST?)
        (("2" (ASSERT)
          (("2" (HIDE 2)
            (("2"
              (INST + "l(ww!1)-1"
               "(LAMBDA (i: below(l(ww!1) - 1)): (fseq[T](ww!1)(i), fseq[T](ww!1)(i + 1)))")
              (("1" (EXPAND "surjective?")
                (("1" (HIDE 2)
                  (("1" (SKOSIMP*)
                    (("1" (TYPEPRED "y!1")
                      (("1" (SKOSIMP*)
                        (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))
               ("2" (HIDE 2)
                (("2" (SKOSIMP*)
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|pre_circuit?_TCC1| "" (SUBTYPE-TCC) NIL)
 (|pre_circuit?_TCC2| "" (SUBTYPE-TCC) NIL)
 (|verts_in?_concat_TCC1| "" (SUBTYPE-TCC) NIL)
 (|verts_in?_concat| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?")
    (("" (SKOSIMP*)
      (("" (TYPEPRED "i!1")
        (("" (EXPAND "o ")
          (("" (GROUND)
            (("1" (TYPEPRED "s1!1")
              (("1" (EXPAND "verts_in?") (("1" (INST?) NIL)))))
             ("2" (TYPEPRED "s2!1")
              (("2" (EXPAND "verts_in?")
                (("2" (INST?) NIL)))))))))))))))))
 (|verts_in?_caret_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?")
    (("" (EXPAND "^")
      (("" (EXPAND "emptyseq")
        (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))
 (|verts_in?_caret| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?")
    (("" (SKOSIMP*)
      (("" (INST?)
        (("1" (TYPEPRED "i!2")
          (("1" (EXPAND "^")
            (("1" (EXPAND "emptyseq")
              (("1" (LIFT-IF)
                (("1" (GROUND)
                  (("1" (TYPEPRED "i!2")
                    (("1" (EXPAND "^")
                      (("1" (TYPEPRED "j!1")
                        (("1" (REVEAL -1)
                          (("1" (INST?) NIL)))))))))))))))))))
         ("2" (TYPEPRED "i!1")
          (("2" (TYPEPRED "i!2")
            (("2" (EXPAND "^")
              (("2" (LIFT-IF)
                (("2" (EXPAND "emptyseq")
                  (("2" (GROUND) NIL)))))))))))))))))))
 (|vert_seq_lem| "" (SKOSIMP*)
  (("" (EXPAND "fseq")
    (("" (TYPEPRED "w!1")
      (("" (EXPAND "verts_in?") (("" (INST -1 "n!1") NIL)))))))))
 (|verts_of_subset| "" (SKOSIMP*)
  (("" (TYPEPRED "w!1")
    (("" (EXPAND "subset?")
      (("" (SKOSIMP*)
        (("" (EXPAND "verts_in?")
          (("" (EXPAND "member")
            (("" (EXPAND "verts_of")
              (("" (SKOSIMP*)
                (("" (EXPAND "fseq")
                  (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))))))
 (|edges_of_subset| "" (SKOSIMP*)
  (("" (EXPAND "subset?")
    (("" (SKOSIMP*)
      (("" (EXPAND "member")
        (("" (EXPAND "edges_of")
          (("" (EXPAND "fseq")
            (("" (SKOSIMP*)
              (("" (REPLACE -2)
                (("" (HIDE -2)
                  (("" (EXPAND "walk?")
                    (("" (FLATTEN)
                      (("" (INST - "i!1")
                        (("" (ASSERT)
                          (("" (EXPAND "edge?")
                            (("" (EXPAND "fseq")
                              ((""
                                (PROPAX)
                                NIL)))))))))))))))))))))))))))))))
 (|walk_verts_in| "" (SKOSIMP*)
  (("" (EXPAND "walk?") (("" (FLATTEN) (("" (PROPAX) NIL)))))))
 (|walk_from_vert| "" (SKOSIMP*)
  (("" (EXPAND "walk_from?")
    (("" (FLATTEN)
      (("" (EXPAND "walk?")
        (("" (FLATTEN)
          (("" (EXPAND "verts_in?")
            (("" (INST-CP -3 "0")
              (("" (INST -3 "l(w!1)-1")
                (("" (ASSERT) NIL)))))))))))))))))
 (|walk_edge_in| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (FLATTEN)
      (("" (SPLIT 1)
        (("1" (HIDE -2)
          (("1" (EXPAND "verts_in?")
            (("1" (SKOSIMP*)
              (("1" (INST?)
                (("1" (EXPAND "verts_of")
                  (("1" (HIDE -2)
                    (("1" (EXPAND "subset?")
                      (("1" (EXPAND "member")
                        (("1" (INST?)
                          (("1" (SPLIT -2)
                            (("1" (PROPAX) NIL)
                             ("2" (INST?)
                              (("2"
                                (EXPAND "fseq")
                                (("2"
                                  (PROPAX)
                                  NIL)))))))))))))))))))))))))
         ("2" (SKOSIMP*)
          (("2" (HIDE -5)
            (("2" (EXPAND "subset?")
              (("2" (EXPAND "member")
                (("2" (INST?)
                  (("2" (ASSERT)
                    (("2" (EXPAND "edge?")
                      (("2" (INST?)
                        (("2" (EXPAND "edges_of")
                          (("2" (ASSERT)
                            (("2" (INST + "n!1")
                              (("2"
                                (ASSERT)
                                NIL)))))))))))))))))))))))))))))))
 (|prewalk_across_TCC1| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC2| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC3| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC4| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC5| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC6| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across_TCC7| "" (SUBTYPE-TCC) NIL)
 (|prewalk_across| "" (SKOSIMP*)
  ((""
    (CASE "(FORALL (i: below(l(ww!1))): seq(ww!1)(i) = seq(ww!1)(0))")
    (("1" (INST -1 "l(ww!1)-1")
      (("1" (ASSERT) (("1" (EXPAND "fseq") (("1" (ASSERT) NIL)))))))
     ("2" (HIDE 3)
      (("2" (INDUCT "i")
        (("1" (ASSERT) NIL)
         ("2" (SKOSIMP*)
          (("2" (REVEAL 1)
            (("2" (INST + "jb!1")
              (("2" (EXPAND "fseq") (("2" (GROUND) NIL)))))))))))))))))
 (|gen_seq1_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?") (("" (PROPAX) NIL)))))
 (|gen_seq2_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "verts_in?") (("" (PROPAX) NIL)))))
 (|trunc1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|trunc1_TCC2| "" (SUBTYPE-TCC) NIL)
 (|add1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|gen_seq1_is_walk| "" (SKOSIMP*)
  (("" (EXPAND "gen_seq1")
    (("" (EXPAND "walk?")
      (("" (EXPAND "verts_in?") (("" (SKOSIMP*) NIL)))))))))
 (|edge_to_walk_TCC1| "" (SUBTYPE-TCC) NIL)
 (|edge_to_walk_TCC2| "" (SKOSIMP*)
  (("" (TYPEPRED "G!1") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|edge_to_walk| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (EXPAND "gen_seq2")
      (("" (SPLIT 2)
        (("1" (EXPAND "verts_in?") (("1" (PROPAX) NIL)))
         ("2" (SKOSIMP*)
          (("2" (EXPAND "fseq")
            (("2" (ASSERT)
              (("2" (EXPAND "edge?")
                (("2" (PROPAX) NIL)))))))))))))))))
 (|walk?_caret_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk?_caret_TCC2| "" (SUBTYPE-TCC) NIL)
 (|walk?_caret| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (FLATTEN)
      (("" (SPLIT +)
        (("1" (REWRITE "verts_in?_caret") NIL)
         ("2" (SKOSIMP*)
          (("2" (EXPAND "fseq")
            (("2" (EXPAND "edge?")
              (("2" (EXPAND "^")
                (("2" (ASSERT)
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|l_trunc1_TCC1| "" (SUBTYPE-TCC) NIL)
 (|l_trunc1| "" (SKOSIMP*)
  (("" (EXPAND "trunc1") (("" (EXPAND "^") (("" (ASSERT) NIL)))))))
 (|walk?_add1| "" (SKOSIMP*)
  (("" (EXPAND "walk?")
    (("" (FLATTEN)
      (("" (SPLIT 1)
        (("1" (EXPAND "verts_in?")
          (("1" (EXPAND "add1")
            (("1" (SKOSIMP*)
              (("1" (HIDE -2)
                (("1" (INST?)
                  (("1" (GROUND) NIL) ("2" (ASSERT) NIL)))))))))))
         ("2" (SKOSIMP*)
          (("2" (EXPAND "fseq")
            (("2" (EXPAND "add1")
              (("2" (LIFT-IF)
                (("2" (SPLIT 1)
                  (("1" (FLATTEN)
                    (("1" (INST?)
                      (("1" (LIFT-IF) (("1" (GROUND) NIL)))))))
                   ("2" (FLATTEN)
                    (("2" (PROPAX) NIL)))))))))))))))))))))
 (|walk_concat_edge_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk_concat_edge| "" (SKOSIMP*)
  (("" (EXPAND "walk_from?")
    (("" (FLATTEN)
      (("" (EXPAND "o ")
        (("" (ASSERT)
          (("" (AUTO-REWRITE "fseq")
            (("" (EXPAND "walk?")
              (("" (ASSERT)
                (("" (FLATTEN)
                  (("" (ASSERT)
                    (("" (SPLIT +)
                      (("1" (EXPAND "verts_in?")
                        (("1" (SKOSIMP*)
                          (("1" (HIDE -4)
                            (("1" (GROUND)
                              (("1" (INST?) NIL)
                               ("2"
                                (HIDE -3)
                                (("2" (INST?) NIL)))))))))))
                       ("2" (SKOSIMP*)
                        (("2" (CASE "n!1 < l(w1!1)")
                          (("1" (ASSERT)
                            (("1" (LIFT-IF)
                              (("1" (INST?) (("1" (GROUND) NIL)))))))
                           ("2" (ASSERT)
                            (("2" (HIDE -5)
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|walk_concat_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk_concat_TCC2| "" (SKOSIMP*)
  (("" (EXPAND "o ")
    (("" (EXPAND "^") (("" (LIFT-IF) (("" (GROUND) NIL)))))))))
 (|walk_concat| "" (SKOSIMP*)
  (("" (EXPAND "walk_from?")
    (("" (FLATTEN)
      (("" (ASSERT)
        (("" (EXPAND "o ")
          (("" (EXPAND "^")
            (("" (EXPAND "walk?")
              (("" (EXPAND "fseq")
                (("" (FLATTEN)
                  (("" (SPLIT +)
                    (("1" (EXPAND "verts_in?")
                      (("1" (SKOSIMP*)
                        (("1" (GROUND)
                          (("1" (INST?) NIL)
                           ("2" (HIDE -2 -3 -4 -5 -6 -7 -9)
                            (("2" (INST?) NIL)))))))))
                     ("2" (SKOSIMP*)
                      (("2" (EXPAND "edge?")
                        (("2" (CASE "n!1 < l(w1!1) - 1")
                          (("1" (ASSERT)
                            (("1" (INST?)
                              (("1"
                                (ASSERT)
                                (("1"
                                  (CASE "n!1 = l(w1!1) - 1")
                                  (("1"
                                    (REPLACE -1)
                                    (("1"
                                      (HIDE -1)
                                      (("1" (ASSERT) NIL)))))
                                   ("2"
                                    (LIFT-IF)
                                    (("2" (ASSERT) NIL)))))))))))
                           ("2" (ASSERT)
                            (("2" (HIDE -6)
                              (("2"
                                (INST?)
                                (("2"
                                  (ASSERT)
                                  NIL)))))))))))))))))))))))))))))))))
 (|walk?_cut_TCC1| "" (SUBTYPE-TCC) NIL)
 (|walk?_cut| "" (SKOSIMP*)
  (("" (EXPAND "walk_from?")
    (("" (FLATTEN)
      (("" (EXPAND "walk?")
        (("" (EXPAND "fseq")
          (("" (EXPAND "o ")
            (("" (EXPAND "^")
              (("" (EXPAND "emptyseq")
                (("" (SPLIT 1)
                  (("1" (PROPAX) NIL)
                   ("2" (FLATTEN)
                    (("2" (LIFT-IF)
                      (("2" (SPLIT 1)
                        (("1" (FLATTEN)
                          (("1" (EXPAND "verts_in?")
                            (("1" (HIDE -7)
                              (("1" (INST?) (("1" (GROUND) NIL)))))))))
                         ("2" (FLATTEN) (("2" (ASSERT) NIL)))))))))
                   ("3" (FLATTEN)
                    (("3" (EXPAND "verts_in?")
                      (("3" (SKOSIMP*)
                        (("3" (HIDE -6)
                          (("3" (SPLIT 1)
                            (("1" (FLATTEN)
                              (("1" (INST?) (("1" (ASSERT) NIL)))))
                             ("2" (FLATTEN)
                              (("2"
                                (ASSERT)
                                (("2"
                                  (TYPEPRED "i!2")
                                  (("2"
                                    (LIFT-IF)
                                    (("2"
                                      (GROUND)
                                      (("2"
                                        (INST?)
                                        NIL)))))))))))))))))))))
                   ("4" (SKOSIMP*)
                    (("4" (LIFT-IF)
                      (("4" (SPLIT 1)
                        (("1" (FLATTEN)
                          (("1" (GROUND)
                            (("1" (INST?) (("1" (ASSERT) NIL)))
                             ("2" (LIFT-IF)
                              (("2"
                                (SPLIT 2)
                                (("1"
                                  (FLATTEN)
                                  (("1" (INST?) (("1" (ASSERT) NIL)))))
                                 ("2"
                                  (FLATTEN)
                                  (("2"
                                    (ASSERT)
                                    (("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        (("2"
                                          (CASE "n!1 = i!1")
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (HIDE -1)
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (REPLACE -4)
                                                  (("1"
                                                    (REVEAL -2)
                                                    (("1"
                                                      (INST -1 "j!1")
                                                      (("1"
                                                        (ASSERT)
                                                        NIL)))))))))))))
                                           ("2"
                                            (ASSERT)
                                            NIL)))))))))))))))))))
                         ("2" (FLATTEN)
                          (("2" (GROUND)
                            (("2" (INST?)
                              (("2"
                                (ASSERT)
                                NIL)))))))))))))))))))))))))))))))
 (|walk_merge| "" (SKOSIMP*)
  (("" (CASE-REPLACE "u!1 = v!1")
    (("1" (HIDE -3)
      (("1" (EXPAND "walk_from?")
        (("1" (FLATTEN)
          (("1" (LEMMA "walk_verts_in")
            (("1" (INST?)
              (("1" (ASSERT)
                (("1" (HIDE -2 -4 -5)
                  (("1" (INST + "gen_seq1(G!1,v!1)")
                    (("1" (EXPAND "gen_seq1")
                      (("1" (EXPAND "walk?")
                        (("1" (EXPAND "verts_in?")
                          (("1" (SKOSIMP*)
                            (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
                     ("2" (EXPAND "verts_in?")
                      (("2" (INST?)
                        (("2" (ASSERT) NIL)))))))))))))))))))))
     ("2" (CASE-REPLACE "u!1 = yt!1")
      (("1" (INST + "p2!1") NIL)
       ("2" (LEMMA "walk_from_l")
        (("2" (INST?)
          (("2" (ASSERT)
            (("2" (LEMMA "walk_concat")
              (("2" (INST?)
                (("2" (INST -1 "v!1" "p2!1")
                  (("2" (ASSERT)
                    (("2" (INST + "p1!1 ^ (0, l(p1!1) - 2) o p2!1")
                      (("2" (HIDE -1 -3 -4)
                        (("2" (GRIND) NIL))))))))))))))))))))))))))
$$$digraph_ops.pvs
%------------------------------------------------------------------------
%
%  Operations on a digraph
%  ------------------------------------------------
%
%      Author: Ricky W. Butler   NASA Langley Research Center
%
%  Defines:
%
%      union(G1,G2)      -- creates digraph that is a union of G1 and G2
%
%      del_vert(G,v)     -- removes a vertex and all adjacent edges from a digraph
%
%      del_edge(e,G)     --  creates di_subgraph with edge e removed
%
%      num_edges(G): nat --  number of edges in a digraph
%
%------------------------------------------------------------------------
digraph_ops[T: TYPE]: THEORY
BEGIN
   IMPORTING digraphs[T]
   G, G1, G2: VAR digraph[T]
   t1,t2: VAR T
   x,v: VAR T
   e,e2: VAR edgetype[T]
   union(G1,G2): digraph[T] = (# vert := union(vert(G1),vert(G2)),
                               edges := union(edges(G1),edges(G2)) #)
   del_vert(G: digraph[T], v: T): digraph[T] =
                        (# vert := remove[T](v,vert(G)),
                           edges := {e | edges(G)(e) AND NOT in?(v,e)} #)
   del_edge(G,e): digraph[T] = G WITH [edges := remove(e,edges(G))]
   num_edges(G): nat = card(edges(G))
%  --------------------- del_vert(G,v) lemmas ----------------
   del_vert_still_in   : LEMMA FORALL (x: (vert(G))):
                                     x /= v IMPLIES vert(del_vert(G, v))(x)
   size_del_vert       : LEMMA FORALL (v: (vert(G))):
                                   size(del_vert(G,v)) = size(G) - 1
   del_vert_le         : LEMMA size(del_vert(G,v)) <= size(G)
   del_vert_ge         : LEMMA size(del_vert(G,v)) >= size(G) - 1
   edge_in_del_vert    : LEMMA (edges(G)(e) AND NOT in?(v,e)) IMPLIES
                                 edges(del_vert(G,v))(e)
   edges_del_vert      : LEMMA edges(del_vert(G,v))(e) IMPLIES
                                       edges(G)(e)
   del_vert_comm       : LEMMA del_vert(del_vert(G, x), v) =
                                    del_vert(del_vert(G, v), x)
   del_vert_empty?     : LEMMA FORALL (v: (vert(G))):
                                  empty?(vert(del_vert(G, v))) IMPLIES
                                      singleton?(G)
%  ---------- del_edge(G,e) ----------------------------------
   del_edge_lem       : LEMMA NOT member(e,edges(del_edge(G,e)))
   del_edge_lem2      : LEMMA edges(del_edge(G,e))(e2)
                    		    IMPLIES edges(G)(e2)
   del_edge_lem3      : LEMMA edges(G)(e2) AND e2 /= e IMPLIES
                    		    edges(del_edge(G,e))(e2)
   del_edge_lem5      : LEMMA NOT edges(G)(e) IMPLIES del_edge(G, e) = G
   vert_del_edge      : LEMMA vert(del_edge(G,e)) = vert(G)
   del_edge_num       : LEMMA num_edges(del_edge(G,e)) = num_edges(G)
                                       - IF edges(G)(e) THEN 1 ELSE 0 ENDIF
   del_edge_singleton : LEMMA singleton?(del_edge(G,e)) IMPLIES singleton?(G)
   del_vert_edge_comm : LEMMA del_vert(del_edge(G, e), v) =
                               del_edge(del_vert(G, v), e)
   del_vert_edge      : LEMMA in?(v,e) IMPLIES
                               del_vert(del_edge(G,e),v) = del_vert(G,v)
END digraph_ops
$$$digraph_ops.prf
(|digraph_ops|
 (|union_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "union")
    (("" (EXPAND "member")
      (("" (SPLIT -1)
        (("1" (TYPEPRED "G1!1")
          (("1" (INST?)
            (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL)))))))))
         ("2" (TYPEPRED "G2!1")
          (("2" (INST?)
            (("2" (ASSERT)
              (("2" (FLATTEN) (("2" (ASSERT) NIL)))))))))))))))))
 (|union_TCC2| "" (SUBTYPE-TCC) NIL)
 (|del_vert_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[edgetype[T]]")
    (("" (INST?)
      (("" (INST -1 "edges(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|del_vert_TCC2| "" (SKOSIMP*)
  (("" (EXPAND "remove")
    (("" (EXPAND "in?")
      (("" (EXPAND "member")
        (("" (TYPEPRED "G!1")
          (("" (INST?)
            (("" (ASSERT)
              (("" (FLATTEN) (("" (ASSERT) NIL)))))))))))))))))
 (|del_edge_TCC1| "" (SKOSIMP*)
  (("" (EXPAND "remove")
    (("" (FLATTEN)
      (("" (EXPAND "member")
        (("" (TYPEPRED "G!1")
          (("" (INST?) (("" (ASSERT) NIL)))))))))))))
 (|del_edge_TCC2| "" (SUBTYPE-TCC) NIL)
 (|num_edges_TCC1| "" (SUBTYPE-TCC))
 (|del_vert_still_in| "" (SKOSIMP*)
  (("" (EXPAND "del_vert")
    (("" (EXPAND "remove")
      (("" (EXPAND "member") (("" (ASSERT) NIL)))))))))
 (|size_del_vert| "" (SKOSIMP*)
  (("" (TYPEPRED "v!1")
    (("" (EXPAND "del_vert")
      (("" (EXPAND "size") (("" (REWRITE "card_remove") NIL)))))))))
 (|del_vert_le| "" (SKOSIMP*)
  (("" (EXPAND "size")
    (("" (EXPAND "del_vert")
      (("" (REWRITE "card_remove")
        (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))
 (|del_vert_ge| "" (SKOSIMP*)
  (("" (EXPAND "size")
    (("" (EXPAND "del_vert")
      (("" (REWRITE "card_remove")
        (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))
 (|edge_in_del_vert| "" (SKOSIMP*)
  (("" (EXPAND "del_vert") (("" (ASSERT) NIL)))))
 (|edges_del_vert| "" (SKOSIMP*)
  (("" (EXPAND "del_vert") (("" (FLATTEN) (("" (PROPAX) NIL)))))))
 (|del_vert_comm| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
    (("1" (EXPAND "del_vert")
      (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T)
        (("1" (IFF 1) (("1" (GROUND) NIL)))))))
     ("2" (EXPAND "del_vert")
      (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
        (("2" (GRIND) NIL)))))))))
 (|del_vert_empty?| "" (SKOSIMP*)
  (("" (LEMMA "card_empty?[T]")
    (("" (INST?)
      (("" (REPLACE -1 * RL)
        (("" (HIDE -1)
          (("" (EXPAND "singleton?")
            (("" (EXPAND "size")
              (("" (LEMMA "size_del_vert")
                (("" (INST?)
                  (("" (EXPAND "size")
                    (("" (ASSERT) NIL)))))))))))))))))))))
 (|del_edge_lem| "" (SKOSIMP*)
  (("" (EXPAND "member")
    (("" (EXPAND "del_edge")
      (("" (EXPAND "remove") (("" (PROPAX) NIL)))))))))
 (|del_edge_lem2| "" (SKOSIMP*) (("" (GRIND) NIL)))
 (|del_edge_lem3| "" (SKOSIMP*) (("" (GRIND) NIL)))
 (|del_edge_lem5| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 2 :HIDE? T)
    (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T)
      (("1" (EXPAND "del_edge") (("1" (GRIND) NIL)))))
     ("2" (EXPAND "del_edge") (("2" (PROPAX) NIL)))))))
 (|vert_del_edge| "" (GRIND) NIL)
 (|del_edge_num| "" (SKOSIMP*)
  (("" (EXPAND "num_edges")
    ((""
      (CASE-REPLACE
       "edges(del_edge(G!1,e!1)) = remove(e!1,edges(G!1))")
      (("1" (REWRITE "card_remove[edgetype[T]]") NIL)
       ("2" (HIDE 2)
        (("2" (APPLY-EXTENSIONALITY :HIDE? T)
          (("2" (IFF 1)
            (("2" (PROP)
              (("1" (LEMMA "del_edge_lem2")
                (("1" (INST?)
                  (("1" (LEMMA "del_edge_lem")
                    (("1" (INST?)
                      (("1" (EXPAND "member")
                        (("1" (ASSERT)
                          (("1" (GRIND :EXCLUDE ("edges" "del_edge"))
                            NIL)))))))))))))
               ("2" (REWRITE "del_edge_lem3")
                (("1" (HIDE 2) (("1" (GRIND :EXCLUDE "edges") NIL)))
                 ("2" (HIDE 2)
                  (("2" (GRIND :EXCLUDE "edges") NIL)))))))))))))))))))
 (|del_edge_singleton| "" (SKOSIMP*)
  (("" (EXPAND "singleton?")
    (("" (EXPAND "size")
      (("" (EXPAND "del_edge") (("" (PROPAX) NIL)))))))))
 (|del_vert_edge_comm| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
    (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL)))
     ("2" (EXPAND "del_edge")
      (("2" (EXPAND "del_vert") (("2" (PROPAX) NIL)))))))))
 (|del_vert_edge| "" (SKOSIMP*)
  (("" (REWRITE "del_vert_edge_comm")
    (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
      (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL)))
       ("2" (EXPAND "del_edge") (("2" (PROPAX) NIL))))))))))
$$$digraph_deg.pvs
digraph_deg[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
%  Defines degree of a vertex
%  ------------------------------------------------
%
%      Author: Ricky W. Butler   NASA Langley Research Center
%
%  Defines:
%
%    incident_edges(v,G) -- returns set of edges attached to vertex v
%
%    deg(v,G)          -- number of edges attached to vertex v
%
%------------------------------------------------------------------------
BEGIN
   IMPORTING digraphs[T], digraph_ops[T]
   v: VAR T
   G,GS: VAR digraph[T]
   incident_edges(v,G)  : finite_set[edgetype[T]]
                              = {e: edgetype[T] | edges(G)(e) AND in?(v,e)}
   incident_edges_subset: LEMMA subset?(incident_edges(v,G),edges(G))
   deg(v,G): nat = card(incident_edges(v,G))
   P : VAR pred[digraph[T]]
   n : VAR nat
   e: VAR edgetype[T]
   x,y: VAR T
   incident_edges_emptyset: LEMMA edges(G) = emptyset[edgetype[T]] IMPLIES
                                    incident_edges(v,G) = emptyset[edgetype[T]]
   deg_del_edge    : LEMMA e = (x,y) AND edges(G)(e) IMPLIES
                             deg(y, G) = deg(y, del_edge(G, e)) + 1
   deg_del_edge1   : LEMMA e = (x,y) AND edges(G)(e) IMPLIES
                             deg(x, G) = deg(x, del_edge(G, e)) + 1
   deg_del_edge2   : LEMMA in?(y,e) AND edges(G)(e) IMPLIES
                             deg(y, G) = deg(y, del_edge(G, e)) + 1
   deg_del_edge3   : LEMMA NOT in?(y,e)  IMPLIES
                              deg(y, G) = deg(y, del_edge(G, e))
   deg_del_edge_ge : LEMMA deg(y, G) >= deg(y, del_edge(G, e))
   deg_del_edge_le : LEMMA deg(y, G) - 1 <= deg(y, del_edge(G, e))
   deg_edge_exists       : LEMMA deg(v,G) > 0 IMPLIES
                             (EXISTS e: in?(v,e) AND edges(G)(e))
   deg_to_card     : LEMMA FORALL (SG: simple_digraph):
                               deg(v,SG) > 0 IMPLIES size(SG) >= 2
   del_vert_deg_0  : LEMMA deg(v,G) = 0 IMPLIES
                               edges(del_vert(G,v)) = edges(G)
%   deg_del_vert    : LEMMA x /= v AND edges(G)((x, v))
%                                IMPLIES deg(v, del_vert(G, x)) =
%                                           deg(v, G) - 1
%
%   del_vert_not_incident: LEMMA x /= v AND NOT edges(G)((x, v))
%                                       IMPLIES
%                                       deg(x, del_vert(G, v)) = deg(x, G)
   singleton_deg: LEMMA FORALL (SG: simple_digraph):
                            singleton?(SG) IMPLIES deg(v, SG) = 0
   deg_1_sing   : LEMMA deg(v, G) = 1 IMPLIES
                           (EXISTS e: incident_edges(v, G) = singleton(e) AND
                                      in?(v,e) AND edges(G)(e))
END digraph_deg
$$$digraph_deg.prf
(|digraph_deg|
 (|incident_edges_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset[edgetype[T]]")
    (("" (INST?)
      (("" (INST -1 "edges(G!1)")
        (("" (ASSERT) (("" (HIDE 2) (("" (GRIND) NIL)))))))))))))
 (|incident_edges_subset| "" (GRIND) NIL)
 (|incident_edges_emptyset| "" (SKOSIMP*)
  (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
    (("" (EXPAND "emptyset")
      (("" (EXPAND "incident_edges")
        (("" (FLATTEN) (("" (REPLACE -3) (("" (ASSERT) NIL)))))))))))))
 (|deg_del_edge| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    ((""
      (CASE-REPLACE "incident_edges(y!1, del_edge(G!1,e!1)) =
                     remove(e!1,incident_edges(y!1, G!1))")
      (("1" (REWRITE "card_remove[edgetype[T]]")
        (("1" (LIFT-IF)
          (("1" (GROUND)
            (("1" (HIDE -1 2)
              (("1" (HIDE -2) (("1" (GRIND) NIL)))))))))))
       ("2" (HIDE 2)
        (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
          (("2" (IFF 1)
            (("2" (PROP)
              (("1" (EXPAND "incident_edges")
                (("1" (GROUND)
                  (("1" (EXPAND "remove")
                    (("1" (EXPAND "member")
                      (("1" (GROUND)
                        (("1" (REPLACE -1)
                          (("1" (HIDE -1)
                            (("1" (LEMMA "del_edge_lem[T]")
                              (("1"
                                (INST?)
                                (("1"
                                  (EXPAND "member")
                                  (("1" (PROPAX) NIL)))))))))))
                         ("2" (LEMMA "del_edge_lem2[T]")
                          (("2" (INST?)
                            (("2" (ASSERT) NIL)))))))))))))))
               ("2" (EXPAND "incident_edges")
                (("2" (EXPAND "remove")
                  (("2" (FLATTEN)
                    (("2" (EXPAND "member")
                      (("2" (GROUND)
                        (("2" (REWRITE "del_edge_lem3")
                          NIL)))))))))))))))))))))))))
 (|deg_del_edge1| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    ((""
      (CASE-REPLACE "incident_edges(x!1, del_edge(G!1,e!1)) =
                     remove(e!1,incident_edges(x!1, G!1))")
      (("1" (REWRITE "card_remove[edgetype[T]]")
        (("1" (LIFT-IF)
          (("1" (GROUND)
            (("1" (HIDE -1 2)
              (("1" (HIDE -2) (("1" (GRIND) NIL)))))))))))
       ("2" (HIDE 2)
        (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
          (("2" (IFF 1)
            (("2" (PROP)
              (("1" (EXPAND "incident_edges")
                (("1" (GROUND)
                  (("1" (EXPAND "remove")
                    (("1" (EXPAND "member")
                      (("1" (GROUND)
                        (("1" (REPLACE -1)
                          (("1" (HIDE -1)
                            (("1" (LEMMA "del_edge_lem[T]")
                              (("1"
                                (INST?)
                                (("1"
                                  (EXPAND "member")
                                  (("1" (PROPAX) NIL)))))))))))
                         ("2" (LEMMA "del_edge_lem2[T]")
                          (("2" (INST?)
                            (("2" (ASSERT) NIL)))))))))))))))
               ("2" (EXPAND "incident_edges")
                (("2" (EXPAND "remove")
                  (("2" (FLATTEN)
                    (("2" (EXPAND "member")
                      (("2" (GROUND)
                        (("2" (REWRITE "del_edge_lem3")
                          NIL)))))))))))))))))))))))))
 (|deg_del_edge2| "" (SKOSIMP*)
  (("" (EXPAND "in?")
    (("" (SPLIT -1)
      (("1" (LEMMA "deg_del_edge1")
        (("1" (INST - "G!1" "e!1" "PROJ_1(e!1)" "PROJ_2(e!1)")
          (("1" (ASSERT)
            (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL)))))))
       ("2" (LEMMA "deg_del_edge")
        (("2" (INST - "G!1" "e!1" "PROJ_1(e!1)" "PROJ_2(e!1)")
          (("2" (ASSERT)
            (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL)))))))))))))
 (|deg_del_edge3| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    ((""
      (CASE "incident_edges(y!1, G!1) = incident_edges(y!1, del_edge(G!1, e!1))")
      (("1" (ASSERT) NIL)
       ("2" (HIDE 3)
        (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
          (("2" (EXPAND "incident_edges")
            (("2" (IFF 1)
              (("2" (GROUND)
                (("1" (LEMMA "del_edge_lem3[T]")
                  (("1" (INST?)
                    (("1" (ASSERT)
                      (("1" (CASE "e!1 = (x!1,x!2)")
                        (("1" (EXPAND "in?")
                          (("1" (REPLACE -1) (("1" (ASSERT) NIL)))))
                         ("2" (ASSERT) NIL)))))))))
                 ("2" (LEMMA "del_edge_lem2[T]")
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|deg_del_edge_ge| "" (LEMMA "deg_del_edge2")
  (("" (SKOSIMP*)
    (("" (CASE "in?(y!1,e!1)")
      (("1" (LEMMA "deg_del_edge2")
        (("1" (INST?)
          (("1" (ASSERT)
            (("1" (LEMMA "del_edge_lem5[T]")
              (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
       ("2" (LEMMA "deg_del_edge3")
        (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
 (|deg_del_edge_le| "" (SKOSIMP*)
  (("" (CASE "in?(y!1,e!1)")
    (("1" (LEMMA "deg_del_edge2")
      (("1" (INST?)
        (("1" (ASSERT)
          (("1" (LEMMA "del_edge_lem5[T]")
            (("1" (INST?) (("1" (ASSERT) NIL)))))))))))
     ("2" (LEMMA "deg_del_edge3")
      (("2" (INST?) (("2" (ASSERT) NIL)))))))))
 (|deg_edge_exists| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    (("" (REWRITE "nonempty_card[edgetype[T]]" :DIR RL)
      (("" (EXPAND "nonempty?")
        (("" (EXPAND "empty?")
          (("" (EXPAND "incident_edges")
            (("" (SKOSIMP*)
              (("" (EXPAND "member")
                (("" (INST?)
                  (("" (FLATTEN) (("" (ASSERT) NIL)))))))))))))))))))))
 (|deg_to_card| "" (SKOSIMP*)
  (("" (LEMMA "deg_edge_exists")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SKOSIMP*)
          (("" (HIDE -1 -3)
            (("" (TYPEPRED "SG!1")
              (("" (INST?)
                (("" (ASSERT)
                  (("" (FLATTEN)
                    ((""
                      (CASE "subset?(add[T](proj_1(e!1),singleton(proj_2(e!1))),vert(SG!1))")
                      (("1" (LEMMA "card_subset[T]")
                        (("1" (INST?)
                          (("1" (ASSERT)
                            (("1" (HIDE -2)
                              (("1"
                                (LEMMA "card_add[T]")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (LEMMA "card_singleton[T]")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (REPLACE -1)
                                        (("1"
                                          (HIDE -1)
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (HIDE -1)
                                              (("1"
                                                (EXPAND "singleton")
                                                (("1"
                                                  (ASSERT)
                                                  (("1"
                                                    (EXPAND "size")
                                                    (("1"
                                                      (ASSERT)
                                                      NIL)))))))))))))))))))))))))))
                           ("2" (REWRITE "finite_add[T]") NIL)))))
                       ("2" (HIDE 3)
                        (("2" (GRIND) NIL)))))))))))))))))))))))))
 (|del_vert_deg_0| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    (("" (LEMMA "card_empty?[edgetype[T]]")
      (("" (INST?)
        (("" (IFF)
          (("" (ASSERT)
            (("" (HIDE -2)
              (("" (EXPAND "incident_edges")
                (("" (EXPAND "empty?")
                  (("" (EXPAND "member")
                    (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                      (("" (EXPAND "del_vert")
                        (("" (INST?)
                          (("" (IFF 1)
                            (("" (GROUND)
                              NIL)))))))))))))))))))))))))))))
 (|singleton_deg| "" (SKOSIMP*)
  (("" (EXPAND "singleton?")
    (("" (EXPAND "deg")
      (("" (REWRITE "card_is_0[edgetype[T]]")
        (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
          (("" (EXPAND "incident_edges")
            (("" (EXPAND "emptyset")
              (("" (FLATTEN)
                (("" (LEMMA "edge_in_card_gt_1[T]")
                  (("" (INST?)
                    (("" (SPLIT -1)
                      (("1" (ASSERT)
                        (("1" (EXPAND "size") (("1" (ASSERT) NIL)))))
                       ("2" (PROPAX) NIL)))))))))))))))))))))))
 (|deg_1_sing| "" (SKOSIMP*)
  (("" (EXPAND "deg")
    (("" (LEMMA "card_one[edgetype[T]]")
      (("" (INST?)
        (("" (FLATTEN)
          (("" (ASSERT)
            (("" (HIDE -2)
              (("" (SKOSIMP*)
                (("" (INST?)
                  (("" (ASSERT)
                    ((""
                      (CASE-REPLACE
                       "incident_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)")
                      (("1" (HIDE -2)
                        (("1" (EXPAND "incident_edges")
                          (("1" (EXPAND "singleton")
                            (("1" (FLATTEN) (("1" (ASSERT) NIL)))))))))
                       ("2" (ASSERT) NIL))))))))))))))))))))))))
$$$pairs.pvs
pairs[T: TYPE]: THEORY
BEGIN
   x,y,v,z: VAR T
   pair: TYPE = [T,T]
   mk_pair(x,y): pair = (x,y)
   mk_pair_eq: LEMMA mk_pair(x,y) = mk_pair(v,z) IMPLIES (x = v AND y = z)
   in?(z:T, p: pair): bool = LET (x,y) = p IN z = x OR z = y
   apair?(x,y): bool = (x /= y)
   apair: TYPE = {p: pair | LET (x,y) = p IN x /= y}
   ap: VAR apair
   apair_irreflexive  : LEMMA LET (x,y) = ap IN x /= y
END pairs
$$$pairs.prf
(|pairs|
 (|mk_pair_eq| "" (SKOSIMP*)
  (("" (EXPAND "mk_pair") (("" (PROPAX) NIL)))))
 (|apair_irreflexive| "" (SKOSIMP*) (("" (ASSERT) NIL))))
$$$digraphs.pvs
digraphs[T: TYPE]: THEORY
%-------------------------------------------------------------------------------
%
% Defines:
%
%      digraph[T] -- digraph over domain T
%      vert(G)  -- vertices of digraph G
%      edges(G) -- set of edges in a digraph G
%
%  Authors:
%
%      Ricky W. Butler   NASA Langley
%      Jon Sjogren       AFOSR
%
%  Version 1.0           Last modified 12/20/96
%
%  Maintained by:
%
%     Rick Butler        NASA Langley Research Center
%                        R.W.Butler@larc.nasa.gov
%
%  NOTE:
%
%-------------------------------------------------------------------------------
BEGIN
  IMPORTING finite_sets@finite_sets[T], pairs[T],
            finite_sets@finite_sets[pair[T]]
  x,y,v: VAR T
  edgetype: TYPE = pair[T]     % ---------- ALLOW SELF LOOPS ----------
  edg(x,(y:{y:T | y /= x})): edgetype = (x,y)
  predigraph: TYPE = [# vert : finite_set[T],
                        edges: finite_set[edgetype] #]
  e: VAR edgetype
  directed_graph: TYPE = {g: predigraph | FORALL e: edges(g)(e) IMPLIES
                                      LET (x,y) = e IN vert(g)(x) AND vert(g)(y)}
  digraph       : TYPE = directed_graph
  simple_digraph: TYPE = {g: digraph | FORALL e: edges(g)(e) IMPLIES
                                                 LET (x,y) = e IN x /= y}
  sd_graph      : TYPE = simple_digraph
  G: var digraph
% edge?(G)(x,y): bool = x /= y AND edges(G)((x,y))
  edge?(G)(x,y): bool = edges(G)((x,y))
  edges_vert      : LEMMA in?(x,e) AND edges(G)(e) IMPLIES
                             (EXISTS y: vert(G)(y) AND in?(y,e))
  other_vert      : LEMMA in?(v,e) AND edges(G)(e)
                          IMPLIES (EXISTS (u: T): vert(G)(u) AND
                                       e = (u, v) OR e = (v,u))
  edges_to_pair   : LEMMA edges(G)(e) IMPLIES
                            (EXISTS x,y: edges(G)(x,y)
                                     AND vert(G)(x) AND vert(G)(y)
                                     AND x = proj_1(e) AND y = proj_2(e))
% -------------- size of digraphs --------------------
  size(G): nat = card[T](vert(G))
  empty?(G): bool = empty?(vert(G))
  singleton?(G): bool = (size(G) = 1)
  isolated?(G): bool = empty?(edges(G))
  empty?_rew          : LEMMA empty?(G) = (card(vert(G)) = 0)
  edges_of_empty      : LEMMA empty?(G)
                                 IMPLIES edges(G) = emptyset[edgetype]
  singleton_edges     : LEMMA FORALL (SG: simple_digraph):
                                   singleton?(SG) IMPLIES  empty?(edges(SG))
  edge_in_card_gt_1   : LEMMA FORALL (SG: simple_digraph):
                                   edges(SG)(e) IMPLIES card(vert(SG)) > 1
  not_singleton_2_vert: LEMMA NOT empty?(G) AND NOT singleton?(G)
                                IMPLIES (EXISTS (x,y: T): x /= y AND
                                     vert(G)(x) AND vert(G)(y))
  proj_rew: LEMMA (proj_1(e), proj_2(e)) = e
  infdigraph: TYPE = [# vert : set[T],
                      edges: set[edgetype] #]
  is_digraph(g: infdigraph): bool = is_finite[T](vert(g))
                                AND is_finite[edgetype](edges(g))
                                AND (FORALL (e: edgetype): edges(g)(e)
                                     IMPLIES (FORALL x: in?(x,e) IMPLIES vert(g)(x)))
  singleton_digraph(v): digraph = (# vert := singleton[T](v),
                                       edges := emptyset[edgetype] #)
  is_sing:  LEMMA singleton?(singleton_digraph(x))
  Digraph: TYPE = {g: digraph | nonempty?(vert(g))}
END digraphs
$$$digraphs.prf
(|digraphs|
 (|edges_vert| "" (SKOSIMP*)
  (("" (TYPEPRED "G!1")
    (("" (INST?)
      (("" (ASSERT)
        (("" (FLATTEN)
          (("" (EXPAND "in?")
            (("" (SPLIT -3)
              (("1" (REPLACE -1 :DIR RL)
                (("1" (INST + "PROJ_2(e!1)") (("1" (ASSERT) NIL)))))
               ("2" (REPLACE -1 :DIR RL)
                (("2" (INST + "PROJ_1(e!1)")
                  (("2" (ASSERT) NIL)))))))))))))))))))
 (|other_vert| "" (SKOSIMP*)
  (("" (TYPEPRED "G!1")
    (("" (INST?)
      (("" (ASSERT)
        (("" (FLATTEN)
          (("" (EXPAND "in?")
            (("" (SPLIT -3)
              (("1" (INST + "PROJ_2(e!1)")
                (("1" (ASSERT)
                  (("1" (FLATTEN)
                    (("1" (APPLY-EXTENSIONALITY 2 :HIDE? T) NIL)))))))
               ("2" (INST + "PROJ_1(e!1)")
                (("2" (ASSERT)
                  (("2" (FLATTEN)
                    (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                      NIL)))))))))))))))))))))
 (|edges_to_pair| "" (SKOSIMP*)
  (("" (INST + "proj_1(e!1)" "proj_2(e!1)")
    (("" (ASSERT)
      (("" (CASE "e!1 = (proj_1(e!1),proj_2(e!1))")
        (("1" (REPLACE -1 -)
          (("1" (ASSERT)
            (("1" (TYPEPRED "G!1")
              (("1" (INST?) (("1" (ASSERT) NIL)))))))))
         ("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL)))))))))
 (|empty?_rew| "" (SKOSIMP*)
  (("" (LEMMA " card_empty?[T]")
    (("" (INST?)
      (("" (EXPAND "empty?" 1)
        (("" (REPLACE -1) (("" (PROPAX) NIL)))))))))))
 (|edges_of_empty| "" (SKOSIMP*)
  (("" (EXPAND "empty?")
    (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
      (("" (EXPAND "emptyset")
        (("" (EXPAND "empty?")
          (("" (EXPAND "member")
            (("" (INST?)
              (("" (ASSERT)
                (("" (TYPEPRED "G!1")
                  (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))))))
 (|singleton_edges| "" (SKOSIMP*)
  (("" (EXPAND "singleton?")
    (("" (EXPAND "size")
      (("" (LEMMA "card_one[T]")
        (("" (INST?)
          (("" (ASSERT)
            (("" (HIDE -2)
              (("" (SKOSIMP*)
                (("" (EXPAND "empty?")
                  (("" (SKOSIMP*)
                    (("" (EXPAND "member")
                      (("" (TYPEPRED "SG!1")
                        (("" (INST?)
                          (("" (INST?)
                            (("" (ASSERT)
                              ((""
                                (FLATTEN)
                                ((""
                                  (REPLACE -3)
                                  ((""
                                    (HIDE -3)
                                    ((""
                                      (EXPAND "singleton")
                                      ((""
                                        (ASSERT)
                                        NIL)))))))))))))))))))))))))))))))))))))))
 (|edge_in_card_gt_1| "" (SKOSIMP*)
  (("" (TYPEPRED "SG!1")
    (("" (ASSERT)
      ((""
        (CASE "subset?(add(PROJ_1(e!1),singleton(PROJ_2(e!1))),vert(SG!1))")
        (("1" (LEMMA "card_subset[T]")
          (("1" (INST?)
            (("1" (ASSERT)
              (("1" (REWRITE "card_add")
                (("1" (REWRITE "card_singleton")
                  (("1" (HIDE -2)
                    (("1" (EXPAND "singleton")
                      (("1" (INST?)
                        (("1" (ASSERT)
                          (("1" (ASSERT) NIL)))))))))))))))
             ("2" (REWRITE "finite_add") NIL)))))
         ("2" (HIDE -3 3) (("2" (GRIND) NIL)))))))))))
 (|not_singleton_2_vert| "" (SKOSIMP*)
  (("" (EXPAND "empty?")
    (("" (LEMMA "card_empty?[T]")
      (("" (INST?)
        (("" (IFF)
          (("" (ASSERT)
            (("" (EXPAND "singleton?")
              (("" (EXPAND "size")
                (("" (LEMMA "card_2_has_2[T]")
                  (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))))))
 (|proj_rew| "" (SKOSIMP*)
  (("" (ASSERT) (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL)))))
 (|singleton_digraph_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_singleton") NIL)))
 (|singleton_digraph_TCC2| "" (SKOSIMP*)
  (("" (EXPAND "emptyset") (("" (PROPAX) NIL)))))
 (|is_sing| "" (SKOSIMP*)
  (("" (EXPAND "singleton_digraph")
    (("" (EXPAND "singleton?")
      (("" (EXPAND "size") (("" (REWRITE "card_singleton") NIL))))))))))