Details About PVS Di-Graphs Library

  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