:: AMISTD_4 semantic presentation

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