:: SIN_COS4  semantic presentation begin  





definitionlet "th" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"tan"::: "th" ->   ($#m1_subset_1 :::"Real":::) equals :: SIN_COS4:def 1 (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  "th" ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  "th" ")" )); end; 





:: deftheorem    defines :::"tan"::: SIN_COS4:def 1 :  (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )))); 
 definitionlet "th" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"cot"::: "th" ->   ($#m1_subset_1 :::"Real":::) equals :: SIN_COS4:def 2 (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  "th" ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  "th" ")" )); end; 





:: deftheorem    defines :::"cot"::: SIN_COS4:def 2 :  (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" )))); 
 definitionlet "th" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"cosec"::: "th" ->   ($#m1_subset_1 :::"Real":::) equals :: SIN_COS4:def 3 (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  "th" ")" )); end; 





:: deftheorem    defines :::"cosec"::: SIN_COS4:def 3 :  (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_sin_cos4 :::"cosec"::: )  (Set (Var "th")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" )))); 
 definitionlet "th" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"sec"::: "th" ->   ($#m1_subset_1 :::"Real":::) equals :: SIN_COS4:def 4 (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  "th" ")" )); end; 





:: deftheorem    defines :::"sec"::: SIN_COS4:def 4 :  (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k4_sin_cos4 :::"sec"::: )  (Set (Var "th")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )))); 
 
theorem :: SIN_COS4:1 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "th")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th")) ")" )))) ; 
 
theorem :: SIN_COS4:2 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_sin_cos4 :::"cosec"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "th")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:3 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "th")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th")) ")" )))) ; 
 
theorem :: SIN_COS4:4 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:5 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:6 (Bool  "for" (Set (Var "th")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th")) ")" )))) ; 
 
theorem :: SIN_COS4:7 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:8 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:9 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:10 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Num 1) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:11 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:12 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:13 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:14 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th3")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Num 1) ")" )))) ; 
 
theorem :: SIN_COS4:15 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:16 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:17 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:18 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:19 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:20 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:21 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:22 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:23 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:24 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:25 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:26 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:27 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:28 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:29 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:30 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:31 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:32 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:33 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th3"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:34 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th3"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:35 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th3"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:36 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "," (Set (Var "th3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k7_xcmplx_0 :::"/"::: )  (Num 4) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th2"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th1")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th3"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th3")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:37 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:38 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:39 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:40 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:41 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:42 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:43 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:44 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 1)  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set (Var "th2")) ")" ) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:45 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )))) ; 
 
theorem :: SIN_COS4:46 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: SIN_COS4:47 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_sin_cos4 :::"tan"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: SIN_COS4:48 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: SIN_COS4:49 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" )))) ; 
 
theorem :: SIN_COS4:50 (Bool  "for" (Set (Var "th1")) "," (Set (Var "th2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "th2")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "th2")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k2_sin_cos4 :::"cot"::: )  (Set  "(" (Set  "(" (Set (Var "th2"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "th1")) ")" )  ($#k7_xcmplx_0 :::"/"::: )  (Num 2) ")" ) ")" )))) ;