:: 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₁ where b₁ is Relation-like the carrier of SCM+FSA -defined Function-like K297(3,SCM+FSA) -compatible Element of sproduct K297(3,SCM+FSA) : b₁ is V38() } is set
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