:: AMISTD_4 semantic presentation
begin
definition
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
s
be ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) ;
let
o
be ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ;
let
a
be ( ( ) ( )
Element
of
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;
:: original:
+*
redefine
func
s
+*
(
o
,
a
)
->
( (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
the_Values_of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( ) ( )
AMI-Struct
over
N
: ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) )
State
of ( ( ) ( )
set
) ) ;
end;
theorem
:: AMISTD_4:1
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
s
being ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
for
w
being ( ( ) ( )
Element
of
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
sequential
&
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
<>
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
IC
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) )
=
IC
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
(
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
w
: ( ( ) ( )
Element
of
Values
b
5
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) ) ;
theorem
:: AMISTD_4:2
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
s
being ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
for
w
being ( ( ) ( )
Element
of
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
sequential
&
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
<>
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) holds
IC
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
(
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
w
: ( ( ) ( )
Element
of
Values
b
5
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) )
=
IC
(
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
w
: ( ( ) ( )
Element
of
Values
b
5
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) ) ;
begin
definition
let
A
be ( ( ) ( )
COM-Struct
) ;
attr
A
is
with_non_trivial_Instructions
means
:: AMISTD_4:def 1
not the
InstructionsF
of
A
: ( ( ) ( )
set
) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) is
trivial
;
end;
definition
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
attr
A
is
with_non_trivial_ObjectKinds
means
:: AMISTD_4:def 2
for
o
being ( ( ) ( )
Object
of ( ( ) ( )
set
) ) holds not
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) is
trivial
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
STC
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) : ( (
strict
) ( non
empty
V64
()
with_non-empty_values
IC-Ins-separated
strict
halting
with_explicit_jumps
IC-relocable
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
->
strict
with_non_trivial_ObjectKinds
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
with_explicit_jumps
IC-relocable
standard
with_non_trivial_Instructions
with_non_trivial_ObjectKinds
for ( ( ) ( )
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
STC
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) : ( (
strict
) ( non
empty
V64
()
with_non-empty_values
IC-Ins-separated
strict
halting
with_explicit_jumps
IC-relocable
standard
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
->
strict
with_non_trivial_Instructions
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_Instructions
with_non_trivial_ObjectKinds
for ( ( ) ( )
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
o
be ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ;
cluster
Values
o
: ( ( ) ( )
Element
of the
carrier
of
A
: ( ( non
empty
with_non-empty_values
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
)
->
non
trivial
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( (
with_non-empty_values
with_non_trivial_Instructions
) (
with_non-empty_values
with_non_trivial_Instructions
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
cluster
the
InstructionsF
of
A
: ( (
with_non-empty_values
with_non_trivial_Instructions
) (
with_non-empty_values
with_non_trivial_Instructions
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
)
->
non
trivial
standard-ins
homogeneous
J/A-independent
V51
() ;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
cluster
Values
(
IC
)
: ( ( ) (
V65
(
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
)
->
non
trivial
;
end;
definition
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
I
be ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ;
func
Output
I
->
( ( ) ( )
Subset
of )
means
:: AMISTD_4:def 3
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) holds
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
it
: ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) iff ex
s
being ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) st
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
.
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
<>
(
Exec
(
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
) ,
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
) ( non
empty
with_non-empty_values
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
.
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) );
end;
definition
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
I
be ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ;
func
Out_\_Inp
I
->
( ( ) ( )
Subset
of )
means
:: AMISTD_4:def 4
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) holds
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
it
: ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) iff for
s
being ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
for
a
being ( ( ) ( )
Element
of
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
Exec
(
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
) ,
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
=
Exec
(
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
) ,
(
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
a
: ( ( ) ( )
Element
of
Values
b
1
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
) );
func
Out_U_Inp
I
->
( ( ) ( )
Subset
of )
means
:: AMISTD_4:def 5
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) holds
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
it
: ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) iff ex
s
being ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) ex
a
being ( ( ) ( )
Element
of
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) st
Exec
(
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
) ,
(
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) )
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
a
: ( ( ) ( )
Element
of
Values
b
1
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
<>
(
Exec
(
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
) ,
s
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
+*
(
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) ,
a
: ( ( ) ( )
Element
of
Values
b
1
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) );
end;
definition
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
I
be ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ;
func
Input
I
->
( ( ) ( )
Subset
of )
equals
:: AMISTD_4:def 6
(
Out_U_Inp
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
)
)
: ( ( ) ( )
Subset
of )
\
(
Out_\_Inp
I
: ( (
natural
) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
set
)
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
Mem-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ;
end;
theorem
:: AMISTD_4:3
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) holds
Out_\_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
c=
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:4
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) holds
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
c=
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:5
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) holds
Out_\_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
=
(
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
)
: ( ( ) ( )
Subset
of )
\
(
Input
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ;
theorem
:: AMISTD_4:6
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) holds
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
=
(
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
)
: ( ( ) ( )
Subset
of )
\/
(
Input
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) : ( ( ) ( )
set
) ) ;
theorem
:: AMISTD_4:7
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) st
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) is
trivial
holds
not
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:8
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) st
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) is
trivial
holds
not
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
Input
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:9
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) st
Values
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( non
empty
)
set
) is
trivial
holds
not
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:10
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) holds
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
halting
iff
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) is
empty
) ;
theorem
:: AMISTD_4:11
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
halting
holds
Out_\_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) is
empty
;
theorem
:: AMISTD_4:12
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
halting
holds
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) is
empty
;
theorem
:: AMISTD_4:13
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
halting
holds
Input
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) is
empty
;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
I
be ( (
halting
) (
halting
non
sequential
)
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ;
cluster
Input
I
: ( (
halting
) (
halting
non
sequential
)
Element
of the
InstructionsF
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
->
empty
;
cluster
Output
I
: ( (
halting
) (
halting
non
sequential
)
Element
of the
InstructionsF
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
->
empty
;
cluster
Out_U_Inp
I
: ( (
halting
) (
halting
non
sequential
)
Element
of the
InstructionsF
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
->
empty
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
halting
with_non_trivial_ObjectKinds
for ( ( ) ( )
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
let
A
be ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
let
I
be ( (
halting
) (
halting
non
sequential
)
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ;
cluster
Out_\_Inp
I
: ( (
halting
) (
halting
non
sequential
)
Element
of the
InstructionsF
of
A
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
halting
with_non_trivial_ObjectKinds
) ( non
empty
with_non-empty_values
IC-Ins-separated
halting
with_non_trivial_ObjectKinds
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of )
->
empty
;
end;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
with_non_trivial_Instructions
for ( ( ) ( )
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
end;
theorem
:: AMISTD_4:14
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
sequential
holds
not
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Out_\_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:15
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st ex
s
being ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) st
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
.
(
IC
)
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
<>
IC
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) ) holds
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
registration
let
N
be ( (
with_zero
) ( non
empty
with_zero
)
set
) ;
cluster
non
empty
with_non-empty_values
IC-Ins-separated
standard
for ( ( ) ( )
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ;
end;
theorem
:: AMISTD_4:16
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
sequential
holds
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:17
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st ex
s
being ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) st
(
Exec
(
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) ,
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) )
)
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
.
(
IC
)
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
<>
IC
s
: ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
the_Values_of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( (
Relation-like
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ) (
Relation-like
non-empty
the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
)
-defined
Function-like
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
set
)
-compatible
V21
( the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) )
State
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V28
()
V33
() )
Element
of
NAT
: ( ( ) ( non
trivial
epsilon-transitive
epsilon-connected
ordinal
non
empty
V28
()
V33
()
V34
() non
with_non-empty_elements
non
empty-membered
)
Element
of
bool
REAL
: ( ( ) ( non
empty
non
with_non-empty_elements
)
set
) : ( ( ) ( )
set
) ) ) holds
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:18
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
sequential
holds
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
standard
) ( non
empty
with_non-empty_values
IC-Ins-separated
standard
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) )
in
Out_U_Inp
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: AMISTD_4:19
for
N
being ( (
with_zero
) ( non
empty
with_zero
)
set
)
for
A
being ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
N
: ( (
with_zero
) ( non
empty
with_zero
)
set
) )
for
I
being ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) )
for
o
being ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) ) st
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) is
jump-only
&
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
in
Output
I
: ( ( ) ( )
Instruction
of ( (
standard-ins
homogeneous
J/A-independent
V51
() ) (
Relation-like
non
empty
standard-ins
homogeneous
J/A-independent
V51
() )
set
) ) : ( ( ) ( )
Subset
of ) holds
o
: ( ( ) ( )
Object
of ( ( ) ( non
empty
)
set
) )
=
IC
: ( ( ) (
V65
(
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) ) )
Element
of the
carrier
of
b
2
: ( ( non
empty
with_non-empty_values
IC-Ins-separated
) ( non
empty
with_non-empty_values
IC-Ins-separated
)
AMI-Struct
over
b
1
: ( (
with_zero
) ( non
empty
with_zero
)
set
) ) : ( ( ) ( non
empty
)
set
) ) ;