:: SIN_COS7 semantic presentation begin theorem :: SIN_COS7:1 (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 (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_power :::"to_power"::: ) (Set "(" ($#k19_binop_2 :::"-"::: ) (Num 1) ")" )))) ; theorem :: SIN_COS7:2 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:3 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:4 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:5 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:6 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:7 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:8 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::">="::: ) (Num 1))) ; theorem :: SIN_COS7:9 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:10 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:11 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: SIN_COS7:12 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:13 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:14 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:15 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:16 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:17 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Num 1))) ; theorem :: SIN_COS7:18 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:19 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ))) ; theorem :: SIN_COS7:20 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Num 1))) ; theorem :: SIN_COS7:21 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ))) "holds" (Bool (Set (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:22 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:23 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:24 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:25 (Bool "for" (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "y")) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "x"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:27 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k19_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS7:28 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Num 1))) ; theorem :: SIN_COS7:29 (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 (Set ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Num 1))) ; theorem :: SIN_COS7:30 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1)) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: SIN_COS7:31 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "t")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "t")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) ; theorem :: SIN_COS7:32 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k19_binop_2 :::"-"::: ) (Num 1)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "t"))) & (Bool (Set (Var "t")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "t")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "t")) ")" )))) ; begin definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"sinh""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 1 (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" "x" ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"sinh""::: SIN_COS7:def 1 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"cosh1""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 2 (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" "x" ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"cosh1""::: SIN_COS7:def 2 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"cosh2""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 3 (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" "x" ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"cosh2""::: SIN_COS7:def 3 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" )))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"tanh""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 4 (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) "x" ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) "x" ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"tanh""::: SIN_COS7:def 4 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ")" )))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"coth""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 5 (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" "x" ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" "x" ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"coth""::: SIN_COS7:def 5 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_sin_cos7 :::"coth""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ")" )))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"sech1""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 6 (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) "x" ")" ) ")" ); end; :: deftheorem defines :::"sech1""::: SIN_COS7:def 6 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_sin_cos7 :::"sech1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ")" ))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"sech2""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 7 (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) "x" ")" ) ")" ")" )); end; :: deftheorem defines :::"sech2""::: SIN_COS7:def 7 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_sin_cos7 :::"sech2""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ")" ")" )))); definitionlet "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"csch""::: "x" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: SIN_COS7:def 8 (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) "x" ")" ) ")" ) if (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) "x") (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) "x" ")" ) ")" ) if (Bool "x" ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ; end; :: deftheorem defines :::"csch""::: SIN_COS7:def 8 : (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x")))) "implies" (Bool (Set ($#k8_sin_cos7 :::"csch""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_sin_cos7 :::"csch""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" ) ")" )) ")" ")" )); theorem :: SIN_COS7:33 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:34 (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 ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:35 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set (Var "x")) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:36 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:37 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS7:38 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:39 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:40 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:41 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Set (Var "x")) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:42 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:43 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:44 (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"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:45 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:46 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set ($#k5_sin_cos7 :::"coth""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS7: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"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k6_sin_cos7 :::"sech1""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS7:48 (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"::: ) )) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool (Set ($#k7_sin_cos7 :::"sech2""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS7:49 (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 ($#k8_sin_cos7 :::"csch""::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Num 1) ($#k12_binop_2 :::"/"::: ) (Set (Var "x")) ")" )))) ; theorem :: SIN_COS7:50 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:51 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k1_sin_cos7 :::"sinh""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:52 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:53 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:54 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k2_sin_cos7 :::"cosh1""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:55 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "x"))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set "(" ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k3_sin_cos7 :::"cosh2""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:56 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:57 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Set (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k11_binop_2 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:58 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SIN_COS7:59 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_sin_cos7 :::"tanh""::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SIN_COS7:60 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_sin_cos7 :::"cosh1""::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS7:61 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (Num 1)) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" )))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_sin_cos7 :::"cosh2""::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS7:62 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x")))) "holds" (Bool (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_sin_cos7 :::"sinh""::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: SIN_COS7:63 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "y")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ))) ; theorem :: SIN_COS7:64 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "y")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "y")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ")" )))) ; theorem :: SIN_COS7:65 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set (Var "y")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set (Var "y")) ")" ) ")" ) ")" ")" )))) ; theorem :: SIN_COS7:66 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k18_binop_2 :::"/"::: ) (Num 2) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Set (Var "y")) ($#k9_binop_2 :::"+"::: ) (Num 1) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set (Var "y")) ($#k10_binop_2 :::"-"::: ) (Num 1) ")" ) ")" ) ")" ")" )))) ; theorem :: SIN_COS7:67 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y")) ")" ) ")" )) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y")) ")" ) ")" ")" ))) ")" )) ; theorem :: SIN_COS7:68 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k12_binop_2 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "x")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k26_sin_cos :::"exp_R"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y")) ")" ) ")" )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set "(" (Num 1) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "y")) ")" ) ")" ))) ; theorem :: SIN_COS7:69 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: SIN_COS7:70 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: SIN_COS7:71 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set ($#k1_sin_cos2 :::"sinh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k4_sin_cos2 :::"cosh"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Num 1)))) ; theorem :: SIN_COS7:72 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_sin_cos2 :::"sinh"::: ) (Set "(" (Num 5) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 5) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 20) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k3_sin_cos2 :::"sinh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 5) ")" ) ")" )))) ; theorem :: SIN_COS7:73 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_sin_cos2 :::"cosh"::: ) (Set "(" (Num 5) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 5) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Num 20) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k6_sin_cos2 :::"cosh"::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 5) ")" ) ")" )))) ;