:: FUNCT_9 semantic presentation begin definitionlet "t" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "F" be ($#m1_hidden :::"Function":::); attr "F" is "t" :::"-periodic"::: means :: FUNCT_9:def 1 (Bool "(" (Bool "t" ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "implies" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) "t") ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) "t") ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "implies" (Bool (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) "t" ")" ))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"-periodic"::: FUNCT_9:def 1 : (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "implies" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) ")" & "(" (Bool (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "implies" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) ")" & "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "implies" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" ))) ")" ")" ) ")" ) ")" ) ")" ))); definitionlet "F" be ($#m1_hidden :::"Function":::); attr "F" is :::"periodic"::: means :: FUNCT_9:def 2 (Bool "ex" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "F" "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )); end; :: deftheorem defines :::"periodic"::: FUNCT_9:def 2 : (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_9 :::"periodic"::: ) ) "iff" (Bool "ex" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) ")" )); theorem :: FUNCT_9:1 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" ))) ")" ) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_9:2 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_valued_1 :::"+"::: ) (Set (Var "G"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:3 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k45_valued_1 :::"-"::: ) (Set (Var "G"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:4 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "G"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:5 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "G")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k50_valued_1 :::"/""::: ) (Set (Var "G"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:6 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "F"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:7 (Bool "for" (Set (Var "t")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "F"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:8 (Bool "for" (Set (Var "t")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "r")) ($#k7_valued_1 :::"+"::: ) (Set (Var "F"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:9 (Bool "for" (Set (Var "t")) "," (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k13_valued_1 :::"-"::: ) (Set (Var "r"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:10 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set ($#k54_valued_1 :::"|."::: ) (Set (Var "F")) ($#k54_valued_1 :::".|"::: ) ) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:11 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k35_valued_1 :::"""::: ) ) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:12 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k39_valued_1 :::"^2"::: ) ) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:13 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t")) ")" )))))) ; theorem :: FUNCT_9:14 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) "holds" (Bool (Set (Var "F")) "is" (Set ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "t"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:15 (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t1")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" (Set (Var "t2")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Set (Var "t1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "F")) "is" (Set (Set (Var "t1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:16 (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "is" (Set (Var "t1")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" (Set (Var "t2")) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Set (Var "t1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "F")) "is" (Set (Set (Var "t1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:17 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t")) ")" ))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t"))) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_funct_9 :::"periodic"::: ) ) ")" ))) ; theorem :: FUNCT_9:18 (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "t1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2")) ")" ))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Set (Var "t1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_funct_9 :::"periodic"::: ) ) ")" ))) ; theorem :: FUNCT_9:19 (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "t1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t1"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t2")) ")" ))) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Set (Var "t1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t2"))) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_funct_9 :::"periodic"::: ) ) ")" ))) ; theorem :: FUNCT_9:20 (Bool "for" (Set (Var "t")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "F")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "t"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )) ")" ) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) "is" (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "t"))) ($#v1_funct_9 :::"-periodic"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_funct_9 :::"periodic"::: ) ) ")" ))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v2_funct_9 :::"periodic"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v2_funct_9 :::"periodic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registrationlet "t" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_funcop_1 :::"-->"::: ) "t") -> "t" ($#v1_funct_9 :::"-periodic"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) "t" ($#v1_funct_9 :::"-periodic"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "t" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "F", "G" be ($#v3_valued_0 :::"real-valued"::: ) (Set (Const "t")) ($#v1_funct_9 :::"-periodic"::: ) ($#m1_hidden :::"Function":::); cluster (Set "F" ($#k1_valued_1 :::"+"::: ) "G") -> "t" ($#v1_funct_9 :::"-periodic"::: ) ; cluster (Set "F" ($#k45_valued_1 :::"-"::: ) "G") -> "t" ($#v1_funct_9 :::"-periodic"::: ) ; cluster (Set "F" ($#k18_valued_1 :::"(#)"::: ) "G") -> "t" ($#v1_funct_9 :::"-periodic"::: ) ; cluster (Set "F" ($#k50_valued_1 :::"/""::: ) "G") -> "t" ($#v1_funct_9 :::"-periodic"::: ) ; end; registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_funct_9 :::"periodic"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "F") -> ($#v2_funct_9 :::"periodic"::: ) ; end; registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_funct_9 :::"periodic"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "F") -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "F") -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set "F" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v2_funct_9 :::"periodic"::: ) ; end; registrationlet "F" be ($#v3_valued_0 :::"real-valued"::: ) ($#v2_funct_9 :::"periodic"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k54_valued_1 :::"|."::: ) "F" ($#k54_valued_1 :::".|"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set "F" ($#k35_valued_1 :::"""::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set "F" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; end; begin registration cluster (Set ($#k16_sin_cos :::"sin"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set ($#k19_sin_cos :::"cos"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; end; theorem :: FUNCT_9:21 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k16_sin_cos :::"sin"::: ) ) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:22 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k19_sin_cos :::"cos"::: ) ) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; registration cluster (Set ($#k2_fdiff_9 :::"cosec"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set ($#k1_fdiff_9 :::"sec"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; end; theorem :: FUNCT_9:23 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k1_fdiff_9 :::"sec"::: ) ) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:24 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k2_fdiff_9 :::"cosec"::: ) ) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; registration cluster (Set ($#k29_sin_cos :::"tan"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; cluster (Set ($#k30_sin_cos :::"cot"::: ) ) -> ($#v2_funct_9 :::"periodic"::: ) ; end; theorem :: FUNCT_9:25 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k29_sin_cos :::"tan"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:26 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k30_sin_cos :::"cot"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:27 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k55_valued_1 :::".|"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:28 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k55_valued_1 :::".|"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:29 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k55_valued_1 :::".|"::: ) ) ($#k3_valued_1 :::"+"::: ) (Set ($#k55_valued_1 :::"|."::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k55_valued_1 :::".|"::: ) )) "is" (Set (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:30 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k41_valued_1 :::"^2"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:31 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k41_valued_1 :::"^2"::: ) ) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:32 (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) )) "is" (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) )) ; theorem :: FUNCT_9:33 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "b")) ($#k9_valued_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" )) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:34 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "b"))) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:35 (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "b")) ($#k9_valued_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" )) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:36 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "b"))) "is" (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i"))) ($#v1_funct_9 :::"-periodic"::: ) ))) ; theorem :: FUNCT_9:37 (Bool "for" (Set (Var "t")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))) "is" (Set (Var "t")) ($#v1_funct_9 :::"-periodic"::: ) )) ; registrationlet "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_funcop_1 :::"-->"::: ) "a") -> ($#v2_funct_9 :::"periodic"::: ) ; end; registrationlet "t" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) "t" ($#v1_funct_9 :::"-periodic"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end;