:: TERMORD semantic presentation begin registration cluster ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); attr "b" is :::"zero"::: means :: TERMORD:def 1 (Bool "b" ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) "X")); end; :: deftheorem defines :::"zero"::: TERMORD:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b")) "is" ($#v1_termord :::"zero"::: ) ) "iff" (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))) ")" ))); theorem :: TERMORD:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "b2")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b"))))) ")" ))) ; theorem :: TERMORD:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m1", "m2" be ($#m1_subset_1 :::"Monomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "m1" ($#k9_polynom1 :::"*'"::: ) "m2") -> ($#v3_polynom7 :::"monomial-like"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "c1", "c2" be ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "c1" ($#k9_polynom1 :::"*'"::: ) "c2") -> ($#v4_polynom7 :::"Constant"::: ) ; end; theorem :: TERMORD:3 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "being" ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a9")) ")" ) "," (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b9")) ")" ) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a9")) "," (Set (Var "b9")) ")" ")" ))))))) ; theorem :: TERMORD:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a9")) ")" ) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set "(" (Set (Var "a9")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )))))) ; begin 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"::: ) ($#v6_relat_2 :::"connected"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v2_bagorder :::"admissible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ))))); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster ($#v1_partfun1 :::"total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v2_bagorder :::"admissible"::: ) -> ($#v1_wellord1 :::"well_founded"::: ) ($#v2_bagorder :::"admissible"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ))))); end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "b", "b9" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "b" :::"<="::: "b9" "," "T" means :: TERMORD:def 2 (Bool (Set ($#k4_tarski :::"["::: ) "b" "," "b9" ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "T"); end; :: deftheorem defines :::"<="::: TERMORD:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b9")) "," (Set (Var "T"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "b9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" )))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "b", "b9" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "b" :::"<"::: "b9" "," "T" means :: TERMORD:def 3 (Bool "(" (Bool "b" ($#r1_termord :::"<="::: ) "b9" "," "T") & (Bool "b" ($#r1_hidden :::"<>"::: ) "b9") ")" ); end; :: deftheorem defines :::"<"::: TERMORD:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_termord :::"<"::: ) (Set (Var "b9")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b9")) "," (Set (Var "T"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set (Var "b9"))) ")" ) ")" )))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); func :::"min"::: "(" "b1" "," "b2" "," "T" ")" -> ($#m1_hidden :::"bag":::) "of" "n" equals :: TERMORD:def 4 "b1" if (Bool "b1" ($#r1_termord :::"<="::: ) "b2" "," "T") otherwise "b2"; func :::"max"::: "(" "b1" "," "b2" "," "T" ")" -> ($#m1_hidden :::"bag":::) "of" "n" equals :: TERMORD:def 5 "b1" if (Bool "b2" ($#r1_termord :::"<="::: ) "b1" "," "T") otherwise "b2"; end; :: deftheorem defines :::"min"::: TERMORD:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T")))) "implies" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T"))))) "implies" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" ")" )))); :: deftheorem defines :::"max"::: TERMORD: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")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "b2")) ($#r1_termord :::"<="::: ) (Set (Var "b1")) "," (Set (Var "T")))) "implies" (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "b2")) ($#r1_termord :::"<="::: ) (Set (Var "b1")) "," (Set (Var "T"))))) "implies" (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" ")" )))); theorem :: TERMORD:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T"))) "iff" (Bool (Bool "not" (Set (Var "b2")) ($#r2_termord :::"<"::: ) (Set (Var "b1")) "," (Set (Var "T")))) ")" )))) ; theorem :: TERMORD:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b")) "," (Set (Var "T")))))) ; theorem :: TERMORD:7 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T"))) & (Bool (Set (Var "b2")) ($#r1_termord :::"<="::: ) (Set (Var "b1")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "b1")) ($#r6_pboole :::"="::: ) (Set (Var "b2")))))) ; theorem :: TERMORD:8 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T"))) & (Bool (Set (Var "b2")) ($#r1_termord :::"<="::: ) (Set (Var "b3")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b3")) "," (Set (Var "T")))))) ; theorem :: TERMORD:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))) ($#r1_termord :::"<="::: ) (Set (Var "b")) "," (Set (Var "T")))))) ; theorem :: TERMORD:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T")))))) ; theorem :: TERMORD:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) "or" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b2"))) ")" )))) ; theorem :: TERMORD:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) "or" (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b2"))) ")" )))) ; theorem :: TERMORD:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set (Var "b1")) "," (Set (Var "T"))) & (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set (Var "b2")) "," (Set (Var "T"))) ")" )))) ; theorem :: TERMORD:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_termord :::"<="::: ) (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) & (Bool (Set (Var "b2")) ($#r1_termord :::"<="::: ) (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) ")" )))) ; theorem :: TERMORD:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) "," (Set (Var "T")) ")" )) & (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) "," (Set (Var "T")) ")" )) ")" )))) ; theorem :: TERMORD:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k1_termord :::"min"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) "iff" (Bool (Set ($#k2_termord :::"max"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b2"))) ")" )))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"HT"::: "(" "p" "," "T" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "n") means :: TERMORD:def 6 (Bool "(" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) "p") ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool it ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) "n")) ")" ) "or" (Bool "(" (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) "p")) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) "p"))) "holds" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) it "," "T") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"HT"::: TERMORD:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )) "iff" (Bool "(" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "b5")) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) ")" ) "or" (Bool "(" (Bool (Set (Var "b5")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b5")) "," (Set (Var "T"))) ")" ) ")" ) ")" ) ")" )))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"HC"::: "(" "p" "," "T" ")" -> ($#m1_subset_1 :::"Element":::) "of" "L" equals :: TERMORD:def 7 (Set "p" ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" "p" "," "T" ")" ")" )); end; :: deftheorem defines :::"HC"::: TERMORD:def 7 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ))))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"HM"::: "(" "p" "," "T" ")" -> ($#m1_subset_1 :::"Monomial":::) "of" "n" "," "L" equals :: TERMORD:def 8 (Set ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" "p" "," "T" ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" "p" "," "T" ")" ")" ) ")" ); end; :: deftheorem defines :::"HM"::: TERMORD:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_polynom7 :::"Monom"::: ) "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ")" )))))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k5_termord :::"HM"::: ) "(" "p" "," "T" ")" ) -> ($#v1_polynom7 :::"non-zero"::: ) ; cluster (Set ($#k4_termord :::"HC"::: ) "(" "p" "," "T" ")" ) -> ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ; end; theorem :: TERMORD:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) "iff" (Bool (Set (Var "p")) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ))))) ; theorem :: TERMORD:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: TERMORD:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))))) ; theorem :: TERMORD:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))))))) ; theorem :: TERMORD:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k1_tarski :::"}"::: ) )) ")" ))))) ; theorem :: TERMORD:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r6_pboole :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )) & (Bool (Set ($#k3_polynom7 :::"coefficient"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )) ")" ))))) ; theorem :: TERMORD:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "m")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k2_polynom7 :::"term"::: ) (Set (Var "m")))) & (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "m")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polynom7 :::"coefficient"::: ) (Set (Var "m")))) & (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "m")) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set (Var "m"))) ")" ))))) ; theorem :: TERMORD:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"ConstPoly":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "c")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) & (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "c")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ))) ")" ))))) ; theorem :: TERMORD:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) & (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))))) ; theorem :: TERMORD:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; theorem :: TERMORD:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; theorem :: TERMORD:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; theorem :: TERMORD:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: TERMORD:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) "{" (Set "(" (Set (Var "s")) ($#k11_pre_poly :::"+"::: ) (Set (Var "t")) ")" ) where s, t "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) : (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "q")))) ")" ) "}" )))) ; theorem :: TERMORD:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: TERMORD:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: TERMORD:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: TERMORD:34 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k2_termord :::"max"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"Red"::: "(" "p" "," "T" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" equals :: TERMORD:def 9 (Set "p" ($#k6_polynom1 :::"-"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" "p" "," "T" ")" ")" )); end; :: deftheorem defines :::"Red"::: TERMORD:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ))))))); theorem :: TERMORD:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))))))) ; theorem :: TERMORD:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: TERMORD:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))))))) ; theorem :: TERMORD:38 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set (Var "p"))))))) ; theorem :: TERMORD:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))))) ; theorem :: TERMORD:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))))))))) ;