:: SCMFSA6A semantic presentation

REAL is non empty V17() non finite V47() set
NAT is epsilon-transitive epsilon-connected ordinal non empty Element of K48(REAL)
K48(REAL) is set
SCM+FSA is non empty with_non-empty_values IC-Ins-separated strict V93(3) with_explicit_jumps IC-relocable V143(3) AMI-Struct over 3
3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
K526() is set
K503(NAT,K526()) is Element of K526()
K519() is non empty set
K529() is Relation-like K526() -defined 3 -valued Function-like V32(K526(),3) Element of K48(K49(K526(),3))
K49(K526(),3) is Relation-like set
K48(K49(K526(),3)) is set
K530() is Relation-like 3 -defined Function-like total set
K537() is Relation-like K519() -defined K152(K276((K529() (#) K530())),K276((K529() (#) K530()))) -valued Function-like V32(K519(),K152(K276((K529() (#) K530())),K276((K529() (#) K530())))) Element of K48(K49(K519(),K152(K276((K529() (#) K530())),K276((K529() (#) K530())))))
K529() (#) K530() is Relation-like K526() -defined Function-like set
K276((K529() (#) K530())) is set
K152(K276((K529() (#) K530())),K276((K529() (#) K530()))) is set
K49(K519(),K152(K276((K529() (#) K530())),K276((K529() (#) K530())))) is Relation-like set
K48(K49(K519(),K152(K276((K529() (#) K530())),K276((K529() (#) K530()))))) is set
AMI-Struct(# K526(),K503(NAT,K526()),K519(),K529(),K530(),K537() #) is strict AMI-Struct over 3
the U2 of SCM+FSA is non empty set
COMPLEX is non empty V17() non finite V47() set
NAT is epsilon-transitive epsilon-connected ordinal non empty set
K48(NAT) is set
K48(NAT) is set
9 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
Segm 9 is Element of K48(NAT)
Int-Locations is non empty set
K313() is set
K48(K313()) is set
2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
K49(K313(),2) is Relation-like set
K48(K49(K313(),2)) is set
K315() is Relation-like K313() -defined 2 -valued Function-like V32(K313(),2) Element of K48(K49(K313(),2))
K316() is Relation-like 2 -defined Function-like total set
K315() (#) K316() is Relation-like K313() -defined Function-like set
K276((K315() (#) K316())) is set
K307() is non empty set
K152(K276((K315() (#) K316())),K276((K315() (#) K316()))) is set
K49(K307(),K152(K276((K315() (#) K316())),K276((K315() (#) K316())))) is Relation-like set
K48(K49(K307(),K152(K276((K315() (#) K316())),K276((K315() (#) K316()))))) is set
K48( the U2 of SCM+FSA) is set
the InstructionsF of SCM+FSA is Relation-like non empty standard-ins V55() J/A-independent V58() set
INT is non empty V17() non finite V47() set
RAT is non empty V17() non finite V47() set
K451() is non empty with_non-empty_values IC-Ins-separated strict strict V93(2) AMI-Struct over 2
the InstructionsF of K451() is Relation-like non empty standard-ins V55() J/A-independent V58() set
the U2 of K451() is non empty set
the_Values_of K451() is Relation-like non-empty the U2 of K451() -defined Function-like total set
the Object-Kind of K451() is Relation-like the U2 of K451() -defined 2 -valued Function-like V32( the U2 of K451(),2) Element of K48(K49( the U2 of K451(),2))
K49( the U2 of K451(),2) is Relation-like set
K48(K49( the U2 of K451(),2)) is set
the ValuesF of K451() is Relation-like 2 -defined Function-like total set
the Object-Kind of K451() (#) the ValuesF of K451() is Relation-like the U2 of K451() -defined Function-like set
K518() is set
K48(K526()) is set
the_Values_of SCM+FSA is Relation-like non-empty the U2 of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like the U2 of SCM+FSA -defined 3 -valued Function-like V32( the U2 of SCM+FSA,3) Element of K48(K49( the U2 of SCM+FSA,3))
K49( the U2 of SCM+FSA,3) is Relation-like set
K48(K49( the U2 of SCM+FSA,3)) is set
the ValuesF of SCM+FSA is Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA is Relation-like the U2 of SCM+FSA -defined Function-like set
Int-Locations is non empty Element of K48( the U2 of SCM+FSA)
K48(Int-Locations) is set
K49(NAT,K48(NAT)) is Relation-like set
K48(K49(NAT,K48(NAT))) is set
FinPartSt SCM+FSA is non empty Element of K48(K280((the_Values_of SCM+FSA)))
K280((the_Values_of SCM+FSA)) is set
K48(K280((the_Values_of SCM+FSA))) is set
{ b₁ where b₁ is Element of K280((the_Values_of SCM+FSA)) : b₁ is finite } is set
K49((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K48(K49((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional ext-real V27() V28() integer finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V124() set
the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional ext-real V27() V28() integer finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V124() set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional ext-real V27() V28() integer finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V124() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional ext-real V27() V28() integer finite finite-yielding V39() FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V124() Element of NAT
12 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
4 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
5 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
6 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
7 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
8 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
10 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
11 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive V27() V28() integer V46() Element of NAT
K21(6,7,8) is finite V46() set
IC is V72( SCM+FSA ) Element of the U2 of SCM+FSA
halt SCM+FSA is ins-loc-free V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
halt the InstructionsF of SCM+FSA is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K31(0,{},{}) is set
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
f is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
goto f is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(f) is Element of the InstructionsF of K451()
q +~ ((halt SCM+FSA),(goto f)) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto f) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} is non empty finite set
{(halt SCM+FSA)} --> (goto f) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto f)} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto f)}) finite Element of K48(K49({(halt SCM+FSA)},{(goto f)}))
{(goto f)} is non empty finite set
K49({(halt SCM+FSA)},{(goto f)}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto f)})) is finite V39() set
q (#) ((halt SCM+FSA) .--> (goto f)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q +* (q (#) ((halt SCM+FSA) .--> (goto f))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card q is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(q,(card q)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card q) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card q)) is Element of the InstructionsF of K451()
q +~ ((halt SCM+FSA),(goto (card q))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card q)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card q)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card q))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card q))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card q))}))
{(goto (card q))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card q))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card q))})) is finite V39() set
q (#) ((halt SCM+FSA) .--> (goto (card q))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q +* (q (#) ((halt SCM+FSA) .--> (goto (card q)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card q is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(q,(card q)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card q) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card q)) is Element of the InstructionsF of K451()
q +~ ((halt SCM+FSA),(goto (card q))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card q)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card q)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card q))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card q))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card q))}))
{(goto (card q))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card q))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card q))})) is finite V39() set
q (#) ((halt SCM+FSA) .--> (goto (card q))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q +* (q (#) ((halt SCM+FSA) .--> (goto (card q)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer set
dom (q) is finite V117() set
f is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer set
dom q is non empty finite V117() set
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
card q is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(q,(card q)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card q) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card q)) is Element of the InstructionsF of K451()
q +~ ((halt SCM+FSA),(goto (card q))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card q)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card q)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card q))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card q))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card q))}))
{(goto (card q))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card q))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card q))})) is finite V39() set
q (#) ((halt SCM+FSA) .--> (goto (card q))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
q +* (q (#) ((halt SCM+FSA) .--> (goto (card q)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
rng (q) is non empty finite set
id the InstructionsF of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued non empty Function-like one-to-one total Element of K48(K49( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA))
K49( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) is Relation-like set
K48(K49( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA)) is set
q is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
f is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(f) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
card f is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(f,(card f)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card f) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card f)) is Element of the InstructionsF of K451()
f +~ ((halt SCM+FSA),(goto (card f))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card f)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card f)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card f))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card f))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card f))}))
{(goto (card f))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card f))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card f))})) is finite V39() set
f (#) ((halt SCM+FSA) .--> (goto (card f))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
f +* (f (#) ((halt SCM+FSA) .--> (goto (card f)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
Reloc ((f),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((f),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((f),q)),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
Reloc (f,q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (f,q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (f,q)),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
q + (card f) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
goto (q + (card f)) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((q + (card f))) is Element of the InstructionsF of K451()
(halt SCM+FSA) .--> (goto (q + (card f))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (q + (card f))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (q + (card f)))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (q + (card f)))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (q + (card f)))}))
{(goto (q + (card f)))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (q + (card f)))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (q + (card f)))})) is finite V39() set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (q + (card f)))) is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
(Reloc (f,q)) (#) ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (q + (card f))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
rng ((halt SCM+FSA) .--> (goto (card f))) is V17() finite set
{(goto (card f))} is Relation-like non empty finite Element of K48( the InstructionsF of SCM+FSA)
K48( the InstructionsF of SCM+FSA) is set
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card f))) is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
rng ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card f)))) is non empty set
rng (id the InstructionsF of SCM+FSA) is non empty set
(rng (id the InstructionsF of SCM+FSA)) \/ {(goto (card f))} is non empty set
dom ((halt SCM+FSA) .--> (goto (card f))) is V17() finite set
{(halt SCM+FSA)} is Relation-like non empty finite Element of K48( the InstructionsF of SCM+FSA)
dom ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA) .--> (goto (card f)))) is non empty set
dom (id the InstructionsF of SCM+FSA) is non empty set
(dom (id the InstructionsF of SCM+FSA)) \/ {(halt SCM+FSA)} is non empty set
IncAddr ((goto (card f)),q) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i is Relation-like the InstructionsF of SCM+FSA -defined the InstructionsF of SCM+FSA -valued Function-like V32( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA) Element of K48(K49( the InstructionsF of SCM+FSA, the InstructionsF of SCM+FSA))
(id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto (card f))) is Relation-like Function-like set
rng f is non empty finite set
Shift ((f),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
IncAddr ((Shift ((f),q)),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
Shift (f,q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
IncAddr ((Shift (f,q)),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
f (#) i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Shift (f,q)) (#) i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (((Shift (f,q)) (#) i),q) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
intloc 0 is V100() V149() Element of the U2 of SCM+FSA
K460(0) is V100() Element of the U2 of K451()
(intloc 0) .--> 1 is Relation-like the U2 of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued V17() Function-like one-to-one constant the_Values_of SCM+FSA -compatible finite data-only set
{(intloc 0)} is non empty finite set
{(intloc 0)} --> 1 is Relation-like non-empty {(intloc 0)} -defined NAT -valued {1} -valued non empty Function-like constant total V32({(intloc 0)},{1}) finite Element of K48(K49({(intloc 0)},{1}))
{1} is non empty finite V46() V47() set
K49({(intloc 0)},{1}) is Relation-like finite set
K48(K49({(intloc 0)},{1})) is finite V39() set
{0,6,7,8} is finite Element of K48(NAT)
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
InsCode i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K39( the InstructionsF of SCM+FSA) is set
j is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Exec (i,j) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) -valued Function-like V32( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K48(K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K48(K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
the Execution of SCM+FSA . i is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . i) . j is set
(Exec (i,j)) . (IC ) is set
IC j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
j . (IC ) is set
succ (IC j) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V27() V28() integer V46() set
K is V100() Element of the U2 of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
K := n is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
AddTo (K,n) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
SubFrom (K,n) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
MultBy (K,n) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
Divide (K,n) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
n is V100() Element of the U2 of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
i is FinSeq-Location
n := (i,K) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*n,i,K*> is Relation-like NAT -defined non empty Function-like finite 3 -element FinSequence-like FinSubsequence-like set
K31(9,{},<*n,i,K*>) is set
n is V100() Element of the U2 of SCM+FSA
K is V100() Element of the U2 of SCM+FSA
i is FinSeq-Location
(i,K) := n is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*n,i,K*> is Relation-like NAT -defined non empty Function-like finite 3 -element FinSequence-like FinSubsequence-like set
K31(10,{},<*n,i,K*>) is set
K is V100() Element of the U2 of SCM+FSA
n is FinSeq-Location
K :=len n is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*K,n*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
K31(11,{},<*K,n*>) is set
K is V100() Element of the U2 of SCM+FSA
n is FinSeq-Location
n :=<0,...,0> K is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*K,n*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
K31(12,{},<*K,n*>) is set
Data-Locations is Element of K48( the U2 of SCM+FSA)
j is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
j . (IC ) is set
K is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC K is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
K . (IC ) is set
DataPart j is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
j | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart K is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
K | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(IC j) + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec (i,j) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) -valued Function-like V32( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K48(K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K48(K49( the InstructionsF of SCM+FSA,K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
the Execution of SCM+FSA . i is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . i) . j is set
IC (Exec (i,j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(Exec (i,j)) . (IC ) is set
(IC (Exec (i,j))) + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
IncAddr (i,n) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((IncAddr (i,n)),K) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
the Execution of SCM+FSA . (IncAddr (i,n)) is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . (IncAddr (i,n))) . K is set
IC (Exec ((IncAddr (i,n)),K)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(Exec ((IncAddr (i,n)),K)) . (IC ) is set
DataPart (Exec (i,j)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Exec (i,j)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Exec ((IncAddr (i,n)),K)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Exec ((IncAddr (i,n)),K)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
succ (IC j) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V27() V28() integer V46() set
(succ (IC j)) + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i0 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i0 + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i0 + 1) + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i0 + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i0 + n) + 1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
succ (IC K) is epsilon-transitive epsilon-connected ordinal natural non empty ext-real V27() V28() integer V46() set
InsCode i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K39( the InstructionsF of SCM+FSA) is set
{6,7,8} is finite V46() Element of K48(NAT)
Exec (i,K) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
( the Execution of SCM+FSA . i) . K is set
l is V100() Element of the U2 of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
l := l1 is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is V100() Element of the U2 of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
AddTo (l,l1) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
K . l is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
(K . l) + (K . l1) is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is V100() Element of the U2 of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
SubFrom (l,l1) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
K . l is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
(K . l) - (K . l1) is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is V100() Element of the U2 of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
MultBy (l,l1) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
K . l is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
(K . l) * (K . l1) is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is V100() Element of the U2 of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
Divide (l,l1) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
K . l is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
(K . l) mod (K . l1) is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
K . l is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
(K . l) div (K . l1) is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
goto l is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(l) is Element of the InstructionsF of K451()
l + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
goto (l + n) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((l + n)) is Element of the InstructionsF of K451()
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 is V100() Element of the U2 of SCM+FSA
l1 =0_goto l is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 =0_goto (l + n) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 is V100() Element of the U2 of SCM+FSA
l1 >0_goto l is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l + n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 >0_goto (l + n) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
l1 := (l1,l) is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*l1,l1,l*> is Relation-like NAT -defined non empty Function-like finite 3 -element FinSequence-like FinSubsequence-like set
K31(9,{},<*l1,l1,l*>) is set
c is V100() Element of the U2 of SCM+FSA
j . l is ext-real V27() V28() integer set
abs (j . l) is ext-real V27() V28() Element of REAL
Exec ((l1 := (l1,l)),j) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
the Execution of SCM+FSA . (l1 := (l1,l)) is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . (l1 := (l1,l))) . j is set
(Exec ((l1 := (l1,l)),j)) . c is ext-real V27() V28() integer set
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
m2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(j . l1) /. m2 is ext-real V27() V28() integer Element of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l is ext-real V27() V28() integer set
abs (K . l) is ext-real V27() V28() Element of REAL
Exec ((l1 := (l1,l)),K) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
( the Execution of SCM+FSA . (l1 := (l1,l))) . K is set
(Exec ((l1 := (l1,l)),K)) . c is ext-real V27() V28() integer set
m1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(K . l1) /. m1 is ext-real V27() V28() integer Element of INT
(Exec (i,j)) . c is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . c is ext-real V27() V28() integer set
c is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . c is ext-real V27() V28() integer set
j . c is ext-real V27() V28() integer set
K . c is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . c is ext-real V27() V28() integer set
c is V100() Element of the U2 of SCM+FSA
c is FinSeq-Location
(Exec (i,j)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l1 is V100() Element of the U2 of SCM+FSA
l is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(l1,l) := l1 is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*l1,l1,l*> is Relation-like NAT -defined non empty Function-like finite 3 -element FinSequence-like FinSubsequence-like set
K31(10,{},<*l1,l1,l*>) is set
c is FinSeq-Location
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l is ext-real V27() V28() integer set
abs (K . l) is ext-real V27() V28() Element of REAL
Exec (((l1,l) := l1),K) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
the Execution of SCM+FSA . ((l1,l) := l1) is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . ((l1,l) := l1)) . K is set
(Exec (((l1,l) := l1),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
m2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(K . l1) +* (m2,(K . l1)) is Relation-like Function-like set
j . l is ext-real V27() V28() integer set
abs (j . l) is ext-real V27() V28() Element of REAL
Exec (((l1,l) := l1),j) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
( the Execution of SCM+FSA . ((l1,l) := l1)) . j is set
(Exec (((l1,l) := l1),j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
m1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(j . l1) +* (m1,(j . l1)) is Relation-like Function-like set
(Exec (i,j)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
c is FinSeq-Location
(Exec (i,j)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . c is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
c is FinSeq-Location
c is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . c is ext-real V27() V28() integer set
j . c is ext-real V27() V28() integer set
K . c is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . c is ext-real V27() V28() integer set
l is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
l :=len l1 is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*l,l1*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
K31(11,{},<*l,l1*>) is set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len (j . l1) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len (K . l1) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
l1 is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l is V100() Element of the U2 of SCM+FSA
l1 is FinSeq-Location
l1 :=<0,...,0> l is ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*l,l1*> is Relation-like NAT -defined non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like set
K31(12,{},<*l,l1*>) is set
l1 is FinSeq-Location
j . l is ext-real V27() V28() integer set
abs (j . l) is ext-real V27() V28() Element of REAL
Exec ((l1 :=<0,...,0> l),j) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
the Execution of SCM+FSA . (l1 :=<0,...,0> l) is Element of K152(K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K276(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . (l1 :=<0,...,0> l)) . j is set
(Exec ((l1 :=<0,...,0> l),j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l is ext-real V27() V28() integer set
abs (K . l) is ext-real V27() V28() Element of REAL
Exec ((l1 :=<0,...,0> l),K) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
( the Execution of SCM+FSA . (l1 :=<0,...,0> l)) . K is set
(Exec ((l1 :=<0,...,0> l),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
c is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
c |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of c -tuples_on NAT
c -tuples_on NAT is FinSequenceSet of NAT
m2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
m2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of m2 -tuples_on NAT
m2 -tuples_on NAT is FinSequenceSet of NAT
l1 is FinSeq-Location
(Exec (i,j)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
j . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
K . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Exec ((IncAddr (i,n)),K)) . l1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
l1 is FinSeq-Location
l1 is V100() Element of the U2 of SCM+FSA
(Exec (i,j)) . l1 is ext-real V27() V28() integer set
j . l1 is ext-real V27() V28() integer set
K . l1 is ext-real V27() V28() integer set
(Exec ((IncAddr (i,n)),K)) . l1 is ext-real V27() V28() integer set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V17() Function-like constant finite initial non halt-free V62( SCM+FSA ) V63( SCM+FSA ) V145(3, SCM+FSA ) set
K234((halt SCM+FSA)) is set
0 .--> (halt SCM+FSA) is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} is non empty functional finite V39() set
{0} --> (halt SCM+FSA) is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(halt SCM+FSA)} -valued non empty Function-like constant total V32({0},{(halt SCM+FSA)}) finite Element of K48(K49({0},{(halt SCM+FSA)}))
K49({0},{(halt SCM+FSA)}) is Relation-like finite set
K48(K49({0},{(halt SCM+FSA)})) is finite V39() set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(i) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
dom j is non empty finite V117() set
{ (b₁ + (card i)) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b₁ in dom j } is set
i0 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer set
dom ((i) +* (Reloc (j,(card i)))) is non empty finite V117() set
i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer set
dom (i) is non empty finite V117() set
dom i is non empty finite V117() set
dom (Reloc (j,(card i))) is finite V117() set
(dom i) \/ { (b₁ + (card i)) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b₁ in dom j } is non empty set
l is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l + (card i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer set
(card i) + l1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
l1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial non halt-free set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
dom i is non empty finite V117() set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i . K is set
(i,j) . K is set
Shift (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
IncAddr ((Shift (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
dom (Reloc (j,(card i))) is finite V117() set
dom (Shift (j,(card i))) is non empty finite V117() set
dom j is non empty finite V117() set
{ (b₁ + (card i)) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b₁ in dom j } is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
n + (card i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(i) . K is set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is set
dom (i) is non empty finite V117() set
dom i is non empty finite V117() set
dom (Reloc (j,(card i))) is finite V117() set
(i) . K is set
(i,j) . K is set
dom (i,j) is non empty finite V117() set
(dom (i)) \/ (dom (Reloc (j,(card i)))) is non empty finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
dom i is non empty finite V117() set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
dom (i,j) is non empty finite V117() set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
dom (i) is non empty finite V117() set
dom (Reloc (j,(card i))) is finite V117() set
(dom (i)) \/ (dom (Reloc (j,(card i)))) is non empty finite set
(dom i) \/ (dom (Reloc (j,(card i)))) is non empty finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
dom (i,j) is non empty finite V117() set
K is set
(i +* (i,j)) . K is set
(i,j) . K is set
dom (i +* (i,j)) is non empty finite V117() set
dom i is non empty finite V117() set
(dom i) \/ (dom (i,j)) is non empty finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc (j,(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc ((Macro j),(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card i) + (card j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
dom (i,j) is non empty finite V117() set
card (dom (i,j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
dom i is non empty finite V117() set
card (dom i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
dom j is non empty finite V117() set
card (dom j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
dom (i) is non empty finite V117() set
dom (Reloc (j,(card i))) is finite V117() set
(dom (i)) \/ (dom (Reloc (j,(card i)))) is non empty finite set
(dom i) \/ (dom (Reloc (j,(card i)))) is non empty finite set
card (dom (Reloc (j,(card i)))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
card (Reloc (j,(card i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
goto j is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(j) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto j)) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto j) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto j) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto j)} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto j)}) finite Element of K48(K49({(halt SCM+FSA)},{(goto j)}))
{(goto j)} is non empty finite set
K49({(halt SCM+FSA)},{(goto j)}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto j)})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
rng (i,j) is finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto j is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(j) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto j)) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto j) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto j) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto j)} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto j)}) finite Element of K48(K49({(halt SCM+FSA)},{(goto j)}))
{(goto j)} is non empty finite set
K49({(halt SCM+FSA)},{(goto j)}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto j)})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
rng i is finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Shift ((IncAddr ((i),j)),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Reloc (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Shift ((IncAddr (i,j)),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(card i) + j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((Reloc (i,j)),((card i) + j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto ((card i) + j) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(((card i) + j)) is Element of the InstructionsF of K451()
(Reloc (i,j)) +~ ((halt SCM+FSA),(goto ((card i) + j))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto ((card i) + j)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto ((card i) + j)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto ((card i) + j))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto ((card i) + j))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto ((card i) + j))}))
{(goto ((card i) + j))} is non empty finite set
K49({(halt SCM+FSA)},{(goto ((card i) + j))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto ((card i) + j))})) is finite V39() set
(Reloc (i,j)) (#) ((halt SCM+FSA) .--> (goto ((card i) + j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Reloc (i,j)) +* ((Reloc (i,j)) (#) ((halt SCM+FSA) .--> (goto ((card i) + j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
dom (Reloc (i,j)) is finite V117() set
dom i is finite V117() set
{ (b₁ + j) where b₁ is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b₁ in dom i } is set
dom (i) is finite V117() set
dom (Reloc ((i),j)) is finite V117() set
K is set
n is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
n + j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(i) . n is set
i . n is set
i0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (i,j)) . K is set
IncAddr (i0,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
{(halt SCM+FSA)} is Relation-like non empty finite Element of K48( the InstructionsF of SCM+FSA)
K48( the InstructionsF of SCM+FSA) is set
dom ((halt SCM+FSA) .--> (goto ((card i) + j))) is V17() finite set
dom ((Reloc (i,j)) (#) ((halt SCM+FSA) .--> (goto ((card i) + j)))) is finite V117() set
((Reloc (i,j)),((card i) + j)) . K is set
((Reloc (i,j)) (#) ((halt SCM+FSA) .--> (goto ((card i) + j)))) . K is set
((halt SCM+FSA) .--> (goto ((card i) + j))) . ((Reloc (i,j)) . K) is set
IncAddr (i,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (i,j)) . K is set
IncAddr (i0,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
InsCode (halt SCM+FSA) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer V141(3, SCM+FSA ) Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K39( the InstructionsF of SCM+FSA) is set
InsCode i0 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of InsCodes the InstructionsF of SCM+FSA
{(halt SCM+FSA)} is Relation-like non empty finite Element of K48( the InstructionsF of SCM+FSA)
K48( the InstructionsF of SCM+FSA) is set
dom ((halt SCM+FSA) .--> (goto ((card i) + j))) is V17() finite set
dom ((Reloc (i,j)) (#) ((halt SCM+FSA) .--> (goto ((card i) + j)))) is finite V117() set
((Reloc (i,j)),((card i) + j)) . K is set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (i,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((Reloc (i,j)),((card i) + j)) . K is set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (i,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((Reloc (i,j)),((card i) + j)) . K is set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr (i,j) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc ((i),j)) . K is set
dom ((Reloc (i,j)),((card i) + j)) is finite V117() set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued non empty Function-like finite initial halt-free V63( SCM+FSA ) set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((i,j),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (i,j)) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (i,j))) is Element of the InstructionsF of K451()
(i,j) +~ ((halt SCM+FSA),(goto (card (i,j)))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (i,j))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (i,j))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (i,j)))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (i,j)))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (i,j)))}))
{(goto (card (i,j)))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (i,j)))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (i,j)))})) is finite V39() set
(i,j) (#) ((halt SCM+FSA) .--> (goto (card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,j) +* ((i,j) (#) ((halt SCM+FSA) .--> (goto (card (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued non empty Function-like finite initial halt-free V63( SCM+FSA ) set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(j,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card j) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card j)) is Element of the InstructionsF of K451()
j +~ ((halt SCM+FSA),(goto (card j))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card j)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card j)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card j))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card j))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card j))}))
{(goto (card j))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card j))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card j))})) is finite V39() set
j (#) ((halt SCM+FSA) .--> (goto (card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j +* (j (#) ((halt SCM+FSA) .--> (goto (card j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(i,(j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j),(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc ((j),(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued non empty Function-like finite initial halt-free V63( SCM+FSA ) set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(card i) + (card j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((Reloc (j,(card i))),((card i) + (card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto ((card i) + (card j)) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457(((card i) + (card j))) is Element of the InstructionsF of K451()
(Reloc (j,(card i))) +~ ((halt SCM+FSA),(goto ((card i) + (card j)))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto ((card i) + (card j))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto ((card i) + (card j))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto ((card i) + (card j)))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto ((card i) + (card j)))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto ((card i) + (card j)))}))
{(goto ((card i) + (card j)))} is non empty finite set
K49({(halt SCM+FSA)},{(goto ((card i) + (card j)))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto ((card i) + (card j)))})) is finite V39() set
(Reloc (j,(card i))) (#) ((halt SCM+FSA) .--> (goto ((card i) + (card j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Reloc (j,(card i))) +* ((Reloc (j,(card i))) (#) ((halt SCM+FSA) .--> (goto ((card i) + (card j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) +* ((Reloc (j,(card i))),((card i) + (card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((Reloc (j,(card i))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
(Reloc (j,(card i))) +~ ((halt SCM+FSA),(goto (card (i,j)))) is Relation-like Function-like set
(Reloc (j,(card i))) (#) ((halt SCM+FSA) .--> (goto (card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Reloc (j,(card i))) +* ((Reloc (j,(card i))) (#) ((halt SCM+FSA) .--> (goto (card (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) +* ((Reloc (j,(card i))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((i),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
(i) +~ ((halt SCM+FSA),(goto (card (i,j)))) is Relation-like Function-like set
(i) (#) ((halt SCM+FSA) .--> (goto (card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) +* ((i) (#) ((halt SCM+FSA) .--> (goto (card (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((i),(card (i,j))) +* ((Reloc (j,(card i))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(i,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop i)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop i)),(card (CutLastLoc (stop i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop i))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop i)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop i)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop i))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop i)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop i))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}))
{(goto (card (CutLastLoc (stop i))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop i))))})) is finite V39() set
(CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop i)) +* ((CutLastLoc (stop i)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card i is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc (j,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((i,j),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((i,j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (i,j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (i,j))),(card (CutLastLoc (stop (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (i,j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (i,j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (i,j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (i,j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (i,j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}))
{(goto (card (CutLastLoc (stop (i,j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))})) is finite V39() set
(CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (i,j))) +* ((CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (i,j)))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (i,j)))) +* (Reloc (K,(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(j,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop j)),(card (CutLastLoc (stop j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop j))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop j)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop j)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop j))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop j)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop j))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}))
{(goto (card (CutLastLoc (stop j))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))})) is finite V39() set
(CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop j)) +* ((CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc (K,(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((j,K),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j,K),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j,K),(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop i))) +* (Reloc ((j,K),(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued non empty Function-like finite initial halt-free V63( SCM+FSA ) set
(j,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card j) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card j)) is Element of the InstructionsF of K451()
j +~ ((halt SCM+FSA),(goto (card j))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card j)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card j)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card j))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card j))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card j))}))
{(goto (card j))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card j))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card j))})) is finite V39() set
j (#) ((halt SCM+FSA) .--> (goto (card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j +* (j (#) ((halt SCM+FSA) .--> (goto (card j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
Reloc ((j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j),(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
Reloc ((Reloc (K,(card j))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Reloc (K,(card j))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Shift ((IncAddr ((Reloc (K,(card j))),(card i))),(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Reloc ((j),(card i))) +* (Reloc ((Reloc (K,(card j))),(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(card j) + (card i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,((card j) + (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,((card j) + (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,((card j) + (card i)))),((card j) + (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(Reloc ((j),(card i))) +* (Reloc (K,((card j) + (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((CutLastLoc (stop i))) +* (Reloc ((j),(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j)) +* (Reloc (K,(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued non empty Function-like finite initial halt-free V63( SCM+FSA ) set
(i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card i) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card i)) is Element of the InstructionsF of K451()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card i)) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card i)) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card i))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card i))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card i))}))
{(goto (card i))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card i))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card i))})) is finite V39() set
i (#) ((halt SCM+FSA) .--> (goto (card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i +* (i (#) ((halt SCM+FSA) .--> (goto (card i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
(Reloc ((j),(card i))) +* (Reloc (K,(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i) +* ((Reloc ((j),(card i))) +* (Reloc (K,(card (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(j,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop j)),(card (CutLastLoc (stop j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop j))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop j)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop j)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop j))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop j)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop j))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}))
{(goto (card (CutLastLoc (stop j))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))})) is finite V39() set
(CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop j)) +* ((CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc (K,(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((j,K),i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((j,K),(Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((j,K),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (j,K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (j,K))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (j,K))),(card (CutLastLoc (stop (j,K))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (j,K)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (j,K))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (j,K))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (j,K)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,K))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (j,K))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (j,K)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,K)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,K)))))}))
{(goto (card (CutLastLoc (stop (j,K)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,K)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,K)))))})) is finite V39() set
(CutLastLoc (stop (j,K))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,K)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (j,K))) +* ((CutLastLoc (stop (j,K))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,K))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (j,K) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro i),(card (j,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro i),(card (j,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro i),(card (j,K)))),(card (j,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (j,K)))) +* (Reloc ((Macro i),(card (j,K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(K,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(K,(Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(K,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop K)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop K)),(card (CutLastLoc (stop K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop K))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop K)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop K)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop K))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop K)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop K))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}))
{(goto (card (CutLastLoc (stop K))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))})) is finite V39() set
(CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop K)) +* ((CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro i),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro i),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro i),(card K))),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop K))) +* (Reloc ((Macro i),(card K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,(K,i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((K,i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((K,i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((K,i),(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc ((K,i),(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(j,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,(Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(j,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop j)),(card (CutLastLoc (stop j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop j))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop j)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop j)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop j))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop j)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop j))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}))
{(goto (card (CutLastLoc (stop j))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))})) is finite V39() set
(CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop j)) +* ((CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro i),(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc ((Macro i),(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((j,i),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (j,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((j,i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (j,i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (j,i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (j,i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (j,i))),(card (CutLastLoc (stop (j,i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (j,i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (j,i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (j,i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (j,i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (j,i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (j,i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,i)))))}))
{(goto (card (CutLastLoc (stop (j,i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (j,i)))))})) is finite V39() set
(CutLastLoc (stop (j,i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (j,i))) +* ((CutLastLoc (stop (j,i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (j,i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (j,i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (j,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (j,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (j,i)))),(card (j,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (j,i)))) +* (Reloc (K,(card (j,i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc (K,(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,(i,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((i,K),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((i,K),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((i,K),(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc ((i,K),(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(K,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(K,(Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(K,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop K)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop K)),(card (CutLastLoc (stop K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop K))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop K)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop K)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop K))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop K)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop K))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}))
{(goto (card (CutLastLoc (stop K))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))})) is finite V39() set
(CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop K)) +* ((CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro i),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro i),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro i),(card K))),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop K))) +* (Reloc ((Macro i),(card K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((K,i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((K,i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (K,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((K,i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (K,i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (K,i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (K,i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (K,i))),(card (CutLastLoc (stop (K,i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (K,i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (K,i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (K,i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (K,i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (K,i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (K,i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (K,i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (K,i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (K,i)))))}))
{(goto (card (CutLastLoc (stop (K,i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (K,i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (K,i)))))})) is finite V39() set
(CutLastLoc (stop (K,i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (K,i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (K,i))) +* ((CutLastLoc (stop (K,i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (K,i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (K,i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (K,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (K,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (K,i)))),(card (K,i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (K,i)))) +* (Reloc ((Macro j),(card (K,i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(K,(i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((i,j),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((i,j),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((i,j),(card K))),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop K))) +* (Reloc ((i,j),(card K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc (j,(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((i,j),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((i,j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (i,j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (i,j))),(card (CutLastLoc (stop (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (i,j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (i,j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (i,j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (i,j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (i,j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}))
{(goto (card (CutLastLoc (stop (i,j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))})) is finite V39() set
(CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (i,j))) +* ((CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (i,j)))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (i,j)))) +* (Reloc (K,(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(j,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop j)),(card (CutLastLoc (stop j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop j))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop j)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop j)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop j))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop j)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop j))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}))
{(goto (card (CutLastLoc (stop j))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))})) is finite V39() set
(CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop j)) +* ((CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc (K,(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j,K),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((j,K),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc (K,(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((i,K),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((i,K),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (i,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((i,K),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (i,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (i,K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (i,K))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (i,K))),(card (CutLastLoc (stop (i,K))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (i,K)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (i,K))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (i,K))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (i,K)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,K))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (i,K))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (i,K)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,K)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,K)))))}))
{(goto (card (CutLastLoc (stop (i,K)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,K)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,K)))))})) is finite V39() set
(CutLastLoc (stop (i,K))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,K)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (i,K))) +* ((CutLastLoc (stop (i,K))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,K))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,K) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (i,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (i,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (i,K)))),(card (i,K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (i,K)))) +* (Reloc ((Macro j),(card (i,K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(K,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(K,(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(K,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop K)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop K)),(card (CutLastLoc (stop K)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop K))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop K)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop K)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop K))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop K)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop K))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}))
{(goto (card (CutLastLoc (stop K))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop K))))})) is finite V39() set
(CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop K)) +* ((CutLastLoc (stop K)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop K)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card K is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card K))),(card K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop K))) +* (Reloc ((Macro j),(card K))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(K,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),(K,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((K,j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((K,j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((K,j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((K,j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((i,j),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((i,j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (i,j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (i,j))),(card (CutLastLoc (stop (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (i,j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (i,j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (i,j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (i,j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (i,j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}))
{(goto (card (CutLastLoc (stop (i,j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))})) is finite V39() set
(CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (i,j))) +* ((CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (i,j)))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (i,j)))) +* (Reloc (K,(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro j),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro j))),(card (CutLastLoc (stop (Macro j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}))
{(goto (card (CutLastLoc (stop (Macro j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))})) is finite V39() set
(CutLastLoc (stop (Macro j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro j))) +* ((CutLastLoc (stop (Macro j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (K,(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (K,(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (K,(card (Macro j)))),(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro j)))) +* (Reloc (K,(card (Macro j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j,K),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((j,K),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
K is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((i,j),K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro K is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> K is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> K is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {K} -valued non empty Function-like constant total V32({0},{K}) finite Element of K48(K49({0},{K}))
{K} is non empty finite set
K49({0},{K}) is Relation-like finite set
K48(K49({0},{K})) is finite V39() set
stop K262(SCM+FSA,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((i,j),(Macro K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((i,j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (i,j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (i,j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (i,j))),(card (CutLastLoc (stop (i,j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (i,j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (i,j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (i,j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (i,j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (i,j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (i,j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}))
{(goto (card (CutLastLoc (stop (i,j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (i,j)))))})) is finite V39() set
(CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (i,j))) +* ((CutLastLoc (stop (i,j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (i,j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro K),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro K),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro K),(card (i,j)))),(card (i,j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (i,j)))) +* (Reloc ((Macro K),(card (i,j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,K) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro j),(Macro K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro j),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro j))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro j))),(card (CutLastLoc (stop (Macro j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro j)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro j))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro j))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro j)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro j))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro j)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}))
{(goto (card (CutLastLoc (stop (Macro j)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro j)))))})) is finite V39() set
(CutLastLoc (stop (Macro j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro j))) +* ((CutLastLoc (stop (Macro j))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro j))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro K),(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro K),(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro K),(card (Macro j)))),(card (Macro j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro j)))) +* (Reloc ((Macro K),(card (Macro j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(i,(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
((Macro i),(j,K)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Reloc ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((j,K),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((j,K),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((j,K),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (j,(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr (j,(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc (j,(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card j) + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card (Macro i)) + (card j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
(j,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(j,(Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224(j,(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop j)),(card (CutLastLoc (stop j)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop j))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop j)))) is Element of the InstructionsF of K451()
(CutLastLoc (stop j)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop j))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop j)))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop j))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}))
{(goto (card (CutLastLoc (stop j))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop j))))})) is finite V39() set
(CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop j)) +* ((CutLastLoc (stop j)) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop j)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card j is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro i),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro i),(card j))),(card j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop j))) +* (Reloc ((Macro i),(card j))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (j,i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card j) + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card (Macro i)) + (card j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
i is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
j is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Macro i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> i is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> i is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {i} -valued non empty Function-like constant total V32({0},{i}) finite Element of K48(K49({0},{i}))
{i} is non empty finite set
K49({0},{i}) is Relation-like finite set
K48(K49({0},{i})) is finite V39() set
stop K262(SCM+FSA,i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro j is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
0 .--> j is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{0} --> j is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {j} -valued non empty Function-like constant total V32({0},{j}) finite Element of K48(K49({0},{j}))
{j} is non empty finite set
K49({0},{j}) is Relation-like finite set
K48(K49({0},{j})) is finite V39() set
stop K262(SCM+FSA,j) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((Macro i),(Macro j)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
stop (Macro i) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
K224((Macro i),(Stop SCM+FSA)) is Relation-like T-Sequence-like Function-like set
CutLastLoc (stop (Macro i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
((CutLastLoc (stop (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
card (CutLastLoc (stop (Macro i))) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
((CutLastLoc (stop (Macro i))),(card (CutLastLoc (stop (Macro i))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite halt-free set
goto (card (CutLastLoc (stop (Macro i)))) is non ins-loc-free V59( the InstructionsF of SCM+FSA) V92(3, SCM+FSA ) with_explicit_jumps IC-relocable V142(3, SCM+FSA ) V144(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K457((card (CutLastLoc (stop (Macro i))))) is Element of the InstructionsF of K451()
(CutLastLoc (stop (Macro i))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like Function-like set
(halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like the InstructionsF of SCM+FSA -defined {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued V17() Function-like one-to-one constant finite set
{(halt SCM+FSA)} --> (goto (card (CutLastLoc (stop (Macro i))))) is Relation-like {(halt SCM+FSA)} -defined the InstructionsF of SCM+FSA -valued {(goto (card (CutLastLoc (stop (Macro i)))))} -valued non empty Function-like constant total V32({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) finite Element of K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}))
{(goto (card (CutLastLoc (stop (Macro i)))))} is non empty finite set
K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))}) is Relation-like finite set
K48(K49({(halt SCM+FSA)},{(goto (card (CutLastLoc (stop (Macro i)))))})) is finite V39() set
(CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(CutLastLoc (stop (Macro i))) +* ((CutLastLoc (stop (Macro i))) (#) ((halt SCM+FSA) .--> (goto (card (CutLastLoc (stop (Macro i))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro i) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
Reloc ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro j),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite initial set
Shift ((IncAddr ((Macro j),(card (Macro i)))),(card (Macro i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like finite set
((CutLastLoc (stop (Macro i)))) +* (Reloc ((Macro j),(card (Macro i)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (i,j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
card (Macro j) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card (Macro i)) + (card (Macro j)) is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
(card (Macro i)) + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT
2 + 2 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT