:: POLYRED semantic presentation begin registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "R" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k15_pre_poly :::"Bags"::: ) "n") ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set ($#k15_pre_poly :::"Bags"::: ) "n") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R")) ($#v1_polynom7 :::"non-zero"::: ) ($#v3_polynom7 :::"monomial-like"::: ) ($#v1_polynom1 :::"finite-Support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "R") ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v6_algstr_0 :::"right_add-cancelable"::: ) ($#v7_algstr_0 :::"add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) bbbadV1_GROUP_1() ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_algstr_1 :::"add-left-invertible"::: ) ($#v3_algstr_1 :::"add-right-invertible"::: ) ($#v4_algstr_1 :::"Loop-like"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; registrationlet "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"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#v1_polynom7 :::"non-zero"::: ) ($#v1_polynom1 :::"finite-Support"::: ) ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "p" ($#k9_polynom1 :::"*'"::: ) "q") -> ($#v1_polynom7 :::"non-zero"::: ) ; end; begin theorem :: POLYRED:1 (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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k5_polynom1 :::"+"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k5_polynom1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "q")) ")" )))))) ; theorem :: POLYRED:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ")" ) ($#k4_polynom1 :::"+"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))) ; theorem :: POLYRED:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k4_polynom1 :::"+"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) & (Bool (Set (Set (Var "p")) ($#k4_polynom1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" )) ")" )))) ; theorem :: POLYRED:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_polynom1 :::"-"::: ) (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))))) ; theorem :: POLYRED:5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))) ; theorem :: POLYRED: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"::: ) ($#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 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k10_polynom1 :::"*'"::: ) (Set (Var "q")))) & (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k10_polynom1 :::"*'"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "q")) ")" ))) ")" )))) ; theorem :: POLYRED:7 (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"::: ) ($#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")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "m")) ($#k3_polynom1 :::"."::: ) (Set "(" ($#k2_polynom7 :::"term"::: ) (Set (Var "m")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" )))))))) ; theorem :: POLYRED:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_algstr_0 :::"left_add-cancelable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k5_polynom7 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "X")) "," (Set (Var "L")) ")" ))))) ; theorem :: POLYRED:9 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")))) & (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" ))) ")" ))))) ; theorem :: POLYRED:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ) ($#k4_polynom1 :::"+"::: ) (Set "(" (Set (Var "a9")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a9")) ")" ) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")))))))) ; theorem :: POLYRED:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "X")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a9")) ")" ) ($#k5_polynom7 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "a9")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: POLYRED:12 (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_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 "p9")) "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")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p9")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p9")) ")" ))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); func "b" :::"*'"::: "p" -> ($#m1_subset_1 :::"Series":::) "of" "n" "," "L" means :: POLYRED:def 1 (Bool "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool "b" ($#r3_pre_poly :::"divides"::: ) (Set (Var "b9")))) "holds" (Bool "(" (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set "p" ($#k3_polynom1 :::"."::: ) (Set "(" (Set (Var "b9")) ($#k12_pre_poly :::"-'"::: ) "b" ")" ))) & (Bool "(" "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Bool "not" "b" ($#r3_pre_poly :::"divides"::: ) (Set (Var "b9"))))) "holds" (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ) ")" )); end; :: deftheorem defines :::"*'"::: POLYRED:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b9")))) "holds" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set "(" (Set (Var "b9")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Bool "not" (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b9"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" )) ")" ))))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#v1_polynom1 :::"finite-Support"::: ) ($#m1_subset_1 :::"Series":::) "of" (Set (Const "n")) "," (Set (Const "L")); cluster (Set "b" ($#k1_polyred :::"*'"::: ) "p") -> ($#v1_polynom1 :::"finite-Support"::: ) ; end; theorem :: POLYRED:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" ) ($#k3_polynom1 :::"."::: ) (Set "(" (Set (Var "b9")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9")))))))) ; theorem :: POLYRED:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) "{" (Set "(" (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b9")) ")" ) where b9 "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) : (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))) "}" ))))) ; theorem :: POLYRED:15 (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"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )))))))) ; theorem :: POLYRED:16 (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"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Var "b9")) ($#r1_termord :::"<="::: ) (Set (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) "," (Set (Var "T")))))))) ; theorem :: POLYRED:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) ($#k1_polyred :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))))) ; theorem :: POLYRED: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" ) ($#k1_polyred :::"*'"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "b1")) ($#k1_polyred :::"*'"::: ) (Set "(" (Set (Var "b2")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: POLYRED:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_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")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))))))) ; theorem :: POLYRED:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ))))))) ; theorem :: POLYRED:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "a")) "being" ($#~v9_struct_0 "non" ($#v9_struct_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "a")) ($#k5_polynom7 :::"*"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ))))))) ; theorem :: POLYRED:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) (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 "a")) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k1_polynom7 :::"Monom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p"))))))))) ; theorem :: POLYRED:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "p")) ")" ) "," (Set (Var "T")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set "(" (Set (Var "m")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "q")) ")" ))))))))) ; begin registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," "T" "#)" ) -> ($#v16_waybel_0 :::"connected"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); cluster (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," "T" "#)" ) -> ($#v1_wellfnd1 :::"well_founded"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "p" :::"<="::: "q" "," "T" means :: POLYRED:def 2 (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) "p" ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) "q" ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k13_bagorder :::"FinOrd"::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," "T" "#)" ))); end; :: deftheorem defines :::"<="::: POLYRED:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")) ")" ) "," (Set "(" ($#k2_polynom1 :::"Support"::: ) (Set (Var "q")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k13_bagorder :::"FinOrd"::: ) (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "," (Set (Var "T")) "#)" ))) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p", "q" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "p" :::"<"::: "q" "," "T" means :: POLYRED:def 3 (Bool "(" (Bool "p" ($#r1_polyred :::"<="::: ) "q" "," "T") & (Bool (Set ($#k2_polynom1 :::"Support"::: ) "p") ($#r1_hidden :::"<>"::: ) (Set ($#k2_polynom1 :::"Support"::: ) "q")) ")" ); end; :: deftheorem defines :::"<"::: POLYRED:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_polyred :::"<"::: ) (Set (Var "q")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) & (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "q")))) ")" ) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); func :::"Support"::: "(" "p" "," "T" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#g1_orders_2 :::"RelStr"::: ) "(#" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "," "T" "#)" ))) equals :: POLYRED:def 4 (Set ($#k2_polynom1 :::"Support"::: ) "p"); end; :: deftheorem defines :::"Support"::: POLYRED:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k2_polyred :::"Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p")))))))); theorem :: POLYRED:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k11_bagorder :::"PosetMax"::: ) (Set "(" ($#k2_polyred :::"Support"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" )))))) ; theorem :: POLYRED:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: POLYRED:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) & (Bool (Set (Var "q")) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))) ")" ) "iff" (Bool (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "q")))) ")" ))))) ; theorem :: POLYRED: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" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) & (Bool (Set (Var "q")) ($#r1_polyred :::"<="::: ) (Set (Var "r")) "," (Set (Var "T")))) "holds" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "r")) "," (Set (Var "T"))))))) ; theorem :: POLYRED:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) "or" (Bool (Set (Var "q")) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))) ")" ))))) ; theorem :: POLYRED:29 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) "iff" (Bool (Bool "not" (Set (Var "q")) ($#r2_polyred :::"<"::: ) (Set (Var "p")) "," (Set (Var "T")))) ")" ))))) ; theorem :: POLYRED:30 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: POLYRED:31 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"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"::: ) ($#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" ($#~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 "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 "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set (Var "p")) ($#r1_polyred :::"<="::: ) (Set (Var "q")) "," (Set (Var "T"))) ")" ) ")" )))))) ; theorem :: POLYRED:32 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_polyred :::"<"::: ) (Set (Var "q")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set (Var "q")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) ")" ) "or" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_termord :::"<"::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) "or" (Bool "(" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" )) & (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_polyred :::"<"::: ) (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "q")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) ")" ) ")" ) ")" ))))) ; theorem :: POLYRED:33 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_polyred :::"<"::: ) (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))))))) ; theorem :: POLYRED: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" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k5_termord :::"HM"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r1_polyred :::"<="::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: POLYRED:35 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set ($#k6_termord :::"Red"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r2_polyred :::"<"::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~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 "f", "p", "g" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "f" :::"reduces_to"::: "g" "," "p" "," "b" "," "T" means :: POLYRED:def 5 (Bool "(" (Bool "f" ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "L" ")" )) & (Bool "p" ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" "n" "," "L" ")" )) & (Bool "b" ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) "f")) & (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool "(" (Bool (Set (Set (Var "s")) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" "p" "," "T" ")" ")" )) ($#r1_hidden :::"="::: ) "b") & (Bool "g" ($#r2_funct_2 :::"="::: ) (Set "f" ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" (Set "(" "f" ($#k3_polynom1 :::"."::: ) "b" ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k4_termord :::"HC"::: ) "(" "p" "," "T" ")" ")" ) ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_polyred :::"*'"::: ) "p" ")" ) ")" ))) ")" )) ")" ); end; :: deftheorem defines :::"reduces_to"::: POLYRED: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 "f")) "," (Set (Var "p")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "T"))) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) & (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "f")))) & (Bool "ex" (Set (Var "s")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Set (Var "s")) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "f")) ($#k3_polynom1 :::"."::: ) (Set (Var "b")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k4_termord :::"HC"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k5_polynom7 :::"*"::: ) (Set "(" (Set (Var "s")) ($#k1_polyred :::"*'"::: ) (Set (Var "p")) ")" ) ")" ))) ")" )) ")" ) ")" )))))); 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 "f", "p", "g" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "f" :::"reduces_to"::: "g" "," "p" "," "T" means :: POLYRED:def 6 (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool "f" ($#r3_polyred :::"reduces_to"::: ) "g" "," "p" "," (Set (Var "b")) "," "T")); end; :: deftheorem defines :::"reduces_to"::: POLYRED: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" ($#~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")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r4_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (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 ($#~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 "f", "g" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "f" :::"reduces_to"::: "g" "," "P" "," "T" means :: POLYRED:def 7 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool "f" ($#r4_polyred :::"reduces_to"::: ) "g" "," (Set (Var "p")) "," "T") ")" )); end; :: deftheorem defines :::"reduces_to"::: POLYRED: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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (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 "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "P")) "," (Set (Var "T"))) "iff" (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 (Var "f")) ($#r4_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "T"))) ")" )) ")" )))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~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 "f", "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "f" :::"is_reducible_wrt"::: "p" "," "T" means :: POLYRED:def 8 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "f" ($#r4_polyred :::"reduces_to"::: ) (Set (Var "g")) "," "p" "," "T")); end; :: deftheorem defines :::"is_reducible_wrt"::: POLYRED: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" ($#~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")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r6_polyred :::"is_reducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Set (Var "f")) ($#r4_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (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 "f", "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); antonym "f" :::"is_irreducible_wrt"::: "p" "," "T" for "f" :::"is_reducible_wrt"::: "p" "," "T"; antonym "f" :::"is_in_normalform_wrt"::: "p" "," "T" for "f" :::"is_reducible_wrt"::: "p" "," "T"; end; 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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "f" :::"is_reducible_wrt"::: "P" "," "T" means :: POLYRED:def 9 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "f" ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," "P" "," "T")); end; :: deftheorem defines :::"is_reducible_wrt"::: POLYRED: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" ($#~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" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (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 "f")) ($#r7_polyred :::"is_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Set (Var "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "P")) "," (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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); antonym "f" :::"is_irreducible_wrt"::: "P" "," "T" for "f" :::"is_reducible_wrt"::: "P" "," "T"; antonym "f" :::"is_in_normalform_wrt"::: "P" "," "T" for "f" :::"is_reducible_wrt"::: "P" "," "T"; end; 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 "f", "p", "g" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "f" :::"top_reduces_to"::: "g" "," "p" "," "T" means :: POLYRED:def 10 (Bool "f" ($#r3_polyred :::"reduces_to"::: ) "g" "," "p" "," (Set ($#k3_termord :::"HT"::: ) "(" "f" "," "T" ")" ) "," "T"); end; :: deftheorem defines :::"top_reduces_to"::: POLYRED: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" ($#~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")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r8_polyred :::"top_reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "T"))) "iff" (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (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 ($#~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 "f", "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); pred "f" :::"is_top_reducible_wrt"::: "p" "," "T" means :: POLYRED:def 11 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "f" ($#r8_polyred :::"top_reduces_to"::: ) (Set (Var "g")) "," "p" "," "T")); end; :: deftheorem defines :::"is_top_reducible_wrt"::: POLYRED:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r9_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Set (Var "f")) ($#r8_polyred :::"top_reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "T")))) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~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 "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "n")) "," (Set (Const "L")); let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); pred "f" :::"is_top_reducible_wrt"::: "P" "," "T" means :: POLYRED:def 12 (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "P") & (Bool "f" ($#r9_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "p")) "," "T") ")" )); end; :: deftheorem defines :::"is_top_reducible_wrt"::: POLYRED:def 12 : (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")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (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 "f")) ($#r10_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "P")) "," (Set (Var "T"))) "iff" (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 (Var "f")) ($#r9_polyred :::"is_top_reducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T"))) ")" )) ")" )))))); theorem :: POLYRED:36 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r6_polyred :::"is_reducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "f")))) & (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "p")) "," (Set (Var "T")) ")" ) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" )) ")" )))))) ; theorem :: POLYRED:37 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ) ($#r6_polyred :::"is_irreducible_wrt"::: ) (Set (Var "p")) "," (Set (Var "T"))))))) ; theorem :: POLYRED: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")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r4_polyred :::"reduces_to"::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set "(" (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "p")) ")" )) "," (Set (Var "p")) "," (Set (Var "T")))) "holds" (Bool (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 "f"))))))))) ; theorem :: POLYRED:39 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool "not" (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g")))))))))) ; theorem :: POLYRED:40 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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")) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_termord :::"<"::: ) (Set (Var "b9")) "," (Set (Var "T"))) & (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool "(" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g")))) "iff" (Bool (Set (Var "b9")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "f")))) ")" )))))) ; theorem :: POLYRED:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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")) (Bool "for" (Set (Var "b")) "," (Set (Var "b9")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_termord :::"<"::: ) (Set (Var "b9")) "," (Set (Var "T"))) & (Bool (Set (Var "f")) ($#r3_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "p")) "," (Set (Var "b")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_polynom1 :::"."::: ) (Set (Var "b9"))))))))) ; theorem :: POLYRED:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~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")) "," (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 "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set ($#k2_polynom1 :::"Support"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "b")) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "," (Set (Var "T")))))))) ; theorem :: POLYRED:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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 (Set (Var "g")) ($#r2_polyred :::"<"::: ) (Set (Var "f")) "," (Set (Var "T"))))))) ; begin definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~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 :::"PolyRedRel"::: "(" "P" "," "T" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ")" )) means :: POLYRED:def 13 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "n" "," "L" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "p")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "q")) "," "P" "," "T") ")" )); end; :: deftheorem defines :::"PolyRedRel"::: POLYRED:def 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")) ")" ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_struct_0 :::"NonZero"::: ) (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool (Set (Var "p")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "q")) "," (Set (Var "P")) "," (Set (Var "T"))) ")" )) ")" )))))); theorem :: POLYRED:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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 "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (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")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r1_polyred :::"<="::: ) (Set (Var "f")) "," (Set (Var "T"))) & (Bool "(" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )) "or" (Bool (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "g")) "," (Set (Var "T")) ")" ) ($#r1_termord :::"<="::: ) (Set ($#k3_termord :::"HT"::: ) "(" (Set (Var "f")) "," (Set (Var "T")) ")" ) "," (Set (Var "T"))) ")" ) ")" )))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "T" be ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Const "n")); let "L" be ($#~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"::: ) ; let "P" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "n")) "," (Set (Const "L")) ")" ")" ); cluster (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" "P" "," "T" ")" ) -> ($#v3_rewrite1 :::"strongly-normalizing"::: ) ; end; theorem :: POLYRED:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"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"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "P")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "h")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "f"))) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))))))) ; theorem :: POLYRED:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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")) ")" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#v1_polynom7 :::"non-zero"::: ) ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Var "f")) ($#r5_polyred :::"reduces_to"::: ) (Set (Var "g")) "," (Set (Var "P")) "," (Set (Var "T")))) "holds" (Bool (Set (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "f"))) ($#r5_polyred :::"reduces_to"::: ) (Set (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g"))) "," (Set (Var "P")) "," (Set (Var "T"))))))))) ; theorem :: POLYRED:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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")) ")" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "f"))) "," (Set (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "g")))))))))) ; theorem :: POLYRED:48 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "T")) "being" ($#v6_relat_2 :::"connected"::: ) ($#v2_bagorder :::"admissible"::: ) ($#m1_subset_1 :::"TermOrder":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "L")) "being" ($#~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")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Monomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "m")) ($#k10_polynom1 :::"*'"::: ) (Set (Var "f"))) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" )))))))) ; theorem :: POLYRED:49 (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 "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "h1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Var "h"))) & (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "h")) "," (Set (Var "h1")))) "holds" (Bool "ex" (Set (Var "f1")) "," (Set (Var "g1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g1"))) ($#r2_funct_2 :::"="::: ) (Set (Var "h1"))) & (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "f1"))) & (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "g")) "," (Set (Var "g1"))) ")" ))))))) ; theorem :: POLYRED:50 (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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r5_rewrite1 :::"are_convergent_wrt"::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ))))))) ; theorem :: POLYRED:51 (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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ))))))) ; definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "I" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "R")); let "a", "b" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); pred "a" "," "b" :::"are_congruent_mod"::: "I" means :: POLYRED:def 14 (Bool (Set "a" ($#k5_algstr_0 :::"-"::: ) "b") ($#r2_hidden :::"in"::: ) "I"); end; :: deftheorem defines :::"are_congruent_mod"::: POLYRED:def 14 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I"))) "iff" (Bool (Set (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "b"))) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) ")" )))); theorem :: POLYRED:52 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "holds" (Bool (Set (Var "a")) "," (Set (Var "a")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))))) ; theorem :: POLYRED:53 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#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"::: ) ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))) "holds" (Bool (Set (Var "b")) "," (Set (Var "a")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))))) ; theorem :: POLYRED:54 (Bool "for" (Set (Var "R")) "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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_ideal_1 :::"add-closed"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I"))) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))))) ; theorem :: POLYRED:55 (Bool "for" (Set (Var "R")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "c"))) "," (Set (Set (Var "b")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "d"))) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))))) ; theorem :: POLYRED:56 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#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"::: ) ($#v3_ideal_1 :::"right-ideal"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "R")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I"))) & (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "c"))) "," (Set (Set (Var "b")) ($#k8_group_1 :::"*"::: ) (Set (Var "d"))) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Var "I")))))) ; theorem :: POLYRED:57 (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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))))))) ; theorem :: POLYRED:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"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")) ")" ")" ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r11_polyred :::"are_congruent_mod"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))) "holds" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_rewrite1 :::"are_convertible_wrt"::: ) (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ))))))) ; theorem :: POLYRED:59 (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 "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_polynom1 :::"-"::: ) (Set (Var "g"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))))))) ; theorem :: POLYRED:60 (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 "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "n")) "," (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_polyred :::"PolyRedRel"::: ) "(" (Set (Var "P")) "," (Set (Var "T")) ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "f")) "," (Set ($#k7_polynom1 :::"0_"::: ) "(" (Set (Var "n")) "," (Set (Var "L")) ")" ))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "P")) ($#k7_ideal_1 :::"-Ideal"::: ) ))))))) ;