:: SFMASTR3 semantic presentation

REAL is non empty V12() V40() V46() set
NAT is non empty V12() V26() V27() V28() V40() V46() countable denumerable Element of K27(REAL)
K27(REAL) is non empty set
SCM+FSA is V89() with_non-empty_values IC-Ins-separated strict V112(3) AMI-Struct over 3
3 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
the U2 of SCM+FSA is set
COMPLEX is non empty V12() V40() V46() set
NAT is non empty V12() V26() V27() V28() V40() V46() countable denumerable set
K27(NAT) is non empty set
K28(NAT,REAL) is non empty set
K27(K28(NAT,REAL)) is non empty set
K27(K27(REAL)) is non empty set
RAT is non empty V12() V40() V46() set
K27(RAT) is non empty set
ExtREAL is non empty set
K27(NAT) is non empty set
9 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
Segm 9 is countable Element of K27(NAT)
Int-Locations is non empty set
K364() is set
K27(K364()) is non empty set
2 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
K28(K364(),2) is set
K27(K28(K364(),2)) is non empty set
K366() is Relation-like K364() -defined 2 -valued Function-like total quasi_total Element of K27(K28(K364(),2))
K367() is Relation-like 2 -defined Function-like non empty total set
K366() * K367() is Relation-like Function-like set
product (K366() * K367()) is functional with_common_domain product-like set
K358() is non empty set
Funcs ((product (K366() * K367())),(product (K366() * K367()))) is functional non empty set
K28(K358(),(Funcs ((product (K366() * K367())),(product (K366() * K367()))))) is non empty set
K27(K28(K358(),(Funcs ((product (K366() * K367())),(product (K366() * K367())))))) is non empty set
K27( the U2 of SCM+FSA) is non empty set
the InstructionsF of SCM+FSA is Relation-like non empty standard-ins V79() J/A-independent V82() set
INT is non empty V12() V40() V46() set
the_Values_of SCM+FSA is Relation-like non-empty the U2 of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like the U2 of SCM+FSA -defined 3 -valued Function-like total quasi_total Element of K27(K28( the U2 of SCM+FSA,3))
K28( the U2 of SCM+FSA,3) is set
K27(K28( the U2 of SCM+FSA,3)) is non empty set
the ValuesF of SCM+FSA is Relation-like 3 -defined Function-like non empty total set
the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA is Relation-like Function-like set
Int-Locations is non empty Element of K27( the U2 of SCM+FSA)
K27(Int-Locations) is non empty set
K28(NAT,K27(NAT)) is non empty set
K27(K28(NAT,K27(NAT))) is non empty set
FinPartSt SCM+FSA is functional non empty Element of K27((sproduct (the_Values_of SCM+FSA)))
sproduct (the_Values_of SCM+FSA) is functional non empty set
K27((sproduct (the_Values_of SCM+FSA))) is non empty set
{ b₁ where b₁ is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible Element of sproduct (the_Values_of SCM+FSA) : b₁ is V40() } is set
K28((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is non empty set
K27(K28((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is non empty set
product (the_Values_of SCM+FSA) is functional non empty with_common_domain product-like set
K28(NAT,(product (the_Values_of SCM+FSA))) is non empty set
K27(K28(NAT,(product (the_Values_of SCM+FSA)))) is non empty set
K96(Int-Locations) is V24() set
FinSeq-Locations is non empty V12() V40() V46() Element of K27( the U2 of SCM+FSA)
K96(FinSeq-Locations) is V24() set
K27(FinSeq-Locations) is non empty set
1 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
{} is Function-like functional empty V26() V27() V28() V30() V31() V32() V33() V34() V35() ext-real non positive non negative V40() V44() countable FinSequence-membered set
0 is Function-like functional empty V26() V27() V28() V30() V31() V32() V33() V34() V35() ext-real non positive non negative V40() V44() countable FinSequence-membered Element of NAT
K127(1) is V33() V34() V35() ext-real non positive Element of REAL
4 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
5 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
7 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
8 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
10 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
12 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
IC is Element of the U2 of SCM+FSA
Data-Locations is Element of K27( the U2 of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K27( the U2 of SCM+FSA)
intloc 0 is V115() read-only Element of the U2 of SCM+FSA
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant non empty V12() V30() V40() countable V77() non halt-free V86( SCM+FSA ) V87( SCM+FSA ) keeping_0 good paraclosed parahalting set
halt SCM+FSA is V111(3, SCM+FSA ) parahalting keeping_0 Element of the InstructionsF of SCM+FSA
halt the InstructionsF of SCM+FSA is ins-loc-free Element of the InstructionsF of SCM+FSA
K298((halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
Goto 0 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() halt-free V87( SCM+FSA ) good set
goto 0 is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) good Element of the InstructionsF of SCM+FSA
Start-At (0,SCM+FSA) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible non empty V40() countable 0 -started set
(IC ) .--> 0 is Relation-like {(IC )} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant V12() V40() countable V60() V61() V62() V63() V64() V65() V66() V67() set
{(IC )} is non empty V40() countable set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
Initialized s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(intloc 0) .--> 1 is Relation-like {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant the_Values_of SCM+FSA -compatible V12() V40() countable V60() V61() V62() V63() V64() V65() V66() V67() set
{(intloc 0)} is non empty V40() countable set
Initialize ((intloc 0) .--> 1) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() Element of the U2 of SCM+FSA
(Initialized s) . f is V33() V34() V35() ext-real set
p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
minpos is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
IExec (p,minpos,s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(IExec (p,minpos,s)) . f is V33() V34() V35() ext-real set
DataPart (Initialized s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Initialized s) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialize (Initialized s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Initialized s) +* (Start-At (0,SCM+FSA)) is Relation-like the U2 of SCM+FSA -defined the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible non empty total 0 -started set
DataPart (Initialize (Initialized s)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Initialize (Initialized s)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
minpos +* p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
Comput ((minpos +* p),(Initialize (Initialized s)),0) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((minpos +* p),(Initialize (Initialized s)),0)) . f is V33() V34() V35() ext-real set
(Initialize (Initialized s)) . f is V33() V34() V35() ext-real set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is V33() V34() V35() ext-real set
DataPart s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
s | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
f is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
IExec ((Stop SCM+FSA),f,s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
DataPart (IExec ((Stop SCM+FSA),f,s)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(IExec ((Stop SCM+FSA),f,s)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Initialized s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(intloc 0) .--> 1 is Relation-like {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant the_Values_of SCM+FSA -compatible V12() V40() countable V60() V61() V62() V63() V64() V65() V66() V67() set
{(intloc 0)} is non empty V40() countable set
Initialize ((intloc 0) .--> 1) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Initialized s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Initialized s) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s is V115() Element of the U2 of SCM+FSA
rng (Stop SCM+FSA) is V12() V40() countable set
{(halt SCM+FSA)} is non empty V40() countable set
f is Element of the InstructionsF of SCM+FSA
s is V115() Element of the U2 of SCM+FSA
f is V115() Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
p := f is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
minpos is V115() Element of the U2 of SCM+FSA
minpos := s is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
InsCode (p := f) is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
AddTo (minpos,s) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
SubFrom (minpos,s) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
MultBy (minpos,s) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
Divide (s,minpos) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
Divide (minpos,s) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
cv is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
s =0_goto cv is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) good Element of the InstructionsF of SCM+FSA
s >0_goto cv is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) good Element of the InstructionsF of SCM+FSA
S is FinSeq-Location
minpos := (S,s) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
(S,minpos) := s is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(S,s) := minpos is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
S :=<0,...,0> s is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
abs (s . p) is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
minpos is FinSeq-Location
f := (minpos,p) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
Exec ((f := (minpos,p)),s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))))))
K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))))) is non empty set
K27(K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)))))) is non empty set
the Execution of SCM+FSA . (f := (minpos,p)) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . (f := (minpos,p))) . s is set
(Exec ((f := (minpos,p)),s)) . f is V33() V34() V35() ext-real set
s . minpos is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
(s . minpos) /. (abs (s . p)) is V33() V34() V35() ext-real Element of INT
cv is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
(s . minpos) /. cv is V33() V34() V35() ext-real Element of INT
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() Element of the U2 of SCM+FSA
s . f is V33() V34() V35() ext-real set
abs (s . f) is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is FinSeq-Location
(minpos,f) := p is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
Exec (((minpos,f) := p),s) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA) is functional with_common_domain product-like set
Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))) is functional non empty set
the Execution of SCM+FSA is Relation-like the InstructionsF of SCM+FSA -defined Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))))))
K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA))))) is non empty set
K27(K28( the InstructionsF of SCM+FSA,(Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)))))) is non empty set
the Execution of SCM+FSA . ((minpos,f) := p) is Relation-like Function-like Element of Funcs ((product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)),(product ( the Object-Kind of SCM+FSA * the ValuesF of SCM+FSA)))
( the Execution of SCM+FSA . ((minpos,f) := p)) . s is set
(Exec (((minpos,f) := p),s)) . minpos is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
s . minpos is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
(s . minpos) +* ((abs (s . f)),(s . p)) is Relation-like Function-like V60() V61() V62() set
cv is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
(s . minpos) +* (cv,(s . p)) is Relation-like Function-like V60() V61() V62() set
s is V115() non read-only Element of the U2 of SCM+FSA
f is V115() Element of the U2 of SCM+FSA
p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() good set
minpos is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() good set
if>0 (s,f,p,minpos) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
SubFrom (s,f) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
if>0 (s,p,minpos) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free good set
(SubFrom (s,f)) ";" (if>0 (s,p,minpos)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() good set
Macro (SubFrom (s,f)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom (s,f))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom (s,f)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom (s,f))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(Macro (SubFrom (s,f))) ";" (if>0 (s,p,minpos)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free good set
s is V115() Element of the U2 of SCM+FSA
f is V115() Element of the U2 of SCM+FSA
{s,f} is non empty V40() countable Element of K27(Int-Locations)
p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
UsedIntLoc p is V40() countable Element of K27(Int-Locations)
{s,f} \/ (UsedIntLoc p) is non empty V40() countable Element of K27(Int-Locations)
minpos is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
if>0 (s,f,p,minpos) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
UsedIntLoc (if>0 (s,f,p,minpos)) is V40() countable Element of K27(Int-Locations)
UsedIntLoc minpos is V40() countable Element of K27(Int-Locations)
({s,f} \/ (UsedIntLoc p)) \/ (UsedIntLoc minpos) is non empty V40() countable Element of K27(Int-Locations)
SubFrom (s,f) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
if>0 (s,p,minpos) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
(SubFrom (s,f)) ";" (if>0 (s,p,minpos)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom (s,f)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() paraclosed parahalting set
K326(SCM+FSA,(SubFrom (s,f))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom (s,f)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom (s,f))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(Macro (SubFrom (s,f))) ";" (if>0 (s,p,minpos)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
UsedIntLoc ((SubFrom (s,f)) ";" (if>0 (s,p,minpos))) is V40() countable Element of K27(Int-Locations)
UsedIntLoc (SubFrom (s,f)) is Element of K96(Int-Locations)
UsedIntLoc (if>0 (s,p,minpos)) is V40() countable Element of K27(Int-Locations)
(UsedIntLoc (SubFrom (s,f))) \/ (UsedIntLoc (if>0 (s,p,minpos))) is set
{s,f} \/ (UsedIntLoc (if>0 (s,p,minpos))) is non empty V40() countable Element of K27(Int-Locations)
{s} is non empty V40() countable Element of K27(Int-Locations)
{s} \/ (UsedIntLoc p) is non empty V40() countable Element of K27(Int-Locations)
({s} \/ (UsedIntLoc p)) \/ (UsedIntLoc minpos) is non empty V40() countable Element of K27(Int-Locations)
{s,f} \/ (({s} \/ (UsedIntLoc p)) \/ (UsedIntLoc minpos)) is non empty V40() countable Element of K27(Int-Locations)
(UsedIntLoc p) \/ (UsedIntLoc minpos) is V40() countable Element of K27(Int-Locations)
{s} \/ ((UsedIntLoc p) \/ (UsedIntLoc minpos)) is non empty V40() countable Element of K27(Int-Locations)
{s,f} \/ ({s} \/ ((UsedIntLoc p) \/ (UsedIntLoc minpos))) is non empty V40() countable Element of K27(Int-Locations)
{s,f} \/ {s} is non empty V40() countable Element of K27(Int-Locations)
({s,f} \/ {s}) \/ ((UsedIntLoc p) \/ (UsedIntLoc minpos)) is non empty V40() countable Element of K27(Int-Locations)
{s,f} \/ ((UsedIntLoc p) \/ (UsedIntLoc minpos)) is non empty V40() countable Element of K27(Int-Locations)
s is V115() Element of the U2 of SCM+FSA
f is V115() Element of the U2 of SCM+FSA
p is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
while>0 (f,p) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
card p is V26() V27() V28() V32() V33() V34() V35() ext-real non negative Element of NAT
dom p is V26() V27() V28() V32() V33() V34() V35() ext-real non negative V40() countable set
(card p) + 4 is non empty V26() V27() V28() V32() V33() V34() V35() ext-real positive non negative V45() Element of NAT
((card p) + 4) .--> (goto 0) is Relation-like NAT -defined {((card p) + 4)} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V12() V40() countable set
{((card p) + 4)} is non empty V40() V45() V46() countable set
p ";" (Goto 0) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
if>0 (f,(p ";" (Goto 0)),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
(if>0 (f,(p ";" (Goto 0)),(Stop SCM+FSA))) +* (((card p) + 4) .--> (goto 0)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V40() countable set
s is V115() Element of the U2 of SCM+FSA
f is V115() Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
minpos is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
if>0 (f,p,minpos,cv) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
SubFrom (f,p) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
if>0 (f,minpos,cv) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
(SubFrom (f,p)) ";" (if>0 (f,minpos,cv)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom (f,p)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() paraclosed parahalting set
K326(SCM+FSA,(SubFrom (f,p))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom (f,p)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom (f,p))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(Macro (SubFrom (f,p))) ";" (if>0 (f,minpos,cv)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() non halt-free set
S is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
minpos is V115() Element of the U2 of SCM+FSA
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
S . minpos is V33() V34() V35() ext-real set
S . p is V33() V34() V35() ext-real set
(S . minpos) - (S . p) is V33() V34() V35() ext-real set
((S . minpos) - (S . p)) + 1 is V33() V34() V35() ext-real set
S +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((S . minpos) - (S . p)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(S +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((S . minpos) - (S . p)) + 1))) +* (f,(S . p)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting Element of the InstructionsF of SCM+FSA
cv ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
cv ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(cv ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),s,((S +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((S . minpos) - (S . p)) + 1))) +* (f,(S . p)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is V33() V34() V35() ext-real set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
minpos is V115() Element of the U2 of SCM+FSA
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(S,f,p,minpos,cv,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
s . minpos is V33() V34() V35() ext-real set
s . p is V33() V34() V35() ext-real set
(s . minpos) - (s . p) is V33() V34() V35() ext-real set
((s . minpos) - (s . p)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
cv ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
cv ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(cv ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),S,((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(S,f,p,minpos,cv,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((S,f,p,minpos,cv,s) . 0) . (intloc 0) is V33() V34() V35() ext-real set
((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p))) . (intloc 0) is V33() V34() V35() ext-real set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) . (intloc 0) is V33() V34() V35() ext-real set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is V115() Element of the U2 of SCM+FSA
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(S,f,p,minpos,cv,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
s . minpos is V33() V34() V35() ext-real set
(s . minpos) - (s . p) is V33() V34() V35() ext-real set
((s . minpos) - (s . p)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
cv ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
cv ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(cv ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),S,((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(S,f,p,minpos,cv,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((S,f,p,minpos,cv,s) . 0) . f is V33() V34() V35() ext-real set
(StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),S,((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p))))) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
dom (s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) is set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is V115() Element of the U2 of SCM+FSA
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(S,f,p,minpos,cv,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
s . minpos is V33() V34() V35() ext-real set
(s . minpos) - (s . p) is V33() V34() V35() ext-real set
((s . minpos) - (s . p)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
cv ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
cv ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(cv ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(intloc 0)))),S,((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(S,f,p,minpos,cv,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((S,f,p,minpos,cv,s) . 0) . p is V33() V34() V35() ext-real set
((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p))) . p is V33() V34() V35() ext-real set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv))),(((s . minpos) - (s . p)) + 1))) . p is V33() V34() V35() ext-real set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is V115() Element of the U2 of SCM+FSA
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(S,f,minpos,p,cv,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,minpos,p} is non empty V40() countable Element of K27(Int-Locations)
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,minpos,p} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
s . minpos is V33() V34() V35() ext-real set
(s . p) - (s . minpos) is V33() V34() V35() ext-real set
((s . p) - (s . minpos)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(((s . p) - (s . minpos)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(((s . p) - (s . minpos)) + 1))) +* (f,(s . minpos)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
cv ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
cv ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(cv ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),((cv ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(intloc 0)))),S,((s +* ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(((s . p) - (s . minpos)) + 1))) +* (f,(s . minpos)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(S,f,minpos,p,cv,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((S,f,minpos,p,cv,s) . 0) . p is V33() V34() V35() ext-real set
((s +* ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(((s . p) - (s . minpos)) + 1))) +* (f,(s . minpos))) . p is V33() V34() V35() ext-real set
(s +* ((1 -thRWNotIn ({f,minpos,p} \/ (UsedIntLoc cv))),(((s . p) - (s . minpos)) + 1))) . p is V33() V34() V35() ext-real set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is V115() Element of the U2 of SCM+FSA
cv is V115() Element of the U2 of SCM+FSA
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
UsedIntLoc S is V40() countable Element of K27(Int-Locations)
I22 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(I22,f,minpos,cv,S,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,minpos,cv} is non empty V40() countable Element of K27(Int-Locations)
{f,minpos,cv} \/ (UsedIntLoc S) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S)) is V115() non read-only Element of the U2 of SCM+FSA
s . cv is V33() V34() V35() ext-real set
s . minpos is V33() V34() V35() ext-real set
(s . cv) - (s . minpos) is V33() V34() V35() ext-real set
((s . cv) - (s . minpos)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(((s . cv) - (s . minpos)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(((s . cv) - (s . minpos)) + 1))) +* (f,(s . minpos)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
S ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
S ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(S ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(S ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),((S ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(intloc 0)))),I22,((s +* ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(((s . cv) - (s . minpos)) + 1))) +* (f,(s . minpos)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(I22,f,minpos,cv,S,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((I22,f,minpos,cv,S,s) . 0) . p is V33() V34() V35() ext-real set
((s +* ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(((s . cv) - (s . minpos)) + 1))) +* (f,(s . minpos))) . p is V33() V34() V35() ext-real set
(s +* ((1 -thRWNotIn ({f,minpos,cv} \/ (UsedIntLoc S))),(((s . cv) - (s . minpos)) + 1))) . p is V33() V34() V35() ext-real set
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
minpos is V115() Element of the U2 of SCM+FSA
cv is FinSeq-Location
s . cv is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
I22 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
(I22,f,p,minpos,S,s) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
UsedIntLoc S is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc S) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S)) is V115() non read-only Element of the U2 of SCM+FSA
s . minpos is V33() V34() V35() ext-real set
s . p is V33() V34() V35() ext-real set
(s . minpos) - (s . p) is V33() V34() V35() ext-real set
((s . minpos) - (s . p)) + 1 is V33() V34() V35() ext-real set
s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(((s . minpos) - (s . p)) + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
AddTo (f,(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
S ";" (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (AddTo (f,(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(AddTo (f,(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(AddTo (f,(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
S ";" (Macro (AddTo (f,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0)) is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
(S ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() keeping_0 good paraclosed parahalting set
K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() 1 -element countable V77() set
K327(SCM+FSA,K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
K288(K326(SCM+FSA,(SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0)))),(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V40() countable V77() set
(S ";" (AddTo (f,(intloc 0)))) ";" (Macro (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
StepWhile>0 ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),((S ";" (AddTo (f,(intloc 0)))) ";" (SubFrom ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(intloc 0)))),I22,((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p)))) is Relation-like NAT -defined product (the_Values_of SCM+FSA) -valued Function-like non empty total quasi_total Function-yielding V122() Element of K27(K28(NAT,(product (the_Values_of SCM+FSA))))
(I22,f,p,minpos,S,s) . 0 is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total Element of product (the_Values_of SCM+FSA)
((I22,f,p,minpos,S,s) . 0) . cv is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
((s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(((s . minpos) - (s . p)) + 1))) +* (f,(s . p))) . cv is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
(s +* ((1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc S))),(((s . minpos) - (s . p)) + 1))) . cv is Relation-like NAT -defined INT -valued Function-like V40() countable V60() V61() V62() FinSequence-like FinSubsequence-like FinSequence of INT
s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
s . (intloc 0) is V33() V34() V35() ext-real set
f is V115() non read-only Element of the U2 of SCM+FSA
p is V115() Element of the U2 of SCM+FSA
f := p is V83( the InstructionsF of SCM+FSA) V111(3, SCM+FSA ) parahalting keeping_0 good Element of the InstructionsF of SCM+FSA
s . p is V33() V34() V35() ext-real set
minpos is V115() Element of the U2 of SCM+FSA
{f,p,minpos} is non empty V40() countable Element of K27(Int-Locations)
s . minpos is V33() V34() V35() ext-real set
(s . minpos) - (s . p) is V33() V34() V35() ext-real set
((s . minpos) - (s . p)) + 1 is V33() V34() V35() ext-real set
cv is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty V30() V40() countable V77() set
UsedIntLoc cv is V40() countable Element of K27(Int-Locations)
{f,p,minpos} \/ (UsedIntLoc cv) is non empty V40() countable Element of K27(Int-Locations)
1 -thRWNotIn ({f,p,minpos} \/ (UsedIntLoc cv)) is V115() non read-only Element of the U2 of SCM+FSA
S is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like non empty total set
Initialized s is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(intloc 0) .--> 1 is Relation-like {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued RAT -valued INT -valued Function-like one-to-one constant the_Values_of SCM+FSA -compatible V12() V40() countable V60() V61() V62() V63() V64() V65() V66() V67() set
{(intloc 0)} is non empty V40() countable set
Initialize ((intloc 0) .--> 1) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the U2 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible total set
(Initialized s) . minpos is V33() V34() V35() ext-real set
finish is V115() non read-only Element of the U2 of SCM+FSA
finish := minpos is V83( the InstructionsF of SCM+FSA) V