:: BAGORDER semantic presentation begin theorem :: BAGORDER:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "x"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "x")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: BAGORDER:2 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Num 1)) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "k")) ($#k9_real_1 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" ) ")" )) ; registrationlet "f" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: BAGORDER:3 canceled; theorem :: BAGORDER:4 (Bool "for" (Set (Var "fs")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "fs"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "fs")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "fs")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) ; definitionlet "n", "i", "j" be ($#m1_hidden :::"Nat":::); let "b" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "n")); func "(" "i" "," "j" ")" :::"-cut"::: "b" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "j" ($#k7_nat_d :::"-'"::: ) "i") means :: BAGORDER:def 1 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set "j" ($#k7_nat_d :::"-'"::: ) "i"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "b" ($#k1_funct_1 :::"."::: ) (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))); end; :: deftheorem defines :::"-cut"::: BAGORDER:def 1 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "b")))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) ")" )))); registrationlet "n", "i", "j" be ($#m1_hidden :::"Nat":::); let "b" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "n")); cluster (Set "(" "i" "," "j" ")" ($#k1_bagorder :::"-cut"::: ) "b") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "n", "i", "j" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "b" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "n")); cluster (Set "(" "i" "," "j" ")" ($#k1_bagorder :::"-cut"::: ) "b") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: BAGORDER:5 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool "(" (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "b")))) & (Bool (Set "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "b")))) ")" ) ")" ))) ; definitionlet "x" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Fin"::: "(" "x" "," "n" ")" -> ($#m1_hidden :::"set"::: ) equals :: BAGORDER:def 2 "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Subset":::) "of" "x" : (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Bool "not" (Set (Var "y")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "y"))) ($#r1_ordinal1 :::"c="::: ) "n") ")" ) "}" ; end; :: deftheorem defines :::"Fin"::: BAGORDER:def 2 : (Bool "for" (Set (Var "x")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_bagorder :::"Fin"::: ) "(" (Set (Var "x")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "y")) where y "is" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "x")) : (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Bool "not" (Set (Var "y")) "is" ($#v1_xboole_0 :::"empty"::: ) )) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "y"))) ($#r1_ordinal1 :::"c="::: ) (Set (Var "n"))) ")" ) "}" ))); registrationlet "x" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_bagorder :::"Fin"::: ) "(" "x" "," "n" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: BAGORDER:6 (Bool "for" (Set (Var "R")) "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" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" )))) ; theorem :: BAGORDER:7 (Bool "for" (Set (Var "R")) "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" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" )))) ; theorem :: BAGORDER:8 (Bool "for" (Set (Var "R")) "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 "f")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_wellfnd1 :::"descending"::: ) )) "holds" (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" )))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_orders_2 :::"RelStr"::: ) ; let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); attr "s" is :::"non-increasing"::: means :: BAGORDER:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" "s" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" "s" ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R"))); end; :: deftheorem defines :::"non-increasing"::: BAGORDER:def 3 : (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")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v1_bagorder :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))) ")" ))); theorem :: BAGORDER:9 (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" ($#v1_bagorder :::"non-increasing"::: ) )) "holds" (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R"))))))) ; theorem :: BAGORDER:10 (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 "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) & (Bool (Set (Var "s")) "is" ($#v1_bagorder :::"non-increasing"::: ) )) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "r")))))))) ; theorem :: BAGORDER:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) )))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); func :::"TotDegree"::: "b" -> ($#m1_hidden :::"Nat":::) means :: BAGORDER:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "b" ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) "n" ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) "b" ")" ) ")" ")" ))) ")" )); end; :: deftheorem defines :::"TotDegree"::: BAGORDER:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" ")" ))) ")" )) ")" )))); theorem :: BAGORDER:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "s")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ")" ")" ))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k2_polynom2 :::"*"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k1_yellow_1 :::"RelIncl"::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set "(" ($#k1_polynom2 :::"support"::: ) (Set (Var "b")) ")" ) ($#k1_finsub_1 :::"\/"::: ) (Set (Var "s")) ")" ) ")" ")" )))) "holds" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "g")))))))) ; theorem :: BAGORDER:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BAGORDER:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set "(" (Set (Var "a")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BAGORDER:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) ")" ))) ; theorem :: BAGORDER:16 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k1_bagorder :::"-cut"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set "(" (Set (Var "j")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" )))) ; theorem :: BAGORDER:17 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k1_bagorder :::"-cut"::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "a")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "b")) ")" ))))) ; theorem :: BAGORDER:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: BAGORDER:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))))) ; theorem :: BAGORDER:20 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "b")) ($#k5_relat_1 :::"|"::: ) (Set (Var "m"))) "is" ($#m1_hidden :::"bag":::) "of" (Set (Var "m"))))) ; theorem :: BAGORDER:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_polynom2 :::"support"::: ) (Set (Var "a")))))) ; begin definitionlet "n" be ($#m1_hidden :::"set"::: ) ; mode TermOrder of "n" is ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ); end; notationlet "n" be ($#m1_hidden :::"Ordinal":::); synonym :::"LexOrder"::: "n" for :::"BagOrder"::: "n"; end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); attr "T" is :::"admissible"::: means :: BAGORDER:def 5 (Bool "(" (Bool "T" ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n")) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) "n" ")" ) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "T") ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "T")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "T") ")" ) ")" ); end; :: deftheorem defines :::"admissible"::: BAGORDER:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_bagorder :::"admissible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "T")) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) "," (Set (Var "a")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" ) ")" ) ")" ))); theorem :: BAGORDER:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k17_pre_poly :::"LexOrder"::: ) (Set (Var "n"))) "is" ($#v2_bagorder :::"admissible"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n") ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "n") "," (Set ($#k15_pre_poly :::"Bags"::: ) "n")) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v2_bagorder :::"admissible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k17_pre_poly :::"LexOrder"::: ) "n") -> ($#v2_bagorder :::"admissible"::: ) ; end; theorem :: BAGORDER:23 (Bool "for" (Set (Var "o")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Bool "not" (Set ($#k17_pre_poly :::"LexOrder"::: ) (Set (Var "o"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) ))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); func :::"InvLexOrder"::: "n" -> ($#m1_subset_1 :::"TermOrder":::) "of" "n" means :: BAGORDER:def 6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) "or" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "n") & (Bool (Set (Set (Var "p")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "q")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) "n")) "holds" (Bool (Set (Set (Var "p")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"InvLexOrder"::: BAGORDER:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_bagorder :::"InvLexOrder"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) "or" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "p")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "q")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" )) ")" ) ")" )) ")" ))); theorem :: BAGORDER:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k4_bagorder :::"InvLexOrder"::: ) (Set (Var "n"))) "is" ($#v2_bagorder :::"admissible"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k4_bagorder :::"InvLexOrder"::: ) "n") -> ($#v2_bagorder :::"admissible"::: ) ; end; theorem :: BAGORDER:25 (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k4_bagorder :::"InvLexOrder"::: ) (Set (Var "o"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "o" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); assume (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "n")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Const "o")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Const "o")))) ; func :::"Graded"::: "o" -> ($#m1_subset_1 :::"TermOrder":::) "of" "n" means :: BAGORDER:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")))) "or" (Bool "(" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "o") ")" ) ")" ) ")" )); end; :: deftheorem defines :::"Graded"::: BAGORDER:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o"))) ")" )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_bagorder :::"Graded"::: ) (Set (Var "o")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "(" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")))) "or" (Bool "(" (Bool (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k3_bagorder :::"TotDegree"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o"))) ")" ) ")" ) ")" )) ")" )))); theorem :: BAGORDER:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "a")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o"))) ")" ) & (Bool (Set (Var "o")) ($#r7_relat_2 :::"is_strongly_connected_in"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k5_bagorder :::"Graded"::: ) (Set (Var "o"))) "is" ($#v2_bagorder :::"admissible"::: ) ))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); func :::"GrLexOrder"::: "n" -> ($#m1_subset_1 :::"TermOrder":::) "of" "n" equals :: BAGORDER:def 8 (Set ($#k5_bagorder :::"Graded"::: ) (Set "(" ($#k17_pre_poly :::"LexOrder"::: ) "n" ")" )); func :::"GrInvLexOrder"::: "n" -> ($#m1_subset_1 :::"TermOrder":::) "of" "n" equals :: BAGORDER:def 9 (Set ($#k5_bagorder :::"Graded"::: ) (Set "(" ($#k4_bagorder :::"InvLexOrder"::: ) "n" ")" )); end; :: deftheorem defines :::"GrLexOrder"::: BAGORDER:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_bagorder :::"GrLexOrder"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_bagorder :::"Graded"::: ) (Set "(" ($#k17_pre_poly :::"LexOrder"::: ) (Set (Var "n")) ")" )))); :: deftheorem defines :::"GrInvLexOrder"::: BAGORDER:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k7_bagorder :::"GrInvLexOrder"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_bagorder :::"Graded"::: ) (Set "(" ($#k4_bagorder :::"InvLexOrder"::: ) (Set (Var "n")) ")" )))); theorem :: BAGORDER:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k6_bagorder :::"GrLexOrder"::: ) (Set (Var "n"))) "is" ($#v2_bagorder :::"admissible"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k6_bagorder :::"GrLexOrder"::: ) "n") -> ($#v2_bagorder :::"admissible"::: ) ; end; theorem :: BAGORDER:28 (Bool "for" (Set (Var "o")) "being" ($#v1_finset_1 :::"infinite"::: ) ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Bool "not" (Set ($#k6_bagorder :::"GrLexOrder"::: ) (Set (Var "o"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) ))) ; theorem :: BAGORDER:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k7_bagorder :::"GrInvLexOrder"::: ) (Set (Var "n"))) "is" ($#v2_bagorder :::"admissible"::: ) )) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k7_bagorder :::"GrInvLexOrder"::: ) "n") -> ($#v2_bagorder :::"admissible"::: ) ; end; theorem :: BAGORDER:30 (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k7_bagorder :::"GrInvLexOrder"::: ) (Set (Var "o"))) "is" ($#v2_wellord1 :::"well-ordering"::: ) )) ; definitionlet "i", "n" be ($#m1_hidden :::"Nat":::); let "o1" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Const "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ); let "o2" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Const "n")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Const "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ); func :::"BlockOrder"::: "(" "i" "," "n" "," "o1" "," "o2" ")" -> ($#m1_subset_1 :::"TermOrder":::) "of" "n" means :: BAGORDER:def 10 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool "(" (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p")) ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "o1") ")" ) "or" (Bool "(" (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "(" (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," "n" ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p")) ")" ) "," (Set "(" "(" (Set "(" "i" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," "n" ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "o2") ")" ) ")" ) ")" )); end; :: deftheorem defines :::"BlockOrder"::: BAGORDER:def 10 : (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k8_bagorder :::"BlockOrder"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" )) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "(" (Bool "(" (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p")) ")" ) "," (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o1"))) ")" ) "or" (Bool "(" (Bool (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "p")) ")" ) "," (Set "(" "(" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "n")) ")" ($#k1_bagorder :::"-cut"::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "o2"))) ")" ) ")" ) ")" )) ")" ))))); theorem :: BAGORDER:31 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "st" (Bool (Bool (Set (Var "o1")) "is" ($#v2_bagorder :::"admissible"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v2_bagorder :::"admissible"::: ) )) "holds" (Bool (Set ($#k8_bagorder :::"BlockOrder"::: ) "(" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ) "is" ($#v2_bagorder :::"admissible"::: ) )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); func :::"NaivelyOrderedBags"::: "n" -> ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) means :: BAGORDER:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n")) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" it)) "iff" (Bool (Set (Var "x")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "y"))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"NaivelyOrderedBags"::: BAGORDER:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_orders_2 :::"strict"::: ) ($#l1_orders_2 :::"RelStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_bagorder :::"NaivelyOrderedBags"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "b2")))) "iff" (Bool (Set (Var "x")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "y"))) ")" ) ")" ) ")" ) ")" ))); theorem :: BAGORDER:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "n")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))))) ; theorem :: BAGORDER:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k9_bagorder :::"NaivelyOrderedBags"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_yellow_1 :::"product"::: ) (Set "(" (Set (Var "n")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k11_dickson :::"OrderedNAT"::: ) ) ")" )))) ; theorem :: BAGORDER:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v2_bagorder :::"admissible"::: ) )) "holds" (Bool "(" (Bool (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k9_bagorder :::"NaivelyOrderedBags"::: ) (Set (Var "n")) ")" )) ($#r1_relset_1 :::"c="::: ) (Set (Var "o"))) & (Bool (Set (Var "o")) "is" ($#v2_wellord1 :::"well-ordering"::: ) ) ")" ))) ; begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); let "X" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R")))); assume (Bool (Bool "not" (Set (Const "X")) "is" ($#v1_xboole_0 :::"empty"::: ) )) ; func :::"PosetMin"::: "X" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: BAGORDER:def 12 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "X") & (Bool it ($#r4_waybel_4 :::"is_minimal_wrt"::: ) "X" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) ")" ); func :::"PosetMax"::: "X" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: BAGORDER:def 13 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "X") & (Bool it ($#r2_waybel_4 :::"is_maximal_wrt"::: ) "X" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) ")" ); end; :: deftheorem defines :::"PosetMin"::: BAGORDER:def 12 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_bagorder :::"PosetMin"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b3")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) ")" )))); :: deftheorem defines :::"PosetMax"::: BAGORDER:def 13 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "st" (Bool (Bool (Bool "not" (Set (Var "X")) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "b3")) ($#r2_waybel_4 :::"is_maximal_wrt"::: ) (Set (Var "X")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) ")" )))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); func :::"FinOrd-Approx"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) means :: BAGORDER:def 14 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#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_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) : (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) ")" ) ")" ) "}" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#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_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) : (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) "}" ) ")" ) ")" ); end; :: deftheorem defines :::"FinOrd-Approx"::: BAGORDER:def 14 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#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_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) : (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) ")" ) "}" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#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_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) : (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "b2")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))) ")" ) "}" ) ")" ) ")" ) ")" ))); theorem :: BAGORDER:35 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")) ")" ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")) ")" ) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: BAGORDER:36 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "not" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")) ")" ) ")" )))))) ; theorem :: BAGORDER:37 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "holds" (Bool (Set (Set (Var "a")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "a")) ")" ) ($#k6_domain_1 :::"}"::: ) )) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))))))) ; theorem :: BAGORDER:38 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")) ")" ) ")" )) "is" ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ")" ))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); func :::"FinOrd"::: "R" -> ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ")" ) equals :: BAGORDER:def 15 (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) "R" ")" ) ")" )); end; :: deftheorem defines :::"FinOrd"::: BAGORDER:def 15 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k13_bagorder :::"FinOrd"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k12_bagorder :::"FinOrd-Approx"::: ) (Set (Var "R")) ")" ) ")" )))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); func :::"FinPoset"::: "R" -> ($#l1_orders_2 :::"Poset":::) equals :: BAGORDER:def 16 (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ")" ) "," (Set "(" ($#k13_bagorder :::"FinOrd"::: ) "R" ")" ) "#)" ); end; :: deftheorem defines :::"FinPoset"::: BAGORDER:def 16 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) "holds" (Bool (Set ($#k14_bagorder :::"FinPoset"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))) ")" ) "," (Set "(" ($#k13_bagorder :::"FinOrd"::: ) (Set (Var "R")) ")" ) "#)" ))); registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k14_bagorder :::"FinPoset"::: ) "R") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: BAGORDER:39 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_bagorder :::"FinPoset"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set "(" ($#k14_bagorder :::"FinPoset"::: ) (Set (Var "R")) ")" ))) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R")))) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "y")) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k11_bagorder :::"PosetMax"::: ) (Set (Var "y")) ")" ) ($#k6_domain_1 :::"}"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k13_bagorder :::"FinOrd"::: ) (Set (Var "R")))) ")" ) ")" ) ")" )) ")" ))) ; registrationlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::); cluster (Set ($#k14_bagorder :::"FinPoset"::: ) "R") -> ($#v16_waybel_0 :::"connected"::: ) ; end; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"RelStr"::: ) ; let "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; assume that (Bool (Set (Const "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) and (Bool (Set (Const "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "R")))) ; func :::"MinElement"::: "(" "C" "," "R" ")" -> ($#m1_subset_1 :::"Element":::) "of" "R" means :: BAGORDER:def 17 (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) "C") & (Bool it ($#r4_waybel_4 :::"is_minimal_wrt"::: ) "C" "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" "R")) ")" ); end; :: deftheorem defines :::"MinElement"::: BAGORDER:def 17 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"RelStr"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) ) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "R"))))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_bagorder :::"MinElement"::: ) "(" (Set (Var "C")) "," (Set (Var "R")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b3")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "b3")) ($#r4_waybel_4 :::"is_minimal_wrt"::: ) (Set (Var "C")) "," (Set "the" ($#u1_orders_2 :::"InternalRel"::: ) "of" (Set (Var "R")))) ")" ) ")" )))); theorem :: BAGORDER:40 (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")) (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "s")) "is" ($#v3_wellfnd1 :::"descending"::: ) )) "holds" (Bool (Set (Set (Var "s")) ($#k10_nat_1 :::"^\"::: ) (Set (Var "j"))) "is" ($#v3_wellfnd1 :::"descending"::: ) )))) ; theorem :: BAGORDER:41 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v16_waybel_0 :::"connected"::: ) ($#l1_orders_2 :::"Poset":::) "st" (Bool (Bool (Set (Var "R")) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) "holds" (Bool (Set ($#k14_bagorder :::"FinPoset"::: ) (Set (Var "R"))) "is" ($#v1_wellfnd1 :::"well_founded"::: ) )) ;