:: DIFF_3 semantic presentation begin theorem :: DIFF_3:1 (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")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:2 (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 "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:3 (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")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:4 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (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 (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_3:5 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:6 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:7 (Bool "for" (Set (Var "h")) "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 "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1)) ($#r2_relset_1 :::"="::: ) (Set ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )))) ; theorem :: DIFF_3:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (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 (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:10 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:11 (Bool "for" (Set (Var "h")) "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 "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1)) ($#r2_relset_1 :::"="::: ) (Set ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )))) ; theorem :: DIFF_3:12 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_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 "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: DIFF_3:13 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (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 (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_3:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set "(" (Set (Var "r1")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (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 (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))))) ; theorem :: DIFF_3:16 (Bool "for" (Set (Var "h")) "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 "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1)) ($#r2_relset_1 :::"="::: ) (Set ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )))) ; theorem :: DIFF_3:17 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_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 "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "m")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: DIFF_3:18 (Bool "for" (Set (Var "n")) "being" ($#m1_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"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (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 "(" (Set (Var "n")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (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 "(" (Set (Var "n")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))))) ; theorem :: DIFF_3:19 (Bool "for" (Set (Var "n")) "being" ($#m1_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"::: ) ) "st" (Bool (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )))) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k5_real_1 :::"-"::: ) (Num 1) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )))))) ; theorem :: DIFF_3:20 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "h")))))) ; theorem :: DIFF_3:21 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set (Var "x")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "h")))))) ; theorem :: DIFF_3:22 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "h")))))) ; theorem :: DIFF_3:23 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "h")))))) ; theorem :: DIFF_3:24 (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"::: ) ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) "," (Set (Var "x")) "," (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 2) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ))))) ; theorem :: DIFF_3:25 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_3:26 (Bool "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ) ($#k7_real_1 :::"+"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_3:27 (Bool "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_3:28 (Bool "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ))))) ; theorem :: DIFF_3:29 (Bool "for" (Set (Var "r")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ))))) ; theorem :: DIFF_3:30 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set (Var "r1")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r1")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f1")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r2")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ")" ))))) ; theorem :: DIFF_3:31 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: DIFF_3:32 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "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 (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x2")) "," (Set (Var "x1")) ($#k10_diff_1 :::"!]"::: ) )))) ; theorem :: DIFF_3:33 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Seq_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k6_newton :::"choose"::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "i")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k4_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" (Set (Var "S")) ($#k12_diff_1 :::"."::: ) (Num 1) ")" ) "," (Num 1) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 2) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" (Set (Var "S")) ($#k12_diff_1 :::"."::: ) (Num 2) ")" ) "," (Num 2) ")" )) ")" )))) ; theorem :: DIFF_3:34 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))) ; theorem :: DIFF_3:35 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Seq_Sequence":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k6_newton :::"choose"::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "i")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f2")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k7_nat_d :::"-'"::: ) (Set (Var "i")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k4_real_1 :::"*"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" (Set (Var "S")) ($#k12_diff_1 :::"."::: ) (Num 1) ")" ) "," (Num 1) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 2) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_series_1 :::"Sum"::: ) "(" (Set "(" (Set (Var "S")) ($#k12_diff_1 :::"."::: ) (Num 2) ")" ) "," (Num 2) ")" )) ")" )))) ; theorem :: DIFF_3:36 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (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 (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ")" ))))) ; theorem :: DIFF_3:37 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x2")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:38 (Bool "for" (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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "x0")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x2")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x3")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "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 "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x3")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x3")) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x3")) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:39 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:40 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_3:41 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 ($#k7_square_1 :::"sqrt"::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:42 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")))))) ; theorem :: DIFF_3:43 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" ) & (Bool (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: DIFF_3:44 (Bool "for" (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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" ) & (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 ($#k6_numbers :::"0"::: ) )))) ; theorem :: DIFF_3: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"::: ) ) "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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" )) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3: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"::: ) ) "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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" )) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ))))) ; theorem :: DIFF_3: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"::: ) ) "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 "x")) ($#k5_square_1 :::"^2"::: ) )) ")" )) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")))))) ; theorem :: DIFF_3:48 (Bool "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "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")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "k")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:49 (Bool "for" (Set (Var "k")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "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")) ($#k10_real_1 :::"/"::: ) (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 "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set (Var "x0")) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "x2")) ")" ) ")" ))))) ; theorem :: DIFF_3:50 (Bool "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "h")) "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")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:51 (Bool "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "h")) "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")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:52 (Bool "for" (Set (Var "k")) "," (Set (Var "x")) "," (Set (Var "h")) "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")) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:53 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" )))) ; theorem :: DIFF_3:54 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:55 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:56 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:57 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x0")) ($#k7_real_1 :::"+"::: ) (Set (Var "x1")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x0")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x0")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" )))) ; theorem :: DIFF_3:58 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:59 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:60 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" )))) ; theorem :: DIFF_3:61 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ) ")" ))))) ; theorem :: DIFF_3:62 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:63 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 2) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ))))) ; theorem :: DIFF_3:64 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_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 (Var "h")) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:65 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ))))) ; theorem :: DIFF_3:66 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ))))) ; theorem :: DIFF_3:67 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ))))) ; theorem :: DIFF_3:68 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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")) ")" ) ")" ))))) ; theorem :: DIFF_3:69 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 16) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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_3:70 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 16) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_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")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:71 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 16) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_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")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:72 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 16) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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_3:73 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set (Var "x0")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1"))) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 16) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x0")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ))))) ; theorem :: DIFF_3:74 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 16) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_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")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:75 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 16) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_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")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "h")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))))) ; theorem :: DIFF_3:76 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Num 16) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (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_3:77 (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 ($#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 "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" )))) ; theorem :: DIFF_3:78 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:79 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_3:80 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (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")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:81 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ))))) ; theorem :: DIFF_3:82 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:83 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_3:84 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (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")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:85 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x0")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ))))) ; theorem :: DIFF_3:86 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:87 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_3:88 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k19_sin_cos :::"cos"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (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")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:89 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k9_real_1 :::"-"::: ) (Set (Var "x1")) ")" ))))) ; theorem :: DIFF_3:90 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_3:91 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_3:92 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k30_sin_cos :::"cot"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k16_sin_cos :::"sin"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (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")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k30_sin_cos :::"cot"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_3:93 (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (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"::: ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x0")) ")" ) ($#k8_real_1 :::"*"::: ) (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_3:94 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_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")) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: DIFF_3:95 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (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 (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_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")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: DIFF_3:96 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "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 "(" (Set ($#k29_sin_cos :::"tan"::: ) ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k29_sin_cos :::"tan"::: ) ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (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")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k29_sin_cos :::"tan"::: ) )))) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k8_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")) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ;