:: SCMFSA_7 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

SCM+FSA is V42() V82(3) IC-Ins-separated strict V90(3) AMI-Struct over 3

3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

the U1 of SCM+FSA is set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

K6(NAT) is set

K6(NAT) is set

9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

K102(9) is Element of K6(NAT)

Int-Locations is set

K180() is set

K6(K180()) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

K7(K180(),2) is Relation-like set

K6(K7(K180(),2)) is set

K182() is Relation-like Function-like V38(K180(),2) Element of K6(K7(K180(),2))

K183() is non empty Relation-like 2 -defined Function-like total set

K182() * K183() is Relation-like Function-like set

K156((K182() * K183())) is set

K174() is non empty set

K128(K156((K182() * K183())),K156((K182() * K183()))) is set

K7(K174(),K128(K156((K182() * K183())),K156((K182() * K183())))) is Relation-like set

K6(K7(K174(),K128(K156((K182() * K183())),K156((K182() * K183()))))) is set

K304() is V42() V82(2) IC-Ins-separated strict strict V90(2) AMI-Struct over 2

the InstructionsF of K304() is non empty Relation-like V71() V72() V73() V75() set

the U1 of K304() is set

K268(2,K304()) is Relation-like non-empty the U1 of K304() -defined Function-like total set

the Object-Kind of K304() is Relation-like Function-like V38( the U1 of K304(),2) Element of K6(K7( the U1 of K304(),2))

K7( the U1 of K304(),2) is Relation-like set

K6(K7( the U1 of K304(),2)) is set

the U7 of K304() is non empty Relation-like 2 -defined Function-like total set

the Object-Kind of K304() * the U7 of K304() is Relation-like Function-like set

K6( the U1 of SCM+FSA) is set

the InstructionsF of SCM+FSA is non empty Relation-like V71() V72() V73() V75() set

INT is set

COMPLEX is set

RAT is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

K268(3,SCM+FSA) is Relation-like non-empty the U1 of SCM+FSA -defined Function-like total set

the Object-Kind of SCM+FSA is Relation-like Function-like V38( the U1 of SCM+FSA,3) Element of K6(K7( the U1 of SCM+FSA,3))

K7( the U1 of SCM+FSA,3) is Relation-like set

K6(K7( the U1 of SCM+FSA,3)) is set

the U7 of SCM+FSA is non empty Relation-like 3 -defined Function-like total set

the Object-Kind of SCM+FSA * the U7 of SCM+FSA is Relation-like Function-like set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered integer V70() Function-yielding V94() ext-real non positive non negative V137() Element of NAT

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered integer V70() Function-yielding V94() ext-real non positive non negative V137() set

IC is Element of the U1 of SCM+FSA

{{}} is non empty functional set

P is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ D is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

((P ^ D) ^ V) ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

V ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ (V ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(D ^ V) ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ ((D ^ V) ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ (V ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (D ^ (V ^ I)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (D ^ V) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ (D ^ V)) ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ D is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

((P ^ D) ^ V) ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(((P ^ D) ^ V) ^ I) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

I ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

((P ^ D) ^ V) ^ (I ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

V ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(V ^ I) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ ((V ^ I) ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

V ^ (I ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ (V ^ (I ^ O)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ V is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(D ^ V) ^ I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

((D ^ V) ^ I) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (((D ^ V) ^ I) ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(D ^ V) ^ (I ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ ((D ^ V) ^ (I ^ O)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ ((V ^ I) ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (D ^ ((V ^ I) ^ O)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ (V ^ (I ^ O)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (D ^ (V ^ (I ^ O))) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ D) ^ (V ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

((P ^ D) ^ (V ^ I)) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ ((D ^ V) ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ ((D ^ V) ^ I)) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D ^ (V ^ I) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ (D ^ (V ^ I)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(P ^ (D ^ (V ^ I))) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(D ^ (V ^ I)) ^ O is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

P ^ ((D ^ (V ^ I)) ^ O) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

D is V11() V12() integer ext-real set

P is V62() Element of the U1 of SCM+FSA

intloc 0 is V62() Element of the U1 of SCM+FSA

K313(0) is V62() Element of the U1 of K304()

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} is non empty functional set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

AddTo (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

halt SCM+FSA is Element of the InstructionsF of SCM+FSA

<%(halt SCM+FSA)%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (halt SCM+FSA) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (halt SCM+FSA) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(halt SCM+FSA)}) Element of K6(K7({0},{(halt SCM+FSA)}))

{(halt SCM+FSA)} is non empty set

K7({0},{(halt SCM+FSA)}) is Relation-like set

K6(K7({0},{(halt SCM+FSA)})) is set

SubFrom (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

D - 1 is V11() V12() integer ext-real set

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(V,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (V --> (AddTo (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

O is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

V + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

1 - D is V11() V12() integer ext-real set

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(SubFrom (P,(intloc 0)))} is non empty set

K7(V,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (V --> (SubFrom (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

O is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

V + D is V11() V12() integer ext-real set

O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

O + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

V is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

O --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like O -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(O, the InstructionsF of SCM+FSA) V70() Element of K6(K7(O, the InstructionsF of SCM+FSA))

K7(O, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(O, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(O,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (O --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (O --> (AddTo (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

s --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like s -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(s, the InstructionsF of SCM+FSA) V70() Element of K6(K7(s, the InstructionsF of SCM+FSA))

K7(s, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(s, the InstructionsF of SCM+FSA)) is set

K7(s,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (s --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (s --> (AddTo (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q + D is V11() V12() integer ext-real set

f is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

q --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like q -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(q, the InstructionsF of SCM+FSA) V70() Element of K6(K7(q, the InstructionsF of SCM+FSA))

K7(q, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(q, the InstructionsF of SCM+FSA)) is set

{(SubFrom (P,(intloc 0)))} is non empty set

K7(q,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (q --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (q --> (SubFrom (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q0 + D is V11() V12() integer ext-real set

p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

q0 --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like q0 -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(q0, the InstructionsF of SCM+FSA) V70() Element of K6(K7(q0, the InstructionsF of SCM+FSA))

K7(q0, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(q0, the InstructionsF of SCM+FSA)) is set

K7(q0,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (q0 --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (q0 --> (SubFrom (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

D is V11() V12() integer ext-real set

P is V62() Element of the U1 of SCM+FSA

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

AddTo (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

D - 1 is V11() V12() integer ext-real set

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(V,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

V + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

1 - D is V11() V12() integer ext-real set

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(SubFrom (P,(intloc 0)))} is non empty set

K7(V,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

V + D is V11() V12() integer ext-real set

O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

O + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

V is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

O --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like O -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(O, the InstructionsF of SCM+FSA) V70() Element of K6(K7(O, the InstructionsF of SCM+FSA))

K7(O, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(O, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(O,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (O --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

I is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

s --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like s -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(s, the InstructionsF of SCM+FSA) V70() Element of K6(K7(s, the InstructionsF of SCM+FSA))

K7(s, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(s, the InstructionsF of SCM+FSA)) is set

K7(s,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (s --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q + D is V11() V12() integer ext-real set

f is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like q -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(q, the InstructionsF of SCM+FSA) V70() Element of K6(K7(q, the InstructionsF of SCM+FSA))

K7(q, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(q, the InstructionsF of SCM+FSA)) is set

{(SubFrom (P,(intloc 0)))} is non empty set

K7(q,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (q --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q0 + D is V11() V12() integer ext-real set

p is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q0 --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like q0 -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(q0, the InstructionsF of SCM+FSA) V70() Element of K6(K7(q0, the InstructionsF of SCM+FSA))

K7(q0, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(q0, the InstructionsF of SCM+FSA)) is set

K7(q0,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (q0 --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P is V62() Element of the U1 of SCM+FSA

D is V11() V12() integer ext-real set

(P,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

(P,D) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(P,D) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

AddTo (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

V --> (AddTo (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(V,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (V --> (AddTo (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

SubFrom (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V + D is V11() V12() integer ext-real set

V --> (SubFrom (P,(intloc 0))) is T-Sequence-like Relation-like V -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(V, the InstructionsF of SCM+FSA) V70() Element of K6(K7(V, the InstructionsF of SCM+FSA))

K7(V, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(V, the InstructionsF of SCM+FSA)) is set

{(SubFrom (P,(intloc 0)))} is non empty set

K7(V,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (V --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (V --> (SubFrom (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

the InstructionsF of SCM+FSA ^omega is non empty functional set

D is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

len D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

intloc 1 is V62() Element of the U1 of SCM+FSA

K313(1) is V62() Element of the U1 of K304()

intloc 2 is V62() Element of the U1 of SCM+FSA

K313(2) is V62() Element of the U1 of K304()

P is FinSeq-Location

(P,(intloc 1)) := (intloc 2) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

10 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

<*(intloc 2),P,(intloc 1)*> is non empty Relation-like NAT -defined Function-like finite V33(3) FinSequence-like FinSubsequence-like set

<*(intloc 2)*> is non empty Relation-like NAT -defined Function-like finite V33(1) FinSequence-like FinSubsequence-like set

[1,(intloc 2)] is set

{[1,(intloc 2)]} is non empty Relation-like Function-like set

<*P*> is non empty Relation-like NAT -defined Function-like finite V33(1) FinSequence-like FinSubsequence-like set

[1,P] is set

{[1,P]} is non empty Relation-like Function-like set

<*(intloc 2)*> ^ <*P*> is non empty Relation-like NAT -defined Function-like finite V33(1 + 1) FinSequence-like FinSubsequence-like set

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

<*(intloc 1)*> is non empty Relation-like NAT -defined Function-like finite V33(1) FinSequence-like FinSubsequence-like set

[1,(intloc 1)] is set

{[1,(intloc 1)]} is non empty Relation-like Function-like set

(<*(intloc 2)*> ^ <*P*>) ^ <*(intloc 1)*> is non empty Relation-like NAT -defined Function-like finite V33((1 + 1) + 1) FinSequence-like FinSubsequence-like set

(1 + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

K55(10,{},<*(intloc 2),P,(intloc 1)*>) is set

<%((P,(intloc 1)) := (intloc 2))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> ((P,(intloc 1)) := (intloc 2)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> ((P,(intloc 1)) := (intloc 2)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{((P,(intloc 1)) := (intloc 2))}) Element of K6(K7({0},{((P,(intloc 1)) := (intloc 2))}))

{((P,(intloc 1)) := (intloc 2))} is non empty set

K7({0},{((P,(intloc 1)) := (intloc 2))}) is Relation-like set

K6(K7({0},{((P,(intloc 1)) := (intloc 2))})) is set

I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set

D . (I + 1) is set

((intloc 1),(I + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

I + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

dom D is Element of K6(NAT)

D . (I + 1) is set

((intloc 1),(I + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

O is V11() V12() integer ext-real set

((intloc 2),O) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(I + 1)) ^ ((intloc 2),O) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(I + 1)) ^ ((intloc 2),O)) ^ <%((P,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

s is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

I is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set

dom I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)

FlattenSeq I is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

O is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

len I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom I is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

dom D is Element of K6(NAT)

D . (s + 1) is set

f is V11() V12() integer ext-real set

p is V11() V12() integer ext-real set

I . s is Relation-like Function-like set

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set

D . (s + 1) is set

((intloc 1),(s + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(s + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 2),p) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(s + 1)) ^ ((intloc 2),p) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(s + 1)) ^ ((intloc 2),p)) ^ <%((P,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q is V11() V12() integer ext-real set

((intloc 2),q) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(s + 1)) ^ ((intloc 2),q) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(s + 1)) ^ ((intloc 2),q)) ^ <%((P,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

I is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

O is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

s is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set

len s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

FlattenSeq s is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

s is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set

len s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

FlattenSeq s is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

f is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

FlattenSeq f is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

f is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set

len f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

FlattenSeq f is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

s . p is Relation-like Function-like set

f . p is Relation-like Function-like set

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

D . (p + 1) is set

((intloc 1),(p + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q is V11() V12() integer ext-real set

((intloc 2),q) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(p + 1)) ^ ((intloc 2),q) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(p + 1)) ^ ((intloc 2),q)) ^ <%((P,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

q0 is V11() V12() integer ext-real set

((intloc 2),q0) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((intloc 1),(p + 1)) ^ ((intloc 2),q0) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(p + 1)) ^ ((intloc 2),q0)) ^ <%((P,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

D is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

len D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

((intloc 1),(len D)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P is FinSeq-Location

P :=<0,...,0> (intloc 1) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

12 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

<*(intloc 1),P*> is non empty Relation-like NAT -defined Function-like finite V33(2) FinSequence-like FinSubsequence-like set

<*P*> is non empty Relation-like NAT -defined Function-like finite V33(1) FinSequence-like FinSubsequence-like set

[1,P] is set

{[1,P]} is non empty Relation-like Function-like set

<*(intloc 1)*> ^ <*P*> is non empty Relation-like NAT -defined Function-like finite V33(1 + 1) FinSequence-like FinSubsequence-like set

K55(12,{},<*(intloc 1),P*>) is set

<%(P :=<0,...,0> (intloc 1))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P :=<0,...,0> (intloc 1)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P :=<0,...,0> (intloc 1))}) Element of K6(K7({0},{(P :=<0,...,0> (intloc 1))}))

{(P :=<0,...,0> (intloc 1))} is non empty set

K7({0},{(P :=<0,...,0> (intloc 1))}) is Relation-like set

K6(K7({0},{(P :=<0,...,0> (intloc 1))})) is set

((intloc 1),(len D)) ^ <%(P :=<0,...,0> (intloc 1))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(P,D) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(((intloc 1),(len D)) ^ <%(P :=<0,...,0> (intloc 1))%>) ^ (P,D) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

((((intloc 1),(len D)) ^ <%(P :=<0,...,0> (intloc 1))%>) ^ (P,D)) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P is V62() Element of the U1 of SCM+FSA

(P,1) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

<%(P := (intloc 0))%> ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

<%(P := (intloc 0))%> ^ {} is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

(<%(P := (intloc 0))%> ^ {}) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set

AddTo (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

0 --> (AddTo (P,(intloc 0))) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined 0 -defined NAT -defined {} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered total total V38( 0 , the InstructionsF of SCM+FSA) integer V70() Function-yielding V94() ext-real non positive non negative V137() Element of K6(K7(0, the InstructionsF of SCM+FSA))

K7(0, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(0, the InstructionsF of SCM+FSA)) is set

{(AddTo (P,(intloc 0)))} is non empty set

K7(0,{(AddTo (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (0 --> (AddTo (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (0 --> (AddTo (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P is V62() Element of the U1 of SCM+FSA

(P,0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set

P := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(P := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (P := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (P := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(P := (intloc 0))}) Element of K6(K7({0},{(P := (intloc 0))}))

{(P := (intloc 0))} is non empty set

K7({0},{(P := (intloc 0))}) is Relation-like set

K6(K7({0},{(P := (intloc 0))})) is set

SubFrom (P,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(SubFrom (P,(intloc 0)))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (SubFrom (P,(intloc 0))) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (SubFrom (P,(intloc 0))) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(SubFrom (P,(intloc 0)))}) Element of K6(K7({0},{(SubFrom (P,(intloc 0)))}))

{(SubFrom (P,(intloc 0)))} is non empty set

K7({0},{(SubFrom (P,(intloc 0)))}) is Relation-like set

K6(K7({0},{(SubFrom (P,(intloc 0)))})) is set

<%(P := (intloc 0))%> ^ <%(SubFrom (P,(intloc 0)))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ <%(SubFrom (P,(intloc 0)))%>) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

1 --> (SubFrom (P,(intloc 0))) is non empty T-Sequence-like Relation-like 1 -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(1, the InstructionsF of SCM+FSA) V70() Element of K6(K7(1, the InstructionsF of SCM+FSA))

K7(1, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(1, the InstructionsF of SCM+FSA)) is set

K7(1,{(SubFrom (P,(intloc 0)))}) is Relation-like set

<%(P := (intloc 0))%> ^ (1 --> (SubFrom (P,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

(<%(P := (intloc 0))%> ^ (1 --> (SubFrom (P,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total D -started set

V . (intloc 0) is V11() V12() integer ext-real set

IC V is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

V . (IC ) is set

I is V62() Element of the U1 of SCM+FSA

O is V11() V12() integer ext-real set

(I,O) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

dom (I,O) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)

len (I,O) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (I,O) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

Comput (P,V,(len (I,O))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

(Comput (P,V,(len (I,O)))) . I is V11() V12() integer ext-real set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(I,s) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

I := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(I := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (I := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (I := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(I := (intloc 0))}) Element of K6(K7({0},{(I := (intloc 0))}))

{(I := (intloc 0))} is non empty set

K7({0},{(I := (intloc 0))}) is Relation-like set

K6(K7({0},{(I := (intloc 0))})) is set

AddTo (I,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

f --> (AddTo (I,(intloc 0))) is T-Sequence-like Relation-like f -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(f, the InstructionsF of SCM+FSA) V70() Element of K6(K7(f, the InstructionsF of SCM+FSA))

K7(f, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(f, the InstructionsF of SCM+FSA)) is set

{(AddTo (I,(intloc 0)))} is non empty set

K7(f,{(AddTo (I,(intloc 0)))}) is Relation-like set

<%(I := (intloc 0))%> ^ (f --> (AddTo (I,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set

len (I,s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (I,s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

len <%(I := (intloc 0))%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom <%(I := (intloc 0))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set

len (f --> (AddTo (I,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

dom (f --> (AddTo (I,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set

(len <%(I := (intloc 0))%>) + (len (f --> (AddTo (I,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

1 + (len (f --> (AddTo (I,(intloc 0))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

dom (I,s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

D + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P . (D + 0) is Element of the InstructionsF of SCM+FSA

(I,s) . 0 is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput (P,V,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

CurInstr (P,(Comput (P,V,p))) is Element of the InstructionsF of SCM+FSA

IC (Comput (P,V,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . (IC ) is set

P /. (IC (Comput (P,V,p))) is Element of the InstructionsF of SCM+FSA

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

Comput (P,V,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

Following (P,(Comput (P,V,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

Exec ((CurInstr (P,(Comput (P,V,p)))),(Comput (P,V,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set

the Execution of SCM+FSA is Relation-like Function-like V38( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K6(K7( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K7( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K6(K7( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,V,p))))) is Element of K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,V,p))))) . (Comput (P,V,p)) is set

Exec ((I := (intloc 0)),V) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(I := (intloc 0))) is Element of K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(I := (intloc 0))) . V is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

p - 1 is V11() V12() integer ext-real set

q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

(I,s) . p is set

(f --> (AddTo (I,(intloc 0)))) . (p - 1) is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

D + p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

P . (D + p) is Element of the InstructionsF of SCM+FSA

(I,s) . p is set

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput (P,V,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

IC (Comput (P,V,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . (IC ) is set

D + p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . I is V11() V12() integer ext-real set

p + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

Comput (P,V,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

IC (Comput (P,V,(p + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,(p + 1))) . (IC ) is set

D + (p + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

(Comput (P,V,(p + 1))) . I is V11() V12() integer ext-real set

(Exec ((I := (intloc 0)),V)) . (IC ) is set

succ (D + p) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set

(D + p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

(Exec ((I := (intloc 0)),V)) . I is V11() V12() integer ext-real set

q is V62() Element of the U1 of SCM+FSA

(Comput (P,V,(p + 1))) . q is V11() V12() integer ext-real set

(Exec ((I := (intloc 0)),V)) . q is V11() V12() integer ext-real set

V . q is V11() V12() integer ext-real set

q is FinSeq-Location

(Comput (P,V,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

V . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Exec ((I := (intloc 0)),V)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

p + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

CurInstr (P,(Comput (P,V,p))) is Element of the InstructionsF of SCM+FSA

P /. (IC (Comput (P,V,p))) is Element of the InstructionsF of SCM+FSA

P . (D + p) is Element of the InstructionsF of SCM+FSA

Following (P,(Comput (P,V,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

Exec ((CurInstr (P,(Comput (P,V,p)))),(Comput (P,V,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,V,p))))) is Element of K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,V,p))))) . (Comput (P,V,p)) is set

Exec ((AddTo (I,(intloc 0))),(Comput (P,V,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(AddTo (I,(intloc 0)))) is Element of K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K130( the InstructionsF of SCM+FSA,K128(K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K156(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(AddTo (I,(intloc 0)))) . (Comput (P,V,p)) is set

succ (IC (Comput (P,V,p))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set

(D + p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

(Comput (P,V,p)) . (intloc 0) is V11() V12() integer ext-real set

p + ((Comput (P,V,p)) . (intloc 0)) is V11() V12() integer ext-real set

q is V62() Element of the U1 of SCM+FSA

(Comput (P,V,(p + 1))) . q is V11() V12() integer ext-real set

(Comput (P,V,p)) . q is V11() V12() integer ext-real set

V . q is V11() V12() integer ext-real set

q is FinSeq-Location

(Comput (P,V,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

V . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P,V,p)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

Comput (P,V,0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

IC (Comput (P,V,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,0)) . (IC ) is set

(Comput (P,V,0)) . I is V11() V12() integer ext-real set

p is V62() Element of the U1 of SCM+FSA

(Comput (P,V,0)) . p is V11() V12() integer ext-real set

V . p is V11() V12() integer ext-real set

q is FinSeq-Location

(Comput (P,V,0)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

V . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput (P,V,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

IC (Comput (P,V,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . (IC ) is set

D + p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . I is V11() V12() integer ext-real set

q is V62() Element of the U1 of SCM+FSA

(Comput (P,V,p)) . q is V11() V12() integer ext-real set

V . q is V11() V12() integer ext-real set

q0 is FinSeq-Location

(Comput (P,V,p)) . q0 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

V . q0 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

Comput (P,V,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set

IC (Comput (P,V,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

(Comput (P,V,p)) . (IC ) is set

D + p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

q is V62() Element of the U1 of SCM+FSA

(Comput (P,V,p)) . q is V11() V12() integer ext-real set

V . q is V11() V12() integer ext-real set

q0 is FinSeq-Location

(Comput (P,V,p)) . q0 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

V . q0 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

- O is V11() V12() integer ext-real set

s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

(s + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT

I := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<%(I := (intloc 0))%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V33(1) V70() set

0 .--> (I := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set

{0} --> (I := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(I := (intloc 0))}) Element of K6(K7({0},{(I := (intloc 0))}))

{(I := (intloc 0))} is non empty set

K7({0},{(I := (intloc 0))}) is Relation-like set

K6(K7({0},{(I := (intloc 0))})) is set

SubFrom (I,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

f is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT

f + O is V11() V12() integer ext-real set

f --> (SubFrom (I,(intloc 0))) is T-Sequence-like Relation-like f -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like constant finite total V38(f, the InstructionsF of SCM+FSA) V70() Element of K6(K7(f, the InstructionsF of SCM+FSA))

K7(f, the InstructionsF of SCM+FSA) is Relation-like set

K6(K7(f, the InstructionsF of SCM+FSA)) is set

{(SubFrom (I,(intloc 0)))} is non empty set

K7(f,{(SubFrom (I,(intloc 0)))}) is Relation-like set

<%(I := (intloc 0))%> ^ (f --> (SubFrom (I,(intloc 0)))) is T-Sequence-like Relation-like