:: MSSCYC_1  semantic presentation begin  







definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); redefine mode  :::"Chain":::  "of" "G" means :: MSSCYC_1:def 1 (Bool  "("  (Bool it "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "G")) & (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st" (Bool (Set (Var "p"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  it))  ")" ); end; 





:: deftheorem    defines :::"Chain"::: MSSCYC_1:def 1 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))) "iff" (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G")))) & (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st" (Bool (Set (Var "p"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "b2"))))  ")" )  ")" ))); 
 
theorem :: MSSCYC_1:1 canceled; 
 
theorem :: MSSCYC_1:2 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set  "(" (Num 1) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  "(" (Num 1) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set  "(" (Set (Var "p"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "q")) ")" ))))) ; 
 notationlet "G" be   ($#l1_graph_1 :::"Graph":::); let "IT" be    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Const "G")); synonym  :::"directed"::: "IT" for  :::"oriented"::: ; end; definitionlet "G" be   ($#l1_graph_1 :::"Graph":::); let "IT" be    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Const "G")); attr "IT" is  :::"cyclic":::  means :: MSSCYC_1:def 2 (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  "IT") & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" )))  ")" )); end; 





:: deftheorem    defines :::"cyclic"::: MSSCYC_1:def 2 :  (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  ) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "IT"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" )))  ")" ))  ")" ))); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v11_struct_0 :::"void"::: )   bbbadV14_STRUCT_0()  for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; 
theorem :: MSSCYC_1:3 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"  (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G"))) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G"))) ")" ))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  bbbadV14_STRUCT_0()   ($#v1_graph_1 :::"strict"::: )     ($#v4_graph_1 :::"simple"::: )     ($#v5_graph_1 :::"connected"::: )     ($#v6_graph_1 :::"finite"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; 
theorem :: MSSCYC_1:4 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "," (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))) & (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e"))))) "holds"  (Bool (Set  ($#k4_pre_poly :::"<*"::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_pre_poly :::"*>"::: ) )  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: MSSCYC_1:5 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))) "holds"  (Bool (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ) "is"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))))) ; 
 


registrationlet "G" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV2_FUNCT_1()  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )     ($#v7_graph_1 :::"directed"::: )    for    ($#m1_graph_1 :::"Chain"::: )   "of" "G"; 
end; 
theorem :: MSSCYC_1:6 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"    ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (Bool  "for" (Set (Var "vs")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  "st" (Bool (Bool (Set (Var "c")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  ) & (Bool (Set (Var "vs"))  ($#r1_graph_2 :::"is_vertex_seq_of"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set (Var "vs"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "vs")) ")" )))))) ; 
 
theorem :: MSSCYC_1:7 (Bool  "for" (Set (Var "G")) "being"   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "G"))))) "holds"  (Bool  "for" (Set (Var "fe")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "fe"))  ($#r1_hidden :::"="::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))) "holds"  (Bool (Set   ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "fe")))  ($#r1_hidden :::"="::: )  (Set  ($#k10_finseq_1 :::"<*"::: ) (Set  "(" (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) "," (Set  "(" (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))) ; 
 
theorem :: MSSCYC_1:8 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))))) ; 
 
theorem :: MSSCYC_1:9 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_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"))))) "holds"  (Bool (Set  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "c"))) "is"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))))) ; 
 
theorem :: MSSCYC_1:10 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "oc")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "oc")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 registrationlet "G" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::); let "oc" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Const "G")); 
cluster (Set   ($#k7_graph_2 :::"vertex-seq"::: )  "oc") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: MSSCYC_1:11 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "oc")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  (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 "oc"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "oc"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "oc"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )))  ")" )))) ; 
 
theorem :: MSSCYC_1:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"FinSequence":::)  "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 "f"))))) "holds"  (Bool  "not" (Bool (Set  "(" (Set (Var "m")) "," (Set (Var "n")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "f"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 
theorem :: MSSCYC_1: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"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "c1")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_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")) ")"   ($#k1_graph_2 :::"-cut"::: )  (Set (Var "c"))))) "holds"  (Bool (Set   ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c1")))  ($#r1_hidden :::"="::: )  (Set  "(" (Set (Var "m")) "," (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")"   ($#k2_graph_2 :::"-cut"::: )  (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c")) ")" )))))) ; 
 
theorem :: MSSCYC_1:14 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "oc")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"  (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "oc")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "G")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "oc"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "oc")) ")" ) ")" ))))) ; 
 
theorem :: MSSCYC_1:15 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c1")) "," (Set (Var "c2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c1")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c1")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c2")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))) "iff" (Bool (Set (Set (Var "c1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "c2"))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))  ")" ))) ; 
 
theorem :: MSSCYC_1:16 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "," (Set (Var "c1")) "," (Set (Var "c2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "c2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c1")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))) & (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c2")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))  ")" ))) ; 
 
theorem :: MSSCYC_1:17 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "oc")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "oc")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "oc")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "oc")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))))) ; 
 
theorem :: MSSCYC_1:18 (Bool  "for" (Set (Var "G")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_graph_1 :::"Graph":::)  (Bool  "for" (Set (Var "c")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "c")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  )) "holds"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "ch")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "ch")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "ch"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "c"))) "is"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "G")))  ")" ))))) ; 
 definitionlet "IT" be   ($#l1_graph_1 :::"Graph":::); attr "IT" is  :::"directed_cycle-less":::  means :: MSSCYC_1:def 3 (Bool  "for" (Set (Var "dc")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" "IT"  "st" (Bool (Bool (Bool  "not" (Set (Var "dc")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "not" (Bool (Set (Var "dc")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  ))); end; 




:: deftheorem    defines :::"directed_cycle-less"::: MSSCYC_1:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_msscyc_1 :::"directed_cycle-less"::: )  ) "iff" (Bool  "for" (Set (Var "dc")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "IT"))  "st" (Bool (Bool (Bool  "not" (Set (Var "dc")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "not" (Bool (Set (Var "dc")) "is"   ($#v1_msscyc_1 :::"cyclic"::: )  )))  ")" )); 
 notationlet "IT" be   ($#l1_graph_1 :::"Graph":::); antonym  :::"with_directed_cycle"::: "IT" for  :::"directed_cycle-less"::: ; end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v11_struct_0 :::"void"::: )    ->   ($#v2_msscyc_1 :::"directed_cycle-less"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; definitionlet "IT" be   ($#l1_graph_1 :::"Graph":::); attr "IT" is  :::"well-founded":::  means :: MSSCYC_1:def 4 (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "IT") (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" "IT"  "st" (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "v")))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))))); end; 




:: deftheorem    defines :::"well-founded"::: MSSCYC_1:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_graph_1 :::"Graph":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_msscyc_1 :::"well-founded"::: )  ) "iff" (Bool  "for" (Set (Var "v")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "IT"))) (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "c")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set (Var "IT"))  "st" (Bool (Bool (Bool  "not" (Set (Var "c")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Set  "("  ($#k7_graph_2 :::"vertex-seq"::: )  (Set (Var "c")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "v")))) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))))))  ")" )); 
 registrationlet "G" be   ($#v11_struct_0 :::"void"::: )    ($#l1_graph_1 :::"Graph":::); 
cluster   ->   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_graph_1 :::"Chain"::: )   "of" "G"; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v11_struct_0 :::"void"::: )    ->   ($#v3_msscyc_1 :::"well-founded"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v3_msscyc_1  "non"   ($#v3_msscyc_1 :::"well-founded"::: )   )   ->  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV14_STRUCT_0()   ($#v3_msscyc_1 :::"well-founded"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_msscyc_1 :::"well-founded"::: )    ->   ($#v2_msscyc_1 :::"directed_cycle-less"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV14_STRUCT_0()  ($#~v3_msscyc_1  "non"   ($#v3_msscyc_1 :::"well-founded"::: )   )   for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )  bbbadV14_STRUCT_0()   ($#v2_msscyc_1 :::"directed_cycle-less"::: )    for    ($#l1_graph_1 :::"MultiGraphStruct"::: )  ; 
end; 
theorem :: MSSCYC_1:19 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t"))  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "p"))  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k"))) "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")))))) ; 
 begin  
theorem :: MSSCYC_1:20 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "t")) "being"   ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "X"))  "st" (Bool (Bool (Bool  "not" (Set (Var "t")) "is"   ($#v1_zfmisc_1 :::"root"::: )  ))) "holds"  (Bool  "ex" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Set (Set (Var "t"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )))))) ; 
 
theorem :: MSSCYC_1:21 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "G")) "being"    ($#m1_msafree :::"GeneratorSet"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "B")) "being"   ($#m3_pboole :::"MSSubset":::) "of" (Set (Var "A"))  "st" (Bool (Bool (Set (Var "G"))  ($#r2_pboole :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "B")) "is"    ($#m1_msafree :::"GeneratorSet"::: )   "of" (Set (Var "A"))))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#v3_msafree2 :::"finitely-generated"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   bbbadV2_RELAT_1() (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#v4_relat_1 :::"-defined"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV2_FINSET_1()   ($#v1_partfun1 :::"total"::: )    for    ($#m1_msafree :::"GeneratorSet"::: )   "of" "A"; 
end; 
theorem :: MSSCYC_1:22 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()   ($#m1_msafree :::"GeneratorSet"::: )   "of" (Set (Var "A")) (Bool  "ex" (Set (Var "F")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ) "," (Set (Var "A")) "st" (Bool (Set (Var "F"))  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set   ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X"))) "," (Set (Var "A"))))))) ; 
 
theorem :: MSSCYC_1:23 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()   ($#m1_msafree :::"GeneratorSet"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v4_msafree2 :::"finite-yielding"::: )  ))) "holds"  (Bool  "not" (Bool (Set   ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X"))) "is"   ($#v4_msafree2 :::"finite-yielding"::: )  ))))) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "X" be bbbadV2_RELAT_1() bbbadV2_FINSET_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))); let "v" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); 
cluster (Set   ($#k12_msafree :::"FreeGen"::: )   "(" "v" "," "X" ")" ) ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: MSSCYC_1:24 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k3_funct_2 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set (Var "A")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; attr "IT" is  :::"finitely_operated":::  means :: MSSCYC_1:def 5 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" "IT" "holds"  (Bool  "{"  (Set (Var "o")) where o "is"   ($#m1_subset_1 :::"OperSymbol":::) "of" "IT" : (Bool (Set   ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  "}"   "is"   ($#v1_finset_1 :::"finite"::: )  )); end; 




:: deftheorem    defines :::"finitely_operated"::: MSSCYC_1:def 5 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_msscyc_1 :::"finitely_operated"::: )  ) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "IT")) "holds"  (Bool  "{"  (Set (Var "o")) where o "is"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "IT")) : (Bool (Set   ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))  "}"   "is"   ($#v1_finset_1 :::"finite"::: )  ))  ")" )); 
 
theorem :: MSSCYC_1:25 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v4_msscyc_1 :::"finitely_operated"::: )  )) "holds"  (Bool (Set   ($#k1_msualg_2 :::"Constants"::: )   "(" (Set (Var "A")) "," (Set (Var "v")) ")" ) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: MSSCYC_1:26 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds"  (Bool  "{"  (Set (Var "t")) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ))  ($#k1_funct_1 :::"."::: )  (Set (Var "v"))) : (Bool (Set   ($#k8_msafree2 :::"depth"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  "}"    ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_msafree :::"FreeGen"::: )   "(" (Set (Var "v")) "," (Set (Var "X")) ")"  ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k1_msualg_2 :::"Constants"::: )   "(" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ) "," (Set (Var "v")) ")"  ")" )))))) ; 
 
theorem :: MSSCYC_1:27 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "v")) "," (Set (Var "vk")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  (Bool  "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ))  ($#k1_funct_1 :::"."::: )  (Set (Var "v")))  (Bool  "for" (Set (Var "a")) "being"    ($#m1_msaterm :::"ArgumentSeq"::: )   "of" (Set   ($#k2_msaterm :::"Sym"::: )   "(" (Set (Var "o")) "," (Set (Var "X")) ")" )  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "ak")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ))  ($#k1_funct_1 :::"."::: )  (Set (Var "vk")))  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "a")))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "a")))) & (Bool (Set (Var "ak"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))) "holds"  (Bool (Set   ($#k8_msafree2 :::"depth"::: )  (Set (Var "ak")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k8_msafree2 :::"depth"::: )  (Set (Var "t")))))))))))) ;