:: SIN_COS3 semantic presentation begin definitionfunc :::"sin_C"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: SIN_COS3:def 1 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))); end; :: deftheorem defines :::"sin_C"::: SIN_COS3:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos3 :::"sin_C"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ")" )); definitionfunc :::"cos_C"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: SIN_COS3:def 2 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))); end; :: deftheorem defines :::"cos_C"::: SIN_COS3:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos3 :::"cos_C"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))) ")" )); definitionfunc :::"sinh_C"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: SIN_COS3:def 3 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))); end; :: deftheorem defines :::"sinh_C"::: SIN_COS3:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos3 :::"sinh_C"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))) ")" )); definitionfunc :::"cosh_C"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) means :: SIN_COS3:def 4 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))); end; :: deftheorem defines :::"cosh_C"::: SIN_COS3:def 4 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos3 :::"cosh_C"::: ) )) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))) ")" )); begin theorem :: SIN_COS3:1 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS3:2 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:3 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:4 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:5 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:6 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:7 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:8 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS3:9 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:10 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:11 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:12 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:13 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:14 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )))) ; theorem :: SIN_COS3:15 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:16 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z"))))) ; theorem :: SIN_COS3:17 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:18 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z"))))) ; theorem :: SIN_COS3:19 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:20 (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: SIN_COS3:21 (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: SIN_COS3:22 (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: SIN_COS3:23 (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: SIN_COS3:24 (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: SIN_COS3:25 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:26 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )))) ; theorem :: SIN_COS3:27 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set (Var "z")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k15_sin_cos :::"exp"::: ) (Set (Var "z"))))) ; theorem :: SIN_COS3:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS3:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS3:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS3:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k23_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS3:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k15_binop_2 :::"+"::: ) (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_complex1 :::""::: ) ))) ; theorem :: SIN_COS3:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k15_binop_2 :::"+"::: ) (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Num 1) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:34 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")))))) ; theorem :: SIN_COS3:35 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k24_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")))))) ; theorem :: SIN_COS3:36 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS3:37 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS3:38 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ; theorem :: SIN_COS3:39 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ; theorem :: SIN_COS3:40 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ; theorem :: SIN_COS3:41 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))))) ; theorem :: SIN_COS3:42 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:43 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:44 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:45 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:46 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:47 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:48 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:49 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: SIN_COS3:50 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))))) ; theorem :: SIN_COS3:51 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "n")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))))) ; theorem :: SIN_COS3:52 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")))))) ; theorem :: SIN_COS3:53 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k15_sin_cos :::"exp"::: ) (Set "(" ($#k1_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set (Var "n")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_sin_cos3 :::"cos_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k7_complex1 :::""::: ) ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos3 :::"sin_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_comseq_3 :::"#N"::: ) (Set (Var "n")))))) ; theorem :: SIN_COS3:54 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k3_binop_2 :::"+"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )))) ; theorem :: SIN_COS3:55 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k3_binop_2 :::"+"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "x")) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )))) ; theorem :: SIN_COS3:56 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))) ; theorem :: SIN_COS3:57 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k6_binop_2 :::"/"::: ) (Num 2)))) ; theorem :: SIN_COS3:58 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Num 1))) ")" )) ; theorem :: SIN_COS3:59 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS3:60 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS3:61 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS3:62 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set ($#k4_sin_cos3 :::"cosh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set ($#k3_sin_cos3 :::"sinh_C"::: ) ) ($#k10_funct_2 :::"/."::: ) (Set "(" (Set (Var "z1")) ($#k4_binop_2 :::"-"::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ;