:: GRAPH_4  semantic presentation begin  


























definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "x", "y" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); let "e" be    ($#m1_hidden :::"set"::: )  ; pred "e" :::"orientedly_joins"::: "x" "," "y" means :: GRAPH_4:def 1 (Bool  "("  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  "e")  ($#r1_hidden :::"="::: )  "x") & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  "e")  ($#r1_hidden :::"="::: )  "y")  ")" ); end; 







:: deftheorem    defines :::"orientedly_joins"::: GRAPH_4:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "e"))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool  "("  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "x"))) & (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Var "y")))  ")" )  ")" )))); 
 
theorem :: GRAPH_4:1 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "e"))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Var "v1")) "," (Set (Var "v2")))) "holds"  (Bool (Set (Var "e"))  ($#r2_graph_1 :::"joins"::: )  (Set (Var "v1")) "," (Set (Var "v2")))))) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "x", "y" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "G"))); pred "x" "," "y" :::"are_orientedly_incident":::  means :: GRAPH_4:def 2 (Bool  "ex" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")) & (Bool (Set (Var "v"))  ($#r1_graph_4 :::"orientedly_joins"::: )  "x" "," "y")  ")" )); end; 






:: deftheorem    defines :::"are_orientedly_incident"::: GRAPH_4:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r2_graph_4 :::"are_orientedly_incident"::: )  ) "iff" (Bool  "ex" (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool (Set (Var "v"))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Var "x")) "," (Set (Var "y")))  ")" ))  ")" ))); 
 
theorem :: GRAPH_4:2 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "," (Set (Var "v4")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "e"))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Var "e"))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Var "v3")) "," (Set (Var "v4")))) "holds"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Var "v3"))) & (Bool (Set (Var "v2"))  ($#r1_hidden :::"="::: )  (Set (Var "v4")))  ")" )))) ; 
 









definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "X" be    ($#m1_hidden :::"set"::: )  ; func "G" :::"-SVSet"::: "X" ->    ($#m1_hidden :::"set"::: )   equals :: GRAPH_4:def 3  "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool  "ex" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  "}"  ; end; 






:: deftheorem    defines :::"-SVSet"::: GRAPH_4:def 3 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "G"))  ($#k1_graph_4 :::"-SVSet"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool  "ex" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  "}"  ))); 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "X" be    ($#m1_hidden :::"set"::: )  ; func "G" :::"-TVSet"::: "X" ->    ($#m1_hidden :::"set"::: )   equals :: GRAPH_4:def 4  "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Element":::) "of" "G" : (Bool  "ex" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" "G")  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  "}"  ; end; 






:: deftheorem    defines :::"-TVSet"::: GRAPH_4:def 4 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "G"))  ($#k2_graph_4 :::"-TVSet"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) : (Bool  "ex" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "v"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))  ")" ))  "}"  ))); 
 
theorem :: GRAPH_4:3 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "G"))  ($#k1_graph_4 :::"-SVSet"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Set (Var "G"))  ($#k2_graph_4 :::"-TVSet"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "vs" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "G"))); let "c" be   ($#m1_hidden :::"FinSequence":::); pred "vs" :::"is_oriented_vertex_seq_of"::: "c" means :: GRAPH_4:def 5 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "vs")  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  "c" ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "c"))) "holds"  (Bool (Set "c"  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set "vs"  ($#k7_partfun1 :::"/."::: )  (Set (Var "n"))) "," (Set "vs"  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_oriented_vertex_seq_of"::: GRAPH_4:def 5 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c"))) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_graph_4 :::"orientedly_joins"::: )  (Set (Set (Var "vs"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n"))) "," (Set (Set (Var "vs"))  ($#k7_partfun1 :::"/."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" )  ")" )  ")" )))); 
 
theorem :: GRAPH_4:4 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))))) ; 
 
theorem :: GRAPH_4:5 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k1_graph_4 :::"-SVSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs"))))))) ; 
 
theorem :: GRAPH_4:6 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "G"))  ($#k2_graph_4 :::"-TVSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs"))))))) ; 
 
theorem :: GRAPH_4:7 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "vs")))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k1_graph_4 :::"-SVSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "G"))  ($#k2_graph_4 :::"-TVSet"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "c")) ")" ) ")" )))))) ; 
 begin  
theorem :: GRAPH_4:8 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds"  (Bool (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) )  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 
theorem :: GRAPH_4:9 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st" (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))))) ; 
 
theorem :: GRAPH_4:10 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Var "vs2"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Var "vs1"))  ($#r1_hidden :::"="::: )  (Set (Var "vs2")))))) ; 
 definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "c" be   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Const "G")); assume 
(Bool (Set (Const "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))
 ; func  :::"oriented-vertex-seq"::: "c" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") means :: GRAPH_4:def 6 (Bool it  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  "c"); end; 







:: deftheorem    defines :::"oriented-vertex-seq"::: GRAPH_4:def 6 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_4 :::"oriented-vertex-seq"::: )  (Set (Var "c")))) "iff" (Bool (Set (Var "b3"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))  ")" )))); 
 
theorem :: GRAPH_4:11 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "," (Set (Var "vs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Var "c1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "vs1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))) "holds"  (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c1"))))))) ; 
 
theorem :: GRAPH_4:12 (Bool  "for" (Set (Var "q")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "c"))))) "holds"  (Bool (Set (Var "q")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))))))) ; 
 
theorem :: GRAPH_4:13 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "," (Set (Var "vs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))) & (Bool (Set (Var "c1"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "c")))) & (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c"))) & (Bool (Set (Var "vs1"))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "m")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set (Var "vs"))))) "holds"  (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c1"))))))) ; 
 
theorem :: GRAPH_4:14 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c1"))) & (Bool (Set (Var "vs2"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c2"))) & (Bool (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs2"))  ($#k1_funct_1 :::"."::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "c1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "c2"))) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_4:15 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "," (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "," (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c1"))) & (Bool (Set (Var "vs2"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c2"))) & (Bool (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs2"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c1"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "c2")))) & (Bool (Set (Var "vs"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs1"))  ($#k4_graph_2 :::"^'"::: )  (Set (Var "vs2"))))) "holds"  (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))))) ; 
 begin  definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "IT" be   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Const "G")); attr "IT" is  :::"Simple":::  means :: GRAPH_4:def 7 (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  "IT") & (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))) "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs"))))  ")" )  ")" )  ")" )); end; 





:: deftheorem    defines :::"Simple"::: GRAPH_4:def 7 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_graph_4 :::"Simple"::: )  ) "iff" (Bool  "ex" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "IT"))) & (Bool  "("   "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m"))) & (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set (Var "m"))))) "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set (Var "m"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs"))))  ")" )  ")" )  ")" ))  ")" ))); 
 registrationlet "G" be   ($#l1_graph_1 :::"Graph":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v7_graph_1 :::"oriented"::: )     ($#v1_graph_4 :::"Simple"::: )    for    ($#m1_graph_1 :::"Chain"::: )   "of" "G"; 
end; registrationlet "G" be   ($#l1_graph_1 :::"Graph":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )    for    ($#m1_graph_1 :::"Chain"::: )   "of" "G"; 
end; 
theorem :: GRAPH_4:16 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "q")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "q"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))))) ; 
 



theorem :: GRAPH_4:17 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "sc")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Set (Var "sc"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_4:18 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "sc")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "sc9")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "sc9"))  ($#r1_hidden :::"="::: )  (Set (Var "sc")))) "holds"  (Bool (Set (Var "sc9")) "is"   ($#v1_graph_4 :::"Simple"::: )  )))) ; 
 
theorem :: GRAPH_4:19 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "sc9")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#v1_graph_4 :::"Simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Var "sc9")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))))) ; 
 




theorem :: GRAPH_4:20 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_graph_4 :::"Simple"::: )  )) & (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "fc")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c"))(Bool  "ex" (Set (Var "fvs")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "vs"))(Bool  "ex" (Set (Var "c1")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))(Bool  "ex" (Set (Var "vs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c1")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))) & (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c1"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")) ")" ))) & (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set (Var "fc")))  ($#r1_hidden :::"="::: )  (Set (Var "c1"))) & (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set (Var "fvs")))  ($#r1_hidden :::"="::: )  (Set (Var "vs1")))  ")" )))))))) ; 
 
theorem :: GRAPH_4:21 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "vs"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool  "ex" (Set (Var "fc")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "c"))(Bool  "ex" (Set (Var "fvs")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "vs"))(Bool  "ex" (Set (Var "sc")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))(Bool  "ex" (Set (Var "vs1")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set (Var "fc")))  ($#r1_hidden :::"="::: )  (Set (Var "sc"))) & (Bool (Set   ($#k15_finseq_1 :::"Seq"::: )  (Set (Var "fvs")))  ($#r1_hidden :::"="::: )  (Set (Var "vs1"))) & (Bool (Set (Var "vs1"))  ($#r3_graph_4 :::"is_oriented_vertex_seq_of"::: )  (Set (Var "sc"))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs1"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs1")) ")" )))  ")" )))))))) ; 
 
theorem :: GRAPH_4:22 (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  "st" (Bool (Bool (Set (Var "p")) "is"   ($#m2_graph_1 :::"OrientedPath":::) "of" (Set (Var "G")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )) "is"   ($#m2_graph_1 :::"OrientedPath":::) "of" (Set (Var "G")))))) ; 
 
theorem :: GRAPH_4:23 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "sc")) "being"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Var "sc")) "is"   ($#m2_graph_1 :::"OrientedPath":::) "of" (Set (Var "G"))))) ; 
 
theorem :: GRAPH_4:24 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c1")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "c1")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v1_graph_4 :::"Simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))) "implies" (Bool (Set (Var "c1")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))  ")"  &  "("  (Bool (Bool (Set (Var "c1")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))) "implies" (Bool (Set (Var "c1")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v1_graph_4 :::"Simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))  ")"  &  "("  (Bool (Bool (Set (Var "c1")) "is"   ($#v7_graph_1 :::"oriented"::: )     ($#v3_graph_2 :::"simple"::: )     ($#m2_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))) "implies" (Bool (Set (Var "c1")) "is"   ($#m2_graph_1 :::"OrientedPath":::) "of" (Set (Var "G")))  ")"   ")" ))) ;