:: SCMPDS_9 semantic presentation
begin
definition
let
la
,
lb
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
a
,
b
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
:: original:
-->
redefine
func
(
la
,
lb
)
-->
(
a
,
b
)
->
( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
)
PartState
of 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ;
end;
registration
let
k
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
goto
k
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
theorem
:: SCMPDS_9:1
for
i
being ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) )
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) st ( for
s
being ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
State
of ( ( ) ( )
set
) ) st
IC
s
: ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
State
of ( ( ) ( )
set
) ) : ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
=
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
Exec
(
i
: ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
s
: ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
State
of ( ( ) ( )
set
) ) )
)
: ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
.
(
IC
)
: ( ( ) ( )
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
succ
(
IC
s
: ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
Relation-like
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ) (
Relation-like
non-empty
the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
)
-defined
Function-like
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V25
( the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) )
State
of ( ( ) ( )
set
) )
)
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) holds
NIC
(
i
: ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:2
for
i
being ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) st ( for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
NIC
(
i
: ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ) holds
JUMP
i
: ( ( ) ( )
Instruction
of ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) ) is
empty
;
theorem
:: SCMPDS_9:3
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
goto
k
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
abs
(
k
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
+
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
: ( ( ) ( non
empty
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
set
) ;
theorem
:: SCMPDS_9:4
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
NIC
(
(
return
a
: ( (
Int-like
) (
Int-like
)
Int_position
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
k
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) where
k
is ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) :
k
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
>
1 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
;
theorem
:: SCMPDS_9:5
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
saveIC
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:6
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
)
:=
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:7
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
:=
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:8
for
a
,
b
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
:=
(
b
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:9
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
AddTo
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:10
for
a
,
b
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
AddTo
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ,
b
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:11
for
a
,
b
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
SubFrom
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ,
b
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:12
for
a
,
b
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
MultBy
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ,
b
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:13
for
a
,
b
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
Divide
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ,
b
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:14
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
<>0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
) ,
(
abs
(
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
+
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:15
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
<=0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
) ,
(
abs
(
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
+
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:16
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
)
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
for
k1
,
k2
being ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) holds
NIC
(
(
(
a
: ( (
Int-like
) (
Int-like
)
Int_position
) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) )
>=0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) ,
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
(
succ
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) ( )
set
) ,
(
abs
(
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
)
+
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
: ( ( ) ( non
empty
)
set
) ;
theorem
:: SCMPDS_9:17
for
a
being ( (
Int-like
) (
Int-like
)
Int_position
) holds
JUMP
(
return
a
: ( (
Int-like
) (
Int-like
)
Int_position
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
{
k
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) where
k
is ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) :
k
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
>
1 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) )
}
;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
cluster
JUMP
(
return
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
infinite
;
end;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
saveIC
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) )
:=
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
,
k2
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
:=
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
,
b
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
,
k2
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
:=
(
b
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
,
k2
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
AddTo
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
,
b
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
,
k2
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
AddTo
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) ,
b
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
cluster
JUMP
(
SubFrom
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) ,
b
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
cluster
JUMP
(
MultBy
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) ,
b
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
cluster
JUMP
(
Divide
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) ,
b
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
registration
let
a
be ( (
Int-like
) (
Int-like
)
Int_position
) ;
let
k1
,
k2
be ( (
integer
) (
V11
()
real
integer
ext-real
)
Integer
) ;
cluster
JUMP
(
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
<>0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
cluster
JUMP
(
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
<=0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
cluster
JUMP
(
(
a
: ( (
Int-like
) (
Int-like
)
Element
of the
U1
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( ( ) ( )
set
) ) ,
k1
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
) )
>=0_goto
k2
: ( (
integer
) (
V11
()
real
integer
ext-real
)
set
)
)
: ( ( ) ( )
Element
of the
InstructionsF
of
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) : ( (
V72
()
V73
()
V74
()
V76
() ) (
V72
()
V73
()
V74
()
V76
() )
set
) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
->
empty
;
end;
theorem
:: SCMPDS_9:18
for
l
being ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
SUCC
(
l
: ( ( ) (
ordinal
natural
V11
()
real
integer
ext-real
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ,
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ) : ( ( ) (
countable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
K6
(
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
) )
=
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ;
registration
cluster
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) )
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) )
->
strict
non
InsLoc-antisymmetric
;
end;
registration
cluster
SCMPDS
: ( (
strict
) (
V50
()
with_non-empty_values
IC-Ins-separated
strict
V91
(2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) ) non
InsLoc-antisymmetric
)
AMI-Struct
over 2 : ( ( ) ( non
empty
ordinal
natural
V11
()
real
integer
non
with_non-empty_elements
ext-real
positive
non
negative
V110
()
V121
()
V122
()
V123
()
V124
()
V125
()
V126
() )
Element
of
NAT
: ( ( ) ( non
finite
countable
denumerable
V121
()
V122
()
V123
()
V124
()
V125
()
V126
()
V127
() )
Element
of
K6
(
REAL
: ( ( ) (
V121
()
V122
()
V123
()
V127
() )
set
) ) : ( ( ) ( )
set
) ) ) )
->
strict
non
weakly_standard
;
end;