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
{ b1 where b1 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible Element of sproduct (the_Values_of SCM+FSA) : b1 is V33() } is set
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