:: SGRAPH1 semantic presentation begin definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); func :::"nat_interval"::: "(" "m" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SGRAPH1:def 1 "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool "m" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n") ")" ) "}" ; end; :: deftheorem defines :::"nat_interval"::: SGRAPH1:def 1 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) "}" )); notationlet "m", "n" be ($#m1_hidden :::"Nat":::); synonym :::"Seg"::: "(" "m" "," "n" ")" for :::"nat_interval"::: "(" "m" "," "n" ")" ; end; registrationlet "m", "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" "m" "," "n" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: SGRAPH1:1 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) ")" ))) ; theorem :: SGRAPH1:2 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" )) ; theorem :: SGRAPH1:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Num 1) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) ; theorem :: SGRAPH1:4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) ; theorem :: SGRAPH1:5 (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "k"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ))) ; theorem :: SGRAPH1:6 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"TWOELEMENTSETS"::: "A" -> ($#m1_hidden :::"set"::: ) equals :: SGRAPH1:def 2 "{" (Set (Var "z")) where z "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "A" : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 2)) "}" ; end; :: deftheorem defines :::"TWOELEMENTSETS"::: SGRAPH1:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "z")) where z "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 2)) "}" )); theorem :: SGRAPH1:7 (Bool "for" (Set (Var "A")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A")))) "iff" (Bool "ex" (Set (Var "z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 2)) ")" )) ")" )) ; theorem :: SGRAPH1:8 (Bool "for" (Set (Var "A")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set (Var "e")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A"))) & (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )) ")" )) ")" ) ")" )) ; theorem :: SGRAPH1:9 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "A"))))) ; theorem :: SGRAPH1:10 (Bool "for" (Set (Var "A")) "," (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "e1")) "," (Set (Var "e2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "e1")) ($#r1_hidden :::"<>"::: ) (Set (Var "e2"))) ")" )) ; theorem :: SGRAPH1:11 (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: SGRAPH1:12 (Bool "for" (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r1_tarski :::"c="::: ) (Set (Var "u")))) "holds" (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "t"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "u"))))) ; theorem :: SGRAPH1:13 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A"))) "is" ($#v1_finset_1 :::"finite"::: ) )) ; theorem :: SGRAPH1:14 (Bool "for" (Set (Var "A")) "being" ($#~v1_zfmisc_1 "non" ($#v1_zfmisc_1 :::"trivial"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "A"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))) ; theorem :: SGRAPH1:15 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"SimpleGraphStruct"::: -> ($#l1_struct_0 :::"1-sorted"::: ) ; aggr :::"SimpleGraphStruct":::(# :::"carrier":::, :::"SEdges"::: #) -> ($#l1_sgraph1 :::"SimpleGraphStruct"::: ) ; sel :::"SEdges"::: "c1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"SIMPLEGRAPHS"::: "X" -> ($#m1_hidden :::"set"::: ) equals :: SGRAPH1:def 3 "{" (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "v")) "," (Set (Var "e")) "#)" ) where v "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "X", e "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "v")) ")" ) : (Bool verum) "}" ; end; :: deftheorem defines :::"SIMPLEGRAPHS"::: SGRAPH1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) "{" (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "v")) "," (Set (Var "e")) "#)" ) where v "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")), e "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "v")) ")" ) : (Bool verum) "}" )); theorem :: SGRAPH1:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ")" ) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode :::"SimpleGraph"::: "of" "X" -> ($#v1_sgraph1 :::"strict"::: ) ($#l1_sgraph1 :::"SimpleGraphStruct"::: ) means :: SGRAPH1:def 4 (Bool it "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) "X")); end; :: deftheorem defines :::"SimpleGraph"::: SGRAPH1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v1_sgraph1 :::"strict"::: ) ($#l1_sgraph1 :::"SimpleGraphStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X"))) "iff" (Bool (Set (Var "b2")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X")))) ")" ))); theorem :: SGRAPH1:17 (Bool "for" (Set (Var "X")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))(Bool "ex" (Set (Var "e")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "v")) ")" ) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "v")) "," (Set (Var "e")) "#)" )))) ")" )) ; begin theorem :: SGRAPH1:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))))) ")" ))) ; theorem :: SGRAPH1:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) )) ")" ))))) ; theorem :: SGRAPH1:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) ")" )))) ; theorem :: SGRAPH1:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))) & (Bool (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ")" )) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "G", "G9" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); pred "G" :::"is_isomorphic_to"::: "G9" means :: SGRAPH1:def 5 (Bool "ex" (Set (Var "Fv")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G9") "st" (Bool "(" (Bool (Set (Var "Fv")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" "G")) "iff" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "Fv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set (Var "Fv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v2")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" "G")) ")" ) ")" ) ")" )); end; :: deftheorem defines :::"is_isomorphic_to"::: SGRAPH1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "G9")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_sgraph1 :::"is_isomorphic_to"::: ) (Set (Var "G9"))) "iff" (Bool "ex" (Set (Var "Fv")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G9"))) "st" (Bool "(" (Bool (Set (Var "Fv")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "G")))) "iff" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "Fv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v1")) ")" ) "," (Set "(" (Set (Var "Fv")) ($#k1_funct_1 :::"."::: ) (Set (Var "v2")) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "G")))) ")" ) ")" ) ")" )) ")" ))); begin scheme :: SGRAPH1:sch 1 IndSimpleGraphs0{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "G")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "G")) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set F1 "(" ")" )))) "holds" (Bool P1[(Set (Var "G"))])) provided (Bool P1[(Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ")" ) "#)" )]) and (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set F1 "(" ")" ))) & (Bool P1[(Set (Var "g"))]) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool (Bool "not" (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))))) "holds" (Bool P1[(Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ) "#)" )]))) and (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "g"))]) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))))) & (Bool (Bool "not" (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g")))))) "holds" (Bool "ex" (Set (Var "sege")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ")" ) "st" (Bool "(" (Bool (Set (Var "sege")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g"))) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "e")) ($#k1_tarski :::"}"::: ) ))) & (Bool P1[(Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) "," (Set (Var "sege")) "#)" )]) ")" )))) proof end; theorem :: SGRAPH1:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ")" ) "#)" )) "or" (Bool "ex" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "v")) ")" ) "st" (Bool "(" (Bool (Bool "not" (Set (Var "v")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "v")) "," (Set (Var "e")) "#)" )) ")" ))) ")" ))) ; theorem :: SGRAPH1:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Evn")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X")))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Evn")) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))))))))) ; theorem :: SGRAPH1:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "v1v2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "v1v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "v1v2")) "#)" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X")))) ")" )))))) ; definitionlet "X", "GG" be ($#m1_hidden :::"set"::: ) ; pred "GG" :::"is_SetOfSimpleGraphs_of"::: "X" means :: SGRAPH1:def 6 (Bool "(" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ")" ) "#)" ) ($#r2_hidden :::"in"::: ) "GG") & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Evn")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) "GG") & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Bool "not" (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Evn")) "#)" ) ($#r2_hidden :::"in"::: ) "GG")))) ")" ) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" "X" (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) "GG") & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Bool "not" (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) "holds" (Bool "ex" (Set (Var "v1v2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "v1v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "v1v2")) "#)" ) ($#r2_hidden :::"in"::: ) "GG") ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"is_SetOfSimpleGraphs_of"::: SGRAPH1:def 6 : (Bool "for" (Set (Var "X")) "," (Set (Var "GG")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "GG")) ($#r2_sgraph1 :::"is_SetOfSimpleGraphs_of"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ")" ) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "GG"))) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Evn")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "GG"))) & (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Bool "not" (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))))) "holds" (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "n")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set (Var "Evn")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "GG")))))) ")" ) & (Bool "(" "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "E")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "GG"))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Bool "not" (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E"))))) "holds" (Bool "ex" (Set (Var "v1v2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set (Var "V")) ")" ) "st" (Bool "(" (Bool (Set (Var "v1v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k2_tarski :::"}"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set (Var "V")) "," (Set (Var "v1v2")) "#)" ) ($#r2_hidden :::"in"::: ) (Set (Var "GG"))) ")" )))) ")" ) ")" ) ")" )); theorem :: SGRAPH1:25 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))) ($#r2_sgraph1 :::"is_SetOfSimpleGraphs_of"::: ) (Set (Var "X")))) ; theorem :: SGRAPH1:26 (Bool "for" (Set (Var "X")) "," (Set (Var "OTHER")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "OTHER")) ($#r2_sgraph1 :::"is_SetOfSimpleGraphs_of"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "OTHER")))) ; theorem :: SGRAPH1:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))) ($#r2_sgraph1 :::"is_SetOfSimpleGraphs_of"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "OTHER")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "OTHER")) ($#r2_sgraph1 :::"is_SetOfSimpleGraphs_of"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_sgraph1 :::"SIMPLEGRAPHS"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "OTHER"))) ")" ) ")" )) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); mode :::"SubGraph"::: "of" "G" -> ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" "X" means :: SGRAPH1:def 7 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) & (Bool (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" it) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" "G")) ")" ); end; :: deftheorem defines :::"SubGraph"::: SGRAPH1:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "," (Set (Var "b3")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_sgraph1 :::"SubGraph"::: ) "of" (Set (Var "G"))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "b3"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "G")))) ")" ) ")" ))); begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "G" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); let "v" be ($#m1_hidden :::"set"::: ) ; func :::"degree"::: "(" "G" "," "v" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SGRAPH1:def 8 (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" "G")) & (Bool "v" ($#r2_hidden :::"in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )); end; :: deftheorem defines :::"degree"::: SGRAPH1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k4_sgraph1 :::"degree"::: ) "(" (Set (Var "G")) "," (Set (Var "v")) ")" )) "iff" (Bool "ex" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "z"))) ")" ) ")" ) ")" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" )) ")" ))))); theorem :: SGRAPH1:28 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "ww")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "ww")) ($#r1_hidden :::"="::: ) "{" (Set (Var "w")) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) : (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "G")))) ")" ) "}" ) & (Bool (Set ($#k4_sgraph1 :::"degree"::: ) "(" (Set (Var "G")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "ww")))) ")" ))))) ; theorem :: SGRAPH1:29 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "VV")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "VV")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set ($#k4_sgraph1 :::"degree"::: ) "(" (Set (Var "g")) "," (Set (Var "v")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "VV")))) ")" ))))) ; theorem :: SGRAPH1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "," (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g")))) & (Bool (Set ($#k4_sgraph1 :::"degree"::: ) "(" (Set (Var "g")) "," (Set (Var "v")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "e"))))))) ; theorem :: SGRAPH1:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "vg")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "vg")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "vg"))) & (Bool (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k4_sgraph1 :::"degree"::: ) "(" (Set (Var "g")) "," (Set (Var "v")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "vg"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "vg")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "w")))) "holds" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g")))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_tarski :::"}"::: ) )) ")" ))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); let "v1", "v2" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "g")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "g"))); pred "p" :::"is_path_of"::: "v1" "," "v2" means :: SGRAPH1:def 9 (Bool "(" (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "v1") & (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" )) ($#r1_hidden :::"="::: ) "v2") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p"))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" "g")) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p"))) "holds" (Bool "(" (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_path_of"::: SGRAPH1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "g")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_sgraph1 :::"is_path_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "v1"))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v2"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set (Var "g")))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_tarski :::"}"::: ) )) ")" ) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); let "v1", "v2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "g"))); func :::"PATHS"::: "(" "v1" "," "v2" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "g") ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: SGRAPH1:def 10 "{" (Set (Var "ss")) where ss "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "g") ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set (Var "ss")) ($#r3_sgraph1 :::"is_path_of"::: ) "v1" "," "v2") "}" ; end; :: deftheorem defines :::"PATHS"::: SGRAPH1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) "holds" (Bool (Set ($#k5_sgraph1 :::"PATHS"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "ss")) where ss "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k3_finseq_2 :::"*"::: ) ) : (Bool (Set (Var "ss")) ($#r3_sgraph1 :::"is_path_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) "}" )))); theorem :: SGRAPH1:32 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k5_sgraph1 :::"PATHS"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) "iff" (Bool "ex" (Set (Var "ss")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set (Var "ss"))) & (Bool (Set (Var "ss")) ($#r3_sgraph1 :::"is_path_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" )) ")" ))))) ; theorem :: SGRAPH1:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) (Bool "for" (Set (Var "e")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "e")) ($#r3_sgraph1 :::"is_path_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k5_sgraph1 :::"PATHS"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "g" be ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Const "X")); let "p" be ($#m1_hidden :::"set"::: ) ; pred "p" :::"is_cycle_of"::: "g" means :: SGRAPH1:def 11 (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "g") "st" (Bool "p" ($#r2_hidden :::"in"::: ) (Set ($#k5_sgraph1 :::"PATHS"::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ))); end; :: deftheorem defines :::"is_cycle_of"::: SGRAPH1:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_sgraph1 :::"is_cycle_of"::: ) (Set (Var "g"))) "iff" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "g"))) "st" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k5_sgraph1 :::"PATHS"::: ) "(" (Set (Var "v")) "," (Set (Var "v")) ")" ))) ")" )))); begin definitionlet "n", "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"K_"::: "(" "m" "," "n" ")" -> ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SGRAPH1:def 12 (Bool "ex" (Set (Var "ee")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "m" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "ee")) ($#r1_hidden :::"="::: ) "{" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ) where i, j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "m")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set "(" "m" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" "m" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" )) ")" ) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" "m" ($#k2_nat_1 :::"+"::: ) "n" ")" ) ")" ) "," (Set (Var "ee")) "#)" )) ")" )); end; :: deftheorem defines :::"K_"::: SGRAPH1:def 12 : (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_sgraph1 :::"K_"::: ) "(" (Set (Var "m")) "," (Set (Var "n")) ")" )) "iff" (Bool "ex" (Set (Var "ee")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "ee")) ($#r1_hidden :::"="::: ) "{" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ) where i, j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "m")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k1_sgraph1 :::"nat_interval"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" )) ")" ) "}" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "ee")) "#)" )) ")" )) ")" ))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"K_"::: "n" -> ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SGRAPH1:def 13 (Bool "ex" (Set (Var "ee")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "ee")) ($#r1_hidden :::"="::: ) "{" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ) where i, j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n")) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n")) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) ")" ) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) "n" ")" ) "," (Set (Var "ee")) "#)" )) ")" )); end; :: deftheorem defines :::"K_"::: SGRAPH1:def 13 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_sgraph1 :::"K_"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "ee")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "ee")) ($#r1_hidden :::"="::: ) "{" (Set ($#k2_tarski :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k2_tarski :::"}"::: ) ) where i, j "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "j"))) ")" ) "}" ) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set (Var "ee")) "#)" )) ")" )) ")" ))); definitionfunc :::"TriangleGraph"::: -> ($#m1_sgraph1 :::"SimpleGraph"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: SGRAPH1:def 14 (Set ($#k7_sgraph1 :::"K_"::: ) (Num 3)); end; :: deftheorem defines :::"TriangleGraph"::: SGRAPH1:def 14 : (Bool (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_sgraph1 :::"K_"::: ) (Num 3))); theorem :: SGRAPH1:34 (Bool "ex" (Set (Var "ee")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_sgraph1 :::"TWOELEMENTSETS"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 3) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "ee")) ($#r1_hidden :::"="::: ) (Set ($#k4_setwiseo :::"{."::: ) (Set ($#k3_setwiseo :::"{."::: ) (Num 1) "," (Num 2) ($#k3_setwiseo :::".}"::: ) ) "," (Set ($#k3_setwiseo :::"{."::: ) (Num 2) "," (Num 3) ($#k3_setwiseo :::".}"::: ) ) "," (Set ($#k3_setwiseo :::"{."::: ) (Num 3) "," (Num 1) ($#k3_setwiseo :::".}"::: ) ) ($#k4_setwiseo :::".}"::: ) )) & (Bool (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_sgraph1 :::"SimpleGraphStruct"::: ) "(#" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Num 3) ")" ) "," (Set (Var "ee")) "#)" )) ")" )) ; theorem :: SGRAPH1:35 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Num 3))) & (Bool (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_setwiseo :::"{."::: ) (Set ($#k3_setwiseo :::"{."::: ) (Num 1) "," (Num 2) ($#k3_setwiseo :::".}"::: ) ) "," (Set ($#k3_setwiseo :::"{."::: ) (Num 2) "," (Num 3) ($#k3_setwiseo :::".}"::: ) ) "," (Set ($#k3_setwiseo :::"{."::: ) (Num 3) "," (Num 1) ($#k3_setwiseo :::".}"::: ) ) ($#k4_setwiseo :::".}"::: ) )) ")" ) ; theorem :: SGRAPH1:36 (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Num 1) "," (Num 2) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) ))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Num 2) "," (Num 3) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) ))) & (Bool (Set ($#k2_tarski :::"{"::: ) (Num 3) "," (Num 1) ($#k2_tarski :::"}"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_sgraph1 :::"SEdges"::: ) "of" (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) ))) ")" ) ; theorem :: SGRAPH1:37 (Bool (Set (Set "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 2) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 3) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r4_sgraph1 :::"is_cycle_of"::: ) (Set ($#k8_sgraph1 :::"TriangleGraph"::: ) )) ;