:: SIN_COS5 semantic presentation begin theorem :: SIN_COS5:1 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_sin_cos4 :::"cosec"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:2 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x3"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x3")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" )))) ; theorem :: SIN_COS5:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x3"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x3")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x3")) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS5:5 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:6 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SIN_COS5:7 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:8 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SIN_COS5:9 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SIN_COS5:10 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:11 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: SIN_COS5:12 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:13 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k4_sin_cos4 :::"sec"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k4_sin_cos4 :::"sec"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:14 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_sin_cos4 :::"cosec"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: SIN_COS5:15 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_sin_cos4 :::"cosec"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_sin_cos4 :::"cosec"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) & (Bool (Set ($#k3_sin_cos4 :::"cosec"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" )) ; theorem :: SIN_COS5:16 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:17 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:18 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS5:19 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k2_sin_cos4 :::"cot"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" )))) ; theorem :: SIN_COS5:20 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: SIN_COS5:21 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ; theorem :: SIN_COS5:22 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 4)))) ; theorem :: SIN_COS5:23 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 4)))) ; theorem :: SIN_COS5:24 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 8)))) ; theorem :: SIN_COS5:25 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 8)))) ; theorem :: SIN_COS5:26 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ))) "or" (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:27 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ))) "or" (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:28 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:29 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:30 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) "or" (Bool (Set ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:31 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:32 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k6_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:33 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) "or" (Bool (Set ($#k2_sin_cos4 :::"cot"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:34 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k4_sin_cos4 :::"sec"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ")" ))))) "holds" (Bool (Set ($#k4_sin_cos4 :::"sec"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS5:35 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos4 :::"tan"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set ($#k3_sin_cos4 :::"cosec"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ))))) "holds" (Bool (Set ($#k3_sin_cos4 :::"cosec"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k4_sin_cos4 :::"sec"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )))) ; definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"coth"::: "x" -> ($#m1_subset_1 :::"Real":::) equals :: SIN_COS5:def 1 (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) "x" ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) "x" ")" )); func :::"sech"::: "x" -> ($#m1_subset_1 :::"Real":::) equals :: SIN_COS5:def 2 (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) "x" ")" )); func :::"cosech"::: "x" -> ($#m1_subset_1 :::"Real":::) equals :: SIN_COS5:def 3 (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) "x" ")" )); end; :: deftheorem defines :::"coth"::: SIN_COS5:def 1 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" )))); :: deftheorem defines :::"sech"::: SIN_COS5:def 2 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" )))); :: deftheorem defines :::"cosech"::: SIN_COS5:def 3 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_sin_cos5 :::"cosech"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" )))); theorem :: SIN_COS5:36 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) & (Bool (Set ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) & (Bool (Set ($#k3_sin_cos5 :::"cosech"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:37 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS5:38 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS5:39 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_sin_cos5 :::"cosech"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: SIN_COS5:40 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" ) ")" )))) ; theorem :: SIN_COS5:41 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" ) ")" )))) ; theorem :: SIN_COS5:42 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x2")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS5:43 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" )))) ; theorem :: SIN_COS5:44 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:45 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS5:46 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS5:47 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS5:48 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )))) ; theorem :: SIN_COS5:49 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS5:50 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" )))) ; theorem :: SIN_COS5:51 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" )))) ; theorem :: SIN_COS5:52 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" )))) ;