:: SCMBSORT semantic presentation

REAL is non empty V12() V38() V72() set

NAT is non empty V12() epsilon-transitive epsilon-connected ordinal V38() countable denumerable V72() Element of K27(REAL)

K27(REAL) is cup-closed diff-closed preBoolean set

SCM+FSA is non empty V90(3) IC-Ins-separated strict V98(3) with_explicit_jumps IC-relocable V130(3) AMI-Struct over 3

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

K600() is set

K612(NAT,K600()) is Element of K600()

K593() is non empty set

K603() is Relation-like K600() -defined 3 -valued Function-like total V18(K600(),3) Element of K27(K28(K600(),3))

K28(K600(),3) is Relation-like set

K27(K28(K600(),3)) is cup-closed diff-closed preBoolean set

K604() is Relation-like 3 -defined Function-like non empty total set

K611() is Relation-like K593() -defined K78((product (K603() * K604())),(product (K603() * K604()))) -valued Function-like non empty total V18(K593(),K78((product (K603() * K604())),(product (K603() * K604())))) Function-yielding V102() Element of K27(K28(K593(),K78((product (K603() * K604())),(product (K603() * K604())))))

K603() * K604() is Relation-like K600() -defined Function-like total set

product (K603() * K604()) is functional with_common_domain product-like set

K78((product (K603() * K604())),(product (K603() * K604()))) is functional non empty set

K28(K593(),K78((product (K603() * K604())),(product (K603() * K604())))) is Relation-like set

K27(K28(K593(),K78((product (K603() * K604())),(product (K603() * K604()))))) is cup-closed diff-closed preBoolean set

AMI-Struct(# K600(),K612(NAT,K600()),K593(),K603(),K604(),K611() #) is strict AMI-Struct over 3

the carrier of SCM+FSA is non empty set

RAT is non empty V12() V38() V72() set

omega is non empty V12() epsilon-transitive epsilon-connected ordinal V38() countable denumerable V72() set

K27(omega) is cup-closed diff-closed preBoolean set

K27(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 V71() Element of NAT

Segm 9 is countable Element of K27(omega)

Int-Locations is non empty set

K209() is set

K27(K209()) 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 V71() Element of NAT

K28(K209(),2) is Relation-like set

K27(K28(K209(),2)) is cup-closed diff-closed preBoolean set

K211() is Relation-like K209() -defined 2 -valued Function-like total V18(K209(),2) Element of K27(K28(K209(),2))

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

K211() * K212() is Relation-like K209() -defined Function-like total set

product (K211() * K212()) is functional with_common_domain product-like set

K203() is non empty set

K78((product (K211() * K212())),(product (K211() * K212()))) is functional non empty set

K28(K203(),K78((product (K211() * K212())),(product (K211() * K212())))) is Relation-like set

K27(K28(K203(),K78((product (K211() * K212())),(product (K211() * K212()))))) is cup-closed diff-closed preBoolean set

K333() is non empty V90(2) IC-Ins-separated strict strict V98(2) AMI-Struct over 2

the InstructionsF of K333() is Relation-like non empty standard-ins V80() J/A-independent V83() set

the carrier of K333() is non empty set

K297(2,K333()) is Relation-like non-empty non empty-yielding the carrier of K333() -defined Function-like non empty total set

the Object-Kind of K333() is Relation-like the carrier of K333() -defined 2 -valued Function-like non empty total V18( the carrier of K333(),2) Element of K27(K28( the carrier of K333(),2))

K28( the carrier of K333(),2) is Relation-like set

K27(K28( the carrier of K333(),2)) is cup-closed diff-closed preBoolean set

the U7 of K333() is Relation-like 2 -defined Function-like non empty total set

the Object-Kind of K333() * the U7 of K333() is Relation-like the carrier of K333() -defined Function-like non empty total set

K27( the carrier of SCM+FSA) is cup-closed diff-closed preBoolean set

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

INT is non empty V12() V38() V72() set

Int-Locations is non empty Element of K27( the carrier of SCM+FSA)

Fin Int-Locations is non empty cup-closed diff-closed preBoolean set

K27(Int-Locations) is cup-closed diff-closed preBoolean set

FinSeq-Locations is non empty V12() V38() V72() Element of K27( the carrier of SCM+FSA)

K602() is Element of K27(K600())

K27(K600()) is cup-closed diff-closed preBoolean set

Fin FinSeq-Locations is non empty cup-closed diff-closed preBoolean set

K27(FinSeq-Locations) is cup-closed diff-closed preBoolean set

K297(3,SCM+FSA) is Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like non empty total set

the Object-Kind of SCM+FSA is Relation-like the carrier of SCM+FSA -defined 3 -valued Function-like non empty total V18( the carrier of SCM+FSA,3) Element of K27(K28( the carrier of SCM+FSA,3))

K28( the carrier of SCM+FSA,3) is Relation-like set

K27(K28( the carrier of SCM+FSA,3)) is cup-closed diff-closed preBoolean set

the U7 of SCM+FSA is Relation-like 3 -defined Function-like non empty total set

the Object-Kind of SCM+FSA * the U7 of SCM+FSA is Relation-like the carrier of SCM+FSA -defined Function-like non empty total set

COMPLEX is non empty V12() V38() V72() set

K28(NAT,K27(NAT)) is Relation-like set

K27(K28(NAT,K27(NAT))) is cup-closed diff-closed preBoolean set

FinPartSt SCM+FSA is functional non empty Element of K27((sproduct K297(3,SCM+FSA)))

sproduct K297(3,SCM+FSA) is functional non empty set

K27((sproduct K297(3,SCM+FSA))) is cup-closed diff-closed preBoolean set

{ b

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

K27(K28((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is cup-closed diff-closed preBoolean set

product K297(3,SCM+FSA) is functional non empty with_common_domain product-like set

K28(NAT,(product K297(3,SCM+FSA))) is Relation-like set

K27(K28(NAT,(product K297(3,SCM+FSA)))) is cup-closed diff-closed preBoolean set

K592() is set

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer Function-yielding V102() V109() V110() V111() V112() set

the Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer Function-yielding V102() V109() V110() V111() V112() set is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer Function-yielding V102() V109() V110() V111() V112() set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer Function-yielding V102() V109() V110() V111() V112() Element of NAT

halt SCM+FSA is ins-loc-free V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V129(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

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

UsedIntLoc (halt SCM+FSA) is V38() countable Element of Fin Int-Locations

K28( the InstructionsF of SCM+FSA,(Fin Int-Locations)) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,(Fin Int-Locations))) is cup-closed diff-closed preBoolean set

K28( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations))) is cup-closed diff-closed preBoolean set

dom {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer Function-yielding V102() V109() V110() V111() V112() set

rng {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V12() ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() V37() V38() V39() V42() FinSequence-like FinSubsequence-like FinSequence-membered Cardinal-yielding countable integer V71() Function-yielding V102() V109() V110() V111() V112() V113() V114() V115() non-increasing V138() V139() V140() V141() V143() set

4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

10 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

7 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

8 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

12 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

11 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

IC is V57( SCM+FSA ) Element of the carrier of SCM+FSA

NonZero SCM+FSA is Element of K27( the carrier of SCM+FSA)

Int-Locations \/ FinSeq-Locations is non empty Element of K27( the carrier of SCM+FSA)

goto 2 is non ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K339(2) is Element of the InstructionsF of K333()

Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant non empty V12() V38() countable V78() non halt-free V87( SCM+FSA ) V88( SCM+FSA ) InitClosed InitHalting keepInt0_1 good V132(3, SCM+FSA ) V134(3, SCM+FSA ) set

K265((halt SCM+FSA)) is set

intloc 0 is V70() read-only Element of the carrier of SCM+FSA

K342(0) is V70() Element of the carrier of K333()

K570((intloc 0),1) is 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 K297(3,SCM+FSA) -compatible V12() V38() countable data-only V109() V110() V111() V112() V113() V114() V115() non-increasing set

{(intloc 0)} is non empty V38() countable set

{(intloc 0)} --> 1 is Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued RAT -valued INT -valued {1} -valued Function-like constant non empty total V18({(intloc 0)},{1}) V38() countable V109() V110() V111() V112() Element of K27(K28({(intloc 0)},{1}))

{1} is non empty V38() countable V71() V72() set

K28({(intloc 0)},{1}) is Relation-like V38() countable set

K27(K28({(intloc 0)},{1})) is cup-closed diff-closed preBoolean V38() V42() countable set

Initialize K570((intloc 0),1) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable 0 -started set

Start-At (0,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty V38() countable 0 -started set

(IC ) .--> 0 is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V12() V38() countable Function-yielding V102() V109() V110() V111() V112() V113() V114() V115() non-increasing set

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

{(IC )} --> 0 is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued {0} -valued Function-like constant non empty total V18({(IC )},{0}) V38() countable Function-yielding V102() V109() V110() V111() V112() Element of K27(K28({(IC )},{0}))

{0} is functional non empty V38() V42() with_common_domain countable set

K28({(IC )},{0}) is Relation-like V38() countable set

K27(K28({(IC )},{0})) is cup-closed diff-closed preBoolean V38() V42() countable set

K570((intloc 0),1) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty V38() countable 0 -started set

UsedIntLoc (Stop SCM+FSA) is V38() countable Element of K27(Int-Locations)

UsedInt*Loc (Stop SCM+FSA) is V38() countable Element of K27(FinSeq-Locations)

K447(NAT,0,1) is non empty V38() countable Element of K27(NAT)

K210() is non empty Element of K27(K209())

(intloc 0) .--> 1 is 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 K297(3,SCM+FSA) -compatible V12() V38() countable data-only V109() V110() V111() V112() V113() V114() V115() non-increasing set

Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable 0 -started set

((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty V38() countable 0 -started set

dom (Initialize ((intloc 0) .--> 1)) is V38() countable set

Sorting-Function is Relation-like FinPartSt SCM+FSA -defined FinPartSt SCM+FSA -valued Function-like Function-yielding V102() Element of K27(K28((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 V71() 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 non empty V38() countable V78() set

a2 is V70() Element of the carrier of SCM+FSA

a1 is V70() Element of the carrier of SCM+FSA

Times (a1,a0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() non halt-free set

Goto 2 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() halt-free V88( SCM+FSA ) good set

SubFrom (a1,(intloc 0)) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

a0 ";" (SubFrom (a1,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() set

if=0 (a1,(Goto 2),(a0 ";" (SubFrom (a1,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() non halt-free set

loop (if=0 (a1,(Goto 2),(a0 ";" (SubFrom (a1,(intloc 0)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() halt-free V88( SCM+FSA ) set

Directed ((if=0 (a1,(Goto 2),(a0 ";" (SubFrom (a1,(intloc 0)))))),0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable V78() halt-free set

if>0 (a1,(loop (if=0 (a1,(Goto 2),(a0 ";" (SubFrom (a1,(intloc 0))))))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() non halt-free set

a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

a1 is FinSeq-Location

a0 . a1 is Relation-like NAT -defined INT -valued Function-like V38() FinSequence-like FinSubsequence-like countable V109() V110() V111() FinSequence of INT

a3 is V70() Element of the carrier of SCM+FSA

a2 is V70() Element of the carrier of SCM+FSA

a3 := (a1,a2) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a1,a2*> is Relation-like NAT -defined Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*a3,a1,a2*>) is set

Exec ((a3 := (a1,a2)),a0) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA) is functional with_common_domain product-like set

K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is functional non empty set

the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Function-yielding V102() Element of K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is cup-closed diff-closed preBoolean set

the Execution of SCM+FSA . (a3 := (a1,a2)) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . (a3 := (a1,a2))) . a0 is set

(Exec ((a3 := (a1,a2)),a0)) . a3 is ext-real V36() V37() integer set

a0 . a2 is ext-real V36() V37() integer set

abs (a0 . a2) is ext-real V36() V37() Element of REAL

(a0 . a1) /. (abs (a0 . a2)) is ext-real V36() V37() integer Element of INT

a4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

(a0 . a1) /. a4 is ext-real V36() V37() integer Element of INT

a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

a1 is FinSeq-Location

a0 . a1 is Relation-like NAT -defined INT -valued Function-like V38() FinSequence-like FinSubsequence-like countable V109() V110() V111() FinSequence of INT

a3 is V70() Element of the carrier of SCM+FSA

a2 is V70() Element of the carrier of SCM+FSA

(a1,a2) := a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a1,a2*> is Relation-like NAT -defined Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like countable set

K50(10,{},<*a3,a1,a2*>) is set

Exec (((a1,a2) := a3),a0) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA) is functional with_common_domain product-like set

K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is functional non empty set

the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Function-yielding V102() Element of K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is cup-closed diff-closed preBoolean set

the Execution of SCM+FSA . ((a1,a2) := a3) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . ((a1,a2) := a3)) . a0 is set

(Exec (((a1,a2) := a3),a0)) . a1 is Relation-like NAT -defined INT -valued Function-like V38() FinSequence-like FinSubsequence-like countable V109() V110() V111() FinSequence of INT

a0 . a2 is ext-real V36() V37() integer set

abs (a0 . a2) is ext-real V36() V37() Element of REAL

a0 . a3 is ext-real V36() V37() integer set

(a0 . a1) +* ((abs (a0 . a2)),(a0 . a3)) is Relation-like Function-like set

a4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

(a0 . a1) +* (a4,(a0 . a3)) is Relation-like Function-like set

a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Initialized a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total 0 -started set

a0 +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty total 0 -started set

a1 is FinSeq-Location

a2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a3 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

intloc a2 is V70() Element of the carrier of SCM+FSA

K342(a2) is V70() Element of the carrier of K333()

intloc (a3 + 1) is V70() non read-only Element of the carrier of SCM+FSA

K342((a3 + 1)) is V70() Element of the carrier of K333()

a0 . (intloc (a3 + 1)) is ext-real V36() V37() integer set

a4 is V70() Element of the carrier of SCM+FSA

(intloc a2) := (a1,a4) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*(intloc a2),a1,a4*> is Relation-like NAT -defined Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*(intloc a2),a1,a4*>) is set

Exec (((intloc a2) := (a1,a4)),(Initialized a0)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA) is functional with_common_domain product-like set

K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is functional non empty set

the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Function-yielding V102() Element of K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is cup-closed diff-closed preBoolean set

the Execution of SCM+FSA . ((intloc a2) := (a1,a4)) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . ((intloc a2) := (a1,a4))) . (Initialized a0) is set

(Exec (((intloc a2) := (a1,a4)),(Initialized a0))) . (intloc (a3 + 1)) is ext-real V36() V37() integer set

(Initialized a0) . (intloc (a3 + 1)) is ext-real V36() V37() integer set

a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Initialized a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total 0 -started set

a0 +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty total 0 -started set

a1 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a2 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

intloc a1 is V70() Element of the carrier of SCM+FSA

K342(a1) is V70() Element of the carrier of K333()

intloc (a2 + 1) is V70() non read-only Element of the carrier of SCM+FSA

K342((a2 + 1)) is V70() Element of the carrier of K333()

a0 . (intloc (a2 + 1)) is ext-real V36() V37() integer set

a3 is V70() Element of the carrier of SCM+FSA

(intloc a1) := a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Exec (((intloc a1) := a3),(Initialized a0)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA) is functional with_common_domain product-like set

K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is functional non empty set

the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Function-yielding V102() Element of K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is cup-closed diff-closed preBoolean set

the Execution of SCM+FSA . ((intloc a1) := a3) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . ((intloc a1) := a3)) . (Initialized a0) is set

(Exec (((intloc a1) := a3),(Initialized a0))) . (intloc (a2 + 1)) is ext-real V36() V37() integer set

(Initialized a0) . (intloc (a2 + 1)) is ext-real V36() V37() integer set

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set

a1 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

IExec ((Stop SCM+FSA),a0,a1) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

a2 is FinSeq-Location

(IExec ((Stop SCM+FSA),a0,a1)) . a2 is Relation-like NAT -defined INT -valued Function-like V38() FinSequence-like FinSubsequence-like countable V109() V110() V111() FinSequence of INT

a1 . a2 is Relation-like NAT -defined INT -valued Function-like V38() FinSequence-like FinSubsequence-like countable V109() V110() V111() FinSequence of INT

a3 is V70() non read-only Element of the carrier of SCM+FSA

(IExec ((Stop SCM+FSA),a0,a1)) . a3 is ext-real V36() V37() integer set

a1 . a3 is ext-real V36() V37() integer set

Initialized a1 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total 0 -started set

a1 +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty total 0 -started set

a1 +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty total 0 -started set

a1 +* ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Initialize (a1 +* ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total 0 -started set

(a1 +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible K297(3,SCM+FSA) -compatible non empty total 0 -started set

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedIntLoc a0 is V38() countable Element of K27(Int-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is V70() Element of the carrier of SCM+FSA

a3 is V70() Element of the carrier of SCM+FSA

a2 := a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

AddTo (a2,a3) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

SubFrom (a2,a3) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

MultBy (a2,a3) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Divide (a2,a3) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

UsedIntLoc a1 is V38() countable Element of Fin Int-Locations

{a2,a3} is non empty V38() countable Element of K27(Int-Locations)

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedIntLoc a0 is V38() countable Element of K27(Int-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is V70() Element of the carrier of SCM+FSA

a3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a2 =0_goto a3 is non ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

a2 >0_goto a3 is non ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

UsedIntLoc a1 is V38() countable Element of Fin Int-Locations

{a2} is non empty V38() countable Element of K27(Int-Locations)

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedIntLoc a0 is V38() countable Element of K27(Int-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is FinSeq-Location

a3 is V70() Element of the carrier of SCM+FSA

a4 is V70() Element of the carrier of SCM+FSA

a3 := (a2,a4) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a2,a4*> is Relation-like NAT -defined Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*a3,a2,a4*>) is set

(a2,a4) := a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*a3,a2,a4*>) is set

UsedIntLoc a1 is V38() countable Element of Fin Int-Locations

{a4,a3} is non empty V38() countable Element of K27(Int-Locations)

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedInt*Loc a0 is V38() countable Element of K27(FinSeq-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is FinSeq-Location

a3 is V70() Element of the carrier of SCM+FSA

a4 is V70() Element of the carrier of SCM+FSA

a3 := (a2,a4) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a2,a4*> is Relation-like NAT -defined Function-like non empty V38() 3 -element FinSequence-like FinSubsequence-like countable set

K50(9,{},<*a3,a2,a4*>) is set

(a2,a4) := a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(10,{},<*a3,a2,a4*>) is set

UsedInt*Loc a1 is V38() countable Element of Fin FinSeq-Locations

{a2} is non empty V38() countable set

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedIntLoc a0 is V38() countable Element of K27(Int-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is FinSeq-Location

a3 is V70() Element of the carrier of SCM+FSA

a3 :=len a2 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a2*> is Relation-like NAT -defined Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*a3,a2*>) is set

a2 :=<0,...,0> a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*a3,a2*>) is set

UsedIntLoc a1 is V38() countable Element of Fin Int-Locations

{a3} is non empty V38() countable Element of K27(Int-Locations)

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

rng a0 is V38() countable set

UsedInt*Loc a0 is V38() countable Element of K27(FinSeq-Locations)

a1 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a2 is FinSeq-Location

a3 is V70() Element of the carrier of SCM+FSA

a3 :=len a2 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

<*a3,a2*> is Relation-like NAT -defined Function-like non empty V38() 2 -element FinSequence-like FinSubsequence-like countable set

K50(11,{},<*a3,a2*>) is set

a2 :=<0,...,0> a3 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K50(12,{},<*a3,a2*>) is set

UsedInt*Loc a1 is V38() countable Element of Fin FinSeq-Locations

{a2} is non empty V38() countable set

a0 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

dom a0 is V38() countable set

a1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() set

UsedInt*Loc a1 is V38() countable Element of K27(FinSeq-Locations)

(dom a0) \/ (UsedInt*Loc a1) is V38() countable set

UsedIntLoc a1 is V38() countable Element of K27(Int-Locations)

((dom a0) \/ (UsedInt*Loc a1)) \/ (UsedIntLoc a1) is V38() countable set

a2 is set

a0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set

a1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set

a2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a4 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

dom a4 is V38() countable set

a5 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V38() countable V78() set

dom a5 is non empty V38() countable set

UsedInt*Loc a5 is V38() countable Element of K27(FinSeq-Locations)

(dom a4) \/ (UsedInt*Loc a5) is V38() countable set

UsedIntLoc a5 is V38() countable Element of K27(Int-Locations)

((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) is V38() countable set

a6 is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

initializeWorkMem is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Comput (a0,a6,a3) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a0,a6,a3)) . (IC ) is set

Comput (a1,initializeWorkMem,a3) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a1,initializeWorkMem,a3)) . (IC ) is set

(Comput (a0,a6,a3)) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,a3)) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

Comput (a0,a6,a2) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a0,a6,a2)) . (IC ) is set

Comput (a1,initializeWorkMem,a2) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a1,initializeWorkMem,a2)) . (IC ) is set

(Comput (a0,a6,a2)) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,a2)) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

b2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer set

a3 + b2 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

b3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a3 + b3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

(dom a4) \/ (UsedIntLoc a5) is V38() countable set

((dom a4) \/ (UsedIntLoc a5)) \/ (UsedInt*Loc a5) is V38() countable set

a3 + 0 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

Comput (a0,a6,(a3 + 0)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a0,a6,(a3 + 0))) . (IC ) is set

Comput (a1,initializeWorkMem,(a3 + 0)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a1,initializeWorkMem,(a3 + 0))) . (IC ) is set

(Comput (a0,a6,(a3 + 0))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + 0))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

b4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a3 + b4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

Comput (a0,a6,(a3 + b4)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a0,a6,(a3 + b4))) . (IC ) is set

Comput (a1,initializeWorkMem,(a3 + b4)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

(Comput (a1,initializeWorkMem,(a3 + b4))) . (IC ) is set

(Comput (a0,a6,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

b4 + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

a3 + (b4 + 1) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

Comput (a0,a6,(a3 + (b4 + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

CurInstr (a0,(Comput (a0,a6,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput (a0,a6,(a3 + b4))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a0 /. (IC (Comput (a0,a6,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Comput (a1,initializeWorkMem,(a3 + (b4 + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

CurInstr (a1,(Comput (a1,initializeWorkMem,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput (a1,initializeWorkMem,(a3 + b4))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

a1 /. (IC (Comput (a1,initializeWorkMem,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a1 . (IC (Comput (a1,initializeWorkMem,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a0 . (IC (Comput (a0,a6,(a3 + b4)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

a5 . (IC (Comput (a0,a6,(a3 + b4)))) is set

rng a5 is non empty V38() countable set

a1 | (dom a5) is Relation-like dom a5 -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

(a1 | (dom a5)) . (IC (Comput (a1,initializeWorkMem,(a3 + b4)))) is set

a0 | (dom a5) is Relation-like dom a5 -defined NAT -defined the InstructionsF of SCM+FSA -valued Function-like V38() countable set

(a0 | (dom a5)) . (IC (Comput (a0,a6,(a3 + b4)))) is set

(a3 + b4) + 1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() Element of NAT

Comput (a0,a6,((a3 + b4) + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Following (a0,(Comput (a0,a6,(a3 + b4)))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Exec ((CurInstr (a0,(Comput (a0,a6,(a3 + b4))))),(Comput (a0,a6,(a3 + b4)))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA) is functional with_common_domain product-like set

K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is functional non empty set

the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) -valued Function-like non empty total V18( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Function-yielding V102() Element of K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K27(K28( the InstructionsF of SCM+FSA,K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is cup-closed diff-closed preBoolean set

the Execution of SCM+FSA . (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . (CurInstr (a0,(Comput (a0,a6,(a3 + b4)))))) . (Comput (a0,a6,(a3 + b4))) is set

Comput (a1,initializeWorkMem,((a3 + b4) + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Following (a1,(Comput (a1,initializeWorkMem,(a3 + b4)))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

Exec ((CurInstr (a1,(Comput (a1,initializeWorkMem,(a3 + b4))))),(Comput (a1,initializeWorkMem,(a3 + b4)))) is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible non empty total set

the Execution of SCM+FSA . (CurInstr (a1,(Comput (a1,initializeWorkMem,(a3 + b4))))) is Relation-like Function-like Element of K78((product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

( the Execution of SCM+FSA . (CurInstr (a1,(Comput (a1,initializeWorkMem,(a3 + b4)))))) . (Comput (a1,initializeWorkMem,(a3 + b4))) is set

dom (Comput (a0,a6,(a3 + (b4 + 1)))) is non empty set

dom (Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) is non empty set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is V70() Element of the carrier of SCM+FSA

i5 is V70() Element of the carrier of SCM+FSA

i4 := i5 is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a0,a6,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is V70() Element of the carrier of SCM+FSA

i5 is V70() Element of the carrier of SCM+FSA

AddTo (i4,i5) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a0,a6,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i4 is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) . i4) + ((Comput (a1,initializeWorkMem,(a3 + b4))) . i5) is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i4 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i4 is set

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is V70() Element of the carrier of SCM+FSA

i5 is V70() Element of the carrier of SCM+FSA

SubFrom (i4,i5) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a0,a6,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i4 is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) . i4) - ((Comput (a1,initializeWorkMem,(a3 + b4))) . i5) is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i4 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i4 is set

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is V70() Element of the carrier of SCM+FSA

i5 is V70() Element of the carrier of SCM+FSA

MultBy (i4,i5) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a0,a6,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i4 is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) . i4) * ((Comput (a1,initializeWorkMem,(a3 + b4))) . i5) is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i4 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i4 is set

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is V70() Element of the carrier of SCM+FSA

i5 is V70() Element of the carrier of SCM+FSA

Divide (i4,i5) is ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a0,a6,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a0,a6,(a3 + b4))) . i4 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i4 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i4 is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

((Comput (a0,a6,(a3 + b4))) . i4) div ((Comput (a0,a6,(a3 + b4))) . i5) is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

((Comput (a0,a6,(a3 + b4))) . i4) mod ((Comput (a0,a6,(a3 + b4))) . i5) is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

((Comput (a0,a6,(a3 + b4))) . i4) mod ((Comput (a0,a6,(a3 + b4))) . i4) is ext-real V36() V37() integer set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

goto i4 is non ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K339(i4) is Element of the InstructionsF of K333()

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i5 is set

(Comput (a0,a6,(a3 + b4))) . i5 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i5 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i5 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i5 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K58( the InstructionsF of SCM+FSA) is set

i4 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of NAT

i5 is V70() Element of the carrier of SCM+FSA

i5 =0_goto i4 is non ins-loc-free V84( the InstructionsF of SCM+FSA) V97(3, SCM+FSA ) with_explicit_jumps IC-relocable good V129(3, SCM+FSA ) V131(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (a0,a6,(a3 + b4))) . i5 is ext-real V36() V37() integer set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i5 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i5 is ext-real V36() V37() integer set

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

succ (IC (Comput (a1,initializeWorkMem,(a3 + b4)))) is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer V71() set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . (IC ) is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . (IC ) is set

i6 is set

(Comput (a0,a6,(a3 + b4))) . i6 is set

((Comput (a1,initializeWorkMem,(a3 + b4))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + b4))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) . i6 is set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) . i6 is set

(Comput (a0,a6,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

(Comput (a1,initializeWorkMem,(a3 + (b4 + 1)))) | (((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5)) is Relation-like the carrier of SCM+FSA -defined ((dom a4) \/ (UsedInt*Loc a5)) \/ (UsedIntLoc a5) -defined the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible V38() countable set

InsCode (CurInstr (a0,(Comput (a0,a6,(a3 + b4))))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() V37() integer Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of