:: MYCIELSK semantic presentation begin begin theorem :: MYCIELSK:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_xreal_0 :::"-'"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_xreal_0 :::"-'"::: ) (Set "(" (Set (Var "x")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" )))) ; theorem :: MYCIELSK:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set (Var "z")))) "iff" (Bool "(" (Bool (Set (Var "z")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "y"))) ")" ) ")" )) ; theorem :: MYCIELSK:3 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) "or" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "E"))) ")" )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "D")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "E"))))) ; theorem :: MYCIELSK:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "C")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "D")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "E")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) ")" ) ")" )) ; theorem :: MYCIELSK:5 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))))) ; theorem :: MYCIELSK:6 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))))) ; begin theorem :: MYCIELSK:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "P"))) ($#r1_ordinal1 :::"c="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); func "P" :::"|"::: "S" -> ($#m1_eqrel_1 :::"a_partition"::: ) "of" "S" equals :: MYCIELSK:def 1 "{" (Set "(" (Set (Var "x")) ($#k9_subset_1 :::"/\"::: ) "S" ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" "P" : (Bool (Set (Var "x")) ($#r1_xboole_0 :::"meets"::: ) "S") "}" ; end; :: deftheorem defines :::"|"::: MYCIELSK:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "P")) ($#k1_mycielsk :::"|"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "x")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "P")) : (Bool (Set (Var "x")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S"))) "}" )))); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) bbbadV1_SETFAM_1() for ($#m1_eqrel_1 :::"a_partition"::: ) "of" "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "P" be ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Const "X")); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set "P" ($#k1_mycielsk :::"|"::: ) "S") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: MYCIELSK:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "P")) ($#k1_mycielsk :::"|"::: ) (Set (Var "S")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "P"))))))) ; theorem :: MYCIELSK:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "P")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "p")) ($#r1_xboole_0 :::"meets"::: ) (Set (Var "S"))) ")" ) "iff" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "P")) ($#k1_mycielsk :::"|"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "P")))) ")" )))) ; theorem :: MYCIELSK:10 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "C")) ($#k1_mycielsk :::"|"::: ) (Set (Var "S"))) "is" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"with_finite_chromatic#"::: means :: MYCIELSK:def 2 (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" "R" "st" (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"with_finite_chromatic#"::: MYCIELSK:def 2 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); registration cluster ($#v1_mycielsk :::"with_finite_chromatic#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v1_mycielsk :::"with_finite_chromatic#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "R" be ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) bbbadV1_SETFAM_1() ($#v6_dilworth :::"StableSet-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; registrationlet "R" be ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ; end; definitionlet "R" be ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"chromatic#"::: "R" -> ($#m1_hidden :::"Nat":::) means :: MYCIELSK:def 3 (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Coloring":::) "of" "R" "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) it)) & (Bool "(" "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Coloring":::) "of" "R" "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" ) ")" ); end; :: deftheorem defines :::"chromatic#"::: MYCIELSK:def 3 : (Bool "for" (Set (Var "R")) "being" ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" ) ")" ) ")" ))); registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_mycielsk :::"chromatic#"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_mycielsk :::"chromatic#"::: ) "R") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"with_finite_cliquecover#"::: means :: MYCIELSK:def 4 (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" "R" "st" (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )); end; :: deftheorem defines :::"with_finite_cliquecover#"::: MYCIELSK:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )) ")" )); registration cluster ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "R" be ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) bbbadV1_SETFAM_1() ($#v5_dilworth :::"Clique-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; registrationlet "R" be ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ; end; definitionlet "R" be ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"cliquecover#"::: "R" -> ($#m1_hidden :::"Nat":::) means :: MYCIELSK:def 5 (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Clique-partition":::) "of" "R" "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) it)) & (Bool "(" "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Clique-partition":::) "of" "R" "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" ) ")" ); end; :: deftheorem defines :::"cliquecover#"::: MYCIELSK:def 5 : (Bool "for" (Set (Var "R")) "being" ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))) ")" ) ")" ) ")" ))); registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_mycielsk :::"cliquecover#"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_mycielsk :::"cliquecover#"::: ) "R") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: MYCIELSK:11 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: MYCIELSK:12 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: MYCIELSK:13 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: MYCIELSK:14 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))))) ; theorem :: MYCIELSK:15 (Bool "for" (Set (Var "R")) "being" ($#v3_dilworth :::"with_finite_clique#"::: ) ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))))) ; theorem :: MYCIELSK:16 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set (Var "R"))))) ; begin theorem :: MYCIELSK:17 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))))) ; theorem :: MYCIELSK:18 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))))) ; registrationlet "R" be ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v8_struct_0 :::"finite"::: ) ; end; theorem :: MYCIELSK:19 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "C")) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:20 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "C")) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R"))))) ; theorem :: MYCIELSK:21 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "C")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:22 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "C")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R"))))) ; registrationlet "R" be ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v4_dilworth :::"with_finite_stability#"::: ) ; end; registrationlet "R" be ($#v1_necklace :::"symmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v3_dilworth :::"with_finite_clique#"::: ) ; end; theorem :: MYCIELSK:23 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:24 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:25 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "C")) "is" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:26 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "C")) "is" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R"))))) ; theorem :: MYCIELSK:27 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "C")) "is" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:28 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" ) "holds" (Bool (Set (Var "C")) "is" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R"))))) ; registrationlet "R" be ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ; end; registrationlet "R" be ($#v1_necklace :::"symmetric"::: ) ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k3_necklace :::"ComplRelStr"::: ) "R") -> ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ; end; theorem :: MYCIELSK:29 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; theorem :: MYCIELSK:30 (Bool "for" (Set (Var "R")) "being" ($#v1_necklace :::"symmetric"::: ) ($#v2_mycielsk :::"with_finite_cliquecover#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set "(" ($#k3_necklace :::"ComplRelStr"::: ) (Set (Var "R")) ")" )))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"Adjacent"::: "v" -> ($#m1_subset_1 :::"Subset":::) "of" "R" means :: MYCIELSK:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_orders_2 :::"<"::: ) "v") "or" (Bool "v" ($#r2_orders_2 :::"<"::: ) (Set (Var "x"))) ")" ) ")" )); end; :: deftheorem defines :::"Adjacent"::: MYCIELSK:def 6 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_mycielsk :::"Adjacent"::: ) (Set (Var "v")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_orders_2 :::"<"::: ) (Set (Var "v"))) "or" (Bool (Set (Var "v")) ($#r2_orders_2 :::"<"::: ) (Set (Var "x"))) ")" ) ")" )) ")" )))); theorem :: MYCIELSK:31 (Bool "for" (Set (Var "R")) "being" ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k4_mycielsk :::"Adjacent"::: ) (Set (Var "v")))) & (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Var "d"))) ")" )) ")" ) ")" ))))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); mode :::"NatRelStr"::: "of" "n" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) means :: MYCIELSK:def 7 (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "n"); end; :: deftheorem defines :::"NatRelStr"::: MYCIELSK:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n"))) "iff" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ))); registration cluster -> ($#v2_struct_0 :::"empty"::: ) for ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set ($#k6_numbers :::"0"::: ) ); end; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); cluster -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#m1_mycielsk :::"NatRelStr"::: ) "of" "n"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> ($#v8_struct_0 :::"finite"::: ) for ($#m1_mycielsk :::"NatRelStr"::: ) "of" "n"; cluster ($#v1_orders_2 :::"strict"::: ) ($#v3_necklace :::"irreflexive"::: ) for ($#m1_mycielsk :::"NatRelStr"::: ) "of" "n"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"CompleteRelStr"::: "n" -> ($#m1_mycielsk :::"NatRelStr"::: ) "of" "n" means :: MYCIELSK:def 8 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) "n" "," "n" ($#k2_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) "n" ")" ))); end; :: deftheorem defines :::"CompleteRelStr"::: MYCIELSK:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")))) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "n")) "," (Set (Var "n")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "n")) ")" ))) ")" ))); theorem :: MYCIELSK:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")) ")" ))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y"))) ")" ))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k5_mycielsk :::"CompleteRelStr"::: ) "n") -> ($#v1_necklace :::"symmetric"::: ) ($#v3_necklace :::"irreflexive"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k2_struct_0 :::"[#]"::: ) (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) "n" ")" )) -> ($#v1_dilworth :::"clique"::: ) ; end; theorem :: MYCIELSK:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: MYCIELSK:34 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: MYCIELSK:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))) ; theorem :: MYCIELSK:36 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set "(" ($#k5_mycielsk :::"CompleteRelStr"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin definitionlet "n" be ($#m1_hidden :::"Nat":::); let "R" be ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Const "n")); func :::"Mycielskian"::: "R" -> ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) means :: MYCIELSK:def 9 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) "n" ")" ) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) "n" ")" ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" ) ($#k6_subset_1 :::"\"::: ) "n" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" ) ($#k6_subset_1 :::"\"::: ) "n" ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))); end; :: deftheorem defines :::"Mycielskian"::: MYCIELSK:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "b3")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")))) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "n")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" )))); theorem :: MYCIELSK:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))))) ; theorem :: MYCIELSK:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) ")" ) "or" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) ")" ) "or" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")))) ")" ) ")" )))) ; theorem :: MYCIELSK:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) "holds" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))))) ; theorem :: MYCIELSK:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))))) ; theorem :: MYCIELSK:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))) ")" )))) ; theorem :: MYCIELSK:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))))) ; theorem :: MYCIELSK:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" )))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))))) ; theorem :: MYCIELSK:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "m")) "," (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "n")) ")" ) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))) ")" )))) ; theorem :: MYCIELSK:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S"))))))) ; theorem :: MYCIELSK:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#v3_necklace :::"irreflexive"::: ) ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" ))))) ; theorem :: MYCIELSK:47 (Bool "for" (Set (Var "R")) "being" ($#v1_mycielsk :::"with_finite_chromatic#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ))))) ; theorem :: MYCIELSK:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#v3_necklace :::"irreflexive"::: ) ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Var "n")) "holds" (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set "(" ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R")) ")" ))))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"Mycielskian"::: "n" -> ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) "n" ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) means :: MYCIELSK:def 10 (Bool "ex" (Set (Var "myc")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) "n")) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "myc"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_mycielsk :::"CompleteRelStr"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R"))))) ")" ) ")" )); end; :: deftheorem defines :::"Mycielskian"::: MYCIELSK:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "n")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_mycielsk :::"Mycielskian"::: ) (Set (Var "n")))) "iff" (Bool "ex" (Set (Var "myc")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "myc"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_mycielsk :::"CompleteRelStr"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "R")) "being" ($#m1_mycielsk :::"NatRelStr"::: ) "of" (Set (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 2) ($#k2_newton :::"|^"::: ) (Set (Var "k")) ")" ) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1)) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "myc")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_mycielsk :::"Mycielskian"::: ) (Set (Var "R"))))) ")" ) ")" )) ")" ))); theorem :: MYCIELSK:49 (Bool "(" (Bool (Set ($#k7_mycielsk :::"Mycielskian"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_mycielsk :::"CompleteRelStr"::: ) (Num 2))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_mycielsk :::"Mycielskian"::: ) (Set "(" (Set (Var "k")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_mycielsk :::"Mycielskian"::: ) (Set "(" ($#k7_mycielsk :::"Mycielskian"::: ) (Set (Var "k")) ")" ))) ")" ) ")" ) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_mycielsk :::"Mycielskian"::: ) "n") -> ($#v3_necklace :::"irreflexive"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k7_mycielsk :::"Mycielskian"::: ) "n") -> ($#v1_necklace :::"symmetric"::: ) ; end; theorem :: MYCIELSK:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k7_mycielsk :::"Mycielskian"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set "(" ($#k7_mycielsk :::"Mycielskian"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 2))) ")" )) ; theorem :: MYCIELSK:51 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k2_mycielsk :::"chromatic#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) ")" ))) ; theorem :: MYCIELSK:52 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool "(" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set ($#k3_mycielsk :::"cliquecover#"::: ) (Set (Var "R"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) ")" ))) ;