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
{ b1 where b1 is Element of K280((the_Values_of SCM+FSA)) : b1 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
{ (b1 + (card i)) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b1 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) \/ { (b1 + (card i)) where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real V27() V28() integer Element of NAT : b1 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