:: DICKSON semantic presentation begin theorem :: DICKSON:1 (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DICKSON:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Var "n")) ($#r1_ordinal1 :::"c="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) ; scheme :: DICKSON:sch 1 FinSegRng2{ F1() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F3 "(" (Set (Var "i")) ")" ) where i "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set F1 "(" ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "i"))]) ")" ) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; theorem :: DICKSON:3 (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "X")) "st" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); attr "f" is :::"ascending"::: means :: DICKSON:def 1 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) ")" )); end; :: deftheorem defines :::"ascending"::: DICKSON:def 1 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_dickson :::"ascending"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" )) ")" ))); definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "f" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); attr "f" is :::"weakly-ascending"::: means :: DICKSON:def 2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" "f" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R"))); end; :: deftheorem defines :::"weakly-ascending"::: DICKSON:def 2 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_dickson :::"weakly-ascending"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))) ")" ))); theorem :: DICKSON:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_dickson :::"weakly-ascending"::: ) )) "holds" (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))))))) ; theorem :: DICKSON:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v16_waybel_0 :::"connected"::: ) ) "iff" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) ")" )) ; theorem :: DICKSON:6 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) ($#k1_wellord1 :::"-Seg"::: ) (Set (Var "a"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y"))) & (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) "iff" (Bool (Set (Var "a")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "Y")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L")))) ")" ))) ; theorem :: DICKSON:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))) ($#k1_wellord1 :::"-Seg"::: ) (Set (Var "x")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "N"))) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))) "holds" (Bool (Set (Var "a")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))))) ; begin definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"quasi_ordered"::: means :: DICKSON:def 3 (Bool "(" (Bool "R" "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool "R" "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ); end; :: deftheorem defines :::"quasi_ordered"::: DICKSON:def 3 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) "iff" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_orders_2 :::"reflexive"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_orders_2 :::"transitive"::: ) ) ")" ) ")" )); definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; assume (Bool (Set (Const "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) ; func :::"EqRel"::: "R" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") equals :: DICKSON:def 4 (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#k2_eqrel_1 :::"/\"::: ) (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#k3_relset_1 :::"~"::: ) ")" )); end; :: deftheorem defines :::"EqRel"::: DICKSON:def 4 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool (Set ($#k1_dickson :::"EqRel"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#k2_eqrel_1 :::"/\"::: ) (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#k3_relset_1 :::"~"::: ) ")" )))); theorem :: DICKSON:8 (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")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "y")) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_orders_2 :::"<="::: ) (Set (Var "y"))) & (Bool (Set (Var "y")) ($#r1_orders_2 :::"<="::: ) (Set (Var "x"))) ")" ) ")" ))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; func :::"<=E"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_dickson :::"EqRel"::: ) "R" ")" ) ")" ) means :: DICKSON:def 5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) "R" ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) "R" ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" )) ")" )); end; :: deftheorem defines :::"<=E"::: DICKSON:def 5 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_dickson :::"<=E"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "a")) ")" )) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "b")) ")" )) & (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b"))) ")" )) ")" )) ")" ))); theorem :: DICKSON:9 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool (Set ($#k2_dickson :::"<=E"::: ) (Set (Var "R"))) ($#r2_orders_1 :::"partially_orders"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" )))) ; theorem :: DICKSON:10 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "R")) "is" ($#v16_waybel_0 :::"connected"::: ) )) "holds" (Bool (Set ($#k2_dickson :::"<=E"::: ) (Set (Var "R"))) ($#r3_orders_1 :::"linearly_orders"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" )))) ; definitionlet "R" be ($#m1_hidden :::"Relation":::); func "R" :::"\~"::: -> ($#m1_hidden :::"Relation":::) equals :: DICKSON:def 6 (Set "R" ($#k6_subset_1 :::"\"::: ) (Set "(" "R" ($#k2_relat_1 :::"~"::: ) ")" )); end; :: deftheorem defines :::"\~"::: DICKSON:def 6 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k3_dickson :::"\~"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "R")) ($#k2_relat_1 :::"~"::: ) ")" )))); registrationlet "R" be ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k3_dickson :::"\~"::: ) ) -> ($#v5_relat_2 :::"asymmetric"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); :: original: :::"\~"::: redefine func "R" :::"\~"::: -> ($#m1_subset_1 :::"Relation":::) "of" "X"; end; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; func "R" :::"\~"::: -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) equals :: DICKSON:def 7 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R") ($#k4_dickson :::"\~"::: ) ")" ) "#)" ); end; :: deftheorem defines :::"\~"::: DICKSON:def 7 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) "," (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#k4_dickson :::"\~"::: ) ")" ) "#)" ))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "R" ($#k5_dickson :::"\~"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_orders_2 :::"strict"::: ) ; end; registrationlet "R" be ($#v4_orders_2 :::"transitive"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "R" ($#k5_dickson :::"\~"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v4_orders_2 :::"transitive"::: ) ; end; registrationlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; cluster (Set "R" ($#k5_dickson :::"\~"::: ) ) -> ($#v1_orders_2 :::"strict"::: ) ($#v5_orders_2 :::"antisymmetric"::: ) ; end; theorem :: DICKSON:11 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: DICKSON:12 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k3_dickson :::"\~"::: ) )) "iff" (Bool (Set (Var "R")) "is" ($#v5_relat_2 :::"asymmetric"::: ) ) ")" )) ; theorem :: DICKSON:13 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v8_relat_2 :::"transitive"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k3_dickson :::"\~"::: ) ) "is" ($#v8_relat_2 :::"transitive"::: ) )) ; theorem :: DICKSON:14 (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_relat_2 :::"antisymmetric"::: ) )) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "R")) ($#k3_dickson :::"\~"::: ) )) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" ) ")" ))) ; theorem :: DICKSON:15 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ; theorem :: DICKSON:16 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) & (Bool (Set (Var "R")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ; begin theorem :: DICKSON:17 (Bool "for" (Set (Var "L")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "L")) ($#k5_dickson :::"\~"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "L")) ($#k5_dickson :::"\~"::: ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "L"))))) "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 "L")))) ")" ) ")" ) ")" )))) ; theorem :: DICKSON:18 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "R")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "S")) "is" ($#v5_orders_2 :::"antisymmetric"::: ) ) & (Bool (Set (Set (Var "S")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "a")) ($#r1_orders_2 :::"<="::: ) (Set (Var "b")))) "implies" (Bool (Set (Set (Var "m")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "m")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) ")" & "(" (Bool (Bool (Set (Set (Var "m")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))))) "implies" (Bool (Set ($#k7_yellow_3 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k7_yellow_3 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")))) ")" ")" ) ")" )) "holds" (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); func :::"min-classes"::: "N" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "R" means :: DICKSON:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" "R" ($#k5_dickson :::"\~"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) "N" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" "R" ($#k5_dickson :::"\~"::: ) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) "R" ")" ) "," (Set (Var "y")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) "N")) ")" )) ")" )); end; :: deftheorem defines :::"min-classes"::: DICKSON:def 8 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "y")) ")" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N")))) ")" )) ")" )) ")" )))); theorem :: DICKSON:19 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "x")))) "holds" (Bool (Set (Var "y")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ))))))) ; theorem :: DICKSON:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N")))))) ")" )) ; theorem :: DICKSON:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" )))) "holds" (Bool "not" (Bool (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: DICKSON:22 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))))) "holds" (Bool "not" (Bool (Set (Var "x")) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; theorem :: DICKSON:23 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "R")) "is" ($#v16_waybel_0 :::"connected"::: ) ) & (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) ")" ) "iff" (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_dickson :::"min-classes"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ")" )) ; theorem :: DICKSON:24 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool "(" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r2_wellord1 :::"well_orders"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "iff" (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k6_dickson :::"min-classes"::: ) (Set (Var "N")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ")" )) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); let "B" be ($#m1_hidden :::"set"::: ) ; pred "B" :::"is_Dickson-basis_of"::: "N" "," "R" means :: DICKSON:def 9 (Bool "(" (Bool "B" ($#r1_tarski :::"c="::: ) "N") & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) "N")) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) "B") & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_Dickson-basis_of"::: DICKSON:def 9 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R"))) "iff" (Bool "(" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "N"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "b")) ($#r1_orders_2 :::"<="::: ) (Set (Var "a"))) ")" )) ")" ) ")" ) ")" )))); theorem :: DICKSON:25 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set ($#k1_subset_1 :::"{}"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "," (Set (Var "R")))) ; theorem :: DICKSON:26 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R")))) "holds" (Bool "not" (Bool (Set (Var "B")) "is" ($#v1_xboole_0 :::"empty"::: ) ))))) ; definitionlet "R" be ($#l1_orders_2 :::"RelStr"::: ) ; attr "R" is :::"Dickson"::: means :: DICKSON:def 10 (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" "R" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," "R") & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))); end; :: deftheorem defines :::"Dickson"::: DICKSON:def 10 : (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) "iff" (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R"))) & (Bool (Set (Var "B")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ))) ")" )); theorem :: DICKSON:27 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) & (Bool (Set (Var "R")) "is" ($#v16_waybel_0 :::"connected"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) ; theorem :: DICKSON:28 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S")))) & (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Var "S")) "is" ($#v4_dickson :::"Dickson"::: ) )) ; definitionlet "f" be ($#m1_hidden :::"Function":::); let "b" be ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) and (Bool (Set (Const "b")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Const "f")))) ; func "f" :::"mindex"::: "b" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: DICKSON:def 11 (Bool "(" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) "b") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "b")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) ")" ) ")" ); end; :: deftheorem defines :::"mindex"::: DICKSON:def 11 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_dickson :::"mindex"::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) ")" ) ")" ) ")" )))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; let "f" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); let "b" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Const "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Const "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Const "b"))) ")" )) ; func "f" :::"mindex"::: "(" "b" "," "m" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: DICKSON:def 12 (Bool "(" (Bool (Set "f" ($#k8_nat_1 :::"."::: ) it) ($#r1_hidden :::"="::: ) "b") & (Bool "m" ($#r1_xxreal_0 :::"<"::: ) it) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "m" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set "f" ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) "b")) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) ")" ) ")" ); end; :: deftheorem defines :::"mindex"::: DICKSON:def 12 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "ex" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_dickson :::"mindex"::: ) "(" (Set (Var "b")) "," (Set (Var "m")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "b5"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "b5")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) ")" ) ")" ) ")" )))))); theorem :: DICKSON:29 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")))) ")" )))) ; theorem :: DICKSON:30 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool (Set (Set "(" (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#k1_wellord1 :::"-Seg"::: ) (Set (Var "x")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k1_dickson :::"EqRel"::: ) (Set (Var "R")) ")" ) "," (Set (Var "x")) ")" ))) "holds" (Bool (Set (Var "x")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "N")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ")" )))))) ; theorem :: DICKSON:31 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_orders_2 :::"<="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Bool "not" (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ))) ; theorem :: DICKSON:32 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool "(" "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Bool "not" (Set ($#k6_dickson :::"min-classes"::: ) (Set (Var "N"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" ) ")" )) "holds" (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) ; theorem :: DICKSON:33 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) "holds" (Bool (Set (Set (Var "R")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ; theorem :: DICKSON:34 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "N")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R"))) & (Bool "(" "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R")))) "holds" (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" ) ")" )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "N" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); assume (Bool (Set (Const "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) ; func :::"Dickson-bases"::: "(" "N" "," "R" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" "R" means :: DICKSON:def 13 (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) "N" "," "R") ")" )); end; :: deftheorem defines :::"Dickson-bases"::: DICKSON:def 13 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_dickson :::"Dickson-bases"::: ) "(" (Set (Var "N")) "," (Set (Var "R")) ")" )) "iff" (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set (Var "R"))) ")" )) ")" )))); theorem :: DICKSON:35 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) "holds" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "t")) "is" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set (Var "s"))) & (Bool (Set (Var "t")) "is" ($#v2_dickson :::"weakly-ascending"::: ) ) ")" )))) ; theorem :: DICKSON:36 (Bool "for" (Set (Var "R")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v2_struct_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) )) ; theorem :: DICKSON:37 (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Var "N")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Var "M")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "N")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v4_dickson :::"Dickson"::: ) ) ")" )) ; theorem :: DICKSON:38 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "," (Set (Var "S")) ($#r5_waybel_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set (Var "S")) "is" ($#v4_dickson :::"Dickson"::: ) ) ")" )) ; theorem :: DICKSON:39 (Bool "for" (Set (Var "p")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Num 1) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Num 1) "holds" (Bool (Set (Set (Var "p")) ($#k3_waybel_3 :::"."::: ) (Set (Var "z"))) "," (Set ($#k5_yellow_1 :::"product"::: ) (Set (Var "p"))) ($#r5_waybel_1 :::"are_isomorphic"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); cluster (Set "p" ($#k5_relat_1 :::"|"::: ) "Y") -> ($#v1_yellow_1 :::"RelStr-yielding"::: ) ; end; theorem :: DICKSON:40 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Bool "not" (Set ($#k5_yellow_1 :::"product"::: ) (Set (Var "p"))) "is" ($#v2_struct_0 :::"empty"::: ) )) "iff" (Bool (Set (Var "p")) "is" ($#v4_waybel_3 :::"non-Empty"::: ) ) ")" ))) ; theorem :: DICKSON:41 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) (Bool "for" (Set (Var "ns")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "ne")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)) "st" (Bool (Bool (Set (Var "ns")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "ne")) ($#r1_hidden :::"="::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set "(" ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set (Var "ns")) ")" ) ")" ) "," (Set "(" (Set (Var "p")) ($#k3_waybel_3 :::"."::: ) (Set (Var "ne")) ")" ) ($#k3_yellow_3 :::":]"::: ) ) "," (Set ($#k5_yellow_1 :::"product"::: ) (Set (Var "p"))) ($#r5_waybel_1 :::"are_isomorphic"::: ) ))))) ; theorem :: DICKSON:42 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "n")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_waybel_3 :::"."::: ) (Set (Var "i"))) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Set (Var "p")) ($#k3_waybel_3 :::"."::: ) (Set (Var "i"))) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) ")" ) ")" )) "holds" (Bool "(" (Bool (Set ($#k5_yellow_1 :::"product"::: ) (Set (Var "p"))) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set ($#k5_yellow_1 :::"product"::: ) (Set (Var "p"))) "is" ($#v4_dickson :::"Dickson"::: ) ) ")" ))) ; registrationlet "p" be ($#v1_yellow_1 :::"RelStr-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ); cluster (Set ($#k5_yellow_1 :::"product"::: ) "p") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) "p") -> ($#v5_orders_2 :::"antisymmetric"::: ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) "p") -> ($#v3_dickson :::"quasi_ordered"::: ) ; end; definitionfunc :::"NATOrd"::: -> ($#m1_subset_1 :::"Relation":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: DICKSON:def 14 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) "}" ; end; :: deftheorem defines :::"NATOrd"::: DICKSON:def 14 : (Bool (Set ($#k10_dickson :::"NATOrd"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) where x, y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) "}" ); theorem :: DICKSON:43 (Bool (Set ($#k10_dickson :::"NATOrd"::: ) ) ($#r1_relat_2 :::"is_reflexive_in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: DICKSON:44 (Bool (Set ($#k10_dickson :::"NATOrd"::: ) ) ($#r4_relat_2 :::"is_antisymmetric_in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: DICKSON:45 (Bool (Set ($#k10_dickson :::"NATOrd"::: ) ) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; theorem :: DICKSON:46 (Bool (Set ($#k10_dickson :::"NATOrd"::: ) ) ($#r8_relat_2 :::"is_transitive_in"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ; definitionfunc :::"OrderedNAT"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) equals :: DICKSON:def 15 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k10_dickson :::"NATOrd"::: ) ) "#)" ); end; :: deftheorem defines :::"OrderedNAT"::: DICKSON:def 15 : (Bool (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k10_dickson :::"NATOrd"::: ) ) "#)" )); registration cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ; cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_dickson :::"Dickson"::: ) ; cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_dickson :::"quasi_ordered"::: ) ; cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_orders_2 :::"antisymmetric"::: ) ; cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_orders_2 :::"transitive"::: ) ; cluster (Set ($#k11_dickson :::"OrderedNAT"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_wellfnd1 :::"well_founded"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "n" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" )) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "n" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" )) -> ($#v4_dickson :::"Dickson"::: ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "n" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" )) -> ($#v3_dickson :::"quasi_ordered"::: ) ; cluster (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" "n" ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" )) -> ($#v5_orders_2 :::"antisymmetric"::: ) ; end; theorem :: DICKSON:47 (Bool "for" (Set (Var "M")) "being" ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "M")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Var "M")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set ($#k3_yellow_3 :::"[:"::: ) (Set (Var "M")) "," (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ($#k3_yellow_3 :::":]"::: ) ) "is" ($#v4_dickson :::"Dickson"::: ) ) ")" )) ; theorem :: DICKSON:48 (Bool "for" (Set (Var "R")) "," (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) & (Bool (Set (Var "S")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "S")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ; theorem :: DICKSON:49 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v3_dickson :::"quasi_ordered"::: ) )) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_dickson :::"Dickson"::: ) ) "iff" (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) "st" (Bool (Bool (Set (Var "S")) "is" ($#v3_dickson :::"quasi_ordered"::: ) ) & (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "S")))) & (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))) "holds" (Bool (Set (Set (Var "S")) ($#k5_dickson :::"\~"::: ) ) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ")" )) ;