$$$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))))))))))