:: SIN_COS2 semantic presentation begin theorem :: SIN_COS2:1 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::">="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "p")) ($#k11_binop_2 :::"*"::: ) (Set (Var "r")) ")" ) ")" )))) ; theorem :: SIN_COS2:2 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS2:3 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS2:4 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS2:5 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS2:6 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SIN_COS2:7 (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS2:8 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) "," (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS2:9 (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SIN_COS2:10 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" ))))) ; theorem :: SIN_COS2:11 (Bool "for" (Set (Var "th")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "th"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "th")) ")" ))))) ; begin definitionfunc :::"sinh"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS2:def 1 (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))); end; :: deftheorem defines :::"sinh"::: SIN_COS2:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos2 :::"sinh"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ")" )); definitionlet "d" be ($#m1_hidden :::"number"::: ) ; func :::"sinh"::: "d" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS2:def 2 (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) "d"); end; :: deftheorem defines :::"sinh"::: SIN_COS2:def 2 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_sin_cos2 :::"sinh"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))); registrationlet "d" be ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_sin_cos2 :::"sinh"::: ) "d") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "d" be ($#m1_hidden :::"number"::: ) ; :: original: :::"sinh"::: redefine func :::"sinh"::: "d" -> ($#m1_subset_1 :::"Real":::); end; definitionfunc :::"cosh"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS2:def 3 (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))); end; :: deftheorem defines :::"cosh"::: SIN_COS2:def 3 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos2 :::"cosh"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2)))) ")" )); definitionlet "d" be ($#m1_hidden :::"number"::: ) ; func :::"cosh"::: "d" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS2:def 4 (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) "d"); end; :: deftheorem defines :::"cosh"::: SIN_COS2:def 4 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_sin_cos2 :::"cosh"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))); registrationlet "d" be ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k5_sin_cos2 :::"cosh"::: ) "d") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "d" be ($#m1_hidden :::"number"::: ) ; :: original: :::"cosh"::: redefine func :::"cosh"::: "d" -> ($#m1_subset_1 :::"Real":::); end; definitionfunc :::"tanh"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: SIN_COS2:def 5 (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" )))); end; :: deftheorem defines :::"tanh"::: SIN_COS2:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_sin_cos2 :::"tanh"::: ) )) "iff" (Bool "for" (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "d")) ")" ) ")" ) ")" )))) ")" )); definitionlet "d" be ($#m1_hidden :::"number"::: ) ; func :::"tanh"::: "d" -> ($#m1_hidden :::"set"::: ) equals :: SIN_COS2:def 6 (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) "d"); end; :: deftheorem defines :::"tanh"::: SIN_COS2:def 6 : (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k8_sin_cos2 :::"tanh"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))); registrationlet "d" be ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k8_sin_cos2 :::"tanh"::: ) "d") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "d" be ($#m1_hidden :::"number"::: ) ; :: original: :::"tanh"::: redefine func :::"tanh"::: "d" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SIN_COS2:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" )))) ; theorem :: SIN_COS2:13 (Bool (Set (Set ($#k24_sin_cos :::"exp_R"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: SIN_COS2:14 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS2:15 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ; theorem :: SIN_COS2:16 (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: SIN_COS2:17 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" )))) ; theorem :: SIN_COS2:18 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ))) & (Bool (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ))) ")" )) ; theorem :: SIN_COS2:19 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) & (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ))) ")" )) ; theorem :: SIN_COS2:20 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:21 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:22 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ")" ))) & (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:23 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:24 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: SIN_COS2:25 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "q")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "q")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "q")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "q")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: SIN_COS2:26 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:27 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:28 (Bool "for" (Set (Var "p")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k9_binop_2 :::"+"::: ) (Set (Var "r")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k10_binop_2 :::"-"::: ) (Set (Var "r")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ))) ")" )) ; theorem :: SIN_COS2:29 (Bool "for" (Set (Var "p")) "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 (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set (Var "p")) ")" ) ")" ))))) ; theorem :: SIN_COS2:30 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_sin_cos2 :::"sinh"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k4_sin_cos2 :::"cosh"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k7_sin_cos2 :::"tanh"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ")" ) ; theorem :: SIN_COS2:31 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS2:32 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS2:33 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#r1_fdiff_1 :::"is_differentiable_in"::: ) (Set (Var "p"))) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: SIN_COS2:34 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS2:35 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")))) ")" )) ; theorem :: SIN_COS2:36 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) & (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k7_sin_cos2 :::"tanh"::: ) ) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" )) ; theorem :: SIN_COS2:37 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ; theorem :: SIN_COS2:38 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Var "p")))) ; theorem :: SIN_COS2:39 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Var "p")))) ; theorem :: SIN_COS2:40 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#r1_fcont_1 :::"is_continuous_in"::: ) (Set (Var "p")))) ; theorem :: SIN_COS2:41 (Bool (Set (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS2:42 (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS2:43 (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SIN_COS2:44 (Bool "for" (Set (Var "p")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set ($#k7_sin_cos2 :::"tanh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )) ;