:: DIFF_1 semantic presentation begin definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Shift"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: DIFF_1:def 1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "h" ")" ) ($#k2_measure6 :::"++"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "h" ")" ) ($#k2_measure6 :::"++"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f" ")" )))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) "h" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Shift"::: DIFF_1:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "h")) ")" ) ($#k2_measure6 :::"++"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "h")) ")" ) ($#k2_measure6 :::"++"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ))) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"Shift"::: redefine func :::"Shift"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: DIFF_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) "h" ")" )))); end; :: deftheorem defines :::"Shift"::: DIFF_1:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" )))) ")" )))); definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"fD"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: DIFF_1:def 3 (Set (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" "f" "," "h" ")" ")" ) ($#k47_valued_1 :::"-"::: ) "f"); end; :: deftheorem defines :::"fD"::: DIFF_1:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set (Var "f")))))); registrationlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_diff_1 :::"fD"::: ) "(" "f" "," "h" ")" ) -> ($#v1_funct_2 :::"quasi_total"::: ) ; end; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"bD"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: DIFF_1:def 4 (Set "f" ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" "f" "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "h" ")" ) ")" ")" )); end; :: deftheorem defines :::"bD"::: DIFF_1:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "h")) ")" ) ")" ")" ))))); registrationlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_diff_1 :::"bD"::: ) "(" "f" "," "h" ")" ) -> ($#v1_funct_2 :::"quasi_total"::: ) ; end; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"cD"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: DIFF_1:def 5 (Set (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" "f" "," (Set "(" "h" ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" "f" "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" "h" ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" )); end; :: deftheorem defines :::"cD"::: DIFF_1:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k1_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k6_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ))))); registrationlet "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k5_diff_1 :::"cD"::: ) "(" "f" "," "h" ")" ) -> ($#v1_funct_2 :::"quasi_total"::: ) ; end; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"forward_difference"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: DIFF_1:def 6 (Bool "(" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) "f") & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" it ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," "h" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"forward_difference"::: DIFF_1:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_diff_1 :::"forward_difference"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k3_diff_1 :::"fD"::: ) "(" (Set "(" (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "h")) ")" )) ")" ) ")" ) ")" )))); notationlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"fdif"::: "(" "f" "," "h" ")" for :::"forward_difference"::: "(" "f" "," "h" ")" ; end; theorem :: DIFF_1:1 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "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 (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_1:2 (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"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))) ; theorem :: DIFF_1: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 "(" ($#k3_diff_1 :::"fD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_1:4 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_diff_1 :::"bD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_1:5 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_diff_1 :::"cD"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ; theorem :: DIFF_1:6 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: DIFF_1:7 (Bool "for" (Set (Var "n")) "being" ($#m2_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 "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_1:8 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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 (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 "(" (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_1:9 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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")) ($#k47_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")) ")" ) ($#k9_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_1:10 (Bool "for" (Set (Var "n")) "being" ($#m2_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")) ")" ) ($#k3_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")) ")" ) ")" ) ($#k7_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_1:11 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"backward_difference"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: DIFF_1:def 7 (Bool "(" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) "f") & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" it ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," "h" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"backward_difference"::: DIFF_1:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_diff_1 :::"backward_difference"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k4_diff_1 :::"bD"::: ) "(" (Set "(" (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "h")) ")" )) ")" ) ")" ) ")" )))); notationlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"bdif"::: "(" "f" "," "h" ")" for :::"backward_difference"::: "(" "f" "," "h" ")" ; end; theorem :: DIFF_1:12 (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"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))) ; theorem :: DIFF_1:13 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: DIFF_1:14 (Bool "for" (Set (Var "n")) "being" ($#m2_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 "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 (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_1:15 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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 (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 "(" (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_1:16 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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")) ($#k47_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")) ")" ) ($#k9_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_1:17 (Bool "for" (Set (Var "n")) "being" ($#m2_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")) ")" ) ($#k3_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")) ")" ) ")" ) ($#k7_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_1:18 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k7_diff_1 :::"bdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; definitionlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"central_difference"::: "(" "f" "," "h" ")" -> ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: DIFF_1:def 8 (Bool "(" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) "f") & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" it ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," "h" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"central_difference"::: DIFF_1:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_diff_1 :::"central_difference"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k5_diff_1 :::"cD"::: ) "(" (Set "(" (Set (Var "b3")) ($#k1_seqfunc :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "h")) ")" )) ")" ) ")" ) ")" )))); notationlet "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "h" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; synonym :::"cdif"::: "(" "f" "," "h" ")" for :::"central_difference"::: "(" "f" "," "h" ")" ; end; theorem :: DIFF_1:19 (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"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ))))) ; theorem :: DIFF_1:20 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: DIFF_1:21 (Bool "for" (Set (Var "n")) "being" ($#m2_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 "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 (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: DIFF_1:22 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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 (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 "(" (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_1:23 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "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")) ($#k47_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")) ")" ) ($#k9_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_1:24 (Bool "for" (Set (Var "n")) "being" ($#m2_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")) ")" ) ($#k3_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")) ")" ) ")" ) ($#k7_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_1:25 (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k8_diff_1 :::"cdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Num 1) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_diff_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ; theorem :: DIFF_1:26 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (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 (Var "n")) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))))) ; theorem :: DIFF_1:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (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 "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" )))))) ; theorem :: DIFF_1:28 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#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 "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )))))) ; definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "x0", "x1" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"[!":::"f" "," "x0" "," "x1":::"!]"::: -> ($#m1_subset_1 :::"Real":::) equals :: DIFF_1:def 9 (Set (Set "(" (Set "(" "f" ($#k1_seq_1 :::"."::: ) "x0" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" "f" ($#k1_seq_1 :::"."::: ) "x1" ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" "x0" ($#k6_xcmplx_0 :::"-"::: ) "x1" ")" )); end; :: deftheorem defines :::"[!"::: DIFF_1:def 9 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x0")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x1")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x1")) ")" ))))); definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "x0", "x1", "x2" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"[!":::"f" "," "x0" "," "x1" "," "x2":::"!]"::: -> ($#m1_subset_1 :::"Real":::) equals :: DIFF_1:def 10 (Set (Set "(" (Set ($#k9_diff_1 :::"[!"::: ) "f" "," "x0" "," "x1" ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) "f" "," "x1" "," "x2" ($#k9_diff_1 :::"!]"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" "x0" ($#k6_xcmplx_0 :::"-"::: ) "x2" ")" )); end; :: deftheorem defines :::"[!"::: DIFF_1:def 10 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k9_diff_1 :::"!]"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x2")) ")" ))))); definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "x0", "x1", "x2", "x3" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"[!":::"f" "," "x0" "," "x1" "," "x2" "," "x3":::"!]"::: -> ($#m1_subset_1 :::"Real":::) equals :: DIFF_1:def 11 (Set (Set "(" (Set ($#k10_diff_1 :::"[!"::: ) "f" "," "x0" "," "x1" "," "x2" ($#k10_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k10_diff_1 :::"[!"::: ) "f" "," "x1" "," "x2" "," "x3" ($#k10_diff_1 :::"!]"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" "x0" ($#k6_xcmplx_0 :::"-"::: ) "x3" ")" )); end; :: deftheorem defines :::"[!"::: DIFF_1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "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 ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) ) ($#k9_real_1 :::"-"::: ) (Set ($#k10_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k10_diff_1 :::"!]"::: ) ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x0")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x3")) ")" ))))); theorem :: DIFF_1:29 (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"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x1")) "," (Set (Var "x0")) ($#k9_diff_1 :::"!]"::: ) )))) ; theorem :: DIFF_1:30 (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 (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: DIFF_1:31 (Bool "for" (Set (Var "r")) "," (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"::: ) ) "holds" (Bool (Set ($#k9_diff_1 :::"[!"::: ) (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set ($#k9_diff_1 :::"[!"::: ) (Set (Var "f")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_1:32 (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")) ($#k3_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 ($#k9_diff_1 :::"[!"::: ) (Set (Var "f2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k9_diff_1 :::"!]"::: ) ))))) ; theorem :: DIFF_1:33 (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")) ")" ) ($#k3_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 :::"!]"::: ) ) ")" ) ($#k7_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_1:34 (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 "(" (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 "x1")) "," (Set (Var "x2")) "," (Set (Var "x0")) ($#k10_diff_1 :::"!]"::: ) )) & (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 "x2")) "," (Set (Var "x1")) "," (Set (Var "x0")) ($#k10_diff_1 :::"!]"::: ) )) ")" ))) ; theorem :: DIFF_1:35 (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 "(" (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 "x2")) "," (Set (Var "x0")) "," (Set (Var "x1")) ($#k10_diff_1 :::"!]"::: ) )) & (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 "x1")) "," (Set (Var "x0")) "," (Set (Var "x2")) ($#k10_diff_1 :::"!]"::: ) )) ")" ))) ; theorem :: DIFF_1:36 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "h")) "," (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (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 "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))))))) ; definitionlet "S" be ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "S" is :::"Sequence-yielding"::: means :: DIFF_1:def 12 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "S" ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Real_Sequence":::))); end; :: deftheorem defines :::"Sequence-yielding"::: DIFF_1:def 12 : (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_diff_1 :::"Sequence-yielding"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "S")) ($#k1_seqfunc :::"."::: ) (Set (Var "n"))) "is" ($#m1_subset_1 :::"Real_Sequence":::))) ")" )); registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_RELAT_1() bbbadV4_RELAT_1((Set ($#k5_numbers :::"NAT"::: ) )) bbbadV5_RELAT_1((Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_diff_1 :::"Sequence-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionmode Seq_Sequence is ($#v1_diff_1 :::"Sequence-yielding"::: ) ($#m1_subset_1 :::"Functional_Sequence":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "S" be ($#m1_subset_1 :::"Seq_Sequence":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"."::: redefine func "S" :::"."::: "n" -> ($#m1_subset_1 :::"Real_Sequence":::); end; theorem :: DIFF_1:37 (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" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k12_diff_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k6_newton :::"choose"::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (Set (Var "f1")) "," (Set (Var "h")) ")" ")" ) ($#k1_seqfunc :::"."::: ) (Set (Var "i")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (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")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k8_real_1 :::"*"::: ) (Set (Var "h")) ")" ) ")" ) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k6_diff_1 :::"fdif"::: ) "(" (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 "(" ($#k6_diff_1 :::"fdif"::: ) "(" (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_1:38 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "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 (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set (Var "h")) ")" ) ")" ))))) ; theorem :: DIFF_1:39 (Bool "for" (Set (Var "x")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (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 (Var "f")))) & (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 (Var "f"))))) "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 (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ))))) ;