:: MSSCYC_2  semantic presentation begin  



definitionlet "S" be    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; func  :::"InducedEdges"::: "S" ->    ($#m1_hidden :::"set"::: )   means :: MSSCYC_2:def 1 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "ex" (Set (Var "op")) "," (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "op")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "op"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S")) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)(Bool  "ex" (Set (Var "args")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#k13_finseq_1 :::"*"::: )  ) "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")  ($#k1_funct_1 :::"."::: )  (Set (Var "op")))  ($#r1_hidden :::"="::: )  (Set (Var "args"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "args")))) & (Bool (Set (Set (Var "args"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )))  ")" ))  ")" )); end; 





:: deftheorem    defines :::"InducedEdges"::: MSSCYC_2:def 1 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "ex" (Set (Var "op")) "," (Set (Var "v")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "op")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "op"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)(Bool  "ex" (Set (Var "args")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k13_finseq_1 :::"*"::: )  ) "st"  (Bool  "("  (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k1_funct_1 :::"."::: )  (Set (Var "op")))  ($#r1_hidden :::"="::: )  (Set (Var "args"))) & (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "args")))) & (Bool (Set (Set (Var "args"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "v")))  ")" )))  ")" ))  ")" ))  ")" ))); 
 
theorem :: MSSCYC_2:1 (Bool  "for" (Set (Var "S")) "being"    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"  (Bool (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ($#k2_zfmisc_1 :::":]"::: ) ))) ; 
 definitionlet "S" be    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; func  :::"InducedSource"::: "S" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  "S" ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") means :: MSSCYC_2:def 2 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  "S"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k2_xtuple_0 :::"`2"::: )  ))); func  :::"InducedTarget"::: "S" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  "S" ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") means :: MSSCYC_2:def 3 (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  "S"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "e"))  ($#k1_xtuple_0 :::"`1"::: )  ")" )))); end; 










:: deftheorem    defines :::"InducedSource"::: MSSCYC_2:def 2 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S")) ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msscyc_2 :::"InducedSource"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "e"))  ($#k2_xtuple_0 :::"`2"::: )  )))  ")" ))); 
 
:: deftheorem    defines :::"InducedTarget"::: MSSCYC_2:def 3 :  (Bool  "for" (Set (Var "S")) "being"    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S")) ")" ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_msscyc_2 :::"InducedTarget"::: )  (Set (Var "S")))) "iff" (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "e"))  ($#k1_xtuple_0 :::"`1"::: )  ")" ))))  ")" ))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; func  :::"InducedGraph"::: "S" ->   ($#l1_graph_1 :::"Graph":::) equals :: MSSCYC_2:def 4 (Set   ($#g1_graph_1 :::"MultiGraphStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") "," (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  "S" ")" ) "," (Set  "("  ($#k2_msscyc_2 :::"InducedSource"::: )  "S" ")" ) "," (Set  "("  ($#k3_msscyc_2 :::"InducedTarget"::: )  "S" ")" ) "#)" ); end; 





:: deftheorem    defines :::"InducedGraph"::: MSSCYC_2:def 4 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"  (Bool (Set   ($#k4_msscyc_2 :::"InducedGraph"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#g1_graph_1 :::"MultiGraphStruct"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k1_msscyc_2 :::"InducedEdges"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k2_msscyc_2 :::"InducedSource"::: )  (Set (Var "S")) ")" ) "," (Set  "("  ($#k3_msscyc_2 :::"InducedTarget"::: )  (Set (Var "S")) ")" ) "#)" ))); 
 
theorem :: MSSCYC_2:2 (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"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool  "ex" (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"))) "st" (Bool (Set   ($#k8_msafree2 :::"depth"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "iff" (Bool  "ex" (Set (Var "c")) "being"   ($#v7_graph_1 :::"directed"::: )     ($#m1_graph_1 :::"Chain"::: )   "of" (Set   ($#k4_msscyc_2 :::"InducedGraph"::: )  (Set (Var "S"))) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (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")))  ")" ))  ")" ))))) ; 
 
theorem :: MSSCYC_2:3 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v11_struct_0 :::"void"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S")) "is"   ($#v5_msafree2 :::"monotonic"::: )  ) "iff" (Bool (Set   ($#k4_msscyc_2 :::"InducedGraph"::: )  (Set (Var "S"))) "is"   ($#v3_msscyc_1 :::"well-founded"::: )  )  ")" )) ; 
 
theorem :: MSSCYC_2:4 (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"::: )    "st" (Bool (Bool (Set (Var "S")) "is"   ($#v5_msafree2 :::"monotonic"::: )  )) "holds"  (Bool (Set   ($#k4_msscyc_2 :::"InducedGraph"::: )  (Set (Var "S"))) "is"   ($#v3_msscyc_1 :::"well-founded"::: )  )) ; 
 
theorem :: MSSCYC_2:5 (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() bbbadV2_FINSET_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v4_msscyc_1 :::"finitely_operated"::: )  )) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (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_xxreal_0 :::"<="::: )  (Set (Var "n")))  "}"   "is"   ($#v1_finset_1 :::"finite"::: )  ))))) ; 
 
theorem :: MSSCYC_2:6 (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"::: )    "st" (Bool (Bool (Set (Var "S")) "is"   ($#v4_msscyc_1 :::"finitely_operated"::: )  ) & (Bool (Set   ($#k4_msscyc_2 :::"InducedGraph"::: )  (Set (Var "S"))) "is"   ($#v3_msscyc_1 :::"well-founded"::: )  )) "holds"  (Bool (Set (Var "S")) "is"   ($#v5_msafree2 :::"monotonic"::: )  )) ;