:: GRAPH_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"MultiGraphStruct"::: -> ($#l5_struct_0 :::"2-sorted"::: ) ; aggr :::"MultiGraphStruct":::(# :::"carrier":::, :::"carrier'":::, :::"Source":::, :::"Target"::: #) -> ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; sel :::"Source"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"Target"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; definitionlet "G" be ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; mode Vertex of "G" is ($#m1_subset_1 :::"Element":::) "of" "G"; mode Edge of "G" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_graph_1 :::"strict"::: ) for ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; end; definitionmode Graph is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; end; definitionlet "C" be ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Edge":::) "of" (Set (Const "C")); func :::"dom"::: "f" -> ($#m1_subset_1 :::"Vertex":::) "of" "C" equals :: GRAPH_1:def 1 (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") ($#k1_funct_1 :::"."::: ) "f") if (Bool "(" (Bool (Bool "not" "C" "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" "C" "is" ($#v2_struct_0 :::"empty"::: ) )) ")" ) otherwise "the" ($#m1_subset_1 :::"Vertex":::) "of" "C"; func :::"cod"::: "f" -> ($#m1_subset_1 :::"Vertex":::) "of" "C" equals :: GRAPH_1:def 2 (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") ($#k1_funct_1 :::"."::: ) "f") if (Bool "(" (Bool (Bool "not" "C" "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" "C" "is" ($#v2_struct_0 :::"empty"::: ) )) ")" ) otherwise "the" ($#m1_subset_1 :::"Vertex":::) "of" "C"; end; :: deftheorem defines :::"dom"::: GRAPH_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_graph_1 :::"MultiGraphStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Edge":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "C")) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" (Set (Var "C")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k1_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "C")) "is" ($#v11_struct_0 :::"void"::: ) ) "or" (Bool (Set (Var "C")) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k1_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "C"))) ")" ")" ))); :: deftheorem defines :::"cod"::: GRAPH_1:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_graph_1 :::"MultiGraphStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Edge":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "C")) "is" ($#v11_struct_0 :::"void"::: ) )) & (Bool (Bool "not" (Set (Var "C")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool (Set ($#k2_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "C")) "is" ($#v11_struct_0 :::"void"::: ) ) "or" (Bool (Set (Var "C")) "is" ($#v2_struct_0 :::"empty"::: ) ) ")" )) "implies" (Bool (Set ($#k2_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "C"))) ")" ")" ))); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Edge":::) "of" (Set (Const "C")); :: original: :::"dom"::: redefine func :::"dom"::: "f" -> ($#m1_subset_1 :::"Vertex":::) "of" "C" equals :: GRAPH_1:def 3 (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") ($#k3_funct_2 :::"."::: ) "f"); :: original: :::"cod"::: redefine func :::"cod"::: "f" -> ($#m1_subset_1 :::"Vertex":::) "of" "C" equals :: GRAPH_1:def 4 (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") ($#k3_funct_2 :::"."::: ) "f"); end; :: deftheorem defines :::"dom"::: GRAPH_1:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_graph_1 :::"MultiGraphStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Edge":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) ($#k3_funct_2 :::"."::: ) (Set (Var "f")))))); :: deftheorem defines :::"cod"::: GRAPH_1:def 4 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_graph_1 :::"MultiGraphStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Edge":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) ($#k3_funct_2 :::"."::: ) (Set (Var "f")))))); definitionlet "G1", "G2" be ($#l1_graph_1 :::"Graph":::); assume that (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Const "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Const "G2")))) and (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Const "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Const "G2")))) ; func "G1" :::"\/"::: "G2" -> ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) means :: GRAPH_1:def 5 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G2"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G2"))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G1"))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G1") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G1") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G2"))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G2") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G2") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"\/"::: GRAPH_1:def 5 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2"))))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G2"))))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G1"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G2"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" ) ")" ) ")" ) ")" ))); definitionlet "G", "G1", "G2" be ($#l1_graph_1 :::"Graph":::); pred "G" :::"is_sum_of"::: "G1" "," "G2" means :: GRAPH_1:def 6 (Bool "(" (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G2")) & (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G1") ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G2")) & (Bool (Set ($#g1_graph_1 :::"MultiGraphStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") "#)" ) ($#r1_hidden :::"="::: ) (Set "G1" ($#k5_graph_1 :::"\/"::: ) "G2")) ")" ); end; :: deftheorem defines :::"is_sum_of"::: GRAPH_1:def 6 : (Bool "for" (Set (Var "G")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2"))) "iff" (Bool "(" (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set ($#g1_graph_1 :::"MultiGraphStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) "#)" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) ")" ) ")" )); definitionlet "IT" be ($#l1_graph_1 :::"Graph":::); attr "IT" is :::"oriented"::: means :: GRAPH_1:def 7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT")) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "IT" is :::"non-multi"::: means :: GRAPH_1:def 8 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT")) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT")) & (Bool "(" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) "or" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))); attr "IT" is :::"simple"::: means :: GRAPH_1:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT")) "or" "not" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "IT") ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )); attr "IT" is :::"connected"::: means :: GRAPH_1:def 10 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" "not" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2")))) "or" "not" (Bool "IT" ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2"))) ")" )); end; :: deftheorem defines :::"oriented"::: GRAPH_1:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_graph_1 :::"oriented"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"non-multi"::: GRAPH_1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_graph_1 :::"non-multi"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT")))) & (Bool "(" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) "or" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ")" )); :: deftheorem defines :::"simple"::: GRAPH_1:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_graph_1 :::"simple"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT")))) "or" "not" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "IT"))) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) ")" )); :: deftheorem defines :::"connected"::: GRAPH_1:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_graph_1 :::"connected"::: ) ) "iff" (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" "not" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1"))) ($#r1_subset_1 :::"misses"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2")))) "or" "not" (Bool (Set (Var "IT")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2"))) ")" )) ")" )); definitionlet "IT" be ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; attr "IT" is :::"finite"::: means :: GRAPH_1:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "IT") "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "IT") "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ); end; :: deftheorem defines :::"finite"::: GRAPH_1:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#l1_graph_1 :::"MultiGraphStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_graph_1 :::"finite"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "IT"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "IT"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) ")" )); registration cluster ($#v6_graph_1 :::"finite"::: ) for ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v14_struct_0 :::"feasible"::: ) ($#v2_graph_1 :::"oriented"::: ) ($#v3_graph_1 :::"non-multi"::: ) ($#v4_graph_1 :::"simple"::: ) ($#v5_graph_1 :::"connected"::: ) ($#v6_graph_1 :::"finite"::: ) for ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; end; registrationlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; cluster (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); let "v" be ($#m1_hidden :::"set"::: ) ; pred "v" :::"joins"::: "x" "," "y" means :: GRAPH_1:def 12 (Bool "(" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "v") ($#r1_hidden :::"="::: ) "x") & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "v") ($#r1_hidden :::"="::: ) "y") ")" ) "or" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "v") ($#r1_hidden :::"="::: ) "y") & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) "v") ($#r1_hidden :::"="::: ) "x") ")" ) ")" ); end; :: deftheorem defines :::"joins"::: GRAPH_1:def 12 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "v")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) "or" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "x", "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); pred "x" "," "y" :::"are_incident"::: means :: GRAPH_1:def 13 (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool (Set (Var "v")) ($#r2_graph_1 :::"joins"::: ) "x" "," "y") ")" )); end; :: deftheorem defines :::"are_incident"::: GRAPH_1:def 13 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_graph_1 :::"are_incident"::: ) ) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "v")) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )) ")" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode :::"Chain"::: "of" "G" -> ($#m1_hidden :::"FinSequence":::) means :: GRAPH_1:def 14 (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) ")" ) & (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x9")) "," (Set (Var "y9"))) ")" )) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"Chain"::: GRAPH_1:def 14 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) ")" ) & (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))))) "holds" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x9")) "," (Set (Var "y9"))) ")" )) ")" ) ")" )) ")" ) ")" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); :: original: :::"Chain"::: redefine mode :::"Chain"::: "of" "G" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G"); end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "IT" be ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); attr "IT" is :::"oriented"::: means :: GRAPH_1:def 15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "IT"))) "holds" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "IT" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"oriented"::: GRAPH_1:def 15 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_graph_1 :::"oriented"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" ))); registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v7_graph_1 :::"oriented"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "IT" be ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Const "G")); :: original: :::"one-to-one"::: redefine attr "IT" is :::"one-to-one"::: means :: GRAPH_1:def 16 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))); end; :: deftheorem defines :::"one-to-one"::: GRAPH_1:def 16 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) ")" ))); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode Path of "G" is bbbadV2_FUNCT_1() ($#m2_graph_1 :::"Chain"::: ) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode OrientedPath of "G" is bbbadV2_FUNCT_1() ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "IT" be ($#m2_graph_1 :::"Path":::) "of" (Set (Const "G")); attr "IT" is :::"cyclic"::: means :: GRAPH_1:def 17 (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "IT" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "IT"))) "holds" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x9")) "," (Set (Var "y9"))) ")" )) ")" ) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" )); end; :: deftheorem defines :::"cyclic"::: GRAPH_1:def 17 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "IT")) "being" ($#m2_graph_1 :::"Path":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v9_graph_1 :::"cyclic"::: ) ) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "IT"))))) "holds" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_graph_1 :::"joins"::: ) (Set (Var "x9")) "," (Set (Var "y9"))) ")" )) ")" ) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) ")" )) ")" ))); registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v9_graph_1 :::"cyclic"::: ) for ($#m1_graph_1 :::"Chain"::: ) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode Cycle of "G" is ($#v9_graph_1 :::"cyclic"::: ) ($#m2_graph_1 :::"Path":::) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode OrientedCycle of "G" is ($#v9_graph_1 :::"cyclic"::: ) ($#m2_graph_1 :::"OrientedPath":::) "of" "G"; end; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); mode :::"Subgraph"::: "of" "G" -> ($#l1_graph_1 :::"Graph":::) means :: GRAPH_1:def 18 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it)) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Subgraph"::: GRAPH_1:def 18 : (Bool "for" (Set (Var "G")) "," (Set (Var "b2")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "b2"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2")))) ")" ) ")" ) ")" ) ")" )); registrationlet "G" be ($#l1_graph_1 :::"Graph":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v14_struct_0 :::"feasible"::: ) ($#v1_graph_1 :::"strict"::: ) for ($#m3_graph_1 :::"Subgraph"::: ) "of" "G"; end; definitionlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); func :::"VerticesCount"::: "G" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPH_1:def 19 (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )); func :::"EdgesCount"::: "G" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPH_1:def 20 (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )); end; :: deftheorem defines :::"VerticesCount"::: GRAPH_1:def 19 : (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_graph_1 :::"VerticesCount"::: ) (Set (Var "G")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )) ")" ))); :: deftheorem defines :::"EdgesCount"::: GRAPH_1:def 20 : (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_graph_1 :::"EdgesCount"::: ) (Set (Var "G")))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B")))) ")" )) ")" ))); definitionlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); let "x" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"EdgesIn"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPH_1:def 21 (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) "x") ")" ) ")" ) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )); func :::"EdgesOut"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPH_1:def 22 (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) "x") ")" ) ")" ) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )); end; :: deftheorem defines :::"EdgesIn"::: GRAPH_1:def 21 : (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_graph_1 :::"EdgesIn"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )) ")" )))); :: deftheorem defines :::"EdgesOut"::: GRAPH_1:def 22 : (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_graph_1 :::"EdgesOut"::: ) (Set (Var "x")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ) ")" ) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )) ")" )))); definitionlet "G" be ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::); let "x" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func :::"Degree"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GRAPH_1:def 23 (Set (Set "(" ($#k8_graph_1 :::"EdgesIn"::: ) "x" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k9_graph_1 :::"EdgesOut"::: ) "x" ")" )); end; :: deftheorem defines :::"Degree"::: GRAPH_1:def 23 : (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k10_graph_1 :::"Degree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_graph_1 :::"EdgesIn"::: ) (Set (Var "x")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k9_graph_1 :::"EdgesOut"::: ) (Set (Var "x")) ")" ))))); definitionlet "G1", "G2" be ($#l1_graph_1 :::"Graph":::); pred "G1" :::"c="::: "G2" means :: GRAPH_1:def 24 (Bool "G1" "is" ($#m3_graph_1 :::"Subgraph"::: ) "of" "G2"); reflexivity (Bool "for" (Set (Var "G1")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set (Var "G1")) "is" ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set (Var "G1")))) ; end; :: deftheorem defines :::"c="::: GRAPH_1:def 24 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2"))) "iff" (Bool (Set (Var "G1")) "is" ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set (Var "G2"))) ")" )); definitionlet "G" be ($#l1_graph_1 :::"Graph":::); func :::"bool"::: "G" -> ($#m1_hidden :::"set"::: ) means :: GRAPH_1:def 25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v1_graph_1 :::"strict"::: ) ($#m3_graph_1 :::"Subgraph"::: ) "of" "G") ")" )); end; :: deftheorem defines :::"bool"::: GRAPH_1:def 25 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#v1_graph_1 :::"strict"::: ) ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set (Var "G"))) ")" )) ")" ))); scheme :: GRAPH_1:sch 1 GraphSeparation{ F1() -> ($#l1_graph_1 :::"Graph":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_graph_1 :::"strict"::: ) ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))]) ")" ) ")" ))) proof end; theorem :: GRAPH_1:1 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G")))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) ")" )) ; theorem :: GRAPH_1:2 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))))) ; theorem :: GRAPH_1:3 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) ")" ))) ; theorem :: GRAPH_1:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "p")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))))) ; theorem :: GRAPH_1:5 (Bool "for" (Set (Var "G1")) "," (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool "(" (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G")))) ")" )) ; theorem :: GRAPH_1:6 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) "holds" (Bool "(" (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2"))))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) ")" )) ; theorem :: GRAPH_1:7 (Bool "for" (Set (Var "G")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G"))))) ; theorem :: GRAPH_1:8 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G1"))))) ; theorem :: GRAPH_1:9 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G3")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G3")))) & (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G3")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G3"))))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" ) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set "(" (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G3")) ")" )))) ; theorem :: GRAPH_1:10 (Bool "for" (Set (Var "G")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G2")) "," (Set (Var "G1")))) ; theorem :: GRAPH_1:11 (Bool "for" (Set (Var "G")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G")) "," (Set (Var "G")))) ; theorem :: GRAPH_1:12 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool "ex" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) ")" ))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G1"))))) ; theorem :: GRAPH_1:13 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool "ex" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G3")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" ) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set "(" (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G3")) ")" )))) ; theorem :: GRAPH_1:14 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")))) ; theorem :: GRAPH_1:15 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v1_graph_1 :::"strict"::: ) ($#m3_graph_1 :::"Subgraph"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "H2")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "H1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "H2"))))) "holds" (Bool (Set (Var "H1")) ($#r1_hidden :::"="::: ) (Set (Var "H2"))))) ; theorem :: GRAPH_1:16 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G1")))) "holds" (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Var "G2")))) ; theorem :: GRAPH_1:17 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G3")))) "holds" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G3")))) ; theorem :: GRAPH_1:18 (Bool "for" (Set (Var "G")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) ")" )) ; theorem :: GRAPH_1:19 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) ")" )) ; theorem :: GRAPH_1:20 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool "ex" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) ")" ))) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")))) ")" )) ; theorem :: GRAPH_1:21 (Bool "for" (Set (Var "G1")) "," (Set (Var "G3")) "," (Set (Var "G2")) "," (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G3"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G3"))) & (Bool (Set (Var "G")) ($#r1_graph_1 :::"is_sum_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool (Set (Var "G")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G3")))) ; theorem :: GRAPH_1:22 (Bool "for" (Set (Var "G1")) "," (Set (Var "G")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) & (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) ; theorem :: GRAPH_1:23 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2")))) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) & (Bool (Set (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) ")" )) ; theorem :: GRAPH_1:24 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2")))) & (Bool "(" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) "or" (Bool (Set (Set (Var "G2")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G1"))) ($#r1_hidden :::"="::: ) (Set (Var "G2"))) ")" )) "holds" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2")))) ; theorem :: GRAPH_1:25 (Bool "for" (Set (Var "G1")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G1")) "is" ($#v2_graph_1 :::"oriented"::: ) ))) ; theorem :: GRAPH_1:26 (Bool "for" (Set (Var "G1")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "G")) "being" ($#v3_graph_1 :::"non-multi"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G1")) "is" ($#v3_graph_1 :::"non-multi"::: ) ))) ; theorem :: GRAPH_1:27 (Bool "for" (Set (Var "G1")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "G")) "being" ($#v4_graph_1 :::"simple"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "G1")) "is" ($#v4_graph_1 :::"simple"::: ) ))) ; theorem :: GRAPH_1:28 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "G1")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G")))) "iff" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G"))) ")" ))) ; theorem :: GRAPH_1:29 (Bool "for" (Set (Var "G")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G"))))) ; theorem :: GRAPH_1:30 (Bool "for" (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "G1")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool "(" (Bool (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2"))) "iff" (Bool (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G1"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G2")))) ")" ))) ; theorem :: GRAPH_1:31 (Bool "for" (Set (Var "G")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "G")) ($#k1_tarski :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G"))))) ; theorem :: GRAPH_1:32 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v1_graph_1 :::"strict"::: ) ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2")))) & (Bool (Set ($#k11_graph_1 :::"bool"::: ) (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k11_graph_1 :::"bool"::: ) (Set (Var "G1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k11_graph_1 :::"bool"::: ) (Set (Var "G2")) ")" ))) & (Bool (Bool "not" (Set (Var "G1")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "G2")) ($#r4_graph_1 :::"c="::: ) (Set (Var "G1")))) ; theorem :: GRAPH_1:33 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G2")))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G1"))) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G2"))))) "holds" (Bool (Set (Set "(" ($#k11_graph_1 :::"bool"::: ) (Set (Var "G1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k11_graph_1 :::"bool"::: ) (Set (Var "G2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set "(" (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2")) ")" )))) ; theorem :: GRAPH_1:34 (Bool "for" (Set (Var "G1")) "," (Set (Var "G")) "," (Set (Var "G2")) "being" ($#l1_graph_1 :::"Graph":::) "st" (Bool (Bool (Set (Var "G1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G")))) & (Bool (Set (Var "G2")) ($#r2_hidden :::"in"::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_graph_1 :::"\/"::: ) (Set (Var "G2"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_graph_1 :::"bool"::: ) (Set (Var "G"))))) ;