:: DIFF_2 semantic presentation

REAL is V1() V44() V45() V46() V50() V59() set
NAT is V44() V45() V46() V47() V48() V49() V50() M2( bool REAL)
bool REAL is set
COMPLEX is V1() V44() V50() V59() set
[:REAL,REAL:] is complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is set
K81(REAL,REAL) is set
[:NAT,K81(REAL,REAL):] is set
bool [:NAT,K81(REAL,REAL):] is set
[:NAT,REAL:] is complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is set
0 is set
1 is V1() natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
K21(0,1) is set
[:NAT,COMPLEX:] is complex-valued set
bool [:NAT,COMPLEX:] is set
[:COMPLEX,COMPLEX:] is complex-valued set
bool [:COMPLEX,COMPLEX:] is set
RAT is V1() V44() V45() V46() V47() V50() V59() set
INT is V1() V44() V45() V46() V47() V48() V50() V59() set
0 is natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
2 is V1() natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
1 / 2 is V11() V12() real set
4 is V1() natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
1 / 4 is V11() V12() real set
K20(0) is V44() V45() V46() V47() V48() V49() set
tan is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
sin is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
cos is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
K167(REAL,REAL,sin,cos) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
K228(REAL,tan) is V44() V45() V46() M2( bool REAL)
cot is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
K167(REAL,REAL,cos,sin) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
K228(REAL,cot) is V44() V45() V46() M2( bool REAL)
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
x0 + x1 is V11() V12() real M2( REAL )
y is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,x0,(x0 + x1)!] is V11() V12() real M2( REAL )
K214(y,x0) is V11() V12() real M2( REAL )
K214(y,(x0 + x1)) is V11() V12() real M2( REAL )
K214(y,x0) - K214(y,(x0 + x1)) is V11() V12() real M2( REAL )
x0 - (x0 + x1) is V11() V12() real set
(K214(y,x0) - K214(y,(x0 + x1))) / (x0 - (x0 + x1)) is V11() V12() real M2( REAL )
forward_difference (y,x1) is Relation-like NAT -defined K81(REAL,REAL) -valued Function-like V30( NAT ,K81(REAL,REAL)) M2( bool [:NAT,K81(REAL,REAL):])
(forward_difference (y,x1)) . 1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((forward_difference (y,x1)) . 1) . x0 is V11() V12() real set
(((forward_difference (y,x1)) . 1) . x0) / x1 is V11() V12() real M2( REAL )
[!y,(x0 + x1),x0!] is V11() V12() real M2( REAL )
K214(y,(x0 + x1)) - K214(y,x0) is V11() V12() real M2( REAL )
(x0 + x1) - x0 is V11() V12() real set
(K214(y,(x0 + x1)) - K214(y,x0)) / ((x0 + x1) - x0) is V11() V12() real M2( REAL )
fD (y,x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
Shift (y,x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(Shift (y,x1)) - y is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(fD (y,x1)) . x0 is V11() V12() real set
((fD (y,x1)) . x0) / x1 is V11() V12() real M2( REAL )
(forward_difference (y,x1)) . 0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
fD (((forward_difference (y,x1)) . 0),x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
Shift (((forward_difference (y,x1)) . 0),x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(Shift (((forward_difference (y,x1)) . 0),x1)) - ((forward_difference (y,x1)) . 0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(fD (((forward_difference (y,x1)) . 0),x1)) . x0 is V11() V12() real set
((fD (((forward_difference (y,x1)) . 0),x1)) . x0) / x1 is V11() V12() real M2( REAL )
0 + 1 is natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
(forward_difference (y,x1)) . (0 + 1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((forward_difference (y,x1)) . (0 + 1)) . x0 is V11() V12() real set
(((forward_difference (y,x1)) . (0 + 1)) . x0) / x1 is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
2 * x0 is V11() V12() real M2( REAL )
x0 ^2 is V11() V12() real M2( REAL )
x0 * x0 is V11() V12() real set
2 * (x0 ^2) is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
x1 + x0 is V11() V12() real M2( REAL )
x1 + (2 * x0) is V11() V12() real M2( REAL )
y is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,x1,(x1 + x0),(x1 + (2 * x0))!] is V11() V12() real M2( REAL )
[!y,x1,(x1 + x0)!] is V11() V12() real M2( REAL )
K214(y,x1) is V11() V12() real M2( REAL )
K214(y,(x1 + x0)) is V11() V12() real M2( REAL )
K214(y,x1) - K214(y,(x1 + x0)) is V11() V12() real M2( REAL )
x1 - (x1 + x0) is V11() V12() real set
(K214(y,x1) - K214(y,(x1 + x0))) / (x1 - (x1 + x0)) is V11() V12() real M2( REAL )
[!y,(x1 + x0),(x1 + (2 * x0))!] is V11() V12() real M2( REAL )
K214(y,(x1 + (2 * x0))) is V11() V12() real M2( REAL )
K214(y,(x1 + x0)) - K214(y,(x1 + (2 * x0))) is V11() V12() real M2( REAL )
(x1 + x0) - (x1 + (2 * x0)) is V11() V12() real set
(K214(y,(x1 + x0)) - K214(y,(x1 + (2 * x0)))) / ((x1 + x0) - (x1 + (2 * x0))) is V11() V12() real M2( REAL )
[!y,x1,(x1 + x0)!] - [!y,(x1 + x0),(x1 + (2 * x0))!] is V11() V12() real M2( REAL )
x1 - (x1 + (2 * x0)) is V11() V12() real set
([!y,x1,(x1 + x0)!] - [!y,(x1 + x0),(x1 + (2 * x0))!]) / (x1 - (x1 + (2 * x0))) is V11() V12() real M2( REAL )
forward_difference (y,x0) is Relation-like NAT -defined K81(REAL,REAL) -valued Function-like V30( NAT ,K81(REAL,REAL)) M2( bool [:NAT,K81(REAL,REAL):])
(forward_difference (y,x0)) . 2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((forward_difference (y,x0)) . 2) . x1 is V11() V12() real set
(((forward_difference (y,x0)) . 2) . x1) / (2 * (x0 ^2)) is V11() V12() real M2( REAL )
(forward_difference (y,x0)) . 1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,(x1 + (2 * x0)),(x1 + x0),x1!] is V11() V12() real M2( REAL )
[!y,(x1 + (2 * x0)),(x1 + x0)!] is V11() V12() real M2( REAL )
K214(y,(x1 + (2 * x0))) - K214(y,(x1 + x0)) is V11() V12() real M2( REAL )
(x1 + (2 * x0)) - (x1 + x0) is V11() V12() real set
(K214(y,(x1 + (2 * x0))) - K214(y,(x1 + x0))) / ((x1 + (2 * x0)) - (x1 + x0)) is V11() V12() real M2( REAL )
[!y,(x1 + x0),x1!] is V11() V12() real M2( REAL )
K214(y,(x1 + x0)) - K214(y,x1) is V11() V12() real M2( REAL )
(x1 + x0) - x1 is V11() V12() real set
(K214(y,(x1 + x0)) - K214(y,x1)) / ((x1 + x0) - x1) is V11() V12() real M2( REAL )
[!y,(x1 + (2 * x0)),(x1 + x0)!] - [!y,(x1 + x0),x1!] is V11() V12() real M2( REAL )
(x1 + (2 * x0)) - x1 is V11() V12() real set
([!y,(x1 + (2 * x0)),(x1 + x0)!] - [!y,(x1 + x0),x1!]) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
[!y,(x1 + x0),(x1 + (2 * x0))!] - [!y,(x1 + x0),x1!] is V11() V12() real M2( REAL )
(x1 + (2 * x0)) - x1 is V11() V12() real M2( REAL )
([!y,(x1 + x0),(x1 + (2 * x0))!] - [!y,(x1 + x0),x1!]) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
(x1 + x0) + x0 is V11() V12() real M2( REAL )
[!y,(x1 + x0),((x1 + x0) + x0)!] is V11() V12() real M2( REAL )
K214(y,((x1 + x0) + x0)) is V11() V12() real M2( REAL )
K214(y,(x1 + x0)) - K214(y,((x1 + x0) + x0)) is V11() V12() real M2( REAL )
(x1 + x0) - ((x1 + x0) + x0) is V11() V12() real set
(K214(y,(x1 + x0)) - K214(y,((x1 + x0) + x0))) / ((x1 + x0) - ((x1 + x0) + x0)) is V11() V12() real M2( REAL )
[!y,(x1 + x0),((x1 + x0) + x0)!] - [!y,x1,(x1 + x0)!] is V11() V12() real M2( REAL )
([!y,(x1 + x0),((x1 + x0) + x0)!] - [!y,x1,(x1 + x0)!]) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
((forward_difference (y,x0)) . 1) . (x1 + x0) is V11() V12() real set
(((forward_difference (y,x0)) . 1) . (x1 + x0)) / x0 is V11() V12() real M2( REAL )
((((forward_difference (y,x0)) . 1) . (x1 + x0)) / x0) - [!y,x1,(x1 + x0)!] is V11() V12() real M2( REAL )
(((((forward_difference (y,x0)) . 1) . (x1 + x0)) / x0) - [!y,x1,(x1 + x0)!]) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
((forward_difference (y,x0)) . 1) . x1 is V11() V12() real set
(((forward_difference (y,x0)) . 1) . x1) / x0 is V11() V12() real M2( REAL )
((((forward_difference (y,x0)) . 1) . (x1 + x0)) / x0) - ((((forward_difference (y,x0)) . 1) . x1) / x0) is V11() V12() real M2( REAL )
(((((forward_difference (y,x0)) . 1) . (x1 + x0)) / x0) - ((((forward_difference (y,x0)) . 1) . x1) / x0)) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
(((forward_difference (y,x0)) . 1) . (x1 + x0)) - (((forward_difference (y,x0)) . 1) . x1) is V11() V12() real set
((((forward_difference (y,x0)) . 1) . (x1 + x0)) - (((forward_difference (y,x0)) . 1) . x1)) / x0 is V11() V12() real M2( REAL )
(((((forward_difference (y,x0)) . 1) . (x1 + x0)) - (((forward_difference (y,x0)) . 1) . x1)) / x0) / ((x1 + (2 * x0)) - x1) is V11() V12() real M2( REAL )
fD (((forward_difference (y,x0)) . 1),x0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
Shift (((forward_difference (y,x0)) . 1),x0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(Shift (((forward_difference (y,x0)) . 1),x0)) - ((forward_difference (y,x0)) . 1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(fD (((forward_difference (y,x0)) . 1),x0)) . x1 is V11() V12() real set
((fD (((forward_difference (y,x0)) . 1),x0)) . x1) / x0 is V11() V12() real M2( REAL )
(((fD (((forward_difference (y,x0)) . 1),x0)) . x1) / x0) / (2 * x0) is V11() V12() real M2( REAL )
1 + 1 is natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
(forward_difference (y,x0)) . (1 + 1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((forward_difference (y,x0)) . (1 + 1)) . x1 is V11() V12() real set
(((forward_difference (y,x0)) . (1 + 1)) . x1) / x0 is V11() V12() real M2( REAL )
((((forward_difference (y,x0)) . (1 + 1)) . x1) / x0) / (2 * x0) is V11() V12() real M2( REAL )
x0 * (2 * x0) is V11() V12() real M2( REAL )
(((forward_difference (y,x0)) . 2) . x1) / (x0 * (2 * x0)) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
x0 - x1 is V11() V12() real M2( REAL )
y is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,(x0 - x1),x0!] is V11() V12() real M2( REAL )
K214(y,(x0 - x1)) is V11() V12() real M2( REAL )
K214(y,x0) is V11() V12() real M2( REAL )
K214(y,(x0 - x1)) - K214(y,x0) is V11() V12() real M2( REAL )
(x0 - x1) - x0 is V11() V12() real set
(K214(y,(x0 - x1)) - K214(y,x0)) / ((x0 - x1) - x0) is V11() V12() real M2( REAL )
backward_difference (y,x1) is Relation-like NAT -defined K81(REAL,REAL) -valued Function-like V30( NAT ,K81(REAL,REAL)) M2( bool [:NAT,K81(REAL,REAL):])
(backward_difference (y,x1)) . 1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x1)) . 1) . x0 is V11() V12() real set
(((backward_difference (y,x1)) . 1) . x0) / x1 is V11() V12() real M2( REAL )
[!y,x0,(x0 - x1)!] is V11() V12() real M2( REAL )
K214(y,x0) - K214(y,(x0 - x1)) is V11() V12() real M2( REAL )
x0 - (x0 - x1) is V11() V12() real set
(K214(y,x0) - K214(y,(x0 - x1))) / (x0 - (x0 - x1)) is V11() V12() real M2( REAL )
bD (y,x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
- x1 is V11() V12() real set
Shift (y,(- x1)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
y - (Shift (y,(- x1))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(bD (y,x1)) . x0 is V11() V12() real set
((bD (y,x1)) . x0) / x1 is V11() V12() real M2( REAL )
(backward_difference (y,x1)) . 0 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
bD (((backward_difference (y,x1)) . 0),x1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
Shift (((backward_difference (y,x1)) . 0),(- x1)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x1)) . 0) - (Shift (((backward_difference (y,x1)) . 0),(- x1))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(bD (((backward_difference (y,x1)) . 0),x1)) . x0 is V11() V12() real set
((bD (((backward_difference (y,x1)) . 0),x1)) . x0) / x1 is V11() V12() real M2( REAL )
0 + 1 is natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
(backward_difference (y,x1)) . (0 + 1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x1)) . (0 + 1)) . x0 is V11() V12() real set
(((backward_difference (y,x1)) . (0 + 1)) . x0) / x1 is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
2 * x0 is V11() V12() real M2( REAL )
x0 ^2 is V11() V12() real M2( REAL )
x0 * x0 is V11() V12() real set
2 * (x0 ^2) is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
x1 - (2 * x0) is V11() V12() real M2( REAL )
x1 - x0 is V11() V12() real M2( REAL )
y is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,(x1 - (2 * x0)),(x1 - x0),x1!] is V11() V12() real M2( REAL )
[!y,(x1 - (2 * x0)),(x1 - x0)!] is V11() V12() real M2( REAL )
K214(y,(x1 - (2 * x0))) is V11() V12() real M2( REAL )
K214(y,(x1 - x0)) is V11() V12() real M2( REAL )
K214(y,(x1 - (2 * x0))) - K214(y,(x1 - x0)) is V11() V12() real M2( REAL )
(x1 - (2 * x0)) - (x1 - x0) is V11() V12() real set
(K214(y,(x1 - (2 * x0))) - K214(y,(x1 - x0))) / ((x1 - (2 * x0)) - (x1 - x0)) is V11() V12() real M2( REAL )
[!y,(x1 - x0),x1!] is V11() V12() real M2( REAL )
K214(y,x1) is V11() V12() real M2( REAL )
K214(y,(x1 - x0)) - K214(y,x1) is V11() V12() real M2( REAL )
(x1 - x0) - x1 is V11() V12() real set
(K214(y,(x1 - x0)) - K214(y,x1)) / ((x1 - x0) - x1) is V11() V12() real M2( REAL )
[!y,(x1 - (2 * x0)),(x1 - x0)!] - [!y,(x1 - x0),x1!] is V11() V12() real M2( REAL )
(x1 - (2 * x0)) - x1 is V11() V12() real set
([!y,(x1 - (2 * x0)),(x1 - x0)!] - [!y,(x1 - x0),x1!]) / ((x1 - (2 * x0)) - x1) is V11() V12() real M2( REAL )
backward_difference (y,x0) is Relation-like NAT -defined K81(REAL,REAL) -valued Function-like V30( NAT ,K81(REAL,REAL)) M2( bool [:NAT,K81(REAL,REAL):])
(backward_difference (y,x0)) . 2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x0)) . 2) . x1 is V11() V12() real set
(((backward_difference (y,x0)) . 2) . x1) / (2 * (x0 ^2)) is V11() V12() real M2( REAL )
(backward_difference (y,x0)) . 1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!y,x1,(x1 - x0),(x1 - (2 * x0))!] is V11() V12() real M2( REAL )
[!y,x1,(x1 - x0)!] is V11() V12() real M2( REAL )
K214(y,x1) - K214(y,(x1 - x0)) is V11() V12() real M2( REAL )
x1 - (x1 - x0) is V11() V12() real set
(K214(y,x1) - K214(y,(x1 - x0))) / (x1 - (x1 - x0)) is V11() V12() real M2( REAL )
[!y,(x1 - x0),(x1 - (2 * x0))!] is V11() V12() real M2( REAL )
K214(y,(x1 - x0)) - K214(y,(x1 - (2 * x0))) is V11() V12() real M2( REAL )
(x1 - x0) - (x1 - (2 * x0)) is V11() V12() real set
(K214(y,(x1 - x0)) - K214(y,(x1 - (2 * x0)))) / ((x1 - x0) - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
[!y,x1,(x1 - x0)!] - [!y,(x1 - x0),(x1 - (2 * x0))!] is V11() V12() real M2( REAL )
x1 - (x1 - (2 * x0)) is V11() V12() real set
([!y,x1,(x1 - x0)!] - [!y,(x1 - x0),(x1 - (2 * x0))!]) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
[!y,(x1 - x0),x1!] - [!y,(x1 - x0),(x1 - (2 * x0))!] is V11() V12() real M2( REAL )
x1 - (x1 - (2 * x0)) is V11() V12() real M2( REAL )
([!y,(x1 - x0),x1!] - [!y,(x1 - x0),(x1 - (2 * x0))!]) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
((backward_difference (y,x0)) . 1) . x1 is V11() V12() real set
(((backward_difference (y,x0)) . 1) . x1) / x0 is V11() V12() real M2( REAL )
((((backward_difference (y,x0)) . 1) . x1) / x0) - [!y,(x1 - x0),(x1 - (2 * x0))!] is V11() V12() real M2( REAL )
(((((backward_difference (y,x0)) . 1) . x1) / x0) - [!y,(x1 - x0),(x1 - (2 * x0))!]) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
(x1 - x0) - x0 is V11() V12() real M2( REAL )
[!y,((x1 - x0) - x0),(x1 - x0)!] is V11() V12() real M2( REAL )
K214(y,((x1 - x0) - x0)) is V11() V12() real M2( REAL )
K214(y,((x1 - x0) - x0)) - K214(y,(x1 - x0)) is V11() V12() real M2( REAL )
((x1 - x0) - x0) - (x1 - x0) is V11() V12() real set
(K214(y,((x1 - x0) - x0)) - K214(y,(x1 - x0))) / (((x1 - x0) - x0) - (x1 - x0)) is V11() V12() real M2( REAL )
((((backward_difference (y,x0)) . 1) . x1) / x0) - [!y,((x1 - x0) - x0),(x1 - x0)!] is V11() V12() real M2( REAL )
(((((backward_difference (y,x0)) . 1) . x1) / x0) - [!y,((x1 - x0) - x0),(x1 - x0)!]) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
((backward_difference (y,x0)) . 1) . (x1 - x0) is V11() V12() real set
(((backward_difference (y,x0)) . 1) . (x1 - x0)) / x0 is V11() V12() real M2( REAL )
((((backward_difference (y,x0)) . 1) . x1) / x0) - ((((backward_difference (y,x0)) . 1) . (x1 - x0)) / x0) is V11() V12() real M2( REAL )
(((((backward_difference (y,x0)) . 1) . x1) / x0) - ((((backward_difference (y,x0)) . 1) . (x1 - x0)) / x0)) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
(((backward_difference (y,x0)) . 1) . x1) - (((backward_difference (y,x0)) . 1) . (x1 - x0)) is V11() V12() real set
((((backward_difference (y,x0)) . 1) . x1) - (((backward_difference (y,x0)) . 1) . (x1 - x0))) / x0 is V11() V12() real M2( REAL )
(((((backward_difference (y,x0)) . 1) . x1) - (((backward_difference (y,x0)) . 1) . (x1 - x0))) / x0) / (x1 - (x1 - (2 * x0))) is V11() V12() real M2( REAL )
bD (((backward_difference (y,x0)) . 1),x0) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
- x0 is V11() V12() real set
Shift (((backward_difference (y,x0)) . 1),(- x0)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x0)) . 1) - (Shift (((backward_difference (y,x0)) . 1),(- x0))) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(bD (((backward_difference (y,x0)) . 1),x0)) . x1 is V11() V12() real set
((bD (((backward_difference (y,x0)) . 1),x0)) . x1) / x0 is V11() V12() real M2( REAL )
(((bD (((backward_difference (y,x0)) . 1),x0)) . x1) / x0) / (2 * x0) is V11() V12() real M2( REAL )
1 + 1 is natural V11() V12() real V44() V45() V46() V47() V48() V49() V57() V58() M3( REAL , NAT )
(backward_difference (y,x0)) . (1 + 1) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
((backward_difference (y,x0)) . (1 + 1)) . x1 is V11() V12() real set
(((backward_difference (y,x0)) . (1 + 1)) . x1) / x0 is V11() V12() real M2( REAL )
((((backward_difference (y,x0)) . (1 + 1)) . x1) / x0) / (2 * x0) is V11() V12() real M2( REAL )
x0 * (2 * x0) is V11() V12() real M2( REAL )
(((backward_difference (y,x0)) . 2) . x1) / (x0 * (2 * x0)) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V11() V12() real M2( REAL )
x3 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x0 (#) x3 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!(x0 (#) x3),x1,y,z!] is V11() V12() real M2( REAL )
[!(x0 (#) x3),x1,y!] is V11() V12() real M2( REAL )
K214((x0 (#) x3),x1) is V11() V12() real M2( REAL )
K214((x0 (#) x3),y) is V11() V12() real M2( REAL )
K214((x0 (#) x3),x1) - K214((x0 (#) x3),y) is V11() V12() real M2( REAL )
x1 - y is V11() V12() real set
(K214((x0 (#) x3),x1) - K214((x0 (#) x3),y)) / (x1 - y) is V11() V12() real M2( REAL )
[!(x0 (#) x3),y,z!] is V11() V12() real M2( REAL )
K214((x0 (#) x3),z) is V11() V12() real M2( REAL )
K214((x0 (#) x3),y) - K214((x0 (#) x3),z) is V11() V12() real M2( REAL )
y - z is V11() V12() real set
(K214((x0 (#) x3),y) - K214((x0 (#) x3),z)) / (y - z) is V11() V12() real M2( REAL )
[!(x0 (#) x3),x1,y!] - [!(x0 (#) x3),y,z!] is V11() V12() real M2( REAL )
x1 - z is V11() V12() real set
([!(x0 (#) x3),x1,y!] - [!(x0 (#) x3),y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!x3,x1,y,z!] is V11() V12() real M2( REAL )
[!x3,x1,y!] is V11() V12() real M2( REAL )
K214(x3,x1) is V11() V12() real M2( REAL )
K214(x3,y) is V11() V12() real M2( REAL )
K214(x3,x1) - K214(x3,y) is V11() V12() real M2( REAL )
(K214(x3,x1) - K214(x3,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!x3,y,z!] is V11() V12() real M2( REAL )
K214(x3,z) is V11() V12() real M2( REAL )
K214(x3,y) - K214(x3,z) is V11() V12() real M2( REAL )
(K214(x3,y) - K214(x3,z)) / (y - z) is V11() V12() real M2( REAL )
[!x3,x1,y!] - [!x3,y,z!] is V11() V12() real M2( REAL )
([!x3,x1,y!] - [!x3,y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
x0 * [!x3,x1,y,z!] is V11() V12() real M2( REAL )
x0 * [!x3,x1,y!] is V11() V12() real M2( REAL )
(x0 * [!x3,x1,y!]) - [!(x0 (#) x3),y,z!] is V11() V12() real M2( REAL )
x1 - z is V11() V12() real M2( REAL )
((x0 * [!x3,x1,y!]) - [!(x0 (#) x3),y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
x0 * [!x3,y,z!] is V11() V12() real M2( REAL )
(x0 * [!x3,x1,y!]) - (x0 * [!x3,y,z!]) is V11() V12() real M2( REAL )
((x0 * [!x3,x1,y!]) - (x0 * [!x3,y,z!])) / (x1 - z) is V11() V12() real M2( REAL )
x0 * ([!x3,x1,y!] - [!x3,y,z!]) is V11() V12() real M2( REAL )
(x0 * ([!x3,x1,y!] - [!x3,y,z!])) / (x1 - z) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!z,x0,x1,y!] is V11() V12() real M2( REAL )
[!z,x0,x1!] is V11() V12() real M2( REAL )
K214(z,x0) is V11() V12() real M2( REAL )
K214(z,x1) is V11() V12() real M2( REAL )
K214(z,x0) - K214(z,x1) is V11() V12() real M2( REAL )
x0 - x1 is V11() V12() real set
(K214(z,x0) - K214(z,x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!z,x1,y!] is V11() V12() real M2( REAL )
K214(z,y) is V11() V12() real M2( REAL )
K214(z,x1) - K214(z,y) is V11() V12() real M2( REAL )
x1 - y is V11() V12() real set
(K214(z,x1) - K214(z,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!z,x0,x1!] - [!z,x1,y!] is V11() V12() real M2( REAL )
x0 - y is V11() V12() real set
([!z,x0,x1!] - [!z,x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
x3 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
z + x3 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!(z + x3),x0,x1,y!] is V11() V12() real M2( REAL )
[!(z + x3),x0,x1!] is V11() V12() real M2( REAL )
K214((z + x3),x0) is V11() V12() real M2( REAL )
K214((z + x3),x1) is V11() V12() real M2( REAL )
K214((z + x3),x0) - K214((z + x3),x1) is V11() V12() real M2( REAL )
(K214((z + x3),x0) - K214((z + x3),x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!(z + x3),x1,y!] is V11() V12() real M2( REAL )
K214((z + x3),y) is V11() V12() real M2( REAL )
K214((z + x3),x1) - K214((z + x3),y) is V11() V12() real M2( REAL )
(K214((z + x3),x1) - K214((z + x3),y)) / (x1 - y) is V11() V12() real M2( REAL )
[!(z + x3),x0,x1!] - [!(z + x3),x1,y!] is V11() V12() real M2( REAL )
([!(z + x3),x0,x1!] - [!(z + x3),x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!x3,x0,x1,y!] is V11() V12() real M2( REAL )
[!x3,x0,x1!] is V11() V12() real M2( REAL )
K214(x3,x0) is V11() V12() real M2( REAL )
K214(x3,x1) is V11() V12() real M2( REAL )
K214(x3,x0) - K214(x3,x1) is V11() V12() real M2( REAL )
(K214(x3,x0) - K214(x3,x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!x3,x1,y!] is V11() V12() real M2( REAL )
K214(x3,y) is V11() V12() real M2( REAL )
K214(x3,x1) - K214(x3,y) is V11() V12() real M2( REAL )
(K214(x3,x1) - K214(x3,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!x3,x0,x1!] - [!x3,x1,y!] is V11() V12() real M2( REAL )
([!x3,x0,x1!] - [!x3,x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!z,x0,x1,y!] + [!x3,x0,x1,y!] is V11() V12() real M2( REAL )
[!z,x0,x1!] + [!x3,x0,x1!] is V11() V12() real M2( REAL )
([!z,x0,x1!] + [!x3,x0,x1!]) - [!(z + x3),x1,y!] is V11() V12() real M2( REAL )
x0 - y is V11() V12() real M2( REAL )
(([!z,x0,x1!] + [!x3,x0,x1!]) - [!(z + x3),x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!z,x1,y!] + [!x3,x1,y!] is V11() V12() real M2( REAL )
([!z,x0,x1!] + [!x3,x0,x1!]) - ([!z,x1,y!] + [!x3,x1,y!]) is V11() V12() real M2( REAL )
(([!z,x0,x1!] + [!x3,x0,x1!]) - ([!z,x1,y!] + [!x3,x1,y!])) / (x0 - y) is V11() V12() real M2( REAL )
([!z,x0,x1!] - [!z,x1,y!]) + ([!x3,x0,x1!] - [!x3,x1,y!]) is V11() V12() real M2( REAL )
(([!z,x0,x1!] - [!z,x1,y!]) + ([!x3,x0,x1!] - [!x3,x1,y!])) / (x0 - y) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V11() V12() real M2( REAL )
x3 is V11() V12() real M2( REAL )
x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x0 (#) x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!x4,y,z,x3!] is V11() V12() real M2( REAL )
[!x4,y,z!] is V11() V12() real M2( REAL )
K214(x4,y) is V11() V12() real M2( REAL )
K214(x4,z) is V11() V12() real M2( REAL )
K214(x4,y) - K214(x4,z) is V11() V12() real M2( REAL )
y - z is V11() V12() real set
(K214(x4,y) - K214(x4,z)) / (y - z) is V11() V12() real M2( REAL )
[!x4,z,x3!] is V11() V12() real M2( REAL )
K214(x4,x3) is V11() V12() real M2( REAL )
K214(x4,z) - K214(x4,x3) is V11() V12() real M2( REAL )
z - x3 is V11() V12() real set
(K214(x4,z) - K214(x4,x3)) / (z - x3) is V11() V12() real M2( REAL )
[!x4,y,z!] - [!x4,z,x3!] is V11() V12() real M2( REAL )
y - x3 is V11() V12() real set
([!x4,y,z!] - [!x4,z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
x0 * [!x4,y,z,x3!] is V11() V12() real M2( REAL )
f is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x1 (#) f is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(x0 (#) x4) + (x1 (#) f) is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!((x0 (#) x4) + (x1 (#) f)),y,z,x3!] is V11() V12() real M2( REAL )
[!((x0 (#) x4) + (x1 (#) f)),y,z!] is V11() V12() real M2( REAL )
K214(((x0 (#) x4) + (x1 (#) f)),y) is V11() V12() real M2( REAL )
K214(((x0 (#) x4) + (x1 (#) f)),z) is V11() V12() real M2( REAL )
K214(((x0 (#) x4) + (x1 (#) f)),y) - K214(((x0 (#) x4) + (x1 (#) f)),z) is V11() V12() real M2( REAL )
(K214(((x0 (#) x4) + (x1 (#) f)),y) - K214(((x0 (#) x4) + (x1 (#) f)),z)) / (y - z) is V11() V12() real M2( REAL )
[!((x0 (#) x4) + (x1 (#) f)),z,x3!] is V11() V12() real M2( REAL )
K214(((x0 (#) x4) + (x1 (#) f)),x3) is V11() V12() real M2( REAL )
K214(((x0 (#) x4) + (x1 (#) f)),z) - K214(((x0 (#) x4) + (x1 (#) f)),x3) is V11() V12() real M2( REAL )
(K214(((x0 (#) x4) + (x1 (#) f)),z) - K214(((x0 (#) x4) + (x1 (#) f)),x3)) / (z - x3) is V11() V12() real M2( REAL )
[!((x0 (#) x4) + (x1 (#) f)),y,z!] - [!((x0 (#) x4) + (x1 (#) f)),z,x3!] is V11() V12() real M2( REAL )
([!((x0 (#) x4) + (x1 (#) f)),y,z!] - [!((x0 (#) x4) + (x1 (#) f)),z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!f,y,z,x3!] is V11() V12() real M2( REAL )
[!f,y,z!] is V11() V12() real M2( REAL )
K214(f,y) is V11() V12() real M2( REAL )
K214(f,z) is V11() V12() real M2( REAL )
K214(f,y) - K214(f,z) is V11() V12() real M2( REAL )
(K214(f,y) - K214(f,z)) / (y - z) is V11() V12() real M2( REAL )
[!f,z,x3!] is V11() V12() real M2( REAL )
K214(f,x3) is V11() V12() real M2( REAL )
K214(f,z) - K214(f,x3) is V11() V12() real M2( REAL )
(K214(f,z) - K214(f,x3)) / (z - x3) is V11() V12() real M2( REAL )
[!f,y,z!] - [!f,z,x3!] is V11() V12() real M2( REAL )
([!f,y,z!] - [!f,z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
x1 * [!f,y,z,x3!] is V11() V12() real M2( REAL )
(x0 * [!x4,y,z,x3!]) + (x1 * [!f,y,z,x3!]) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z,x3!] is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z!] is V11() V12() real M2( REAL )
K214((x0 (#) x4),y) is V11() V12() real M2( REAL )
K214((x0 (#) x4),z) is V11() V12() real M2( REAL )
K214((x0 (#) x4),y) - K214((x0 (#) x4),z) is V11() V12() real M2( REAL )
(K214((x0 (#) x4),y) - K214((x0 (#) x4),z)) / (y - z) is V11() V12() real M2( REAL )
[!(x0 (#) x4),z,x3!] is V11() V12() real M2( REAL )
K214((x0 (#) x4),x3) is V11() V12() real M2( REAL )
K214((x0 (#) x4),z) - K214((x0 (#) x4),x3) is V11() V12() real M2( REAL )
(K214((x0 (#) x4),z) - K214((x0 (#) x4),x3)) / (z - x3) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z!] - [!(x0 (#) x4),z,x3!] is V11() V12() real M2( REAL )
([!(x0 (#) x4),y,z!] - [!(x0 (#) x4),z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!(x1 (#) f),y,z,x3!] is V11() V12() real M2( REAL )
[!(x1 (#) f),y,z!] is V11() V12() real M2( REAL )
K214((x1 (#) f),y) is V11() V12() real M2( REAL )
K214((x1 (#) f),z) is V11() V12() real M2( REAL )
K214((x1 (#) f),y) - K214((x1 (#) f),z) is V11() V12() real M2( REAL )
(K214((x1 (#) f),y) - K214((x1 (#) f),z)) / (y - z) is V11() V12() real M2( REAL )
[!(x1 (#) f),z,x3!] is V11() V12() real M2( REAL )
K214((x1 (#) f),x3) is V11() V12() real M2( REAL )
K214((x1 (#) f),z) - K214((x1 (#) f),x3) is V11() V12() real M2( REAL )
(K214((x1 (#) f),z) - K214((x1 (#) f),x3)) / (z - x3) is V11() V12() real M2( REAL )
[!(x1 (#) f),y,z!] - [!(x1 (#) f),z,x3!] is V11() V12() real M2( REAL )
([!(x1 (#) f),y,z!] - [!(x1 (#) f),z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z,x3!] + [!(x1 (#) f),y,z,x3!] is V11() V12() real M2( REAL )
(x0 * [!x4,y,z,x3!]) + [!(x1 (#) f),y,z,x3!] is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V11() V12() real M2( REAL )
x3 is V11() V12() real M2( REAL )
x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x0 (#) x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!(x0 (#) x4),x1,y,z,x3!] is V11() V12() real M2( REAL )
[!(x0 (#) x4),x1,y,z!] is V11() V12() real M2( REAL )
[!(x0 (#) x4),x1,y!] is V11() V12() real M2( REAL )
K214((x0 (#) x4),x1) is V11() V12() real M2( REAL )
K214((x0 (#) x4),y) is V11() V12() real M2( REAL )
K214((x0 (#) x4),x1) - K214((x0 (#) x4),y) is V11() V12() real M2( REAL )
x1 - y is V11() V12() real set
(K214((x0 (#) x4),x1) - K214((x0 (#) x4),y)) / (x1 - y) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z!] is V11() V12() real M2( REAL )
K214((x0 (#) x4),z) is V11() V12() real M2( REAL )
K214((x0 (#) x4),y) - K214((x0 (#) x4),z) is V11() V12() real M2( REAL )
y - z is V11() V12() real set
(K214((x0 (#) x4),y) - K214((x0 (#) x4),z)) / (y - z) is V11() V12() real M2( REAL )
[!(x0 (#) x4),x1,y!] - [!(x0 (#) x4),y,z!] is V11() V12() real M2( REAL )
x1 - z is V11() V12() real set
([!(x0 (#) x4),x1,y!] - [!(x0 (#) x4),y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z,x3!] is V11() V12() real M2( REAL )
[!(x0 (#) x4),z,x3!] is V11() V12() real M2( REAL )
K214((x0 (#) x4),x3) is V11() V12() real M2( REAL )
K214((x0 (#) x4),z) - K214((x0 (#) x4),x3) is V11() V12() real M2( REAL )
z - x3 is V11() V12() real set
(K214((x0 (#) x4),z) - K214((x0 (#) x4),x3)) / (z - x3) is V11() V12() real M2( REAL )
[!(x0 (#) x4),y,z!] - [!(x0 (#) x4),z,x3!] is V11() V12() real M2( REAL )
y - x3 is V11() V12() real set
([!(x0 (#) x4),y,z!] - [!(x0 (#) x4),z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!(x0 (#) x4),x1,y,z!] - [!(x0 (#) x4),y,z,x3!] is V11() V12() real M2( REAL )
x1 - x3 is V11() V12() real set
([!(x0 (#) x4),x1,y,z!] - [!(x0 (#) x4),y,z,x3!]) / (x1 - x3) is V11() V12() real M2( REAL )
[!x4,x1,y,z,x3!] is V11() V12() real M2( REAL )
[!x4,x1,y,z!] is V11() V12() real M2( REAL )
[!x4,x1,y!] is V11() V12() real M2( REAL )
K214(x4,x1) is V11() V12() real M2( REAL )
K214(x4,y) is V11() V12() real M2( REAL )
K214(x4,x1) - K214(x4,y) is V11() V12() real M2( REAL )
(K214(x4,x1) - K214(x4,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!x4,y,z!] is V11() V12() real M2( REAL )
K214(x4,z) is V11() V12() real M2( REAL )
K214(x4,y) - K214(x4,z) is V11() V12() real M2( REAL )
(K214(x4,y) - K214(x4,z)) / (y - z) is V11() V12() real M2( REAL )
[!x4,x1,y!] - [!x4,y,z!] is V11() V12() real M2( REAL )
([!x4,x1,y!] - [!x4,y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!x4,y,z,x3!] is V11() V12() real M2( REAL )
[!x4,z,x3!] is V11() V12() real M2( REAL )
K214(x4,x3) is V11() V12() real M2( REAL )
K214(x4,z) - K214(x4,x3) is V11() V12() real M2( REAL )
(K214(x4,z) - K214(x4,x3)) / (z - x3) is V11() V12() real M2( REAL )
[!x4,y,z!] - [!x4,z,x3!] is V11() V12() real M2( REAL )
([!x4,y,z!] - [!x4,z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!x4,x1,y,z!] - [!x4,y,z,x3!] is V11() V12() real M2( REAL )
([!x4,x1,y,z!] - [!x4,y,z,x3!]) / (x1 - x3) is V11() V12() real M2( REAL )
x0 * [!x4,x1,y,z,x3!] is V11() V12() real M2( REAL )
x0 * [!x4,x1,y,z!] is V11() V12() real M2( REAL )
(x0 * [!x4,x1,y,z!]) - [!(x0 (#) x4),y,z,x3!] is V11() V12() real M2( REAL )
x1 - x3 is V11() V12() real M2( REAL )
((x0 * [!x4,x1,y,z!]) - [!(x0 (#) x4),y,z,x3!]) / (x1 - x3) is V11() V12() real M2( REAL )
x0 * [!x4,y,z,x3!] is V11() V12() real M2( REAL )
(x0 * [!x4,x1,y,z!]) - (x0 * [!x4,y,z,x3!]) is V11() V12() real M2( REAL )
((x0 * [!x4,x1,y,z!]) - (x0 * [!x4,y,z,x3!])) / (x1 - x3) is V11() V12() real M2( REAL )
x0 * ([!x4,x1,y,z!] - [!x4,y,z,x3!]) is V11() V12() real M2( REAL )
(x0 * ([!x4,x1,y,z!] - [!x4,y,z,x3!])) / (x1 - x3) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V11() V12() real M2( REAL )
x3 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!x3,x0,x1,y,z!] is V11() V12() real M2( REAL )
[!x3,x0,x1,y!] is V11() V12() real M2( REAL )
[!x3,x0,x1!] is V11() V12() real M2( REAL )
K214(x3,x0) is V11() V12() real M2( REAL )
K214(x3,x1) is V11() V12() real M2( REAL )
K214(x3,x0) - K214(x3,x1) is V11() V12() real M2( REAL )
x0 - x1 is V11() V12() real set
(K214(x3,x0) - K214(x3,x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!x3,x1,y!] is V11() V12() real M2( REAL )
K214(x3,y) is V11() V12() real M2( REAL )
K214(x3,x1) - K214(x3,y) is V11() V12() real M2( REAL )
x1 - y is V11() V12() real set
(K214(x3,x1) - K214(x3,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!x3,x0,x1!] - [!x3,x1,y!] is V11() V12() real M2( REAL )
x0 - y is V11() V12() real set
([!x3,x0,x1!] - [!x3,x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!x3,x1,y,z!] is V11() V12() real M2( REAL )
[!x3,y,z!] is V11() V12() real M2( REAL )
K214(x3,z) is V11() V12() real M2( REAL )
K214(x3,y) - K214(x3,z) is V11() V12() real M2( REAL )
y - z is V11() V12() real set
(K214(x3,y) - K214(x3,z)) / (y - z) is V11() V12() real M2( REAL )
[!x3,x1,y!] - [!x3,y,z!] is V11() V12() real M2( REAL )
x1 - z is V11() V12() real set
([!x3,x1,y!] - [!x3,y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!x3,x0,x1,y!] - [!x3,x1,y,z!] is V11() V12() real M2( REAL )
x0 - z is V11() V12() real set
([!x3,x0,x1,y!] - [!x3,x1,y,z!]) / (x0 - z) is V11() V12() real M2( REAL )
x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x3 + x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!(x3 + x4),x0,x1,y,z!] is V11() V12() real M2( REAL )
[!(x3 + x4),x0,x1,y!] is V11() V12() real M2( REAL )
[!(x3 + x4),x0,x1!] is V11() V12() real M2( REAL )
K214((x3 + x4),x0) is V11() V12() real M2( REAL )
K214((x3 + x4),x1) is V11() V12() real M2( REAL )
K214((x3 + x4),x0) - K214((x3 + x4),x1) is V11() V12() real M2( REAL )
(K214((x3 + x4),x0) - K214((x3 + x4),x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!(x3 + x4),x1,y!] is V11() V12() real M2( REAL )
K214((x3 + x4),y) is V11() V12() real M2( REAL )
K214((x3 + x4),x1) - K214((x3 + x4),y) is V11() V12() real M2( REAL )
(K214((x3 + x4),x1) - K214((x3 + x4),y)) / (x1 - y) is V11() V12() real M2( REAL )
[!(x3 + x4),x0,x1!] - [!(x3 + x4),x1,y!] is V11() V12() real M2( REAL )
([!(x3 + x4),x0,x1!] - [!(x3 + x4),x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!(x3 + x4),x1,y,z!] is V11() V12() real M2( REAL )
[!(x3 + x4),y,z!] is V11() V12() real M2( REAL )
K214((x3 + x4),z) is V11() V12() real M2( REAL )
K214((x3 + x4),y) - K214((x3 + x4),z) is V11() V12() real M2( REAL )
(K214((x3 + x4),y) - K214((x3 + x4),z)) / (y - z) is V11() V12() real M2( REAL )
[!(x3 + x4),x1,y!] - [!(x3 + x4),y,z!] is V11() V12() real M2( REAL )
([!(x3 + x4),x1,y!] - [!(x3 + x4),y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!(x3 + x4),x0,x1,y!] - [!(x3 + x4),x1,y,z!] is V11() V12() real M2( REAL )
([!(x3 + x4),x0,x1,y!] - [!(x3 + x4),x1,y,z!]) / (x0 - z) is V11() V12() real M2( REAL )
[!x4,x0,x1,y,z!] is V11() V12() real M2( REAL )
[!x4,x0,x1,y!] is V11() V12() real M2( REAL )
[!x4,x0,x1!] is V11() V12() real M2( REAL )
K214(x4,x0) is V11() V12() real M2( REAL )
K214(x4,x1) is V11() V12() real M2( REAL )
K214(x4,x0) - K214(x4,x1) is V11() V12() real M2( REAL )
(K214(x4,x0) - K214(x4,x1)) / (x0 - x1) is V11() V12() real M2( REAL )
[!x4,x1,y!] is V11() V12() real M2( REAL )
K214(x4,y) is V11() V12() real M2( REAL )
K214(x4,x1) - K214(x4,y) is V11() V12() real M2( REAL )
(K214(x4,x1) - K214(x4,y)) / (x1 - y) is V11() V12() real M2( REAL )
[!x4,x0,x1!] - [!x4,x1,y!] is V11() V12() real M2( REAL )
([!x4,x0,x1!] - [!x4,x1,y!]) / (x0 - y) is V11() V12() real M2( REAL )
[!x4,x1,y,z!] is V11() V12() real M2( REAL )
[!x4,y,z!] is V11() V12() real M2( REAL )
K214(x4,z) is V11() V12() real M2( REAL )
K214(x4,y) - K214(x4,z) is V11() V12() real M2( REAL )
(K214(x4,y) - K214(x4,z)) / (y - z) is V11() V12() real M2( REAL )
[!x4,x1,y!] - [!x4,y,z!] is V11() V12() real M2( REAL )
([!x4,x1,y!] - [!x4,y,z!]) / (x1 - z) is V11() V12() real M2( REAL )
[!x4,x0,x1,y!] - [!x4,x1,y,z!] is V11() V12() real M2( REAL )
([!x4,x0,x1,y!] - [!x4,x1,y,z!]) / (x0 - z) is V11() V12() real M2( REAL )
[!x3,x0,x1,y,z!] + [!x4,x0,x1,y,z!] is V11() V12() real M2( REAL )
[!x3,x0,x1,y!] + [!x4,x0,x1,y!] is V11() V12() real M2( REAL )
([!x3,x0,x1,y!] + [!x4,x0,x1,y!]) - [!(x3 + x4),x1,y,z!] is V11() V12() real M2( REAL )
x0 - z is V11() V12() real M2( REAL )
(([!x3,x0,x1,y!] + [!x4,x0,x1,y!]) - [!(x3 + x4),x1,y,z!]) / (x0 - z) is V11() V12() real M2( REAL )
[!x3,x1,y,z!] + [!x4,x1,y,z!] is V11() V12() real M2( REAL )
([!x3,x0,x1,y!] + [!x4,x0,x1,y!]) - ([!x3,x1,y,z!] + [!x4,x1,y,z!]) is V11() V12() real M2( REAL )
(([!x3,x0,x1,y!] + [!x4,x0,x1,y!]) - ([!x3,x1,y,z!] + [!x4,x1,y,z!])) / (x0 - z) is V11() V12() real M2( REAL )
([!x3,x0,x1,y!] - [!x3,x1,y,z!]) + ([!x4,x0,x1,y!] - [!x4,x1,y,z!]) is V11() V12() real M2( REAL )
(([!x3,x0,x1,y!] - [!x3,x1,y,z!]) + ([!x4,x0,x1,y!] - [!x4,x1,y,z!])) / (x0 - z) is V11() V12() real M2( REAL )
x0 is V11() V12() real M2( REAL )
x1 is V11() V12() real M2( REAL )
y is V11() V12() real M2( REAL )
z is V11() V12() real M2( REAL )
x3 is V11() V12() real M2( REAL )
x4 is V11() V12() real M2( REAL )
f is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x0 (#) f is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!f,y,z,x3,x4!] is V11() V12() real M2( REAL )
[!f,y,z,x3!] is V11() V12() real M2( REAL )
[!f,y,z!] is V11() V12() real M2( REAL )
K214(f,y) is V11() V12() real M2( REAL )
K214(f,z) is V11() V12() real M2( REAL )
K214(f,y) - K214(f,z) is V11() V12() real M2( REAL )
y - z is V11() V12() real set
(K214(f,y) - K214(f,z)) / (y - z) is V11() V12() real M2( REAL )
[!f,z,x3!] is V11() V12() real M2( REAL )
K214(f,x3) is V11() V12() real M2( REAL )
K214(f,z) - K214(f,x3) is V11() V12() real M2( REAL )
z - x3 is V11() V12() real set
(K214(f,z) - K214(f,x3)) / (z - x3) is V11() V12() real M2( REAL )
[!f,y,z!] - [!f,z,x3!] is V11() V12() real M2( REAL )
y - x3 is V11() V12() real set
([!f,y,z!] - [!f,z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!f,z,x3,x4!] is V11() V12() real M2( REAL )
[!f,x3,x4!] is V11() V12() real M2( REAL )
K214(f,x4) is V11() V12() real M2( REAL )
K214(f,x3) - K214(f,x4) is V11() V12() real M2( REAL )
x3 - x4 is V11() V12() real set
(K214(f,x3) - K214(f,x4)) / (x3 - x4) is V11() V12() real M2( REAL )
[!f,z,x3!] - [!f,x3,x4!] is V11() V12() real M2( REAL )
z - x4 is V11() V12() real set
([!f,z,x3!] - [!f,x3,x4!]) / (z - x4) is V11() V12() real M2( REAL )
[!f,y,z,x3!] - [!f,z,x3,x4!] is V11() V12() real M2( REAL )
y - x4 is V11() V12() real set
([!f,y,z,x3!] - [!f,z,x3,x4!]) / (y - x4) is V11() V12() real M2( REAL )
x0 * [!f,y,z,x3,x4!] is V11() V12() real M2( REAL )
x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
x1 (#) x4 is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
(x0 (#) f) + (x1 (#) x4) is V1() Relation-like REAL -defined REAL -valued Function-like V26( REAL ) V30( REAL , REAL ) complex-valued ext-real-valued real-valued M2( bool [:REAL,REAL:])
[!((x0 (#) f) + (x1 (#) x4)),y,z,x3,x4!] is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),y,z,x3!] is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),y,z!] is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),y) is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),z) is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),y) - K214(((x0 (#) f) + (x1 (#) x4)),z) is V11() V12() real M2( REAL )
(K214(((x0 (#) f) + (x1 (#) x4)),y) - K214(((x0 (#) f) + (x1 (#) x4)),z)) / (y - z) is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),z,x3!] is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),x3) is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),z) - K214(((x0 (#) f) + (x1 (#) x4)),x3) is V11() V12() real M2( REAL )
(K214(((x0 (#) f) + (x1 (#) x4)),z) - K214(((x0 (#) f) + (x1 (#) x4)),x3)) / (z - x3) is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),y,z!] - [!((x0 (#) f) + (x1 (#) x4)),z,x3!] is V11() V12() real M2( REAL )
([!((x0 (#) f) + (x1 (#) x4)),y,z!] - [!((x0 (#) f) + (x1 (#) x4)),z,x3!]) / (y - x3) is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),z,x3,x4!] is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),x3,x4!] is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),x4) is V11() V12() real M2( REAL )
K214(((x0 (#) f) + (x1 (#) x4)),x3) - K214(((x0 (#) f) + (x1 (#) x4)),x4) is V11() V12() real M2( REAL )
(K214(((x0 (#) f) + (x1 (#) x4)),x3) - K214(((x0 (#) f) + (x1 (#) x4)),x4)) / (x3 - x4) is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),z,x3!] - [!((x0 (#) f) + (x1 (#) x4)),x3,x4!] is V11() V12() real M2( REAL )
([!((x0 (#) f) + (x1 (#) x4)),z,x3!] - [!((x0 (#) f) + (x1 (#) x4)),x3,x4!]) / (z - x4) is V11() V12() real M2( REAL )
[!((x0 (#) f) + (x1 (#) x4)),y,z,x3!] - [!((x0 (#) f) + (x1 (#) x4)),z,x3,x4!] is V11() V12() real M2( REAL )
([!((x0 (#) f) + (x1 (#) x4)),y,z,x3!] - [!((x0 (#) f) + (x1 (#) x4)),z,x3,x4!]) / (y - x4) is V11() V12() real M2( REAL )
[!x4,y,z,x3,x4!] is V11() V12() real M2( REAL )
[!x4,y,z,x3!] is V11() V12() real M2( REAL )
[!x4,y,z!] is V11() V12() real M2( REAL )
K214(x4,y) is V11() V12() real M2( REAL )
K214(x4,z) is V11() V12() real M2( REAL )
K214(x4,y) - K214(x4,z) is V11() V12() real M2( REAL )
(K214(x4,y) - K214(x4,z)) / (y - z) is V11() V12() real M2( REAL )
[!x4,z,x3!] is V11() V12() real M2( REAL )
K214(x4,x3) is V11() V12() real M2( REAL )
K214(x4,z) - K214(x4,x3) is V11() V12() real M2(