:: 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 NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() 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 --> (SubFrom (I,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (f --> (SubFrom (I,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len <%(I := (intloc 0))%>) + (len (f --> (SubFrom (I,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
1 + (len (f --> (SubFrom (I,(intloc 0))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of 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,O) . 0 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
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,(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
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
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
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((s + 1) + 1) - 1 is V11() V12() integer ext-real set
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
(I,O) . p is set
(f --> (SubFrom (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,O) . 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 is V11() V12() integer ext-real non positive set
(- p) + 1 is V11() V12() integer ext-real set
((- p) + 1) + 1 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
- (p + 1) is V11() V12() integer ext-real non positive set
(- (p + 1)) + 1 is V11() V12() integer ext-real set
((- (p + 1)) + 1) + 1 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 ((SubFrom (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,(SubFrom (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,(SubFrom (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) + 1) + 1) - ((Comput (P,V,p)) . (intloc 0)) is V11() V12() integer ext-real set
(((- p) + 1) + 1) - (V . (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
- 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() set
(- 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
((- 0) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative 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
- p is V11() V12() integer ext-real non positive set
(- p) + 1 is V11() V12() integer ext-real set
((- p) + 1) + 1 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
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
(- O) + (1 + 1) is V11() V12() integer ext-real set
- ((- O) + (1 + 1)) is V11() V12() integer ext-real set
(- ((- O) + (1 + 1))) + 1 is V11() V12() integer ext-real set
((- ((- O) + (1 + 1))) + 1) + 1 is V11() V12() integer ext-real set
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total 0 -started set
D . (intloc 0) is V11() V12() integer ext-real set
V is V62() Element of the U1 of SCM+FSA
I is V11() V12() integer ext-real set
(V,I) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
len (V,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (V,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,D,(len (V,I))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,(len (V,I)))) . V is V11() V12() integer ext-real set
dom (V,I) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(V,I) . O is set
0 + O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P . (0 + O) is Element of the InstructionsF of SCM+FSA
O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,O) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,O)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,O)) . (IC ) is set
0 + O is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s is V62() Element of the U1 of SCM+FSA
(Comput (P,D,O)) . s is V11() V12() integer ext-real set
D . s is V11() V12() integer ext-real set
f is FinSeq-Location
(Comput (P,D,O)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total 0 -started set
D . (intloc 0) is V11() V12() integer ext-real set
Result (P,D) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
D . (IC ) is set
V is V62() Element of the U1 of SCM+FSA
(Result (P,D)) . V is V11() V12() integer ext-real set
I is V11() V12() integer ext-real set
(V,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
V := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<%(V := (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 .--> (V := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set
{0} --> (V := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(V := (intloc 0))}) Element of K6(K7({0},{(V := (intloc 0))}))
{(V := (intloc 0))} is non empty set
K7({0},{(V := (intloc 0))}) is Relation-like set
K6(K7({0},{(V := (intloc 0))})) is set
AddTo (V,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
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
O --> (AddTo (V,(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 (V,(intloc 0)))} is non empty set
K7(O,{(AddTo (V,(intloc 0)))}) is Relation-like set
<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
len (<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%(V := (intloc 0))%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(V := (intloc 0))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
len (O --> (AddTo (V,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (O --> (AddTo (V,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len <%(V := (intloc 0))%>) + (len (O --> (AddTo (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
1 + (len (O --> (AddTo (V,(intloc 0))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 is set
(O --> (AddTo (V,(intloc 0)))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
<%(V := (intloc 0))%> ^ ((O --> (AddTo (V,(intloc 0)))) ^ <%(halt SCM+FSA)%>) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(<%(V := (intloc 0))%> ^ ((O --> (AddTo (V,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 is set
len ((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%(halt SCM+FSA)%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(halt SCM+FSA)%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
(len (<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) 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
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) 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
P . p is Element of the InstructionsF of SCM+FSA
((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
P . 0 is Element of the InstructionsF of SCM+FSA
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
P /. (IC (Comput (P,D,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,D,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Following (P,(Comput (P,D,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,p)))),(Comput (P,D,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,D,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,D,p))))) . (Comput (P,D,p)) is set
Exec ((V := (intloc 0)),D) 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,(V := (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,(V := (intloc 0))) . D 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
s - 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
dom (<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
(<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) . p is set
(O --> (AddTo (V,(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
P . p is Element of the InstructionsF of SCM+FSA
((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,q) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,q)) . (IC ) is set
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
Comput (P,D,(q + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,(q + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,(q + 1))) . (IC ) is set
(Exec ((V := (intloc 0)),D)) . (IC ) is set
succ q is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
q + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
CurInstr (P,(Comput (P,D,q))) is Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,D,q))) is Element of the InstructionsF of SCM+FSA
P . q is Element of the InstructionsF of SCM+FSA
Following (P,(Comput (P,D,q))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,q)))),(Comput (P,D,q))) 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,D,q))))) 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,D,q))))) . (Comput (P,D,q)) is set
Exec ((AddTo (V,(intloc 0))),(Comput (P,D,q))) 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 (V,(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 (V,(intloc 0)))) . (Comput (P,D,q)) is set
succ (IC (Comput (P,D,q))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
Comput (P,D,0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,0)) . (IC ) is set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,p)) . V 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,D,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,(p + 1))) . V is V11() V12() integer ext-real set
(Exec ((V := (intloc 0)),D)) . V is V11() V12() integer ext-real set
q is V62() Element of the U1 of SCM+FSA
(Comput (P,D,(p + 1))) . q is V11() V12() integer ext-real set
(Exec ((V := (intloc 0)),D)) . q is V11() V12() integer ext-real set
D . q is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((V := (intloc 0)),D)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
P /. (IC (Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
p + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
CurInstr (P,(Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
P . p is Element of the InstructionsF of SCM+FSA
Following (P,(Comput (P,D,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,p)))),(Comput (P,D,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,D,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,D,p))))) . (Comput (P,D,p)) is set
Exec ((AddTo (V,(intloc 0))),(Comput (P,D,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 (V,(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 (V,(intloc 0)))) . (Comput (P,D,p)) is set
(Comput (P,D,p)) . (intloc 0) is V11() V12() integer ext-real set
p + ((Comput (P,D,p)) . (intloc 0)) is V11() V12() integer ext-real set
q is V62() Element of the U1 of SCM+FSA
(Comput (P,D,(p + 1))) . q is V11() V12() integer ext-real set
(Comput (P,D,p)) . q is V11() V12() integer ext-real set
D . q is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,D,p)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s + (len <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((<%(V := (intloc 0))%> ^ (O --> (AddTo (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . s is set
s - s is V11() V12() integer ext-real set
<%(halt SCM+FSA)%> . (s - s) is set
Comput (P,D,0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,0)) . V is V11() V12() integer ext-real set
p is V62() Element of the U1 of SCM+FSA
(Comput (P,D,0)) . p is V11() V12() integer ext-real set
D . p is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,0)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Comput (P,D,s) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,s)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,s)) . (IC ) is set
P /. (IC (Comput (P,D,s))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,D,s))) is Element of the InstructionsF of SCM+FSA
CurInstr (P,(Comput (P,D,s))) is Element of the InstructionsF of SCM+FSA
P . s is Element of the InstructionsF of SCM+FSA
p is V62() Element of the U1 of SCM+FSA
(Result (P,D)) . p is V11() V12() integer ext-real set
D . p is V11() V12() integer ext-real set
q is FinSeq-Location
(Result (P,D)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
- I 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
(O + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
V := (intloc 0) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<%(V := (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 .--> (V := (intloc 0)) is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one set
{0} --> (V := (intloc 0)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(V := (intloc 0))}) Element of K6(K7({0},{(V := (intloc 0))}))
{(V := (intloc 0))} is non empty set
K7({0},{(V := (intloc 0))}) is Relation-like set
K6(K7({0},{(V := (intloc 0))})) is set
SubFrom (V,(intloc 0)) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s + I is V11() V12() integer ext-real set
s --> (SubFrom (V,(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
{(SubFrom (V,(intloc 0)))} is non empty set
K7(s,{(SubFrom (V,(intloc 0)))}) is Relation-like set
<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
len (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%(V := (intloc 0))%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(V := (intloc 0))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
len (s --> (SubFrom (V,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s --> (SubFrom (V,(intloc 0)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len <%(V := (intloc 0))%>) + (len (s --> (SubFrom (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
1 + (len (s --> (SubFrom (V,(intloc 0))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . 0 is set
(s --> (SubFrom (V,(intloc 0)))) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
<%(V := (intloc 0))%> ^ ((s --> (SubFrom (V,(intloc 0)))) ^ <%(halt SCM+FSA)%>) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(<%(V := (intloc 0))%> ^ ((s --> (SubFrom (V,(intloc 0)))) ^ <%(halt SCM+FSA)%>)) . 0 is set
len ((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%(halt SCM+FSA)%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(halt SCM+FSA)%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
(len (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0)))))) + (len <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((O + 1) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) 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
P . p is Element of the InstructionsF of SCM+FSA
((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
P . 0 is Element of the InstructionsF of SCM+FSA
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
CurInstr (P,(Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
P /. (IC (Comput (P,D,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,D,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Following (P,(Comput (P,D,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,p)))),(Comput (P,D,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,D,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,D,p))))) . (Comput (P,D,p)) is set
Exec ((V := (intloc 0)),D) 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,(V := (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,(V := (intloc 0))) . D 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
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 V11() V12() integer ext-real set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
(<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) . p is set
(s --> (SubFrom (V,(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
P . p is Element of the InstructionsF of SCM+FSA
((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . p is set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
q is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,q) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,q)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,q)) . (IC ) is set
q + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
Comput (P,D,(q + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,(q + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,(q + 1))) . (IC ) is set
(Exec ((V := (intloc 0)),D)) . (IC ) is set
succ q is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
q + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
CurInstr (P,(Comput (P,D,q))) is Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,D,q))) is Element of the InstructionsF of SCM+FSA
P . q is Element of the InstructionsF of SCM+FSA
Following (P,(Comput (P,D,q))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,q)))),(Comput (P,D,q))) 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,D,q))))) 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,D,q))))) . (Comput (P,D,q)) is set
Exec ((SubFrom (V,(intloc 0))),(Comput (P,D,q))) 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,(SubFrom (V,(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,(SubFrom (V,(intloc 0)))) . (Comput (P,D,q)) is set
succ (IC (Comput (P,D,q))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
Comput (P,D,0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,0)) . (IC ) is set
p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,D,p) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,p)) . V is V11() V12() integer ext-real set
- p is V11() V12() integer ext-real non positive set
(- p) + 1 is V11() V12() integer ext-real set
((- p) + 1) + 1 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,D,(p + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,(p + 1))) . V is V11() V12() integer ext-real set
- (p + 1) is V11() V12() integer ext-real non positive set
(- (p + 1)) + 1 is V11() V12() integer ext-real set
((- (p + 1)) + 1) + 1 is V11() V12() integer ext-real set
(Exec ((V := (intloc 0)),D)) . V is V11() V12() integer ext-real set
q is V62() Element of the U1 of SCM+FSA
(Comput (P,D,(p + 1))) . q is V11() V12() integer ext-real set
(Exec ((V := (intloc 0)),D)) . q is V11() V12() integer ext-real set
D . q is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((V := (intloc 0)),D)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
IC (Comput (P,D,p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,p)) . (IC ) is set
P /. (IC (Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
p + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
CurInstr (P,(Comput (P,D,p))) is Element of the InstructionsF of SCM+FSA
P . p is Element of the InstructionsF of SCM+FSA
Following (P,(Comput (P,D,p))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,D,p)))),(Comput (P,D,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,D,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,D,p))))) . (Comput (P,D,p)) is set
Exec ((SubFrom (V,(intloc 0))),(Comput (P,D,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,(SubFrom (V,(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,(SubFrom (V,(intloc 0)))) . (Comput (P,D,p)) is set
(Comput (P,D,p)) . (intloc 0) is V11() V12() integer ext-real set
(((- p) + 1) + 1) - ((Comput (P,D,p)) . (intloc 0)) is V11() V12() integer ext-real set
(((- p) + 1) + 1) - (D . (intloc 0)) is V11() V12() integer ext-real set
q is V62() Element of the U1 of SCM+FSA
(Comput (P,D,(p + 1))) . q is V11() V12() integer ext-real set
(Comput (P,D,p)) . q is V11() V12() integer ext-real set
D . q is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,(p + 1))) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,D,p)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))) ^ <%(halt SCM+FSA)%>) . ((O + 1) + 1) is set
((O + 1) + 1) - (len (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0)))))) is V11() V12() integer ext-real set
<%(halt SCM+FSA)%> . (((O + 1) + 1) - (len (<%(V := (intloc 0))%> ^ (s --> (SubFrom (V,(intloc 0))))))) is set
Comput (P,D,((O + 1) + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,D,((O + 1) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,D,((O + 1) + 1))) . (IC ) is set
P /. (IC (Comput (P,D,((O + 1) + 1)))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,D,((O + 1) + 1)))) is Element of the InstructionsF of SCM+FSA
CurInstr (P,(Comput (P,D,((O + 1) + 1)))) is Element of the InstructionsF of SCM+FSA
P . ((O + 1) + 1) is Element of the InstructionsF of SCM+FSA
Comput (P,D,0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,D,0)) . V is V11() V12() integer ext-real 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() set
(- 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
((- 0) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
p is V62() Element of the U1 of SCM+FSA
(Comput (P,D,0)) . p is V11() V12() integer ext-real set
D . p is V11() V12() integer ext-real set
q is FinSeq-Location
(Comput (P,D,0)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
- ((O + 1) + 1) is V11() V12() integer ext-real non positive set
(- ((O + 1) + 1)) + 1 is V11() V12() integer ext-real set
((- ((O + 1) + 1)) + 1) + 1 is V11() V12() integer ext-real set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
O + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
p is V62() Element of the U1 of SCM+FSA
(Result (P,D)) . p is V11() V12() integer ext-real set
D . p is V11() V12() integer ext-real set
q is FinSeq-Location
(Result (P,D)) . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
D . q is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total 0 -started set
s . (intloc 0) is V11() V12() integer ext-real set
Result (P,s) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
f is FinSeq-Location
(Result (P,s)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(f,p) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
len p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((intloc 1),(len p)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
f :=<0,...,0> (intloc 1) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*(intloc 1),f*> is non empty Relation-like NAT -defined Function-like finite V33(2) FinSequence-like FinSubsequence-like set
<*f*> is non empty Relation-like NAT -defined Function-like finite V33(1) FinSequence-like FinSubsequence-like set
[1,f] is set
{[1,f]} is non empty Relation-like Function-like set
<*(intloc 1)*> ^ <*f*> is non empty Relation-like NAT -defined Function-like finite V33(1 + 1) FinSequence-like FinSubsequence-like set
K55(12,{},<*(intloc 1),f*>) is set
<%(f :=<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 .--> (f :=<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} --> (f :=<0,...,0> (intloc 1)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{(f :=<0,...,0> (intloc 1))}) Element of K6(K7({0},{(f :=<0,...,0> (intloc 1))}))
{(f :=<0,...,0> (intloc 1))} is non empty set
K7({0},{(f :=<0,...,0> (intloc 1))}) is Relation-like set
K6(K7({0},{(f :=<0,...,0> (intloc 1))})) is set
((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(f,p) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
q0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
P . q0 is Element of the InstructionsF of SCM+FSA
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . q0 is set
(f,(intloc 1)) := (intloc 2) is V76( the InstructionsF of SCM+FSA) V89(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*(intloc 2),f,(intloc 1)*> is non empty Relation-like NAT -defined Function-like finite V33(3) FinSequence-like FinSubsequence-like set
<*(intloc 2)*> ^ <*f*> is non empty Relation-like NAT -defined Function-like finite V33(1 + 1) FinSequence-like FinSubsequence-like set
(<*(intloc 2)*> ^ <*f*>) ^ <*(intloc 1)*> is non empty Relation-like NAT -defined Function-like finite V33((1 + 1) + 1) FinSequence-like FinSubsequence-like set
K55(10,{},<*(intloc 2),f,(intloc 1)*>) is set
<%((f,(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 .--> ((f,(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} --> ((f,(intloc 1)) := (intloc 2)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V38({0},{((f,(intloc 1)) := (intloc 2))}) Element of K6(K7({0},{((f,(intloc 1)) := (intloc 2))}))
{((f,(intloc 1)) := (intloc 2))} is non empty set
K7({0},{((f,(intloc 1)) := (intloc 2))}) is Relation-like set
K6(K7({0},{((f,(intloc 1)) := (intloc 2))})) is set
pp is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
len pp is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
FlattenSeq pp is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len <%(halt SCM+FSA)%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(halt SCM+FSA)%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
k is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
pp0 is set
<%pp0%> is non empty T-Sequence-like Relation-like NAT -defined Function-like finite V33(1) V70() set
0 .--> pp0 is non empty Relation-like NAT -defined {0} -defined Function-like one-to-one set
{0} --> pp0 is non empty Relation-like {0} -defined Function-like constant total V38({0},{pp0}) Element of K6(K7({0},{pp0}))
{pp0} is non empty set
K7({0},{pp0}) is Relation-like set
K6(K7({0},{pp0})) is set
k ^ <%pp0%> is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom k is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%pp0%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%pp0%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
len (k ^ <%pp0%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (k ^ <%pp0%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
dom (k ^ <%pp0%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
dom pp is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
p . ((len k) + 1) is set
pp . (len k) is Relation-like Function-like set
((intloc 1),((len k) + 1)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
g is V11() V12() integer ext-real set
((intloc 2),g) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
((intloc 1),((len k) + 1)) ^ ((intloc 2),g) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) ^ <%((f,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
Seg (len pp) is finite V33( len pp) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp ) } is set
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg (len pp0) is finite V33( len pp0) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp0 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
p | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
len ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg (len pp0) is finite V33( len pp0) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp0 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
p | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
len ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(k ^ <%pp0%>) . (len k) is set
pp0 ^ <%pp0%> is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
pp1 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
FlattenSeq pp1 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len pp1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (len pp1) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg (len pp1) is finite V33( len pp1) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp1 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1)) is Relation-like NAT -defined Seg (len pp1) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
p | (len pp1) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p | (Seg (len pp1)) is Relation-like NAT -defined Seg (len pp1) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
len ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
x is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
<%x%> is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V33(1) V70() Function-yielding V94() set
0 .--> x is non empty Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA ^omega -valued Function-like one-to-one Function-yielding V94() set
{0} --> x is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA ^omega -valued Function-like constant total V38({0},{x}) Function-yielding V94() Element of K6(K7({0},{x}))
{x} is non empty functional set
K7({0},{x}) is Relation-like set
K6(K7({0},{x})) is set
FlattenSeq <%x%> is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(FlattenSeq pp0) ^ (FlattenSeq <%x%>) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(FlattenSeq pp0) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
Seg (len p) is finite V33( len p) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len p ) } is set
dom p is Element of K6(NAT)
p | (Seg (len pp1)) is Relation-like NAT -defined Seg (len pp1) -defined NAT -defined INT -valued Function-like FinSubsequence-like Element of K6(K7(NAT,INT))
K7(NAT,INT) is Relation-like set
K6(K7(NAT,INT)) is set
dom (p | (Seg (len pp1))) is set
((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
((intloc 1),((len k) + 1)) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len (FlattenSeq pp1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (FlattenSeq pp1) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (FlattenSeq pp1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(FlattenSeq pp0) ^ ((intloc 1),((len k) + 1)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (((FlattenSeq pp0) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len (((intloc 2),g) ^ <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
len ((intloc 2),g) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((intloc 2),g) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%((f,(intloc 1)) := (intloc 2))%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%((f,(intloc 1)) := (intloc 2))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
(len ((intloc 2),g)) + (len <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ((len ((intloc 2),g)) + (len <%((f,(intloc 1)) := (intloc 2))%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len ((intloc 2),g)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ((len ((intloc 2),g)) + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
s1 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
(FlattenSeq pp0) ^ s1 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((FlattenSeq pp0) ^ s1) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ s1 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
IC (Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . (IC ) is set
s1 is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) -started set
s1 . (intloc 0) is V11() V12() integer ext-real set
dom ((intloc 1),((len k) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
c3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((intloc 1),((len k) + 1)) . c3 is set
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P . ((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is Element of the InstructionsF of SCM+FSA
dom (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) . ((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is set
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . ((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3) is set
len ((intloc 1),((len k) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((intloc 1),((len k) + 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s1,(len ((intloc 1),((len k) + 1)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s1,(len ((intloc 1),((len k) + 1))))) . (intloc 1) is V11() V12() integer ext-real set
((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
c3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s1,c3) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s1,c3)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s1,c3)) . (IC ) is set
Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + c3))) . (IC ) is set
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((intloc 1),((len k) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))),(len ((intloc 1),((len k) + 1)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))))) . (IC ) is set
s2 is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) -started set
s2 . (intloc 0) is V11() V12() integer ext-real set
dom ((intloc 2),g) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
rq is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((intloc 2),g) . rq is set
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
P . ((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq) is Element of the InstructionsF of SCM+FSA
dom ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ (((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)) . ((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq) is set
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . ((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq) is set
Comput (P,s2,(len ((intloc 2),g))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s2,(len ((intloc 2),g)))) . (intloc 2) is V11() V12() integer ext-real set
Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,s2,(len ((intloc 2),g)))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s2 . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s1 . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
rq is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s2,rq) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s2,rq)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s2,rq)) . (IC ) is set
Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + rq))) . (IC ) is set
rq is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,rq) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,rq)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,rq)) . (IC ) is set
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + 1) - (len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is V11() V12() integer ext-real set
rq - (len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is V11() V12() integer ext-real set
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) - (len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) is V11() V12() integer ext-real set
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ki)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ki))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ki))) . (IC ) is set
((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + 1) - (len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) is V11() V12() integer ext-real set
rq - (len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) is V11() V12() integer ext-real set
((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))) - (len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) is V11() V12() integer ext-real set
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ki)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ki))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + ki))) . (IC ) is set
((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
IC (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . (IC ) is set
P /. (IC (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) is Element of the InstructionsF of SCM+FSA
rq is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) ^ rq is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
dom (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
dom <%((f,(intloc 1)) := (intloc 2))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of K6(NAT)
len ((((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) ^ <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) ^ <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
dom ((((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) ^ <%((f,(intloc 1)) := (intloc 2))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
CurInstr (P,(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) is Element of the InstructionsF of SCM+FSA
P . (len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))) is Element of the InstructionsF of SCM+FSA
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . (len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))) is set
(len ((intloc 1),((len k) + 1))) + (len ((intloc 2),g)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len ((intloc 1),((len k) + 1))) + (len ((intloc 2),g))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + ((len ((intloc 1),((len k) + 1))) + (len ((intloc 2),g)))) is set
(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ x) . ((len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))) + (len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g)))) is set
(len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g))) + 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
((((intloc 1),((len k) + 1)) ^ ((intloc 2),g)) ^ <%((f,(intloc 1)) := (intloc 2))%>) . ((len (((intloc 1),((len k) + 1)) ^ ((intloc 2),g))) + 0) is set
<%((f,(intloc 1)) := (intloc 2))%> . 0 is set
(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
Comput (P,s,((len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))) + 1)) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Following (P,(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))))),(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) 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,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))))) 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,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))))) . (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) is set
Exec (((f,(intloc 1)) := (intloc 2)),(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) 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,((f,(intloc 1)) := (intloc 2))) 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,((f,(intloc 1)) := (intloc 2))) . (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) is set
IC (Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . (IC ) is set
succ (IC (Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g)))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
succ (len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,ki) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,ki)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,ki)) . (IC ) is set
(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . (intloc 2) is V11() V12() integer ext-real set
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . (intloc 2) is V11() V12() integer ext-real set
(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . (intloc 1) is V11() V12() integer ext-real set
abs ((Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . (intloc 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Exec (((f,(intloc 1)) := (intloc 2)),(Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Replace (((Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . f),ki,((Comput (P,s,(len ((((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1))) ^ ((intloc 2),g))))) . (intloc 2))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . (intloc 1) is V11() V12() integer ext-real set
abs ((Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . (intloc 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s2,(len ((intloc 2),g)))) . (intloc 1) is V11() V12() integer ext-real set
abs ((Comput (P,s2,(len ((intloc 2),g)))) . (intloc 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
s2 . (intloc 1) is V11() V12() integer ext-real set
abs (s2 . (intloc 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (s1 . f) is Element of K6(NAT)
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1)) is Relation-like NAT -defined Seg (len pp1) -defined NAT -defined INT -valued Function-like FinSubsequence-like Element of K6(K7(NAT,INT))
h is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . h is set
(p | (Seg (len pp1))) . h is set
len <%x%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%x%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
(len pp0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1)))) . h is set
p . h is set
Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1)))) . h is set
(s1 . f) . h is set
p | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like Element of K6(K7(NAT,INT))
(p | (Seg (len pp0))) . h is set
p . h is set
h is set
(((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) . h is set
(p | (Seg (len pp1))) . h is set
Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom (Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1)))) is Element of K6(NAT)
dom ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) is Element of K6(NAT)
dom (((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . f) | (Seg (len pp1))) is set
len (Replace ((s1 . f),((len k) + 1),(p . ((len k) + 1)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
len (s1 . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
h is V62() Element of the U1 of SCM+FSA
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h is V11() V12() integer ext-real set
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . h is V11() V12() integer ext-real set
(Comput (P,s2,(len ((intloc 2),g)))) . h is V11() V12() integer ext-real set
s2 . h is V11() V12() integer ext-real set
s1 . h is V11() V12() integer ext-real set
s . h is V11() V12() integer ext-real set
h is FinSeq-Location
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp1))))) . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,s,((len (((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) ^ ((intloc 1),((len k) + 1)))) + (len ((intloc 2),g))))) . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,s2,(len ((intloc 2),g)))) . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s2 . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s1 . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s . h is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len ((intloc 1),(len p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((intloc 1),(len p)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len <%(f :=<0,...,0> (intloc 1))%> is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom <%(f :=<0,...,0> (intloc 1))%> is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len ((intloc 1),(len p))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative Element of NAT
(f,p) ^ <%(halt SCM+FSA)%> is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ ((f,p) ^ <%(halt SCM+FSA)%>) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
<%(f :=<0,...,0> (intloc 1))%> ^ ((f,p) ^ <%(halt SCM+FSA)%>) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
((intloc 1),(len p)) ^ (<%(f :=<0,...,0> (intloc 1))%> ^ ((f,p) ^ <%(halt SCM+FSA)%>)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
Comput (P,s,(len ((intloc 1),(len p)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((intloc 1),(len p))))) . (intloc 1) is V11() V12() integer ext-real set
pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,pp0) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,pp0)) . (IC ) is set
<%> ( the InstructionsF of SCM+FSA ^omega) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined the InstructionsF of SCM+FSA ^omega -valued 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
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg (len pp0) is finite V33( len pp0) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp0 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
p | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
len ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega)) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq (<%> ( the InstructionsF of SCM+FSA ^omega))) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
<%> the InstructionsF of SCM+FSA is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined the InstructionsF of SCM+FSA -valued 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
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (<%> the InstructionsF of SCM+FSA) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V70() set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ {} is T-Sequence-like Relation-like NAT -defined Function-like finite V70() set
IC (Comput (P,s,(len ((intloc 1),(len p))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len ((intloc 1),(len p))))) . (IC ) is set
P /. (IC (Comput (P,s,(len ((intloc 1),(len p)))))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,s,(len ((intloc 1),(len p)))))) is Element of the InstructionsF of SCM+FSA
len ((f,p) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((f,p) ^ <%(halt SCM+FSA)%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)) + (len ((f,p) ^ <%(halt SCM+FSA)%>)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of K6(NAT)
CurInstr (P,(Comput (P,s,(len ((intloc 1),(len p)))))) is Element of the InstructionsF of SCM+FSA
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . (len ((intloc 1),(len p))) is set
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) . (len ((intloc 1),(len p))) is set
Comput (P,s,(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Following (P,(Comput (P,s,(len ((intloc 1),(len p)))))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P,(Comput (P,s,(len ((intloc 1),(len p))))))),(Comput (P,s,(len ((intloc 1),(len 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,s,(len ((intloc 1),(len 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,s,(len ((intloc 1),(len p)))))))) . (Comput (P,s,(len ((intloc 1),(len p))))) is set
Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len ((intloc 1),(len 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,(f :=<0,...,0> (intloc 1))) 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,(f :=<0,...,0> (intloc 1))) . (Comput (P,s,(len ((intloc 1),(len p))))) is set
IC (Comput (P,s,(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . (IC ) is set
succ (IC (Comput (P,s,(len ((intloc 1),(len p)))))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V63() ext-real positive non negative set
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,ki) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,ki)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,ki)) . (IC ) is set
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,ki) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,ki)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,ki)) . (IC ) is set
abs ((Comput (P,s,(len ((intloc 1),(len p))))) . (intloc 1)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Exec ((f :=<0,...,0> (intloc 1)),(Comput (P,s,(len ((intloc 1),(len p))))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
ki is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
ki |-> 0 is Relation-like empty-yielding NAT -defined NAT -valued Function-like finite V33(ki) FinSequence-like FinSubsequence-like Function-yielding V94() Element of ki -tuples_on NAT
ki -tuples_on NAT is non empty functional FinSequence-membered FinSequenceSet of NAT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined INT -valued 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() FinSequence of INT
Seg 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 V33( 0 ) FinSequence-like FinSubsequence-like FinSequence-membered integer V70() Function-yielding V94() ext-real non positive non negative V137() Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (Seg 0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() Relation-like non-empty empty-yielding NAT -defined Seg 0 -defined NAT -defined INT -valued 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
g is V62() Element of the U1 of SCM+FSA
(Comput (P,s,(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g is V11() V12() integer ext-real set
(Comput (P,s,(len ((intloc 1),(len p))))) . g is V11() V12() integer ext-real set
s . g is V11() V12() integer ext-real set
g is V62() Element of the U1 of SCM+FSA
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g is V11() V12() integer ext-real set
s . g is V11() V12() integer ext-real set
g is FinSeq-Location
(Comput (P,s,(len (((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>)))) . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P,s,(len ((intloc 1),(len p))))) . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
g is FinSeq-Location
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
pp0 is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA ^omega -valued Function-like finite V70() Function-yielding V94() set
FlattenSeq pp0 is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
(((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0) is T-Sequence-like Relation-like NAT -defined Function-like finite V70() Element of the InstructionsF of SCM+FSA ^omega
len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
len pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom pp0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative set
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Seg (len pp0) is finite V33( len pp0) Element of K6(NAT)
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT : ( 1 <= b₁ & b₁ <= len pp0 ) } is set
((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
p | (len pp0) is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
p | (Seg (len pp0)) is Relation-like NAT -defined Seg (len pp0) -defined NAT -defined INT -valued Function-like FinSubsequence-like set
len ((Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp0))))) . f) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))) is Relation-like the U1 of SCM+FSA -defined Function-like K268(3,SCM+FSA) -compatible total set
IC (Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))))) . (IC ) is set
P /. (IC (Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) is Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) is Element of the InstructionsF of SCM+FSA
CurInstr (P,(Comput (P,s,(len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp)))))) is Element of the InstructionsF of SCM+FSA
(((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (f,p)) ^ <%(halt SCM+FSA)%>) . (len ((((intloc 1),(len p)) ^ <%(f :=<0,...,0> (intloc 1))%>) ^ (FlattenSeq pp))) is set
dom p is Element of K6(NAT)
ki is V62() Element of the U1 of SCM+FSA
(Result (P,s)) . ki is V11() V12() integer ext-real set
s . ki is V11() V12() integer ext-real set
g is FinSeq-Location
(Result (P,s)) . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
s . g is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT