:: 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