:: DIFF_4 semantic presentation begin theorem :: DIFF_4:1 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x0")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "x0")) ($#k13_complex1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ))) ; theorem :: DIFF_4:2 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x0")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set "(" (Set (Var "x0")) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ")" ))) ; theorem :: DIFF_4:3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_power :::"log"::: ) "(" (Set ($#k8_power :::"number_e"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))) ; theorem :: DIFF_4:4 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x0")) ($#k13_complex1 :::"/"::: ) (Set (Var "x1")) ")" )))) ; theorem :: DIFF_4:5 (Bool "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x2")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x3")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k11_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k11_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x0")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k11_complex1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k9_complex1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x3")) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k8_complex1 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x3")) ")" ))))) ; theorem :: DIFF_4:6 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:7 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:8 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k9_real_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:9 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "h")) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "h")) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:10 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) ; theorem :: DIFF_4:11 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: DIFF_4:12 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: DIFF_4:13 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_complex1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))) ; theorem :: DIFF_4:14 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) ; theorem :: DIFF_4:15 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:16 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:17 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: DIFF_4:18 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" )))) ; theorem :: DIFF_4:19 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:20 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:21 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 4) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "h")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:22 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))) ; theorem :: DIFF_4:23 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))) ; theorem :: DIFF_4:24 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: DIFF_4:25 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:26 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))) ; theorem :: DIFF_4:27 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))) ; theorem :: DIFF_4:28 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" )))) ; theorem :: DIFF_4:29 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:30 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x0")) ($#k13_complex1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" )))) ; theorem :: DIFF_4:31 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: DIFF_4:32 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:33 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set ($#k3_taylor_1 :::"ln"::: ) ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_taylor_1 :::"ln"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Num 1) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_4:34 (Bool "for" (Set (Var "h")) "," (Set (Var "k")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k25_sin_cos :::"exp_R"::: ) (Set "(" (Set (Var "h")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "h")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k25_sin_cos :::"exp_R"::: ) (Set (Var "k")) ")" )))) ; theorem :: DIFF_4:35 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:36 (Bool "for" (Set (Var "h")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_4:37 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: DIFF_4:38 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:39 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:40 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:41 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_4:42 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:43 (Bool "for" (Set (Var "h")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_4:44 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:45 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:46 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_4:47 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_4:48 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" )))))) ; theorem :: DIFF_4:49 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k10_complex1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:50 (Bool "for" (Set (Var "h")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "g")) "," (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_4:51 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:52 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_4:53 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_4:54 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_4:55 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" )))))) ; theorem :: DIFF_4:56 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) ; theorem :: DIFF_4:57 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ; theorem :: DIFF_4:58 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ; theorem :: DIFF_4:59 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ; theorem :: DIFF_4:60 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x0")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) ; theorem :: DIFF_4:61 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ; theorem :: DIFF_4:62 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ; theorem :: DIFF_4:63 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k30_sin_cos :::"cot"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_real_1 :::"""::: ) ")" ) ($#k2_newton :::"|^"::: ) (Num 2) ")" ) ")" )))) ;