:: GLIB_000 semantic presentation begin registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode GraphStruct is (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); end; definitionfunc :::"VertexSelector"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 1 (Num 1); func :::"EdgeSelector"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 2 (Num 2); func :::"SourceSelector"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 3 (Num 3); func :::"TargetSelector"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 4 (Num 4); end; :: deftheorem defines :::"VertexSelector"::: GLIB_000:def 1 : (Bool (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); :: deftheorem defines :::"EdgeSelector"::: GLIB_000:def 2 : (Bool (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)); :: deftheorem defines :::"SourceSelector"::: GLIB_000:def 3 : (Bool (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)); :: deftheorem defines :::"TargetSelector"::: GLIB_000:def 4 : (Bool (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)); definitionfunc :::"_GraphSelectors"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 5 (Set ($#k9_domain_1 :::"{"::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) "," (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) "," (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) "," (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#k9_domain_1 :::"}"::: ) ); end; :: deftheorem defines :::"_GraphSelectors"::: GLIB_000:def 5 : (Bool (Set ($#k5_glib_000 :::"_GraphSelectors"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_domain_1 :::"{"::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) "," (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) "," (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) "," (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#k9_domain_1 :::"}"::: ) )); definitionlet "G" be ($#m1_hidden :::"GraphStruct":::); func :::"the_Vertices_of"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: GLIB_000:def 6 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) )); func :::"the_Edges_of"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: GLIB_000:def 7 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_000 :::"EdgeSelector"::: ) )); func :::"the_Source_of"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: GLIB_000:def 8 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_000 :::"SourceSelector"::: ) )); func :::"the_Target_of"::: "G" -> ($#m1_hidden :::"set"::: ) equals :: GLIB_000:def 9 (Set "G" ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_000 :::"TargetSelector"::: ) )); end; :: deftheorem defines :::"the_Vertices_of"::: GLIB_000:def 6 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) )))); :: deftheorem defines :::"the_Edges_of"::: GLIB_000:def 7 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_000 :::"EdgeSelector"::: ) )))); :: deftheorem defines :::"the_Source_of"::: GLIB_000:def 8 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_000 :::"SourceSelector"::: ) )))); :: deftheorem defines :::"the_Target_of"::: GLIB_000:def 9 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_000 :::"TargetSelector"::: ) )))); definitionlet "G" be ($#m1_hidden :::"GraphStruct":::); attr "G" is :::"[Graph-like]"::: means :: GLIB_000:def 10 (Bool "(" (Bool (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "G")) & (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ) & (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) "G") "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" )) & (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) "G") "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" )) ")" ); end; :: deftheorem defines :::"[Graph-like]"::: GLIB_000:def 10 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_000 :::"[Graph-like]"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ) & (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set (Var "G"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) & (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set (Var "G"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode _Graph is ($#v1_glib_000 :::"[Graph-like]"::: ) ($#m1_hidden :::"GraphStruct":::); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); :: original: :::"the_Source_of"::: redefine func :::"the_Source_of"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ); :: original: :::"the_Target_of"::: redefine func :::"the_Target_of"::: "G" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ); end; definitionlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "V")); func :::"createGraph"::: "(" "V" "," "E" "," "S" "," "T" ")" -> ($#m1_hidden :::"_Graph":::) equals :: GLIB_000:def 11 (Set ($#k7_finseq_4 :::"<*"::: ) "V" "," "E" "," "S" "," "T" ($#k7_finseq_4 :::"*>"::: ) ); end; :: deftheorem defines :::"createGraph"::: GLIB_000:def 11 : (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "V")) "holds" (Bool (Set ($#k12_glib_000 :::"createGraph"::: ) "(" (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_finseq_4 :::"<*"::: ) (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ($#k7_finseq_4 :::"*>"::: ) ))))); definitionlet "G" be ($#m1_hidden :::"GraphStruct":::); let "n" be ($#m1_hidden :::"Nat":::); let "x" be ($#m1_hidden :::"set"::: ) ; func "G" :::".set"::: "(" "n" "," "x" ")" -> ($#m1_hidden :::"GraphStruct":::) equals :: GLIB_000:def 12 (Set "G" ($#k1_funct_4 :::"+*"::: ) (Set "(" "n" ($#k16_funcop_1 :::".-->"::: ) "x" ")" )); end; :: deftheorem defines :::".set"::: GLIB_000:def 12 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "n")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x")) ")" )))))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster (Set "G" ($#k5_relat_1 :::"|"::: ) (Set ($#k5_glib_000 :::"_GraphSelectors"::: ) )) -> ($#v1_glib_000 :::"[Graph-like]"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "x", "y", "e" be ($#m1_hidden :::"set"::: ) ; pred "e" :::"Joins"::: "x" "," "y" "," "G" means :: GLIB_000:def 13 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "x") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "y") ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "y") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "x") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Joins"::: GLIB_000:def 13 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "x", "y", "e" be ($#m1_hidden :::"set"::: ) ; pred "e" :::"DJoins"::: "x" "," "y" "," "G" means :: GLIB_000:def 14 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "x") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "y") ")" ); end; :: deftheorem defines :::"DJoins"::: GLIB_000:def 14 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X", "Y", "e" be ($#m1_hidden :::"set"::: ) ; pred "e" :::"SJoins"::: "X" "," "Y" "," "G" means :: GLIB_000:def 15 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "Y") ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "Y") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "X") ")" ) ")" ) ")" ); pred "e" :::"DSJoins"::: "X" "," "Y" "," "G" means :: GLIB_000:def 16 (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r2_hidden :::"in"::: ) "Y") ")" ); end; :: deftheorem defines :::"SJoins"::: GLIB_000:def 15 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool "(" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) "or" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ) ")" ) ")" ))); :: deftheorem defines :::"DSJoins"::: GLIB_000:def 16 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); attr "G" is :::"finite"::: means :: GLIB_000:def 17 (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G") "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ); attr "G" is :::"loopless"::: means :: GLIB_000:def 18 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) "or" "not" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" )); attr "G" is :::"trivial"::: means :: GLIB_000:def 19 (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" )) ($#r1_hidden :::"="::: ) (Num 1)); attr "G" is :::"non-multi"::: means :: GLIB_000:def 20 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," "G") & (Bool (Set (Var "e2")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," "G")) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))); attr "G" is :::"non-Dmulti"::: means :: GLIB_000:def 21 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," "G") & (Bool (Set (Var "e2")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," "G")) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))); end; :: deftheorem defines :::"finite"::: GLIB_000:def 17 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_glib_000 :::"finite"::: ) ) "iff" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" )); :: deftheorem defines :::"loopless"::: GLIB_000:def 18 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_000 :::"loopless"::: ) ) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) "or" "not" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" )) ")" )); :: deftheorem defines :::"trivial"::: GLIB_000:def 19 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v4_glib_000 :::"trivial"::: ) ) "iff" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )); :: deftheorem defines :::"non-multi"::: GLIB_000:def 20 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_glib_000 :::"non-multi"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G"))) & (Bool (Set (Var "e2")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))) ")" )); :: deftheorem defines :::"non-Dmulti"::: GLIB_000:def 21 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) ) "iff" (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G"))) & (Bool (Set (Var "e2")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))) ")" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); attr "G" is :::"simple"::: means :: GLIB_000:def 22 (Bool "(" (Bool "G" "is" ($#v3_glib_000 :::"loopless"::: ) ) & (Bool "G" "is" ($#v5_glib_000 :::"non-multi"::: ) ) ")" ); attr "G" is :::"Dsimple"::: means :: GLIB_000:def 23 (Bool "(" (Bool "G" "is" ($#v3_glib_000 :::"loopless"::: ) ) & (Bool "G" "is" ($#v6_glib_000 :::"non-Dmulti"::: ) ) ")" ); end; :: deftheorem defines :::"simple"::: GLIB_000:def 22 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v7_glib_000 :::"simple"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_000 :::"loopless"::: ) ) & (Bool (Set (Var "G")) "is" ($#v5_glib_000 :::"non-multi"::: ) ) ")" ) ")" )); :: deftheorem defines :::"Dsimple"::: GLIB_000:def 23 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v8_glib_000 :::"Dsimple"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_000 :::"loopless"::: ) ) & (Bool (Set (Var "G")) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) ) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v5_glib_000 :::"non-multi"::: ) -> ($#v6_glib_000 :::"non-Dmulti"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v7_glib_000 :::"simple"::: ) -> ($#v3_glib_000 :::"loopless"::: ) ($#v5_glib_000 :::"non-multi"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#v5_glib_000 :::"non-multi"::: ) -> ($#v7_glib_000 :::"simple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#v6_glib_000 :::"non-Dmulti"::: ) -> ($#v8_glib_000 :::"Dsimple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v8_glib_000 :::"Dsimple"::: ) -> ($#v3_glib_000 :::"loopless"::: ) ($#v6_glib_000 :::"non-Dmulti"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#v4_glib_000 :::"trivial"::: ) -> ($#v2_glib_000 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v6_glib_000 :::"non-Dmulti"::: ) -> ($#v2_glib_000 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v7_glib_000 :::"simple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v7_glib_000 :::"simple"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "G" be ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "V")); cluster (Set ($#k12_glib_000 :::"createGraph"::: ) "(" "V" "," "E" "," "S" "," "T" ")" ) -> ($#v2_glib_000 :::"finite"::: ) ; end; registrationlet "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set (Const "V")); cluster (Set ($#k12_glib_000 :::"createGraph"::: ) "(" "V" "," "E" "," "S" "," "T" ")" ) -> ($#v7_glib_000 :::"simple"::: ) ; end; registrationlet "v", "E" be ($#m1_hidden :::"set"::: ) ; let "S", "T" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "E")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Const "v")) ($#k1_tarski :::"}"::: ) ); cluster (Set ($#k12_glib_000 :::"createGraph"::: ) "(" (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) ) "," "E" "," "S" "," "T" ")" ) -> ($#v4_glib_000 :::"trivial"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".order()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_000:def 24 (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" )); end; :: deftheorem defines :::".order()"::: GLIB_000:def 24 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k14_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); :: original: :::".order()"::: redefine func "G" :::".order()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".size()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_000:def 25 (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )); end; :: deftheorem defines :::".size()"::: GLIB_000:def 25 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k16_glib_000 :::".size()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); :: original: :::".size()"::: redefine func "G" :::".size()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "G" :::".edgesInto"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_000:def 26 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) "X") ")" ) ")" )); func "G" :::".edgesOutOf"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_000:def 27 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) "X") ")" ) ")" )); end; :: deftheorem defines :::".edgesInto"::: GLIB_000:def 26 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) ")" )))); :: deftheorem defines :::".edgesOutOf"::: GLIB_000:def 27 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "G" :::".edgesInOut"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_000:def 28 (Set (Set "(" "G" ($#k18_glib_000 :::".edgesInto"::: ) "X" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" "G" ($#k19_glib_000 :::".edgesOutOf"::: ) "X" ")" )); func "G" :::".edgesBetween"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_000:def 29 (Set (Set "(" "G" ($#k18_glib_000 :::".edgesInto"::: ) "X" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" "G" ($#k19_glib_000 :::".edgesOutOf"::: ) "X" ")" )); end; :: deftheorem defines :::".edgesInOut"::: GLIB_000:def 28 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X")) ")" ))))); :: deftheorem defines :::".edgesBetween"::: GLIB_000:def 29 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X")) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X", "Y" be ($#m1_hidden :::"set"::: ) ; func "G" :::".edgesBetween"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_000:def 30 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) "X" "," "Y" "," "G") ")" )); func "G" :::".edgesDBetween"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) means :: GLIB_000:def 31 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) "X" "," "Y" "," "G") ")" )); end; :: deftheorem defines :::".edgesBetween"::: GLIB_000:def 30 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k22_glib_000 :::".edgesBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G"))) ")" )) ")" )))); :: deftheorem defines :::".edgesDBetween"::: GLIB_000:def 31 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G"))) ")" )) ")" )))); scheme :: GLIB_000:sch 1 FinGraphOrderInd{ P1[ ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::)] } : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool P1[(Set (Var "G"))])) provided (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool P1[(Set (Var "G"))])) and (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "(" "for" (Set (Var "Gk")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "Gk")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool P1[(Set (Var "Gk"))]) ")" )) "holds" (Bool "for" (Set (Var "Gk1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "Gk1")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool P1[(Set (Var "Gk1"))]))) proof end; scheme :: GLIB_000:sch 2 FinGraphSizeInd{ P1[ ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::)] } : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool P1[(Set (Var "G"))])) provided (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "G")) ($#k17_glib_000 :::".size()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool P1[(Set (Var "G"))])) and (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "Gk")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "Gk")) ($#k17_glib_000 :::".size()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool P1[(Set (Var "Gk"))]) ")" )) "holds" (Bool "for" (Set (Var "Gk1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Set (Var "Gk1")) ($#k17_glib_000 :::".size()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool P1[(Set (Var "Gk1"))]))) proof end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"Subgraph"::: "of" "G" -> ($#m1_hidden :::"_Graph":::) means :: GLIB_000:def 32 (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) it) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) it) ($#r1_tarski :::"c="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) it))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) it ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) it ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Subgraph"::: GLIB_000:def 32 : (Bool "for" (Set (Var "G")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "b2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "b2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" ) ")" ) ")" ) ")" )); definitionlet "G1" be ($#m1_hidden :::"_Graph":::); let "G2" be ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G1")); :: original: :::"the_Vertices_of"::: redefine func :::"the_Vertices_of"::: "G2" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G1" ")" ); :: original: :::"the_Edges_of"::: redefine func :::"the_Edges_of"::: "G2" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G1" ")" ); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v7_glib_000 :::"simple"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster -> ($#v2_glib_000 :::"finite"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v3_glib_000 :::"loopless"::: ) ($#m1_hidden :::"_Graph":::); cluster -> ($#v3_glib_000 :::"loopless"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::); cluster -> ($#v4_glib_000 :::"trivial"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v5_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"_Graph":::); cluster -> ($#v5_glib_000 :::"non-multi"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G1" be ($#m1_hidden :::"_Graph":::); let "G2" be ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G1")); attr "G2" is :::"spanning"::: means :: GLIB_000:def 33 (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) "G2") ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G1")); end; :: deftheorem defines :::"spanning"::: GLIB_000:def 33 : (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v9_glib_000 :::"spanning"::: ) ) "iff" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v9_glib_000 :::"spanning"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G1", "G2" be ($#m1_hidden :::"_Graph":::); pred "G1" :::"=="::: "G2" means :: GLIB_000:def 34 (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G1") ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G2")) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G1") ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G2")) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) "G1") ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) "G2")) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) "G1") ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) "G2")) ")" ); reflexivity (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1")))) ")" )) ; symmetry (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G2"))))) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G2"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1")))) ")" )) ; end; :: deftheorem defines :::"=="::: GLIB_000:def 34 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) "iff" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G2")))) ")" ) ")" )); notationlet "G1", "G2" be ($#m1_hidden :::"_Graph":::); antonym "G1" :::"!="::: "G2" for "G1" :::"=="::: "G2"; end; definitionlet "G1", "G2" be ($#m1_hidden :::"_Graph":::); pred "G1" :::"c="::: "G2" means :: GLIB_000:def 35 (Bool "G1" "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" "G2"); reflexivity (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")))) ; end; :: deftheorem defines :::"c="::: GLIB_000:def 35 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r6_glib_000 :::"c="::: ) (Set (Var "G2"))) "iff" (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2"))) ")" )); definitionlet "G1", "G2" be ($#m1_hidden :::"_Graph":::); pred "G1" :::"c<"::: "G2" means :: GLIB_000:def 36 (Bool "(" (Bool "G1" ($#r6_glib_000 :::"c="::: ) "G2") & (Bool "G1" ($#r5_glib_000 :::"!="::: ) "G2") ")" ); irreflexivity (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" "not" (Bool (Set (Var "G1")) ($#r6_glib_000 :::"c="::: ) (Set (Var "G1"))) "or" "not" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"!="::: ) (Set (Var "G1"))) ")" )) ; end; :: deftheorem defines :::"c<"::: GLIB_000:def 36 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r7_glib_000 :::"c<"::: ) (Set (Var "G2"))) "iff" (Bool "(" (Bool (Set (Var "G1")) ($#r6_glib_000 :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r5_glib_000 :::"!="::: ) (Set (Var "G2"))) ")" ) ")" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "V", "E" be ($#m1_hidden :::"set"::: ) ; mode :::"inducedSubgraph"::: "of" "G" "," "V" "," "E" -> ($#m1_glib_000 :::"Subgraph"::: ) "of" "G" means :: GLIB_000:def 37 (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) it) ($#r1_hidden :::"="::: ) "V") & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) it) ($#r1_hidden :::"="::: ) "E") ")" ) if (Bool "(" (Bool "V" "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" )) & (Bool "E" ($#r1_tarski :::"c="::: ) (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V")) ")" ) otherwise (Bool it ($#r5_glib_000 :::"=="::: ) "G"); end; :: deftheorem defines :::"inducedSubgraph"::: GLIB_000:def 37 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "V")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "V"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G")) "," (Set (Var "V")) "," (Set (Var "E"))) "iff" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "V"))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "E"))) ")" ) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "V")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) "or" "not" (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "V")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G")) "," (Set (Var "V")) "," (Set (Var "E"))) "iff" (Bool (Set (Var "b4")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G"))) ")" ) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode inducedSubgraph of "G" "," "V" is ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "V"); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ); let "E" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Const "V")) ")" ); cluster -> ($#v2_glib_000 :::"finite"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," "E"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G"))); let "E" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Const "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ); cluster -> ($#v4_glib_000 :::"trivial"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) ) "," "E"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G"))); cluster -> ($#v2_glib_000 :::"finite"::: ) ($#v4_glib_000 :::"trivial"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "V" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Const "G")) ")" ); cluster -> ($#v7_glib_000 :::"simple"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "V" "," (Set ($#k1_xboole_0 :::"{}"::: ) ); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "E" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Const "G")) ")" ); cluster -> ($#v9_glib_000 :::"spanning"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," "E"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster -> ($#v9_glib_000 :::"spanning"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," (Set ($#k1_xboole_0 :::"{}"::: ) ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_hidden :::"set"::: ) ; mode removeVertex of "G" "," "v" is ($#m2_glib_000 :::"inducedSubgraph":::) "of" "G" "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) ) ")" ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "V" be ($#m1_hidden :::"set"::: ) ; mode removeVertices of "G" "," "V" is ($#m2_glib_000 :::"inducedSubgraph":::) "of" "G" "," (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) "V" ")" ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "e" be ($#m1_hidden :::"set"::: ) ; mode removeEdge of "G" "," "e" is ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "e" ($#k1_tarski :::"}"::: ) )); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "E" be ($#m1_hidden :::"set"::: ) ; mode removeEdges of "G" "," "E" is ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) "E"); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "e" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v9_glib_000 :::"spanning"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "e" ($#k1_tarski :::"}"::: ) )); end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "E" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v9_glib_000 :::"spanning"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "," (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) "E"); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode Vertex of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G"); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "v" :::".edgesIn()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_000:def 38 (Set "G" ($#k18_glib_000 :::".edgesInto"::: ) (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) )); func "v" :::".edgesOut()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_000:def 39 (Set "G" ($#k19_glib_000 :::".edgesOutOf"::: ) (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) )); func "v" :::".edgesInOut()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_000:def 40 (Set "G" ($#k20_glib_000 :::".edgesInOut"::: ) (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::".edgesIn()"::: GLIB_000:def 38 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))); :: deftheorem defines :::".edgesOut()"::: GLIB_000:def 39 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))); :: deftheorem defines :::".edgesInOut()"::: GLIB_000:def 40 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "e" be ($#m1_hidden :::"set"::: ) ; func "v" :::".adj"::: "e" -> ($#m1_subset_1 :::"Vertex":::) "of" "G" equals :: GLIB_000:def 41 (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") if (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "v") ")" ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") if (Bool "(" (Bool "e" ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G")) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "v") & (Bool (Bool "not" (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) "e") ($#r1_hidden :::"="::: ) "v")) ")" ) otherwise "v"; end; :: deftheorem defines :::".adj"::: GLIB_000:def 41 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "implies" (Bool (Set (Set (Var "v")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Bool "not" (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) "implies" (Bool (Set (Set (Var "v")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) "or" "not" (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) & (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) "or" "not" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) "or" (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )) "implies" (Bool (Set (Set (Var "v")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "v" :::".inDegree()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_000:def 42 (Set ($#k1_card_1 :::"card"::: ) (Set "(" "v" ($#k26_glib_000 :::".edgesIn()"::: ) ")" )); func "v" :::".outDegree()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_000:def 43 (Set ($#k1_card_1 :::"card"::: ) (Set "(" "v" ($#k27_glib_000 :::".edgesOut()"::: ) ")" )); end; :: deftheorem defines :::".inDegree()"::: GLIB_000:def 42 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k30_glib_000 :::".inDegree()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ))))); :: deftheorem defines :::".outDegree()"::: GLIB_000:def 43 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k31_glib_000 :::".outDegree()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); :: original: :::".inDegree()"::: redefine func "v" :::".inDegree()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::".outDegree()"::: redefine func "v" :::".outDegree()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "v" :::".degree()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_000:def 44 (Set (Set "(" "v" ($#k30_glib_000 :::".inDegree()"::: ) ")" ) ($#k1_card_2 :::"+`"::: ) (Set "(" "v" ($#k31_glib_000 :::".outDegree()"::: ) ")" )); end; :: deftheorem defines :::".degree()"::: GLIB_000:def 44 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k34_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k30_glib_000 :::".inDegree()"::: ) ")" ) ($#k1_card_2 :::"+`"::: ) (Set "(" (Set (Var "v")) ($#k31_glib_000 :::".outDegree()"::: ) ")" ))))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); :: original: :::".degree()"::: redefine func "v" :::".degree()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_000:def 45 (Set (Set "(" "v" ($#k32_glib_000 :::".inDegree()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" "v" ($#k33_glib_000 :::".outDegree()"::: ) ")" )); end; :: deftheorem defines :::".degree()"::: GLIB_000:def 45 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k32_glib_000 :::".inDegree()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k33_glib_000 :::".outDegree()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "v" :::".inNeighbors()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) equals :: GLIB_000:def 46 (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" "v" ($#k26_glib_000 :::".edgesIn()"::: ) ")" )); func "v" :::".outNeighbors()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) equals :: GLIB_000:def 47 (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) "G" ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" "v" ($#k27_glib_000 :::".edgesOut()"::: ) ")" )); end; :: deftheorem defines :::".inNeighbors()"::: GLIB_000:def 46 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k36_glib_000 :::".inNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ))))); :: deftheorem defines :::".outNeighbors()"::: GLIB_000:def 47 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k37_glib_000 :::".outNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "v" :::".allNeighbors()"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) equals :: GLIB_000:def 48 (Set (Set "(" "v" ($#k36_glib_000 :::".inNeighbors()"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" "v" ($#k37_glib_000 :::".outNeighbors()"::: ) ")" )); end; :: deftheorem defines :::".allNeighbors()"::: GLIB_000:def 48 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k38_glib_000 :::".allNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k36_glib_000 :::".inNeighbors()"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "v")) ($#k37_glib_000 :::".outNeighbors()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); attr "v" is :::"isolated"::: means :: GLIB_000:def 49 (Bool (Set "v" ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"isolated"::: GLIB_000:def 49 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v10_glib_000 :::"isolated"::: ) ) "iff" (Bool (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); redefine attr "v" is :::"isolated"::: means :: GLIB_000:def 50 (Bool (Set "v" ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"isolated"::: GLIB_000:def 50 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v10_glib_000 :::"isolated"::: ) ) "iff" (Bool (Set (Set (Var "v")) ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); attr "v" is :::"endvertex"::: means :: GLIB_000:def 51 (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set "v" ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) & (Bool (Bool "not" (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) "v" "," "v" "," "G")) ")" )); end; :: deftheorem defines :::"endvertex"::: GLIB_000:def 51 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) & (Bool (Bool "not" (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v")) "," (Set (Var "v")) "," (Set (Var "G")))) ")" )) ")" ))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); redefine attr "v" is :::"endvertex"::: means :: GLIB_000:def 52 (Bool (Set "v" ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); end; :: deftheorem defines :::"endvertex"::: GLIB_000:def 52 : (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "v")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) "iff" (Bool (Set (Set (Var "v")) ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" ))); definitionlet "F" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "F" is :::"Graph-yielding"::: means :: GLIB_000:def 53 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_hidden :::"_Graph":::))); attr "F" is :::"halting"::: means :: GLIB_000:def 54 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"Graph-yielding"::: GLIB_000:def 53 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v12_glib_000 :::"Graph-yielding"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#m1_hidden :::"_Graph":::))) ")" )); :: deftheorem defines :::"halting"::: GLIB_000:def 54 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v13_glib_000 :::"halting"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); definitionlet "F" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "F" :::".Lifespan()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_000:def 55 (Bool "(" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" it ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) if (Bool "F" "is" ($#v13_glib_000 :::"halting"::: ) ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::".Lifespan()"::: GLIB_000:def 55 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "F")) "is" ($#v13_glib_000 :::"halting"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k39_glib_000 :::".Lifespan()"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "b2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "F")) "is" ($#v13_glib_000 :::"halting"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k39_glib_000 :::".Lifespan()"::: ) )) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ")" ))); definitionlet "F" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "F" :::".Result()"::: -> ($#m1_hidden :::"set"::: ) equals :: GLIB_000:def 56 (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" "F" ($#k39_glib_000 :::".Lifespan()"::: ) ")" )); end; :: deftheorem defines :::".Result()"::: GLIB_000:def 56 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k40_glib_000 :::".Result()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k39_glib_000 :::".Lifespan()"::: ) ")" )))); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode GraphSeq is ($#v12_glib_000 :::"Graph-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "GSq" be ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "GSq" be ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "GSq" be ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_glib_000 :::"[Graph-like]"::: ) ; end; definitionlet "GSq" be ($#m1_hidden :::"GraphSeq":::); attr "GSq" is :::"finite"::: means :: GLIB_000:def 57 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_glib_000 :::"finite"::: ) )); attr "GSq" is :::"loopless"::: means :: GLIB_000:def 58 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_glib_000 :::"loopless"::: ) )); attr "GSq" is :::"trivial"::: means :: GLIB_000:def 59 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_glib_000 :::"trivial"::: ) )); attr "GSq" is :::"non-trivial"::: means :: GLIB_000:def 60 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Bool "not" (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_glib_000 :::"trivial"::: ) ))); attr "GSq" is :::"non-multi"::: means :: GLIB_000:def 61 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v5_glib_000 :::"non-multi"::: ) )); attr "GSq" is :::"non-Dmulti"::: means :: GLIB_000:def 62 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) )); attr "GSq" is :::"simple"::: means :: GLIB_000:def 63 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_glib_000 :::"simple"::: ) )); attr "GSq" is :::"Dsimple"::: means :: GLIB_000:def 64 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v8_glib_000 :::"Dsimple"::: ) )); end; :: deftheorem defines :::"finite"::: GLIB_000:def 57 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v14_glib_000 :::"finite"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_glib_000 :::"finite"::: ) )) ")" )); :: deftheorem defines :::"loopless"::: GLIB_000:def 58 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v15_glib_000 :::"loopless"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_glib_000 :::"loopless"::: ) )) ")" )); :: deftheorem defines :::"trivial"::: GLIB_000:def 59 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v16_glib_000 :::"trivial"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_glib_000 :::"trivial"::: ) )) ")" )); :: deftheorem defines :::"non-trivial"::: GLIB_000:def 60 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v17_glib_000 :::"non-trivial"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Bool "not" (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_glib_000 :::"trivial"::: ) ))) ")" )); :: deftheorem defines :::"non-multi"::: GLIB_000:def 61 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v18_glib_000 :::"non-multi"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v5_glib_000 :::"non-multi"::: ) )) ")" )); :: deftheorem defines :::"non-Dmulti"::: GLIB_000:def 62 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v19_glib_000 :::"non-Dmulti"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) )) ")" )); :: deftheorem defines :::"simple"::: GLIB_000:def 63 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v20_glib_000 :::"simple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v7_glib_000 :::"simple"::: ) )) ")" )); :: deftheorem defines :::"Dsimple"::: GLIB_000:def 64 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v21_glib_000 :::"Dsimple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v8_glib_000 :::"Dsimple"::: ) )) ")" )); definitionlet "GSq" be ($#m1_hidden :::"GraphSeq":::); redefine attr "GSq" is :::"halting"::: means :: GLIB_000:def 65 (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"halting"::: GLIB_000:def 65 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v13_glib_000 :::"halting"::: ) ) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v14_glib_000 :::"finite"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v16_glib_000 :::"trivial"::: ) ($#v18_glib_000 :::"non-multi"::: ) ($#v19_glib_000 :::"non-Dmulti"::: ) ($#v20_glib_000 :::"simple"::: ) ($#v21_glib_000 :::"Dsimple"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v14_glib_000 :::"finite"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v17_glib_000 :::"non-trivial"::: ) ($#v18_glib_000 :::"non-multi"::: ) ($#v19_glib_000 :::"non-Dmulti"::: ) ($#v20_glib_000 :::"simple"::: ) ($#v21_glib_000 :::"Dsimple"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "GSq" be ($#v14_glib_000 :::"finite"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v2_glib_000 :::"finite"::: ) ; end; registrationlet "GSq" be ($#v15_glib_000 :::"loopless"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v3_glib_000 :::"loopless"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v16_glib_000 :::"trivial"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v4_glib_000 :::"trivial"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v17_glib_000 :::"non-trivial"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v18_glib_000 :::"non-multi"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v5_glib_000 :::"non-multi"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v19_glib_000 :::"non-Dmulti"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v6_glib_000 :::"non-Dmulti"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v20_glib_000 :::"simple"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v7_glib_000 :::"simple"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v21_glib_000 :::"Dsimple"::: ) ($#m1_hidden :::"GraphSeq":::); let "x" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "x") -> ($#v8_glib_000 :::"Dsimple"::: ) for ($#m1_hidden :::"_Graph":::); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v18_glib_000 :::"non-multi"::: ) -> ($#v19_glib_000 :::"non-Dmulti"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v20_glib_000 :::"simple"::: ) -> ($#v15_glib_000 :::"loopless"::: ) ($#v18_glib_000 :::"non-multi"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v18_glib_000 :::"non-multi"::: ) -> ($#v20_glib_000 :::"simple"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v19_glib_000 :::"non-Dmulti"::: ) -> ($#v21_glib_000 :::"Dsimple"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v21_glib_000 :::"Dsimple"::: ) -> ($#v15_glib_000 :::"loopless"::: ) ($#v19_glib_000 :::"non-Dmulti"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v16_glib_000 :::"trivial"::: ) -> ($#v14_glib_000 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v16_glib_000 :::"trivial"::: ) ($#v19_glib_000 :::"non-Dmulti"::: ) -> ($#v14_glib_000 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin theorem :: GLIB_000:1 (Bool "(" (Bool (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) ; theorem :: GLIB_000:2 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k5_glib_000 :::"_GraphSelectors"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "G"))))) ; theorem :: GLIB_000:3 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "GS"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "GS")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_glib_000 :::"VertexSelector"::: ) ))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "GS"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "GS")) ($#k1_funct_1 :::"."::: ) (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ))) & (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set (Var "GS"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "GS")) ($#k1_funct_1 :::"."::: ) (Set ($#k3_glib_000 :::"SourceSelector"::: ) ))) & (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set (Var "GS"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "GS")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_glib_000 :::"TargetSelector"::: ) ))) ")" )) ; theorem :: GLIB_000:4 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) ")" )) ; theorem :: GLIB_000:5 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) "holds" (Bool "(" (Bool (Set (Var "GS")) "is" ($#v1_glib_000 :::"[Graph-like]"::: ) ) "iff" (Bool "(" (Bool (Set ($#k5_glib_000 :::"_GraphSelectors"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "GS")))) & (Bool (Bool "not" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "GS"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set (Var "GS"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "GS")) ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "GS")) ")" )) & (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set (Var "GS"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "GS")) ")" ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "GS")) ")" )) ")" ) ")" )) ; theorem :: GLIB_000:6 (Bool "for" (Set (Var "V")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "E")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set "(" ($#k12_glib_000 :::"createGraph"::: ) "(" (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "V"))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set "(" ($#k12_glib_000 :::"createGraph"::: ) "(" (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "E"))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set "(" ($#k12_glib_000 :::"createGraph"::: ) "(" (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set (Var "S"))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set "(" ($#k12_glib_000 :::"createGraph"::: ) "(" (Set (Var "V")) "," (Set (Var "E")) "," (Set (Var "S")) "," (Set (Var "T")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set (Var "T"))) ")" )))) ; theorem :: GLIB_000:7 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "GS")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: GLIB_000:8 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; theorem :: GLIB_000:9 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r1_hidden :::"<>"::: ) (Set (Var "n2")))) "holds" (Bool (Set (Set (Var "GS")) ($#k1_funct_1 :::"."::: ) (Set (Var "n2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n1")) "," (Set (Var "x")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n2"))))))) ; theorem :: GLIB_000:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Bool "not" (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k5_glib_000 :::"_GraphSelectors"::: ) )))) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" ))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" ))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" ))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set "(" (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ")" ))) & (Bool (Set (Set (Var "G")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n")) "," (Set (Var "x")) ")" ) "is" ($#m1_hidden :::"_Graph":::)) ")" )))) ; theorem :: GLIB_000:11 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k1_glib_000 :::"VertexSelector"::: ) ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k2_glib_000 :::"EdgeSelector"::: ) ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k8_glib_000 :::"the_Source_of"::: ) (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k3_glib_000 :::"SourceSelector"::: ) ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k9_glib_000 :::"the_Target_of"::: ) (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set ($#k4_glib_000 :::"TargetSelector"::: ) ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: GLIB_000:12 (Bool "for" (Set (Var "GS")) "being" ($#m1_hidden :::"GraphStruct":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n1")) ($#r1_hidden :::"<>"::: ) (Set (Var "n2")))) "holds" (Bool "(" (Bool (Set (Var "n1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n1")) "," (Set (Var "x")) ")" ")" ) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n2")) "," (Set (Var "y")) ")" ")" ))) & (Bool (Set (Var "n2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n1")) "," (Set (Var "x")) ")" ")" ) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n2")) "," (Set (Var "y")) ")" ")" ))) & (Bool (Set (Set "(" (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n1")) "," (Set (Var "x")) ")" ")" ) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n2")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n1"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "GS")) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n1")) "," (Set (Var "x")) ")" ")" ) ($#k13_glib_000 :::".set"::: ) "(" (Set (Var "n2")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n2"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )))) ; theorem :: GLIB_000:13 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) ")" ))) ; theorem :: GLIB_000:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "G"))))) ; theorem :: GLIB_000:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "G"))) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x2")) "," (Set (Var "y2")) "," (Set (Var "G"))) & (Bool "not" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" ))) ; theorem :: GLIB_000:16 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "or" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "y")) "," (Set (Var "x")) "," (Set (Var "G"))) ")" ) ")" ))) ; theorem :: GLIB_000:17 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) & (Bool "(" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) "holds" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G"))))) ; theorem :: GLIB_000:18 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_000 :::"loopless"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v")) "," (Set (Var "v")) "," (Set (Var "G"))))) ")" )) ; theorem :: GLIB_000:19 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ")" ))))) ; theorem :: GLIB_000:20 (Bool "for" (Set (Var "G")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: GLIB_000:21 (Bool "for" (Set (Var "G")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))))) ; theorem :: GLIB_000:22 (Bool "for" (Set (Var "G")) "being" ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::) (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GLIB_000:23 (Bool "for" (Set (Var "G")) "being" ($#v3_glib_000 :::"loopless"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: GLIB_000:24 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "G")) "is" ($#v7_glib_000 :::"simple"::: ) )) ; theorem :: GLIB_000:25 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ; theorem :: GLIB_000:26 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool (Set (Var "G")) "is" ($#v4_glib_000 :::"trivial"::: ) ) ")" )) ; theorem :: GLIB_000:27 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) ")" )) ; theorem :: GLIB_000:28 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "or" (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ) "iff" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))) ")" ))) ; theorem :: GLIB_000:29 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))) ")" ))) ; theorem :: GLIB_000:30 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )))) ; theorem :: GLIB_000:31 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) "iff" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X")))) ")" ))) ; theorem :: GLIB_000:32 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X")))))) ; theorem :: GLIB_000:33 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))))) ; theorem :: GLIB_000:34 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )))) ; theorem :: GLIB_000:35 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")) ")" ))))) ; theorem :: GLIB_000:36 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "Y")))))) ; theorem :: GLIB_000:37 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "G")) ($#k22_glib_000 :::".edgesBetween"::: ) "(" (Set (Var "X1")) "," (Set (Var "Y1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k22_glib_000 :::".edgesBetween"::: ) "(" (Set (Var "X2")) "," (Set (Var "Y2")) ")" )))) ; theorem :: GLIB_000:38 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X1")) "," (Set (Var "Y1")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X2")) "," (Set (Var "Y2")) ")" )))) ; theorem :: GLIB_000:39 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "," (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) & (Bool (Set (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" )) ")" ))) ; theorem :: GLIB_000:40 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Var "G")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")))) ; theorem :: GLIB_000:41 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2"))) & (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1"))) "iff" (Bool "(" (Bool (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G2")))) ")" ) ")" )) ; theorem :: GLIB_000:42 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")))) ")" ")" )))) ; theorem :: GLIB_000:43 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "G3")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2")) "holds" (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")))))) ; theorem :: GLIB_000:44 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2"))))) ; theorem :: GLIB_000:45 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G1")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) & (Bool (Set ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G1")) ")" ) ($#k5_relset_1 :::"|"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) ")" ))) ; theorem :: GLIB_000:46 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "E1")) "," (Set (Var "E2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G")) "," (Set (Var "V1")) "," (Set (Var "E1")) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G")) "," (Set (Var "V2")) "," (Set (Var "E2")) "st" (Bool (Bool (Set (Var "V2")) ($#r1_tarski :::"c="::: ) (Set (Var "V1"))) & (Bool (Set (Var "E2")) ($#r1_tarski :::"c="::: ) (Set (Var "E1"))) & (Bool (Set (Var "V2")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )) & (Bool (Set (Var "E2")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "V2"))))) "holds" (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1"))))))) ; theorem :: GLIB_000:47 (Bool "for" (Set (Var "G1")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G1")) "," (Set (Var "v")) "holds" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ))) ")" )))) ; theorem :: GLIB_000:48 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G1")) "," (Set (Var "v")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "G2")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k15_glib_000 :::".order()"::: ) )) & (Bool (Set (Set "(" (Set (Var "G2")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k17_glib_000 :::".size()"::: ) )) ")" )))) ; theorem :: GLIB_000:49 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertices":::) "of" (Set (Var "G1")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "V")) ")" ))) ")" )))) ; theorem :: GLIB_000:50 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertices":::) "of" (Set (Var "G1")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "G2")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k15_glib_000 :::".order()"::: ) )) & (Bool (Set (Set "(" (Set (Var "G2")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "G1")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "V")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k17_glib_000 :::".size()"::: ) )) ")" )))) ; theorem :: GLIB_000:51 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeEdge":::) "of" (Set (Var "G1")) "," (Set (Var "e")) "holds" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; theorem :: GLIB_000:52 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeEdge":::) "of" (Set (Var "G1")) "," (Set (Var "e")) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k15_glib_000 :::".order()"::: ) )) & "(" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))))) "implies" (Bool (Set (Set "(" (Set (Var "G2")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k17_glib_000 :::".size()"::: ) )) ")" ")" )))) ; theorem :: GLIB_000:53 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeEdges":::) "of" (Set (Var "G1")) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "E")))) ")" )))) ; theorem :: GLIB_000:54 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeEdges":::) "of" (Set (Var "G1")) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "G1")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k15_glib_000 :::".order()"::: ) ))))) ; theorem :: GLIB_000:55 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1")) ")" ) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeEdges":::) "of" (Set (Var "G1")) "," (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "G2")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k17_glib_000 :::".size()"::: ) ))))) ; theorem :: GLIB_000:56 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) )) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) ")" )))) ; theorem :: GLIB_000:57 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "v")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:58 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) )) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) ")" )))) ; theorem :: GLIB_000:59 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) )) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v")) "," (Set (Var "x")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:60 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "v")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ))))) ; theorem :: GLIB_000:61 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) "iff" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")))) & (Bool "(" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) "or" (Bool (Set (Set "(" ($#k11_glib_000 :::"the_Target_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) ")" ) ")" )))) ; theorem :: GLIB_000:62 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v1")) ($#k28_glib_000 :::".edgesInOut()"::: ) ))))) ; theorem :: GLIB_000:63 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G"))) "or" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v1")) ($#k26_glib_000 :::".edgesIn()"::: ) )) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v2")) ($#k27_glib_000 :::".edgesOut()"::: ) )) ")" ) "or" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v2")) ($#k26_glib_000 :::".edgesIn()"::: ) )) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v1")) ($#k27_glib_000 :::".edgesOut()"::: ) )) ")" ) ")" )))) ; theorem :: GLIB_000:64 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v1")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) "iff" (Bool "ex" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:65 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: GLIB_000:66 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Set (Var "v1")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Set (Var "v2")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) ")" )))) ; theorem :: GLIB_000:67 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) "iff" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v")) "," (Set (Set (Var "v")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) "," (Set (Var "G"))) ")" )))) ; theorem :: GLIB_000:68 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v1")) ($#k35_glib_000 :::".degree()"::: ) )) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v2")) ($#k35_glib_000 :::".degree()"::: ) )) ")" )))) ; theorem :: GLIB_000:69 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k36_glib_000 :::".inNeighbors()"::: ) )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "v")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:70 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k37_glib_000 :::".outNeighbors()"::: ) )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "v")) "," (Set (Var "x")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:71 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k38_glib_000 :::".allNeighbors()"::: ) )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v")) "," (Set (Var "x")) "," (Set (Var "G")))) ")" )))) ; theorem :: GLIB_000:72 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2")))) "implies" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2")))) "implies" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2")))) "implies" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2")))) "implies" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1"))) ")" ")" )))) ; theorem :: GLIB_000:73 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" ")" )))) ; theorem :: GLIB_000:74 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#v9_glib_000 :::"spanning"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "G3")) "being" ($#v9_glib_000 :::"spanning"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2")) "holds" (Bool (Set (Var "G3")) "is" ($#v9_glib_000 :::"spanning"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")))))) ; theorem :: GLIB_000:75 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set (Set (Var "G2")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G1")) ($#k15_glib_000 :::".order()"::: ) )) & (Bool (Set (Set (Var "G2")) ($#k17_glib_000 :::".size()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G1")) ($#k17_glib_000 :::".size()"::: ) )) ")" ))) ; theorem :: GLIB_000:76 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "G2")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G2")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G2")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G2")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X")))) ")" )))) ; theorem :: GLIB_000:77 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "G2")) ($#k22_glib_000 :::".edgesBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k22_glib_000 :::".edgesBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Set (Var "G2")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) ")" )))) ; theorem :: GLIB_000:78 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set (Set (Var "v2")) ($#k26_glib_000 :::".edgesIn()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k26_glib_000 :::".edgesIn()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k27_glib_000 :::".edgesOut()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k27_glib_000 :::".edgesOut()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) ")" ))))) ; theorem :: GLIB_000:79 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set (Set (Var "v2")) ($#k26_glib_000 :::".edgesIn()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k26_glib_000 :::".edgesIn()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) & (Bool (Set (Set (Var "v2")) ($#k27_glib_000 :::".edgesOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k27_glib_000 :::".edgesOut()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) & (Bool (Set (Set (Var "v2")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k28_glib_000 :::".edgesInOut()"::: ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")) ")" ))) ")" ))))) ; theorem :: GLIB_000:80 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "v1")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))))))))) ; theorem :: GLIB_000:81 (Bool "for" (Set (Var "G1")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set (Set (Var "v2")) ($#k32_glib_000 :::".inDegree()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v1")) ($#k32_glib_000 :::".inDegree()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k33_glib_000 :::".outDegree()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v1")) ($#k33_glib_000 :::".outDegree()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k35_glib_000 :::".degree()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "v1")) ($#k35_glib_000 :::".degree()"::: ) )) ")" ))))) ; theorem :: GLIB_000:82 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool "(" (Bool (Set (Set (Var "v2")) ($#k36_glib_000 :::".inNeighbors()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k36_glib_000 :::".inNeighbors()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k37_glib_000 :::".outNeighbors()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k37_glib_000 :::".outNeighbors()"::: ) )) & (Bool (Set (Set (Var "v2")) ($#k38_glib_000 :::".allNeighbors()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "v1")) ($#k38_glib_000 :::".allNeighbors()"::: ) )) ")" ))))) ; theorem :: GLIB_000:83 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) "is" ($#v10_glib_000 :::"isolated"::: ) )) "holds" (Bool (Set (Var "v2")) "is" ($#v10_glib_000 :::"isolated"::: ) ))))) ; theorem :: GLIB_000:84 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) & (Bool (Bool "not" (Set (Var "v2")) "is" ($#v11_glib_000 :::"endvertex"::: ) ))) "holds" (Bool (Set (Var "v2")) "is" ($#v10_glib_000 :::"isolated"::: ) ))))) ; theorem :: GLIB_000:85 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G3")))) "holds" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G3")))) ; theorem :: GLIB_000:86 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))))) ; theorem :: GLIB_000:87 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) "iff" (Bool "(" (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2"))) & (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1"))) ")" ) ")" )) ; theorem :: GLIB_000:88 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r3_glib_000 :::"SJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G2"))) ")" & "(" (Bool (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G1")))) "implies" (Bool (Set (Var "e")) ($#r4_glib_000 :::"DSJoins"::: ) (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "G2"))) ")" ")" ))) ; theorem :: GLIB_000:89 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "G1")) "is" ($#v2_glib_000 :::"finite"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v2_glib_000 :::"finite"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v3_glib_000 :::"loopless"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v3_glib_000 :::"loopless"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v4_glib_000 :::"trivial"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v4_glib_000 :::"trivial"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v5_glib_000 :::"non-multi"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v5_glib_000 :::"non-multi"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v6_glib_000 :::"non-Dmulti"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v7_glib_000 :::"simple"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v7_glib_000 :::"simple"::: ) ) ")" & "(" (Bool (Bool (Set (Var "G1")) "is" ($#v8_glib_000 :::"Dsimple"::: ) )) "implies" (Bool (Set (Var "G2")) "is" ($#v8_glib_000 :::"Dsimple"::: ) ) ")" ")" )) ; theorem :: GLIB_000:90 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k14_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k14_glib_000 :::".order()"::: ) )) & (Bool (Set (Set (Var "G1")) ($#k16_glib_000 :::".size()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k16_glib_000 :::".size()"::: ) )) & (Bool (Set (Set (Var "G1")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k18_glib_000 :::".edgesInto"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G1")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k19_glib_000 :::".edgesOutOf"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G1")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G1")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "G1")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k23_glib_000 :::".edgesDBetween"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) ")" ))) ; theorem :: GLIB_000:91 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")))) "holds" (Bool (Set (Var "G3")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G2")))) ; theorem :: GLIB_000:92 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G3")))) "holds" (Bool (Set (Var "G2")) "is" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G3")))) ; theorem :: GLIB_000:93 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G")) "," (Set (Var "V")) "," (Set (Var "E")) "holds" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))))) ; theorem :: GLIB_000:94 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"inducedSubgraph":::) "of" (Set (Var "G1")) "," (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1")) ")" ) "holds" (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))))) ; theorem :: GLIB_000:95 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "V")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G3")) "being" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G1")) "," (Set (Var "V")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool (Set (Var "G3")) "is" ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" (Set (Var "G2")) "," (Set (Var "V")) "," (Set (Var "E")))))) ; theorem :: GLIB_000:96 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool "(" (Bool (Set (Set (Var "v1")) ($#k26_glib_000 :::".edgesIn()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k26_glib_000 :::".edgesIn()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k27_glib_000 :::".edgesOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k27_glib_000 :::".edgesOut()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k28_glib_000 :::".edgesInOut()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e")))) & (Bool (Set (Set (Var "v1")) ($#k30_glib_000 :::".inDegree()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k30_glib_000 :::".inDegree()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k31_glib_000 :::".outDegree()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k31_glib_000 :::".outDegree()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k34_glib_000 :::".degree()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k34_glib_000 :::".degree()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k36_glib_000 :::".inNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k36_glib_000 :::".inNeighbors()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k37_glib_000 :::".outNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k37_glib_000 :::".outNeighbors()"::: ) )) & (Bool (Set (Set (Var "v1")) ($#k38_glib_000 :::".allNeighbors()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k38_glib_000 :::".allNeighbors()"::: ) )) ")" ))))) ; theorem :: GLIB_000:97 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v1")) "is" ($#v10_glib_000 :::"isolated"::: ) )) "implies" (Bool (Set (Var "v2")) "is" ($#v10_glib_000 :::"isolated"::: ) ) ")" & "(" (Bool (Bool (Set (Var "v1")) "is" ($#v11_glib_000 :::"endvertex"::: ) )) "implies" (Bool (Set (Var "v2")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) ")" ")" )))) ; theorem :: GLIB_000:98 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "not" (Bool (Set (Var "G1")) ($#r7_glib_000 :::"c<"::: ) (Set (Var "G2"))) "or" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) "or" (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")))) ")" ))) ; theorem :: GLIB_000:99 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "not" (Bool (Set (Var "G1")) ($#r7_glib_000 :::"c<"::: ) (Set (Var "G2"))) "or" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G1"))))) ")" )) "or" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2")))) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G1"))))) ")" )) ")" ))) ;