Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 772


Synopsis:        AUTO_REWRITE+ statements impact TCCS via conversion
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri May 23 11:30:01 2003
Originator:      Rick Butler
Organization:    larc
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  This is a very strange bug.  Merely adding two AUTO_REWRITE+ statements:
  
     AUTO_REWRITE+ dbl_in                
     AUTO_REWRITE+ dbl_not_in
              
  changes the meaning of the language.
  
  Typechecking tree_paths yields the following TCCs:
  
    % Subtype TCC generated (at line 33, column 25) for  i
        % expected type  below[l(p)]
      % proved - incomplete
    min_dual_distin_TCC1: OBLIGATION
      FORALL (G: Graph[T], p: Path[T](G), q: Path[T](G)):
        is_min_dual?(G, p, q) IMPLIES
         (FORALL (i, j: nat): i < p`l - 1 AND j < q`l - 1 IMPLIES i < p`l);
    
    % Subtype TCC generated (at line 33, column 30) for  j
        % expected type  below[l(q)]
      % proved - incomplete
    min_dual_distin_TCC2: OBLIGATION
      FORALL (G: Graph[T], p: Path[T](G), q: Path[T](G)):
        is_min_dual?(G, p, q) IMPLIES
         (FORALL (i, j: nat): i < p`l - 1 AND j < q`l - 1 IMPLIES j < q`l);
  
  But if you add the following statements at the end of the "doubletons" theory
  
     AUTO_REWRITE+ dbl_in                
     AUTO_REWRITE+ dbl_not_in            
  
  then the generated TCCS are:
  
    % Subtype TCC generated (at line 33, column 25) for  i
        % expected type  below[l(p)]
      % unfinished
    min_dual_distin_TCC1: OBLIGATION
      FORALL (G: Graph[T], p: Path[T](G), q: Path[T](G)):
        is_min_dual?(G, p, q) IMPLIES
         (FORALL (i, j: nat):
  	 extend[[real, numfield], [real, real], bool, FALSE](<)(i, p`l - 1) AND
  	   j < q`l - 1
  	   IMPLIES i < p`l);
    
    % Subtype TCC generated (at line 33, column 30) for  j
        % expected type  below[l(q)]
      % proved - incomplete
    min_dual_distin_TCC2: OBLIGATION
      FORALL (G: Graph[T], p: Path[T](G), q: Path[T](G)):
        is_min_dual?(G, p, q) IMPLIES
         (FORALL (i, j: nat):
  	 extend[[real, numfield], [real, real], bool, FALSE](<)(i, p`l - 1) AND
  	   j < q`l - 1
  	   IMPLIES j < q`l);
      
  
  NOTE the presence of the extra "extends" in these TCCS.
  
  I removed as much text as possible to simplify the isolation process.
  
  Rick 
  
  ------------------------------------------
  
  %% PVS Version 3.1
  %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
  
  
  $$$tree_paths.pvs
  tree_paths[T: TYPE]: THEORY
  BEGIN
  
     IMPORTING abstract_min, % tree_circ[T], 
               paths[T] %, path_circ[T] %, circuits[T] 
               % graph_connected[T]
  
     u,v: VAR T
   
     m,n: VAR nat
     G: VAR graph[T]
     p,q: VAR prewalk
  
     dual_paths?(G,(p:Path(G)),(q:Path(G))):bool = p /= q AND p(0)=q(0)
      AND p(l(p)-1)=q(l(q)-1)
  
     Dual_paths(G):TYPE = {((p:Path(G)),(q:Path(G))) | dual_paths?(G,p,q)}
  
  
     min_dual_paths(G: Graph[T], r: Path(G), s: Path(G) | dual_paths?(G,r,s)): 
              Dual_paths(G) = min[[Path(G),Path(G)],
     (LAMBDA (r:Path(G),s:Path(G)): l(r)+l(s)),
     (LAMBDA (r:Path(G),s:Path(G)): dual_paths?(G,r,s))]
  
  
     is_min_dual?(G,(p:Path(G)),(q:Path(G))):bool = dual_paths?(G,p,q) 
                        AND FORALL (r:Path(G),s:Path(G)): dual_paths?(G,r,s) 
                              IMPLIES  l(r) + l(s) >= l(p)+l(q)
  
  
      min_dual_distin: LEMMA FORALL (G: Graph[T], p: Path(G), q:
        Path(G)): is_min_dual?(G,p,q) IMPLIES (FORALL (i,j:nat):i<l(p)-1 AND
            j<l(q)-1 AND p(i)=q(j) IMPLIES (i=0 AND j=0))
  
  	
  
  
  END tree_paths
  
  
  $$$tree_paths.prf
  (tree_paths
   (dual_paths?_TCC1 0
    (dual_paths?_TCC1-1 nil 3262616807 3262696029 ("" (subtype-tcc) nil nil)
     proved ((/= const-decl "boolean" notequal nil)) 103 100 nil nil))
   (dual_paths?_TCC2 0
    (dual_paths?_TCC2-1 nil 3262616807 3262696029 ("" (subtype-tcc) nil nil)
     proved ((/= const-decl "boolean" notequal nil)) 157 90 nil nil))
   (dual_paths?_TCC3 0
    (dual_paths?_TCC3-1 nil 3262616807 3262696030 ("" (subtype-tcc) nil nil)
     proved
     ((/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil))
     110 110 nil nil))
   (dual_paths?_TCC4 0
    (dual_paths?_TCC4-1 nil 3262616807 3262696030 ("" (subtype-tcc) nil nil)
     proved
     ((/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil))
     113 110 nil nil))
   (min_dual_paths_TCC1 0
    (min_dual_paths_TCC1-1 nil 3262616807 3262696030
     ("" (skolem-typepred) (("" (inst + "(r!1,s!1)") nil nil)) nil) unfinished
     ((dual_paths? const-decl "bool" tree_paths nil)
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil
 )
      (finite_set type-eq-decl nil finite_sets nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil) (T formal-type-decl nil tree_paths nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     31 30 t nil))
   (min_dual_paths_TCC2 0
    (min_dual_paths_TCC2-1 nil 3262616807 3262696030
     ("" (skolem-typepred)
      ((""
        (typepred "min[[Path(G!1), Path(G!1)],
                         LAMBDA (r: Path(G!1), s: Path(G!1)): l(r) + l(s),
                         LAMBDA (r: Path(G!1), s: Path(G!1)):
                           dual_paths?(G!1, r, s)]")
        (("1" (assert) (("1" (expand "minimal?") (("1" (propax) nil nil)) nil))
          nil)
         ("2" (hide 2) (("2" (inst + "(r!1,s!1)") nil nil)) nil))
        nil))
      nil)
     unfinished
     ((min const-decl "{S: T | minimal?(S)}" abstract_min nil)
      (minimal? const-decl "bool" abstract_min nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil) (pregraph type-eq-decl nil graphs nil
 )
      (finite_set type-eq-decl nil finite_sets nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil) (T formal-type-decl nil tree_paths nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     77 70 t nil))
   (min_dual_paths_TCC3 0
    (min_dual_paths_TCC3-1 nil 3262696030 3262696037
     ("" (subtype-tcc)
      (("1" (postpone) nil nil) ("2" (postpone) nil nil)
       ("3" (postpone) nil nil) ("4" (postpone) nil nil)
       ("5" (postpone) nil nil) ("6" (postpone) nil nil)
       ("7" (postpone) nil nil) ("8" (postpone) nil nil)
       ("9" (postpone) nil nil) ("10" (postpone) nil nil)
       ("11" (postpone) nil nil) ("12" (postpone) nil nil)
       ("13" (postpone) nil nil) ("14" (postpone) nil nil)
       ("15" (postpone) nil nil) ("16" (postpone) nil nil)
       ("17" (postpone) nil nil) ("18" (postpone) nil nil)
       ("19" (postpone) nil nil) ("20" (postpone) nil nil)
       ("21" (postpone) nil nil) ("22" (postpone) nil nil)
       ("23" (postpone) nil nil) ("24" (postpone) nil nil)
       ("25" (postpone) nil nil) ("26" (postpone) nil nil)
       ("27" (postpone) nil nil) ("28" (postpone) nil nil)
       ("29" (postpone) nil nil) ("30" (postpone) nil nil)
       ("31" (postpone) nil nil) ("32" (postpone) nil nil)
       ("33" (postpone) nil nil) ("34" (postpone) nil nil)
       ("35" (postpone) nil nil) ("36" (postpone) nil nil))
      nil)
     unfinished nil 6893 6290 nil shostak))
   (dual_path_trunc_TCC1 0
    (dual_path_trunc_TCC1-1 nil 3262616807 3262696037 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (T formal-type-decl nil tree_paths nil) (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil)
      (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil)
      (empty? const-decl "bool" sets nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil))
     369 340 nil nil))
   (dual_path_trunc_TCC2 0
    (dual_path_trunc_TCC2-1 nil 3262616807 3262696038 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (T formal-type-decl nil tree_paths nil) (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil)
      (Path type-eq-decl nil paths nil) (member const-decl "bool" sets nil)
      (empty? const-decl "bool" sets nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil))
     570 530 nil nil))
   (dual_path_trunc_TCC3 0
    (dual_path_trunc_TCC3-1 nil 3262616807 3262696039 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil)
      (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     829 740 nil nil))
   (dual_path_trunc_TCC4 0
    (dual_path_trunc_TCC4-1 nil 3262616807 3262696039 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil)
      (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     910 850 nil nil))
   (dual_path_trunc_TCC5 0
    (dual_path_trunc_TCC5-1 nil 3262616807 3262696040 ("" (subtype-tcc) nil nil
 )
     proved
     ((/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     485 470 nil nil))
   (dual_path_trunc_TCC6 0
    (dual_path_trunc_TCC6-1 nil 3262616807 3262696041 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil)
      (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     1250 1200 nil nil))
   (dual_path_trunc_TCC7 0
    (dual_path_trunc_TCC7-1 nil 3262616807 3262696042 ("" (subtype-tcc) nil nil
 )
     proved
     ((/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     637 620 nil nil))
   (dual_path_trunc_TCC8 0
    (dual_path_trunc_TCC8-1 nil 3262616807 3262696044 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (Path type-eq-decl nil paths nil)
      (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (T formal-type-decl nil tree_paths nil)
      (verts_in? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil) (walk? const-decl "bool" walks nil)
      (path? const-decl "bool" paths nil))
     1675 1610 nil nil))
   (dual_path_trunc 0
    (dual_path_trunc-1 nil 3262616807 3262617167
     ("" (skosimp*)
      (("" (case "l(p!1)>1")
        (("1" (case "l(q!1)>1")
          (("1" (bddsimp)
            (("1" (typepred "q!1")
              (("1" (lemma "path?_caret")
                (("1" (inst? -1)
                  (("1" (bddsimp (-1 -3 -4))
                    (("1" (propax) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (lemma "path?_caret")
              (("2" (inst? -1)
                (("2" (typepred "p!1")
                  (("2" (bddsimp (-2 -3 -5))
                    (("1" (propax) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (typepred "q!1")
              (("3" (lemma "path?_caret")
                (("3" (inst? -1)
                  (("1" (bddsimp (-1 -3 -4))
                    (("1" (propax) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil)
             ("4" (typepred "p!1")
              (("4" (lemma "path?_caret")
                (("4" (inst? -1)
                  (("1" (bddsimp (-1 -3 -5))
                    (("1" (propax) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (expand "dual_paths?")
              (("2" (expand "fseq")
                (("2" (bddsimp)
                  (("2" (flatten)
                    (("2" (case "l(q!1)=1")
                      (("1" (replace -1 * lr)
                        (("1" (assert)
                          (("1" (replace -4 -3 rl)
                            (("1" (typepred "p!1")
                              (("1" (expand "path?")
                                (("1" (flatten)
                                  (("1" (inst -3 "0" "l(p!1)-1")
                                    (("1" (expand "fseq")
                                      (("1" (propax) nil nil)) nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (case "l(p!1)=1")
            (("1" (expand "dual_paths?")
              (("1" (expand "fseq")
                (("1" (flatten)
                  (("1" (replace -1 * lr)
                    (("1" (assert)
                      (("1" (replace -3 -2 lr)
                        (("1" (typepred "q!1")
                          (("1" (expand "path?")
                            (("1" (flatten)
                              (("1" (inst -3 "0" "l(q!1)-1")
                                (("1" (expand "fseq")
                                  (("1" (assert)
                                    (("1" (flatten)
                                      (("1" (case "l(q!1)=1")
                                        (("1"
                                          (apply-extensionality 2 :hide? t)
                                          (("1"
                                            (apply-extensionality 1 :hide? t)
                                            (("1" (grind) nil nil))
                                            nil))
                                          nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((Path type-eq-decl nil paths nil) (Graph type-eq-decl nil graphs nil)
      (nonempty? const-decl "bool" sets nil) (path? const-decl "bool" paths nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil) (prewalk type-eq-decl nil walks nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (T formal-type-decl nil tree_paths nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (> const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil naturalnumbers nil)
      (dual_paths? const-decl "bool" tree_paths nil) nil
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (>= const-decl "bool" reals nil)
      (int nonempty-type-eq-decl nil integers nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (IFF const-decl "[bool, bool -> bool]" booleans nil)
      (walk? const-decl "bool" walks nil) (edge? const-decl "bool" graphs nil)
      (verts_in? const-decl "bool" walks nil))
     970 900 nil nil))
   (dual_path_length 0
    (dual_path_length-1 nil 3262616807 3262617169
     ("" (skosimp*)
      (("" (lemma " dual_path_trunc")
        (("" (inst -1 "G!1" "p!1" "q!1")
          (("" (bddsimp)
            (("" (delete -4 -5 -6 -7)
              (("" (expand "dual_paths?")
                (("" (flatten)
                  (("" (expand "fseq")
                    (("" (lemma "plus_up")
                      (("" (inst? -1)
                        (("" (inst -1 "seq(p!1)(0)" "seq(p!1)(l(p!1)-1)")
                          (("" (assert)
                            (("" (bddsimp)
                              (("1" (install-rewrites "walks[T]")
                                (("1" (assert)
                                  (("1" (case "l(p!1)=2")
                                    (("1" (replace -1 * lr)
                                      (("1" (assert)
                                        (("1"
                                          (case "l(q!1)=2")
                                          (("1"
                                            (replace -1 * lr)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (delete -5 -6)
                                                (("1"
                                                  (delete 3 4)
                                                  (("1"
                                                    (apply-extensionality
                                                     1
                                                     :hide?
                                                     t)
                                                    (("1"
                                                      (replace -1 * lr)
                                                      (("1"
                                                        (replace -2 * lr)
                                                        (("1" (assert) nil nil)
 )
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (install-rewrites "walks[T]")
                                (("2" (assert) nil nil)) nil)
                               ("3" (install-rewrites "walks[T]")
                                (("3" (assert) nil nil)) nil)
                               ("4" (assert)
                                (("4" (lemma "path_one")
                                  (("4"
                                    (inst -1 "G!1" "p!1" "seq(p!1)(0)"
                                     "seq(p!1)(l(p!1)-1)")
                                    (("4" (assert)
                                      (("4" (expand "path_from?")
                                        (("4"
                                          (expand "from?")
                                          (("4" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((dual_path_trunc formula-decl nil tree_paths nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (path_from? const-decl "bool" paths nil)
      (path_one formula-decl nil nil nil) (from? const-decl "bool" walks nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
      (IFF const-decl "[bool, bool -> bool]" booleans nil) nil
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (plus_up formula-decl nil nil nil) (Path type-eq-decl nil paths nil)
      (path? const-decl "bool" paths nil) (prewalk type-eq-decl nil walks nil)
      (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil tree_paths nil))
     1152 1050 nil nil))
   (min_dual_reduc_TCC1 0
    (min_dual_reduc_TCC1-1 nil 3262616807 3262696044
     ("" (skosimp*)
      (("" (expand "is_min_dual?")
        (("" (flatten)
          (("" (lemma "dual_path_trunc")
            (("" (inst? -1) (("" (bddsimp (-1 -2)) (("" (assert) nil nil)) nil)
 )
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((is_min_dual? const-decl "bool" tree_paths nil)
      (dual_path_trunc formula-decl nil tree_paths nil)
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil tree_paths nil))
     156 140 nil nil))
   (min_dual_reduc_TCC2 0
    (min_dual_reduc_TCC2-1 nil 3262616807 3262696044
     ("" (skosimp*)
      (("" (expand "is_min_dual?")
        (("" (flatten)
          (("" (lemma "dual_path_trunc")
            (("" (inst? -1) (("" (bddsimp (-1 -2)) (("" (assert) nil nil)) nil)
 )
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((is_min_dual? const-decl "bool" tree_paths nil)
      (dual_path_trunc formula-decl nil tree_paths nil)
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil tree_paths nil))
     141 140 nil nil))
   (min_dual_reduc_TCC3 0
    (min_dual_reduc_TCC3-1 nil 3262616807 3262696044
     ("" (skosimp*)
      (("" (expand "fseq")
        (("" (expand "is_min_dual?")
          (("" (flatten)
            (("" (lemma "dual_path_trunc")
              (("" (inst? -1)
                (("" (bddsimp (-1 -2)) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (T formal-type-decl nil tree_paths nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (/= const-decl "boolean" notequal nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (Graph type-eq-decl nil graphs nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil)
      (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil)
      (dual_path_trunc formula-decl nil tree_paths nil)
      (is_min_dual? const-decl "bool" tree_paths nil))
     166 140 nil nil))
   (min_dual_reduc_TCC4 0
    (min_dual_reduc_TCC4-1 nil 3262616807 3262696044
     ("" (skosimp*)
      (("" (expand "is_min_dual?")
        (("" (flatten)
          (("" (lemma "dual_path_trunc")
            (("" (inst? -1) (("" (bddsimp (-1 -2)) (("" (assert) nil nil)) nil)
 )
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((is_min_dual? const-decl "bool" tree_paths nil)
      (dual_path_trunc formula-decl nil tree_paths nil)
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil tree_paths nil))
     141 140 nil nil))
   (min_dual_reduc 0
    (min_dual_reduc-1 nil 3262616807 3262617180
     ("" (skosimp*)
      (("" (expand "fseq")
        (("" (lemma "dual_path_trunc")
          (("" (inst? -1)
            (("" (inst -1 "q!1")
              (("" (expand "is_min_dual?")
                (("" (flatten)
                  (("" (bddsimp (-1 -2))
                    (("" (inst -8 "p!1^(0,l(p!1)-2)" "q!1^(0,l(q!1)-2)")
                      (("1" (bddsimp)
                        (("1" (hide -1 -4 -5 -6 -7)
                          (("1" (install-rewrites "walks[T]")
                            (("1" (assert) nil nil)) nil))
                          nil)
                         ("2" (hide -1 -4 -5 -6 -7)
                          (("2" (install-rewrites "walks[T]")
                            (("2" (assert) nil nil)) nil))
                          nil)
                         ("3" (expand "dual_paths?")
                          (("3" (expand "fseq")
                            (("3" (flatten)
                              (("3" (bddsimp)
                                (("1" (expand "^" 2) (("1" (assert) nil nil))
                                  nil)
                                 ("2" (expand "^" 2) (("2" (assert) nil nil))
                                  nil)
                                 ("3" (flatten)
                                  (("3" (hide -5 -6 -7 -8)
                                    (("3" (install-rewrites "walks[T]")
                                      (("3" (apply-extensionality 1)
                                        (("3"
                                          (apply-extensionality 1 :hide? t)
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (case
                                               " (LAMBDA (x: below[l(p!1) - 1])
 : seq(p!1)(x))(x!1) =
         (LAMBDA (x: below[l(q!1) - 1]): seq(q!1)(x))(x!1)")
                                              (("1"
                                                (hide -7)
                                                (("1"
                                                  (beta -1)
                                                  (("1" (propax) nil nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (replace -6 1 lr)
                                                (("2" (propax) nil nil))
                                                nil)
                                               ("3"
                                                (typepred "x!1")
                                                (("3"
                                                  (replace -6 -1 lr)
                                                  (("3"
                                                    (case "x!1=l(q!1)-1")
                                                    (("1"
                                                      (replace -1 2 lr)
                                                      (("1"
                                                        (replace -7 -4 lr)
                                                        (("1" (propax) nil nil)
 )
                                                        nil))
                                                      nil)
                                                     ("2" (assert) nil nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("4"
                                                (typepred "x!1")
                                                (("4"
                                                  (case "x!1=l(p!1)-1")
                                                  (("1"
                                                    (replace -1 2 lr)
                                                    (("1"
                                                      (replace -7 -4 rl)
                                                      (("1" (propax) nil nil))
                                                      nil))
                                                    nil)
                                                   ("2" (assert) nil nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (flatten)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("4" (expand "dual_paths?")
                          (("4" (expand "fseq")
                            (("4" (flatten)
                              (("4" (bddsimp)
                                (("1" (expand "^" 2)
                                  (("1" (assert)
                                    (("1" (reveal -1)
                                      (("1"
                                        (inst
                                         -1
                                         "p!1^(1,l(p!1)-1)"
                                         "q!1^(1,l(q!1)-1)")
                                        (("1"
                                          (bddsimp)
                                          (("1"
                                            (hide -6 -7 -8 -9)
                                            (("1"
                                              (install-rewrites "walks[T]")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "dual_paths?")
                                            (("2"
                                              (expand "fseq")
                                              (("2"
                                                (bddsimp)
                                                (("1"
                                                  (expand "^" 1)
                                                  (("1" (propax) nil nil))
                                                  nil)
                                                 ("2"
                                                  (expand "^" 1)
                                                  (("2" (propax) nil nil))
                                                  nil)
                                                 ("3"
                                                  (flatten)
                                                  (("3"
                                                    (hide -6 -7 -8 -9)
                                                    (("3"
                                                      (install-rewrites
                                                       "walks[T]")
                                                      (("3"
                                                        (assert)
                                                        (("3"
                                                          (flatten)
                                                          (("3"
                                                            (apply-extensionali
 ty
                                                             1
                                                             :hide?
                                                             t)
                                                            (("3"
                                                              (apply-extensiona
 lity
                                                               1
                                                               :hide?
                                                               t)
                                                              (("1"
                                                                (case
                                                                 "(LAMBDA (x: b
 elow[l(p!1) - 1]): seq(p!1)(1 + x))(x!1-1) =
         (LAMBDA (x: below[l(q!1) - 1]): seq(q!1)(1 + x))(x!1-1)")
                                                                (("1"
                                                                  (beta -1)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (replace
  
                                                                   -2
                                                                   1
  
                                                                   lr)
                                                                  (("2"
                                                                    (propax)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (replace
  
                                                                 -1
                                                                 1
  
                                                                 lr)
                                                                (("2"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand "^" 1)
                                          (("2" (assert) nil nil))
                                          nil)
                                         ("3"
                                          (expand "^" 1)
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (expand "^" 2) (("2" (assert) nil nil))
                                  nil)
                                 ("3" (expand "^" 2)
                                  (("3" (assert)
                                    (("3" (hide -5 -6 -7 -8)
                                      (("3" (install-rewrites "walks[T]")
                                        (("3"
                                          (apply-extensionality 1 :hide? t)
                                          (("3"
                                            (flatten)
                                            (("3"
                                              (apply-extensionality 1 :hide? t)
                                              (("1"
                                                (case
                                                 "(LAMBDA (x: below[l(p!1) - 1]
 ): seq(p!1)(x))(x!1) =
         (LAMBDA (x: below[l(q!1) - 1]): seq(q!1)(x))(x!1)")
                                                (("1"
                                                  (hide -7)
                                                  (("1"
                                                    (beta -1)
                                                    (("1" (propax) nil nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (replace -6 1 lr)
                                                  (("2" (propax) nil nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (replace -5 1 lr)
                                                (("2" (assert) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (bddsimp)
                        (("1" (expand "^" 1) (("1" (assert) nil nil)) nil)
                         ("2" (expand "^" 1) (("2" (assert) nil nil)) nil))
                        nil)
                       ("3" (assert) nil nil)
                       ("4" (bddsimp)
                        (("1" (expand "^" 1) (("1" (assert) nil nil)) nil)
                         ("2" (expand "^" 1) (("2" (assert) nil nil)) nil))
                        nil)
                       ("5" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (T formal-type-decl nil tree_paths nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (/= const-decl "boolean" notequal nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (Graph type-eq-decl nil graphs nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil)
      (path? const-decl "bool" paths nil) (Path type-eq-decl nil paths nil)
      (is_min_dual? const-decl "bool" tree_paths nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (IFF const-decl "[bool, bool -> bool]" booleans nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (< const-decl "bool" reals nil)
      (below type-eq-decl nil naturalnumbers nil)
      (IF const-decl "[boolean, T, T -> T]" if_def nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (fin_seq type-eq-decl nil seq_def nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (>= const-decl "bool" reals nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (dual_path_trunc formula-decl nil tree_paths nil))
     10186 3330 nil nil))
   (min_dual_distin_TCC1 0
    (min_dual_distin_TCC1-1 nil 3262616807 3262696045 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (T formal-type-decl nil tree_paths nil) (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil)
      (Path type-eq-decl nil paths nil) (walk? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil)
      (verts_in? const-decl "bool" walks nil)
      (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil)
      (>= const-decl "bool" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (is_min_dual? const-decl "bool" tree_paths nil))
     483 470 nil nil))
   (min_dual_distin_TCC2 0
    (min_dual_distin_TCC2-1 nil 3262616807 3262696045 ("" (subtype-tcc) nil nil
 )
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (T formal-type-decl nil tree_paths nil) (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil
 )
      (nonempty? const-decl "bool" sets nil) (Graph type-eq-decl nil graphs nil
 )
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (> const-decl "bool" reals nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (below type-eq-decl nil nat_types nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (prewalk type-eq-decl nil walks nil) (path? const-decl "bool" paths nil)
      (Path type-eq-decl nil paths nil) (walk? const-decl "bool" walks nil)
      (edge? const-decl "bool" graphs nil)
      (verts_in? const-decl "bool" walks nil)
      (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil)
      (>= const-decl "bool" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (/= const-decl "boolean" notequal nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil)
      (dual_paths? const-decl "bool" tree_paths nil)
      (is_min_dual? const-decl "bool" tree_paths nil))
     512 450 nil nil))
   (min_dual_distin 0
    (min_dual_distin-1 nil 3262616807 3262683138
     ("" (skosimp*)
      (("" (expand "fseq")
        (("" (lemma "min_dual_reduc")
          (("" (inst? -1)
            (("" (expand "fseq")
              (("" (bddsimp (-1 -2))
                (("" (expand "is_min_dual?")
                  (("" (flatten)
                    (("" (lemma "dual_path_trunc")
                      (("" (inst? -1)
                        (("" (bddsimp (-1 -2))
                          (("" (delete -4 -5 -6 -7)
                            (("" (hide -2 -3)
                              (("" (inst -2 "p!1^(0,i!1)" "q!1^(0,j!1)")
                                (("1" (expand "dual_paths?")
                                  (("1" (expand "fseq")
                                    (("1" (flatten)
                                      (("1" (bddsimp)
                                        (("1"
                                          (expand "^")
                                          (("1" (assert) nil nil))
                                          nil)
                                         ("2"
                                          (expand "^")
                                          (("2" (assert) nil nil))
                                          nil)
                                         ("3"
                                          (expand "^")
                                          (("3" (propax) nil nil))
                                          nil)
                                         ("4"
                                          (expand "^")
                                          (("4" (propax) nil nil))
                                          nil)
                                         ("5"
                                          (expand "^")
                                          (("5" (propax) nil nil))
                                          nil)
                                         ("6"
                                          (expand "^")
                                          (("6" (propax) nil nil))
                                          nil)
                                         ("7"
                                          (expand "^")
                                          (("7"
                                            (flatten)
                                            (("7"
                                              (case
                                               " (LAMBDA (x: below[1 + i!1]): s
 eq(p!1)(x))(1) =       (LAMBDA (x: below[1 + j!1]): seq(q!1)(x))(1)")
                                              (("1"
                                                (beta -1)
                                                (("1" (propax) nil nil))
                                                nil)
                                               ("2"
                                                (replace -4 1 lr)
                                                (("2" (propax) nil nil))
                                                nil)
                                               ("3"
                                                (skosimp*)
                                                (("3" (assert) nil nil))
                                                nil)
                                               ("4" (assert) nil nil)
                                               ("5"
                                                (skosimp*)
                                                (("5" (assert) nil nil))
                                                nil)
                                               ("6" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("8"
                                          (expand "^")
                                          (("8"
                                            (flatten)
                                            (("8"
                                              (case
                                               " (LAMBDA (x: below[1 + i!1]): s
 eq(p!1)(x))(1) =       (LAMBDA (x: below[1 + j!1]): seq(q!1)(x))(1)")
                                              (("1"
                                                (beta -1)
                                                (("1" (propax) nil nil))
                                                nil)
                                               ("2"
                                                (replace -4 1 lr)
                                                (("2" (propax) nil nil))
                                                nil)
                                               ("3"
                                                (skosimp*)
                                                (("3" (assert) nil nil))
                                                nil)
                                               ("4" (assert) nil nil)
                                               ("5" (assert) nil nil)
                                               ("6" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (assert)
                                  (("2" (lemma "path?_caret")
                                    (("2" (inst -1 "G!1" "0" "j!1" "q!1")
                                      (("2" (typepred "j!1")
                                        (("2"
                                          (expand "dual_paths?")
                                          (("2"
                                            (expand "fseq")
                                            (("2"
                                              (typepred "q!1")
                                              (("2"
                                                (assert (-3 -4 -7))
                                                (("2"
                                                  (bddsimp)
                                                  (("1"
                                                    (expand "^" 1)
                                                    (("1" (assert) nil nil))
                                                    nil)
                                                   ("2"
                                                    (expand "^" 1)
                                                    (("2" (assert) nil nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("3" (assert) nil nil)
                                 ("4" (bddsimp)
                                  (("1" (lemma "path?_caret")
                                    (("1" (inst -1 "G!1" "0" "i!1" "p!1")
                                      (("1" (typepred "i!1")
                                        (("1"
                                          (typepred "p!1")
                                          (("1"
                                            (assert (-2 -3 -4))
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (lemma "path?_caret")
                                    (("2" (inst -1 "G!1" "0" "i!1" "p!1")
                                      (("2" (typepred "p!1")
                                        (("2"
                                          (assert (-2 -3 -4))
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3" (expand "^") (("3" (assert) nil nil))
                                    nil)
                                   ("4" (expand "^") (("4" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("5" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unfinished
     ((min_dual_reduc formula-decl nil tree_paths nil)
      (is_min_dual? const-decl "bool" tree_paths nil)
      (dual_path_trunc formula-decl nil tree_paths nil)
      (NOT const-decl "[bool -> bool]" booleans nil) nil
      (dual_paths? const-decl "bool" tree_paths nil) nil nil
      (below type-eq-decl nil naturalnumbers nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (IF const-decl "[boolean, T, T -> T]" if_def nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (fin_seq type-eq-decl nil seq_def nil)
      (^ const-decl "fin_seq(IF PROJ_1(p) > PROJ_2(p) THEN 0
          ELSE PROJ_2(p) - PROJ_1(p) + 1
          ENDIF)" seq_def nil)
      (< const-decl "bool" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (>= const-decl "bool" reals nil) nil nil nil
      (Path type-eq-decl nil paths nil) (path? const-decl "bool" paths nil)
      (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (finite_seq type-eq-decl nil seq_def nil)
      (below type-eq-decl nil nat_types nil)
      (nat nonempty-type-eq-decl nil naturalnumbers nil)
      (Graph type-eq-decl nil graphs nil) (nonempty? const-decl "bool" sets nil
 )
      (graph type-eq-decl nil graphs nil)
      (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
      (pregraph type-eq-decl nil graphs nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil tree_paths nil)
      (fseq const-decl "[below[l(fs)] -> T]" seq_def nil))
     262819 12620 t 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) (|care
 t_TCC2| "" (SUBTYPE-TCC) NIL)
   (|caret_TCC3| "" (SUBTYPE-TCC) NIL) (|caret_TCC4| "" (SUBTYPE-TCC) NIL) (|ca
 ret_TCC5| "" (SUBTYPE-TCC) NIL)
   (|rev_TCC1| "" (SUBTYPE-TCC) NIL))
  
  $$$walks.pvs
  
  walks[T: TYPE]: THEORY
  
  BEGIN
  
     IMPORTING graphs[T], seq_def, finite_sets@finite_sets_eq
  
     G,GG: VAR graph[T]
     n: VAR nat
     x,u,v,u1,u2,v1,v2,v3: VAR T
     e: VAR doubleton[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)}
  
  
     verts_of(ww: prewalk): finite_set[T] = 
                 {t: T | (EXISTS (i: below(l(ww))): ww(i) = t)}
  
     edges_of(ww): finite_set[doubleton[T]] = {e: doubleton[T] |
                             EXISTS (i: below(l(ww)-1)): e = dbl(ww(i),ww(i+1))
 }
  
  
     pre_circuit?(G: graph[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)
    
  %%  ----------- 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 EN
 DIF)
  %                         #)
  
  
  %   gen_seq1_is_walk: LEMMA vert(G)(x) IMPLIES walk?(G,gen_seq1(G,x))
  
  %   edge_to_walk    : LEMMA u /= v AND edges(G)(edg[T](u, v)) IMPLIES
  %                             walk?(G,gen_seq2(G,u,v))
  
  
  %   walk?_rev       : LEMMA walk?(G,ps) IMPLIES walk?(G,rev(ps))
  
     
  
  %   w1,w2: VAR prewalk
  %   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, u2, v)
  %      		 IMPLIES
  %      		     walk_from?(G, w1 ^ (0, l(w1) - 2) o rev(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, v, yt) AND
  %      	             walk_from?(G, p2, u, yt)
  %                           IMPLIES
  %      	                (EXISTS (p: prewalk): walk_from?(G, p, u, v))
  
  
  END walks
  
  
  $$$walks.prf
  (|walks| (|walk?_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|walk?_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|from?_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|from?_TCC2| "" (SUBTYPE-TCC) NIL 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 NIL))
                                NIL))
                              NIL)
                             ("2" (EXPAND "fullset") (("2" (PROPAX) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (SKOSIMP*)
                  (("2" (EXPAND "fseq")
                    (("2" (INST?)
                      (("2" (EXPAND "restrict") (("2" (PROPAX) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("3" (SKOSIMP*)
                  (("3" (EXPAND "fseq") (("3" (INST?) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (HIDE 2)
            (("2" (EXPAND "is_finite")
              (("2" (INST 1 "l(ww!1)" "(LAMBDA (ii: below(l(ww!1))): ii)")
                (("2" (EXPAND "injective?")
                  (("2" (EXPAND "restrict") (("2" (SKOSIMP*) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edges_of_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|edges_of_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|edges_of_TCC3| "" (SKOSIMP*)
    (("" (EXPAND "is_finite")
      ((""
        (INST 1 "l(ww!1) - 1" "(LAMBDA (e: {e: doubleton[T] |
             EXISTS (i: below(l(ww!1) - 1)):
               e = dbl[T](fseq[T](ww!1)(i), fseq[T](ww!1)(i + 1))}): 
          choose({i: below(l(ww!1) - 1) | 
                     e = dbl[T](fseq[T](ww!1)(i), fseq[T](ww!1)(i + 1))}))")
        (("1" (EXPAND "injective?")
          (("1" (SKOSIMP*) (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (SKOSIMP*)
          (("2" (EXPAND "nonempty?")
            (("2" (EXPAND "empty?")
              (("2" (EXPAND "member")
                (("2" (EXPAND "fseq")
                  (("2" (TYPEPRED "ww!1")
                    (("2" (TYPEPRED "e!1")
                      (("2" (SKOSIMP*)
                        (("2" (INST -4 "i!1")
                          (("2" (EXPAND "fseq") (("2" (PROPAX) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|pre_circuit?_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|pre_circuit?_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|verts_in?_concat_TCC1| "" (SUBTYPE-TCC) NIL 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 NIL)) NIL)) NIL)
               ("2" (TYPEPRED "s2!1")
                (("2" (EXPAND "verts_in?") (("2" (INST?) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|verts_in?_caret_TCC1| "" (SKOSIMP*)
    (("" (EXPAND "verts_in?")
      (("" (EXPAND "^")
        (("" (EXPAND "emptyseq") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    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 NIL)) NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (TYPEPRED "i!1")
            (("2" (TYPEPRED "i!2")
              (("2" (EXPAND "^")
                (("2" (LIFT-IF)
                  (("2" (EXPAND "emptyseq") (("2" (GROUND) NIL NIL)) NIL)) NIL)
 )
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|vert_seq_lem| "" (SKOSIMP*)
    (("" (EXPAND "fseq")
      (("" (TYPEPRED "w!1")
        (("" (EXPAND "verts_in?") (("" (INST - "n!1") NIL NIL)) NIL)) NIL))
      NIL))
    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 NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    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 NIL)) NIL)
 )
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk_verts_in| "" (SKOSIMP*)
    (("" (EXPAND "walk?") (("" (FLATTEN) NIL NIL)) NIL)) 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 NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    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 NIL)
                               ("2" (INST?)
                                (("2" (EXPAND "fseq") (("2" (PROPAX) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP*)
            (("2" (HIDE -5)
              (("2" (EXPAND "subset?")
                (("2" (EXPAND "member")
                  (("2" (INST?)
                    (("2" (ASSERT)
                      (("2" (EXPAND "edge?")
                        (("2" (FLATTEN)
                          (("2" (INST?)
                            (("1" (EXPAND "edges_of")
                              (("1" (SPLIT -4)
                                (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|gen_seq1_TCC1| "" (SKOSIMP*)
    (("" (EXPAND "verts_in?") (("" (PROPAX) NIL NIL)) NIL)) NIL)
   (|gen_seq2_TCC1| "" (SKOSIMP*)
    (("" (EXPAND "verts_in?") (("" (PROPAX) NIL NIL)) NIL)) NIL)
   (|trunc1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|trunc1_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|add1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|gen_seq1_is_walk| "" (SKOSIMP*)
    (("" (EXPAND "gen_seq1")
      (("" (EXPAND "walk?")
        (("" (EXPAND "verts_in?") (("" (SKOSIMP*) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|edge_to_walk_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|edge_to_walk_TCC2| "" (SKOSIMP*)
    (("" (EXPAND "edg")
      (("" (TYPEPRED "G!1")
        (("" (INST?)
          (("1" (ASSERT)
            (("1" (INST?)
              (("1" (HIDE -2)
                (("1" (EXPAND "dbl") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
              NIL))
            NIL)
           ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edge_to_walk_TCC3| "" (SKOSIMP*)
    (("" (TYPEPRED "G!1")
      (("" (INST?)
        (("1" (ASSERT)
          (("1" (INST -1 "v!1")
            (("1" (EXPAND "edg")
              (("1" (EXPAND "dbl") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
            NIL))
          NIL)
         ("2" (ASSERT) NIL NIL))
        NIL))
      NIL))
    NIL)
   (|edge_to_walk| "" (SKOSIMP*)
    (("" (EXPAND "walk?")
      (("" (EXPAND "gen_seq2")
        (("" (SPLIT 2)
          (("1" (EXPAND "verts_in?") (("1" (PROPAX) NIL NIL)) NIL)
           ("2" (SKOSIMP*)
            (("2" (EXPAND "fseq")
              (("2" (ASSERT)
                (("2" (EXPAND "edge?")
                  (("2" (EXPAND "edg") (("2" (PROPAX) NIL NIL)) NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk?_rev_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|walk?_rev| "" (SKOSIMP*)
    (("" (EXPAND "walk?")
      (("" (FLATTEN)
        (("" (SPLIT +)
          (("1" (HIDE -2)
            (("1" (EXPAND "verts_in?")
              (("1" (SKOSIMP*)
                (("1" (TYPEPRED "i!1")
                  (("1" (EXPAND "rev")
                    (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOSIMP*)
            (("2" (EXPAND "fseq")
              (("2" (EXPAND "edge?")
                (("2" (HIDE -2)
                  (("2" (EXPAND "rev")
                    (("2" (INST - "l(ps!1) - 2 - n!1")
                      (("1" (ASSERT)
                        (("1" (FLATTEN)
                          (("1" (ASSERT) (("1" (REWRITE "dbl_comm") NIL NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk?_reverse| "" (SKOSIMP*)
    (("" (EXPAND "walk_from?")
      (("" (FLATTEN)
        ((""
          (INST 1 "(# l := l(w1!1),
                    seq := (LAMBDA (i: below(l(w1!1))): seq(w1!1)(l(w1!1)-1-i))
  #)")
          (("1" (ASSERT) NIL NIL)
           ("2" (EXPAND "walk?")
            (("2" (SPLIT)
              (("1" (ASSERT)
                (("1" (EXPAND "verts_in?")
                  (("1" (SKOSIMP*)
                    (("1" (TYPEPRED "w1!1") (("1" (INST?) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL)
               ("2" (SKOSIMP*)
                (("2" (EXPAND "fseq")
                  (("2" (LEMMA "edge?_comm")
                    (("2" (INST?)
                      (("1" (ASSERT)
                        (("1" (HIDE 2)
                          (("1" (TYPEPRED "w1!1")
                            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                          NIL))
                        NIL)
                       ("2" (ASSERT) NIL NIL)
                       ("3" (HIDE 2)
                        (("3" (TYPEPRED "n!1") (("3" (ASSERT) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk?_caret_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|walk?_caret| "" (SKOSIMP*)
    (("" (EXPAND "walk?")
      (("" (FLATTEN)
        (("" (SPLIT +)
          (("1" (REWRITE "verts_in?_caret") NIL NIL)
           ("2" (SKOSIMP*)
            (("2" (EXPAND "fseq")
              (("2" (EXPAND "edge?")
                (("2" (EXPAND "^")
                  (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|l_trunc1_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|l_trunc1| "" (SKOSIMP*)
    (("" (EXPAND "trunc1") (("" (EXPAND "^") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 )
    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 NIL) ("2" (ASSERT) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            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 NIL)) NIL)) NIL))
                      NIL)
                     ("2" (FLATTEN) NIL NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk_concat_edge_TCC1| "" (SUBTYPE-TCC) NIL 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 NIL)
                                 ("2" (HIDE -3) (("2" (INST?) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (SKOSIMP*)
                          (("2" (CASE "n!1 < l(w1!1)")
                            (("1" (ASSERT)
                              (("1" (LIFT-IF)
                                (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL))
                                NIL))
                              NIL)
                             ("2" (ASSERT)
                              (("2" (HIDE -5)
                                (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk_concat_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|walk_concat_TCC2| "" (SKOSIMP*)
    (("" (EXPAND "o ")
      (("" (EXPAND "rev")
        (("" (EXPAND "^") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|walk_concat| "" (SKOSIMP*)
    (("" (EXPAND "walk_from?")
      (("" (FLATTEN)
        (("" (ASSERT)
          (("" (EXPAND "o ")
            (("" (EXPAND "rev")
              (("" (EXPAND "^")
                (("" (EXPAND "walk?")
                  (("" (EXPAND "fseq")
                    (("" (FLATTEN)
                      (("" (SPLIT +)
                        (("1" (EXPAND "verts_in?")
                          (("1" (SKOSIMP*)
                            (("1" (GROUND)
                              (("1" (INST?) NIL NIL)
                               ("2" (HIDE -2 -3 -4 -5 -6 -7 -9)
                                (("2" (INST - "l(w1!1) + l(w2!1) - 2 - i!1") NI
 L
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (SKOSIMP*)
                          (("2" (EXPAND "edge?")
                            (("2" (CASE "n!1 < l(w1!1) - 1")
                              (("1" (ASSERT)
                                (("1" (INST?)
                                  (("1" (ASSERT)
                                    (("1" (FLATTEN)
                                      (("1" (ASSERT)
                                        (("1"
                                          (CASE "n!1 = l(w1!1) - 1")
                                          (("1"
                                            (REPLACE -1)
                                            (("1"
                                              (HIDE -1)
                                              (("1" (ASSERT) NIL NIL))
                                              NIL))
                                            NIL)
                                           ("2"
                                            (LIFT-IF)
                                            (("2" (ASSERT) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (ASSERT)
                                (("2" (HIDE -6)
                                  (("2" (INST - "l(w1!1) + l(w2!1) - 3 - n!1")
                                    (("2" (ASSERT)
                                      (("2" (FLATTEN)
                                        (("2"
                                          (ASSERT)
                                          (("2" (REWRITE "dbl_comm") NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk?_cut_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|walk?_cut_TCC2| "" (SKOSIMP*)
    (("" (EXPAND "o ")
      (("" (EXPAND "^") (("" (LIFT-IF) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)
 )
    NIL)
   (|walk?_cut| "" (SKOSIMP*)
    (("" (EXPAND "walk_from?")
      (("" (FLATTEN)
        (("" (EXPAND "walk?")
          (("" (EXPAND "fseq")
            (("" (EXPAND "o ")
              (("" (EXPAND "^")
                (("" (EXPAND "emptyseq")
                  (("" (SPLIT 1)
                    (("1" (PROPAX) NIL NIL)
                     ("2" (FLATTEN)
                      (("2" (LIFT-IF)
                        (("2" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "verts_in?")
                              (("1" (HIDE -7)
                                (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("3" (FLATTEN)
                      (("3" (EXPAND "verts_in?")
                        (("3" (SKOSIMP*)
                          (("3" (HIDE -6)
                            (("3" (SPLIT 1)
                              (("1" (FLATTEN)
                                (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL))
                                NIL)
                               ("2" (FLATTEN)
                                (("2" (ASSERT)
                                  (("2" (TYPEPRED "i!2")
                                    (("2" (LIFT-IF)
                                      (("2" (GROUND) (("2" (INST?) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("4" (SKOSIMP*)
                      (("4" (LIFT-IF)
                        (("4" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (GROUND)
                              (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
                               ("2" (LIFT-IF)
                                (("2" (SPLIT 2)
                                  (("1" (FLATTEN)
                                    (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
 )
                                    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 NIL)
 )
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2" (ASSERT) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (FLATTEN)
                            (("2" (GROUND)
                              (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)
 )
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|walk_merge| "" (SKOSIMP*)
    (("" (CASE "l(p2!1) = 1")
      (("1" (INST 1 "rev(p1!1)")
        (("1" (EXPAND "walk_from?")
          (("1" (FLATTEN)
            (("1" (EXPAND "rev")
              (("1" (ASSERT)
                (("1" (LEMMA "walk?_rev")
                  (("1" (INST?)
                    (("1" (ASSERT)
                      (("1" (EXPAND "rev") (("1" (PROPAX) NIL NIL)) NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (EXPAND "rev") (("2" (ASSERT) NIL NIL)) NIL))
        NIL)
       ("2" (INST + "trunc1(p2!1) o rev(p1!1)")
        (("1" (EXPAND "walk_from?")
          (("1" (EXPAND "o ")
            (("1" (EXPAND "trunc1")
              (("1" (EXPAND "rev")
                (("1" (EXPAND "^")
                  (("1" (ASSERT)
                    (("1" (FLATTEN)
                      (("1" (ASSERT)
                        (("1" (EXPAND "walk?")
                          (("1" (SPLIT +)
                            (("1" (EXPAND "verts_in?")
                              (("1" (SKOSIMP*)
                                (("1" (ASSERT)
                                  (("1" (TYPEPRED "i!1")
                                    (("1" (HIDE -5 -9)
                                      (("1" (HIDE -2 -3 -5 -6)
                                        (("1"
                                          (GROUND)
                                          (("1"
                                            (HIDE -3)
                                            (("1" (INST?) NIL NIL))
                                            NIL)
                                           ("2" (INST?) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (SKOSIMP*)
                              (("2" (EXPAND "fseq")
                                (("2" (LIFT-IF)
                                  (("2" (GROUND)
                                    (("1" (EXPAND "edge?")
                                      (("1" (INST -10 "n!1")
                                        (("1"
                                          (ASSERT)
                                          (("1"
                                            (FLATTEN)
                                            (("1"
                                              (ASSERT)
                                              (("1"
                                                (LIFT-IF)
                                                (("1" (ASSERT) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2" (EXPAND "edge?")
                                      (("2"
                                        (INST -5 "l(p1!1) + l(p2!1) - 3 - n!1")
                                        (("2"
                                          (ASSERT)
                                          (("2"
                                            (FLATTEN)
                                            (("2"
                                              (ASSERT)
                                              (("2"
                                                (REWRITE "dbl_comm")
                                                NIL
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (EXPAND "o ")
          (("2" (EXPAND "rev")
            (("2" (EXPAND "trunc1")
              (("2" (EXPAND "^")
                (("2" (EXPAND "emptyseq") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("3" (ASSERT) NIL NIL))
        NIL))
      NIL))
    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_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)
  
  
     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)
  
  
  %   finite_dbl: LEMMA is_finite(dbl[T](x,y))
  
     e: VAR doubleton
     finite_doubleton: LEMMA is_finite(e)
  
     card_dbl: LEMMA x /= y IMPLIES card(dbl(x,y)) = 2
  
     JUDGEMENT dbl(x,y) HAS_TYPE finite_set[T]
  
  
  %  ------------- The following are bad
  
  %   AUTO_REWRITE+ dbl_in                
  %   AUTO_REWRITE+ dbl_not_in            
  
  
  
  END doubletons
  
  $$$doubletons.prf
  (doubletons
   (dbl_comm 0
    (dbl_comm-1 nil 3262619824 3262620019
     ("" (skosimp*)
      (("" (expand "dbl")
        (("" (apply-extensionality 1 :hide? t)
          (("" (iff) (("" (ground) nil))))))))
      nil)
     proved
     ((dbl const-decl "set[T]" doubletons nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil doubletons nil))
     67 70 nil nil))
   (doubleton_irreflexive 0
    (doubleton_irreflexive-1 nil 3262619824 3262620019
     ("" (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))))))))))))))
      nil)
     proved
     ((doubleton? const-decl "bool" doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil doubletons nil))
     138 90 nil nil))
   (doubleton_nonempty 0
    (doubleton_nonempty-1 nil 3262619824 3262620019
     ("" (auto-rewrite-defs :always? t)
      (("" (assert)
        (("" (skolem-typepred)
          (("" (skolem-typepred)
            (("" (flatten)
              (("" (replace*)
                (("" (assert)
                  (("" (inst? :if-match t :polarity? nil)
                    (("" (flatten) (("" (propax) nil))))))))))))))))))
      nil)
     proved
     ((nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil
 )
      (member const-decl "bool" sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     115 70 nil nil))
   (doubleton_rest_nonempty 0
    (doubleton_rest_nonempty-1 nil 3262619824 3262620019
     ("" (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))))))))))))))))))))))))))))
      nil)
     proved
     ((doubleton_nonempty formula-decl nil doubletons nil)
      (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil)
      (remove const-decl "set" sets nil) (nonempty? const-decl "bool" sets nil)
      (rest const-decl "set" sets nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     120 120 nil nil))
   (dbl_choose_TCC1 0
    (dbl_choose_TCC1-1 nil 3262619824 nil ("" (subtype-tcc) nil nil)
     proved-complete
     ((nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil
 )
      (member const-decl "bool" sets nil)
      (dbl const-decl "set[T]" doubletons nil)
      (T formal-type-decl nil doubletons nil))
     nil nil nil nil))
   (dbl_choose 0
    (dbl_choose-1 nil 3262619824 3262620019
     ("" (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))))))))))
      nil)
     proved
     ((dbl const-decl "set[T]" doubletons nil)
      (pred type-eq-decl nil defined_types nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (TRUE const-decl "bool" booleans nil)
      (epsilon_ax formula-decl nil epsilons nil)
      (T formal-type-decl nil doubletons nil)
      (choose const-decl "(p)" sets nil))
     104 70 nil nil))
   (dbl_rest_choose_TCC1 0
    (dbl_rest_choose_TCC1-1 nil 3262619824 nil
     ("" (skosimp*)
      (("" (use "doubleton_rest_nonempty") (("" (inst?) (("" (assert) nil))))))
      nil)
     proved-incomplete
     ((T formal-type-decl nil doubletons nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (/= const-decl "boolean" notequal nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (doubleton_rest_nonempty formula-decl nil doubletons nil))
     nil nil nil nil))
   (dbl_rest_choose 0
    (dbl_rest_choose-1 nil 3262619824 3262620020
     ("" (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))))))))))))
      nil)
     proved
     ((rest const-decl "set" sets nil)
      (y!1 skolem-const-decl "T" doubletons nil)
      (x!1 skolem-const-decl "T" doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (remove const-decl "set" sets nil) (member const-decl "bool" sets nil)
      (epsilon_ax formula-decl nil epsilons nil)
      (TRUE const-decl "bool" booleans nil)
      (pred type-eq-decl nil defined_types nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (choose const-decl "(p)" sets nil)
      (dbl_choose formula-decl nil doubletons nil)
      (nonempty? const-decl "bool" sets nil)
      (doubleton_nonempty formula-decl nil doubletons nil))
     350 300 nil nil))
   (dbl_to_pair_TCC1 0
    (dbl_to_pair_TCC1-1 nil 3262619824 nil
     ("" (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))))
      nil)
     proved-incomplete
     ((T formal-type-decl nil doubletons nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (/= const-decl "boolean" notequal nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil)
      (rest const-decl "set" sets nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (dbl_comm formula-decl nil doubletons nil)
      (dbl_rest_choose formula-decl nil doubletons nil)
      (dbl_choose formula-decl nil doubletons nil)
      (doubleton_rest_nonempty formula-decl nil doubletons nil)
      (doubleton_nonempty formula-decl nil doubletons nil))
     nil nil nil nil))
   (dbl_def 0
    (dbl_def-1 nil 3262619824 3262620020 ("" (skosimp*) (("" (assert) nil)) nil
 )
     proved nil 16 20 nil nil))
   (dbl_in 0
    (dbl_in-1 nil 3262619824 3262620020
     ("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil
 )
     proved ((dbl const-decl "set[T]" doubletons nil)) 38 40 nil nil))
   (dbl_not_in 0
    (dbl_not_in-1 nil 3262619824 3262620020
     ("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil
 )
     proved ((dbl const-decl "set[T]" doubletons nil)) 43 50 nil nil))
   (dbl_to_pair_lem_TCC1 0
    (dbl_to_pair_lem_TCC1-1 nil 3262619824 nil ("" (subtype-tcc) nil nil)
     proved-complete
     ((/= const-decl "boolean" notequal nil)
      (T formal-type-decl nil doubletons nil))
     nil nil nil nil))
   (dbl_to_pair_lem 0
    (dbl_to_pair_lem-1 nil 3262619824 3262620020
     ("" (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))))))
      nil)
     proved
     ((dbl_to_pair const-decl "{x, y | D = dbl(x, y)}" doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (y!1 skolem-const-decl "T" doubletons nil)
      (x!1 skolem-const-decl "T" doubletons nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil))
     326 300 nil nil))
   (dbl_to_pair_inverse_l 0
    (dbl_to_pair_inverse_l-1 nil 3262619824 3262620020
     ("" (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))))))))))))))
      nil)
     proved
     ((dbl_to_pair_lem formula-decl nil doubletons nil)
      (dbl_comm formula-decl nil doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     108 90 nil nil))
   (dbl_proj 0
    (dbl_proj-1 nil 3262619824 3262620020
     ("" (skosimp*)
      (("" (lemma "dbl_to_pair_inverse_l")
        (("" (inst?)
          (("" (expand "dbl") (("" (replace -1 + rl) (("" (assert) nil)))))))))
 )
      nil)
     proved
     ((dbl_to_pair_inverse_l formula-decl nil doubletons nil)
      (doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (set type-eq-decl nil sets nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (T formal-type-decl nil doubletons nil))
     49 40 nil nil))
   (proj_dbl 0
    (proj_dbl-1 nil 3262619824 3262620020
     ("" (skosimp*)
      (("" (typepred "D!1")
        (("" (skosimp*)
          (("" (replace -1)
            (("" (hide -1)
              (("" (lemma "dbl_to_pair_lem")
                (("" (inst?) (("" (assert) (("" (grind) nil))))))))))))))))
      nil)
     proved
     ((doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (dbl_to_pair_lem formula-decl nil doubletons nil))
     104 80 nil nil))
   (dbl_eq 0
    (dbl_eq-1 nil 3262619824 3262620021
     ("" (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))))
      nil)
     proved
     ((dbl const-decl "set[T]" doubletons nil) (set type-eq-decl nil sets nil)
      (T formal-type-decl nil doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil))
     133 130 nil nil))
   (finite_dbl 0
    (finite_dbl-1 nil 3262619839 3262620021
     ("" (skosimp*)
      (("" (case-replace "dbl[T](x!1, y!1) = add(x!1,singleton(y!1))")
        (("1" (hide -1) (("1" (rewrite "finite_add") nil nil)) nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((T formal-type-decl nil doubletons nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (nonempty? const-decl "bool" sets nil)
      (add const-decl "(nonempty?)" sets nil)
      (singleton? const-decl "bool" sets nil)
      (singleton const-decl "(singleton?)" sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (finite_add formula-decl nil finite_sets nil)
      (member const-decl "bool" sets nil))
     175 140 t nil))
   (finite_doubleton 0
    (finite_doubleton-1 nil 3262619876 3262620021
     ("" (skosimp*)
      (("" (typepred "e!1")
        (("" (skosimp*)
          (("" (replace -1)
            (("" (hide -1) (("" (rewrite "finite_dbl") nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((doubleton type-eq-decl nil doubletons nil)
      (dbl const-decl "set[T]" doubletons nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (T formal-type-decl nil doubletons nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (finite_dbl formula-decl nil doubletons nil))
     44 40 nil nil))
   (card_dbl_TCC1 0
    (card_dbl_TCC1-1 nil 3262619970 3262620011
     ("" (skosimp*) (("" (lemma "finite_dbl") (("" (inst?) nil nil)) nil)) nil)
     proved
     ((finite_dbl formula-decl nil doubletons nil)
      (T formal-type-decl nil doubletons nil))
     12208 1430 t shostak))
   (card_dbl 0
    (card_dbl-1 nil 3262619942 3262620021
     ("" (skosimp*)
      (("" (case-replace "dbl(x!1, y!1) = add(x!1,singleton(y!1))")
        (("1" (hide -1)
          (("1" (rewrite "card_add")
            (("1" (rewrite "card_singleton")
              (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (hide 3)
          (("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((T formal-type-decl nil doubletons nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (set type-eq-decl nil sets nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (dbl const-decl "set[T]" doubletons nil)
      (nonempty? const-decl "bool" sets nil)
      (add const-decl "(nonempty?)" sets nil)
      (singleton? const-decl "bool" sets nil)
      (singleton const-decl "(singleton?)" sets nil)
      (finite_set type-eq-decl nil finite_sets nil)
      (is_finite const-decl "bool" finite_sets nil)
      (card_add formula-decl nil finite_sets nil)
      (card_singleton formula-decl nil finite_sets nil)
      (member const-decl "bool" sets nil))
     502 460 nil nil))
   (dbl_TCC1 0
    (dbl_TCC1-1 nil 3262619970 3262620055
     ("" (skosimp*) (("" (rewrite "finite_dbl") nil nil)) nil) proved
     ((finite_dbl formula-decl nil doubletons nil)
      (T formal-type-decl nil doubletons nil))
     11617 970 t shostak)))
  
  
  $$$graphs.pvs
  graphs[T: TYPE]: THEORY
  %----------------------------------------------------------------------------
 ---
  %
  % Defines:
  %
  %      Graph[T] -- graph over domain T
  %      vert(G)  -- vertices of graph G
  %      edges(G) -- set of edges in a graph 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], 
              doubletons[T] 
              %finite_sets@finite_sets[doubleton[T]]
  
    R: VAR PRED[[T, T]]
    x,y,v: VAR T
  
    pregraph: TYPE = [# vert : finite_set[T],
                        edges: finite_set[doubleton[T]] #]
  
    graph: TYPE = {g: pregraph | (FORALL (e: doubleton[T]): edges(g)(e) IMPLIES
                                       (FORALL (x: T): e(x) IMPLIES vert(g)(x))
 )}
   
    e: VAR doubleton[T]
    G: var graph
   
    edg(x,(y:{y:T | y /= x})): doubleton[T] = dbl[T](x,y)
  
    edge?(G)(x,y): bool = x /= y AND edges(G)(dbl[T](x,y))
  
  %  edge?_comm : LEMMA edge?(G)(y, x) IMPLIES edge?(G)(x, y)
  
  %  edges_vert      : LEMMA e(x) AND edges(G)(e) IMPLIES
  %                             (EXISTS y: x /= y AND vert(G)(y) AND e(y))
  
  
  %  other_vert      : LEMMA e(v) AND edges(G)(e)
  %                         IMPLIES (EXISTS (u: T): u /= v AND vert(G)(u) 
  %                                                 AND e = dbl[T](u, v))
  
  %  edge_has_2_verts: LEMMA x /= v AND e(x) AND e(v)
  %                                   IMPLIES e = dbl(x,v)
  
  %   dbl_uneq: LEMMA e=dbl[T](x,y) IMPLIES x /=y
  
  %   edges_symm:  LEMMA edges(G)(e) AND e=(dbl[T](x,y)) IMPLIES 
  %		edges(G)(dbl[T](y,x))
  
  
    Graph: TYPE = {g: graph | nonempty?(vert(g))}
  
  
  END graphs
  
  
  $$$graphs.prf
  (|graphs|
   (|edg_TCC1| "" (SKOSIMP*) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL))
    NIL)
   (|edge?_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|edge?_comm| "" (SKOSIMP*)
    (("" (EXPAND "edge?")
      (("" (REWRITE "dbl_comm")
        (("" (FLATTEN) (("" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|edges_vert| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (LEMMA "dbl_to_pair_lem")
              (("" (INST?)
                (("" (ASSERT)
                  (("" (PROP)
                    (("1" (HIDE -1)
                      (("1" (EXPAND "dbl" -1)
                        (("1" (PROP)
                          (("1" (INST 2 "y!1")
                            (("1" (ASSERT)
                              (("1" (TYPEPRED "G!1")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (ASSERT)
                                    (("1"
                                      (INST -1 "y!1")
                                      (("1"
                                        (EXPAND "dbl")
                                        (("1" (PROPAX) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL)
                                   ("2"
                                    (INST?)
                                    (("2" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (REPLACE -1)
                            (("2" (HIDE -1)
                              (("2" (INST?)
                                (("2"
                                  (TYPEPRED "G!1")
                                  (("2"
                                    (INST?)
                                    (("1"
                                      (ASSERT)
                                      (("1"
                                        (INST?)
                                        (("1"
                                          (EXPAND "dbl")
                                          (("1" (PROPAX) NIL NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (INST?)
                                      (("2"
                                        (ASSERT)
                                        (("2"
                                          (HIDE -1 3)
                                          (("2"
                                            (APPLY-EXTENSIONALITY
                                             :HIDE?
                                             T)
                                            (("2" (GRIND) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (HIDE -1)
                      (("2" (EXPAND "dbl" -1)
                        (("2" (SPLIT)
                          (("1" (REPLACE -1)
                            (("1" (HIDE -1)
                              (("1" (INST 2 "y!1")
                                (("1"
                                  (ASSERT)
                                  (("1"
                                    (TYPEPRED "G!1")
                                    (("1"
                                      (INST?)
                                      (("1"
                                        (ASSERT)
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (EXPAND "dbl")
                                            (("1" (PROPAX) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2"
                                        (INST?)
                                        (("2" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (REPLACE -1)
                            (("2" (HIDE -1)
                              (("2" (INST 2 "x!2")
                                (("2"
                                  (ASSERT)
                                  (("2"
                                    (TYPEPRED "G!1")
                                    (("2"
                                      (INST?)
                                      (("1"
                                        (ASSERT)
                                        (("1"
                                          (INST?)
                                          (("1"
                                            (EXPAND "dbl")
                                            (("1" (PROPAX) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2"
                                        (INST?)
                                        (("2" (ASSERT) NIL NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|other_vert| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (EXPAND "dbl" -1)
              (("" (PROP)
                (("1" (REPLACE -1)
                  (("1" (HIDE -1)
                    (("1" (INST 2 "y!1")
                      (("1" (TYPEPRED "G!1")
                        (("1" (INST?)
                          (("1" (ASSERT)
                            (("1" (INST -1 "y!1")
                              (("1" (EXPAND "dbl" -1)
                                (("1"
                                  (ASSERT)
                                  (("1"
                                    (HIDE -1 -2)
                                    (("1"
                                      (APPLY-EXTENSIONALITY 2 :HIDE? T)
                                      (("1" (GRIND) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (INST?)
                            (("2" (ASSERT)
                              (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                                (("2" (GRIND) NIL NIL)) NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (REPLACE -1)
                  (("2" (HIDE -1)
                    (("2" (INST 2 "x!1")
                      (("2" (TYPEPRED "G!1")
                        (("2" (INST?)
                          (("1" (ASSERT)
                            (("1" (INST -1 "x!1")
                              (("1" (ASSERT)
                                (("1"
                                  (EXPAND "dbl")
                                  (("1" (PROPAX) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edge_has_2_verts| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (APPLY-EXTENSIONALITY 3 :HIDE? T)
              (("" (EXPAND "dbl")
                (("" (IFF) (("" (GROUND) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|dbl_uneq| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (LEMMA "dbl_eq")
          (("" (INST -1 "x!2" "x!1" "y!1" "y!2")
            (("" (REPLACE -3 -2 LR)
              (("" (BDDSIMP)
                (("1" (REPLACE -2 -5 LR)
                  (("1" (REPLACE -3 -5 LR) (("1" (PROPAX) NIL NIL)) NIL))
                  NIL)
                 ("2" (REPLACE -2 -5 LR)
                  (("2" (REPLACE -3 -5 LR) (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edges_symm_TCC1| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (INST 2 "x!2" "y!2")
          (("" (REPLACE -3 -1)
            (("" (LEMMA "dbl_comm")
              (("" (INST -1 "y!1" "x!1")
                (("" (REPLACE -1 2 LR) (("" (ASSERT) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edges_symm| "" (SKOSIMP*)
    (("" (LEMMA "dbl_comm")
      (("" (INST? -1)
        (("" (REPLACE -3 -2 LR)
          (("" (REPLACE -1 -2 LR) (("" (PROPAX) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|empty?_rew| "" (SKOSIMP*)
    (("" (LEMMA " card_empty?[T]")
      (("" (INST?)
        (("" (EXPAND "empty?" 1)
          (("" (REPLACE -1) (("" (PROPAX) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL)
   (|edges_of_empty| "" (SKOSIMP*)
    (("" (EXPAND "empty?")
      (("" (APPLY-EXTENSIONALITY 1 :HIDE? T)
        (("" (EXPAND "emptyset")
          (("" (EXPAND "empty?")
            (("" (TYPEPRED "x!1")
              (("" (SKOSIMP*)
                (("" (INST -3 "y!1")
                  (("" (EXPAND "member")
                    (("" (TYPEPRED "G!1")
                      (("" (INST?)
                        (("" (ASSERT)
                          (("" (INST -1 "y!1")
                            (("" (REPLACE -2)
                              (("" (EXPAND "dbl") (("" (PROPAX) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|singleton_edges| "" (SKOSIMP*)
    (("" (EXPAND "singleton?")
      (("" (EXPAND "size")
        (("" (LEMMA "card_one[T]")
          (("" (INST?)
            (("" (ASSERT)
              (("" (HIDE -2)
                (("" (SKOSIMP*)
                  (("" (EXPAND "empty?")
                    (("" (SKOSIMP*)
                      (("" (EXPAND "member")
                        (("" (TYPEPRED "x!2")
                          (("" (SKOSIMP*)
                            (("" (REPLACE -1)
                              (("" (HIDE -1)
                                ((""
                                  (TYPEPRED "G!1")
                                  ((""
                                    (INST?)
                                    (("1"
                                      (ASSERT)
                                      (("1"
                                        (INST-CP -1 "x!3")
                                        (("1"
                                          (INST -1 "y!1")
                                          (("1"
                                            (EXPAND "dbl")
                                            (("1"
                                              (HIDE -4)
                                              (("1"
                                                (REPLACE -3)
                                                (("1"
                                                  (HIDE -3)
                                                  (("1"
                                                    (EXPAND "singleton")
                                                    (("1"
                                                      (ASSERT)
                                                      NIL
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2"
                                      (INST?)
                                      (("2" (ASSERT) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|edge_in_card_gt_1| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (REPLACE -1)
          (("" (HIDE -1)
            (("" (TYPEPRED "G!1")
              (("" (ASSERT)
                (("" (INST?)
                  (("1" (ASSERT)
                    (("1" (HIDE -2)
                      (("1" (INST-CP -1 "x!1")
                        (("1" (INST -1 "y!1")
                          (("1" (EXPAND "dbl")
                            (("1"
                              (CASE "subset?(add(x!1,singleton(y!1)),vert(G!1))
 ")
                              (("1" (LEMMA "card_subset[T]")
                                (("1"
                                  (INST?)
                                  (("1"
                                    (REWRITE "card_add")
                                    (("1"
                                      (REWRITE "card_singleton")
                                      (("1"
                                        (ASSERT)
                                        (("1"
                                          (HIDE -2)
                                          (("1"
                                            (EXPAND "singleton")
                                            (("1" (ASSERT) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (GRIND) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    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 NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|singleton_graph_TCC1| "" (SKOSIMP*)
    (("" (EXPAND "emptyset") (("" (PROPAX) NIL NIL)) NIL)) NIL)
   (|is_sing| "" (SKOSIMP*)
    (("" (EXPAND "singleton_graph")
      (("" (EXPAND "singleton?")
        (("" (EXPAND "size") (("" (REWRITE "card_singleton") NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|finite_dbl| "" (SKOSIMP*)
    (("" (CASE-REPLACE "dbl[T](x!1, y!1) = add(x!1,singleton(y!1))")
      (("1" (HIDE -1) (("1" (REWRITE "finite_add") NIL NIL)) NIL)
       ("2" (HIDE 2)
        (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|finite_doubleton| "" (SKOSIMP*)
    (("" (TYPEPRED "e!1")
      (("" (SKOSIMP*)
        (("" (REPLACE -1)
          (("" (HIDE -1) (("" (REWRITE "finite_dbl") NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|card_dbl_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_dbl") NIL NIL))
    NIL)
   (|card_dbl| "" (SKOSIMP*)
    (("" (CASE-REPLACE "dbl(x!1, y!1) = add(x!1,singleton(y!1))")
      (("1" (HIDE -1)
        (("1" (REWRITE "card_add")
          (("1" (REWRITE "card_singleton")
            (("1" (EXPAND "singleton") (("1" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL)
       ("2" (HIDE 3)
        (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|dbl_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_dbl") NIL NIL)) NIL))
  
  
  $$$paths.pvs
  paths[T: TYPE]: THEORY
  
  BEGIN
  
     IMPORTING graphs[T], walks[T], seq_def
  
     G: VAR graph[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)
  
  
  
  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?_rev_TCC1| "" (SUBTYPE-TCC) NIL)
   (|path?_rev| "" (SKOSIMP*)
    (("" (EXPAND "path?")
      (("" (FLATTEN)
        (("" (REWRITE "walk?_rev")
          (("" (ASSERT)
            (("" (SKOSIMP*)
              (("" (EXPAND "fseq")
                (("" (TYPEPRED "i!1")
                  (("" (TYPEPRED "j!1")
                    (("" (EXPAND "rev")
                      (("" (INST?)
                        (("1" (INST - "l(ps!1) - 1 - j!1")
                          (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))
                         ("2" (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" (FLATTEN)
                  (("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))))))))))))))
  
  $$$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 NIL)) NIL)
   (|min_in| "" (TYPEPRED "min")
    (("" (EXPAND "minimal?") (("" (FLATTEN) (("" (PROPAX) NIL)))))))
   (|min_is_min| "" (SKOSIMP*)
    (("" (TYPEPRED "min")
      (("" (EXPAND "minimal?")
        (("" (FLATTEN) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL))
      NIL))
    NIL))

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools