:: CONVFUN1 semantic presentation begin definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; func :::"Add_in_Prod_of_RLS"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) means :: CONVFUN1:def 1 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "X" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "Y" "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "X") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "Y") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ))))); end; :: deftheorem defines :::"Add_in_Prod_of_RLS"::: CONVFUN1:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_convfun1 :::"Add_in_Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "X"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "Y"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ")" ))); definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; func :::"Mult_in_Prod_of_RLS"::: "(" "X" "," "Y" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) means :: CONVFUN1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "X" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "Y" "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "X") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "Y") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) )))))); end; :: deftheorem defines :::"Mult_in_Prod_of_RLS"::: CONVFUN1:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_convfun1 :::"Mult_in_Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "b3")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "X"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "Y"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ")" ))); definitionlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; func :::"Prod_of_RLS"::: "(" "X" "," "Y" ")" -> ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: CONVFUN1:def 3 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "Y") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "X" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "Y" ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k1_convfun1 :::"Add_in_Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ")" ) "," (Set "(" ($#k2_convfun1 :::"Mult_in_Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ")" ) "#)" ); end; :: deftheorem defines :::"Prod_of_RLS"::: CONVFUN1:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "Y")) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" ($#k1_convfun1 :::"Add_in_Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "," (Set "(" ($#k2_convfun1 :::"Mult_in_Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "#)" ))); registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; theorem :: CONVFUN1:1 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "p")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "p")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))) ; theorem :: CONVFUN1:2 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" ) "st" (Bool (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "u2")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "u1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set (Var "y1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#v3_rlvect_1 :::"add-associative"::: ) ; end; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#v13_algstr_0 :::"right_complementable"::: ) ; end; registrationlet "X", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," "Y" ")" ) -> ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; theorem :: CONVFUN1:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) (Bool "for" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ")" )) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "y")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))))) ; begin definitionfunc :::"RLS_Real"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: CONVFUN1:def 4 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "#)" ); end; :: deftheorem defines :::"RLS_Real"::: CONVFUN1:def 4 : (Bool (Set ($#k4_convfun1 :::"RLS_Real"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k33_binop_2 :::"addreal"::: ) ) "," (Set ($#k35_binop_2 :::"multreal"::: ) ) "#)" )); registration cluster (Set ($#k4_convfun1 :::"RLS_Real"::: ) ) -> ($#~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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; begin begin definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); func :::"epigraph"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_convfun1 :::"Prod_of_RLS"::: ) "(" "X" "," (Set ($#k4_convfun1 :::"RLS_Real"::: ) ) ")" ")" ) equals :: CONVFUN1:def 5 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) where x "is" ($#m1_subset_1 :::"Element":::) "of" "X", y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set "f" ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "y")))) "}" ; end; :: deftheorem defines :::"epigraph"::: CONVFUN1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool (Set ($#k5_convfun1 :::"epigraph"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) where x "is" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")), y "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) : (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "y")))) "}" ))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ); attr "f" is :::"convex"::: means :: CONVFUN1:def 6 (Bool (Set ($#k5_convfun1 :::"epigraph"::: ) "f") "is" ($#v1_convex1 :::"convex"::: ) ); end; :: deftheorem defines :::"convex"::: CONVFUN1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool (Set ($#k5_convfun1 :::"epigraph"::: ) (Set (Var "f"))) "is" ($#v1_convex1 :::"convex"::: ) ) ")" ))); theorem :: CONVFUN1:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "p")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x1")) ")" ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x2")) ")" ) ")" ))))) ")" ))) ; theorem :: CONVFUN1:5 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set (Var "p")) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x1")) ")" ) ")" ) ($#k3_supinf_2 :::"+"::: ) (Set "(" (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "p")) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x2")) ")" ) ")" ))))) ")" ))) ; begin theorem :: CONVFUN1:6 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k4_convfun1 :::"RLS_Real"::: ) )) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k4_convfun1 :::"RLS_Real"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "implies" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))))) "implies" (Bool (Set (Set (Var "g")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_supinf_1 :::"+infty"::: ) )) ")" ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "X")) "is" ($#v1_convex1 :::"convex"::: ) ) ")" ) ")" )))) ; begin theorem :: CONVFUN1:7 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) ")" ) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "z"))) ($#r2_hidden :::"in"::: ) (Set (Var "M")))))) ")" ))) ; begin theorem :: CONVFUN1:8 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "F")))))))) ")" ))) ; theorem :: CONVFUN1:9 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "," (Set ($#k7_numbers :::"ExtREAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_supinf_1 :::"-infty"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_convfun1 :::"convex"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k7_numbers :::"ExtREAL"::: ) ) (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k12_supinf_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_measure6 :::"R_EAL"::: ) (Set "(" (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_extreal1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" (Set (Var "y")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k12_supinf_2 :::"."::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "z")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_extreal1 :::"Sum"::: ) (Set (Var "F")))))))) ")" ))) ;