:: GLIB_002 semantic presentation begin definitionlet "G" be ($#m1_hidden :::"_Graph":::); attr "G" is :::"connected"::: means :: GLIB_002:def 1 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" "G" "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "u")) "," (Set (Var "v"))))); end; :: deftheorem defines :::"connected"::: GLIB_002:def 1 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "u")) "," (Set (Var "v"))))) ")" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); attr "G" is :::"acyclic"::: means :: GLIB_002:def 2 (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" "G" "holds" (Bool (Bool "not" (Set (Var "W")) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ))); end; :: deftheorem defines :::"acyclic"::: GLIB_002:def 2 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_glib_002 :::"acyclic"::: ) ) "iff" (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "W")) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ))) ")" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); attr "G" is :::"Tree-like"::: means :: GLIB_002:def 3 (Bool "(" (Bool "G" "is" ($#v2_glib_002 :::"acyclic"::: ) ) & (Bool "G" "is" ($#v1_glib_002 :::"connected"::: ) ) ")" ); end; :: deftheorem defines :::"Tree-like"::: GLIB_002:def 3 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_002 :::"Tree-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_glib_002 :::"acyclic"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) ")" ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v4_glib_000 :::"trivial"::: ) -> ($#v1_glib_002 :::"connected"::: ) 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_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v3_glib_000 :::"loopless"::: ) ($#v4_glib_000 :::"trivial"::: ) -> ($#v3_glib_002 :::"Tree-like"::: ) 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_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_002 :::"acyclic"::: ) -> ($#v7_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_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v3_glib_002 :::"Tree-like"::: ) -> ($#v1_glib_002 :::"connected"::: ) ($#v2_glib_002 :::"acyclic"::: ) 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_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v1_glib_002 :::"connected"::: ) ($#v2_glib_002 :::"acyclic"::: ) -> ($#v3_glib_002 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); cluster -> ($#v3_glib_002 :::"Tree-like"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set ($#k6_domain_1 :::"{"::: ) "v" ($#k6_domain_1 :::"}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_hidden :::"set"::: ) ; pred "G" :::"is_DTree_rooted_at"::: "v" means :: GLIB_002:def 4 (Bool "(" (Bool "G" "is" ($#v3_glib_002 :::"Tree-like"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" "G" "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) "v" "," (Set (Var "x")))) ")" ) ")" ); end; :: deftheorem defines :::"is_DTree_rooted_at"::: GLIB_002:def 4 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_glib_002 :::"is_DTree_rooted_at"::: ) (Set (Var "v"))) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_002 :::"Tree-like"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "x")))) ")" ) ")" ) ")" ))); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v3_glib_002 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v3_glib_002 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; 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"::: ) bbbadV1_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v2_glib_000 :::"finite"::: ) ($#v4_glib_000 :::"trivial"::: ) ($#v3_glib_002 :::"Tree-like"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"_Graph":::); cluster -> ($#v2_glib_002 :::"acyclic"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "G" :::".reachableFrom"::: "v" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) means :: GLIB_002:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" "G" "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) "v" "," (Set (Var "x")))) ")" )); end; :: deftheorem defines :::".reachableFrom"::: GLIB_002:def 5 : (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 "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "x")))) ")" )) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "G" :::".reachableDFrom"::: "v" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) means :: GLIB_002:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" "G" "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) "v" "," (Set (Var "x")))) ")" )); end; :: deftheorem defines :::".reachableDFrom"::: GLIB_002:def 6 : (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 "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "x")))) ")" )) ")" )))); definitionlet "G1" be ($#m1_hidden :::"_Graph":::); let "G2" be ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Const "G1")); attr "G2" is :::"Component-like"::: means :: GLIB_002:def 7 (Bool "(" (Bool "G2" "is" ($#v1_glib_002 :::"connected"::: ) ) & (Bool "(" "for" (Set (Var "G3")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G1" "holds" (Bool (Bool "not" "G2" ($#r7_glib_000 :::"c<"::: ) (Set (Var "G3")))) ")" ) ")" ); end; :: deftheorem defines :::"Component-like"::: GLIB_002:def 7 : (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" ($#v4_glib_002 :::"Component-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) ) & (Bool "(" "for" (Set (Var "G3")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) "holds" (Bool (Bool "not" (Set (Var "G2")) ($#r7_glib_000 :::"c<"::: ) (Set (Var "G3")))) ")" ) ")" ) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v4_glib_002 :::"Component-like"::: ) -> ($#v1_glib_002 :::"connected"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); cluster -> ($#v4_glib_002 :::"Component-like"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set "G" ($#k1_glib_002 :::".reachableFrom"::: ) "v") "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" "G" ($#k1_glib_002 :::".reachableFrom"::: ) "v" ")" )); 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"::: ) bbbadV1_FINSET_1() ($#v1_glib_000 :::"[Graph-like]"::: ) ($#v4_glib_002 :::"Component-like"::: ) for ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode Component of "G" is ($#v4_glib_002 :::"Component-like"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".componentSet()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) means :: GLIB_002:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set "G" ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v"))))) ")" )); end; :: deftheorem defines :::".componentSet()"::: GLIB_002:def 8 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_glib_002 :::".componentSet()"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v"))))) ")" )) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Const "G")) ($#k3_glib_002 :::".componentSet()"::: ) ); cluster -> ($#v4_glib_002 :::"Component-like"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," "X" "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) "X"); end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".numComponents()"::: -> ($#m1_hidden :::"Cardinal":::) equals :: GLIB_002:def 9 (Set ($#k1_card_1 :::"card"::: ) (Set "(" "G" ($#k3_glib_002 :::".componentSet()"::: ) ")" )); end; :: deftheorem defines :::".numComponents()"::: GLIB_002:def 9 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" (Set (Var "G")) ($#k3_glib_002 :::".componentSet()"::: ) ")" )))); definitionlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); :: original: :::".numComponents()"::: redefine func "G" :::".numComponents()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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")); attr "v" is :::"cut-vertex"::: means :: GLIB_002:def 10 (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" "G" "," "v" "holds" (Bool (Set "G" ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G2")) ($#k4_glib_002 :::".numComponents()"::: ) ))); end; :: deftheorem defines :::"cut-vertex"::: GLIB_002:def 10 : (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" ($#v5_glib_002 :::"cut-vertex"::: ) ) "iff" (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G")) "," (Set (Var "v")) "holds" (Bool (Set (Set (Var "G")) ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G2")) ($#k4_glib_002 :::".numComponents()"::: ) ))) ")" ))); 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 :::"cut-vertex"::: means :: GLIB_002:def 11 (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" "G" "," "v" "holds" (Bool (Set "G" ($#k5_glib_002 :::".numComponents()"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G2")) ($#k5_glib_002 :::".numComponents()"::: ) ))); end; :: deftheorem defines :::"cut-vertex"::: GLIB_002:def 11 : (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" ($#v5_glib_002 :::"cut-vertex"::: ) ) "iff" (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G")) "," (Set (Var "v")) "holds" (Bool (Set (Set (Var "G")) ($#k5_glib_002 :::".numComponents()"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "G2")) ($#k5_glib_002 :::".numComponents()"::: ) ))) ")" ))); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::); cluster ($#~v5_glib_002 "non" ($#v5_glib_002 :::"cut-vertex"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G"); end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_hidden :::"_Graph":::); cluster ($#v11_glib_000 :::"endvertex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G"); end; registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_hidden :::"_Graph":::); let "v" be ($#v11_glib_000 :::"endvertex"::: ) ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); cluster -> ($#v3_glib_002 :::"Tree-like"::: ) for ($#m2_glib_000 :::"inducedSubgraph"::: ) "of" "G" "," (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) )) "," (Set "G" ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) "v" ($#k1_tarski :::"}"::: ) ) ")" )); end; definitionlet "GSq" be ($#m1_hidden :::"GraphSeq":::); attr "GSq" is :::"connected"::: means :: GLIB_002:def 12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_glib_002 :::"connected"::: ) )); attr "GSq" is :::"acyclic"::: means :: GLIB_002:def 13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v2_glib_002 :::"acyclic"::: ) )); attr "GSq" is :::"Tree-like"::: means :: GLIB_002:def 14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "GSq" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v3_glib_002 :::"Tree-like"::: ) )); end; :: deftheorem defines :::"connected"::: GLIB_002:def 12 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v6_glib_002 :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v1_glib_002 :::"connected"::: ) )) ")" )); :: deftheorem defines :::"acyclic"::: GLIB_002:def 13 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v7_glib_002 :::"acyclic"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v2_glib_002 :::"acyclic"::: ) )) ")" )); :: deftheorem defines :::"Tree-like"::: GLIB_002:def 14 : (Bool "for" (Set (Var "GSq")) "being" ($#m1_hidden :::"GraphSeq":::) "holds" (Bool "(" (Bool (Set (Var "GSq")) "is" ($#v8_glib_002 :::"Tree-like"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "GSq")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "is" ($#v3_glib_002 :::"Tree-like"::: ) )) ")" )); 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"::: ) -> ($#v6_glib_002 :::"connected"::: ) 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"::: ) ($#v15_glib_000 :::"loopless"::: ) ($#v16_glib_000 :::"trivial"::: ) -> ($#v8_glib_002 :::"Tree-like"::: ) 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"::: ) ($#v7_glib_002 :::"acyclic"::: ) -> ($#v20_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"::: ) bbbadV1_PARTFUN1((Set ($#k5_numbers :::"NAT"::: ) )) ($#v12_glib_000 :::"Graph-yielding"::: ) ($#v8_glib_002 :::"Tree-like"::: ) -> ($#v6_glib_002 :::"connected"::: ) ($#v7_glib_002 :::"acyclic"::: ) 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"::: ) ($#v6_glib_002 :::"connected"::: ) ($#v7_glib_002 :::"acyclic"::: ) -> ($#v8_glib_002 :::"Tree-like"::: ) 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"::: ) ($#v13_glib_000 :::"halting"::: ) ($#v14_glib_000 :::"finite"::: ) ($#v8_glib_002 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "GSq" be ($#v6_glib_002 :::"connected"::: ) ($#m1_hidden :::"GraphSeq":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "n") -> ($#v1_glib_002 :::"connected"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v7_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"GraphSeq":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "n") -> ($#v2_glib_002 :::"acyclic"::: ) for ($#m1_hidden :::"_Graph":::); end; registrationlet "GSq" be ($#v8_glib_002 :::"Tree-like"::: ) ($#m1_hidden :::"GraphSeq":::); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "GSq" ($#k1_funct_1 :::"."::: ) "n") -> ($#v3_glib_002 :::"Tree-like"::: ) for ($#m1_hidden :::"_Graph":::); end; begin theorem :: GLIB_002:1 canceled; theorem :: GLIB_002:2 (Bool "for" (Set (Var "G")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "v")) "is" ($#v10_glib_000 :::"isolated"::: ) )))) ; theorem :: GLIB_002:3 (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")) "st" (Bool (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) ) & (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "v")) ($#k28_glib_000 :::".edgesInOut()"::: ) )) & (Bool (Bool "not" (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v")) "," (Set (Var "v")) "," (Set (Var "G1")))) ")" ))) "holds" (Bool (Set (Var "G1")) "is" ($#v1_glib_002 :::"connected"::: ) )))) ; theorem :: GLIB_002:4 (Bool "for" (Set (Var "G1")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v1_glib_002 :::"connected"::: ) ($#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")) "st" (Bool (Bool (Set (Var "v")) "is" ($#v11_glib_000 :::"endvertex"::: ) )) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) )))) ; theorem :: GLIB_002:5 (Bool "for" (Set (Var "G1")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (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")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ))) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) ))))) ; theorem :: GLIB_002:6 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool "ex" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v1")) "," (Set (Var "v2"))))))) "holds" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) )) ; theorem :: GLIB_002:7 (Bool "for" (Set (Var "G")) "being" ($#v4_glib_000 :::"trivial"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) )) ; theorem :: GLIB_002:8 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) "is" ($#v1_glib_002 :::"connected"::: ) )) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) )) ; theorem :: GLIB_002:9 (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 (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")))))) ; theorem :: GLIB_002:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1")))) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1"))))))) ; theorem :: GLIB_002:11 (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 "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k20_glib_000 :::".edgesInOut"::: ) (Set "(" (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")) ")" ))))) ; theorem :: GLIB_002:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v2"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v2")))))) ; theorem :: GLIB_002:13 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) "holds" (Bool (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v"))))))) ; theorem :: GLIB_002:14 (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 (Set (Set (Var "G2")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1")))))))) ; theorem :: GLIB_002:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))))) "holds" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) )) ; theorem :: GLIB_002:16 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) )) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))))) ; theorem :: GLIB_002:17 (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 "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v2"))))))) ; theorem :: GLIB_002:18 (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 (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v")))))) ; theorem :: GLIB_002:19 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v1")))) & (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v1"))))))) ; theorem :: GLIB_002:20 (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 "G")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")))))) ; theorem :: GLIB_002:21 (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 (Set (Set (Var "G2")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G1")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v1")))))))) ; theorem :: GLIB_002:22 (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 "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k2_glib_002 :::".reachableDFrom"::: ) (Set (Var "v2"))))))) ; theorem :: GLIB_002:23 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "G2")) "is" ($#v9_glib_000 :::"spanning"::: ) )) "holds" (Bool (Set (Var "G1")) "is" ($#v1_glib_002 :::"connected"::: ) ))) ; theorem :: GLIB_002:24 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "G")) ($#k3_glib_002 :::".componentSet()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))) ; theorem :: GLIB_002:25 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) "iff" (Bool (Set (Set (Var "G")) ($#k3_glib_002 :::".componentSet()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k1_tarski :::"}"::: ) )) ")" )) ; theorem :: GLIB_002:26 (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 (Set (Set (Var "G1")) ($#k3_glib_002 :::".componentSet()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k3_glib_002 :::".componentSet()"::: ) ))) ; theorem :: GLIB_002:27 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k3_glib_002 :::".componentSet()"::: ) ))) "holds" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" )))) ; theorem :: GLIB_002:28 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) "iff" (Bool (Set (Set (Var "G")) ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: GLIB_002:29 (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 (Set (Set (Var "G1")) ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k4_glib_002 :::".numComponents()"::: ) ))) ; theorem :: GLIB_002:30 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#m1_glib_000 :::"Component":::) "of" (Set (Var "G"))) "iff" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) ")" )) ; theorem :: GLIB_002:31 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "C")) "being" ($#m1_glib_000 :::"Component":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C")) ")" ))))) ; theorem :: GLIB_002:32 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_glib_000 :::"Component":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C2")))) "iff" (Bool (Set (Var "C1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "C2"))) ")" ))) ; theorem :: GLIB_002:33 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "C")) "being" ($#m1_glib_000 :::"Component":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C")))) "iff" (Bool (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v")))) ")" )))) ; theorem :: GLIB_002:34 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_glib_000 :::"Component":::) "of" (Set (Var "G")) (Bool "for" (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 "C1")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "C2"))))) "holds" (Bool (Set (Var "C1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "C2")))))) ; theorem :: GLIB_002:35 (Bool "for" (Set (Var "G")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "v")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )) "iff" (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G")) "," (Set (Var "v")) "holds" (Bool (Set (Set (Var "G2")) ($#k4_glib_002 :::".numComponents()"::: ) ) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "G")) ($#k4_glib_002 :::".numComponents()"::: ) ))) ")" ))) ; theorem :: GLIB_002:36 (Bool "for" (Set (Var "G")) "being" ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "G2")) "being" ($#m2_glib_000 :::"removeVertex":::) "of" (Set (Var "G")) "," (Set (Var "v")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) ))) "holds" (Bool (Set (Var "G2")) "is" ($#v1_glib_002 :::"connected"::: ) )))) ; theorem :: GLIB_002:37 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Bool "not" (Set (Var "v1")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )) & (Bool (Bool "not" (Set (Var "v2")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )) ")" ))) ; theorem :: GLIB_002:38 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )) "holds" (Bool "not" (Bool (Set (Var "G")) "is" ($#v4_glib_000 :::"trivial"::: ) )))) ; theorem :: GLIB_002:39 (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 "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )) "holds" (Bool (Set (Var "v2")) "is" ($#v5_glib_002 :::"cut-vertex"::: ) )))) ; theorem :: GLIB_002:40 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#v1_glib_002 :::"connected"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ; theorem :: GLIB_002:41 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Var "G")) "is" ($#v7_glib_000 :::"simple"::: ) )) ; theorem :: GLIB_002:42 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v5_glib_001 :::"Path-like"::: ) )))) ; theorem :: GLIB_002:43 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v2_glib_002 :::"acyclic"::: ) ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) & (Bool (Set (Var "v2")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k1_glib_002 :::".reachableFrom"::: ) (Set (Var "v1")))) ")" ))) ; theorem :: GLIB_002:44 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) "is" ($#v2_glib_002 :::"acyclic"::: ) )) "holds" (Bool (Set (Var "G2")) "is" ($#v2_glib_002 :::"acyclic"::: ) )) ; theorem :: GLIB_002:45 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#v3_glib_002 :::"Tree-like"::: ) ($#m1_hidden :::"_Graph":::) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) & (Bool (Set (Var "v2")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) ")" ))) ; theorem :: GLIB_002:46 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_002 :::"Tree-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v2_glib_002 :::"acyclic"::: ) ) & (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" )) ; theorem :: GLIB_002:47 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) "is" ($#v3_glib_002 :::"Tree-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "G")) "is" ($#v1_glib_002 :::"connected"::: ) ) & (Bool (Set (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k17_glib_000 :::".size()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" )) ; theorem :: GLIB_002:48 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) "is" ($#v3_glib_002 :::"Tree-like"::: ) )) "holds" (Bool (Set (Var "G2")) "is" ($#v3_glib_002 :::"Tree-like"::: ) )) ; theorem :: GLIB_002:49 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r1_glib_002 :::"is_DTree_rooted_at"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))))) ; theorem :: GLIB_002:50 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G1")) ($#r1_glib_002 :::"is_DTree_rooted_at"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "G2")) ($#r1_glib_002 :::"is_DTree_rooted_at"::: ) (Set (Var "x"))))) ;