:: GROEB_3 semantic presentation begin theorem :: GROEB_3: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 (Set (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" ) ($#k1_groeb_2 :::"/"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "b1"))))) ; theorem :: GROEB_3:2 (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")) "," (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")))) "holds" (Bool (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) ($#r1_termord :::"<="::: ) (Set (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) "," (Set (Var "T")))))) ; theorem :: GROEB_3: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 "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")) ($#r2_termord :::"<"::: ) (Set (Var "b3")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "b1")) ($#r2_termord :::"<"::: ) (Set (Var "b3")) "," (Set (Var "T")))))) ; theorem :: GROEB_3:4 (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")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r2_termord :::"<"::: ) (Set (Var "b2")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) ($#r2_termord :::"<"::: ) (Set (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) "," (Set (Var "T")))))) ; theorem :: GROEB_3:5 (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")) "," (Set (Var "b3")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r2_termord :::"<"::: ) (Set (Var "b2")) "," (Set (Var "T"))) & (Bool (Set (Var "b3")) ($#r1_termord :::"<="::: ) (Set (Var "b4")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) ($#r2_termord :::"<"::: ) (Set (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b4"))) "," (Set (Var "T")))))) ; theorem :: GROEB_3:6 (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")) "," (Set (Var "b3")) "," (Set (Var "b4")) "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 "b3")) ($#r2_termord :::"<"::: ) (Set (Var "b4")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) ($#r2_termord :::"<"::: ) (Set (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b4"))) "," (Set (Var "T")))))) ; begin theorem :: GROEB_3:7 (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 "m1")) "," (Set (Var "m2")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom7 :::"term"::: ) (Set "(" (Set (Var "m1")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "m2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m1")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m2")) ")" )))))) ; theorem :: GROEB_3:8 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) "iff" (Bool (Set (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ))) ")" )))))) ; theorem :: GROEB_3:9 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" ) where b "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) : (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) "}" ))))) ; theorem :: GROEB_3:10 (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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) ")" ))))))) ; theorem :: GROEB_3:11 (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"::: ) "holds" (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; theorem :: GROEB_3:12 (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"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set (Var "q"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Var "q")))))) ; theorem :: GROEB_3:13 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (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"::: ) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )))) ; theorem :: GROEB_3:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (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 "f")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k6_polynom1 :::"-"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))))))) ; theorem :: GROEB_3: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 "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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); 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")); cluster (Set ($#k2_polynom1 :::"Support"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); :: original: :::"{"::: redefine func :::"{":::"p" "," "q":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" ); end; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "s" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "X")) "," (Set (Const "L")); let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "X")) ")" ); func "s" :::"|"::: "Y" -> ($#m1_subset_1 :::"Series":::) "of" "X" "," "L" equals :: GROEB_3:def 1 (Set "s" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_polynom1 :::"Support"::: ) "s" ")" ) ($#k4_xboole_0 :::"\"::: ) "Y" ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "L" ")" ) ")" )); end; :: deftheorem defines :::"|"::: GROEB_3:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "s")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set (Var "Y")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ")" ))))))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); 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")); let "Y" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n")) ")" ); cluster (Set "p" ($#k2_groeb_3 :::"|"::: ) "Y") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; theorem :: GROEB_3:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "X")) ")" ) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "s")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set (Var "Y")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set (Var "Y")) ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")))) ")" ) ")" ))))) ; theorem :: GROEB_3:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "Y")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "X")) ")" ) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set (Var "Y")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "s")))))))) ; theorem :: GROEB_3:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "s")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "s")) ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k1_subset_1 :::"{}"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "X")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; 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")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool (Set (Const "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Const "p")) ")" ))) ; func :::"Upper_Support"::: "(" "p" "," "T" "," "i" ")" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) means :: GROEB_3:def 2 (Bool "(" (Bool it ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) "p")) & (Bool (Set ($#k5_card_1 :::"card"::: ) it) ($#r1_hidden :::"="::: ) "i") & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) it) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) "p")) & (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b9")) "," "T")) "holds" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) it) ")" ) ")" ); end; :: deftheorem defines :::"Upper_Support"::: GROEB_3:def 2 : (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set (Var "b6")) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "b6"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "b6"))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b9")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "b6"))) ")" ) ")" ) ")" ))))))); 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")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Lower_Support"::: "(" "p" "," "T" "," "i" ")" -> ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) equals :: GROEB_3:def 3 (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" "p" "," "T" "," "i" ")" ")" )); end; :: deftheorem defines :::"Lower_Support"::: GROEB_3:def 3 : (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))))))); theorem :: GROEB_3: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" ($#~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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))))) ; theorem :: GROEB_3: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" ($#~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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ))) "holds" (Bool (Set (Var "b9")) ($#r2_termord :::"<"::: ) (Set (Var "b")) "," (Set (Var "T"))))))))) ; theorem :: GROEB_3: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" ($#~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 "(" (Bool (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) ")" ))))) ; theorem :: GROEB_3: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" ($#~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 "(" (Bool (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))))) ; theorem :: GROEB_3: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" ($#~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" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ))))))) ; theorem :: GROEB_3: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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")))) & (Bool "(" "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set (Var "b9")) ($#r1_termord :::"<="::: ) (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) ")" ) ")" )))))) ; 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")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Up"::: "(" "p" "," "T" "," "i" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" equals :: GROEB_3:def 4 (Set "p" ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" "p" "," "T" "," "i" ")" ")" )); func :::"Low"::: "(" "p" "," "T" "," "i" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" equals :: GROEB_3:def 5 (Set "p" ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k4_groeb_3 :::"Lower_Support"::: ) "(" "p" "," "T" "," "i" ")" ")" )); end; :: deftheorem defines :::"Up"::: GROEB_3:def 4 : (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))))))); :: deftheorem defines :::"Low"::: GROEB_3:def 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 "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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k2_groeb_3 :::"|"::: ) (Set "(" ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))))))); theorem :: GROEB_3: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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_groeb_3 :::"Upper_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) & (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_groeb_3 :::"Lower_Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" )) ")" )))))) ; theorem :: GROEB_3: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" ($#~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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) & (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) ")" )))))) ; theorem :: GROEB_3: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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )))))))) ; theorem :: GROEB_3: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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (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 "(" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))) "or" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))) ")" ) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ")" )))) ")" ))))))) ; theorem :: GROEB_3:29 (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))) & (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool (Set (Var "b")) ($#r2_termord :::"<"::: ) (Set (Var "b9")) "," (Set (Var "T"))))))))) ; theorem :: GROEB_3:30 (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))))))) ; theorem :: GROEB_3:31 (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (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 "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ))))))) ; theorem :: GROEB_3:32 (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (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 "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ))))))) ; theorem :: GROEB_3:33 (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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Set "(" ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))))) ; theorem :: GROEB_3:34 (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 "(" (Bool (Set ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))) ")" ))))) ; theorem :: GROEB_3: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))) & (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ))))) ; theorem :: GROEB_3: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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k5_groeb_3 :::"Up"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Num 1) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )) & (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Num 1) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_termord :::"Red"::: ) "(" (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"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p" be ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k5_groeb_3 :::"Up"::: ) "(" "p" "," "T" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) -> ($#v3_polynom7 :::"monomial-like"::: ) ; end; 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"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set ($#k5_groeb_3 :::"Up"::: ) "(" "p" "," "T" "," (Num 1) ")" ) -> ($#v1_polynom7 :::"non-zero"::: ) ($#v3_polynom7 :::"monomial-like"::: ) ; cluster (Set ($#k6_groeb_3 :::"Low"::: ) "(" "p" "," "T" "," (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) ")" ) ")" ) -> ($#v3_polynom7 :::"monomial-like"::: ) ; end; theorem :: GROEB_3: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")) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) "holds" (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "j")) ")" ) "is" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")))))))) ; theorem :: GROEB_3:38 (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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "T")) ")" ) "," (Set (Var "T")))))))) ; theorem :: GROEB_3: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" ($#~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")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r2_termord :::"<"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) "," (Set (Var "T")))))))) ; theorem :: GROEB_3:40 (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")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))) "iff" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))) ")" )))))))) ; theorem :: GROEB_3:41 (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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" )))))))) ; theorem :: GROEB_3:42 (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"::: ) ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "T")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: GROEB_3:43 (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"::: ) ($#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 "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k6_termord :::"Red"::: ) "(" (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ) "," (Set (Var "T")) ")" ))))))) ; theorem :: GROEB_3:44 (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")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set ($#k6_groeb_3 :::"Low"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) "," (Set (Var "i")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set "(" ($#k6_groeb_3 :::"Low"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) "," (Set (Var "i")) ")" ")" ))))))))) ; begin theorem :: GROEB_3:45 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r4_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "T")))) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) ($#r4_polyred :::"reduces_to"::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "g"))) "," (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: GROEB_3:46 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "g")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "f1")) "," (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T"))) & (Bool "(" "for" (Set (Var "b1")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g"))))) "holds" (Bool "not" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b1")))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k5_polynom1 :::"+"::: ) (Set (Var "g"))) ($#r5_polyred :::"reduces_to"::: ) (Set (Set (Var "f1")) ($#k5_polynom1 :::"+"::: ) (Set (Var "g"))) "," (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T"))))))) ; theorem :: GROEB_3:47 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "f")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g"))) ($#r5_polyred :::"reduces_to"::: ) (Set (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g"))) "," (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "g")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T"))))))) ; theorem :: GROEB_3:48 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "f")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g")) ")" ) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g")) ")" ) ($#k5_polynom1 :::"+"::: ) (Set (Var "p"))) ($#r5_polyred :::"reduces_to"::: ) (Set (Set "(" (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g")) ")" ) ($#k5_polynom1 :::"+"::: ) (Set (Var "p"))) "," (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "g")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")))))))) ; theorem :: GROEB_3:49 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) "," (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "g"))))))))) ; theorem :: GROEB_3:50 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f1")) "," (Set (Var "g")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "f1"))) & (Bool "(" "for" (Set (Var "b1")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g"))))) "holds" (Bool "not" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b1")))) ")" )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "f")) ($#k5_polynom1 :::"+"::: ) (Set (Var "g"))) "," (Set (Set (Var "f1")) ($#k5_polynom1 :::"+"::: ) (Set (Var "g")))))))) ; theorem :: GROEB_3:51 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "g")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "f")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g"))) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))))) ; begin theorem :: GROEB_3:52 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) "holds" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ))) & (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" )))) "holds" (Bool "not" (Bool (Set (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b1")))))))))) ; theorem :: GROEB_3:53 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) "holds" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" ))))))) ; theorem :: GROEB_3:54 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) "holds" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p2")) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p1")) ")" ))))))) ; theorem :: GROEB_3:55 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) ) & (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "is" ($#v1_polynom7 :::"non-zero"::: ) ) & (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) "is" ($#v1_polynom7 :::"non-zero"::: ) )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p1")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" ($#k5_termord :::"HM"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" )) "," (Set (Set (Var "p2")) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k6_termord :::"Red"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: GROEB_3:56 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_3 :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k1_groeb_3 :::"}"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))))) ; theorem :: GROEB_3:57 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T")))) "holds" (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Bool "not" (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) ))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "T")) ")" ) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))))) ; theorem :: GROEB_3:58 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Bool "not" (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Bool "not" (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) ))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "T")) ")" ) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Bool "not" (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) & (Bool (Set (Var "h")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))))) ; theorem :: GROEB_3:59 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Bool "not" (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "g1")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "g2")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Bool "not" (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g1")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g2")) "," (Set (Var "T")) ")" ) ($#r1_groeb_2 :::"are_disjoint"::: ) )) & (Bool (Set (Var "h")) ($#r4_rewrite1 :::"is_a_normal_form_of"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "T")) ")" ) "," (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" )) "holds" (Bool (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T"))))))) ;