:: SCMFSA_9 semantic presentation

REAL is non empty V20() V33() V45() set

NAT is epsilon-transitive epsilon-connected ordinal non empty V20() V33() V45() countable denumerable Element of K43(REAL)

K43(REAL) is set

SCM+FSA is V63() with_non-empty_values IC-Ins-separated strict V91(3) with_explicit_jumps IC-relocable V146(3) AMI-Struct over 3

3 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

the U2 of SCM+FSA is set

NAT is epsilon-transitive epsilon-connected ordinal non empty V20() V33() V45() countable denumerable set

K43(NAT) is set

K43(NAT) is set

9 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

Segm 9 is countable Element of K43(NAT)

Int-Locations is non empty set

K258() is set

K43(K258()) is set

2 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

K44(K258(),2) is Relation-like set

K43(K44(K258(),2)) is set

K260() is Relation-like K258() -defined 2 -valued Function-like total V30(K258(),2) Element of K43(K44(K258(),2))

K261() is Relation-like 2 -defined non empty Function-like total set

K260() (#) K261() is Relation-like K258() -defined Function-like set

product (K260() (#) K261()) is functional with_common_domain product-like set

K252() is non empty set

K97((product (K260() (#) K261())),(product (K260() (#) K261()))) is non empty functional set

K44(K252(),K97((product (K260() (#) K261())),(product (K260() (#) K261())))) is Relation-like set

K43(K44(K252(),K97((product (K260() (#) K261())),(product (K260() (#) K261()))))) is set

K43( the U2 of SCM+FSA) is set

the InstructionsF of SCM+FSA is Relation-like non empty standard-ins V53() J/A-independent V56() set

INT is non empty V20() V33() V45() set

Int-Locations is non empty Element of K43( the U2 of SCM+FSA)

K295(Int-Locations) is V98() set

K43(Int-Locations) is set

FinSeq-Locations is non empty V20() V33() V45() Element of K43( the U2 of SCM+FSA)

K295(FinSeq-Locations) is V98() set

K43(FinSeq-Locations) 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 total V30( the U2 of SCM+FSA,3) Element of K43(K44( the U2 of SCM+FSA,3))

K44( the U2 of SCM+FSA,3) is Relation-like set

K43(K44( the U2 of SCM+FSA,3)) is set

the ValuesF of SCM+FSA is Relation-like 3 -defined non empty 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

COMPLEX is non empty V20() V33() V45() set

RAT is non empty V20() V33() V45() set

K44(NAT,K43(NAT)) is Relation-like set

K43(K44(NAT,K43(NAT))) is set

FinPartSt SCM+FSA is non empty functional Element of K43((sproduct (the_Values_of SCM+FSA)))

sproduct (the_Values_of SCM+FSA) is non empty functional set

K43((sproduct (the_Values_of SCM+FSA))) is set

{ b

K44((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set

K43(K44((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set

1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

{} is ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V27() V28() V33() V34() V37() V41() V42() V43() initial Cardinal-yielding countable V104() V106() V107() V108() V109() Function-yielding V140() set

0 is ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined RAT -valued epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty Function-like one-to-one constant functional V27() V28() V33() V34() V37() V41() V42() V43() initial Cardinal-yielding countable V104() V106() V107() V108() V109() Function-yielding V140() Element of NAT

IC is Element of the U2 of SCM+FSA

halt SCM+FSA is ins-loc-free V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(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

K26(0,{},{}) is set

goto 2 is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

intloc 0 is V94() read-only Element of the U2 of SCM+FSA

Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued T-Sequence-like non empty V20() Function-like constant V33() initial non halt-free V60( SCM+FSA ) V61( SCM+FSA ) countable keeping_0 good V148(3, SCM+FSA ) paraclosed parahalting set

K179((halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() 1 -element initial countable set

0 .--> (halt SCM+FSA) is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{0} is non empty functional V33() V37() with_common_domain countable 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 V30({0},{(halt SCM+FSA)}) V33() countable Element of K43(K44({0},{(halt SCM+FSA)}))

{(halt SCM+FSA)} is non empty V33() countable set

K44({0},{(halt SCM+FSA)}) is Relation-like V33() countable set

K43(K44({0},{(halt SCM+FSA)})) is V33() V37() countable set

4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

K482(NAT,0,1) is non empty V33() countable Element of K43(NAT)

card (Stop SCM+FSA) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (Stop SCM+FSA) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V20() V27() V28() V33() V44() countable V104() V121() set

(Stop SCM+FSA) . 0 is set

dom (Stop SCM+FSA) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V20() V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

Start-At (0,SCM+FSA) is Relation-like the U2 of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() countable 0 -started set

(IC ) .--> 0 is Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued V20() Function-like one-to-one constant V33() countable V106() V107() V108() V109() V110() V111() V112() V113() Function-yielding V140() set

{(IC )} is non empty V33() countable set

{(IC )} --> 0 is Relation-like {(IC )} -defined NAT -valued INT -valued RAT -valued {0} -valued non empty Function-like constant total V30({(IC )},{0}) V33() countable V106() V107() V108() V109() Function-yielding V140() Element of K43(K44({(IC )},{0}))

K44({(IC )},{0}) is Relation-like V33() countable set

K43(K44({(IC )},{0})) is V33() V37() countable set

Goto 0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial halt-free V61( SCM+FSA ) countable good set

6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

(card I) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (I ";" (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (I ";" (Goto 0)) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card (I ";" (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card (I ";" (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

card (Goto 0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (Goto 0) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + (card (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

((card I) + (card (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + (card (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(card I) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 1) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + 1) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

(card I) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (I ";" (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (I ";" (Goto 0)) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card (I ";" (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card (I ";" (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

card (Goto 0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (Goto 0) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + (card (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

((card I) + (card (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + (card (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(card I) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 1) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + 1) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

I is V94() Element of the U2 of SCM+FSA

a is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

a ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop a is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(a,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop a) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop a)),(card (CutLastLoc (stop a)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop a))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop a)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop a))))) is Relation-like Function-like set

card a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom a is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card a))),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop a))) +* (Reloc ((Goto 0),(card a))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card a) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

goto 0 is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

((card a) + 4) .--> (goto 0) is Relation-like NAT -defined {((card a) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card a) + 4)} is non empty V33() V44() V45() countable set

{((card a) + 4)} --> (goto 0) is Relation-like {((card a) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card a) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card a) + 4)},{(goto 0)}))

{(goto 0)} is non empty V33() countable set

K44({((card a) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card a) + 4)},{(goto 0)})) is V33() V37() countable set

(if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) +* (((card a) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card a) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

dom (if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) +* (((card a) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card a) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card a) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if=0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)))) \/ {((card a) + 4)} is non empty V33() countable set

P1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) +* (((card a) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card a) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

dom (if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA))) +* (((card a) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card a) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card a) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if>0 (I,(a ";" (Goto 0)),(Stop SCM+FSA)))) \/ {((card a) + 4)} is non empty V33() countable set

P1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

11 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

(card I) + 11 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

1 + (card (if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(1 + (card (if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

card (I ";" (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (I ";" (Goto 0)) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card (I ";" (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card (I ";" (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card (I ";" (Goto 0))) + 1) + 4) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((((card (I ";" (Goto 0))) + 1) + 4) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

card (Goto 0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (Goto 0) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + (card (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

((card I) + (card (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + (card (Goto 0))) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((((card I) + (card (Goto 0))) + 1) + 4) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((((card I) + (card (Goto 0))) + 1) + 4) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(card I) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 1) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((card I) + 1) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((((card I) + 1) + 1) + 4) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

(((((card I) + 1) + 1) + 4) + 1) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

I is V94() Element of the U2 of SCM+FSA

a is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

a ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop a is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(a,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop a) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop a)),(card (CutLastLoc (stop a)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop a))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop a)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop a))))) is Relation-like Function-like set

card a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom a is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card a))),(card a)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop a))) +* (Reloc ((Goto 0),(card a))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card a) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card a) + 4) .--> (goto 0) is Relation-like NAT -defined {((card a) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card a) + 4)} is non empty V33() V44() V45() countable set

{((card a) + 4)} --> (goto 0) is Relation-like {((card a) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card a) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card a) + 4)},{(goto 0)}))

K44({((card a) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card a) + 4)},{(goto 0)})) is V33() V37() countable set

(if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0)))))) +* (((card a) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0)))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card a) + 11 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

dom (if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0)))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0)))))) +* (((card a) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card a) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0))))))) \/ (dom (((card a) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if=0 (I,(Stop SCM+FSA),(if>0 (I,(Stop SCM+FSA),(a ";" (Goto 0))))))) \/ {((card a) + 4)} is non empty V33() countable set

P1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

k is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

(a,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card I) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 4) .--> (goto 0) is Relation-like NAT -defined {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card I) + 4)} is non empty V33() V44() V45() countable set

{((card I) + 4)} --> (goto 0) is Relation-like {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card I) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card I) + 4)},{(goto 0)}))

K44({((card I) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card I) + 4)},{(goto 0)})) is V33() V37() countable set

(if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (a,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (a,I) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card I) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)))) \/ {((card I) + 4)} is non empty V33() countable set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + 6 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

(a,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card I) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 4) .--> (goto 0) is Relation-like NAT -defined {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card I) + 4)} is non empty V33() V44() V45() countable set

{((card I) + 4)} --> (goto 0) is Relation-like {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card I) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card I) + 4)},{(goto 0)}))

K44({((card I) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card I) + 4)},{(goto 0)})) is V33() V37() countable set

(if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (a,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (a,I) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card I) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)))) \/ (dom (((card I) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA)))) \/ {((card I) + 4)} is non empty V33() countable set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

card I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom I is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card I) + 11 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a is V94() Element of the U2 of SCM+FSA

(a,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

I ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(I,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop I)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop I)),(card (CutLastLoc (stop I)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop I))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop I)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop I))))) is Relation-like Function-like set

Reloc ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card I))),(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop I))) +* (Reloc ((Goto 0),(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card I) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card I) + 4) .--> (goto 0) is Relation-like NAT -defined {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card I) + 4)} is non empty V33() V44() V45() countable set

{((card I) + 4)} --> (goto 0) is Relation-like {((card I) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card I) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card I) + 4)},{(goto 0)}))

K44({((card I) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card I) + 4)},{(goto 0)})) is V33() V37() countable set

(if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) +* (((card I) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

card (a,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (a,I) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

card (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

dom ((if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0)))))) +* (((card I) + 4) .--> (goto 0))) is non empty V33() countable V121() set

dom (((card I) + 4) .--> (goto 0)) is V20() V33() countable V121() set

(dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))))))) \/ (dom (((card I) + 4) .--> (goto 0))) is non empty V33() countable set

(dom (if=0 (a,(Stop SCM+FSA),(if>0 (a,(Stop SCM+FSA),(I ";" (Goto 0))))))) \/ {((card I) + 4)} is non empty V33() countable set

a is V94() Element of the U2 of SCM+FSA

F is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(a,F) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

F ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop F is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(F,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop F) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop F)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop F)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop F)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop F)),(card (CutLastLoc (stop F)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop F))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop F)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop F))))) is Relation-like Function-like set

card F is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom F is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Goto 0),(card F)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

IncAddr ((Goto 0),(card F)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Goto 0),(card F))),(card F)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop F))) +* (Reloc ((Goto 0),(card F))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

if=0 (a,(F ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(card F) + 4 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

((card F) + 4) .--> (goto 0) is Relation-like NAT -defined {((card F) + 4)} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{((card F) + 4)} is non empty V33() V44() V45() countable set

{((card F) + 4)} --> (goto 0) is Relation-like {((card F) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued non empty Function-like constant total V30({((card F) + 4)},{(goto 0)}) V33() countable Element of K43(K44({((card F) + 4)},{(goto 0)}))

K44({((card F) + 4)},{(goto 0)}) is Relation-like V33() countable set

K43(K44({((card F) + 4)},{(goto 0)})) is V33() V37() countable set

(if=0 (a,(F ";" (Goto 0)),(Stop SCM+FSA))) +* (((card F) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

dom (a,F) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

(a,F) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

if>0 (a,(F ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

(if>0 (a,(F ";" (Goto 0)),(Stop SCM+FSA))) +* (((card F) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

dom (a,F) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() Element of K43(NAT)

(card (Stop SCM+FSA)) + 3 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

a =0_goto ((card (Stop SCM+FSA)) + 3) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K207(SCM+FSA,(a =0_goto ((card (Stop SCM+FSA)) + 3))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() 1 -element initial countable set

0 .--> (a =0_goto ((card (Stop SCM+FSA)) + 3)) is Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued V20() Function-like one-to-one constant V33() countable set

{0} --> (a =0_goto ((card (Stop SCM+FSA)) + 3)) is Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(a =0_goto ((card (Stop SCM+FSA)) + 3))} -valued non empty Function-like constant total V30({0},{(a =0_goto ((card (Stop SCM+FSA)) + 3))}) V33() countable Element of K43(K44({0},{(a =0_goto ((card (Stop SCM+FSA)) + 3))}))

{(a =0_goto ((card (Stop SCM+FSA)) + 3))} is non empty V33() countable set

K44({0},{(a =0_goto ((card (Stop SCM+FSA)) + 3))}) is Relation-like V33() countable set

K43(K44({0},{(a =0_goto ((card (Stop SCM+FSA)) + 3))})) is V33() V37() countable set

stop K207(SCM+FSA,(a =0_goto ((card (Stop SCM+FSA)) + 3))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(K207(SCM+FSA,(a =0_goto ((card (Stop SCM+FSA)) + 3))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

(Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) ";" (Stop SCM+FSA) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169((Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V33() countable V104() V121() set

Directed ((CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))),(card (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

goto (card (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) with_explicit_jumps IC-relocable V145(3, SCM+FSA ) V147(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))))))) is Relation-like Function-like set

card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

Reloc ((Stop SCM+FSA),(card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() non halt-free countable set

IncAddr ((Stop SCM+FSA),(card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

Shift ((IncAddr ((Stop SCM+FSA),(card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))))),(card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() countable set

(Directed (CutLastLoc (stop (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))))) +* (Reloc ((Stop SCM+FSA),(card (Macro (a =0_goto ((card (Stop SCM+FSA)) + 3)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V33() non halt-free countable set

card (F ";" (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V27() V28() V104() Element of NAT

dom (F ";" (Goto 0)) is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V33() V44() countable V104() V121() set

(card (F ";" (Goto 0))) + 1 is ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural non empty V27() V28() V44() V104() Element of NAT

Goto ((card (F ";" (Goto 0))) + 1) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial halt-free V61( SCM+FSA ) countable good set

((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (F ";" (Goto 0))) + 1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

stop ((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like non empty Function-like V33() initial countable set

K169(((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

CutLastLoc (stop ((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued T-Sequence-like Function-like V33() initial countable set

Directed (CutLastLoc (stop ((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() countable set

card (CutLastLoc (stop ((a =0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal