:: CONVEX2 semantic presentation begin theorem :: CONVEX2:1 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "M")) "," (Set (Var "N")) "being" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "M")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "N"))) "is" ($#v1_convex1 :::"convex"::: ) ))) ; theorem :: CONVEX2:2 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (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 (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")) ")" )))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "u")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "}" )) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: CONVEX2:3 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (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 (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")) ")" )))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "u")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "}" )) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: CONVEX2:4 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (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 (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")) ")" )))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "u")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "}" )) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: CONVEX2:5 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_bhsp_1 :::"RealUnitarySpace-like"::: ) ($#l1_bhsp_1 :::"UNITSTR"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) (Bool "for" (Set (Var "B")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) "{" (Set (Var "u")) where u "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) : (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 (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "B")) ")" )))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "u")) ($#k1_bhsp_1 :::".|."::: ) (Set (Var "v"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ))) "}" )) "holds" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ))))) ; theorem :: CONVEX2:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L")) "being" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "N")) "st" (Bool (Bool (Set (Var "L")) "is" ($#v2_convex1 :::"convex"::: ) ) & (Bool (Set (Var "N")) ($#r1_tarski :::"c="::: ) (Set (Var "M")))) "holds" (Bool (Set ($#k6_rlvect_2 :::"Sum"::: ) (Set (Var "L"))) ($#r2_hidden :::"in"::: ) (Set (Var "M")))) ")" ) "iff" (Bool (Set (Var "M")) "is" ($#v1_convex1 :::"convex"::: ) ) ")" ))) ; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); func :::"LinComb"::: "M" -> ($#m1_hidden :::"set"::: ) means :: CONVEX2:def 1 (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "L")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" "M") ")" )); end; :: deftheorem defines :::"LinComb"::: CONVEX2:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_convex2 :::"LinComb"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "L")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "L")) "is" ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "M"))) ")" )) ")" )))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() ($#v2_convex1 :::"convex"::: ) for ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V"; end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); mode Convex_Combination of "V" is ($#v2_convex1 :::"convex"::: ) ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" "V"; end; registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) bbbadV1_VALUED_0() bbbadV2_VALUED_0() bbbadV3_VALUED_0() ($#v2_convex1 :::"convex"::: ) for ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" "M"; end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "M" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); mode Convex_Combination of "M" is ($#v2_convex1 :::"convex"::: ) ($#m2_rlvect_2 :::"Linear_Combination"::: ) "of" "M"; end; theorem :: CONVEX2:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k2_convex1 :::"Convex-Family"::: ) (Set (Var "M"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CONVEX2:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" )) "is" ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")))))) ; theorem :: CONVEX2:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" )) "is" ($#m2_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "M"))))))) ; begin theorem :: CONVEX2:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W1")) ")" ) ($#k7_rusub_4 :::"+"::: ) (Set "(" ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W2")) ")" ))))) ; theorem :: CONVEX2:11 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set ($#k3_rusub_4 :::"Up"::: ) (Set "(" (Set (Var "W1")) ($#k2_rlsub_2 :::"/\"::: ) (Set (Var "W2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k3_rusub_4 :::"Up"::: ) (Set (Var "W2")) ")" ))))) ; theorem :: CONVEX2:12 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L1")) "," (Set (Var "L2")) "being" ($#m1_rlvect_2 :::"Convex_Combination":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ($#k7_rlvect_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set (Var "a")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L1")) ")" ) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k3_rlvect_2 :::"Carrier"::: ) (Set "(" (Set (Var "b")) ($#k8_rlvect_2 :::"*"::: ) (Set (Var "L2")) ")" ) ")" )))))) ; theorem :: CONVEX2:13 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "z1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "z2")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set (Var "z2"))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "z1")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "z2")))) ")" )))) ; theorem :: CONVEX2:14 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L"))))) "holds" (Bool "ex" (Set (Var "L1")) "being" ($#m1_rlvect_2 :::"Linear_Combination"::: ) "of" (Set (Var "V")) "st" (Bool (Set ($#k3_rlvect_2 :::"Carrier"::: ) (Set (Var "L1"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ;