:: DILWORTH semantic presentation begin scheme :: DILWORTH:sch 1 FraenkelFinCard1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F2() -> ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool (Set ($#k5_card_1 :::"card"::: ) (Set F2 "(" ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set F1 "(" ")" ))) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set F3 "(" (Set (Var "w")) ")" ) where w "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "w"))]) "}" ) proof end; theorem :: DILWORTH:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))))) ; theorem :: DILWORTH:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "G"))) "is" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ))))) ; theorem :: DILWORTH:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "G")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "G"))) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))))))) ; theorem :: DILWORTH:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set (Var "X"))))) ; theorem :: DILWORTH:5 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "ex" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "S" is :::"connected"::: means :: DILWORTH:def 1 (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#r6_relat_2 :::"is_connected_in"::: ) "S"); end; :: deftheorem defines :::"connected"::: DILWORTH:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_dilworth :::"connected"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r6_relat_2 :::"is_connected_in"::: ) (Set (Var "S"))) ")" ))); notationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); synonym :::"clique"::: "S" for :::"connected"::: ; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_zfmisc_1 :::"trivial"::: ) -> ($#v1_dilworth :::"clique"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_dilworth :::"clique"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode Clique of "R" is ($#v1_dilworth :::"clique"::: ) ($#m1_subset_1 :::"Subset":::) "of" "R"; end; theorem :: DILWORTH:6 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a")))) ")" ))) ; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) ($#v1_dilworth :::"connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#v3_orders_2 :::"reflexive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_dilworth :::"connected"::: ) -> ($#v6_orders_2 :::"strongly_connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_dilworth :::"connected"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; theorem :: DILWORTH:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R"))) & (Bool (Bool "not" (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))))) "holds" (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1"))))) ; theorem :: DILWORTH:8 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) "or" (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1"))) ")" )) "holds" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R"))))) ; theorem :: DILWORTH:9 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) "holds" (Bool (Set (Var "S")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))))) ; theorem :: DILWORTH:10 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) ")" ))))) ; theorem :: DILWORTH:11 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set (Var "C"))) & (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "C")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))))) ; theorem :: DILWORTH:12 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set (Var "C"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "C")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "S" is :::"stable"::: means :: DILWORTH:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) ")" )); end; :: deftheorem defines :::"stable"::: DILWORTH:def 2 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_dilworth :::"stable"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y")))) & (Bool (Bool "not" (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x")))) ")" )) ")" ))); registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_zfmisc_1 :::"trivial"::: ) -> ($#v2_dilworth :::"stable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v2_dilworth :::"stable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode StableSet of "R" is ($#v2_dilworth :::"stable"::: ) ($#m1_subset_1 :::"Subset":::) "of" "R"; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_finset_1 :::"finite"::: ) ($#v2_dilworth :::"stable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v2_dilworth :::"stable"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; theorem :: DILWORTH:13 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set (Var "a2"))) & (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))) "holds" (Bool "(" (Bool (Bool "not" (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2")))) & (Bool (Bool "not" (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1")))) ")" ))) ; theorem :: DILWORTH:14 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a2"))) "or" (Bool (Set (Var "a2")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a1"))) "or" (Bool (Set ($#k7_domain_1 :::"{"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k7_domain_1 :::"}"::: ) ) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R"))) ")" ))) ; theorem :: DILWORTH:15 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))))) ; theorem :: DILWORTH:16 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "B")) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))))) ; theorem :: DILWORTH:17 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"with_finite_clique#"::: means :: DILWORTH:def 3 (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" "R" "st" (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" "R" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))))); end; :: deftheorem defines :::"with_finite_clique#"::: DILWORTH:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_dilworth :::"with_finite_clique#"::: ) ) "iff" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "st" (Bool "for" (Set (Var "D")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "D"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C")))))) ")" )); registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v3_dilworth :::"with_finite_clique#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "R" be ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_dilworth :::"connected"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; definitionlet "R" be ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"clique#"::: "R" -> ($#m1_hidden :::"Nat":::) means :: DILWORTH:def 4 (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" "R" "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) it)) & (Bool "(" "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" "R" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "T"))) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"clique#"::: DILWORTH:def 4 : (Bool "for" (Set (Var "R")) "being" ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool "ex" (Set (Var "C")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "T"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_dilworth :::"clique#"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k1_dilworth :::"clique#"::: ) "R") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: DILWORTH:18 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: DILWORTH:19 (Bool "for" (Set (Var "R")) "being" ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"with_finite_stability#"::: means :: DILWORTH:def 5 (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" "R" "st" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" "R" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A")))))); end; :: deftheorem defines :::"with_finite_stability#"::: DILWORTH:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_dilworth :::"with_finite_stability#"::: ) ) "iff" (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool "for" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A")))))) ")" )); registration cluster ($#v8_struct_0 :::"finite"::: ) -> ($#v4_dilworth :::"with_finite_stability#"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; registrationlet "R" be ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v2_dilworth :::"stable"::: ) -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; definitionlet "R" be ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; func :::"stability#"::: "R" -> ($#m1_hidden :::"Nat":::) means :: DILWORTH:def 6 (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" "R" "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) it)) & (Bool "(" "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" "R" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "T"))) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"stability#"::: DILWORTH:def 6 : (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool "ex" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "T"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_dilworth :::"stability#"::: ) "R") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k2_dilworth :::"stability#"::: ) "R") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: DILWORTH:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: DILWORTH:21 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))) ; registration cluster ($#v3_dilworth :::"with_finite_clique#"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) -> ($#v8_struct_0 :::"finite"::: ) for ($#l1_orders_2 :::"RelStr"::: ) ; end; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); func :::"Lower"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "R" equals :: DILWORTH:def 7 (Set "X" ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) "X" ")" )); func :::"Upper"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" "R" equals :: DILWORTH:def 8 (Set "X" ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) "X" ")" )); end; :: deftheorem defines :::"Lower"::: DILWORTH:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k3_dilworth :::"Lower"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_waybel_0 :::"downarrow"::: ) (Set (Var "X")) ")" ))))); :: deftheorem defines :::"Upper"::: DILWORTH:def 8 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k4_dilworth :::"Upper"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k4_waybel_0 :::"uparrow"::: ) (Set (Var "X")) ")" ))))); theorem :: DILWORTH:22 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k4_dilworth :::"Upper"::: ) (Set (Var "A")))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k3_dilworth :::"Lower"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))))) ; theorem :: DILWORTH:23 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))))) "holds" (Bool (Set (Set "(" ($#k4_dilworth :::"Upper"::: ) (Set (Var "A")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_dilworth :::"Lower"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:24 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set ($#k3_dilworth :::"Lower"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))))))) ; theorem :: DILWORTH:25 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set ($#k4_dilworth :::"Upper"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))))))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"minimals"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "R" means :: DILWORTH:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "R")) ")" )) if (Bool (Bool "not" "R" "is" ($#v2_struct_0 :::"empty"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); func :::"maximals"::: "R" -> ($#m1_subset_1 :::"Subset":::) "of" "R" means :: DILWORTH:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) "R")) ")" )) if (Bool (Bool "not" "R" "is" ($#v2_struct_0 :::"empty"::: ) )) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"minimals"::: DILWORTH:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "R")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R")))) "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 "b2"))) "iff" (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "R")) "is" ($#v2_struct_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); :: deftheorem defines :::"maximals"::: DILWORTH:def 10 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "R")) "is" ($#v2_struct_0 :::"empty"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R")))) "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 "b2"))) "iff" (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Set (Var "R")) "is" ($#v2_struct_0 :::"empty"::: ) )) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k6_dilworth :::"maximals"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set ($#k5_dilworth :::"minimals"::: ) "R") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set ($#k5_dilworth :::"minimals"::: ) "R") -> ($#v2_dilworth :::"stable"::: ) ; cluster (Set ($#k6_dilworth :::"maximals"::: ) "R") -> ($#v2_dilworth :::"stable"::: ) ; end; theorem :: DILWORTH:26 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Bool (Bool "not" (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) "holds" (Bool "not" (Bool (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_dilworth :::"Upper"::: ) (Set (Var "A"))))))) ; theorem :: DILWORTH:27 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Bool (Bool "not" (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))))) "holds" (Bool "not" (Bool (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_dilworth :::"Lower"::: ) (Set (Var "A"))))))) ; begin registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "X") -> ($#v8_struct_0 :::"finite"::: ) ; end; theorem :: DILWORTH:28 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) "holds" (Bool (Set (Var "C")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))))) ; theorem :: DILWORTH:29 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "C")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S"))) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ))))) ; theorem :: DILWORTH:30 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))))) ; theorem :: DILWORTH:31 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "A")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "S"))) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ))))) ; theorem :: DILWORTH:32 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "y")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set (Var "B")))))))) ; theorem :: DILWORTH:33 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "x")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "y")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set (Var "B")))))))) ; theorem :: DILWORTH:34 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" ($#k3_dilworth :::"Lower"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))))))) ; theorem :: DILWORTH:35 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" ($#k4_dilworth :::"Upper"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Bool "not" (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))))))) ; registrationlet "R" be ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v3_dilworth :::"with_finite_clique#"::: ) ; end; registrationlet "R" be ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); cluster (Set ($#k5_yellow_0 :::"subrelstr"::: ) "S") -> ($#v4_dilworth :::"with_finite_stability#"::: ) ; end; theorem :: DILWORTH:36 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r5_waybel_4 :::"is_minimal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")))) & (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "y")) ($#r2_orders_2 :::"<"::: ) (Set (Var "x"))) ")" ) ")" )))) ; theorem :: DILWORTH:37 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k4_dilworth :::"Upper"::: ) (Set "(" ($#k5_dilworth :::"minimals"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))))) ; theorem :: DILWORTH:38 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r3_waybel_4 :::"is_maximal_in"::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R")))) & (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "or" (Bool (Set (Var "x")) ($#r2_orders_2 :::"<"::: ) (Set (Var "y"))) ")" ) ")" )))) ; theorem :: DILWORTH:39 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k3_dilworth :::"Lower"::: ) (Set "(" ($#k6_dilworth :::"maximals"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "R"))))) ; theorem :: DILWORTH:40 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k5_dilworth :::"minimals"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:41 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_dilworth :::"maximals"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:42 (Bool "for" (Set (Var "R")) "being" ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:43 (Bool "for" (Set (Var "R")) "being" ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R")))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k1_dilworth :::"clique#"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R"))))))) ; theorem :: DILWORTH:44 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:45 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool (Set ($#k2_dilworth :::"stability#"::: ) (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); attr "P" is :::"Clique-wise"::: means :: DILWORTH:def 11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Clique":::) "of" "R")); end; :: deftheorem defines :::"Clique-wise"::: DILWORTH:def 11 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v5_dilworth :::"Clique-wise"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")))) ")" ))); registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#v5_dilworth :::"Clique-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode Clique-partition of "R" is ($#v5_dilworth :::"Clique-wise"::: ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v5_dilworth :::"Clique-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; theorem :: DILWORTH:46 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:47 (Bool "for" (Set (Var "R")) "being" ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ) ")" ))))) ; theorem :: DILWORTH:48 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "C")))) "holds" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "c")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: DILWORTH:49 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "U")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" ($#k4_dilworth :::"Upper"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "L")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set "(" ($#k3_dilworth :::"Lower"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "U"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "L"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))))) "holds" (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R"))))))))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "P" be ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R"))); attr "P" is :::"StableSet-wise"::: means :: DILWORTH:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"StableSet":::) "of" "R")); end; :: deftheorem defines :::"StableSet-wise"::: DILWORTH:def 12 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "holds" (Bool "(" (Bool (Set (Var "P")) "is" ($#v6_dilworth :::"StableSet-wise"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")))) ")" ))); registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#v6_dilworth :::"StableSet-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; mode Coloring of "R" is ($#v6_dilworth :::"StableSet-wise"::: ) ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; registrationlet "R" be ($#v2_struct_0 :::"empty"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster -> ($#v6_dilworth :::"StableSet-wise"::: ) for ($#m1_eqrel_1 :::"a_partition"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R"); end; theorem :: DILWORTH:50 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R")))))) ; begin theorem :: DILWORTH:51 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); attr "C" is :::"strong-chain"::: means :: DILWORTH:def 13 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" "R" (Bool "ex" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_dilworth :::"stability#"::: ) "R")) & (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "S")) ($#k9_subset_1 :::"/\"::: ) "C") ($#r1_tarski :::"c="::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set "C" ($#k8_subset_1 :::"/\"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )) ")" ))); end; :: deftheorem defines :::"strong-chain"::: DILWORTH:def 13 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v7_dilworth :::"strong-chain"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "P")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set "(" ($#k5_yellow_0 :::"subrelstr"::: ) (Set (Var "S")) ")" ) "st" (Bool "(" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "P"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))) & (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "S")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "C"))) ($#r1_tarski :::"c="::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set (Var "C")) ($#k8_subset_1 :::"/\"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" )) ")" ))) ")" ))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster ($#v7_dilworth :::"strong-chain"::: ) -> ($#v1_dilworth :::"clique"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Num 1) ($#v3_card_1 :::"-element"::: ) -> ($#v7_dilworth :::"strong-chain"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")); end; theorem :: DILWORTH:52 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "S")) "is" ($#v7_dilworth :::"strong-chain"::: ) ) & (Bool "(" "for" (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" "not" (Bool (Set (Var "D")) "is" ($#v7_dilworth :::"strong-chain"::: ) ) "or" "not" (Bool (Set (Var "S")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "D"))) ")" ) ")" ) ")" ))) ; theorem :: DILWORTH:53 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v4_dilworth :::"with_finite_stability#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "C")) "being" ($#m1_eqrel_1 :::"Clique-partition":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k2_dilworth :::"stability#"::: ) (Set (Var "R")))))) ; theorem :: DILWORTH:54 (Bool "for" (Set (Var "R")) "being" ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#v3_dilworth :::"with_finite_clique#"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_eqrel_1 :::"Coloring":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_dilworth :::"clique#"::: ) (Set (Var "R")))))) ; begin theorem :: DILWORTH:55 (Bool "for" (Set (Var "R")) "being" ($#v8_struct_0 :::"finite"::: ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" "not" (Bool (Set ($#k7_struct_0 :::"card"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) "or" (Bool "ex" (Set (Var "C")) "being" ($#m1_subset_1 :::"Clique":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "C"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) "or" (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"StableSet":::) "of" (Set (Var "R")) "st" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "s")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)))) ")" ))) ; theorem :: DILWORTH:56 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "ex" (Set (Var "g")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSubsequence":::) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "f"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "g"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) & (Bool "(" (Bool (Set (Var "g")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" ) ")" )))) ;