:: EXTREAL2 semantic presentation

REAL is V1() V30() V38() V39() V40() V44() set
NAT is V38() V39() V40() V41() V42() V43() V44() M2(K6(REAL))
K6(REAL) is set
ExtREAL is V1() V39() set
K7(NAT,ExtREAL) is set
K6(K7(NAT,ExtREAL)) is set
K6(ExtREAL) is set
COMPLEX is V1() V30() V38() V44() set
NAT is V38() V39() V40() V41() V42() V43() V44() set
K6(NAT) is set
RAT is V1() V30() V38() V39() V40() V41() V44() set
INT is V1() V30() V38() V39() V40() V41() V42() V44() set
K6(NAT) is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set
K6(K6(REAL)) is set
K6(RAT) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is set
K7(K7(NAT,NAT),NAT) is set
K6(K7(K7(NAT,NAT),NAT)) is set
0 is V1() V10() V11() V12() ext-real non positive non negative V38() V39() V40() V41() V42() V43() V44() V81() V82() M3( REAL , NAT )
1. is ext-real M2( ExtREAL )
1 is V1() V10() V11() V12() ext-real positive non negative V38() V39() V40() V41() V42() V43() V81() V82() M3( REAL , NAT )
2 is V1() V10() V11() V12() ext-real positive non negative V38() V39() V40() V41() V42() V43() V81() V82() M3( REAL , NAT )
+infty is V1() V12() ext-real positive non negative set
-infty is V1() V12() ext-real non positive negative set
K151(-infty) is V1() ext-real positive non negative set
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is V11() V12() ext-real M2( REAL )
abs y is V11() V12() ext-real M2( REAL )
- x is ext-real M2( ExtREAL )
- y is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- x is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- x is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- x is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- x is ext-real M2( ExtREAL )
- 0 is V1() V11() V12() ext-real non positive non negative V38() V39() V40() V41() V42() V43() V44() M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
x * y is ext-real M2( ExtREAL )
|.(x * y).| is ext-real non negative M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| * |.y.| is ext-real non negative M2( ExtREAL )
- y is ext-real M2( ExtREAL )
- (x * y) is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
(- x) * y is ext-real M2( ExtREAL )
- (x * y) is ext-real M2( ExtREAL )
- y is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
(- x) * (- y) is ext-real M2( ExtREAL )
x * (- y) is ext-real M2( ExtREAL )
- (x * (- y)) is ext-real M2( ExtREAL )
- (x * y) is ext-real M2( ExtREAL )
- (- (x * y)) is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- |.x.| is ext-real non positive M2( ExtREAL )
- x is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
- y is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
- y is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
- y is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
x + y is ext-real M2( ExtREAL )
|.(x + y).| is ext-real non negative M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| + |.y.| is ext-real non negative M2( ExtREAL )
- |.x.| is ext-real non positive M2( ExtREAL )
- |.y.| is ext-real non positive M2( ExtREAL )
(- |.x.|) - |.y.| is ext-real non positive M2( ExtREAL )
K151(|.y.|) is ext-real non positive set
K150((- |.x.|),K151(|.y.|)) is ext-real non positive set
- (|.x.| + |.y.|) is ext-real non positive M2( ExtREAL )
(- |.x.|) + (- |.y.|) is ext-real non positive M2( ExtREAL )
-infty is V1() V12() ext-real non positive negative M2( ExtREAL )
+infty is V1() V12() ext-real positive non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
1. / x is ext-real M2( ExtREAL )
K154(x) is ext-real set
K153(1.,K154(x)) is ext-real set
|.(1. / x).| is ext-real non negative M2( ExtREAL )
|.x.| * |.(1. / x).| is ext-real non negative M2( ExtREAL )
y is V11() V12() ext-real M2( REAL )
1 / y is V11() V12() ext-real M2( REAL )
y * (1 / y) is V11() V12() ext-real M2( REAL )
- x is ext-real M2( ExtREAL )
- y is V11() V12() ext-real M2( REAL )
- (1. / x) is ext-real M2( ExtREAL )
- (1 / y) is V11() V12() ext-real M2( REAL )
(- y) * (- (1 / y)) is V11() V12() ext-real M2( REAL )
y * (1 / y) is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
1. / x is ext-real M2( ExtREAL )
K154(x) is ext-real set
K153(1.,K154(x)) is ext-real set
|.(1. / x).| is ext-real non negative M2( ExtREAL )
|.x.| * |.(1. / x).| is ext-real non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
1. / x is ext-real M2( ExtREAL )
K154(x) is ext-real set
K153(1.,K154(x)) is ext-real set
|.(1. / x).| is ext-real non negative M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
1. / |.x.| is ext-real M2( ExtREAL )
K154(|.x.|) is ext-real non negative set
K153(1.,K154(|.x.|)) is ext-real set
- +infty is V1() ext-real non positive negative M2( ExtREAL )
|.(1. / x).| * |.x.| is ext-real non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
x / y is ext-real M2( ExtREAL )
K154(y) is ext-real set
K153(x,K154(y)) is ext-real set
|.(x / y).| is ext-real non negative M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| / |.y.| is ext-real non negative M2( ExtREAL )
K154(|.y.|) is ext-real non negative set
K153(|.x.|,K154(|.y.|)) is ext-real non negative set
- y is ext-real M2( ExtREAL )
- y is ext-real M2( ExtREAL )
a is V11() V12() ext-real M2( REAL )
abs a is V11() V12() ext-real M2( REAL )
b is V11() V12() ext-real M2( REAL )
abs b is V11() V12() ext-real M2( REAL )
(abs a) / (abs b) is V11() V12() ext-real M2( REAL )
a / b is V11() V12() ext-real M2( REAL )
abs (a / b) is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- x is ext-real M2( ExtREAL )
|.(- x).| is ext-real non negative M2( ExtREAL )
- (- x) is ext-real M2( ExtREAL )
|.+infty.| is ext-real non negative M2( ExtREAL )
|.-infty.| is ext-real non negative M2( ExtREAL )
- -infty is V1() ext-real positive non negative M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| - |.y.| is ext-real M2( ExtREAL )
K151(|.y.|) is ext-real non positive set
K150(|.x.|,K151(|.y.|)) is ext-real set
x - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150(x,K151(y)) is ext-real set
|.(x - y).| is ext-real non negative M2( ExtREAL )
(x - y) + y is ext-real M2( ExtREAL )
|.(x - y).| + |.y.| is ext-real non negative M2( ExtREAL )
a is V11() V12() ext-real M2( REAL )
abs a is V11() V12() ext-real M2( REAL )
b is V11() V12() ext-real M2( REAL )
a - b is V11() V12() ext-real M2( REAL )
abs (a - b) is V11() V12() ext-real M2( REAL )
abs b is V11() V12() ext-real M2( REAL )
(abs a) - (abs b) is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
x - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150(x,K151(y)) is ext-real set
|.(x - y).| is ext-real non negative M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| + |.y.| is ext-real non negative M2( ExtREAL )
a is V11() V12() ext-real M2( REAL )
abs a is V11() V12() ext-real M2( REAL )
b is V11() V12() ext-real M2( REAL )
abs b is V11() V12() ext-real M2( REAL )
(abs a) + (abs b) is V11() V12() ext-real M2( REAL )
a - b is V11() V12() ext-real M2( REAL )
abs (a - b) is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
a is ext-real M2( ExtREAL )
|.a.| is ext-real non negative M2( ExtREAL )
x + a is ext-real M2( ExtREAL )
|.(x + a).| is ext-real non negative M2( ExtREAL )
b is ext-real M2( ExtREAL )
y + b is ext-real M2( ExtREAL )
- y is ext-real M2( ExtREAL )
- b is ext-real M2( ExtREAL )
(- y) + (- b) is ext-real M2( ExtREAL )
(- y) - b is ext-real M2( ExtREAL )
K151(b) is ext-real set
K150((- y),K151(b)) is ext-real set
- (y + b) is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| - |.y.| is ext-real M2( ExtREAL )
K151(|.y.|) is ext-real non positive set
K150(|.x.|,K151(|.y.|)) is ext-real set
|.(|.x.| - |.y.|).| is ext-real non negative M2( ExtREAL )
x - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150(x,K151(y)) is ext-real set
|.(x - y).| is ext-real non negative M2( ExtREAL )
|.y.| - |.x.| is ext-real M2( ExtREAL )
K151(|.x.|) is ext-real non positive set
K150(|.y.|,K151(|.x.|)) is ext-real set
- (|.x.| - |.y.|) is ext-real M2( ExtREAL )
y - x is ext-real M2( ExtREAL )
K151(x) is ext-real set
K150(y,K151(x)) is ext-real set
- (x - y) is ext-real M2( ExtREAL )
|.(y - x).| is ext-real non negative M2( ExtREAL )
- |.(x - y).| is ext-real non positive M2( ExtREAL )
- (- (|.x.| - |.y.|)) is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
y is ext-real M2( ExtREAL )
x * y is ext-real M2( ExtREAL )
x + y is ext-real M2( ExtREAL )
|.(x + y).| is ext-real non negative M2( ExtREAL )
|.y.| is ext-real non negative M2( ExtREAL )
|.x.| + |.y.| is ext-real non negative M2( ExtREAL )
- (x + y) is ext-real M2( ExtREAL )
- x is ext-real M2( ExtREAL )
(- x) - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150((- x),K151(y)) is ext-real set
R_EAL 2 is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
min (x,y) is ext-real set
x + y is ext-real M2( ExtREAL )
x - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150(x,K151(y)) is ext-real set
|.(x - y).| is ext-real non negative M2( ExtREAL )
(x + y) - |.(x - y).| is ext-real M2( ExtREAL )
K151(|.(x - y).|) is ext-real non positive set
K150((x + y),K151(|.(x - y).|)) is ext-real set
((x + y) - |.(x - y).|) / (R_EAL 2) is ext-real M2( ExtREAL )
K154((R_EAL 2)) is ext-real set
K153(((x + y) - |.(x - y).|),K154((R_EAL 2))) is ext-real set
a is V11() V12() ext-real M2( REAL )
b is V11() V12() ext-real M2( REAL )
a - b is V11() V12() ext-real M2( REAL )
a + b is V11() V12() ext-real M2( REAL )
abs (a - b) is V11() V12() ext-real M2( REAL )
(a + b) - (abs (a - b)) is V11() V12() ext-real M2( REAL )
((a + b) - (abs (a - b))) / 2 is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
max (x,y) is ext-real set
x + y is ext-real M2( ExtREAL )
x - y is ext-real M2( ExtREAL )
K151(y) is ext-real set
K150(x,K151(y)) is ext-real set
|.(x - y).| is ext-real non negative M2( ExtREAL )
(x + y) + |.(x - y).| is ext-real M2( ExtREAL )
((x + y) + |.(x - y).|) / (R_EAL 2) is ext-real M2( ExtREAL )
K154((R_EAL 2)) is ext-real set
K153(((x + y) + |.(x - y).|),K154((R_EAL 2))) is ext-real set
a is V11() V12() ext-real M2( REAL )
b is V11() V12() ext-real M2( REAL )
a - b is V11() V12() ext-real M2( REAL )
a + b is V11() V12() ext-real M2( REAL )
abs (a - b) is V11() V12() ext-real M2( REAL )
(a + b) + (abs (a - b)) is V11() V12() ext-real M2( REAL )
((a + b) + (abs (a - b))) / 2 is V11() V12() ext-real M2( REAL )
x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
max (x,y) is ext-real set
min (x,y) is ext-real set
x is ext-real M2( ExtREAL )
y is ext-real M2( ExtREAL )
(x,y) is ext-real M2( ExtREAL )
(x,y) is ext-real M2( ExtREAL )
(x,y) + (x,y) is ext-real M2( ExtREAL )
x + y is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )
- |.x.| is ext-real non positive M2( ExtREAL )
- x is ext-real M2( ExtREAL )
- (- x) is ext-real M2( ExtREAL )
x is ext-real M2( ExtREAL )
|.x.| is ext-real non negative M2( ExtREAL )