:: XREAL_0 semantic presentation
begin
definition
let
r
be ( ( ) ( )
number
) ;
attr
r
is
real
means
:: XREAL_0:def 1
r
: ( (
ext-real
) (
ext-real
)
set
)
in
REAL
: ( ( ) ( non
empty
)
set
) ;
end;
registration
cluster
->
real
for ( ( ) ( )
Element
of
REAL
: ( ( ) ( non
empty
)
set
) ) ;
end;
registration
cluster
-infty
: ( ( ) ( non
empty
ext-real
non
positive
negative
)
set
)
->
non
real
;
cluster
+infty
: ( ( ) ( non
empty
ext-real
positive
non
negative
)
set
)
->
non
real
;
end;
registration
cluster
natural
->
real
for ( ( ) ( )
set
) ;
cluster
real
->
complex
for ( ( ) ( )
set
) ;
end;
registration
cluster
real
for ( ( ) ( )
set
) ;
cluster
real
->
ext-real
for ( ( ) ( )
set
) ;
end;
registration
let
x
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
-
x
: ( (
real
) (
complex
ext-real
real
)
set
) : ( (
complex
) (
complex
)
set
)
->
complex
real
;
cluster
x
: ( (
real
) (
complex
ext-real
real
)
set
)
"
: ( (
complex
) (
complex
)
set
)
->
complex
real
;
let
y
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
x
: ( (
real
) (
complex
ext-real
real
)
set
)
+
y
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) (
complex
)
set
)
->
real
;
cluster
x
: ( (
real
) (
complex
ext-real
real
)
set
)
*
y
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) (
complex
)
set
)
->
real
;
end;
registration
let
x
,
y
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
x
: ( (
real
) (
complex
ext-real
real
)
set
)
-
y
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) (
complex
)
set
)
->
real
;
cluster
x
: ( (
real
) (
complex
ext-real
real
)
set
)
/
y
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) (
complex
)
set
)
->
real
;
end;
begin
registration
cluster
complex
ext-real
positive
real
for ( ( ) ( )
set
) ;
cluster
complex
ext-real
negative
real
for ( ( ) ( )
set
) ;
cluster
zero
complex
ext-real
real
for ( ( ) ( )
set
) ;
end;
registration
let
r
,
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
+
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
end;
registration
let
r
,
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
+
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
end;
registration
let
r
be ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
number
) ;
let
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
set
)
+
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
negative
real
)
set
)
->
positive
;
cluster
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
+
r
: ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
negative
real
)
set
)
->
positive
;
end;
registration
let
r
be ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
number
) ;
let
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
)
+
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
non
positive
real
)
set
)
->
negative
;
cluster
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
+
r
: ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
positive
real
)
set
)
->
negative
;
end;
registration
let
r
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
-
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( (
complex
) (
complex
ext-real
real
)
set
)
->
complex
non
negative
;
end;
registration
let
r
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
-
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( (
complex
) (
complex
ext-real
real
)
set
)
->
complex
non
positive
;
end;
registration
let
r
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
let
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
-
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
cluster
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
-
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
end;
registration
let
r
be ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
number
) ;
let
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
set
)
-
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
non
negative
real
)
set
)
->
positive
;
cluster
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
-
r
: ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
positive
real
)
set
)
->
negative
;
end;
registration
let
r
be ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
number
) ;
let
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
)
-
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
positive
real
)
set
)
->
negative
;
cluster
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
-
r
: ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
) : ( ( ) (
complex
ext-real
non
negative
real
)
set
)
->
positive
;
end;
registration
let
r
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
let
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
*
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
cluster
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
*
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
end;
registration
let
r
,
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
*
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
end;
registration
let
r
,
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
*
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
end;
registration
let
r
be ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
number
) ;
cluster
r
: ( (
positive
real
) ( non
empty
complex
ext-real
positive
non
negative
real
)
set
)
"
: ( (
complex
) ( non
empty
complex
ext-real
real
)
set
)
->
complex
positive
;
end;
registration
let
r
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
"
: ( (
complex
) (
complex
ext-real
real
)
set
)
->
complex
non
positive
;
end;
registration
let
r
be ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
number
) ;
cluster
r
: ( (
negative
real
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
)
"
: ( (
complex
) ( non
empty
complex
ext-real
non
positive
negative
real
)
set
)
->
complex
negative
;
end;
registration
let
r
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
"
: ( (
complex
) (
complex
ext-real
real
)
set
)
->
complex
non
negative
;
end;
registration
let
r
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
let
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
/
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
cluster
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
/
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
positive
;
end;
registration
let
r
,
s
be ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
number
) ;
cluster
r
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
)
/
s
: ( ( non
negative
real
) (
complex
ext-real
non
negative
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
end;
registration
let
r
,
s
be ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
number
) ;
cluster
r
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
)
/
s
: ( ( non
positive
real
) (
complex
ext-real
non
positive
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
;
end;
begin
registration
let
r
,
s
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
min
(
r
: ( (
real
) (
complex
ext-real
real
)
set
) ,
s
: ( (
real
) (
complex
ext-real
real
)
set
) ) : ( ( ) (
ext-real
)
set
)
->
real
;
cluster
max
(
r
: ( (
real
) (
complex
ext-real
real
)
set
) ,
s
: ( (
real
) (
complex
ext-real
real
)
set
) ) : ( ( ) (
ext-real
)
set
)
->
real
;
end;
definition
let
r
,
s
be ( (
real
) (
complex
ext-real
real
)
number
) ;
func
r
-'
s
->
( ( ) ( )
set
)
equals
:: XREAL_0:def 2
r
: ( ( ) ( )
set
)
-
s
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) ( )
set
)
if
r
: ( ( ) ( )
set
)
-
s
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) ( )
set
)
>=
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
ext-real
non
positive
non
negative
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) )
otherwise
0
: ( ( ) (
empty
epsilon-transitive
epsilon-connected
ordinal
T-Sequence-like
c=-linear
natural
complex
ext-real
non
positive
non
negative
real
)
Element
of
NAT
: ( ( ) ( non
empty
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ) ;
end;
registration
let
r
,
s
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
r
: ( (
real
) (
complex
ext-real
real
)
set
)
-'
s
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) ( )
set
)
->
real
;
end;
registration
let
r
,
s
be ( (
real
) (
complex
ext-real
real
)
number
) ;
cluster
r
: ( (
real
) (
complex
ext-real
real
)
set
)
-'
s
: ( (
real
) (
complex
ext-real
real
)
set
) : ( ( ) (
complex
ext-real
real
)
set
)
->
non
negative
real
for ( (
real
) (
complex
ext-real
real
)
number
) ;
end;