:: SIN_COS8 semantic presentation begin theorem :: SIN_COS8:1 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: SIN_COS8:2 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k3_sin_cos5 :::"cosech"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "x")) ")" ))) ")" )) ; theorem :: SIN_COS8:3 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_sin_cos5 :::"sech"::: ) (Set (Var "x")))) & (Bool (Set ($#k2_sin_cos5 :::"sech"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS8:4 (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 ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS8:5 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:6 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ))) ")" ))) ; theorem :: SIN_COS8:7 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:8 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) ")" )) ; theorem :: SIN_COS8:9 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS8:10 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:11 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:12 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS8:13 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: SIN_COS8:14 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" )))) ; theorem :: SIN_COS8:15 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k1_sin_cos5 :::"coth"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" )))) ; theorem :: SIN_COS8:16 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS8:17 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS8:18 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:19 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS8:20 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y"))))) ; theorem :: SIN_COS8:21 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "w")) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "w")) ")" ))) & (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "w")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "z")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:22 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "w")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "z")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "w")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Set (Var "y")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "z")) ")" ) ")" )))) ; theorem :: SIN_COS8:23 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "z")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "w")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "w")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "w")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "w")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "z")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "w")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Set (Var "y")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "w")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS8:24 (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 "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" )))) ; theorem :: SIN_COS8:25 (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 "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" ) ")" )))) ; theorem :: SIN_COS8:26 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:27 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 1) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" ($#k9_sin_cos2 :::"tanh"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS8:28 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 7) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS8:29 (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 ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS8:30 (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 ($#k9_sin_cos2 :::"tanh"::: ) (Set "(" (Set (Var "x")) ($#k7_xcmplx_0 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS8:31 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 4))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 3) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 8))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 10) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 16))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 6)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 15) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 10) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 32))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 7)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 7) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 7) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 21) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 35) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 64))) & (Bool (Set (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 8)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 28) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 56) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 35) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 128))) ")" )) ; theorem :: SIN_COS8:32 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 4))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 3) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 8))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 5)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 10) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 16))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 6)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 15) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 10) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 32))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 7)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 7) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 7) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 5) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 21) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 35) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 64))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 8)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 28) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 56) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 35) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Num 128))) ")" )) ; theorem :: SIN_COS8:33 (Bool "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "z")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "y")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "z")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) ;