NAT is non trivial epsilon-transitive epsilon-connected ordinal non empty V28() V33() V34() non with_non-empty_elements non empty-membered Element of bool REAL
REAL is non empty non with_non-empty_elements set
bool REAL is set
NAT is non trivial epsilon-transitive epsilon-connected ordinal non empty V28() V33() V34() non with_non-empty_elements non empty-membered set
bool NAT is V28() set
bool NAT is V28() set
COMPLEX is set
RAT is set
INT is set
{} is set
the trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V28() V33() V35( {} ) set is trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V28() V33() V35( {} ) set
2 is non empty set
ExtREAL is set
1 is non empty set
0 is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
K388(NAT,0) is trivial non empty V35(1) Element of bool NAT
[:NAT,NAT,NAT:] is set
K386(NAT,NAT,NAT,0,0,0) is V22() V23() Element of [:NAT,NAT,NAT:]
[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 [:NAT,NAT,NAT:]
[1,0] is non empty V22() set
[[1,0],0] is non empty V22() set
K389([:NAT,NAT,NAT:],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 [:NAT,NAT,NAT:]
bool [:NAT,NAT,NAT:] is set
0 .--> 0 is trivial Relation-like NAT -defined {0} -defined NAT -valued Function-like one-to-one non empty V35(1) set
{0} is trivial non empty V35(1) set
{0} --> 0 is Relation-like {0} -defined NAT -valued {0} -valued Function-like constant non empty V21({0}) V25({0},{0}) Element of bool [:{0},{0}:]
[:{0},{0}:] is set
bool [:{0},{0}:] 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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
(the_Values_of A) . o is set
I is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
l is Element of Values o
I +* (o,l) is Relation-like Function-like set
dom I is set
o .--> l is trivial Relation-like the carrier of A -defined {o} -defined the carrier of A -defined Values o -valued Values o -valued Function-like one-to-one the_Values_of A -compatible non empty V35(1) set
{o} is trivial non empty V35(1) set
{o} --> l is Relation-like {o} -defined Values o -valued {l} -valued Function-like constant non empty V21({o}) V25({o},{l}) Element of bool [:{o},{l}:]
{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
A is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
o is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
IC (Exec (I,o)) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(Exec (I,o)) . (IC ) is set
l is Element of the carrier of A
Values l is non empty set
(the_Values_of A) . 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))) . (IC ) is set
IC o is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
o . (IC ) is set
succ (IC o) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
IC (N,A,o,l,sICt) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(N,A,o,l,sICt) . (IC ) 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
A is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
o is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
l is Element of the carrier of A
Values l is non empty set
(the_Values_of A) . 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))) . (IC ) 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) . (IC ) is set
IC (Exec (I,o)) is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
(Exec (I,o)) . (IC ) is set
N is non empty non with_non-empty_elements set
N is non empty non with_non-empty_elements set
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard AMI-Struct over N
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
N --> NAT is Relation-like non-empty N -defined {NAT} -valued Function-like constant non empty V21(N) V25(N,{NAT}) Element of bool [:N,{NAT}:]
{NAT} is trivial non empty V35(1) with_non-empty_elements non empty-membered set
[:N,{NAT}:] is set
bool [:N,{NAT}:] is set
0 .--> NAT is trivial Relation-like NAT -defined {0} -defined Function-like one-to-one non empty V35(1) set
{0} --> NAT is Relation-like non-empty {0} -defined {NAT} -valued Function-like constant non empty V21({0}) V25({0},{NAT}) Element of bool [:{0},{NAT}:]
[:{0},{NAT}:] is set
bool [:{0},{NAT}:] is set
(0 .--> NAT) . A is set
N is non empty non with_non-empty_elements set
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard (N) AMI-Struct over N
[1,0,0] is V22() V23() set
[0,0,0] is V22() V23() set
{[1,0,0],[0,0,0]} is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
{[0,0,0],[1,0,0]} is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
N is non empty non with_non-empty_elements set
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard (N) AMI-Struct over N
[0,0,0] is V22() V23() set
[1,0,0] is V22() V23() set
the InstructionsF of (STC N) is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
{[0,0,0],[1,0,0]} is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
N is non empty non with_non-empty_elements set
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard () (N) AMI-Struct over N
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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_Values_of A) . I is set
N is non empty non with_non-empty_elements set
A is with_non-empty_values () AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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
IC is V65(A) Element of the carrier of A
the carrier of A is non empty set
Values (IC ) is non empty set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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_Values_of A) . (IC ) 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
bool the carrier of A is set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
w is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
bool the carrier of A is set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
(the_Values_of A) . 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
(the_Values_of A) . 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
(the_Values_of A) . l is set
sICt is Element of the carrier of A
Values sICt is non empty set
(the_Values_of A) . sICt is set
w is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
Values o is non trivial non empty non empty-membered set
(the_Values_of A) . 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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
l 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
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
(the_Values_of A) . 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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_Values_of A) . o is set
l is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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_Values_of A) . 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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_Values_of A) . 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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 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
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
(the_Values_of A) . o is set
l is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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 {}
bool {} is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard () (N) 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 halting (N) AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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 is non empty non with_non-empty_elements set
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard () (N) 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 standard AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set
IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . (IC ) is set
succ (IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) is epsilon-transitive epsilon-connected ordinal natural non empty V28() V33() set
Values (IC ) is non trivial non empty non empty-membered set
(the_Values_of A) . (IC ) is set
sICt is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
w is Element of Values (IC )
(N,A, the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ,(IC ),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 )) . (IC ) 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 ,(IC ),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 ,(IC ),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 ,(IC ),w))) . (IC ) 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 ,(IC ),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 ,(IC ),w) . (IC ) 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 ,(IC ),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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
IC is V65(A) Element of the carrier of A
(Exec (I,o)) . (IC ) is set
IC o is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
o . (IC ) 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
STC N is non empty V64() with_non-empty_values IC-Ins-separated strict halting with_explicit_jumps IC-relocable standard () (N) 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 standard AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 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 )) . (IC ) is set
IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . (IC ) is set
succ (IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
the carrier of A is non empty set
the_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
o is Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) 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
(Exec (I,o)) . (IC ) is set
IC o is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
o . (IC ) is set
N is non empty non with_non-empty_elements set
A is non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
the InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() 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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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 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 )) . (IC ) is set
IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of NAT
the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set . (IC ) is set
succ (IC the Relation-like the carrier of A -defined Function-like the_Values_of A -compatible V21( the carrier of A) set ) 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 InstructionsF of A is Relation-like non empty standard-ins homogeneous J/A-independent V51() set
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_Values_of A is Relation-like non-empty the carrier of A -defined Function-like V21( the carrier of A) 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
InsCode I is epsilon-transitive epsilon-connected ordinal natural V28() V33() Element of InsCodes the InstructionsF of A
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 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
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
{(IC )} is trivial non empty V35(1) set
{(IC )} \/ (NonZero A) is set