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

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

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