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

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

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

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