:: GROEB_2 semantic presentation begin theorem :: GROEB_2:1 (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" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" )))))) ; theorem :: GROEB_2:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k2_finseq_7 :::"Swap"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "j")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "f"))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); assume (Bool (Set (Const "b2")) ($#r3_pre_poly :::"divides"::: ) (Set (Const "b1"))) ; func "b1" :::"/"::: "b2" -> ($#m1_hidden :::"bag":::) "of" "X" means :: GROEB_2:def 1 (Bool (Set "b2" ($#k11_pre_poly :::"+"::: ) it) ($#r6_pboole :::"="::: ) "b1"); end; :: deftheorem defines :::"/"::: GROEB_2:def 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")) "st" (Bool (Bool (Set (Var "b2")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b1")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_groeb_2 :::"/"::: ) (Set (Var "b2")))) "iff" (Bool (Set (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b4"))) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); func :::"lcm"::: "(" "b1" "," "b2" ")" -> ($#m1_hidden :::"bag":::) "of" "X" means :: GROEB_2:def 2 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" "b1" ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" "b2" ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ))); commutativity (Bool "for" (Set (Var "b1")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "X")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )))) ; idempotence (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "X")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) ")" )))) ; end; :: deftheorem defines :::"lcm"::: GROEB_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b4")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" )) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) "," (Set "(" (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "k")) ")" ) ")" ))) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); synonym "b1" :::"lcm"::: "b2" for :::"lcm"::: "(" "b1" "," "b2" ")" ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); pred "b1" "," "b2" :::"are_disjoint"::: means :: GROEB_2:def 3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set "b1" ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set "b2" ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); end; :: deftheorem defines :::"are_disjoint"::: GROEB_2:def 3 : (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")) "," (Set (Var "b2")) ($#r1_groeb_2 :::"are_disjoint"::: ) ) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Set (Var "b2")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))); notationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); antonym "b1" "," "b2" :::"are_non_disjoint"::: for "b1" "," "b2" :::"are_disjoint"::: ; end; theorem :: GROEB_2:3 (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 ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" )) & (Bool (Set (Var "b2")) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" )) ")" ))) ; theorem :: GROEB_2:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b3"))) & (Bool (Set (Var "b2")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b3")))) "holds" (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b3"))))) ; theorem :: GROEB_2:5 (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")) "," (Set (Var "b2")) ($#r1_groeb_2 :::"are_disjoint"::: ) ) "iff" (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")))) ")" ))) ; theorem :: GROEB_2:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b")) ($#k1_groeb_2 :::"/"::: ) (Set (Var "b"))) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))))) ; theorem :: GROEB_2:7 (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 "b2")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b1"))) "iff" (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) ")" ))) ; theorem :: GROEB_2:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" ))) "holds" (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" )))) ; theorem :: GROEB_2:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b1")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" ))) "holds" (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b3")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" )))) ; theorem :: GROEB_2:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b1")) "," (Set (Var "b3")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" ))) "holds" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set (Var "b2")) "," (Set (Var "b3")) ")" )))) ; theorem :: GROEB_2:11 (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 "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool "(" "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set (Var "b9")) "," (Set (Var "T"))) ")" ) ")" ))))) ; registrationlet "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 "a" be ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k4_algstr_0 :::"-"::: ) "a") -> ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "m" be ($#m1_subset_1 :::"Monomial":::) "of" (Set (Const "X")) "," (Set (Const "L")); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "a" ($#k5_polynom7 :::"*"::: ) "m") -> ($#v3_polynom7 :::"monomial-like"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p" be ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "a" be ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set "a" ($#k5_polynom7 :::"*"::: ) "p") -> ($#v1_polynom7 :::"non-zero"::: ) ; end; theorem :: GROEB_2:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: GROEB_2:13 (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"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: GROEB_2:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: GROEB_2:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: GROEB_2:16 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k4_polynom7 :::"|"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; begin theorem :: GROEB_2:17 (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 "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) & (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set "(" (Set (Var "m1")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p1")) ")" ) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k5_termord :::"HM"::: ) "(" (Set "(" (Set (Var "m2")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p2")) ")" ) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set "(" (Set (Var "m1")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p1")) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set (Var "m2")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p2")) ")" )) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) ")" )) "holds" (Bool (Set (Var "P")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (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 ($#~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"::: ) ; let "p1", "p2" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"S-Poly"::: "(" "p1" "," "p2" "," "T" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" equals :: GROEB_2:def 4 (Set (Set "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" "p2" "," "T" ")" ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_groeb_2 :::"lcm"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" "p1" "," "T" ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" "p2" "," "T" ")" ")" ) ")" ")" ) ($#k1_groeb_2 :::"/"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" "p1" "," "T" ")" ")" ) ")" ) ($#k1_polyred :::"*'"::: ) "p1" ")" ) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" "p1" "," "T" ")" ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_groeb_2 :::"lcm"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" "p1" "," "T" ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" "p2" "," "T" ")" ")" ) ")" ")" ) ($#k1_groeb_2 :::"/"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" "p2" "," "T" ")" ")" ) ")" ) ($#k1_polyred :::"*'"::: ) "p2" ")" ) ")" )); end; :: deftheorem defines :::"S-Poly"::: GROEB_2: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" ($#~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")) "holds" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_groeb_2 :::"lcm"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" ")" ) ($#k1_groeb_2 :::"/"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k1_polyred :::"*'"::: ) (Set (Var "p1")) ")" ) ")" ) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k2_groeb_2 :::"lcm"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" ")" ) ($#k1_groeb_2 :::"/"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k1_polyred :::"*'"::: ) (Set (Var "p2")) ")" ) ")" ))))))); theorem :: GROEB_2: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"::: ) ) ($#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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))))))) ; theorem :: GROEB_2: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"::: ) ) ($#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 "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "m1")) "," (Set (Var "m2")) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))))) ; theorem :: GROEB_2: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"::: ) ) ($#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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "," (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ))))) ; theorem :: GROEB_2:21 (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")) "holds" (Bool "(" (Bool (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) "or" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r2_termord :::"<"::: ) (Set ($#k2_groeb_2 :::"lcm"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ")" ) "," (Set (Var "T"))) ")" ))))) ; theorem :: GROEB_2: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"::: ) ) ($#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" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p1")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) ($#k5_polynom7 :::"*"::: ) (Set (Var "p1"))) ($#r8_polyred :::"top_reduces_to"::: ) (Set ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ) "," (Set (Var "p2")) "," (Set (Var "T"))))))) ; theorem :: GROEB_2:23 (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")) "," (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 (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")) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))))) ; theorem :: GROEB_2:24 (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 "(" "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 (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")) ($#r8_pboole :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" )) "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")))) "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_2:25 (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")) "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")))) "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 (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (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 ($#~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"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); func :::"S-Poly"::: "(" "P" "," "T" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" ) equals :: GROEB_2:def 5 "{" (Set "(" ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," "T" ")" ")" ) where p1, p2 "is" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" : (Bool "(" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) "P") ")" ) "}" ; end; :: deftheorem defines :::"S-Poly"::: GROEB_2: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" ($#~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 "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool (Set ($#k4_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_groeb_2 :::"S-Poly"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "T")) ")" ")" ) where p1, p2 "is" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) : (Bool "(" (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) ")" ) "}" ))))); 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"::: ) ($#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"::: ) ; let "P" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); cluster (Set ($#k4_groeb_2 :::"S-Poly"::: ) "(" "P" "," "T" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: GROEB_2:26 (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 "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))) ")" )) "holds" (Bool (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T"))))))) ; begin theorem :: GROEB_2:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i"))) "is" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P"))))))) ; theorem :: GROEB_2:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "A")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i"))) "is" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P"))))))) ; theorem :: GROEB_2:29 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set (Var "A")) "is" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "Q")))))) ; 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" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); let "A", "B" be ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Const "P")); :: original: :::"^"::: redefine func "A" :::"^"::: "B" -> ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" "P"; 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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); let "A" be ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Const "P")); pred "A" :::"is_MonomialRepresentation_of"::: "f" means :: GROEB_2:def 6 (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) "A") ($#r1_hidden :::"="::: ) "f") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "A"))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" "n" "," "L"(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_MonomialRepresentation_of"::: GROEB_2:def 6 : (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "f"))) "iff" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))(Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) ")" ))) ")" ) ")" ) ")" )))))); theorem :: GROEB_2:30 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "A")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) ")" ) where m "is" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")), p "is" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) : (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) ")" )) "}" ))))))) ; theorem :: GROEB_2:31 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "A")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "f"))) & (Bool (Set (Var "B")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "A")) ($#k5_groeb_2 :::"^"::: ) (Set (Var "B"))) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Set (Var "f")) ($#k4_polynom1 :::"+"::: ) (Set (Var "g"))))))))) ; 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"::: ) ) ($#~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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); let "A" be ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Const "P")); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "A" :::"is_Standard_Representation_of"::: "f" "," "P" "," "b" "," "T" means :: GROEB_2:def 7 (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) "A") ($#r1_hidden :::"="::: ) "f") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "A"))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" "n" "," "L"(Bool "ex" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set "A" ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," "T" ")" ) ($#r1_termord :::"<="::: ) "b" "," "T") ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_Standard_Representation_of"::: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A"))))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))(Bool "ex" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set (Var "b")) "," (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"::: ) ) ($#~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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); let "A" be ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Const "P")); pred "A" :::"is_Standard_Representation_of"::: "f" "," "P" "," "T" means :: GROEB_2:def 8 (Bool "A" ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) "f" "," "P" "," (Set ($#k3_termord :::"HT"::: ) "(" "f" "," "T" ")" ) "," "T"); end; :: deftheorem defines :::"is_Standard_Representation_of"::: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r4_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "T"))) "iff" (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "," (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"::: ) ) ($#~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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "f" :::"has_a_Standard_Representation_of"::: "P" "," "b" "," "T" means :: GROEB_2:def 9 (Bool "ex" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" "P" "st" (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) "f" "," "P" "," "b" "," "T")); end; :: deftheorem defines :::"has_a_Standard_Representation_of"::: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r5_groeb_2 :::"has_a_Standard_Representation_of"::: ) (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (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"::: ) ) ($#~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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "f" :::"has_a_Standard_Representation_of"::: "P" "," "T" means :: GROEB_2:def 10 (Bool "ex" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" "P" "st" (Bool (Set (Var "A")) ($#r4_groeb_2 :::"is_Standard_Representation_of"::: ) "f" "," "P" "," "T")); end; :: deftheorem defines :::"has_a_Standard_Representation_of"::: GROEB_2:def 10 : (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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r6_groeb_2 :::"has_a_Standard_Representation_of"::: ) (Set (Var "P")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Set (Var "A")) ($#r4_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "T")))) ")" )))))); theorem :: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "A")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "f")))))))))) ; theorem :: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))) & (Bool (Set (Var "B")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "g")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "A")) ($#k5_groeb_2 :::"^"::: ) (Set (Var "B"))) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Set (Var "f")) ($#k4_polynom1 :::"+"::: ) (Set (Var "g"))) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T")))))))))) ; theorem :: GROEB_2: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"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "A")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Var "B")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))))))))))) ; theorem :: GROEB_2: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"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "A")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "i")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "A")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "B")) ($#r3_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) "," (Set (Var "P")) "," (Set (Var "b")) "," (Set (Var "T"))))))))))) ; theorem :: GROEB_2: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "A")) ($#r2_groeb_2 :::"is_MonomialRepresentation_of"::: ) (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))(Bool "ex" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) ")" )))))))))) ; theorem :: GROEB_2: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~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"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "A")) "being" ($#m2_ideal_1 :::"LeftLinearCombination"::: ) "of" (Set (Var "P")) "st" (Bool (Bool (Set (Var "A")) ($#r4_groeb_2 :::"is_Standard_Representation_of"::: ) (Set (Var "f")) "," (Set (Var "P")) "," (Set (Var "T")))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L"))(Bool "ex" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "A")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" )) ")" )))))))))) ; theorem :: GROEB_2: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"::: ) ) ($#~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 "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (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 ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r6_groeb_2 :::"has_a_Standard_Representation_of"::: ) (Set (Var "P")) "," (Set (Var "T")))))))) ; theorem :: GROEB_2:39 (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 "f")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r6_groeb_2 :::"has_a_Standard_Representation_of"::: ) (Set (Var "P")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T")))))))) ; theorem :: GROEB_2:40 (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" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T"))) "iff" (Bool "for" (Set (Var "f")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "G")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r6_groeb_2 :::"has_a_Standard_Representation_of"::: ) (Set (Var "G")) "," (Set (Var "T")))) ")" ))))) ;