:: AMISTD_4 semantic presentation

REAL is non empty non with_non-empty_elements set

bool NAT is V28() set
bool NAT is V28() set

RAT is set
INT is set
{} is set

2 is non empty set

1 is non empty set

K388(NAT,0) is trivial non empty V35(1) Element of bool NAT
is set
K386(NAT,NAT,NAT,0,0,0) is V22() V23() Element of
[0,0] is non empty V22() set
[[0,0],0] is non empty V22() set
K386(NAT,NAT,NAT,1,0,0) is V22() V23() Element of
[1,0] is non empty V22() set
[[1,0],0] is non empty V22() set
K389(,K386(NAT,NAT,NAT,0,0,0),K386(NAT,NAT,NAT,1,0,0)) is Relation-like non empty standard-ins homogeneous J/A-independent V51() Element of bool

is trivial non empty V35(1) set

N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
the carrier of A is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
o is Element of the carrier of A
Values o is non empty set
() . o is set

l is Element of Values o
I +* (o,l) is Relation-like Function-like set
dom I is set

{o} is trivial non empty V35(1) set

{l} is trivial non empty V35(1) set
[:{o},{l}:] is set
bool [:{o},{l}:] is set
I +* (o .--> l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible non empty V21( the carrier of A) set
N is non empty non with_non-empty_elements set

the carrier of A is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
IC is V65(A) Element of the carrier of A
I is Element of the InstructionsF of A

Exec (I,o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . o is Relation-like Function-like set

(Exec (I,o)) . () is set
l is Element of the carrier of A
Values l is non empty set
() . l is set
sICt is Element of Values l
(N,A,o,l,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,o,l,sICt)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,o,l,sICt) is Relation-like Function-like set
IC (Exec (I,(N,A,o,l,sICt))) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(Exec (I,(N,A,o,l,sICt))) . () is set

o . () is set

IC (N,A,o,l,sICt) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(N,A,o,l,sICt) . () is set
succ (IC (N,A,o,l,sICt)) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
N is non empty non with_non-empty_elements set

the carrier of A is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
IC is V65(A) Element of the carrier of A
I is Element of the InstructionsF of A

Exec (I,o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . o is Relation-like Function-like set
l is Element of the carrier of A
Values l is non empty set
() . l is set
sICt is Element of Values l
(N,A,o,l,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,o,l,sICt)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,o,l,sICt) is Relation-like Function-like set
IC (Exec (I,(N,A,o,l,sICt))) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(Exec (I,(N,A,o,l,sICt))) . () is set
(N,A,(Exec (I,o)),l,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
IC (N,A,(Exec (I,o)),l,sICt) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(N,A,(Exec (I,o)),l,sICt) . () is set

(Exec (I,o)) . () is set
N is non empty non with_non-empty_elements set
N is non empty non with_non-empty_elements set

the carrier of (STC N) is non empty V28() set
A is Element of the carrier of (STC N)
Values A is non empty set
the_Values_of (STC N) is Relation-like non-empty the carrier of (STC N) -defined Function-like V21( the carrier of (STC N)) set
the Object-Kind of (STC N) is Relation-like the carrier of (STC N) -defined N -valued Function-like V25( the carrier of (STC N),N) Element of bool [: the carrier of (STC N),N:]
[: the carrier of (STC N),N:] is set
bool [: the carrier of (STC N),N:] is set
the ValuesF of (STC N) is Relation-like N -defined Function-like V21(N) set
the Object-Kind of (STC N) * the ValuesF of (STC N) is Relation-like set
(the_Values_of (STC N)) . A is set

is set
bool is set

() . A is set
N is non empty non with_non-empty_elements set

[1,0,0] is V22() V23() set
[0,0,0] is V22() V23() set

N is non empty non with_non-empty_elements set

[0,0,0] is V22() V23() set
[1,0,0] is V22() V23() set

N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values (N) AMI-Struct over N
the carrier of A is non empty set
I is Element of the carrier of A
Values I is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
() . I is set
N is non empty non with_non-empty_elements set
A is with_non-empty_values () AMI-Struct over N

N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
IC is V65(A) Element of the carrier of A
the carrier of A is non empty set
Values () is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
() . () is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values AMI-Struct over N

the carrier of A is non empty set
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
I is Element of the InstructionsF of A
o is Element of bool the carrier of A
l is Element of the carrier of A

sICt is Element of the carrier of A
w . sICt is set
Exec (I,w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . w is Relation-like Function-like set
(Exec (I,w)) . sICt is set
o is Element of bool the carrier of A
l is Element of bool the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
I is Element of the InstructionsF of A
o is Element of bool the carrier of A
l is Element of the carrier of A
Values l is non empty set
() . l is set
sICt is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . sICt is Relation-like Function-like set
w is Element of Values l
(N,A,sICt,l,w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,sICt,l,w)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,sICt,l,w) is Relation-like Function-like set
s is Element of the carrier of A
Values s is non empty set
() . s is set
o is Element of bool the carrier of A
l is Element of bool the carrier of A
o is Element of bool the carrier of A
l is Element of the carrier of A
Values l is non empty set
() . l is set
sICt is Element of the carrier of A
Values sICt is non empty set
() . sICt is set

s is Element of Values sICt
(N,A,w,sICt,s) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,w,sICt,s)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,w,sICt,s) is Relation-like Function-like set
Exec (I,w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . w is Relation-like Function-like set
(N,A,(Exec (I,w)),sICt,s) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
sICt is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
w is Element of Values l
(N,A,sICt,l,w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,sICt,l,w)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,sICt,l,w) is Relation-like Function-like set
Exec (I,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . sICt is Relation-like Function-like set
(N,A,(Exec (I,sICt)),l,w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
o is Element of bool the carrier of A
l is Element of bool the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
o is Element of the carrier of A

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

Values o is non trivial non empty non empty-membered set
() . o is set
the Element of Values o is Element of Values o
w is set
s is Element of Values o
(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
dom (N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s) is set
dom the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is set
(N,A,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s),o, the Element of Values o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s),o, the Element of Values o)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s),o, the Element of Values o) is Relation-like Function-like set
(Exec (I,(N,A,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s),o, the Element of Values o))) . o is set
(N,A,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s),o, the Element of Values o) . o is set
Exec (I,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s) is Relation-like Function-like set
(Exec (I,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s))) . o is set
(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,o,s) . o is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
o is Element of the carrier of A

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

l . o is set
Exec (I,l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . l is Relation-like Function-like set
(Exec (I,l)) . o is set
Values o is non empty set
() . o is set
sICt is Element of Values o
(N,A,l,o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,l,o,sICt)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,l,o,sICt) is Relation-like Function-like set
(N,A,(Exec (I,l)),o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
dom (Exec (I,l)) is set
(N,A,(Exec (I,l)),o,sICt) . o is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
o is Element of the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
(N,A,I) \/ (N,A,I) is Element of bool the carrier of A
o is Element of the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
o is Element of the carrier of A
Values o is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
() . o is set

sICt is Element of Values o
(N,A,l,o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,l,o,sICt)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,l,o,sICt) is Relation-like Function-like set
Exec (I,l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . l is Relation-like Function-like set
(N,A,(Exec (I,l)),o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
l . o is set
dom (Exec (I,l)) is set
w is set
(N,A,(Exec (I,l)),o,sICt) . w is set
(Exec (I,l)) . w is set
(Exec (I,l)) . o is set
dom (N,A,(Exec (I,l)),o,sICt) is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
o is Element of the carrier of A
Values o is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
() . o is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
o is Element of the carrier of A
Values o is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
() . o is set
(N,A,I) is Element of bool the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
o is Element of the carrier of A

l . o is set
Exec (I,l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . l is Relation-like Function-like set
(Exec (I,l)) . o is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

Exec (I,o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . o is Relation-like Function-like set
dom o is set
dom (Exec (I,o)) is set
l is set
(Exec (I,o)) . l is set
o . l is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated (N) AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
o is Element of the carrier of A
Values o is non empty set
() . o is set

sICt is Element of Values o
(N,A,l,o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I,(N,A,l,o,sICt)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A,l,o,sICt) is Relation-like Function-like set
Exec (I,l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . l is Relation-like Function-like set
(N,A,(Exec (I,l)),o,sICt) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
{} \ (N,A,I) is Element of bool {}

N is non empty non with_non-empty_elements set

I is halting non sequential Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
(N,A,I) \ (N,A,I) is Element of bool the carrier of A
(N,A,I) is Element of bool the carrier of A
N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated halting (N) AMI-Struct over N

I is halting non sequential Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
the carrier of A is non empty set
bool the carrier of A is set
N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

IC is V65(A) Element of the carrier of A
the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . () is set
succ () is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
Values () is non trivial non empty non empty-membered set
() . () is set

w is Element of Values ()
(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is Relation-like Function-like set
(Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set )) . () is set
Exec (I,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w)) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . (N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w) is Relation-like Function-like set
(Exec (I,(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w))) . () is set
IC (N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w) . () is set
succ (IC (N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(),w)) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
dom the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
I is Element of the InstructionsF of A

Exec (I,o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . o is Relation-like Function-like set
IC is V65(A) Element of the carrier of A
(Exec (I,o)) . () is set

o . () is set
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
N is non empty non with_non-empty_elements set

N is non empty non with_non-empty_elements set

IC is V65(A) Element of the carrier of A
the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is Relation-like Function-like set
(Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set )) . () is set

the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . () is set
succ () is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set
IC is V65(A) Element of the carrier of A
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
(N,A,I) is Element of bool the carrier of A

Exec (I,o) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . o is Relation-like Function-like set
(Exec (I,o)) . () is set

o . () is set
N is non empty non with_non-empty_elements set

IC is V65(A) Element of the carrier of A
the carrier of A is non empty set
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is Relation-like Function-like set
(Exec (I, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set )) . () is set

the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . () is set
succ () is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

the carrier of A is non empty set
IC is V65(A) Element of the carrier of A
I is Element of the InstructionsF of A
(N,A,I) is Element of bool the carrier of A
bool the carrier of A is set
o is Element of the carrier of A

the Object-Kind of A is Relation-like the carrier of A -defined N -valued Function-like V25( the carrier of A,N) Element of bool [: the carrier of A,N:]
[: the carrier of A,N:] is set
bool [: the carrier of A,N:] is set
the ValuesF of A is Relation-like N -defined Function-like V21(N) set
the Object-Kind of A * the ValuesF of A is Relation-like set

InsCodes the InstructionsF of A is non empty set
K48(I) is set
K48(K48(I)) is set
NonZero A is Element of bool the carrier of A

l . o is set
Exec (I,l) is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
K209(( the Object-Kind of A * the ValuesF of A)) is set
K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) is set
the Execution of A is Relation-like the InstructionsF of A -defined K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))) -valued Function-like V25( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))) Element of bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):]
[: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
bool [: the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))):] is set
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) is Element of K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A)))
K80( the InstructionsF of A,K78(K209(( the Object-Kind of A * the ValuesF of A)),K209(( the Object-Kind of A * the ValuesF of A))), the Execution of A,I) . l is Relation-like Function-like set
(Exec (I,l)) . o is set
{()} is trivial non empty V35(1) set
{()} \/ () is set