:: REAL_1 semantic presentation
begin
registration
cluster
->
real
for ( ( ) ( )
Element
of
REAL
: ( ( ) (
V1
() )
set
) ) ;
end;
definition
mode
Real
is
( ( ) (
V11
()
ext-real
real
)
Element
of
REAL
: ( ( ) (
V1
() )
set
) ) ;
end;
registration
cluster
V11
()
ext-real
positive
real
for ( ( ) ( )
Element
of
REAL
: ( ( ) (
V1
() )
set
) ) ;
end;
definition
let
x
be ( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
-
redefine
func
-
x
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
"
redefine
func
x
"
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
end;
definition
let
x
be ( (
real
) (
V11
()
ext-real
real
)
number
) ;
let
y
be ( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
+
redefine
func
x
+
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
*
redefine
func
x
*
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
-
redefine
func
x
-
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
/
redefine
func
x
/
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
end;
definition
let
x
be ( ( ) (
V11
()
ext-real
real
)
Real
) ;
let
y
be ( (
real
) (
V11
()
ext-real
real
)
number
) ;
:: original:
+
redefine
func
x
+
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
*
redefine
func
x
*
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
-
redefine
func
x
-
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
:: original:
/
redefine
func
x
/
y
->
( ( ) (
V11
()
ext-real
real
)
Real
) ;
end;
theorem
:: REAL_1:1
REAL+
: ( ( ) ( )
set
)
=
{
r
: ( ( ) (
V11
()
ext-real
real
)
Real
) where
r
is ( ( ) (
V11
()
ext-real
real
)
Real
) :
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
ext-real
real
)
Element
of
NAT
: ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
Element
of
bool
REAL
: ( ( ) (
V1
() )
set
) : ( ( ) ( )
set
) ) )
<=
r
: ( ( ) (
V11
()
ext-real
real
)
Real
)
}
;