:: GLIB_001 semantic presentation begin theorem :: GLIB_001:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y"))) "iff" (Bool (Set (Set (Var "x")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) ")" )) ; theorem :: GLIB_001:2 canceled; theorem :: GLIB_001:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "fs"))))))) ; theorem :: GLIB_001:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss")) ")" )))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "fs")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "fs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )))))) ; theorem :: GLIB_001:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "fss"))))))) ; theorem :: GLIB_001:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "fss")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "fs")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "fss")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k14_finseq_1 :::"Sgm"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "fss")) ")" ) ")" )))))) ; begin definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"VertexSeq"::: "of" "G" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") means :: GLIB_001:def 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"::: ) it))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," "G"))); end; :: deftheorem defines :::"VertexSeq"::: GLIB_001:def 1 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_glib_001 :::"VertexSeq"::: ) "of" (Set (Var "G"))) "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 "b2"))))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "G"))))) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"EdgeSeq"::: "of" "G" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) "G") means :: GLIB_001:def 2 (Bool "ex" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G") "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs"))) ($#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"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," "G") ")" ) ")" )); end; :: deftheorem defines :::"EdgeSeq"::: GLIB_001:def 2 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_glib_001 :::"EdgeSeq"::: ) "of" (Set (Var "G"))) "iff" (Bool "ex" (Set (Var "vs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs"))) ($#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 "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "G"))) ")" ) ")" )) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode :::"Walk"::: "of" "G" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )) means :: GLIB_001:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) "G")) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_glib_000 :::"Joins"::: ) (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) "," "G") ")" ) ")" ); end; :: deftheorem defines :::"Walk"::: GLIB_001:def 3 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b2"))) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (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 "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G"))) ")" ) ")" ) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster (Set ($#k1_card_1 :::"card"::: ) "W") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_abian :::"odd"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); func "G" :::".walkOf"::: "v" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 4 (Set ($#k12_finseq_1 :::"<*"::: ) "v" ($#k12_finseq_1 :::"*>"::: ) ); end; :: deftheorem defines :::".walkOf"::: GLIB_001:def 4 : (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")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "x", "y", "e" be ($#m1_hidden :::"set"::: ) ; func "G" :::".walkOf"::: "(" "x" "," "e" "," "y" ")" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 5 (Set ($#k11_finseq_1 :::"<*"::: ) "x" "," "e" "," "y" ($#k11_finseq_1 :::"*>"::: ) ) if (Bool "e" ($#r1_glib_000 :::"Joins"::: ) "x" "," "y" "," "G") otherwise (Set "G" ($#k1_glib_001 :::".walkOf"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ")" )); end; :: deftheorem defines :::".walkOf"::: GLIB_001:def 5 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "implies" (Bool (Set (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ($#k11_finseq_1 :::"*>"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))))) "implies" (Bool (Set (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set "(" ($#k10_subset_1 :::"choose"::: ) (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G")) ")" ) ")" ))) ")" ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".first()"::: -> ($#m1_subset_1 :::"Vertex":::) "of" "G" equals :: GLIB_001:def 6 (Set "W" ($#k1_funct_1 :::"."::: ) (Num 1)); func "W" :::".last()"::: -> ($#m1_subset_1 :::"Vertex":::) "of" "G" equals :: GLIB_001:def 7 (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "W" ")" )); end; :: deftheorem defines :::".first()"::: GLIB_001:def 6 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Num 1))))); :: deftheorem defines :::".last()"::: GLIB_001:def 7 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "n" be ($#m1_hidden :::"Nat":::); func "W" :::".vertexAt"::: "n" -> ($#m1_subset_1 :::"Vertex":::) "of" "G" equals :: GLIB_001:def 8 (Set "W" ($#k1_funct_1 :::"."::: ) "n") if (Bool "(" (Bool "n" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) ")" ) otherwise (Set "W" ($#k3_glib_001 :::".first()"::: ) ); end; :: deftheorem defines :::".vertexAt"::: GLIB_001:def 8 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "implies" (Bool (Set (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" )) "implies" (Bool (Set (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) )) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".reverse()"::: -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 9 (Set ($#k4_finseq_5 :::"Rev"::: ) "W"); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "b1"))))) ; end; :: deftheorem defines :::".reverse()"::: GLIB_001:def 9 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "W")))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W1", "W2" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W1" :::".append"::: "W2" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 10 (Set "W1" ($#k4_graph_2 :::"^'"::: ) "W2") if (Bool (Set "W1" ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set "W2" ($#k3_glib_001 :::".first()"::: ) )) otherwise "W1"; end; :: deftheorem defines :::".append"::: GLIB_001:def 10 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "implies" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k4_graph_2 :::"^'"::: ) (Set (Var "W2")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )))) "implies" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) ")" ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_hidden :::"Nat":::); func "W" :::".cut"::: "(" "m" "," "n" ")" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 11 (Set "(" "m" "," "n" ")" ($#k2_graph_2 :::"-cut"::: ) "W") if (Bool "(" (Bool "m" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "n" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "m" ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) ")" ) otherwise "W"; end; :: deftheorem defines :::".cut"::: GLIB_001:def 11 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "implies" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "m")) "," (Set (Var "n")) ")" ($#k2_graph_2 :::"-cut"::: ) (Set (Var "W")))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" )) "implies" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "W" :::".remove"::: "(" "m" "," "n" ")" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 12 (Set (Set "(" "W" ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," "m" ")" ")" ) ($#k7_glib_001 :::".append"::: ) (Set "(" "W" ($#k8_glib_001 :::".cut"::: ) "(" "n" "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "W" ")" ) ")" ")" )) if (Bool "(" (Bool "m" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "n" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "m" ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) "m") ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) "n")) ")" ) otherwise "W"; end; :: deftheorem defines :::".remove"::: GLIB_001:def 12 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "W")) ($#k9_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ")" ) ($#k7_glib_001 :::".append"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "n")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ")" ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) "or" "not" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )) "implies" (Bool (Set (Set (Var "W")) ($#k9_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "W"))) ")" ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "e" be ($#m1_hidden :::"set"::: ) ; func "W" :::".addEdge"::: "e" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" equals :: GLIB_001:def 13 (Set "W" ($#k7_glib_001 :::".append"::: ) (Set "(" "G" ($#k2_glib_001 :::".walkOf"::: ) "(" (Set "(" "W" ($#k4_glib_001 :::".last()"::: ) ")" ) "," "e" "," (Set "(" (Set "(" "W" ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k29_glib_000 :::".adj"::: ) "e" ")" ) ")" ")" )); end; :: deftheorem defines :::".addEdge"::: GLIB_001:def 13 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k7_glib_001 :::".append"::: ) (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) "," (Set (Var "e")) "," (Set "(" (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k29_glib_000 :::".adj"::: ) (Set (Var "e")) ")" ) ")" ")" )))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".vertexSeq()"::: -> ($#m1_glib_001 :::"VertexSeq"::: ) "of" "G" means :: GLIB_001:def 14 (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "W" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"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"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::".vertexSeq()"::: GLIB_001:def 14 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m1_glib_001 :::"VertexSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) )) "iff" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"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 "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".edgeSeq()"::: -> ($#m2_glib_001 :::"EdgeSeq"::: ) "of" "G" means :: GLIB_001:def 15 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "W") ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) it ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"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"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::".edgeSeq()"::: GLIB_001:def 15 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "b3")) "being" ($#m2_glib_001 :::"EdgeSeq"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"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 "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".vertices()"::: -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) equals :: GLIB_001:def 16 (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" "W" ($#k11_glib_001 :::".vertexSeq()"::: ) ")" )); end; :: deftheorem defines :::".vertices()"::: GLIB_001:def 16 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".edges()"::: -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) equals :: GLIB_001:def 17 (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" )); end; :: deftheorem defines :::".edges()"::: GLIB_001:def 17 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); func "W" :::".length()"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GLIB_001:def 18 (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" )); end; :: deftheorem defines :::".length()"::: GLIB_001:def 18 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k15_glib_001 :::".length()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "v" be ($#m1_hidden :::"set"::: ) ; func "W" :::".find"::: "v" -> ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_001:def 19 (Bool "(" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) "v") & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "v")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) if (Bool "v" ($#r2_hidden :::"in"::: ) (Set "W" ($#k13_glib_001 :::".vertices()"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")); end; :: deftheorem defines :::".find"::: GLIB_001:def 19 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k16_glib_001 :::".find"::: ) (Set (Var "v")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k16_glib_001 :::".find"::: ) (Set (Var "v")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ) ")" ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "W" :::".find"::: "n" -> ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_001:def 20 (Bool "(" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) "n")) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) "n"))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) if (Bool "(" (Bool "n" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")); end; :: deftheorem defines :::".find"::: GLIB_001:def 20 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k17_glib_001 :::".find"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_abian :::"odd"::: ) ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k17_glib_001 :::".find"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ) ")" ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "v" be ($#m1_hidden :::"set"::: ) ; func "W" :::".rfind"::: "v" -> ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_001:def 21 (Bool "(" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) "v") & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "v")) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ) if (Bool "v" ($#r2_hidden :::"in"::: ) (Set "W" ($#k13_glib_001 :::".vertices()"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")); end; :: deftheorem defines :::".rfind"::: GLIB_001:def 21 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k18_glib_001 :::".rfind"::: ) (Set (Var "v")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b4"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k18_glib_001 :::".rfind"::: ) (Set (Var "v")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ) ")" ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "W" :::".rfind"::: "n" -> ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GLIB_001:def 22 (Bool "(" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) "n")) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) "n"))) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ) if (Bool "(" (Bool "n" "is" ($#v1_abian :::"odd"::: ) ) & (Bool "n" ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")); end; :: deftheorem defines :::".rfind"::: GLIB_001:def 22 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k19_glib_001 :::".rfind"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b4"))) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "n")) "is" ($#v1_abian :::"odd"::: ) ) "or" "not" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k19_glib_001 :::".rfind"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ) ")" ")" ))))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "u", "v" be ($#m1_hidden :::"set"::: ) ; let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); pred "W" :::"is_Walk_from"::: "u" "," "v" means :: GLIB_001:def 23 (Bool "(" (Bool (Set "W" ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) "u") & (Bool (Set "W" ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) "v") ")" ); end; :: deftheorem defines :::"is_Walk_from"::: GLIB_001:def 23 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "u")) "," (Set (Var "v"))) "iff" (Bool "(" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "u"))) & (Bool (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) ")" )))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); attr "W" is :::"closed"::: means :: GLIB_001:def 24 (Bool (Set "W" ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set "W" ($#k4_glib_001 :::".last()"::: ) )); attr "W" is :::"directed"::: means :: GLIB_001:def 25 (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W"))) "holds" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) "G" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "W" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))); attr "W" is :::"trivial"::: means :: GLIB_001:def 26 (Bool (Set "W" ($#k15_glib_001 :::".length()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); attr "W" is :::"Trail-like"::: means :: GLIB_001:def 27 (Bool (Set "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ); end; :: deftheorem defines :::"closed"::: GLIB_001:def 24 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) )) ")" ))); :: deftheorem defines :::"directed"::: GLIB_001:def 25 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v2_glib_001 :::"directed"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" ($#k10_glib_000 :::"the_Source_of"::: ) (Set (Var "G")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ))); :: deftheorem defines :::"trivial"::: GLIB_001:def 26 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k15_glib_001 :::".length()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); :: deftheorem defines :::"Trail-like"::: GLIB_001:def 27 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))); notationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); antonym :::"open"::: "W" for :::"closed"::: ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); attr "W" is :::"Path-like"::: means :: GLIB_001:def 28 (Bool "(" (Bool "W" "is" ($#v4_glib_001 :::"Trail-like"::: ) ) & (Bool "(" "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Path-like"::: GLIB_001:def 28 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) & (Bool "(" "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ) ")" ) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); attr "W" is :::"vertex-distinct"::: means :: GLIB_001:def 29 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "W")) & (Bool (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))); end; :: deftheorem defines :::"vertex-distinct"::: GLIB_001:def 29 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); attr "W" is :::"Circuit-like"::: means :: GLIB_001:def 30 (Bool "(" (Bool "W" "is" ($#v1_glib_001 :::"closed"::: ) ) & (Bool "W" "is" ($#v4_glib_001 :::"Trail-like"::: ) ) & (Bool (Bool "not" "W" "is" ($#v3_glib_001 :::"trivial"::: ) )) ")" ); attr "W" is :::"Cycle-like"::: means :: GLIB_001:def 31 (Bool "(" (Bool "W" "is" ($#v1_glib_001 :::"closed"::: ) ) & (Bool "W" "is" ($#v5_glib_001 :::"Path-like"::: ) ) & (Bool (Bool "not" "W" "is" ($#v3_glib_001 :::"trivial"::: ) )) ")" ); end; :: deftheorem defines :::"Circuit-like"::: GLIB_001:def 30 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v7_glib_001 :::"Circuit-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) & (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) & (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) ")" ) ")" ))); :: deftheorem defines :::"Cycle-like"::: GLIB_001:def 31 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) & (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) & (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) ")" ) ")" ))); registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v5_glib_001 :::"Path-like"::: ) -> ($#v4_glib_001 :::"Trail-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; cluster ($#v3_glib_001 :::"trivial"::: ) -> ($#v5_glib_001 :::"Path-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; cluster ($#v3_glib_001 :::"trivial"::: ) -> ($#v6_glib_001 :::"vertex-distinct"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; cluster ($#v6_glib_001 :::"vertex-distinct"::: ) -> ($#v5_glib_001 :::"Path-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; cluster ($#v7_glib_001 :::"Circuit-like"::: ) -> ($#v1_glib_001 :::"closed"::: ) ($#~v3_glib_001 "non" ($#v3_glib_001 :::"trivial"::: ) ) ($#v4_glib_001 :::"Trail-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; cluster ($#v8_glib_001 :::"Cycle-like"::: ) -> ($#v1_glib_001 :::"closed"::: ) ($#~v3_glib_001 "non" ($#v3_glib_001 :::"trivial"::: ) ) ($#v5_glib_001 :::"Path-like"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_glib_001 :::"closed"::: ) ($#v2_glib_001 :::"directed"::: ) ($#v3_glib_001 :::"trivial"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v6_glib_001 :::"vertex-distinct"::: ) for ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode Trail of "G" is ($#v4_glib_001 :::"Trail-like"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" "G"; mode Path of "G" is ($#v5_glib_001 :::"Path-like"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); mode DWalk of "G" is ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" "G"; mode DTrail of "G" is ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Trail":::) "of" "G"; mode DPath of "G" is ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Path":::) "of" "G"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); cluster (Set "G" ($#k1_glib_001 :::".walkOf"::: ) "v") -> ($#v1_glib_001 :::"closed"::: ) ($#v2_glib_001 :::"directed"::: ) ($#v3_glib_001 :::"trivial"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "x", "e", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k2_glib_001 :::".walkOf"::: ) "(" "x" "," "e" "," "y" ")" ) -> ($#v5_glib_001 :::"Path-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "x", "e" be ($#m1_hidden :::"set"::: ) ; cluster (Set "G" ($#k2_glib_001 :::".walkOf"::: ) "(" "x" "," "e" "," "x" ")" ) -> ($#v1_glib_001 :::"closed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v1_glib_001 :::"closed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster (Set "W" ($#k6_glib_001 :::".reverse()"::: ) ) -> ($#v1_glib_001 :::"closed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v3_glib_001 :::"trivial"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster (Set "W" ($#k6_glib_001 :::".reverse()"::: ) ) -> ($#v3_glib_001 :::"trivial"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Trail":::) "of" (Set (Const "G")); cluster (Set "W" ($#k6_glib_001 :::".reverse()"::: ) ) -> ($#v4_glib_001 :::"Trail-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Path":::) "of" (Set (Const "G")); cluster (Set "W" ($#k6_glib_001 :::".reverse()"::: ) ) -> ($#v5_glib_001 :::"Path-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W1", "W2" be ($#v1_glib_001 :::"closed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster (Set "W1" ($#k7_glib_001 :::".append"::: ) "W2") -> ($#v1_glib_001 :::"closed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W1", "W2" be ($#m3_glib_001 :::"DWalk":::) "of" (Set (Const "G")); cluster (Set "W1" ($#k7_glib_001 :::".append"::: ) "W2") -> ($#v2_glib_001 :::"directed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W1", "W2" be ($#v3_glib_001 :::"trivial"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster (Set "W1" ($#k7_glib_001 :::".append"::: ) "W2") -> ($#v3_glib_001 :::"trivial"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"DWalk":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k8_glib_001 :::".cut"::: ) "(" "m" "," "n" ")" ) -> ($#v2_glib_001 :::"directed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v3_glib_001 :::"trivial"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k8_glib_001 :::".cut"::: ) "(" "m" "," "n" ")" ) -> ($#v3_glib_001 :::"trivial"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Trail":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k8_glib_001 :::".cut"::: ) "(" "m" "," "n" ")" ) -> ($#v4_glib_001 :::"Trail-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Path":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k8_glib_001 :::".cut"::: ) "(" "m" "," "n" ")" ) -> ($#v5_glib_001 :::"Path-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v6_glib_001 :::"vertex-distinct"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k8_glib_001 :::".cut"::: ) "(" "m" "," "n" ")" ) -> ($#v6_glib_001 :::"vertex-distinct"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v1_glib_001 :::"closed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k9_glib_001 :::".remove"::: ) "(" "m" "," "n" ")" ) -> ($#v1_glib_001 :::"closed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"DWalk":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k9_glib_001 :::".remove"::: ) "(" "m" "," "n" ")" ) -> ($#v2_glib_001 :::"directed"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#v3_glib_001 :::"trivial"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k9_glib_001 :::".remove"::: ) "(" "m" "," "n" ")" ) -> ($#v3_glib_001 :::"trivial"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Trail":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k9_glib_001 :::".remove"::: ) "(" "m" "," "n" ")" ) -> ($#v4_glib_001 :::"Trail-like"::: ) ; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Path":::) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "W" ($#k9_glib_001 :::".remove"::: ) "(" "m" "," "n" ")" ) -> ($#v5_glib_001 :::"Path-like"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); mode :::"Subwalk"::: "of" "W" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G" means :: GLIB_001:def 32 (Bool "(" (Bool it ($#r1_glib_001 :::"is_Walk_from"::: ) (Set "W" ($#k3_glib_001 :::".first()"::: ) ) "," (Set "W" ($#k4_glib_001 :::".last()"::: ) )) & (Bool "ex" (Set (Var "es")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "W" ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) "st" (Bool (Set it ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "es"))))) ")" ); end; :: deftheorem defines :::"Subwalk"::: GLIB_001:def 32 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "," (Set (Var "b3")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W"))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) "," (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) )) & (Bool "ex" (Set (Var "es")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) "st" (Bool (Set (Set (Var "b3")) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_finseq_1 :::"Seq"::: ) (Set (Var "es"))))) ")" ) ")" ))); definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); let "m", "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::".remove"::: redefine func "W" :::".remove"::: "(" "m" "," "n" ")" -> ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_glib_001 :::"Trail-like"::: ) ($#v5_glib_001 :::"Path-like"::: ) for ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Const "G")); mode Trail of "W" is ($#v4_glib_001 :::"Trail-like"::: ) ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; mode Path of "W" is ($#v5_glib_001 :::"Path-like"::: ) ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; end; registrationlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"DWalk":::) "of" (Set (Const "G")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v2_glib_001 :::"directed"::: ) ($#v4_glib_001 :::"Trail-like"::: ) ($#v5_glib_001 :::"Path-like"::: ) for ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "W" be ($#m3_glib_001 :::"DWalk":::) "of" (Set (Const "G")); mode DWalk of "W" is ($#v2_glib_001 :::"directed"::: ) ($#m4_glib_001 :::"Subwalk"::: ) "of" "W"; mode DTrail of "W" is ($#v2_glib_001 :::"directed"::: ) ($#m4_glib_001 :::"Trail":::) "of" "W"; mode DPath of "W" is ($#v2_glib_001 :::"directed"::: ) ($#m4_glib_001 :::"Path":::) "of" "W"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allWalks()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" (Set "(" ($#k6_glib_000 :::"the_Vertices_of"::: ) "G" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k7_glib_000 :::"the_Edges_of"::: ) "G" ")" ) ")" ) ($#k13_finseq_1 :::"*"::: ) ")" ) equals :: GLIB_001:def 33 "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Walk"::: ) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allWalks()"::: GLIB_001:def 33 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k21_glib_001 :::".allWalks()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) : (Bool verum) "}" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allTrails()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "G" ($#k21_glib_001 :::".allWalks()"::: ) ")" ) equals :: GLIB_001:def 34 "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Trail":::) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allTrails()"::: GLIB_001:def 34 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k22_glib_001 :::".allTrails()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) : (Bool verum) "}" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allPaths()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "G" ($#k22_glib_001 :::".allTrails()"::: ) ")" ) equals :: GLIB_001:def 35 "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Path":::) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allPaths()"::: GLIB_001:def 35 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k23_glib_001 :::".allPaths()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) : (Bool verum) "}" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allDWalks()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "G" ($#k21_glib_001 :::".allWalks()"::: ) ")" ) equals :: GLIB_001:def 36 "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"DWalk":::) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allDWalks()"::: GLIB_001:def 36 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k24_glib_001 :::".allDWalks()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) : (Bool verum) "}" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allDTrails()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "G" ($#k22_glib_001 :::".allTrails()"::: ) ")" ) equals :: GLIB_001:def 37 "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"DTrail":::) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allDTrails()"::: GLIB_001:def 37 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k25_glib_001 :::".allDTrails()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#m3_glib_001 :::"DTrail":::) "of" (Set (Var "G")) : (Bool verum) "}" )); definitionlet "G" be ($#m1_hidden :::"_Graph":::); func "G" :::".allDPaths()"::: -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" "G" ($#k25_glib_001 :::".allDTrails()"::: ) ")" ) equals :: GLIB_001:def 38 "{" (Set (Var "W")) where W "is" ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Path":::) "of" "G" : (Bool verum) "}" ; end; :: deftheorem defines :::".allDPaths()"::: GLIB_001:def 38 : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) "holds" (Bool (Set (Set (Var "G")) ($#k26_glib_001 :::".allDPaths()"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set (Var "W")) where W "is" ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) : (Bool verum) "}" )); registrationlet "G" be ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::); cluster (Set "G" ($#k22_glib_001 :::".allTrails()"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k21_glib_001 :::".allWalks()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"Walk"::: ) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k22_glib_001 :::".allTrails()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"Trail":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k23_glib_001 :::".allPaths()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"Path":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k24_glib_001 :::".allDWalks()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"DWalk":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k25_glib_001 :::".allDTrails()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"DTrail":::) "of" "G"; end; definitionlet "G" be ($#m1_hidden :::"_Graph":::); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "G")) ($#k26_glib_001 :::".allDPaths()"::: ) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "X" -> ($#m3_glib_001 :::"DPath":::) "of" "G"; end; begin theorem :: GLIB_001:7 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k6_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G"))))))) ; theorem :: GLIB_001:8 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))))))) ; theorem :: GLIB_001:9 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W"))))) "holds" (Bool "ex" (Set (Var "naa1")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "naa1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "naa1"))) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) "," (Set (Var "G"))) ")" ))))) ; theorem :: GLIB_001:10 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n")) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))))) ; theorem :: GLIB_001:11 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#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 "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n")) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))))) ; theorem :: GLIB_001:12 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" )))) ; theorem :: GLIB_001:13 (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 ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "v")) "," (Set (Var "v"))) ")" ))) ; theorem :: GLIB_001:14 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Num 3)))) ; theorem :: GLIB_001:15 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))) ; theorem :: GLIB_001:16 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k4_glib_001 :::".last()"::: ) )) ")" )))) ; theorem :: GLIB_001:17 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool "(" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" )))) ; theorem :: GLIB_001:18 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))) ")" )))) ; theorem :: GLIB_001:19 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" ))))) ; theorem :: GLIB_001:20 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "W1")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n")))))))) ; theorem :: GLIB_001:21 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ))) ")" ))) ; theorem :: GLIB_001:22 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k4_glib_001 :::".last()"::: ) )) & (Bool (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k3_glib_001 :::".first()"::: ) )) ")" ))) ; theorem :: GLIB_001:23 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "y")) "," (Set (Var "x"))) ")" )))) ; theorem :: GLIB_001:24 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ))) ")" )))) ; theorem :: GLIB_001:25 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" )))) ; theorem :: GLIB_001:26 canceled; theorem :: GLIB_001:27 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k6_glib_001 :::".reverse()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k6_glib_001 :::".reverse()"::: ) ))))) ; theorem :: GLIB_001:28 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")) ")" ))))) ; theorem :: GLIB_001:29 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ))) ")" ))) ; theorem :: GLIB_001:30 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k4_glib_001 :::".last()"::: ) )) & (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) "," (Set (Set (Var "W2")) ($#k4_glib_001 :::".last()"::: ) )) ")" ))) ; theorem :: GLIB_001:31 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "y")) "," (Set (Var "z")))) "holds" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "z")))))) ; theorem :: GLIB_001:32 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W1"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ))) ")" )))) ; theorem :: GLIB_001:33 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ))) ")" )))) ; theorem :: GLIB_001:34 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ))) "or" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W1")))) "or" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))) & (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))) ")" )) ")" )))) ; theorem :: GLIB_001:35 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1A")) "," (Set (Var "W1B")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2A")) "," (Set (Var "W2B")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1A")) ($#r1_hidden :::"="::: ) (Set (Var "W2A"))) & (Bool (Set (Var "W1B")) ($#r1_hidden :::"="::: ) (Set (Var "W2B")))) "holds" (Bool (Set (Set (Var "W1A")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W1B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2A")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2B"))))))) ; theorem :: GLIB_001:36 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" ) ")" ) ")" )))) ; theorem :: GLIB_001:37 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) & (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" )))) ; theorem :: GLIB_001:38 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "o")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "o"))) & (Bool (Set (Var "o")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k7_glib_001 :::".append"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "n")) "," (Set (Var "o")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "o")) ")" ))))) ; theorem :: GLIB_001:39 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "W"))))) ; theorem :: GLIB_001:40 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "n")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))))) ; theorem :: GLIB_001:41 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k10_glib_001 :::".addEdge"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ) ")" ))))) ; theorem :: GLIB_001:42 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "n")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: GLIB_001:43 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) "is" ($#v1_abian :::"odd"::: ) ) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ")" ) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ))))) ; theorem :: GLIB_001:44 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1")))) & (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W1")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))))) ; theorem :: GLIB_001:45 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m")))))) ; theorem :: GLIB_001:46 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ")" ))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: GLIB_001:47 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" ))))) ; theorem :: GLIB_001:48 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )))))) ; theorem :: GLIB_001:49 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m"))))))) ; theorem :: GLIB_001:50 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y")))) "holds" (Bool (Set (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))))))) ; theorem :: GLIB_001:51 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))))) ; theorem :: GLIB_001:52 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "m")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "W")))))) ; theorem :: GLIB_001:53 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "n")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ))))) ; theorem :: GLIB_001:54 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: GLIB_001:55 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "m")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ))))) ; theorem :: GLIB_001:56 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "n"))))))) ; theorem :: GLIB_001:57 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ))) "holds" (Bool (Set (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ))))) ; theorem :: GLIB_001:58 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))))) "holds" (Bool (Set (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Num 1) "," (Set (Var "m")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ")" ))))) ; theorem :: GLIB_001:59 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) )) ")" )))) ; theorem :: GLIB_001:60 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))))) "holds" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ))) ")" ))))) ; theorem :: GLIB_001:61 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k20_glib_001 :::".remove"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )))))) ; theorem :: GLIB_001:62 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "e")) "," (Set (Var "x")) ($#k10_finseq_1 :::"*>"::: ) )))))) ; theorem :: GLIB_001:63 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) "," (Set (Var "x"))) ")" )))) ; theorem :: GLIB_001:64 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: GLIB_001:65 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ) ")" )))) ; theorem :: GLIB_001:66 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "z")))))) ; theorem :: GLIB_001:67 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ))))) ; theorem :: GLIB_001:68 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_nat_d :::"div"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_nat_d :::"div"::: ) (Num 2))) & (Bool (Set (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_nat_d :::"div"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ))) ")" )))) ; theorem :: GLIB_001:69 (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 "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" ) ($#k11_glib_001 :::".vertexSeq()"::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: GLIB_001:70 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k11_glib_001 :::".vertexSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )))) ; theorem :: GLIB_001:71 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ) ")" ))) ")" ))) ; theorem :: GLIB_001:72 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_nat_d :::"div"::: ) (Num 2) ")" )))))) ; theorem :: GLIB_001:73 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ))) "iff" (Bool (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" )))) ; theorem :: GLIB_001:74 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ")" ) ($#k11_glib_001 :::".vertexSeq()"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ))))) ; theorem :: GLIB_001:75 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k11_glib_001 :::".vertexSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )))))) ; theorem :: GLIB_001:76 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k11_glib_001 :::".vertexSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k11_glib_001 :::".vertexSeq()"::: ) ))))) ; theorem :: GLIB_001:77 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#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 "W"))))) "holds" (Bool "(" (Bool (Set (Set (Var "n")) ($#k3_nat_d :::"div"::: ) (Num 2)) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k3_nat_d :::"div"::: ) (Num 2) ")" ))) ")" )))) ; theorem :: GLIB_001:78 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) "iff" (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "W")))) ")" )))) ; theorem :: GLIB_001:79 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k7_glib_000 :::"the_Edges_of"::: ) (Set (Var "G"))))))) ; theorem :: GLIB_001:80 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "ex" (Set (Var "lenWaa1")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "lenWaa1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "lenWaa1")) ($#k3_nat_d :::"div"::: ) (Num 2))) ")" )))) ; theorem :: GLIB_001:81 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ")" ) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ))))) ; theorem :: GLIB_001:82 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) )))))) ; theorem :: GLIB_001:83 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "iff" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) )) ")" ))) ; theorem :: GLIB_001:84 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r2_relset_1 :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))))) ; theorem :: GLIB_001:85 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "W2")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))))) ; theorem :: GLIB_001:86 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k12_glib_001 :::".edgeSeq()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k12_glib_001 :::".edgeSeq()"::: ) ))))) ; theorem :: GLIB_001:87 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ")" )))) ; theorem :: GLIB_001:88 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) & (Bool (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) ")" ))) ; theorem :: GLIB_001:89 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k5_glib_001 :::".vertexAt"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))))) ; theorem :: GLIB_001:90 (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 "(" (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v")) ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: GLIB_001:91 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )))) ; theorem :: GLIB_001:92 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k13_glib_001 :::".vertices()"::: ) )))) ; theorem :: GLIB_001:93 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "W2")) ($#k13_glib_001 :::".vertices()"::: ) ")" ))))) ; theorem :: GLIB_001:94 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))))) ; theorem :: GLIB_001:95 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: GLIB_001:96 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k13_glib_001 :::".vertices()"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: GLIB_001:97 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) "holds" (Bool "ex" (Set (Var "W9")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Set (Var "W9")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))))))) ; theorem :: GLIB_001:98 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k13_glib_001 :::".vertices()"::: ) ))))) ; theorem :: GLIB_001:99 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#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 "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )) ")" )))) ; theorem :: GLIB_001:100 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )) ")" )))) ; theorem :: GLIB_001:101 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ")" ))))) ; theorem :: GLIB_001:102 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2")) ")" ) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) ")" ))))) ; theorem :: GLIB_001:103 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ))) "holds" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" ))) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "G"))) ")" )))))) ; theorem :: GLIB_001:104 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ))) & (Bool (Set (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" )) ")" )))) ; theorem :: GLIB_001:105 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )) & (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) ")" )))) ; theorem :: GLIB_001:106 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ")" ) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ))))) ; theorem :: GLIB_001:107 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ")" ) ($#k14_glib_001 :::".edges()"::: ) )))) ; theorem :: GLIB_001:108 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) "iff" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ")" ) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: GLIB_001:109 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "G")) ($#k21_glib_000 :::".edgesBetween"::: ) (Set "(" (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ")" ))))) ; theorem :: GLIB_001:110 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) ))))) ; theorem :: GLIB_001:111 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e")) ")" ) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: GLIB_001:112 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set "(" (Set (Var "W")) ($#k15_glib_001 :::".length()"::: ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GLIB_001:113 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))) "iff" (Bool (Set (Set (Var "W1")) ($#k15_glib_001 :::".length()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k15_glib_001 :::".length()"::: ) )) ")" ))) ; theorem :: GLIB_001:114 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k15_glib_001 :::".length()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k15_glib_001 :::".length()"::: ) ))))) ; theorem :: GLIB_001:115 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k16_glib_001 :::".find"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "W")) ($#k18_glib_001 :::".rfind"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) ")" )))) ; theorem :: GLIB_001:116 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k16_glib_001 :::".find"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k16_glib_001 :::".find"::: ) (Set (Var "v")))) & (Bool (Set (Set (Var "W1")) ($#k18_glib_001 :::".rfind"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k18_glib_001 :::".rfind"::: ) (Set (Var "v")))) ")" ))))) ; theorem :: GLIB_001:117 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k17_glib_001 :::".find"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "W")) ($#k19_glib_001 :::".rfind"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Var "n"))) ")" )))) ; theorem :: GLIB_001:118 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ))) ")" ))) ; theorem :: GLIB_001:119 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "x")))) ")" ))) ; theorem :: GLIB_001:120 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) "is" ($#v1_glib_001 :::"closed"::: ) ) ")" ))) ; theorem :: GLIB_001:121 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) & (Bool (Set (Var "W1")) "is" ($#v1_glib_001 :::"closed"::: ) )) "holds" (Bool (Set (Var "W2")) "is" ($#v1_glib_001 :::"closed"::: ) )))) ; theorem :: GLIB_001:122 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v2_glib_001 :::"directed"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_glib_000 :::"DJoins"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) "," (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) "," (Set (Var "G")))) ")" ))) ; theorem :: GLIB_001:123 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W")) "is" ($#v2_glib_001 :::"directed"::: ) ) & (Bool (Set (Var "W")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Set (Var "e")) ($#r2_glib_000 :::"DJoins"::: ) (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "G")))) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v2_glib_001 :::"directed"::: ) ) & (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "z"))) ")" )))) ; theorem :: GLIB_001:124 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"DWalk":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v2_glib_001 :::"directed"::: ) )))) ; theorem :: GLIB_001:125 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "iff" (Bool (Num 3) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) ")" ))) ; theorem :: GLIB_001:126 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "iff" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_hidden :::"<>"::: ) (Num 1)) ")" ))) ; theorem :: GLIB_001:127 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )))) ; theorem :: GLIB_001:128 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Set (Var "W")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k1_glib_001 :::".walkOf"::: ) (Set (Var "v"))))) ")" ))) ; theorem :: GLIB_001:129 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) "is" ($#v3_glib_001 :::"trivial"::: ) ) ")" ))) ; theorem :: GLIB_001:130 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "holds" (Bool (Set (Set (Var "W1")) ($#k7_glib_001 :::".append"::: ) (Set (Var "W2"))) ($#r2_relset_1 :::"="::: ) (Set (Var "W1"))))) ; theorem :: GLIB_001:131 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v3_glib_001 :::"trivial"::: ) ) "iff" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )))) ; theorem :: GLIB_001:132 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool "not" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v3_glib_001 :::"trivial"::: ) ))))) ; theorem :: GLIB_001:133 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "holds" (Bool "ex" (Set (Var "lenW2")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "lenW2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 2))) & (Bool (Set (Set "(" (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Num 1) "," (Set (Var "lenW2")) ")" ")" ) ($#k10_glib_001 :::".addEdge"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "lenW2")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "W"))) ")" )))) ; theorem :: GLIB_001:134 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W2")) "," (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) )) & (Bool (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ))) "holds" (Bool (Set (Set (Var "W2")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W1")) ($#k13_glib_001 :::".vertices()"::: ) )))) ; theorem :: GLIB_001:135 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "v")) "is" ($#v10_glib_000 :::"isolated"::: ) ))))) ; theorem :: GLIB_001:136 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: GLIB_001:137 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) & (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "holds" (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) )))) ; theorem :: GLIB_001:138 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) "iff" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) ")" ))) ; theorem :: GLIB_001:139 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<="::: ) (Num 3))) "holds" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ))) ; theorem :: GLIB_001:140 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) ")" ))) ; theorem :: GLIB_001:141 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v4_glib_001 :::"Trail-like"::: ) )))) ; theorem :: GLIB_001:142 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) )) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v4_glib_001 :::"Trail-like"::: ) )))) ; theorem :: GLIB_001:143 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )) & (Bool (Set (Var "v")) "is" ($#v11_glib_000 :::"endvertex"::: ) ) & (Bool (Bool "not" (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) )))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ))))) ; theorem :: GLIB_001:144 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k12_glib_001 :::".edgeSeq()"::: ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "G")) ($#k17_glib_000 :::".size()"::: ) )))) ; theorem :: GLIB_001:145 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))) ($#r1_xxreal_0 :::"<="::: ) (Num 3))) "holds" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: GLIB_001:146 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W")))) & (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: GLIB_001:147 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))))) ; theorem :: GLIB_001:148 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) "iff" (Bool (Set (Set (Var "W")) ($#k6_glib_001 :::".reverse()"::: ) ) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" ))) ; theorem :: GLIB_001:149 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "W")) ($#k8_glib_001 :::".cut"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) "is" ($#v5_glib_001 :::"Path-like"::: ) )))) ; theorem :: GLIB_001:150 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "v")) "," (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ))) & (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "or" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"open"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#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 "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Var "v"))) ")" )) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v5_glib_001 :::"Path-like"::: ) )))) ; theorem :: GLIB_001:151 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "v")) "," (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ))) & (Bool "(" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) "or" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"open"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v5_glib_001 :::"Path-like"::: ) )))) ; theorem :: GLIB_001:152 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k16_glib_001 :::".find"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k18_glib_001 :::".rfind"::: ) (Set "(" (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" )) "holds" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: GLIB_001:153 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W"))))) "holds" (Bool (Set (Set (Var "W")) ($#k19_glib_001 :::".rfind"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ))) ; theorem :: GLIB_001:154 (Bool "for" (Set (Var "G")) "being" ($#v2_glib_000 :::"finite"::: ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Path":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" (Set (Var "W")) ($#k11_glib_001 :::".vertexSeq()"::: ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "G")) ($#k15_glib_000 :::".order()"::: ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: GLIB_001:155 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#v6_glib_001 :::"vertex-distinct"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Set (Var "W")) ($#k4_glib_001 :::".last()"::: ) ) "," (Set (Var "v")) "," (Set (Var "G"))) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )))) "holds" (Bool (Set (Set (Var "W")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )))) ; theorem :: GLIB_001:156 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "x")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "G")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "x")) ")" ) "is" ($#v8_glib_001 :::"Cycle-like"::: ) ))) ; theorem :: GLIB_001:157 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "e")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) )) & (Bool (Set (Var "W1")) "is" ($#v8_glib_001 :::"Cycle-like"::: ) )) "holds" (Bool "ex" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) ))) ")" ))))) ; theorem :: GLIB_001:158 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "holds" (Bool (Set (Var "W")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W"))))) ; theorem :: GLIB_001:159 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W2")) "being" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W1")) (Bool "for" (Set (Var "W3")) "being" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")) "holds" (Bool (Set (Var "W3")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W1"))))))) ; theorem :: GLIB_001:160 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Var "W1")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) "iff" (Bool (Set (Var "W2")) ($#r1_glib_001 :::"is_Walk_from"::: ) (Set (Var "x")) "," (Set (Var "y"))) ")" )))) ; theorem :: GLIB_001:161 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k3_glib_001 :::".first()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k3_glib_001 :::".first()"::: ) )) & (Bool (Set (Set (Var "W1")) ($#k4_glib_001 :::".last()"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k4_glib_001 :::".last()"::: ) )) ")" ))) ; theorem :: GLIB_001:162 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))))) ; theorem :: GLIB_001:163 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool "(" (Bool (Set (Set (Var "W1")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W2")) ($#k14_glib_001 :::".edges()"::: ) )) & (Bool (Set (Set (Var "W1")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Set (Var "W2")) ($#k13_glib_001 :::".vertices()"::: ) )) ")" ))) ; theorem :: GLIB_001:164 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1"))))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"odd"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ))))) ; theorem :: GLIB_001:165 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W1")) "is" ($#m4_glib_001 :::"Subwalk"::: ) "of" (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "m")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W1"))))) "holds" (Bool "ex" (Set (Var "n")) "being" ($#v1_abian :::"even"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "W2")))) & (Bool (Set (Set (Var "W1")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) ")" ))))) ; theorem :: GLIB_001:166 (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Trail":::) "of" (Set (Var "G")) "st" (Bool (Bool (Bool "not" (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) ))) "holds" (Bool "ex" (Set (Var "W2")) "being" ($#m4_glib_001 :::"Path":::) "of" (Set (Var "W1")) "st" (Bool (Bool "not" (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) ))))) ; theorem :: GLIB_001:167 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")))))) ; theorem :: GLIB_001:168 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ) & (Bool (Set (Set (Var "W")) ($#k3_glib_001 :::".first()"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")))))) ; theorem :: GLIB_001:169 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Bool "not" (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) & (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")))))) ; theorem :: GLIB_001:170 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k24_glib_000 :::"the_Vertices_of"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k25_glib_000 :::"the_Edges_of"::: ) (Set (Var "G2"))))) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")))))) ; theorem :: GLIB_001:171 (Bool "for" (Set (Var "G1")) "being" ($#~v4_glib_000 "non" ($#v4_glib_000 :::"trivial"::: ) ) ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (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 (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k13_glib_001 :::".vertices()"::: ) )))) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2"))))))) ; theorem :: GLIB_001:172 (Bool "for" (Set (Var "G1")) "being" ($#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 (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "W")) ($#k14_glib_001 :::".edges()"::: ) )))) "holds" (Bool (Set (Var "W")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2"))))))) ; theorem :: GLIB_001:173 (Bool "for" (Set (Var "G1")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "G2")) "being" ($#m1_glib_000 :::"Subgraph"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r1_glib_000 :::"Joins"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ))))) ; theorem :: GLIB_001:174 (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 "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "W2")) ($#k4_glib_001 :::".last()"::: ) ")" ) ($#k28_glib_000 :::".edgesInOut()"::: ) ))) "holds" (Bool (Set (Set (Var "W1")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W2")) ($#k10_glib_001 :::".addEdge"::: ) (Set (Var "e"))))))))) ; theorem :: GLIB_001:175 (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 "W")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v1_glib_001 :::"closed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v2_glib_001 :::"directed"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v2_glib_001 :::"directed"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v3_glib_001 :::"trivial"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v5_glib_001 :::"Path-like"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" & "(" (Bool (Bool (Set (Var "W")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )) "implies" (Bool (Set (Var "W")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1"))) ")" ")" )))) ; theorem :: GLIB_001:176 (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 "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "W1")) "is" ($#v1_glib_001 :::"closed"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v1_glib_001 :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v1_glib_001 :::"closed"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v1_glib_001 :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v2_glib_001 :::"directed"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v2_glib_001 :::"directed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v2_glib_001 :::"directed"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v2_glib_001 :::"directed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v4_glib_001 :::"Trail-like"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v4_glib_001 :::"Trail-like"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v5_glib_001 :::"Path-like"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v5_glib_001 :::"Path-like"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ) ")" ")" ))))) ; theorem :: GLIB_001:177 (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 "x")) "is" ($#m1_glib_001 :::"VertexSeq"::: ) "of" (Set (Var "G1")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_glib_001 :::"VertexSeq"::: ) "of" (Set (Var "G2"))))) ; theorem :: GLIB_001:178 (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 "x")) "is" ($#m2_glib_001 :::"EdgeSeq"::: ) "of" (Set (Var "G1")))) "holds" (Bool (Set (Var "x")) "is" ($#m2_glib_001 :::"EdgeSeq"::: ) "of" (Set (Var "G2"))))) ; theorem :: GLIB_001:179 (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 "x")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")))) "holds" (Bool (Set (Var "x")) "is" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2"))))) ; theorem :: GLIB_001:180 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G2")) ($#k2_glib_001 :::".walkOf"::: ) "(" (Set (Var "x")) "," (Set (Var "e")) "," (Set (Var "y")) ")" )))) ; theorem :: GLIB_001:181 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"_Graph":::) (Bool "for" (Set (Var "W1")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G1")) (Bool "for" (Set (Var "W2")) "being" ($#m3_glib_001 :::"Walk"::: ) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r5_glib_000 :::"=="::: ) (Set (Var "G2"))) & (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "W2")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "W1")) "is" ($#v1_glib_001 :::"closed"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v1_glib_001 :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v1_glib_001 :::"closed"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v1_glib_001 :::"closed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v2_glib_001 :::"directed"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v2_glib_001 :::"directed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v2_glib_001 :::"directed"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v2_glib_001 :::"directed"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v3_glib_001 :::"trivial"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v3_glib_001 :::"trivial"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v4_glib_001 :::"Trail-like"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v4_glib_001 :::"Trail-like"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v4_glib_001 :::"Trail-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v5_glib_001 :::"Path-like"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v5_glib_001 :::"Path-like"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v5_glib_001 :::"Path-like"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W1")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )) "implies" (Bool (Set (Var "W2")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ) ")" & "(" (Bool (Bool (Set (Var "W2")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) )) "implies" (Bool (Set (Var "W1")) "is" ($#v6_glib_001 :::"vertex-distinct"::: ) ) ")" ")" )))) ;