:: O_RING_1 semantic presentation begin definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); func "x" :::"^2"::: -> ($#m1_subset_1 :::"Scalar":::) "of" "R" equals :: O_RING_1:def 1 (Set "x" ($#k6_algstr_0 :::"*"::: ) "x"); end; :: deftheorem defines :::"^2"::: O_RING_1:def 1 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool (Set (Set (Var "x")) ($#k1_o_ring_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_a_square"::: means :: O_RING_1:def 2 (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_o_ring_1 :::"^2"::: ) ))); end; :: deftheorem defines :::"being_a_square"::: O_RING_1:def 2 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_o_ring_1 :::"^2"::: ) ))) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_a_Sum_of_squares"::: means :: O_RING_1:def 3 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_a_Sum_of_squares"::: O_RING_1:def 3 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_o_ring_1 :::"being_a_Sum_of_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_a_sum_of_squares"::: means :: O_RING_1:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_o_ring_1 :::"being_a_Sum_of_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"being_a_sum_of_squares"::: O_RING_1:def 4 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_o_ring_1 :::"being_a_Sum_of_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_a_Product_of_squares"::: means :: O_RING_1:def 5 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_a_Product_of_squares"::: O_RING_1:def 5 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_o_ring_1 :::"being_a_Product_of_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_a_product_of_squares"::: means :: O_RING_1:def 6 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_o_ring_1 :::"being_a_Product_of_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"being_a_product_of_squares"::: O_RING_1:def 6 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_o_ring_1 :::"being_a_Product_of_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_a_Sum_of_products_of_squares"::: means :: O_RING_1:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_a_Sum_of_products_of_squares"::: O_RING_1:def 7 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_o_ring_1 :::"being_a_Sum_of_products_of_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_a_sum_of_products_of_squares"::: means :: O_RING_1:def 8 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_o_ring_1 :::"being_a_Sum_of_products_of_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"being_a_sum_of_products_of_squares"::: O_RING_1:def 8 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_o_ring_1 :::"being_a_Sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_an_Amalgam_of_squares"::: means :: O_RING_1:def 9 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Bool "not" (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_an_Amalgam_of_squares"::: O_RING_1:def 9 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_o_ring_1 :::"being_an_Amalgam_of_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_an_amalgam_of_squares"::: means :: O_RING_1:def 10 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_o_ring_1 :::"being_an_Amalgam_of_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"being_an_amalgam_of_squares"::: O_RING_1:def 10 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_o_ring_1 :::"being_an_Amalgam_of_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_a_Sum_of_amalgams_of_squares"::: means :: O_RING_1:def 11 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_a_Sum_of_amalgams_of_squares"::: O_RING_1:def 11 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_o_ring_1 :::"being_a_Sum_of_amalgams_of_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1)) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"being_a_sum_of_amalgams_of_squares"::: means :: O_RING_1:def 12 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_o_ring_1 :::"being_a_Sum_of_amalgams_of_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"being_a_sum_of_amalgams_of_squares"::: O_RING_1:def 12 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_o_ring_1 :::"being_a_Sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "R")); attr "f" is :::"being_a_generation_from_squares"::: means :: O_RING_1:def 13 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool (Bool "not" (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) "or" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) ")" ) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"being_a_generation_from_squares"::: O_RING_1:def 13 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_o_ring_1 :::"being_a_generation_from_squares"::: ) ) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool (Bool "not" (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) "or" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "j")) ")" ))) ")" ) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "j")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) ")" )) ")" ) ")" ) ")" ))); definitionlet "R" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Scalar":::) "of" (Set (Const "R")); attr "x" is :::"generated_from_squares"::: means :: O_RING_1:def 14 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "R" "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_o_ring_1 :::"being_a_generation_from_squares"::: ) ) & (Bool "x" ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )); end; :: deftheorem defines :::"generated_from_squares"::: O_RING_1:def 14 : (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "R")) "st" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_o_ring_1 :::"being_a_generation_from_squares"::: ) ) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ))) ")" )) ")" ))); theorem :: O_RING_1:1 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:2 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ))) ; theorem :: O_RING_1:3 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ))) ; theorem :: O_RING_1:4 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ))) ; theorem :: O_RING_1:5 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ))) ; theorem :: O_RING_1:6 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ))) ; begin theorem :: O_RING_1:7 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ))) ; theorem :: O_RING_1:8 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ))) ; theorem :: O_RING_1:9 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool "(" (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) ")" ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool "(" (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) ")" ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ))) ; theorem :: O_RING_1:10 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool "(" (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) "or" (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:11 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:12 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:13 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:14 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:15 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:16 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:17 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:18 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:19 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:20 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:21 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:22 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:23 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:24 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:25 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:26 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:27 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:28 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:29 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:30 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:31 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:32 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:33 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:34 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:35 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:36 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:37 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:38 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool "(" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) ")" ) ")" )) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; begin theorem :: O_RING_1:39 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ))) ; theorem :: O_RING_1:40 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ))) ; theorem :: O_RING_1:41 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:42 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:43 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:44 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:45 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:46 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:47 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ))) ; theorem :: O_RING_1:48 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:49 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:50 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:51 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:52 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:53 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:54 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:55 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:56 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:57 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:58 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:59 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:60 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:61 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:62 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:63 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:64 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:65 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:66 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:67 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:68 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:69 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:70 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:71 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:72 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:73 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:74 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:75 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:76 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:77 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:78 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:79 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:80 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:81 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v1_o_ring_1 :::"being_a_square"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:82 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v9_o_ring_1 :::"being_an_amalgam_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:83 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v3_o_ring_1 :::"being_a_sum_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:84 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v5_o_ring_1 :::"being_a_product_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:85 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v7_o_ring_1 :::"being_a_sum_of_products_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ; theorem :: O_RING_1:86 (Bool "for" (Set (Var "R")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Scalar":::) "of" (Set (Var "R")) "st" (Bool (Bool (Set (Var "x")) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ) & (Bool (Set (Var "y")) "is" ($#v11_o_ring_1 :::"being_a_sum_of_amalgams_of_squares"::: ) )) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) "is" ($#v13_o_ring_1 :::"generated_from_squares"::: ) ))) ;