:: SCMISORT semantic presentation

REAL is non empty V5() V51() V53() set
NAT is non empty V5() epsilon-transitive epsilon-connected ordinal V51() V53() countable denumerable Element of K32(REAL)
K32(REAL) is cup-closed diff-closed preBoolean set
SCM+FSA is non empty with_non-empty_values IC-Ins-separated strict V108(3) with_explicit_jumps IC-relocable V157(3) AMI-Struct over 3
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
K571() is set
K589(NAT,K571()) is Element of K571()
K564() is non empty set
K574() is Relation-like K571() -defined 3 -valued Function-like total V18(K571(),3) Element of K32(K33(K571(),3))
K33(K571(),3) is Relation-like set
K32(K33(K571(),3)) is cup-closed diff-closed preBoolean set
K575() is non empty Relation-like 3 -defined Function-like total set
K582() is non empty Relation-like K564() -defined K99((product (K574() (#) K575())),(product (K574() (#) K575()))) -valued Function-like total V18(K564(),K99((product (K574() (#) K575())),(product (K574() (#) K575())))) Function-yielding V151() Element of K32(K33(K564(),K99((product (K574() (#) K575())),(product (K574() (#) K575())))))
K574() (#) K575() is Relation-like K571() -defined Function-like total set
product (K574() (#) K575()) is functional with_common_domain product-like set
K99((product (K574() (#) K575())),(product (K574() (#) K575()))) is non empty functional set
K33(K564(),K99((product (K574() (#) K575())),(product (K574() (#) K575())))) is Relation-like set
K32(K33(K564(),K99((product (K574() (#) K575())),(product (K574() (#) K575()))))) is cup-closed diff-closed preBoolean set
AMI-Struct(# K571(),K589(NAT,K571()),K564(),K574(),K575(),K582() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
RAT is non empty V5() V51() V53() set
COMPLEX is non empty V5() V51() V53() set
NAT is non empty V5() epsilon-transitive epsilon-connected ordinal V51() V53() countable denumerable set
K32(NAT) is cup-closed diff-closed preBoolean set
K32(NAT) is cup-closed diff-closed preBoolean set
9 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Segm 9 is countable Element of K32(NAT)
Int-Locations is non empty set
K350() is set
K32(K350()) is cup-closed diff-closed preBoolean set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
K33(K350(),2) is Relation-like set
K32(K33(K350(),2)) is cup-closed diff-closed preBoolean set
K352() is Relation-like K350() -defined 2 -valued Function-like total V18(K350(),2) Element of K32(K33(K350(),2))
K353() is non empty Relation-like 2 -defined Function-like total set
K352() (#) K353() is Relation-like K350() -defined Function-like total set
product (K352() (#) K353()) is functional with_common_domain product-like set
K344() is non empty set
K99((product (K352() (#) K353())),(product (K352() (#) K353()))) is non empty functional set
K33(K344(),K99((product (K352() (#) K353())),(product (K352() (#) K353())))) is Relation-like set
K32(K33(K344(),K99((product (K352() (#) K353())),(product (K352() (#) K353()))))) is cup-closed diff-closed preBoolean set
K32( the carrier of SCM+FSA) is cup-closed diff-closed preBoolean set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V97() J/A-independent V100() set
INT is non empty V5() V51() V53() set
the_Values_of SCM+FSA is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is non empty Relation-like the carrier of SCM+FSA -defined 3 -valued Function-like total V18( the carrier of SCM+FSA,3) Element of K32(K33( the carrier of SCM+FSA,3))
K33( the carrier of SCM+FSA,3) is Relation-like set
K32(K33( the carrier of SCM+FSA,3)) is cup-closed diff-closed preBoolean set
the ValuesF of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA is non empty Relation-like the carrier of SCM+FSA -defined Function-like total set
Int-Locations is non empty Element of K32( the carrier of SCM+FSA)
K32(Int-Locations) is cup-closed diff-closed preBoolean set
K33(NAT,K32(NAT)) is Relation-like set
K32(K33(NAT,K32(NAT))) is cup-closed diff-closed preBoolean set
FinPartSt SCM+FSA is non empty functional Element of K32((sproduct (the_Values_of SCM+FSA)))
sproduct (the_Values_of SCM+FSA) is non empty functional set
K32((sproduct (the_Values_of SCM+FSA))) is cup-closed diff-closed preBoolean set
{ b₁ where b₁ is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible Element of sproduct (the_Values_of SCM+FSA) : b₁ is V53() } is set
K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is cup-closed diff-closed preBoolean set
product (the_Values_of SCM+FSA) is non empty functional with_common_domain product-like set
K33(NAT,(product (the_Values_of SCM+FSA))) is Relation-like set
K32(K33(NAT,(product (the_Values_of SCM+FSA)))) is cup-closed diff-closed preBoolean set
K563() is set
K32(K571()) is cup-closed diff-closed preBoolean set
Fin Int-Locations is non empty cup-closed diff-closed preBoolean set
FinSeq-Locations is non empty V5() V51() V53() Element of K32( the carrier of SCM+FSA)
K573() is Element of K32(K571())
Fin FinSeq-Locations is non empty cup-closed diff-closed preBoolean set
K32(FinSeq-Locations) is cup-closed diff-closed preBoolean set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V40() V41() integer V53() V54() V57() Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V151() set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V40() V41() integer V53() V54() V57() Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V151() Element of NAT
K33( the InstructionsF of SCM+FSA,(Fin Int-Locations)) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,(Fin Int-Locations))) is cup-closed diff-closed preBoolean set
halt SCM+FSA is ins-loc-free V107(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(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
K33( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations))) is cup-closed diff-closed preBoolean set
4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
10 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
7 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
8 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
11 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
IC is V74( SCM+FSA ) Element of the carrier of SCM+FSA
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K32( the carrier of SCM+FSA)
intloc 0 is V111() read-only Element of the carrier of SCM+FSA
goto 2 is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V53() countable V95() non halt-free V104( SCM+FSA ) V105( SCM+FSA ) InitClosed InitHalting keepInt0_1 good V159(3, SCM+FSA ) set
K303((halt SCM+FSA)) is set
K555((intloc 0),1) is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant the_Values_of SCM+FSA -compatible V38() V39() V40() V41() V42() V43() V44() non-increasing V53() countable data-only set
{(intloc 0)} is non empty V53() countable set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant total V18({(intloc 0)},{1}) V38() V39() V40() V41() V53() countable Element of K32(K33({(intloc 0)},{1}))
{1} is non empty V50() V51() V53() countable set
K33({(intloc 0)},{1}) is Relation-like V53() countable set
K32(K33({(intloc 0)},{1})) is cup-closed diff-closed preBoolean V53() V57() countable set
Initialize K555((intloc 0),1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V53() countable 0 -started set
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V53() countable 0 -started set
(IC ) .--> 0 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V38() V39() V40() V41() V42() V43() V44() non-increasing V53() countable Function-yielding V151() set
{(IC )} is non empty V53() countable set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant total V18({(IC )},{0}) V38() V39() V40() V41() V53() countable Function-yielding V151() Element of K32(K33({(IC )},{0}))
{0} is non empty functional V53() V57() with_common_domain countable set
K33({(IC )},{0}) is Relation-like V53() countable set
K32(K33({(IC )},{0})) is cup-closed diff-closed preBoolean V53() V57() countable set
K555((intloc 0),1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible V53() countable 0 -started set
12 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Goto 0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() halt-free V105( SCM+FSA ) good set
goto 0 is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
goto 3 is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K81(NAT,0,1) is non empty V53() countable Element of K32(NAT)
K351() is non empty Element of K32(K350())
(intloc 0) .--> 1 is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant the_Values_of SCM+FSA -compatible V38() V39() V40() V41() V42() V43() V44() non-increasing V53() countable data-only set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V53() countable 0 -started set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible V53() countable 0 -started set
dom (Initialize ((intloc 0) .--> 1)) is V53() countable set
K81( the carrier of SCM+FSA,(intloc 0),(IC )) is non empty V53() countable Element of K32( the carrier of SCM+FSA)
Sorting-Function is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Function-yielding V151() Element of K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)))
dom Sorting-Function is set
fsloc 0 is FinSeq-Location
0 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
- (0 + 1) is ext-real non positive V36() V37() integer set
a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
dom a0 is V53() countable V132() set
UsedIntLoc a0 is V53() countable Element of K32(Int-Locations)
a1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
a0 . a1 is set
a2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedIntLoc a2 is V53() countable Element of Fin Int-Locations
a1 .--> a2 is V5() Relation-like NAT -defined {a1} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V53() countable set
{a1} is non empty V53() countable set
{a1} --> a2 is non empty Relation-like {a1} -defined the InstructionsF of SCM+FSA -valued {a2} -valued Function-like constant total V18({a1},{a2}) V53() countable Element of K32(K33({a1},{a2}))
{a2} is non empty V53() countable set
K33({a1},{a2}) is Relation-like V53() countable set
K32(K33({a1},{a2})) is cup-closed diff-closed preBoolean V53() V57() countable set
a0 +* (a1 .--> a2) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
UsedIntLoc (a0 +* (a1 .--> a2)) is V53() countable Element of K32(Int-Locations)
a4 is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of K32(K33( the InstructionsF of SCM+FSA,(Fin Int-Locations)))
a0 (#) a4 is Relation-like NAT -defined Fin Int-Locations -valued Function-like V53() countable set
Union (a0 (#) a4) is set
rng (a0 (#) a4) is V53() countable set
union (rng (a0 (#) a4)) is set
(a0 +* (a1 .--> a2)) (#) a4 is Relation-like NAT -defined Fin Int-Locations -valued Function-like V53() countable set
initializeWorkMem is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like total V18( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of K32(K33( the InstructionsF of SCM+FSA,(Fin Int-Locations)))
(a0 +* (a1 .--> a2)) (#) initializeWorkMem is Relation-like NAT -defined Fin Int-Locations -valued Function-like V53() countable set
Union ((a0 +* (a1 .--> a2)) (#) initializeWorkMem) is set
rng ((a0 +* (a1 .--> a2)) (#) initializeWorkMem) is V53() countable set
union (rng ((a0 +* (a1 .--> a2)) (#) initializeWorkMem)) is set
f0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a4 . f0 is V53() countable Element of Fin Int-Locations
initializeWorkMem . f0 is V53() countable Element of Fin Int-Locations
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedIntLoc b1 is V53() countable Element of Fin Int-Locations
(a0 +* (a1 .--> a2)) . a1 is set
a0 +* (a1,a2) is Relation-like Function-like set
(a0 +* (a1,a2)) . a1 is set
dom a4 is non empty set
rng a0 is V53() countable set
dom (a0 (#) a4) is V53() countable V132() set
dom (a0 +* (a1 .--> a2)) is V53() countable V132() set
rng (a0 +* (a1 .--> a2)) is V53() countable set
dom ((a0 +* (a1 .--> a2)) (#) a4) is V53() countable V132() set
f0 is set
(a0 +* (a1 .--> a2)) . f0 is set
dom (a1 .--> a2) is V5() V53() countable V132() set
a0 . f0 is set
(a0 (#) a4) . f0 is set
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a4 . b1 is V53() countable Element of Fin Int-Locations
((a0 +* (a1 .--> a2)) (#) a4) . f0 is set
(a0 (#) a4) . f0 is set
a0 . f0 is set
a4 . (a0 . f0) is set
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedIntLoc b1 is V53() countable Element of Fin Int-Locations
a4 . b1 is V53() countable Element of Fin Int-Locations
((a0 +* (a1 .--> a2)) (#) a4) . f0 is set
b2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedIntLoc b2 is V53() countable Element of Fin Int-Locations
a0 is V111() Element of the carrier of SCM+FSA
a1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a1 ";" (Goto 0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
if>0 (a0,(a1 ";" (Goto 0)),(Stop SCM+FSA)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
card a1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card a1) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
(if>0 (a0,(a1 ";" (Goto 0)),(Stop SCM+FSA))) . ((card a1) + 4) is set
goto ((card a1) + 4) is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
card (Stop SCM+FSA) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card (Stop SCM+FSA)) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
a0 >0_goto ((card (Stop SCM+FSA)) + 3) is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() good set
card (a1 ";" (Goto 0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card (a1 ";" (Goto 0))) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Goto ((card (a1 ";" (Goto 0))) + 1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() halt-free V105( SCM+FSA ) good set
((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() good set
(((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
(Goto 0) ";" (Stop SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() non halt-free good set
(card a1) + 6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
card (if>0 (a0,(a1 ";" (Goto 0)),(Stop SCM+FSA))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
dom (if>0 (a0,(a1 ";" (Goto 0)),(Stop SCM+FSA))) is non empty V53() countable V132() set
0 + ((card a1) + 4) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
(Goto 0) . 0 is set
dom (Goto 0) is non empty V53() countable V132() set
((Goto 0) ";" (Stop SCM+FSA)) . 0 is set
Directed (Goto 0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() halt-free V105( SCM+FSA ) good set
(Directed (Goto 0)) . 0 is set
card ((Goto 0) ";" (Stop SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
card (Goto 0) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card (Goto 0)) + (card (Stop SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
1 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
dom ((Goto 0) ";" (Stop SCM+FSA)) is non empty V53() countable V132() set
{ (b₁ + ((card a1) + 4)) where b₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT : b₁ in dom ((Goto 0) ";" (Stop SCM+FSA)) } is set
Shift (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
dom (Shift (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) is non empty V53() countable V132() set
(Shift (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) /. ((card a1) + 4) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Shift (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) . (0 + ((card a1) + 4)) is set
card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
card (((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card (((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1)))) + (card a1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
card ((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
card (Goto ((card (a1 ";" (Goto 0))) + 1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card ((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA))) + (card (Goto ((card (a1 ";" (Goto 0))) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
((card ((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA))) + (card (Goto ((card (a1 ";" (Goto 0))) + 1)))) + (card a1) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card ((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA))) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
((card ((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA))) + 1) + (card a1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
(2 + 1) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
((2 + 1) + 1) + (card a1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
dom ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) is non empty V53() countable V132() set
Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable non halt-free set
IncAddr (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
Shift ((IncAddr (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))),((card a1) + 4)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
IncAddr ((Shift (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))),((card a1) + 4)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
stop ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
K293(((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1),(Stop SCM+FSA)) is Relation-like Function-like T-Sequence-like set
CutLastLoc (stop ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
(((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" (a1 ";" (Goto 0)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" (a1 ";" (Goto 0))) ";" (Stop SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() non halt-free set
((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) ";" (Goto 0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
(((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) ";" (Goto 0)) ";" (Stop SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() non halt-free set
((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) ";" ((Goto 0) ";" (Stop SCM+FSA)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() non halt-free set
Directed ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() halt-free V105( SCM+FSA ) set
(Directed ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)) +* (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V53() countable non halt-free set
dom (Directed ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)) is non empty V53() countable V132() set
dom (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) is V53() countable V132() set
(dom (Directed ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1))) \/ (dom (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)))) is non empty V53() countable set
Directed (((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1),(card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() halt-free set
dom (Directed (((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1),(card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)))) is V53() countable V132() set
(dom (Directed (((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1),(card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1))))) \/ (dom (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)))) is V53() countable set
goto (card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)) is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) +~ ((halt SCM+FSA),(goto (card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)))) is Relation-like Function-like set
dom (((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) +~ ((halt SCM+FSA),(goto (card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1))))) is set
(dom (((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1) +~ ((halt SCM+FSA),(goto (card ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)))))) \/ (dom (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)))) is set
(dom ((((a0 >0_goto ((card (Stop SCM+FSA)) + 3)) ";" (Stop SCM+FSA)) ";" (Goto ((card (a1 ";" (Goto 0))) + 1))) ";" a1)) \/ (dom (Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4)))) is non empty V53() countable set
(Reloc (((Goto 0) ";" (Stop SCM+FSA)),((card a1) + 4))) . ((card a1) + 4) is set
IncAddr ((goto 0),((card a1) + 4)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
dom a0 is V53() countable V132() set
UsedInt*Loc a0 is V53() countable Element of K32(FinSeq-Locations)
a1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
a0 . a1 is set
a2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedInt*Loc a2 is V53() countable Element of Fin FinSeq-Locations
a1 .--> a2 is V5() Relation-like NAT -defined {a1} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V53() countable set
{a1} is non empty V53() countable set
{a1} --> a2 is non empty Relation-like {a1} -defined the InstructionsF of SCM+FSA -valued {a2} -valued Function-like constant total V18({a1},{a2}) V53() countable Element of K32(K33({a1},{a2}))
{a2} is non empty V53() countable set
K33({a1},{a2}) is Relation-like V53() countable set
K32(K33({a1},{a2})) is cup-closed diff-closed preBoolean V53() V57() countable set
a0 +* (a1 .--> a2) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
UsedInt*Loc (a0 +* (a1 .--> a2)) is V53() countable Element of K32(FinSeq-Locations)
a4 is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of K32(K33( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)))
a0 (#) a4 is Relation-like NAT -defined Fin FinSeq-Locations -valued Function-like V53() countable set
Union (a0 (#) a4) is set
rng (a0 (#) a4) is V53() countable set
union (rng (a0 (#) a4)) is set
(a0 +* (a1 .--> a2)) (#) a4 is Relation-like NAT -defined Fin FinSeq-Locations -valued Function-like V53() countable set
initializeWorkMem is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like total V18( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of K32(K33( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)))
(a0 +* (a1 .--> a2)) (#) initializeWorkMem is Relation-like NAT -defined Fin FinSeq-Locations -valued Function-like V53() countable set
Union ((a0 +* (a1 .--> a2)) (#) initializeWorkMem) is set
rng ((a0 +* (a1 .--> a2)) (#) initializeWorkMem) is V53() countable set
union (rng ((a0 +* (a1 .--> a2)) (#) initializeWorkMem)) is set
f0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a4 . f0 is V53() countable Element of Fin FinSeq-Locations
initializeWorkMem . f0 is V53() countable Element of Fin FinSeq-Locations
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedInt*Loc b1 is V53() countable Element of Fin FinSeq-Locations
(a0 +* (a1 .--> a2)) . a1 is set
a0 +* (a1,a2) is Relation-like Function-like set
(a0 +* (a1,a2)) . a1 is set
dom a4 is non empty set
rng a0 is V53() countable set
dom (a0 (#) a4) is V53() countable V132() set
dom (a0 +* (a1 .--> a2)) is V53() countable V132() set
rng (a0 +* (a1 .--> a2)) is V53() countable set
dom ((a0 +* (a1 .--> a2)) (#) a4) is V53() countable V132() set
f0 is set
(a0 +* (a1 .--> a2)) . f0 is set
dom (a1 .--> a2) is V5() V53() countable V132() set
a0 . f0 is set
(a0 (#) a4) . f0 is set
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a4 . b1 is V53() countable Element of Fin FinSeq-Locations
((a0 +* (a1 .--> a2)) (#) a4) . f0 is set
(a0 (#) a4) . f0 is set
a0 . f0 is set
a4 . (a0 . f0) is set
b1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedInt*Loc b1 is V53() countable Element of Fin FinSeq-Locations
a4 . b1 is V53() countable Element of Fin FinSeq-Locations
((a0 +* (a1 .--> a2)) (#) a4) . f0 is set
b2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
UsedInt*Loc b2 is V53() countable Element of Fin FinSeq-Locations
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a2 is V111() Element of the carrier of SCM+FSA
a1 is V111() Element of the carrier of SCM+FSA
while>0 (a1,a0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
card a0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card a0) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
((card a0) + 4) .--> (goto 0) is V5() Relation-like NAT -defined {((card a0) + 4)} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V53() countable set
{((card a0) + 4)} is non empty V50() V51() V53() countable set
{((card a0) + 4)} --> (goto 0) is non empty Relation-like {((card a0) + 4)} -defined the InstructionsF of SCM+FSA -valued {(goto 0)} -valued Function-like constant total V18({((card a0) + 4)},{(goto 0)}) V53() countable Element of K32(K33({((card a0) + 4)},{(goto 0)}))
{(goto 0)} is non empty V53() countable set
K33({((card a0) + 4)},{(goto 0)}) is Relation-like V53() countable set
K32(K33({((card a0) + 4)},{(goto 0)})) is cup-closed diff-closed preBoolean V53() V57() countable set
a0 ";" (Goto 0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
if>0 (a1,(a0 ";" (Goto 0)),(Stop SCM+FSA)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
(if>0 (a1,(a0 ";" (Goto 0)),(Stop SCM+FSA))) +* (((card a0) + 4) .--> (goto 0)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a1 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Initialize (Initialized a1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
IExec (a2,a0,a1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan ((a0 +* a2),(Initialize (Initialized a1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput ((a0 +* a2),(Initialize (Initialized a1)),(LifeSpan ((a0 +* a2),(Initialize (Initialized a1))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
initializeWorkMem is V111() Element of the carrier of SCM+FSA
(IExec (a2,a0,a1)) . initializeWorkMem is ext-real V36() V37() integer set
Result ((a0 +* a2),(Initialize (Initialized a1))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(Result ((a0 +* a2),(Initialize (Initialized a1)))) . initializeWorkMem is ext-real V36() V37() integer set
(Comput ((a0 +* a2),(Initialize (Initialized a1)),(LifeSpan ((a0 +* a2),(Initialize (Initialized a1)))))) . initializeWorkMem is ext-real V36() V37() integer set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
a3 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() InitClosed InitHalting set
a4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput (a0,a2,a4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (a0,a2,a4)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a0,a2,a4)) . (IC ) is set
dom a3 is non empty V53() countable V132() set
Comput (a1,a2,a4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (a1,a2,a4)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a1,a2,a4)) . (IC ) is set
a5 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput (a1,a2,a5) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (a1,a2,a5)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a1,a2,a5)) . (IC ) is set
CurInstr (a1,(Comput (a1,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a1 /. (IC (Comput (a1,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a1 . (IC (Comput (a1,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a3 . (IC (Comput (a1,a2,a4))) is set
a0 . (IC (Comput (a0,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (a0,(Comput (a0,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a0 /. (IC (Comput (a0,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a2 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
LifeSpan (a0,a2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
LifeSpan (a1,a2) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Result (a0,a2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Result (a1,a2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
a3 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() InitClosed InitHalting set
a4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput (a1,a2,a4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (a1,(Comput (a1,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (a1,a2,a4)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a1,a2,a4)) . (IC ) is set
a1 /. (IC (Comput (a1,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (a0,a2,a4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (a0,(Comput (a0,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (a0,a2,a4)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a0,a2,a4)) . (IC ) is set
a0 /. (IC (Comput (a0,a2,a4))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (a1,a2,(LifeSpan (a0,a2))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (a1,(Comput (a1,a2,(LifeSpan (a0,a2))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (a1,a2,(LifeSpan (a0,a2)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a1,a2,(LifeSpan (a0,a2)))) . (IC ) is set
a1 /. (IC (Comput (a1,a2,(LifeSpan (a0,a2))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (a0,a2,(LifeSpan (a0,a2))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (a0,(Comput (a0,a2,(LifeSpan (a0,a2))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (a0,a2,(LifeSpan (a0,a2)))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput (a0,a2,(LifeSpan (a0,a2)))) . (IC ) is set
a0 /. (IC (Comput (a0,a2,(LifeSpan (a0,a2))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a3 is V111() non read-only Element of the carrier of SCM+FSA
a1 . a3 is ext-real V36() V37() integer set
while>0 (a3,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
Initialized a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a1 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) . a3 is ext-real V36() V37() integer set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is V111() Element of the carrier of SCM+FSA
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
while>0 (a1,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* (while>0 (a1,a2)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a4 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a4 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a4 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
LifeSpan ((a0 +* a2),(Initialized a4)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
a5 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
1 + a5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),(1 + a5)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),(1 + a5))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),(1 + a5))) . (IC ) is set
Comput ((a0 +* a2),(Initialized a4),a5) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialized a4),a5)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialized a4),a5)) . (IC ) is set
(IC (Comput ((a0 +* a2),(Initialized a4),a5))) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
DataPart (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),(1 + a5))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),(1 + a5))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput ((a0 +* a2),(Initialized a4),a5)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* a2),(Initialized a4),a5)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(1 + a5) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),((1 + a5) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),((1 + a5) + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),((1 + a5) + 1))) . (IC ) is set
a5 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* a2),(Initialized a4),(a5 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialized a4),(a5 + 1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialized a4),(a5 + 1))) . (IC ) is set
(IC (Comput ((a0 +* a2),(Initialized a4),(a5 + 1)))) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
DataPart (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),((1 + a5) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a4),((1 + a5) + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput ((a0 +* a2),(Initialized a4),(a5 + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* a2),(Initialized a4),(a5 + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (Initialized a4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a4) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is V111() Element of the carrier of SCM+FSA
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
while>0 (a1,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* (while>0 (a1,a2)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
card a2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card a2) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
goto ((card a2) + 4) is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
a3 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a3 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a3 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
LifeSpan ((a0 +* a2),(Initialized a3)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
1 + (LifeSpan ((a0 +* a2),(Initialized a3))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* (while>0 (a1,a2))),(Initialized a3),(1 + (LifeSpan ((a0 +* a2),(Initialized a3))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a3),(1 + (LifeSpan ((a0 +* a2),(Initialized a3)))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a3),(1 + (LifeSpan ((a0 +* a2),(Initialized a3)))))) . (IC ) is set
Comput ((a0 +* a2),(Initialized a3),(LifeSpan ((a0 +* a2),(Initialized a3)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialized a3),(LifeSpan ((a0 +* a2),(Initialized a3))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialized a3),(LifeSpan ((a0 +* a2),(Initialized a3))))) . (IC ) is set
(IC (Comput ((a0 +* a2),(Initialized a3),(LifeSpan ((a0 +* a2),(Initialized a3)))))) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
CurInstr ((a0 +* (while>0 (a1,a2))),(Comput ((a0 +* (while>0 (a1,a2))),(Initialized a3),(1 + (LifeSpan ((a0 +* a2),(Initialized a3))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(a0 +* (while>0 (a1,a2))) /. (IC (Comput ((a0 +* (while>0 (a1,a2))),(Initialized a3),(1 + (LifeSpan ((a0 +* a2),(Initialized a3))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Initialize (Initialized a3) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a3) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a1 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan ((a0 +* a2),(Initialized a1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(LifeSpan ((a0 +* a2),(Initialized a1))) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
a3 is V111() non read-only Element of the carrier of SCM+FSA
a1 . a3 is ext-real V36() V37() integer set
while>0 (a3,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* (while>0 (a3,a2)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) . (IC ) is set
dom (while>0 (a3,a2)) is non empty V53() countable V132() set
Initialize (Initialized a1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) . a3 is ext-real V36() V37() integer set
b1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),b1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),b1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),b1)) . (IC ) is set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a1 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan ((a0 +* a2),(Initialized a1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(LifeSpan ((a0 +* a2),(Initialized a1))) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
a3 is V111() non read-only Element of the carrier of SCM+FSA
a1 . a3 is ext-real V36() V37() integer set
while>0 (a3,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* (while>0 (a3,a2)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom (while>0 (a3,a2)) is non empty V53() countable V132() set
Initialize (Initialized a1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
dom a2 is non empty V53() countable V132() set
a6 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput ((a0 +* a2),(Initialize (Initialized a1)),a6) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialize (Initialized a1)),a6)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialize (Initialized a1)),a6)) . (IC ) is set
(Initialized a1) . a3 is ext-real V36() V37() integer set
a6 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),a6) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),a6)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),a6)) . (IC ) is set
a0 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized a1 is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
a1 +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* a2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan ((a0 +* a2),(Initialized a1)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(LifeSpan ((a0 +* a2),(Initialized a1))) + 3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* a2),(Initialized a1),(LifeSpan ((a0 +* a2),(Initialized a1)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput ((a0 +* a2),(Initialized a1),(LifeSpan ((a0 +* a2),(Initialized a1))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* a2),(Initialized a1),(LifeSpan ((a0 +* a2),(Initialized a1))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
a3 is V111() non read-only Element of the carrier of SCM+FSA
a1 . a3 is ext-real V36() V37() integer set
while>0 (a3,a2) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V53() countable V95() set
a0 +* (while>0 (a3,a2)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) . (IC ) is set
DataPart (Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((a0 +* (while>0 (a3,a2))),(Initialized a1),((LifeSpan ((a0 +* a2),(Initialized a1))) + 3))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (Initialized a1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized a1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Comput ((a0 +* (while>0 (a3,a2))),(Initialize (Initialized a1)),1) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
a3 >0_goto 4 is non ins-loc-free V101( the InstructionsF of SCM+FSA) V107(3, SCM+FSA ) good with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
LifeSpan ((a0 +* a2),(Initialize (Initialized a1))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
card a2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(card a2) + 4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
1 + (LifeSpan ((a0 +* a2),(Initialize (Initialized a1)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
(1 + (LifeSpan ((a0 +* a2),(Initialize (Initialized a1))))) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* (while>0 (a3,a2))),(Initialize (Initialized a1)),((1 + (LifeSpan ((a0 +* a2),(Initialize (Initialized a1))))) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
dom (while>0 (a3,a2)) is non empty V53() countable V132() set
dom a2 is non empty V53() countable V132() set
b5 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
Comput ((a0 +* a2),(Initialize (Initialized a1)),b5) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialize (Initialized a1)),b5)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialize (Initialized a1)),b5)) . (IC ) is set
b5 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
1 + b5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V50() Element of NAT
Comput ((a0 +* (while>0 (a3,a2))),(Initialize (Initialized a1)),(1 + b5)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* (while>0 (a3,a2))),(Initialize (Initialized a1)),(1 + b5))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* (while>0 (a3,a2))),(Initialize (Initialized a1)),(1 + b5))) . (IC ) is set
Comput ((a0 +* a2),(Initialize (Initialized a1)),b5) is non empty Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((a0 +* a2),(Initialize (Initialized a1)),b5)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT
(Comput ((a0 +* a2),(Initialize (Initialized a1)),b5)) . (IC ) is set
(IC (Comput ((a0 +* a2),(Initialize (Initialized