:: POLYNOM6 semantic presentation begin notationlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; synonym "L1" "," "L2" :::"are_isomorphic"::: for "L1" :::"is_ringisomorph_to"::: "L2"; end; definitionlet "L1", "L2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; :: original: :::"are_isomorphic"::: redefine pred "L1" :::"is_ringisomorph_to"::: "L2"; reflexivity (Bool "for" (Set (Var "L1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool bbbadR2_QUOFIELD((Set (Var "b1")) "," (Set (Var "b1"))))) ; end; theorem :: POLYNOM6:1 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o")))) & (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "o2"))) ")" )) ")" ) ")" )) "holds" (Bool (Set (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")))))) ; registrationlet "o1" be ($#m1_hidden :::"Ordinal":::); let "o2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Ordinal":::); cluster (Set "o1" ($#k10_ordinal2 :::"+^"::: ) "o2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "o2" ($#k10_ordinal2 :::"+^"::: ) "o1") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: POLYNOM6:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "a")) ($#r1_pre_poly :::"<"::: ) (Set (Var "b")))) "holds" (Bool "ex" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "o")))) "holds" (Bool (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" )))) ; begin definitionlet "o1", "o2" be ($#m1_hidden :::"Ordinal":::); let "a" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Const "o1"))); let "b" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Const "o2"))); func "a" :::"+^"::: "b" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" "o1" ($#k10_ordinal2 :::"+^"::: ) "o2" ")" )) means :: POLYNOM6:def 1 (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) "o1")) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set "a" ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Set "(" "o1" ($#k10_ordinal2 :::"+^"::: ) "o2" ")" ) ($#k6_subset_1 :::"\"::: ) "o1"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set "b" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "o")) ($#k5_ordinal3 :::"-^"::: ) "o1" ")" ))) ")" ")" )); end; :: deftheorem defines :::"+^"::: POLYNOM6:def 1 : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) (Bool "for" (Set (Var "b5")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "o1")))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "o")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "o1"))))) "implies" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "o")) ($#k5_ordinal3 :::"-^"::: ) (Set (Var "o1")) ")" ))) ")" ")" )) ")" ))))); theorem :: POLYNOM6:3 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: POLYNOM6:4 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Var "o1")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; theorem :: POLYNOM6:5 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "holds" (Bool "(" (Bool (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2"))) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "b1")) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "o1")))) & (Bool (Set (Var "b2")) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "o2")))) ")" ) ")" )))) ; theorem :: POLYNOM6:6 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "c")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" )) (Bool "ex" (Set (Var "c1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1")))(Bool "ex" (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Set (Var "c")) ($#r6_pboole :::"="::: ) (Set (Set (Var "c1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "c2")))))))) ; theorem :: POLYNOM6:7 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "," (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "c1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "c2"))))) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r6_pboole :::"="::: ) (Set (Var "c1"))) & (Bool (Set (Var "b2")) ($#r6_pboole :::"="::: ) (Set (Var "c2"))) ")" )))) ; theorem :: POLYNOM6:8 (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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Series":::) "of" (Set (Var "n")) "," (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k5_polynom1 :::"+"::: ) (Set (Var "q")) ")" ) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r")) ")" ) ($#k5_polynom1 :::"+"::: ) (Set "(" (Set (Var "q")) ($#k9_polynom1 :::"*'"::: ) (Set (Var "r")) ")" )))))) ; begin registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" "n" "," "L" ")" ) -> ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ; end; definitionlet "o1", "o2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Ordinal":::); let "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "P" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "o1")) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Const "o2")) "," (Set (Const "L")) ")" ")" ); func :::"Compress"::: "P" -> ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" "o1" ($#k10_ordinal2 :::"+^"::: ) "o2" ")" ) "," "L" means :: POLYNOM6:def 2 (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" "o1" ($#k10_ordinal2 :::"+^"::: ) "o2" ")" )) (Bool "ex" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "o1")(Bool "ex" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "o2")(Bool "ex" (Set (Var "Q1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "o2" "," "L" "st" (Bool "(" (Bool (Set (Var "Q1")) ($#r1_hidden :::"="::: ) (Set "P" ($#k3_polynom1 :::"."::: ) (Set (Var "b1")))) & (Bool (Set (Var "b")) ($#r8_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")))) & (Bool (Set it ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q1")) ($#k3_polynom1 :::"."::: ) (Set (Var "b2")))) ")" ))))); end; :: deftheorem defines :::"Compress"::: POLYNOM6:def 2 : (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Ordinal":::) (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "o1")) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "o2")) "," (Set (Var "L")) ")" ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) "," (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom6 :::"Compress"::: ) (Set (Var "P")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" )) (Bool "ex" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1")))(Bool "ex" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2")))(Bool "ex" (Set (Var "Q1")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "o2")) "," (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "Q1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_polynom1 :::"."::: ) (Set (Var "b1")))) & (Bool (Set (Var "b")) ($#r8_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")))) & (Bool (Set (Set (Var "b5")) ($#k3_polynom1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q1")) ($#k3_polynom1 :::"."::: ) (Set (Var "b2")))) ")" ))))) ")" ))))); theorem :: POLYNOM6:9 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "," (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "c1"))) & (Bool (Set (Var "b2")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "c2")))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2"))) ($#r3_pre_poly :::"divides"::: ) (Set (Set (Var "c1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "c2"))))))) ; theorem :: POLYNOM6:10 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2"))) (Bool "for" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2"))))) "holds" (Bool "ex" (Set (Var "c1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1")))(Bool "ex" (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool "(" (Bool (Set (Var "c1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b1"))) & (Bool (Set (Var "c2")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2"))) & (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "c1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "c2")))) ")" ))))))) ; theorem :: POLYNOM6:11 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "a2"))) ($#r1_pre_poly :::"<"::: ) (Set (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")))) "iff" (Bool "(" (Bool (Set (Var "a1")) ($#r1_pre_poly :::"<"::: ) (Set (Var "b1"))) "or" (Bool "(" (Bool (Set (Var "a1")) ($#r6_pboole :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_pre_poly :::"<"::: ) (Set (Var "b2"))) ")" ) ")" ) ")" )))) ; theorem :: POLYNOM6:12 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b1")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b1")) ")" )))) "holds" (Bool "ex" (Set (Var "a19")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1")))(Bool "ex" (Set (Var "Fk")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" )) "st" (Bool "(" (Bool (Set (Var "Fk")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k9_pre_poly :::"/."::: ) (Set (Var "i")))) & (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b1")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r6_pboole :::"="::: ) (Set (Var "a19"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "Fk"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b2")) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "Fk"))))) "holds" (Bool "ex" (Set (Var "a199")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool "(" (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "m"))) ($#r6_pboole :::"="::: ) (Set (Var "a199"))) & (Bool (Set (Set (Var "Fk")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "a19")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "a199")))) ")" )) ")" ) ")" ))) ")" )) "holds" (Bool (Set ($#k20_pre_poly :::"divisors"::: ) (Set "(" (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "G")))))))) ; theorem :: POLYNOM6:13 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "," (Set (Var "c1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "a2")) "," (Set (Var "b2")) "," (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool (Bool (Set (Var "c1")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "a1")))) & (Bool (Set (Var "c2")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b2")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "a2"))))) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")) ")" ) ($#k12_pre_poly :::"-'"::: ) (Set "(" (Set (Var "a1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "a2")) ")" )) ($#r6_pboole :::"="::: ) (Set (Set (Var "c1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "c2"))))))) ; theorem :: POLYNOM6:14 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1"))) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b1")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b1")) ")" )))) "holds" (Bool "ex" (Set (Var "a19")) "," (Set (Var "b19")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o1")))(Bool "ex" (Set (Var "Fk")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) ")" )) "st" (Bool "(" (Bool (Set (Var "Fk")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k9_pre_poly :::"/."::: ) (Set (Var "i")))) & (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b1")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom3 :::"<*"::: ) (Set (Var "a19")) "," (Set (Var "b19")) ($#k2_polynom3 :::"*>"::: ) )) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "Fk"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b2")) ")" ))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "Fk"))))) "holds" (Bool "ex" (Set (Var "a199")) "," (Set (Var "b199")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "o2"))) "st" (Bool "(" (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b2")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom3 :::"<*"::: ) (Set (Var "a199")) "," (Set (Var "b199")) ($#k2_polynom3 :::"*>"::: ) )) & (Bool (Set (Set (Var "Fk")) ($#k9_pre_poly :::"/."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom3 :::"<*"::: ) (Set "(" (Set (Var "a19")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "a199")) ")" ) "," (Set "(" (Set (Var "b19")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b199")) ")" ) ($#k2_polynom3 :::"*>"::: ) )) ")" )) ")" ) ")" ))) ")" )) "holds" (Bool (Set ($#k21_pre_poly :::"decomp"::: ) (Set "(" (Set (Var "b1")) ($#k1_polynom6 :::"+^"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "G")))))))) ; theorem :: POLYNOM6:15 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "o1")) "," (Set "(" ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set (Var "o2")) "," (Set (Var "L")) ")" ")" ) ")" ) "," (Set ($#k11_polynom1 :::"Polynom-Ring"::: ) "(" (Set "(" (Set (Var "o1")) ($#k10_ordinal2 :::"+^"::: ) (Set (Var "o2")) ")" ) "," (Set (Var "L")) ")" ) ($#r2_quofield :::"are_isomorphic"::: ) ))) ;