:: GROEB_1 semantic presentation begin 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 ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); :: original: :::"{"::: redefine func :::"{":::"p":::"}"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" ); end; theorem :: GROEB_1:1 (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 "f")) "," (Set (Var "p")) "," (Set (Var "g")) "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 "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: GROEB_1:2 (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")) "," (Set (Var "p")) "," (Set (Var "g")) "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 "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ))) & (Bool (Bool "not" (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g"))))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) ")" )))))) ; theorem :: GROEB_1: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" ($#~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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q"))) & (Bool (Set (Var "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "P")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "Q")) "," (Set (Var "T")))))))) ; theorem :: GROEB_1: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 "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "Q")) "," (Set (Var "T")) ")" )))))) ; theorem :: GROEB_1:5 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))))))) ; theorem :: GROEB_1:6 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r6_pboole :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; theorem :: GROEB_1:7 (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"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set (Var "q")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k2_termord :::"max"::: ) "(" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))))))) ; theorem :: GROEB_1:8 (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 "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "q"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: GROEB_1:9 (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"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r6_polyred :::"is_reducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T")))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))))))) ; begin theorem :: GROEB_1:10 (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" ($#~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 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ))))) ; theorem :: GROEB_1: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 "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 "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 "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) ($#k7_ideal_1 :::"-Ideal"::: ) )) ")" ))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ))))) ; 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 "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); func :::"HT"::: "(" "P" "," "T" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) equals :: GROEB_1:def 1 "{" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," "T" ")" ")" ) where p "is" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" : (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "L" ")" )) ")" ) "}" ; end; :: deftheorem defines :::"HT"::: GROEB_1:def 1 : (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 "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) where p "is" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) : (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ) "}" ))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "S" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n")) ")" ); func :::"multiples"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) equals :: GROEB_1:def 2 "{" (Set (Var "b")) where b "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "n") : (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) "S") & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" )) "}" ; end; :: deftheorem defines :::"multiples"::: GROEB_1:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k3_groeb_1 :::"multiples"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "b")) where b "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) : (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" )) "}" ))); theorem :: GROEB_1:12 (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 (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v7_rewrite1 :::"confluent"::: ) ))))) ; theorem :: GROEB_1:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "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")) ")" ")" ) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v7_rewrite1 :::"confluent"::: ) )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v4_rewrite1 :::"with_UN_property"::: ) ))))) ; theorem :: GROEB_1:14 (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 (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v4_rewrite1 :::"with_UN_property"::: ) )) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) ))))) ; theorem :: GROEB_1:15 (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" ($#~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")) ")" ) "is" ($#v8_rewrite1 :::"with_Church-Rosser_property"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (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")) ")" ))))))) ; theorem :: GROEB_1:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "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")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (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 "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 "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r7_polyred :::"is_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T")))))))) ; theorem :: GROEB_1: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 "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 "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r7_polyred :::"is_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T"))) ")" )) "holds" (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 "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T")))))))) ; theorem :: GROEB_1: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"::: ) ($#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 "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 "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T"))) ")" )) "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_groeb_1 :::"HT"::: ) "(" (Set "(" (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ")" ) "," (Set (Var "T")) ")" ))) "holds" (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" )) & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" ))))))) ; theorem :: GROEB_1: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 "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set "(" (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ")" ) "," (Set (Var "T")) ")" ))) "holds" (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" )) & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" )) ")" )) "holds" (Bool (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set "(" (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ")" ) "," (Set (Var "T")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_groeb_1 :::"multiples"::: ) (Set "(" ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: GROEB_1:20 (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 (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set "(" (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ")" ) "," (Set (Var "T")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_groeb_1 :::"multiples"::: ) (Set "(" ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ")" )))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ))))) ; 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 "G" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "G" :::"is_Groebner_basis_wrt"::: "T" means :: GROEB_1:def 3 (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" "G" "," "T" ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ); end; :: deftheorem defines :::"is_Groebner_basis_wrt"::: GROEB_1: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" ($#~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 "G")) "being" ($#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 (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) ")" ))))); 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 "G", "I" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "G" :::"is_Groebner_basis_of"::: "I" "," "T" means :: GROEB_1:def 4 (Bool "(" (Bool (Set "G" ($#k7_ideal_1 :::"-Ideal"::: ) ) ($#r1_hidden :::"="::: ) "I") & (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" "G" "," "T" ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) ")" ); end; :: deftheorem defines :::"is_Groebner_basis_of"::: GROEB_1: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 "G")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool (Set (Set (Var "G")) ($#k7_ideal_1 :::"-Ideal"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) "is" ($#v9_rewrite1 :::"locally-confluent"::: ) ) ")" ) ")" ))))); theorem :: GROEB_1:21 (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")) "," (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 "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "P")) "," (Set (Var "T")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) "is" ($#m2_rewrite1 :::"Completion"::: ) "of" (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" )))))) ; theorem :: GROEB_1:22 (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")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (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")) ")" ")" ) "st" (Bool (Bool (Set (Var "G")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T")))) "holds" (Bool "(" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Set (Var "G")) ($#k7_ideal_1 :::"-Ideal"::: ) )) "iff" (Bool (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "p")) "," (Set "(" ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_rewrite1 :::"nf"::: ) "(" (Set (Var "q")) "," (Set "(" ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ")" ) ")" )) ")" )))))) ; theorem :: GROEB_1: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 "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 (Var "P")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T")))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) )) "iff" (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")) ")" )) ")" )))))) ; theorem :: GROEB_1: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 "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (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")) ")" ")" ) "st" (Bool (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))))))) ; theorem :: GROEB_1: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" ($#~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 "G")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" )) "holds" (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 (Var "I")))) "holds" (Bool (Set (Var "f")) ($#r7_polyred :::"is_reducible_wrt"::: ) (Set (Var "G")) "," (Set (Var "T")))))))) ; theorem :: GROEB_1: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 "I")) "being" ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (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_tarski :::"c="::: ) (Set (Var "I"))) & (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 (Var "I")))) "holds" (Bool (Set (Var "f")) ($#r7_polyred :::"is_reducible_wrt"::: ) (Set (Var "G")) "," (Set (Var "T"))) ")" )) "holds" (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 (Var "I")))) "holds" (Bool (Set (Var "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "G")) "," (Set (Var "T"))))))))) ; theorem :: GROEB_1: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"::: ) ($#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 "G")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (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 (Var "I")))) "holds" (Bool (Set (Var "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "G")) "," (Set (Var "T"))) ")" )) "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_groeb_1 :::"HT"::: ) "(" (Set (Var "I")) "," (Set (Var "T")) ")" ))) "holds" (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" )) & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" ))))))) ; theorem :: GROEB_1: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" ($#~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 "G")) "," (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "I")) "," (Set (Var "T")) ")" ))) "holds" (Bool "ex" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" )) & (Bool (Set (Var "b9")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" )) ")" )) "holds" (Bool (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "I")) "," (Set (Var "T")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_groeb_1 :::"multiples"::: ) (Set "(" ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ")" ))))))) ; theorem :: GROEB_1:29 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (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")) ")" ")" ) "st" (Bool (Bool (Set (Var "G")) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) & (Bool (Set ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "I")) "," (Set (Var "T")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_groeb_1 :::"multiples"::: ) (Set "(" ($#k2_groeb_1 :::"HT"::: ) "(" (Set (Var "G")) "," (Set (Var "T")) ")" ")" )))) "holds" (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T")))))))) ; begin theorem :: GROEB_1:30 (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" ($#~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"::: ) "holds" (Bool (Set ($#k1_groeb_1 :::"{"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k1_groeb_1 :::"}"::: ) ) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k1_groeb_1 :::"}"::: ) ) "," (Set (Var "T")))))) ; theorem :: GROEB_1:31 (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" ($#~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 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) ) ($#k7_ideal_1 :::"-Ideal"::: ) ) "," (Set (Var "T"))))))) ; theorem :: GROEB_1:32 (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (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 ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "I"))) & (Bool (Set (Var "P")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "L")) ")" ")" ) ($#k1_groeb_1 :::"}"::: ) ))) "holds" (Bool (Set (Var "P")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))))))) ; theorem :: GROEB_1:33 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#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"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "not" (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 (Var "P")) ($#r1_groeb_1 :::"is_Groebner_basis_wrt"::: ) (Set (Var "T")))))))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); func :::"DivOrder"::: "n" -> ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) means :: GROEB_1:def 5 (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2"))) ")" )); end; :: deftheorem defines :::"DivOrder"::: GROEB_1:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_groeb_1 :::"DivOrder"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2"))) ")" )) ")" ))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "(" ($#k4_groeb_1 :::"DivOrder"::: ) "n" ")" ) "#)" ) -> ($#v4_dickson :::"Dickson"::: ) ; end; theorem :: GROEB_1:34 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_groeb_1 :::"DivOrder"::: ) (Set (Var "n")) ")" ) "#)" ) (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "st" (Bool (Set (Var "B")) ($#r1_dickson :::"is_Dickson-basis_of"::: ) (Set (Var "N")) "," (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k4_groeb_1 :::"DivOrder"::: ) (Set (Var "n")) ")" ) "#)" ))))) ; theorem :: GROEB_1:35 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "ex" (Set (Var "G")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T")))))))) ; theorem :: GROEB_1:36 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k1_groeb_1 :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))) & (Bool (Bool "not" (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r2_hidden :::"in"::: ) (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"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "p" :::"is_monic_wrt"::: "T" means :: GROEB_1:def 6 (Bool (Set ($#k4_termord :::"HC"::: ) "(" "p" "," "T" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) "L")); end; :: deftheorem defines :::"is_monic_wrt"::: GROEB_1:def 6 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_groeb_1 :::"is_monic_wrt"::: ) (Set (Var "T"))) "iff" (Bool (Set ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (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 ($#~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")) ")" ")" ); pred "P" :::"is_reduced_wrt"::: "T" means :: GROEB_1:def 7 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_groeb_1 :::"is_monic_wrt"::: ) "T") & (Bool (Set (Var "p")) ($#r7_polyred :::"is_irreducible_wrt"::: ) (Set "P" ($#k7_subset_1 :::"\"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) )) "," "T") ")" )); end; :: deftheorem defines :::"is_reduced_wrt"::: GROEB_1: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" ($#~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 "(" (Bool (Set (Var "P")) ($#r4_groeb_1 :::"is_reduced_wrt"::: ) (Set (Var "T"))) "iff" (Bool "for" (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")))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_groeb_1 :::"is_monic_wrt"::: ) (Set (Var "T"))) & (Bool (Set (Var "p")) ($#r7_polyred :::"is_irreducible_wrt"::: ) (Set (Set (Var "P")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) )) "," (Set (Var "T"))) ")" )) ")" ))))); notationlet "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")) ")" ")" ); synonym "P" :::"is_autoreduced_wrt"::: "T" for "P" :::"is_reduced_wrt"::: "T"; end; theorem :: GROEB_1:37 (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 "I")) "being" ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (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 (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "g")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "or" "not" (Bool (Set (Var "p")) ($#r2_polyred :::"<"::: ) (Set (Var "f")) "," (Set (Var "T"))) "or" "not" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) "or" "not" (Bool (Set (Var "p")) ($#r2_polyred :::"<"::: ) (Set (Var "g")) "," (Set (Var "T"))) "or" "not" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "m"))) ")" ) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))))) ; theorem :: GROEB_1:38 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "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 "G"))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set (Var "q"))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )) & (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "G")) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set (Var "p")) ($#k1_groeb_1 :::"}"::: ) )) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T")))))))))) ; theorem :: GROEB_1:39 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "I")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_groeb_1 :::"{"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k1_groeb_1 :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool "(" (Bool (Set (Var "G")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))) & (Bool (Set (Var "G")) ($#r4_groeb_1 :::"is_reduced_wrt"::: ) (Set (Var "T"))) ")" )))))) ; theorem :: GROEB_1: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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#v2_ideal_1 :::"left-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "G1")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))) & (Bool (Set (Var "G1")) ($#r4_groeb_1 :::"is_reduced_wrt"::: ) (Set (Var "T"))) & (Bool (Set (Var "G2")) ($#r2_groeb_1 :::"is_Groebner_basis_of"::: ) (Set (Var "I")) "," (Set (Var "T"))) & (Bool (Set (Var "G2")) ($#r4_groeb_1 :::"is_reduced_wrt"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "G1")) ($#r1_hidden :::"="::: ) (Set (Var "G2")))))))) ;