REAL is V1() V44() V50() V51() V52() V56() set
NAT is V50() V51() V52() V53() V54() V55() V56() Element of bool REAL
bool REAL is set
[:NAT,REAL:] is V33() V34() V35() set
bool [:NAT,REAL:] is set
COMPLEX is V1() V44() V50() V56() set
RAT is V1() V44() V50() V51() V52() V53() V56() set
INT is V1() V44() V50() V51() V52() V53() V54() V56() set
0 is V1() V50() V51() V52() V53() V54() V55() V56() set
1 is V1() V10() V11() V12() ext-real positive V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
K21(0,1) is V1() set
[:REAL,REAL:] is V33() V34() V35() set
bool [:REAL,REAL:] is set
K69(REAL,REAL) is set
[:NAT,K69(REAL,REAL):] is set
bool [:NAT,K69(REAL,REAL):] is set
[:NAT,COMPLEX:] is V33() set
bool [:NAT,COMPLEX:] is set
[:COMPLEX,COMPLEX:] is V33() set
bool [:COMPLEX,COMPLEX:] is set
NAT is V50() V51() V52() V53() V54() V55() V56() set
bool NAT is set
bool NAT is set
0 is V1() V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() V56() Element of NAT
K20(0) is V1() V50() V51() V52() V53() V54() V55() set
2 is V1() V10() V11() V12() ext-real positive V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
K41(1,2) is V1() V11() V12() ext-real set
K39(2) is V1() V11() V12() ext-real positive set
K37(1,K39(2)) is V1() V11() V12() ext-real set
4 is V1() V10() V11() V12() ext-real positive V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
K41(1,4) is V1() V11() V12() ext-real set
K39(4) is V1() V11() V12() ext-real positive set
K37(1,K39(4)) is V1() V11() V12() ext-real set
tan is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
sin is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
cos is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
K274(REAL,REAL,sin,cos) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
dom tan is V50() V51() V52() Element of bool REAL
cot is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K274(REAL,REAL,cos,sin) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
dom cot is V50() V51() V52() Element of bool REAL
x is V11() V12() ext-real Element of REAL
x / 2 is V11() V12() ext-real Element of REAL
K37(x,K39(2)) is V11() V12() ext-real set
- (x / 2) is V11() V12() ext-real Element of REAL
h is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
cD (f,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x / 2 is V11() V12() ext-real Element of REAL
Shift (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
- (x / 2) is V11() V12() ext-real Element of REAL
Shift (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(x / 2))) - (Shift (f,(- (x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(cD (f,x)) . h is V11() V12() ext-real Element of REAL
fD (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(x / 2))) - f is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(fD (f,(x / 2))) . h is V11() V12() ext-real Element of REAL
fD (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(- (x / 2)))) - f is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(fD (f,(- (x / 2)))) . h is V11() V12() ext-real Element of REAL
((fD (f,(x / 2))) . h) - ((fD (f,(- (x / 2)))) . h) is V11() V12() ext-real Element of REAL
K38(((fD (f,(- (x / 2)))) . h)) is V11() V12() ext-real set
K36(((fD (f,(x / 2))) . h),K38(((fD (f,(- (x / 2)))) . h))) is V11() V12() ext-real set
h + (x / 2) is V11() V12() ext-real Element of REAL
f . (h + (x / 2)) is V11() V12() ext-real Element of REAL
f . h is V11() V12() ext-real Element of REAL
(f . (h + (x / 2))) - (f . h) is V11() V12() ext-real Element of REAL
K38((f . h)) is V11() V12() ext-real set
K36((f . (h + (x / 2))),K38((f . h))) is V11() V12() ext-real set
((f . (h + (x / 2))) - (f . h)) + (f . h) is V11() V12() ext-real Element of REAL
h - (x / 2) is V11() V12() ext-real Element of REAL
K38((x / 2)) is V11() V12() ext-real set
K36(h,K38((x / 2))) is V11() V12() ext-real set
f . (h - (x / 2)) is V11() V12() ext-real Element of REAL
(((f . (h + (x / 2))) - (f . h)) + (f . h)) - (f . (h - (x / 2))) is V11() V12() ext-real Element of REAL
K38((f . (h - (x / 2)))) is V11() V12() ext-real set
K36((((f . (h + (x / 2))) - (f . h)) + (f . h)),K38((f . (h - (x / 2))))) is V11() V12() ext-real set
(f . (h - (x / 2))) - (f . h) is V11() V12() ext-real Element of REAL
K36((f . (h - (x / 2))),K38((f . h))) is V11() V12() ext-real set
((f . (h + (x / 2))) - (f . h)) - ((f . (h - (x / 2))) - (f . h)) is V11() V12() ext-real Element of REAL
K38(((f . (h - (x / 2))) - (f . h))) is V11() V12() ext-real set
K36(((f . (h + (x / 2))) - (f . h)),K38(((f . (h - (x / 2))) - (f . h)))) is V11() V12() ext-real set
((fD (f,(x / 2))) . h) - ((f . (h - (x / 2))) - (f . h)) is V11() V12() ext-real Element of REAL
K36(((fD (f,(x / 2))) . h),K38(((f . (h - (x / 2))) - (f . h)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x / 2 is V11() V12() ext-real Element of REAL
K37(x,K39(2)) is V11() V12() ext-real set
- (x / 2) is V11() V12() ext-real Element of REAL
h is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
fD (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(- (x / 2)))) - f is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(fD (f,(- (x / 2)))) . h is V11() V12() ext-real Element of REAL
bD (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K38((x / 2)) is V11() V12() ext-real set
Shift (f,K38((x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
f - (Shift (f,K38((x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(bD (f,(x / 2))) . h is V11() V12() ext-real Element of REAL
- ((bD (f,(x / 2))) . h) is V11() V12() ext-real Element of REAL
h - (x / 2) is V11() V12() ext-real Element of REAL
K36(h,K38((x / 2))) is V11() V12() ext-real set
f . (h - (x / 2)) is V11() V12() ext-real Element of REAL
f . h is V11() V12() ext-real Element of REAL
(f . (h - (x / 2))) - (f . h) is V11() V12() ext-real Element of REAL
K38((f . h)) is V11() V12() ext-real set
K36((f . (h - (x / 2))),K38((f . h))) is V11() V12() ext-real set
(f . h) - (f . (h - (x / 2))) is V11() V12() ext-real Element of REAL
K38((f . (h - (x / 2)))) is V11() V12() ext-real set
K36((f . h),K38((f . (h - (x / 2))))) is V11() V12() ext-real set
- ((f . h) - (f . (h - (x / 2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x / 2 is V11() V12() ext-real Element of REAL
K37(x,K39(2)) is V11() V12() ext-real set
- (x / 2) is V11() V12() ext-real Element of REAL
h is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
cD (f,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x / 2 is V11() V12() ext-real Element of REAL
Shift (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
- (x / 2) is V11() V12() ext-real Element of REAL
Shift (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(x / 2))) - (Shift (f,(- (x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(cD (f,x)) . h is V11() V12() ext-real Element of REAL
bD (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K38((x / 2)) is V11() V12() ext-real set
Shift (f,K38((x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
f - (Shift (f,K38((x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(bD (f,(x / 2))) . h is V11() V12() ext-real Element of REAL
bD (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K38((- (x / 2))) is V11() V12() ext-real set
Shift (f,K38((- (x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
f - (Shift (f,K38((- (x / 2))))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(bD (f,(- (x / 2)))) . h is V11() V12() ext-real Element of REAL
((bD (f,(x / 2))) . h) - ((bD (f,(- (x / 2)))) . h) is V11() V12() ext-real Element of REAL
K38(((bD (f,(- (x / 2)))) . h)) is V11() V12() ext-real set
K36(((bD (f,(x / 2))) . h),K38(((bD (f,(- (x / 2)))) . h))) is V11() V12() ext-real set
fD (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (f,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(x / 2))) - f is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(fD (f,(x / 2))) . h is V11() V12() ext-real Element of REAL
- ((bD (f,(- (x / 2)))) . h) is V11() V12() ext-real Element of REAL
h + (x / 2) is V11() V12() ext-real Element of REAL
f . (h + (x / 2)) is V11() V12() ext-real Element of REAL
f . h is V11() V12() ext-real Element of REAL
(f . (h + (x / 2))) - (f . h) is V11() V12() ext-real Element of REAL
K38((f . h)) is V11() V12() ext-real set
K36((f . (h + (x / 2))),K38((f . h))) is V11() V12() ext-real set
h - (- (x / 2)) is V11() V12() ext-real Element of REAL
K36(h,K38((- (x / 2)))) is V11() V12() ext-real set
f . (h - (- (x / 2))) is V11() V12() ext-real Element of REAL
(f . h) - (f . (h - (- (x / 2)))) is V11() V12() ext-real Element of REAL
K38((f . (h - (- (x / 2))))) is V11() V12() ext-real set
K36((f . h),K38((f . (h - (- (x / 2)))))) is V11() V12() ext-real set
- ((f . h) - (f . (h - (- (x / 2))))) is V11() V12() ext-real Element of REAL
fD (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (f,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (f,(- (x / 2)))) - f is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(fD (f,(- (x / 2)))) . h is V11() V12() ext-real Element of REAL
(- ((bD (f,(- (x / 2)))) . h)) - ((fD (f,(- (x / 2)))) . h) is V11() V12() ext-real Element of REAL
K38(((fD (f,(- (x / 2)))) . h)) is V11() V12() ext-real set
K36((- ((bD (f,(- (x / 2)))) . h)),K38(((fD (f,(- (x / 2)))) . h))) is V11() V12() ext-real set
- ((bD (f,(x / 2))) . h) is V11() V12() ext-real Element of REAL
(- ((bD (f,(- (x / 2)))) . h)) - (- ((bD (f,(x / 2))) . h)) is V11() V12() ext-real Element of REAL
K38((- ((bD (f,(x / 2))) . h))) is V11() V12() ext-real set
K36((- ((bD (f,(- (x / 2)))) . h)),K38((- ((bD (f,(x / 2))) . h)))) is V11() V12() ext-real set
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((forward_difference (f,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) f) + x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (((h (#) f) + x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (((h (#) f) + x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (((h (#) f) + x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
forward_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(h * (((forward_difference (f,f)) . (x + 1)) . z)) + (((forward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
forward_difference ((h (#) f),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference ((h (#) f),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference ((h (#) f),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((forward_difference ((h (#) f),f)) . (x + 1)) . z) + (((forward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f + (h (#) x20) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference ((f + (h (#) x20)),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference ((f + (h (#) x20)),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference ((f + (h (#) x20)),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
forward_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((forward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
(((forward_difference (f,f)) . (x + 1)) . z) + (h * (((forward_difference (x20,f)) . (x + 1)) . z)) is V11() V12() ext-real Element of REAL
forward_difference ((h (#) x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference ((h (#) x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference ((h (#) x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((forward_difference (f,f)) . (x + 1)) . z) + (((forward_difference ((h (#) x20),f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (x20,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (x20,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (x20,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
h * (((forward_difference (x20,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f (#) x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) x20) - (f (#) x21) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (((h (#) x20) - (f (#) x21)),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
forward_difference (x21,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (x21,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference (x21,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
f * (((forward_difference (x21,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
(h * (((forward_difference (x20,z)) . (x + 1)) . f)) - (f * (((forward_difference (x21,z)) . (x + 1)) . f)) is V11() V12() ext-real Element of REAL
K38((f * (((forward_difference (x21,z)) . (x + 1)) . f))) is V11() V12() ext-real set
K36((h * (((forward_difference (x20,z)) . (x + 1)) . f)),K38((f * (((forward_difference (x21,z)) . (x + 1)) . f)))) is V11() V12() ext-real set
forward_difference ((h (#) x20),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference ((h (#) x20),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference ((h (#) x20),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
forward_difference ((f (#) x21),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference ((f (#) x21),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((forward_difference ((f (#) x21),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
(((forward_difference ((h (#) x20),z)) . (x + 1)) . f) - (((forward_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K38((((forward_difference ((f (#) x21),z)) . (x + 1)) . f)) is V11() V12() ext-real set
K36((((forward_difference ((h (#) x20),z)) . (x + 1)) . f),K38((((forward_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
(h * (((forward_difference (x20,z)) . (x + 1)) . f)) - (((forward_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K36((h * (((forward_difference (x20,z)) . (x + 1)) . f)),K38((((forward_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
h is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
forward_difference (h,x) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(forward_difference (h,x)) . 1 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
fD (h,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (h,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (h,x)) - h is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
0 + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(forward_difference (h,x)) . (0 + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(forward_difference (h,x)) . 0 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
fD (((forward_difference (h,x)) . 0),x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (((forward_difference (h,x)) . 0),x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (((forward_difference (h,x)) . 0),x)) - ((forward_difference (h,x)) . 0) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((backward_difference (f,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) f) + x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (((h (#) f) + x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (((h (#) f) + x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (((h (#) f) + x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
backward_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(h * (((backward_difference (f,f)) . (x + 1)) . z)) + (((backward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
backward_difference ((h (#) f),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference ((h (#) f),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference ((h (#) f),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((backward_difference ((h (#) f),f)) . (x + 1)) . z) + (((backward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f + (h (#) x20) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference ((f + (h (#) x20)),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference ((f + (h (#) x20)),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference ((f + (h (#) x20)),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
backward_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((backward_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
(((backward_difference (f,f)) . (x + 1)) . z) + (h * (((backward_difference (x20,f)) . (x + 1)) . z)) is V11() V12() ext-real Element of REAL
backward_difference ((h (#) x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference ((h (#) x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference ((h (#) x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((backward_difference (f,f)) . (x + 1)) . z) + (((backward_difference ((h (#) x20),f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (x20,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (x20,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (x20,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
h * (((backward_difference (x20,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f (#) x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) x20) - (f (#) x21) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (((h (#) x20) - (f (#) x21)),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
backward_difference (x21,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (x21,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (x21,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
f * (((backward_difference (x21,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
(h * (((backward_difference (x20,z)) . (x + 1)) . f)) - (f * (((backward_difference (x21,z)) . (x + 1)) . f)) is V11() V12() ext-real Element of REAL
K38((f * (((backward_difference (x21,z)) . (x + 1)) . f))) is V11() V12() ext-real set
K36((h * (((backward_difference (x20,z)) . (x + 1)) . f)),K38((f * (((backward_difference (x21,z)) . (x + 1)) . f)))) is V11() V12() ext-real set
backward_difference ((h (#) x20),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference ((h (#) x20),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference ((h (#) x20),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
backward_difference ((f (#) x21),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference ((f (#) x21),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference ((f (#) x21),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
(((backward_difference ((h (#) x20),z)) . (x + 1)) . f) - (((backward_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K38((((backward_difference ((f (#) x21),z)) . (x + 1)) . f)) is V11() V12() ext-real set
K36((((backward_difference ((h (#) x20),z)) . (x + 1)) . f),K38((((backward_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
(h * (((backward_difference (x20,z)) . (x + 1)) . f)) - (((backward_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K36((h * (((backward_difference (x20,z)) . (x + 1)) . f)),K38((((backward_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
h is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (h,x) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (h,x)) . 1 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
bD (h,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K38(x) is V11() V12() ext-real set
Shift (h,K38(x)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
h - (Shift (h,K38(x))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
0 + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (h,x)) . (0 + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(backward_difference (h,x)) . 0 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
bD (((backward_difference (h,x)) . 0),x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (((backward_difference (h,x)) . 0),K38(x)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (h,x)) . 0) - (Shift (((backward_difference (h,x)) . 0),K38(x))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + h is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (f,f)) . x is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
backward_difference (((backward_difference (f,f)) . x),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(backward_difference (((backward_difference (f,f)) . x),f)) . h is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (((backward_difference (f,f)) . x),f)) . h) . z is V11() V12() ext-real Element of REAL
(backward_difference (f,f)) . (x + h) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (f,f)) . (x + h)) . z is V11() V12() ext-real Element of REAL
(backward_difference (((backward_difference (f,f)) . x),f)) . 0 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x + 0 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (f,f)) . (x + 0) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x20 is V11() V12() ext-real Element of REAL
((backward_difference (((backward_difference (f,f)) . x),f)) . 0) . x20 is V11() V12() ext-real Element of REAL
((backward_difference (f,f)) . (x + 0)) . x20 is V11() V12() ext-real Element of REAL
x20 is V10() V11() V12() ext-real set
(backward_difference (((backward_difference (f,f)) . x),f)) . x20 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x + x20 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (f,f)) . (x + x20) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x20 + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (((backward_difference (f,f)) . x),f)) . (x20 + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x + (x20 + 1) is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (f,f)) . (x + (x20 + 1)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x21 is V11() V12() ext-real Element of REAL
((backward_difference (((backward_difference (f,f)) . x),f)) . (x20 + 1)) . x21 is V11() V12() ext-real Element of REAL
((backward_difference (f,f)) . (x + (x20 + 1))) . x21 is V11() V12() ext-real Element of REAL
bD (((backward_difference (((backward_difference (f,f)) . x),f)) . x20),f) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
K38(f) is V11() V12() ext-real set
Shift (((backward_difference (((backward_difference (f,f)) . x),f)) . x20),K38(f)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (((backward_difference (f,f)) . x),f)) . x20) - (Shift (((backward_difference (((backward_difference (f,f)) . x),f)) . x20),K38(f))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(bD (((backward_difference (((backward_difference (f,f)) . x),f)) . x20),f)) . x21 is V11() V12() ext-real Element of REAL
((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . x21 is V11() V12() ext-real Element of REAL
x21 - f is V11() V12() ext-real Element of REAL
K36(x21,K38(f)) is V11() V12() ext-real set
((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f) is V11() V12() ext-real Element of REAL
(((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . x21) - (((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f)) is V11() V12() ext-real Element of REAL
K38((((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f))) is V11() V12() ext-real set
K36((((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . x21),K38((((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f)))) is V11() V12() ext-real set
((backward_difference (f,f)) . (x + x20)) . x21 is V11() V12() ext-real Element of REAL
(((backward_difference (f,f)) . (x + x20)) . x21) - (((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f)) is V11() V12() ext-real Element of REAL
K36((((backward_difference (f,f)) . (x + x20)) . x21),K38((((backward_difference (((backward_difference (f,f)) . x),f)) . x20) . (x21 - f)))) is V11() V12() ext-real set
((backward_difference (f,f)) . (x + x20)) . (x21 - f) is V11() V12() ext-real Element of REAL
(((backward_difference (f,f)) . (x + x20)) . x21) - (((backward_difference (f,f)) . (x + x20)) . (x21 - f)) is V11() V12() ext-real Element of REAL
K38((((backward_difference (f,f)) . (x + x20)) . (x21 - f))) is V11() V12() ext-real set
K36((((backward_difference (f,f)) . (x + x20)) . x21),K38((((backward_difference (f,f)) . (x + x20)) . (x21 - f)))) is V11() V12() ext-real set
bD (((backward_difference (f,f)) . (x + x20)),f) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (((backward_difference (f,f)) . (x + x20)),K38(f)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (f,f)) . (x + x20)) - (Shift (((backward_difference (f,f)) . (x + x20)),K38(f))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(bD (((backward_difference (f,f)) . (x + x20)),f)) . x21 is V11() V12() ext-real Element of REAL
(x + x20) + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(backward_difference (f,f)) . ((x + x20) + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((backward_difference (f,f)) . ((x + x20) + 1)) . x21 is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((central_difference (f,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) f) + x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (((h (#) f) + x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (((h (#) f) + x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (((h (#) f) + x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
central_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(h * (((central_difference (f,f)) . (x + 1)) . z)) + (((central_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
central_difference ((h (#) f),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference ((h (#) f),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference ((h (#) f),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((central_difference ((h (#) f),f)) . (x + 1)) . z) + (((central_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (f,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (f,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (f,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f + (h (#) x20) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference ((f + (h (#) x20)),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference ((f + (h (#) x20)),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference ((f + (h (#) x20)),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
central_difference (x20,f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (x20,f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (x20,f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
h * (((central_difference (x20,f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
(((central_difference (f,f)) . (x + 1)) . z) + (h * (((central_difference (x20,f)) . (x + 1)) . z)) is V11() V12() ext-real Element of REAL
central_difference ((h (#) x20),f) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference ((h (#) x20),f)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference ((h (#) x20),f)) . (x + 1)) . z is V11() V12() ext-real Element of REAL
(((central_difference (f,f)) . (x + 1)) . z) + (((central_difference ((h (#) x20),f)) . (x + 1)) . z) is V11() V12() ext-real Element of REAL
x is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
x + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
h is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
z is V11() V12() ext-real Element of REAL
f is V11() V12() ext-real Element of REAL
x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
h (#) x20 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (x20,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (x20,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (x20,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
h * (((central_difference (x20,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
f (#) x21 is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
(h (#) x20) - (f (#) x21) is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (((h (#) x20) - (f (#) x21)),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (((h (#) x20) - (f (#) x21)),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
central_difference (x21,z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (x21,z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference (x21,z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
f * (((central_difference (x21,z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
(h * (((central_difference (x20,z)) . (x + 1)) . f)) - (f * (((central_difference (x21,z)) . (x + 1)) . f)) is V11() V12() ext-real Element of REAL
K38((f * (((central_difference (x21,z)) . (x + 1)) . f))) is V11() V12() ext-real set
K36((h * (((central_difference (x20,z)) . (x + 1)) . f)),K38((f * (((central_difference (x21,z)) . (x + 1)) . f)))) is V11() V12() ext-real set
central_difference ((h (#) x20),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference ((h (#) x20),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference ((h (#) x20),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
central_difference ((f (#) x21),z) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference ((f (#) x21),z)) . (x + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
((central_difference ((f (#) x21),z)) . (x + 1)) . f is V11() V12() ext-real Element of REAL
(((central_difference ((h (#) x20),z)) . (x + 1)) . f) - (((central_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K38((((central_difference ((f (#) x21),z)) . (x + 1)) . f)) is V11() V12() ext-real set
K36((((central_difference ((h (#) x20),z)) . (x + 1)) . f),K38((((central_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
(h * (((central_difference (x20,z)) . (x + 1)) . f)) - (((central_difference ((f (#) x21),z)) . (x + 1)) . f) is V11() V12() ext-real Element of REAL
K36((h * (((central_difference (x20,z)) . (x + 1)) . f)),K38((((central_difference ((f (#) x21),z)) . (x + 1)) . f))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
h is V1() V13() V16( REAL ) V17( REAL ) V18() V23( REAL ) V27( REAL , REAL ) V33() V34() V35() Element of bool [:REAL,REAL:]
central_difference (h,x) is V13() V16( NAT ) V17(K69(REAL,REAL)) V18() V27( NAT ,K69(REAL,REAL)) Element of bool [:NAT,K69(REAL,REAL):]
(central_difference (h,x)) . 1 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
cD (h,x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
x / 2 is V11() V12() ext-real Element of REAL
K37(x,K39(2)) is V11() V12() ext-real set
Shift (h,(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
- (x / 2) is V11() V12() ext-real Element of REAL
Shift (h,(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (h,(x / 2))) - (Shift (h,(- (x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
0 + 1 is V10() V11() V12() ext-real V43() V49() V50() V51() V52() V53() V54() V55() Element of NAT
(central_difference (h,x)) . (0 + 1) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(central_difference (h,x)) . 0 is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
cD (((central_difference (h,x)) . 0),x) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (((central_difference (h,x)) . 0),(x / 2)) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
Shift (((central_difference (h,x)) . 0),(- (x / 2))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34() V35() Element of bool [:REAL,REAL:]
(Shift (((central_difference (h,x)) . 0),(x / 2))) - (Shift (((central_difference (h,x)) . 0),(- (x / 2)))) is V13() V16( REAL ) V17( REAL ) V18() V33() V34()